Theory Sep_Generic_Wp

section ‹General VCG Setup for Separation Logic›
theory Sep_Generic_Wp
imports 
  "../lib/Sep_Algebra_Add" 
  "../lib/Frame_Infer"
  "../lib/MM/MMonad"
begin

  
  
(* TODO: Move *)  
declare sep_disj_commuteI[sym]  


context acc_consistent_loc begin  
  
  lemma acc_r_alloc: "addr.block`r ⊆ Collect (is_ALLOC s) ∪ a"
    by (smt (verit, best) Un_def block.exhaust_disc image_subset_iff acc_ref_not_freed acc_ref_not_fresh is_FRESH'_eq mem_Collect_eq sup_ge1)
  
  lemma acc_w_alloc: "addr.block`w ⊆ Collect (is_ALLOC s) ∪ a"
    by (smt (verit, best) Un_def block.exhaust_disc image_subset_iff acc_ref_not_freed acc_ref_not_fresh is_FRESH'_eq mem_Collect_eq sup_ge1)

end


subsection ‹Weakest Precondition›

locale generic_wp =
  fixes wp :: "'c ⇒ ('r ⇒ acc ⇒ 's ⇒ bool) ⇒ 's ⇒ bool"
  assumes wp_comm_inf: "inf (wp c Q) (wp c Q') = wp c (inf Q Q')"
begin

  lemma wp_comm_conj: "wp c (λr i. Q r i and Q' r i) s ⟷ wp c Q s ∧ wp c Q' s"
    using wp_comm_inf[of c Q Q']
    unfolding inf_fun_def inf_bool_def by metis

  lemma wp_comm_conjI: "⟦ wp c Q s; wp c Q' s ⟧ ⟹ wp c (λr i s. Q r i s ∧ Q' r i s) s"
    using wp_comm_inf[of c Q Q']
    unfolding inf_fun_def inf_bool_def by metis


  lemma wp_mono: "Q≤Q' ⟹ wp c Q ≤ wp c Q'"
    by (metis (mono_tags) antisym_conv le_inf_iff order_refl wp_comm_inf)

  lemma wp_monoI:
    assumes "wp c Q s"
    assumes "⋀r i x. Q r i x ⟹ Q' r i x"
    shows "wp c Q' s"
    using assms wp_mono[of Q Q' c]
    by (metis le_funI predicate1D predicate1I wp_mono)
    
end

hide_const (open) NEMonad.wp

definition wp where "wp c Q s ≡ NEMonad.wp (run c s) (λ(r,i,s). Q r i s)"

lemma pw_wp[pw_init]: "wp c Q s ⟷ ¬is_fail (run c s) ∧ (∀r i s'. is_res (run c s) (r,i,s') ⟶ Q r i s')"
  unfolding wp_def by pw


lemma wp_cons: "⟦ wp c Q s; ⋀r i s'. Q r i s' ⟹ Q' r i s' ⟧ ⟹ wp c Q' s"  
  by pw
  
lemma wp_false[simp]: "¬wp c (λ_ _ _. False) s" by pw

interpretation generic_wp wp 
  apply unfold_locales 
  unfolding fun_eq_iff inf_fun_def inf_bool_def
  by pw

subsubsection ‹VCG Setup›  
  
lemma wp_return[vcg_normalize_simps]: "wp (Mreturn x) Q s ⟷ Q x 0 s" by pw

lemma wp_fail[vcg_normalize_simps]: "¬ wp (Mfail) Q s" by pw 

lemma wp_assert[vcg_normalize_simps]: "wp (Massert Φ) Q s ⟷ Φ ∧ Q () 0 s" by pw
  
lemma wp_bind[vcg_normalize_simps]: "wp (doM {x←m; f x}) Q s = wp m (λx i. wp (f x) (λx' i'. Q x' (i+i'))) s"  
  by (pw; blast)
  
lemma wp_par:  
  assumes "wp m1 Q1 s"
  assumes "wp m2 Q2 s"
  assumes "⋀r1 s1 i1 r2 s2 i2. ⟦ 
      acc_consistent s i1 s1; acc_consistent s i2 s2; spar_feasible i1 i2;
      Q1 r1 i1 s1; Q2 r2 i2 s2 
    ⟧ 
    ⟹ acc_norace i1 i2 ∧ Q (r1,r2) (i1+i2) (combine_states s1 i2 s2)"
  shows "wp (Mpar m1 m2) Q s"
  using assms apply -
  apply pw 
  apply (meson res_run_consistentI)
  apply (meson res_run_consistentI)
  done
  
lemma wp_malloc[vcg_normalize_simps]: "wp (Mmalloc xs) Q s ⟷ (∀r. is_FRESH s r ⟶ Q r (acc_a r) (addr_alloc xs r s))"  
  supply [pw_simp] = malloc_def
  by pw
  
lemma wp_free[vcg_normalize_simps]: "wp (Mfree b) Q s ⟷ is_ALLOC s b ∧ Q () (acc_f b) (addr_free b s)"  
  supply [pw_simp] = mfree_def
  by pw
  
lemma wp_load[vcg_normalize_simps]: "wp (Mload a) Q s ⟷ is_valid_addr s a ∧ Q (get_addr s a) (acc_r a) s"  
  supply [pw_simp] = mload_def
  by pw

lemma wp_mstore[vcg_normalize_simps]: "wp (Mstore a x) Q s ⟷ is_valid_addr s a ∧ Q () (acc_w a) (put_addr s a x)"  
  supply [pw_simp] = mstore_def
  by pw

lemma wp_valid_addr[vcg_normalize_simps]: "wp (Mvalid_addr a) Q s ⟷ is_valid_addr s a ∧ Q () (acc_r a) s"  
  supply [pw_simp] = mvalid_addr_def
  by pw
  
(*lemma wp_valid_ptr_addr[vcg_normalize_simps]: "wp (Mvalid_ptr_addr a) Q s ⟷ is_valid_ptr_addr s a ∧ Q () (acc_e (addr.block a)) s"  
  supply [pw_simp] = mvalid_ptr_addr_def
  by pw
*)    

subsection ‹Connecting Separation Algebra and Concrete Memory›

locale abs_sep =  
  fixes α :: "'v memory ⇒ 'a::{stronger_sep_algebra}"
    and addrs :: "'a ⇒ addr set"    (* Addresses *)
    and blocks :: "'a ⇒ block_idx set"  (* Blocks *)
    and aget :: "'a ⇒ addr ⇒ 'v"   (* Modeled values *) 
    and bget :: "'a ⇒ block_idx ⇒ nat" (* Modeled block sizes *)

  assumes disj_iff: "as1 ## as2 ⟷ (addrs as1 ∩ addrs as2 = {} ∧ blocks as1 ∩ blocks as2 = {})"
  assumes zero_char[simp]: "addrs 0 = {}" "blocks 0 = {}"
  assumes plus_char[simp]: "as1 ## as2 ⟹ addrs (as1+as2) = addrs as1 ∪ addrs as2 ∧ blocks (as1+as2) = blocks as1 ∪ blocks as2"
    
  assumes aget_add: "as1 ## as2 ⟹ a∈addrs as1 ⟹ aget (as1 + as2) a = aget as1 a"
  assumes bget_add: "as1 ## as2 ⟹ b∈blocks as1 ⟹ bget (as1 + as2) b = bget as1 b"
  
  assumes complete: "⟦ A ⊆ Collect (is_valid_addr s); B ⊆ Collect (is_ALLOC s) ⟧ ⟹
    ∃as1 as2. addrs as1 = A ∧ blocks as1 = B ∧ as1##as2 ∧ α s = as1+as2"
  
  assumes α_iff: "α s = as ⟷ (
    addrs as = Collect (is_valid_addr s) ∧ blocks as = Collect (is_ALLOC s)
  ∧ (∀a. is_valid_addr s a ⟶ aget as a = get_addr s a)  
  ∧ (∀b. is_ALLOC s b ⟶ bget as b = block_size s b)
  )"
  
begin

  abbreviation "caddrs s ≡ Collect (is_valid_addr s)"
  abbreviation "cblocks s ≡ Collect (is_ALLOC s)"

  lemma aget_add': "as1 ## as2 ⟹ a∈addrs as2 ⟹ aget (as1 + as2) a = aget as2 a"
    by (metis aget_add sep_add_commute sep_disj_commuteI)
  
  lemma bget_add': "as1 ## as2 ⟹ b∈blocks as2 ⟹ bget (as1 + as2) b = bget as2 b"
    by (metis bget_add sep_add_commute sep_disj_commuteI)

  lemmas get_add = aget_add aget_add' bget_add bget_add'  
    
  lemma α_simps:
    "addrs (α s) = caddrs s"
    "blocks (α s) = cblocks s"
    "is_valid_addr s a ⟹ aget (α s) a = get_addr s a"
    "is_ALLOC s b ⟹ bget (α s) b = block_size s b"
    using α_iff[THEN iffD1, OF refl] by auto

  lemma α_eqI: 
    assumes "addrs as = caddrs s" 
    assumes "blocks as = cblocks s"
    assumes "⋀a. is_valid_addr s a ⟶ aget as a = get_addr s a"
    assumes "⋀b. is_ALLOC s b ⟶ bget as b = block_size s b"
    shows "α s = as"  
    apply (subst α_iff) using assms by blast

  lemma complete': 
    assumes "A ⊆ caddrs s" "B ⊆ cblocks s" 
    obtains as1 as2 where
      "addrs as1 = A"
      "blocks as1 = B" 
      "addrs as2 = caddrs s - A"
      "blocks as2 = cblocks s - B"
      "as1##as2" 
      "α s = as1+as2"
  proof -  
    from complete[OF assms] obtain as1 as2 where
      [simp]:
      "addrs as1 = A"
      "blocks as1 = B" 
      "α s = as1+as2"
      and
      DJ: "as1##as2" 
      by blast
      
    from α_simps[of s] DJ have 
      "A ∪ addrs as2 = caddrs s" 
      "B ∪ blocks as2 = cblocks s" 
      by (simp_all add: plus_char)
    with ‹as1##as2› have
      "addrs as2 = caddrs s - A"
      "blocks as2 = cblocks s - B"
      by (auto simp: disj_iff)
      
    show ?thesis
      apply rule
      by fact+
  qed
  
  
      
  (* Partial Characterization *)  
    
  (* As sep-logic *)
  definition "pchar as s ≡ ∃f. as##f ∧ α s = as + f"
  
  (* Via concrete memory *)
  lemma pchar_alt: "pchar as s ⟷ (
    addrs as ⊆ caddrs s ∧ blocks as ⊆ cblocks s
  ∧ (∀a∈addrs as. aget as a = get_addr s a)  
  ∧ (∀b∈blocks as. bget as b = block_size s b)  
  )" 
  proof (rule, goal_cases)
    case 1
    then show ?case by (metis Int_Collect Un_Int_eq(3) α_simps(1) α_simps(2) α_simps(3) α_simps(4) aget_add bget_add inf_sup_ord(3) pchar_def plus_char)
  next
    case 2
    
    from complete'[of "addrs as" s  "blocks as"]
    obtain as1 as2 where
      "addrs as1 = addrs as" 
      "blocks as1 = blocks as"
      "addrs as2 = Collect (is_valid_addr s) - addrs as"
      "blocks as2 = {b. is_ALLOC s b} - blocks as"
      "as1 ## as2"
      and
      C1: "α s = as1 + as2"
      using 2 by blast
      
    have "as ## as2"
      using ‹addrs as1 = addrs as› ‹as1 ## as2› ‹blocks as1 = blocks as› disj_iff by auto
      
    moreover have "α s = as + as2" using C1
      unfolding α_iff
      apply clarsimp
      by (smt (verit, ccfv_threshold) "2" Un_iff ‹addrs as1 = addrs as› ‹as ## as2› ‹as1 ## as2› ‹blocks as1 = blocks as› 
        aget_add' bget_add' mem_Collect_eq plus_char sep_add_commute sep_disj_commuteI)
    
    ultimately show ?case unfolding pchar_def by blast
  qed
  

  lemma pchar_completeI: 
    assumes "pchar as s"
    assumes "addrs as = caddrs s"
    assumes "blocks as = cblocks s"
    shows "α s = as"
    using α_eqI assms pchar_alt by auto
    
  lemma pchar_add: 
    assumes "pchar as1 s"
    assumes "pchar as2 s"
    assumes "as1 ## as2"
    shows "pchar (as1+as2) s"
    using assms
    unfolding pchar_alt
    by (auto simp: get_add)
  
    
  lemma pchar_xfer: 
    assumes "pchar as s" 
    assumes "∀a∈addrs as. is_valid_addr s' a ∧ get_addr s' a = get_addr s a"
    assumes "∀b∈blocks as. is_ALLOC s' b ∧ block_size s' b = block_size s b"
    shows "pchar as s'"
    using assms unfolding pchar_alt
    by auto
    
    
    
  lemma addrs_djI[intro]:
    "a##b ⟹ x∈addrs a ⟹ x∉addrs b"  
    "a##b ⟹ x∈addrs b ⟹ x∉addrs a"  
    by (auto simp: disj_iff)
    
  lemma blocks_djI[intro]:
    "a##b ⟹ x∈blocks a ⟹ x∉blocks b"  
    "a##b ⟹ x∈blocks b ⟹ x∉blocks a"  
    by (auto simp: disj_iff)


subsection ‹Weakest Precondition With Access Report›    
    
text ‹Access report does not include blocks and addresses from frame›
definition "acc_excludes i asf 
  ≡ acc.r i ∪ acc.w i ⊆ -addrs asf ∧ acc.f i ⊆ - (addr.block`addrs asf ∪ blocks asf)"
    
lemma acc_excludes_simps[simp]:
  "acc_excludes 0 asf"  
  "acc_excludes i 0"  
  unfolding acc_excludes_def by auto
  
lemma "acc_excludes i asf ⟷
  (∀a∈addrs asf. a∉acc.r i ∧ a∉acc.w i ∧ addr.block a ∉ acc.f i)
∧ (∀b∈blocks asf. b∉acc.f i)"  
  unfolding acc_excludes_def by auto
  
text ‹Weakest precondition for program, such that accesses are disjoint from frame›  
definition wpa where [pw_init]: "wpa asf c Q s ≡ wp c (λr i s'. 
    Q r s' 
  ∧ acc_excludes i asf
) s"

lemma wpa_monoI:
  assumes "wpa A c Q s"
  assumes "⋀r s'. ⟦ Q r s' ⟧ ⟹ Q' r s'"
  assumes "blocks A' ⊆ blocks A" "addrs A' ⊆ addrs A"
  shows "wpa A' c Q' s"
  using assms unfolding wpa_def acc_excludes_def
  by (blast intro: wp_monoI)

subsubsection ‹VCG Setup›
  
lemma wpa_false[vcg_normalize_simps]: "¬wpa A m (λ_ _. False) s"  
  by (simp add: wpa_def vcg_normalize_simps)

lemma wpa_spec[vcg_normalize_simps]: "wpa asf (Mspec P) Q s ⟷ (P≠bot) ∧ (∀x. P x ⟶ Q x s)" by pw

lemma wpa_return[vcg_normalize_simps]: "wpa asf (Mreturn x) Q s ⟷ Q x s" by pw

lemma wpa_fail[vcg_normalize_simps]: "¬ wpa asf (Mfail) Q s" by pw 

lemma wpa_assert[vcg_normalize_simps]: "wpa asf (Massert Φ) Q s ⟷ Φ ∧ Q () s" by pw

lemma wpa_bindI[vcg_decomp_rules]: "wpa asf m (λx. wpa asf (f x) Q) s ⟹ wpa asf (doM {x←m; f x}) Q s"  
  unfolding wpa_def acc_excludes_def
  apply (simp add: vcg_normalize_simps)
  apply (erule wp_cons)
  apply clarify
  apply (erule wp_cons)
  apply auto
  done
  
lemma wpa_ifI[vcg_decomp_rules]: 
  assumes "b ⟹ wpa asf c Q s"
  assumes "¬b ⟹ wpa asf e Q s"
  shows "wpa asf (if b then c else e) Q s"  
  using assms by auto
  
  
  
  
subsection ‹Hoare Triples›  
definition "STATE asf P s ≡ ∃as. as ## asf ∧ α s = as+asf ∧ P as"

definition "htriple P c Q ≡ (∀s asf. STATE asf P s 
  ⟶ wpa asf c (λr s'. STATE asf (Q r) s') s)"

lemma htripleI[intro?]:
  assumes "⋀s asf. STATE asf P s ⟹ wpa asf c (λr s'. STATE asf (Q r) s') s"
  shows "htriple P c Q"
  using assms unfolding htriple_def by blast

lemma htripleD: 
  assumes "htriple P c Q"
  assumes "STATE asf P s"
  shows "wpa asf c (λr s'. STATE asf (Q r) s') s"
  using assms unfolding htriple_def by blast

subsubsection ‹Semantic Definition of Hoare-Triples›  
text ‹
  The Hoare-triple is defined wrt. the semantics. 
  Unfolding all intermediate concepts, a Hoare-triple 
  implies a statement over the bare-bones semantics const‹run›:
›
lemma htriple_semanticsD:
  assumes "htriple P c Q"
  assumes "as ## asf" "α μ = as+asf" "P as" ― ‹Given memory that can be split into part that satisfies precondition, and a frame›
  obtains R where 
    "run c μ = SPEC R" ― ‹The program does not fail›
    "∀x i μ'. R (x,i,μ') ⟶ ― ‹And all possible results ...›
      (∃as'. as'##asf ∧ α μ' = as'+asf ― ‹Can be split into the original frame and another part›
           ∧ Q x as')" ― ‹that satisfies the postcondition›
  using assms
  unfolding htriple_def wpa_def STATE_def wp_def NEMonad.wp_def is_res_def the_spec_def is_fail_def
  apply (auto split: neM.splits)
  by (metis neM.exhaust)
  
  
  
subsubsection ‹VCG Setup›
  

  lemma STATE_triv[simp]: "¬STATE asf sep_false s"
    by (simp add: STATE_def)
    
  lemma STATE_monoI: "STATE asf P s ⟹ P ⊢ P' ⟹ STATE asf P' s"  
    unfolding STATE_def entails_def by blast
    
  lemma STATE_frame1:
    "STATE asf (P**F) s ⟹ ∃asf'. asf'##asf ∧ F asf' ∧ STATE (asf'+asf) P s"  
    unfolding STATE_def
    apply (auto simp: sep_algebra_simps sep_conj_def)
    by fastforce

  lemma STATE_frame2: 
    assumes "STATE (asf'+asf) P s"
    assumes "asf' ## asf"  
    assumes "F asf'"
    shows "STATE asf (P**F) s"
    using assms
    unfolding STATE_def
    apply (auto simp: sep_algebra_simps sep_conj_def) 
    by (metis assms(2) sep_add_assoc sep_add_commute sep_disj_add_eq)

  lemma htriple_triv[simp, intro!]: "htriple sep_false c Q"
    by (auto simp: htriple_def)
      
  lemma cons_rule:
    assumes "htriple P c Q"
    assumes "⋀s. P' s ⟹ P s"
    assumes "⋀r s. Q r s ⟹ Q' r s"
    shows "htriple P' c Q'"
  proof
    fix asf s
    assume "STATE asf P' s"
    with STATE_monoI assms(2) have "STATE asf P s" unfolding entails_def by blast
    from htripleD[OF assms(1) this] have "wpa asf c (λr. STATE asf (Q r)) s" .
    then show "wpa asf c (λr. STATE asf (Q' r)) s"
      apply (rule wpa_monoI)
      apply (erule STATE_monoI)
      using assms(3) unfolding entails_def 
      by auto
      
  qed  
      
  lemma cons_post_rule:
    assumes "htriple P c Q"
    assumes "⋀r s. Q r s ⟹ Q' r s"
    shows "htriple P c Q'"
    using cons_rule assms by blast
    
  lemma apply_htriple_rule:
    assumes "STATE asf (P**F) s"
    assumes "htriple P c Q"
    assumes "⋀s' r. STATE asf (Q r ** F) s' ⟹ Q' r s'"
    shows "wpa asf c Q' s"  
  proof -
    from STATE_frame1[OF assms(1)] obtain asf' where 
      D: "asf' ## asf" "F asf'" 
      and S: "STATE (asf' + asf) P s" 
      by blast
  
    from htripleD[OF assms(2) S] have "wpa (asf'+asf) c (λr s'. STATE (asf' + asf) (Q r) s') s" .
    moreover have "⟦STATE (asf' + asf) (Q r) s'⟧ ⟹ STATE asf (Q r ** F) s'" for r s'
      by (rule STATE_frame2; (assumption|rule D)?)
    ultimately have "wpa (asf)  c (λr s'. STATE asf (Q r ** F) s') s"
      apply (rule wpa_monoI) by (auto simp: D)
    then show ?thesis using assms(3)
      by (rule wpa_monoI) auto
  qed

        
  lemma frame_rule: "htriple P c Q ⟹ htriple (P ** F) c (λr. Q r ** F)"
    apply rule
    apply (erule apply_htriple_rule)
    .
    
subsubsection ‹Disjoint Concurrency Rule›    

context begin    
(* This rule is used to show disjointness in the lemma below.
  Just using blast there will be inefficient due to big terms.
*)    
private lemma dj_subsetXI:    
  assumes "a⊆a1∪a2"
  assumes "b⊆b1∪b2"
  assumes "a1∩b1 = {}"
  assumes "a1∩b2 = {}"
  assumes "a2∩b1 = {}"
  assumes "a2∩b2 = {}"
  shows "a∩b = {}"
  using assms
  by blast  
  
    
lemma ht_par:
  assumes HT1: "htriple P1 m1 Q1"
  assumes HT2: "htriple P2 m2 Q2"
  shows "htriple (P1**P2) (m1 ∥M m2) (λ(r1,r2). Q1 r1 ** Q2 r2)"
proof
  fix s asf
  
  ― ‹Precondition›
  assume "STATE asf (P1 ∧* P2) s"
  then obtain as1 as2 where 
        [simp]: "as1 ## as2" "(as1 + as2) ## asf" 
    and S_SPLIT: "α s = as1 + as2 + asf" 
    and PRECOND[simp]: "P1 as1" "P2 as2"
    unfolding STATE_def by (auto simp: sep_conj_def)

  have [simp, symmetric, simp]: "as1 ## asf" "as2 ## asf"
    using ‹as1 ## as2› ‹as1 + as2 ## asf› sep_add_disjD apply blast
    using ‹as1 ## as2› ‹as1 + as2 ## asf› sep_add_disjD apply blast
    done   

  ― ‹Addresses breakdown on concrete level›    
  have CA_SPLIT: "caddrs s = addrs as1 ∪ addrs as2 ∪ addrs asf"  
    and CB_SPLIT: "cblocks s = blocks as1 ∪ blocks as2 ∪ blocks asf"
    using S_SPLIT by (simp_all flip: α_simps)
    
  have ADDRS_DJ: 
    "addrs as1 ∩ addrs as2 = {}"  
    "addrs as1 ∩ addrs asf = {}"  
    "addrs as2 ∩ addrs asf = {}"  
  and BLOCKS_DJ:   
    "blocks as1 ∩ blocks as2 = {}"  
    "blocks as1 ∩ blocks asf = {}"  
    "blocks as2 ∩ blocks asf = {}"  
    using disj_iff by force+
          
  ― ‹Re-shuffle to get frames›
  have S1: "STATE (as2 + asf) P1 s"  
    unfolding STATE_def by (auto simp: sep_conj_def sep_algebra_simps S_SPLIT intro!: exI[where x="as1"])
    
  have S2: "STATE (as1 + asf) P2 s"  
    unfolding STATE_def by (auto simp: sep_conj_def sep_algebra_simps S_SPLIT intro!: exI[where x="as2"])

  ― ‹Executions›  
  note WPA1 = htripleD[OF HT1 S1]
  note WPA2 = htripleD[OF HT2 S2]
  
  ― ‹Break down ‹wpa››
  show "wpa asf (m1 ∥M m2) (λr. STATE asf (case r of (r1, r2) ⇒ Q1 r1 ∧* Q2 r2)) s"
    using WPA1 WPA2
    apply (simp add: wpa_def)
    apply (erule (1) wp_par, thin_tac "wp _ _ _"; clarsimp)
  proof goal_cases
    case (1 x1 s1 i1 x2 s2 i2)

    ― ‹Make assumptions explicit›
    
    interpret feasible_parallel_execution s s1 i1 s2 i2 using 1 apply unfold_locales by simp_all

    note STATE1 = ‹STATE (as2 + asf) (Q1 x1) s1›
    note STATE2 = ‹STATE (as1 + asf) (Q2 x2) s2›
    note IEXCL1 = ‹acc_excludes i1 (as2 + asf)›
    note IEXCL2 = ‹acc_excludes i2 (as1 + asf)›

    
    from IEXCL1 IEXCL2 have G_EXCL: "acc_excludes (i1 + i2) asf"
      unfolding acc_excludes_def
      by auto
        
      
      
    ― ‹Prove race freedom›
    have G1: "acc_norace i1 i2"
    proof -
    
      text ‹From consistency, we know that interference only talks about valid addresses.
        Note that the allocated addresses are on over-approximation here
      ›
      have SS1: "r1 ∪ w1 ⊆ addrs as1 ∪ c1.allocated_addrs_approx" "f1 ⊆ blocks as1 ∪ a1"
        using c1.rw_valid_or_alloc IEXCL1 ADDRS_DJ c1.f_valid_or_alloc BLOCKS_DJ
        unfolding CA_SPLIT CB_SPLIT acc_excludes_def
        by auto
        
      have SS2: "r2 ∪ w2 ⊆ addrs as2 ∪ c2.allocated_addrs_approx" "f2 ⊆ blocks as2 ∪ a2"
        using c2.rw_valid_or_alloc IEXCL2 ADDRS_DJ c2.f_valid_or_alloc BLOCKS_DJ
        unfolding CA_SPLIT CB_SPLIT acc_excludes_def
        by auto
    
      text ‹The allocations are disjoint by feasibility assumption›  
      note alloc_addrs_disj alloc_disj
      
      text ‹The allocations are disjoint from the original addresses by consistency›
      from c1.a_dj_valid c1.a_dj_alloc c2.a_dj_valid c2.a_dj_alloc
      have ORIG_DJ: 
        "(addrs as1 ∪ addrs as2) ∩ (c1.allocated_addrs_approx ∪ c2.allocated_addrs_approx) = {}"
        "(blocks as1 ∪ blocks as2) ∩ (a1 ∪ a2) = {}"
        unfolding CA_SPLIT CB_SPLIT by blast+
        
      note ADDRS_DJ BLOCKS_DJ
      
      have G1: "(r1∪w1) ∩ (r2∪w2) = {}"
        apply (rule dj_subsetXI, fact, fact, fact)
        using ORIG_DJ apply blast
        using ORIG_DJ apply blast
        using alloc_addrs_approx_disj .
        
      have G2: "f1∩f2={}" 
        apply (rule dj_subsetXI, fact, fact, fact)
        using ORIG_DJ apply blast
        using ORIG_DJ apply blast
        by fact
        
      note c1.rw_valid_or_alloc
      note IEXCL1  
        
      have G3: "addr.block`(r1∪w1) ∩ f2 = {}"
      proof -
        have "f2 ⊆ -addr.block`(addrs as1 ∪ addrs asf)"  
          using IEXCL2 unfolding acc_excludes_def by simp
        moreover have "addr.block`(r1∪w1) ⊆ addr.block`(addrs as1 ∪ addrs asf) ∪ a1"  
          using SS1(1) by auto
        ultimately show ?thesis  
          using alloc_free_dj
          by blast
      qed  

      have G4: "addr.block`(r2∪w2) ∩ f1 = {}"
      proof -
        have "f1 ⊆ -addr.block`(addrs as2 ∪ addrs asf)"  
          using IEXCL1 unfolding acc_excludes_def by simp
        moreover have "addr.block`(r2∪w2) ⊆ addr.block`(addrs as2 ∪ addrs asf) ∪ a2"  
          using SS2(1) by auto
        ultimately show ?thesis  
          using free_alloc_dj
          by blast
      qed  
        
      show "acc_norace i1 i2"
        unfolding acc_norace_def Let_def
        apply simp
        using G1 G2 G3 G4
        by blast
        
    qed
        
        
    ― ‹Now we have a valid parallel execution›  
    interpret valid_parallel_execution s s1 i1 s2 i2 apply unfold_locales by fact+
    
    have G2: "STATE asf (Q1 x1 ∧* Q2 x2) s'" 
    proof -
    
      note ‹STATE (as2 + asf) (Q1 x1) s1› ‹STATE (as1 + asf) (Q2 x2) s2›
      then obtain as1' as2' where 
            A12_FMT:
        "α s1 = as1' + as2 + asf"
        "α s2 = as1 + as2' + asf"
        and ASx'_DJS:
        "as1' ## (as2 + asf)"
        "as2' ## (as1 + asf)"
        and 
        "Q1 x1 as1'"
        "Q2 x2 as2'"
        unfolding STATE_def
        by (auto simp: sep_algebra_simps )
    
      from ASx'_DJS have [simp, symmetric, simp]:
        "as1' ## as2"  
        "as1' ## asf"  
        "as2' ## as1"  
        "as2' ## asf"  
        by auto
        
      ― ‹Addresses breakdown on concrete level›    
      have CA'_SPLIT: 
          "caddrs s1 = addrs as1' ∪ addrs as2 ∪ addrs asf"  
          "caddrs s2 = addrs as1 ∪ addrs as2' ∪ addrs asf"  
        and CB'_SPLIT: 
          "cblocks s1 = blocks as1' ∪ blocks as2 ∪ blocks asf"
          "cblocks s2 = blocks as1 ∪ blocks as2' ∪ blocks asf"
        using A12_FMT by (simp_all flip: α_simps)
        
      have ADDRS'_DJ: 
        "addrs as1' ∩ addrs as2 = {}" 
        "addrs as1' ∩ addrs asf = {}" 
        "addrs as2' ∩ addrs as1 = {}" 
        "addrs as2' ∩ addrs asf = {}" 
        using disj_iff by force+
        
      have BLOCKS'_DJ: 
        "blocks as1' ∩ blocks as2 = {}" 
        "blocks as1' ∩ blocks asf = {}" 
        "blocks as2' ∩ blocks as1 = {}" 
        "blocks as2' ∩ blocks asf = {}" 
        using disj_iff by force+
        
      have AS1'_EQ: "addrs as1' = addrs as1 ∪ c1.allocated_addrs - c1.freed_addrs"
        apply auto
        subgoal using ADDRS'_DJ(1) ADDRS'_DJ(2) CA'_SPLIT(1) CA_SPLIT c1.allocated_addrs_def by auto
        subgoal using CA'_SPLIT(1) c1.valid_s'_alt' by auto
        subgoal using ADDRS_DJ(1) ADDRS_DJ(2) CA'_SPLIT(1) CA_SPLIT c1.freed_addrs_def by auto
        subgoal by (metis CA'_SPLIT(1) CA_SPLIT DiffD2 UnE UnI2 c1.allocated_addrs_def c1.valid_s'_alt inf_sup_aci(5))
        done
      
      have AS2'_EQ: "addrs as2' = addrs as2 ∪ c2.allocated_addrs - c2.freed_addrs"
        apply auto
        subgoal using ADDRS'_DJ(3) ADDRS'_DJ(4) CA'_SPLIT(2) CA_SPLIT c2.allocated_addrs_def by auto
        subgoal by (simp add: CA'_SPLIT(2) c2.freed_addrs_def)
        subgoal using CA'_SPLIT(2) CA_SPLIT ‹as1 ## as2› ‹asf ## as2› addrs_djI(2) c2.freed_addrs_def by force
        subgoal using CA'_SPLIT(2) CA_SPLIT c2.allocated_addrs_def by force
        done

      have CB1_EQ: "cblocks s1 = cblocks s ∪ a1 - f1"  
        by (auto simp: c1.is_ALLOC'_eq)

      have CB2_EQ: "cblocks s2 = cblocks s ∪ a2 - f2"  
        by (auto simp: c2.is_ALLOC'_eq)
        
                
      have B1'_EQ: "blocks as1' = blocks as1 ∪ a1 - f1" 
        apply (auto simp: )
        subgoal using BLOCKS'_DJ(1) BLOCKS'_DJ(2) CB'_SPLIT(1) CB_SPLIT c1.is_ALLOC'_eq by auto
        subgoal using CB'_SPLIT(1) c1.is_FREED'_eq by blast
        subgoal using BLOCKS_DJ(1) BLOCKS_DJ(2) CB'_SPLIT(1) CB_SPLIT c1.is_ALLOC'_eq by auto
        subgoal using CB'_SPLIT(1) CB_SPLIT c1.a_dj_alloc c1.is_ALLOC'_eq by auto
        done

      have B2'_EQ: "blocks as2' = blocks as2 ∪ a2 - f2" 
        apply (auto simp: )
        subgoal using BLOCKS'_DJ(3,4) CB'_SPLIT(2) CB_SPLIT c2.is_ALLOC'_eq by auto
        subgoal using CB'_SPLIT(2) c2.is_FREED'_eq by blast
        subgoal using BLOCKS_DJ CB'_SPLIT(2) CB_SPLIT c2.is_ALLOC'_eq by auto
        subgoal using CB'_SPLIT(2) CB_SPLIT c2.a_dj_alloc c2.is_ALLOC'_eq by auto
        done

                
      ― ‹The new abstract state covers exactly the addresses of the concrete state›  
      have COVERAGE: 
        "caddrs s' = addrs as1' ∪ addrs as2' ∪ addrs asf"
        "cblocks s' = blocks as1' ∪ blocks as2' ∪ blocks asf"
      proof -
          
        have "caddrs s' = (caddrs s1 - c2.freed_addrs) ∪ (caddrs s2 - c1.freed_addrs)"  
          by (simp add: valid_addr'')
        also note c1.valid_s'_alt'  
        also note c2.valid_s'_alt'  
        finally have "caddrs s' = (caddrs s ∪ c1.allocated_addrs ∪ c2.allocated_addrs) - c1.freed_addrs - c2.freed_addrs" by blast
        also note CA_SPLIT
        also have "(addrs as1 ∪ addrs as2 ∪ addrs asf ∪ c1.allocated_addrs ∪ c2.allocated_addrs) - c1.freed_addrs - c2.freed_addrs
          = (addrs as1 ∪ c1.allocated_addrs - c1.freed_addrs) 
          ∪ (addrs as2 ∪ c2.allocated_addrs - c2.freed_addrs)
          ∪ addrs asf"
          apply auto
          subgoal using CA'_SPLIT(1) c1.valid_s'_alt' by auto
          subgoal using alloc_freed_addrs_disj(2) by auto
          subgoal by (simp add: CA'_SPLIT(1) c1.freed_addrs_def)
          subgoal by (simp add: CA'_SPLIT(2) c2.freed_addrs_def)
          subgoal using alloc_freed_addrs_disj(1) by blast
          subgoal using CA'_SPLIT(2) c2.valid_s'_alt' by auto
          done
        also note AS1'_EQ[symmetric]   
        also note AS2'_EQ[symmetric]
        finally show "caddrs s' = addrs as1' ∪ addrs as2' ∪ addrs asf" .
      
        have "cblocks s' = (cblocks s1 - f2) ∪ (cblocks s2 - f1)"
          by (auto simp: is_ALLOC'_eq c1.is_ALLOC'_eq c2.is_ALLOC'_eq)
        also note CB1_EQ
        also note CB2_EQ
        finally have "cblocks s' = cblocks s ∪ a1 ∪ a2 - f1 - f2"
          by auto
        also note CB_SPLIT
        also have "blocks as1 ∪ blocks as2 ∪ blocks asf ∪ a1 ∪ a2 - f1 - f2
          = (blocks as1 ∪ a1 - f1) ∪ (blocks as2 ∪ a2 - f2) ∪ blocks asf"
          apply auto
          subgoal using CB'_SPLIT(1) c1.is_ALLOC'_eq by auto
          subgoal using free_alloc_dj by blast
          subgoal using CB'_SPLIT(1) CB1_EQ by blast
          subgoal using CB'_SPLIT(2) CB2_EQ by blast
          subgoal using alloc_free_dj by auto
          subgoal using CB'_SPLIT(2) CB2_EQ by blast
          done
        also note B1'_EQ[symmetric]
        also note B2'_EQ[symmetric]
        finally show "cblocks s' = blocks as1' ∪ blocks as2' ∪ blocks asf" .
      qed  
      
      ― ‹The abstract states from both sides are disjoint›  
      have DISJOINT[simp]: "as1' ## as2'" 
        apply (simp add: disj_iff)
        using ADDRS_DJ BLOCKS_DJ
        apply (auto simp: AS1'_EQ AS2'_EQ B1'_EQ B2'_EQ)
        subgoal using CA_SPLIT c2.allocated_addrs_def by auto
        subgoal by (simp add: CA_SPLIT c1.allocated_addrs_def)
        subgoal by (meson alloc_addrs_disj disjoint_iff)
        subgoal by (metis B2'_EQ Diff_iff IntD1 Un_Int_eq(2) ‹as1 ## as2'› blocks_djI(1))
        subgoal by (metis B1'_EQ DiffI Un_upper2 ‹as2 ## as1'› blocks_djI(1) subset_iff)
        subgoal by (meson alloc_disj disjoint_iff)
        done


      ― ‹The new abstract states characterize their concrete counterparts.
        In the rest of this proof, we will transfer these to ‹s'›, using
        the fact that ‹s'› is equal to ‹s1›/‹s2›/‹asf› on the relevant addresses
       ›  
      have "pchar as1' s1" "pchar asf s1" "pchar as2' s2"  
        unfolding pchar_def
        by (auto simp: A12_FMT sep_algebra_simps 
          intro: exI[where x="as2+asf"] exI[where x="as1+asf"] exI[where x="as1'+as2"]
        )
        
        
                
      have "pchar as1' s'"
        apply (rule pchar_xfer[OF ‹pchar as1' s1›]; intro ballI conjI)
      proof -
      
        from IEXCL2 have "addrs as1 ∩ w2 = {}"  
          unfolding acc_excludes_def by auto
        then have "addrs as1' ∩ (w2) = {}" 
          apply (auto simp add: AS1'_EQ)
          by (smt (verit, ccfv_threshold) Un_iff alloc_disj c1.allocated_addrs_approx c1.valid_s_not_alloc c2.rw_valid_or_alloc disjoint_iff mem_Collect_eq subset_eq)
        
        have "addr.block`addrs as1' ∩ a2 = {}"
          apply (auto simp add: AS1'_EQ)
          subgoal using CA_SPLIT c2.a_dj_valid by auto
          subgoal using alloc_disj c1.allocated_addrs_approx by blast
          done
          
        fix a 
        assume A: "a ∈ addrs as1'"
        thus "is_valid_addr s' a"
          using  CA'_SPLIT COVERAGE(1)
          by (auto simp:)
        thus "get_addr s' a = get_addr s1 a" 
          using A ‹addrs as1' ∩ (w2) = {}› ‹addr.block`addrs as1' ∩ a2 = {}›
          by (auto simp add: get_addr_combine)
      next
        fix b
        assume A: "b ∈ blocks as1'"
        thus "is_ALLOC s' b"
          using CB'_SPLIT COVERAGE(2) by auto
        show "block_size s' b = block_size s1 b"
          (* TODO: That's a generic lemma from valid-combination! *)
          by (metis A UnCI ‹is_ALLOC s' b› ‹pchar as1' s1› block_size_combine c2.is_FREED'_eq block.disc(2) combine_states_def is_FREED'_eq pchar_alt subset_Collect_conv)
      qed    

      moreover
      
      have "pchar asf s'"
        apply (rule pchar_xfer[OF ‹pchar asf s1›]; intro ballI conjI)
      proof -
      
        from IEXCL2 have "addrs asf ∩ w2 = {}"  
          unfolding acc_excludes_def by auto
        
        have ‹addr.block`addrs asf ∩ a2 = {}›
          using c2.a_dj_valid
          unfolding CA_SPLIT by blast
      
        fix a
        assume A: "a ∈ addrs asf"
        thus "is_valid_addr s' a"
          using ‹caddrs s' = addrs as1' ∪ addrs as2' ∪ addrs asf› by blast
        thus "get_addr s' a = get_addr s1 a" 
          using A ‹addrs asf ∩ (w2) = {}› ‹addr.block`addrs asf ∩ a2 = {}›
          by (auto simp add: get_addr_combine)
      next
        fix b
        assume A: "b ∈ blocks asf"
        thus "is_ALLOC s' b"
          using CB'_SPLIT COVERAGE(2) by auto
        show "block_size s' b = block_size s1 b"
          (* TODO: That's a generic lemma from valid-combination! *)
          by (metis A CB'_SPLIT(1) UnI2 Un_upper2 ‹is_ALLOC s' b› block_size_combine c2.is_FREED'_eq combine_states_def is_ALLOC_conv is_FREED'_eq subset_Collect_conv)
      qed    
        
      moreover
      
      have "pchar as2' s'"
        apply (rule pchar_xfer[OF ‹pchar as2' s2›]; intro ballI conjI)
      proof -
      
        from IEXCL1 have "addrs as2 ∩ w1 = {}"  
          unfolding acc_excludes_def by auto
        then have "addrs as2' ∩ (w1) = {}" 
          apply (auto simp add: AS2'_EQ)
          by (smt (verit, ccfv_threshold) Un_iff alloc_blocks_def alloc_disj c1.acc_w_alloc c1.rw_valid_s c2.allocated_addrs_approx c2.acc_a_alloc disjoint_iff fresh_freed_not_valid(1) image_subset_iff mem_Collect_eq subset_iff)
        
        have "addr.block`addrs as2' ∩ a1 = {}"
          apply (auto simp add: AS2'_EQ)
          subgoal using CA_SPLIT c1.a_dj_valid by auto
          subgoal using alloc_disj c2.allocated_addrs_approx by blast
          done
      
        fix a 
        assume A: "a ∈ addrs as2'"
        
        from A show "is_valid_addr s' a"
          using  CA'_SPLIT COVERAGE(1)
          by (auto simp:)
        thus "get_addr s' a = get_addr s2 a" 
          using A ‹addrs as2' ∩ (w1) = {}› ‹addr.block`addrs as2' ∩ a1 = {}›
          apply (auto simp add: get_addr_combine)
          apply (subst valid_addr'_outside_wa_eq_orig[of a]; auto?)
          apply (subst valid_addr'_outside_wa_eq_orig[of a]; auto?)
          done
      next
        fix b
        assume A: "b ∈ blocks as2'"
        thus "is_ALLOC s' b"
          using CB'_SPLIT COVERAGE(2) by auto
        show "block_size s' b = block_size s2 b"
          (* TODO: That's a generic lemma from valid-combination! *)
          by (metis (no_types, lifting) A UnCI ‹is_ALLOC s' b› ‹pchar as2' s2› block_size_combine c1.is_FREED'_eq combine_states_def is_ALLOC_conv is_FREED'_eq par_blocks_same_length pchar_alt subset_Collect_conv)
      qed    
      
      ultimately
      
      have "pchar (as1' + as2' + asf) s'"
        apply (intro pchar_add)
        by simp_all
        
      ― ‹As these addresses cover all of ‹s'›, we can write the abstraction of ‹s'› accordingly›
      from pchar_completeI[OF this] COVERAGE have "α s' = as1' + as2' + asf" by simp
      
      ― ‹From the correctness of the parallel strands, and disjointness of ‹as1' ## as2'›,
        we get that both postconditions hold simultaneously
      ›
      moreover have "(Q1 x1 ** Q2 x2) (as1' + as2')"
        by (meson ‹Q1 x1 as1'› ‹Q2 x2 as2'› ‹as1' ## as2'› sep_conjI)
      
      ultimately show ?thesis
        unfolding STATE_def apply -
        apply (rule exI[where x = "as1' + as2'"])
        apply (simp)
        done
    qed    
    
    show ?case using G1 G2 G_EXCL by blast
  qed 
qed        

end
   

  
subsection ‹Realizable abstract Predicates›    
  text ‹Auxiliary concept, stating that there is actually a concrete memory on 
    part of which an assertion can be satisfied. This follows from the precondition of a Hoare-triple.
  ›
  definition "realizable P ≡ ∃s as asf. P as ∧ α s = as + asf ∧ as ## asf"
  
  lemma realizable_conjD: "realizable (P**Q) ⟹ realizable P ∧ realizable Q"
    apply (clarsimp simp: realizable_def sep_conj_def sep_algebra_simps sep_conj_c; intro conjI)
    subgoal for s x asf y
      apply (rule exI[where x=s])
      apply (rule exI[where x="x"])
      apply simp
      apply (rule exI[where x="asf+y"])
      by simp
    
    subgoal for s x asf y
      apply (rule exI[where x=s])
      apply (rule exI[where x="y"])
      apply simp
      apply (rule exI[where x="asf+x"])
      by (simp add: sep_algebra_simps)
      
    done

  lemma realizable_emp[simp]: "realizable □"    
    by (auto simp add: realizable_def sep_algebra_simps)
          
  lemma realizable_pure[simp]: "realizable (↑φ) ⟷ φ"  
    by (auto simp add: realizable_def sep_algebra_simps)
      
  lemma realizable_extract_pure[simp]: "realizable (↑φ ** P) ⟷ φ ∧ realizable P"  
    by (auto simp add: realizable_def sep_algebra_simps)
      
  lemma htriple_false: "htriple P c (λr s. False) ⟷ ¬realizable P"
    unfolding htriple_def STATE_def
    by (auto simp: wpa_false realizable_def)
    
    
  lemma htriple_realizable_preI: 
    assumes "realizable P ⟹ htriple P c Q"
    shows "htriple P c Q"
    using assms
    using cons_post_rule htriple_false by fastforce
    
  lemma STATE_realizableI: "STATE f P s ⟹ realizable P"  
    unfolding STATE_def realizable_def by auto
    
    
subsection ‹VCG Setup›    
    
lemma STATE_assn_cong[fri_extract_congs]: "P≡P' ⟹ STATE f P s ≡ STATE f P' s" by simp
  
lemma STATE_extract[vcg_normalize_simps]:
  "STATE asf (↑Φ) h ⟷ Φ ∧ STATE asf □ h"
  "STATE asf (↑Φ ** P) h ⟷ Φ ∧ STATE asf P h"
  "STATE asf (EXS x. Q x) h ⟷ (∃x. STATE asf (Q x) h)"
  "STATE asf (λ_. False) h ⟷ False"
  "STATE asf ((λ_. False) ** P) h ⟷ False"
  by (auto simp: STATE_def sep_algebra_simps)
 

definition POSTCOND where [vcg_tag_defs]: "POSTCOND ≡ STATE"
  
lemma POSTCONDI:
  "STATE asf Q h ⟹ POSTCOND asf Q h"
  by (auto simp add: POSTCOND_def)
lemma POSTCOND_cong[vcg_normalize_congs]: "POSTCOND asf Q = POSTCOND asf Q" ..

lemma POSTCOND_triv_simps[vcg_normalize_simps]:
  (* "POSTCOND A asf sep_true h" *)
  "¬POSTCOND asf sep_false h"
  unfolding POSTCOND_def STATE_def by auto
  
lemma start_entailsE:
  assumes "STATE asf P h"
  assumes "ENTAILS P P'"
  shows "STATE asf P' h"
  using assms unfolding STATE_def ENTAILS_def entails_def
  by auto

declaration ‹fn phi =>
   (Basic_VCG.add_xformer (map (Morphism.thm phi) @{thms POSTCONDI},@{binding postcond_xformer},
    fn ctxt => eresolve_tac ctxt (map (Morphism.thm phi) @{thms start_entailsE})
  ))
›

named_theorems htriple_vcg_intros
named_theorems htriple_vcg_intro_congs
definition [vcg_tag_defs]: "DECOMP_HTRIPLE φ ≡ φ"
lemma DECOMP_HTRIPLEI: "φ ⟹ DECOMP_HTRIPLE φ" unfolding vcg_tag_defs by simp

  lemma htriple_vcg_frame_erule[vcg_frame_erules]:
    assumes S: "STATE asf P' s"
    assumes F: "PRECOND (FRAME P' P F)"
    assumes HT: "htriple P c Q"  
    assumes P: "⋀r s. STATE asf (Q r ** F) s ⟹ PRECOND (EXTRACT (Q' r s))"
    shows "wpa asf c Q' s"
  proof -
    from S F have S': "STATE asf (P**F) s"
      unfolding PRECOND_def FRAME_def
      using STATE_monoI by blast

    show ?thesis
      apply (rule apply_htriple_rule[OF S' HT])
      using P unfolding vcg_tag_defs .
      
  qed    
  
  lemma htriple_vcgI': 
    assumes "⋀asf s. STATE asf P s ⟹ wpa asf c (λr. POSTCOND asf (Q r)) s"
    shows "htriple P c Q"
    apply (rule htripleI)
    using assms unfolding vcg_tag_defs .
  
  lemma htriple_vcgI[htriple_vcg_intros]: 
    assumes "⋀asf s. STATE asf P s ⟹ EXTRACT (wpa asf c (λr s. EXTRACT (POSTCOND asf (Q r) s)) s)"
    shows "htriple P c Q"
    apply (rule htripleI)
    using assms unfolding vcg_tag_defs STATE_def .

      
  lemma htriple_decompI[vcg_decomp_rules]: 
    "DECOMP_HTRIPLE (htriple P c Q) ⟹ htriple P c Q"
    unfolding vcg_tag_defs by auto

  lemma htriple_assn_cong[htriple_vcg_intro_congs]: 
    "P≡P' ⟹ Q≡Q' ⟹  htriple P c Q ≡ htriple P' c Q'" by simp

  lemma htriple_ent_pre:
    "P⊢P' ⟹ htriple P' c Q ⟹ htriple P c Q"
    unfolding entails_def
    apply (erule cons_rule) by blast+
    
  lemma htriple_ent_post:
    "⟦⋀r. Q r ⊢ Q' r⟧ ⟹ htriple P c Q ⟹ htriple P c Q'"
    unfolding entails_def
    apply (erule cons_rule) by blast+
   
  lemma htriple_pure_preI: "⟦pure_part P ⟹ htriple P c Q⟧ ⟹ htriple P c Q"  
    using entails_pureI htriple_ent_pre by blast
    
  
  declaration ‹
    fn phi => (Basic_VCG.add_xformer (map (Morphism.thm phi) @{thms DECOMP_HTRIPLEI},@{binding decomp_htriple_xformer},
      fn ctxt => 
        (full_simp_tac (put_simpset HOL_basic_ss ctxt 
          addsimps (Named_Theorems.get ctxt @{named_theorems vcg_tag_defs})
          |> fold Simplifier.add_cong (Named_Theorems.get ctxt @{named_theorems htriple_vcg_intro_congs})
        ))
        THEN' resolve_tac ctxt (Named_Theorems.get ctxt @{named_theorems htriple_vcg_intros})
    ))
  ›
  
  
end  

end