Theory RDR

section ‹Recoverable Data Types›

theory RDR
imports Main Sequences
begin

subsection ‹The pre-RDR locale contains definitions later used in the RDR locale 
  to state the properties of RDRs›

locale pre_RDR = Sequences +
  fixes δ::"'a ⇒ ('b × 'c) ⇒ 'a" (infix ‹∙› 65)
  and γ::"'a ⇒ ('b × 'c) ⇒ 'd"
  and bot::'a (‹⊥›)
begin

fun exec::"'a ⇒ ('b×'c)list ⇒ 'a" (infix ‹⋆› 65) where 
  "exec s Nil = s"
| "exec s (rs#r) = (exec s rs) ∙ r"

definition less_eq (infix ‹≼› 50) where
  "less_eq s s' ≡ ∃ rs . s' = (s⋆rs)"

definition less (infix ‹≺› 50) where
  "less s s' ≡ less_eq s s' ∧ s ≠ s'"

definition is_lb where
  "is_lb s s1 s2 ≡ s ≼ s2 ∧ s ≼ s1"

definition is_glb where
  "is_glb s s1 s2 ≡ is_lb s s1 s2 ∧ (∀ s' . is_lb s' s1 s2 ⟶ s' ≼ s)"
  
definition contains where
  "contains s r ≡ ∃ rs . r ∈ set rs ∧ s = (⊥ ⋆ rs)"

definition inf  (infix ‹⊓› 65) where
  "inf s1 s2 ≡ THE s . is_glb s s1 s2"

subsection ‹Useful Lemmas in the pre-RDR locale›

lemma exec_cons: 
  "s ⋆ (rs # r)= (s ⋆ rs) ∙ r" by simp

lemma exec_append: 
  "(s ⋆ rs) ⋆ rs'  = s ⋆ (rs@rs')"
