Theory Validity

theory Validity imports Computation begin

definition "assume" :: "'s set ⇒ ('s×'s) set ⇒ ('p×'s) list set" where
  "assume pre rely ≡ {cpt. snd (hd cpt) ∈ pre ∧ (∀i. Suc i < length cpt ⟶ (cpt!i ─e→ cpt!(Suc i)) ⟶ (snd (cpt!i), snd (cpt!Suc i)) ∈ rely)}"

definition commit :: "(('p×'s) × ('p×'s)) set ⇒ 'p set ⇒ ('s×'s) set ⇒ 's set ⇒ ('p×'s) list set" where
  "commit tran fin guar post ≡
   {cpt. (∀i. Suc i < length cpt ⟶ (cpt!i, cpt!(Suc i)) ∈ tran ⟶ (snd (cpt!i), snd (cpt!(Suc i))) ∈ guar) ∧
         (fst (last cpt) ∈ fin ⟶ snd (last cpt) ∈ post)}"

definition validity :: "(('p×'s) × ('p×'s)) set ⇒ 'p set ⇒ 'p ⇒ 's set ⇒ ('s×'s) set ⇒ ('s×'s) set ⇒ 's set ⇒ bool" where
  "validity tran fin P pre rely guar post ≡ ∀s0. cpts_from tran (P,s0) ∩ assume pre rely ⊆ commit tran fin guar post"

declare validity_def[simp]

lemma commit_Cons_env:
  ‹∀P s t. ((P,s),(P,t)) ∉ tran ⟹
   (P,t)#cpt ∈ commit tran fin guar post ⟹
   (P,s)#(P,t)#cpt ∈ commit tran fin guar post›
  apply (simp add: commit_def)
  apply clarify
  apply(case_tac i, auto)
  done

lemma commit_Cons_comp:
  ‹(Q,t)#cpt ∈ commit tran fin guar post ⟹
   ((P,s),(Q,t)) ∈ tran ⟹
   (s,t)∈guar ⟹
   (P,s)#(Q,t)#cpt ∈ commit tran fin guar post›
  apply (simp add: commit_def)
  apply clarify
  apply(case_tac i, auto)
  done

lemma cpts_from_assume_take:
  assumes h: "cpt ∈ cpts_from tran c ∩ assume pre rely"
  assumes i: "i ≠ 0"
  shows "take i cpt ∈ cpts_from tran c ∩ assume pre rely"
proof
  from h have ‹cpt ∈ cpts_from tran c› by blast
  with i cpts_from_take show ‹take i cpt ∈ cpts_from tran c› by blast
next
  from h have ‹cpt ∈ assume pre rely› by blast
  with i show ‹take i cpt ∈ assume pre rely› by (simp add: assume_def)
qed

lemma assume_snoc:
  assumes "assume": ‹cpt ∈ assume pre rely›
    and nonnil: ‹cpt ≠ []›
    and tran: ‹¬(last cpt ─e→ c)›
  shows ‹cpt@[c] ∈ assume pre rely›
  using "assume" nonnil apply (simp add: assume_def)
proof
  fix i
  show ‹i < length cpt ⟶
         fst ((cpt @ [c]) ! i) = fst ((cpt @ [c]) ! Suc i) ⟶ (snd ((cpt @ [c]) ! i), snd ((cpt @ [c]) ! Suc i)) ∈ rely›
  proof(cases ‹Suc i < length cpt›)
    case True
    then show ?thesis using "assume" nonnil
      apply (simp add: assume_def)
      apply clarify
      apply(erule allE[where x=i])
      by (simp add: nth_append)
  next
    case False
    then show ?thesis
      apply clarsimp
      apply(subgoal_tac "Suc i = length cpt")
       apply simp
       apply (smt Suc_lessD append_eq_conv_conj etran_def etran_p_def hd_drop_conv_nth last_snoc length_append_singleton lessI mem_Collect_eq prod.simps(2) take_hd_drop tran)
      apply simp
      done
  qed
qed

lemma commit_tl:
  ‹(P,s)#(Q,t)#cs ∈ commit tran fin guar post ⟹
   (Q,t)#cs ∈ commit tran fin guar post›
  apply(unfold commit_def)
  apply(unfold mem_Collect_eq)
  apply clarify
  apply(rule conjI)
   apply fastforce
  by simp

lemma assume_appendD:
  ‹(P,s)#cs@cs' ∈ assume pre rely ⟹ (P,s)#cs ∈ assume pre rely›
  apply(auto simp add: assume_def)
  apply(erule_tac x=i in allE)
  apply auto
  apply (metis append_Cons length_Cons lessI less_trans nth_append)
  by (metis Suc_diff_1 Suc_lessD linorder_neqE_nat nth_Cons' nth_append zero_order(3))

lemma assume_appendD2:
  ‹cs@cs' ∈ assume pre rely ⟹ ∀i. Suc i < length cs' ⟶ cs'!i ─e→ cs'!Suc i ⟶ (snd(cs'!i), snd(cs'!Suc i))∈rely›
  apply(auto simp add: assume_def)
  apply(erule_tac x=‹length cs+i› in allE)
  apply simp
  by (metis add_Suc_right nth_append_length_plus)

lemma commit_append:
  assumes cmt1: ‹cs ∈ commit tran fin guar mid›
    and guar: ‹(snd (last cs), snd c') ∈ guar›
    and cmt2: ‹c'#cs' ∈ commit tran fin guar post›
  shows ‹cs@c'#cs' ∈ commit tran fin guar post›
  apply(auto simp add: commit_def)
  using cmt1 apply(simp add: commit_def)
  using guar apply (metis Suc_lessI append_Nil2 append_eq_conv_conj hd_drop_conv_nth nth_append nth_append_length snoc_eq_iff_butlast take_hd_drop)
  using cmt2 apply(simp add: commit_def)
   apply(case_tac ‹Suc i < length cs›)
  using cmt1 apply(simp add: commit_def) apply (simp add: nth_append)
   apply(case_tac ‹Suc i = length cs›)
  using guar apply (metis Cons_nth_drop_Suc drop_eq_Nil id_take_nth_drop last.simps last_appendR le_refl lessI less_irrefl_nat less_le_trans nth_append nth_append_length)
  using cmt2 apply(simp add: commit_def) apply (simp add: nth_append)
  using cmt2 apply(simp add: commit_def) .

lemma assume_append:
  assumes asm1: ‹cs ∈ assume pre rely›
    and asm2: ‹∀i. Suc i < length (c'#cs') ⟶ (c'#cs')!i ─e→ (c'#cs')!Suc i ⟶ (snd((c'#cs')!i), snd((c'#cs')!Suc i)) ∈ rely›
    and rely: ‹last cs ─e→ c' ⟶ (snd (last cs), snd c') ∈ rely›
    and ‹cs≠[]›
  shows ‹cs@c'#cs' ∈ assume pre rely›
  using asm1 ‹cs≠[]›
  apply(auto simp add: assume_def)
  apply(case_tac ‹Suc i < length cs›)
   apply(erule_tac x=i in allE)
   apply (metis Suc_lessD append_eq_conv_conj nth_take)
  apply(case_tac ‹Suc i = length cs›)
   apply simp
  using rely apply(simp add: last_conv_nth) apply (metis diff_Suc_Suc diff_zero lessI nth_append)
  subgoal for i
    using asm2[THEN spec[where x=‹i-length cs›]] by (simp add: nth_append)
  done

end