proof (induct rs')
  show "(s ⋆ rs) ⋆ []  = s ⋆ (rs@[])" by simp
next
  fix rs' r
  assume ih:"(s ⋆ rs) ⋆ rs'  = s ⋆ (rs@rs')"
  thus "(s ⋆ rs) ⋆ (rs'#r)  = s ⋆ (rs @ (rs'#r))"
    by (metis append_Cons exec_cons)
qed

lemma trans:
  assumes "s1 ≼ s2" and "s2 ≼ s3"
  shows "s1 ≼ s3" using assms
    by (auto simp add:less_eq_def, metis exec_append)

lemma contains_star:
  fixes s r rs
  assumes "contains s r"
  shows "contains (s ⋆ rs) r"
proof (induct rs)
  case Nil
  show "contains (s ⋆ []) r" using assms by auto
next
  case (Cons r' rs)
  with this obtain rs' where 1:"s ⋆ rs = ⊥ ⋆ rs'" and 2:"r ∈ set rs'" 
    by (auto simp add:contains_def)
  have 3:"s ⋆ (rs#r') = ⊥⋆(rs'#r')" using 1 by fastforce
  show "contains (s ⋆ (rs#r')) r" using 2 3 
    by (auto simp add:contains_def) (metis exec_cons rev_subsetD set_subset_Cons)
qed

lemma preceq_star: "s ⋆ (rs#r) ≼ s' ⟹ s ⋆ rs ≼ s'"
by (metis pre_RDR.exec.simps(1) pre_RDR.exec.simps(2) pre_RDR.less_eq_def trans)

end

subsection ‹The RDR locale›

locale RDR = pre_RDR +
  assumes idem1:"contains s r ⟹ s ∙ r = s"
  and idem2:"⋀ s r r' . fst r ≠ fst r' ⟹ γ s r = γ ((s ∙ r) ∙ r') r"
  and antisym:"⋀ s1 s2 . s1 ≼ s2 ∧ s2 ≼ s1 ⟹ s1 = s2"
  and glb_exists:"⋀ s1 s2 . ∃ s . is_glb s s1 s2"
  and consistency:"⋀s1 s2 s3 rs . s1 ≼ s2 ⟹ s2 ≼ s3 ⟹ s3 = s1 ⋆ rs 
    ⟹ ∃ rs' rs'' . s2 = s1 ⋆ rs' ∧ s3 = s2 ⋆ rs'' 
      ∧ set rs' ⊆ set rs ∧ set rs'' ⊆ set rs"
  and bot:"⋀ s . ⊥ ≼ s"
begin

lemma inf_glb:"is_glb (s1 ⊓ s2) s1 s2"
proof -
  { fix s s'
    assume "is_glb s s1 s2" and "is_glb s' s1 s2"
    hence "s = s'" using antisym by (auto simp add:is_glb_def is_lb_def) }
    from this and glb_exists show ?thesis
      by (auto simp add:inf_def, metis (lifting) theI')
qed

sublocale ordering less_eq less
proof
  fix s
  show "s ≼ s"
  by (metis exec.simps(1) less_eq_def)
next
  fix s s'
  show "s ≺ s' = (s ≼ s' ∧ s ≠ s')" 
  by (auto simp add:less_def)
next
  fix s s'
  assume "s ≼ s'" and "s' ≼ s"
  thus "s = s'"
  using antisym by auto
next
  fix s1 s2 s3
  assume "s1 ≼ s2" and "s2 ≼ s3"
  thus "s1 ≼ s3"
  using trans by blast
qed

sublocale semilattice_set inf
proof
  fix s
  show "s ⊓ s = s" 
    using inf_glb
    by (metis antisym is_glb_def is_lb_def refl) 
next
  fix s1 s2
  show "s1 ⊓ s2 = (s2 ⊓ s1)"
    using inf_glb 
    by (smt antisym is_glb_def pre_RDR.is_lb_def)
next
  fix s1 s2 s3
  show "(s1 ⊓ s2) ⊓ s3 = (s1 ⊓ (s2 ⊓ s3))"
    using inf_glb 
    by(auto simp add:is_glb_def is_lb_def, smt antisym trans)
qed

sublocale semilattice_order_set inf less_eq less
proof 
  fix s s'
  show "s ≼ s' = (s = s ⊓ s')"
  by (metis antisym idem inf_glb pre_RDR.is_glb_def pre_RDR.is_lb_def)
next
  fix s s'
  show "s ≺ s' = (s = s ⊓ s' ∧ s ≠ s')"
  by (metis inf_glb local.antisym local.refl pre_RDR.is_glb_def pre_RDR.is_lb_def pre_RDR.less_def)
qed

notation F (‹⨅ _› [99])

subsection ‹Some useful lemmas›

lemma idem_star: 
fixes r s rs
assumes "contains s r"
shows "s ⋆ rs = s ⋆ (filter (λ x . x ≠ r) rs)"
proof (induct rs)
  case Nil
  show "s ⋆ [] = s ⋆ (filter (λ x . x ≠ r) [])" 
    using assms by auto
next
  case (Cons r' rs)
  have 1:"contains (s ⋆ rs) r" using assms and contains_star by auto
  show "s ⋆ (rs#r') = s ⋆ (filter (λ x . x ≠ r) (rs#r'))"
  proof (cases "r' = r")
    case True
    hence "s ⋆ (rs#r') = s ⋆ rs" using idem1 1 by auto
    thus ?thesis using Cons by simp
  next
    case False
    thus ?thesis using Cons by auto
  qed
qed

lemma idem_star2: 
  fixes s rs' 
  shows "∃ rs' . s ⋆ rs = s ⋆ rs' ∧ set rs' ⊆ set rs 
    ∧ (∀ r ∈ set rs' . ¬ contains s r)"
proof (induct rs)
  case Nil
  thus "∃ rs' . s ⋆ [] = s ⋆ rs' ∧ set rs' ⊆ set [] 
    ∧ (∀ r ∈ set rs' . ¬ contains s r)" by force
next
  case (Cons r rs)
  obtain rs' where 1:"s ⋆ rs = s ⋆ rs'" and 2:"set rs' ⊆ set rs"
  and 3:"∀ r ∈ set rs' . ¬ contains s r" using Cons(1) by blast
  show "∃ rs' . s ⋆ (rs#r) = s ⋆ rs' ∧ set rs' ⊆ set (rs#r)
    ∧ (∀ r ∈ set rs' . ¬ contains s r)"
  proof (cases "contains s r")
    case True
    have "s⋆(rs#r) = s⋆rs'"
    proof -
      have "s ⋆ (rs#r) = s⋆rs" using True
        by (metis contains_star exec_cons idem1)
      moreover
      have "s ⋆ (rs'#r) = s⋆rs'" using True
        by (metis contains_star exec_cons idem1) 
      ultimately show ?thesis using 1 by simp
    qed
    moreover have "set rs' ⊆ set (rs#r)" using 2 
      by (simp, metis subset_insertI2) 
    moreover have "∀ r ∈ set rs' . ¬ contains s r" 
      using 3 by assumption
    ultimately show ?thesis by blast
  next
    case False
    have "s⋆(rs#r) = s⋆(rs'#r)" using 1 by simp
    moreover
    have "set (rs'#r) ⊆ set (rs#r)" using 2 by auto
    moreover have "∀ r ∈ set (rs'#r) . ¬ contains s r" 
      using 3 False by auto
    ultimately show ?thesis by blast
  qed 
qed

lemma idem2_star:
assumes "contains s r" 
and "⋀ r' . r' ∈ set rs ⟹ fst r' ≠ fst r"
shows "γ s r = γ (s ⋆ rs) r" using assms
proof (induct rs)  
  case Nil
  show "γ s r = γ (s ⋆ []) r" by simp
next
  case (Cons r' rs)
  thus "γ s r = γ (s ⋆ (rs#r')) r"
    using assms by auto
      (metis contains_star fst_conv idem1 idem2 prod.exhaust) 
qed

lemma glb_common:
fixes s1 s2 s rs1 rs2
assumes "s1 = s ⋆ rs1" and "s2 = s ⋆ rs2"
shows "∃ rs . s1 ⊓ s2 = s ⋆ rs ∧ set rs ⊆ set rs1 ∪ set rs2"
proof -
  have 1:"s ≼ s1" and 2:"s ≼ s2" using assms by (auto simp add:less_eq_def)
  hence 3:"s ≼ s1 ⊓ s2" by (metis inf_glb is_lb_def pre_RDR.is_glb_def)
  have 4:"s1 ⊓ s2 ≼ s1" by (metis cobounded1) 
  show ?thesis using 3 4 assms(1) and consistency by blast
qed

lemma glb_common_set:
fixes ss s0 rset
assumes "finite ss"  and "ss ≠ {}"
and "⋀ s . s ∈ ss ⟹ ∃ rs . s = s0 ⋆ rs ∧ set rs ⊆ rset"
shows "∃ rs . ⨅ ss = s0 ⋆ rs ∧ set rs ⊆ rset"
using assms
proof (induct ss rule:finite_ne_induct)
  case (singleton s)
  obtain rs where "s = s0 ⋆ rs ∧ set rs ⊆ rset" using singleton by force
  moreover have "⨅ {s} = s" using singleton by auto
  ultimately show "∃ rs . ⨅ {s} = s0 ⋆ rs ∧ set rs ⊆ rset" by blast
next
  case (insert s ss)
  have 1:"⋀ s' . s' ∈ ss ⟹ ∃ rs . s' = s0 ⋆ rs ∧ set rs ⊆ rset"
    using insert(5) by force
  obtain rs where 2:"⨅ ss = s0 ⋆ rs" and 3:"set rs ⊆ rset" 
    using insert(4) 1 by blast
  obtain rs' where 4:"s = s0 ⋆ rs'"and 5:"set rs' ⊆ rset"
    using insert(5) by blast
  have 6:"⨅ (insert s ss) = s ⊓ (⨅ ss)"
    by (metis insert.hyps(1-3) insert_not_elem) 
  obtain rs'' where 7:"⨅ (insert s ss) = s0 ⋆ rs''" 
    and 8:"set rs'' ⊆ set rs' ∪ set rs"
    using glb_common 2 4 6 by force
  have 9:"set rs'' ⊆ rset" using 3 5 8 by blast
  show "∃ rs . ⨅ (insert s ss) = s0 ⋆ rs ∧ set rs ⊆ rset"
    using 7 9 by blast
qed

end 

end