Theory Separation_Logic_Imperative_HOL.Assertions

section "Assertions"

theory Assertions
imports 
  "Tools/Imperative_HOL_Add" 
  "Tools/Syntax_Match" 
  Automatic_Refinement.Misc
begin

subsection ‹Partial Heaps›
text ‹
  A partial heap is modeled by a heap and a set of valid addresses, with the
  side condition that the valid addresses have to be within the limit of the
  heap. This modeling is somewhat strange for separation logic, however, it 
  allows us to solve some technical problems related to definition of 
  Hoare triples, that will be detailed later.
›
type_synonym pheap = "heap × addr set"

text ‹Predicate that expresses that the address set of a partial heap is 
  within the heap's limit.
›
fun in_range :: "(heap × addr set) ⇒ bool" 
  where "in_range (h,as) ⟷ (∀a∈as. a < lim h)"

declare in_range.simps[simp del]

lemma in_range_empty[simp, intro!]: "in_range (h,{})"
  by (auto simp: in_range.simps)

lemma in_range_dist_union[simp]: 
  "in_range (h,as ∪ as') ⟷ in_range (h,as) ∧ in_range (h,as')"
  by (auto simp: in_range.simps)

lemma in_range_subset: 
  "⟦as ⊆ as'; in_range (h,as')⟧ ⟹ in_range (h,as)"
  by (auto simp: in_range.simps)

text ‹Relation that holds if two heaps are identical on a given 
  address range›
definition relH :: "addr set ⇒ heap ⇒ heap ⇒ bool" 
  where "relH as h h' ≡ 
  in_range (h,as) 
  ∧ in_range (h',as) 
  ∧ (∀t. ∀a ∈ as. 
        refs h t a = refs h' t a 
      ∧ arrays h t a = arrays h' t a
    )"

lemma relH_in_rangeI:
  assumes "relH as h h'"
  shows "in_range (h,as)" and "in_range (h',as)"
  using assms unfolding relH_def by auto

text "Reflexivity"
lemma relH_refl: "in_range (h,as) ⟹ relH as h h"
  unfolding relH_def by simp

text "Symmetry"
lemma relH_sym: "relH as h h' ⟹ relH as h' h"
  unfolding relH_def
  by auto

text "Transitivity"
lemma relH_trans[trans]: "⟦relH as h1 h2; relH as h2 h3⟧ ⟹ relH as h1 h3"
  unfolding relH_def
  by auto

lemma relH_dist_union[simp]: 
  "relH (as∪as') h h' ⟷ relH as h h' ∧ relH as' h h'"
  unfolding relH_def
  by auto

lemma relH_subset:
  assumes "relH bs h h'"
  assumes "as ⊆ bs"
  shows "relH as h h'"
  using assms unfolding relH_def by (auto intro: in_range_subset)

lemma relH_ref:
  assumes "relH as h h'"
  assumes "addr_of_ref r ∈ as"
  shows "Ref.get h r = Ref.get h' r"
  using assms unfolding relH_def Ref.get_def by auto

lemma relH_array:
  assumes "relH as h h'"
  assumes "addr_of_array r ∈ as"
  shows "Array.get h r = Array.get h' r"
  using assms unfolding relH_def Array.get_def by auto

lemma relH_set_ref: "⟦ addr_of_ref r ∉ as; in_range (h,as)⟧ 
  ⟹ relH as h (Ref.set r x h)"
  unfolding relH_def Ref.set_def 
  by (auto simp: in_range.simps)

lemma relH_set_array: "⟦addr_of_array r ∉ as; in_range (h,as)⟧ 
  ⟹ relH as h (Array.set r x h)"
  unfolding relH_def Array.set_def 
  by (auto simp: in_range.simps)

subsection ‹Assertions›
text ‹
  Assertions are predicates on partial heaps, that fulfill a well-formedness 
  condition called properness: They only depend on the part of the heap
  by the address set, and must be false for partial heaps that are not in range.
›
type_synonym assn_raw = "pheap ⇒ bool"

definition proper :: "assn_raw ⇒ bool" where
  "proper P ≡ ∀h h' as. (P (h,as) ⟶ in_range (h,as)) 
    ∧ (P (h,as) ∧ relH as h h' ∧ in_range (h',as) ⟶ P (h',as))"

lemma properI[intro?]: 
  assumes "⋀as h. P (h,as) ⟹ in_range (h,as)"
  assumes "⋀as h h'. 
    ⟦P (h,as); relH as h h'; in_range (h',as)⟧ ⟹ P (h',as)"
  shows "proper P"
  unfolding proper_def using assms by blast

lemma properD1:
  assumes "proper P"
  assumes "P (h,as)"
  shows "in_range (h,as)"
  using assms unfolding proper_def by blast

lemma properD2:
  assumes "proper P"
  assumes "P (h,as)"
  assumes "relH as h h'"
  assumes "in_range (h',as)"
  shows "P (h',as)"
  using assms unfolding proper_def by blast

lemmas properD = properD1 properD2

lemma proper_iff:
  assumes "proper P"
  assumes "relH as h h'"
  assumes "in_range (h',as)"
  shows "P (h,as) ⟷ P (h',as)"
  using assms
  by (metis properD2 relH_in_rangeI(1) relH_sym) 

text ‹We encapsulate assertions in their own type›  
typedef assn = "Collect proper" 
  apply simp
  unfolding proper_def 
  by fastforce

lemmas [simp] = Rep_assn_inverse Rep_assn_inject 
lemmas [simp, intro!] = Rep_assn[unfolded mem_Collect_eq]

lemma Abs_assn_eqI[intro?]: 
  "(⋀h. P h = Rep_assn Pr h) ⟹ Abs_assn P = Pr"
  "(⋀h. P h = Rep_assn Pr h) ⟹ Pr = Abs_assn P"
  by (metis Rep_assn_inverse predicate1I xt1(5))+

abbreviation models :: "pheap ⇒ assn ⇒ bool" (infix "⊨" 50) 
  where "h⊨P ≡ Rep_assn P h"


lemma models_in_range: "h⊨P ⟹ in_range h"
  apply (cases h)
  by (metis mem_Collect_eq Rep_assn properD1)
    
subsubsection ‹Empty Partial Heap›
text ‹The empty partial heap satisfies some special properties.
  We set up a simplification that tries to rewrite it to the standard
  empty partial heap ‹h⇩⊥››
abbreviation h_bot ("h⇩⊥") where "h⇩⊥ ≡ (undefined,{})"
lemma mod_h_bot_indep: "(h,{})⊨P ⟷ (h',{})⊨P"
  by (metis mem_Collect_eq Rep_assn emptyE in_range_empty 
    proper_iff relH_def)

lemma mod_h_bot_normalize[simp]: 
  "syntax_fo_nomatch undefined h ⟹ (h,{})⊨P ⟷ h⇩⊥ ⊨ P"
  using mod_h_bot_indep[where h'=undefined] by simp

text ‹Properness, lifted to the assertion type.›
lemma mod_relH: "relH as h h' ⟹ (h,as)⊨P ⟷ (h',as)⊨P"
  by (metis mem_Collect_eq Rep_assn proper_iff relH_in_rangeI(2))
    
subsection ‹Connectives›
text ‹
  We define several operations on assertions, and instantiate some type classes.
›

subsubsection ‹Empty Heap and Separation Conjunction›
text ‹The assertion that describes the empty heap, and the separation
  conjunction form a commutative monoid:›
instantiation assn :: one begin
  fun one_assn_raw :: "pheap ⇒ bool" 
    where "one_assn_raw (h,as) ⟷ as={}"
  
  lemma one_assn_proper[intro!,simp]: "proper one_assn_raw"
    by (auto intro!: properI)
  
  definition one_assn :: assn where "1 ≡ Abs_assn one_assn_raw"
  instance ..
end

abbreviation one_assn::assn ("emp") where "one_assn ≡ 1"
  
instantiation assn :: times begin
  fun times_assn_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
    "times_assn_raw P Q (h,as) 
    = (∃as1 as2. as=as1∪as2 ∧ as1∩as2={} 
        ∧ P (h,as1) ∧ Q (h,as2))"

  lemma times_assn_proper[intro!,simp]: 
    "proper P ⟹ proper Q ⟹ proper (times_assn_raw P Q)"
    apply (rule properI)
    apply (auto dest: properD1) []
    apply clarsimp
    apply (drule (3) properD2)
    apply (drule (3) properD2)
    apply blast
    done

  definition times_assn where "P*Q ≡ 
    Abs_assn (times_assn_raw (Rep_assn P) (Rep_assn Q))"

  instance ..
end

lemma mod_star_conv: "h⊨A*B 
  ⟷ (∃hr as1 as2. h=(hr,as1∪as2) ∧ as1∩as2={} ∧ (hr,as1)⊨A ∧ (hr,as2)⊨B)"
  unfolding times_assn_def
  apply (cases h)
  by (auto simp: Abs_assn_inverse)

lemma mod_starD: "h⊨A*B ⟹ ∃h1 h2. h1⊨A ∧ h2⊨B"
  by (auto simp: mod_star_conv)

lemma star_assnI:
  assumes "(h,as)⊨P" and "(h,as')⊨Q" and "as∩as'={}"
  shows "(h,as∪as')⊨P*Q"
  using assms unfolding times_assn_def
  by (auto simp: Abs_assn_inverse)
 
instantiation assn :: comm_monoid_mult begin
  lemma assn_one_left: "1*P = (P::assn)"
    unfolding one_assn_def times_assn_def
    apply (rule)
    apply (auto simp: Abs_assn_inverse)
    done

  lemma assn_times_comm: "P*Q = Q*(P::assn)"
    unfolding times_assn_def
    apply rule
    apply (fastforce simp add: Abs_assn_inverse Un_ac)
    done

  lemma assn_times_assoc: "(P*Q)*R = P*(Q*(R::assn))"
    unfolding times_assn_def
    apply rule
    apply (auto simp: Abs_assn_inverse)
    apply (rule_tac x="as1∪as1a" in exI)
    apply (rule_tac x="as2a" in exI)
    apply (auto simp add: Un_ac) []

    apply (rule_tac x="as1a" in exI)
    apply (rule_tac x="as2a∪as2" in exI)
    apply (fastforce simp add: Un_ac) []
    done

  instance 
    apply standard
    apply (rule assn_times_assoc)
    apply (rule assn_times_comm)
    apply (rule assn_one_left)
    done

end
  
subsubsection ‹Magic Wand›
fun wand_raw :: "assn_raw ⇒ assn_raw ⇒ assn_raw" where
  "wand_raw P Q (h,as) ⟷ in_range (h,as) 
  ∧ (∀h' as'. as∩as'={} ∧ relH as h h' ∧ in_range (h',as)
    ∧ P (h',as')
    ⟶ Q (h',as∪as'))"

lemma wand_proper[simp, intro!]: "proper (wand_raw P Q)"
  apply (rule properI)
  apply simp
  apply (auto dest: relH_trans)
  done

definition 
  wand_assn :: "assn ⇒ assn ⇒ assn" (infixl "-*" 56)
  where "P-*Q ≡ Abs_assn (wand_raw (Rep_assn P) (Rep_assn Q))"

lemma wand_assnI: 
  assumes "in_range (h,as)"
  assumes "⋀h' as'. ⟦
    as ∩ as' = {}; 
    relH as h h'; 
    in_range (h',as); 
    (h',as')⊨Q 
  ⟧ ⟹ (h',as∪as') ⊨ R"
  shows "(h,as) ⊨ Q -* R"
  using assms 
  unfolding wand_assn_def
  apply (auto simp: Abs_assn_inverse)
  done

subsubsection ‹Boolean Algebra on Assertions›
instantiation assn :: boolean_algebra begin
  definition top_assn where "top ≡ Abs_assn in_range"
  definition bot_assn where "bot ≡ Abs_assn (λ_. False)"
  definition sup_assn where "sup P Q ≡ Abs_assn (λh. h⊨P ∨ h⊨Q)"
  definition inf_assn where "inf P Q ≡ Abs_assn (λh. h⊨P ∧ h⊨Q)"
  definition uminus_assn where 
    "-P ≡ Abs_assn (λh. in_range h ∧ ¬h⊨P)"

  lemma bool_assn_proper[simp, intro!]:
    "proper in_range"
    "proper (λ_. False)"
    "proper P ⟹ proper Q ⟹ proper (λh. P h ∨ Q h)"
    "proper P ⟹ proper Q ⟹ proper (λh. P h ∧ Q h)"
    "proper P ⟹ proper (λh. in_range h ∧ ¬P h)"
    apply (auto 
      intro!: properI 
      intro: relH_in_rangeI 
      dest: properD1 
      simp: proper_iff)
    done

  text ‹(And, Or, True, False, Not) are a Boolean algebra. 
    Due to idiosyncrasies of the Isabelle/HOL class setup, we have to
    also define a difference and an ordering:›
  definition less_eq_assn where
  [simp]: "(a::assn) ≤ b ≡ a = inf a b"

  definition less_assn where
  [simp]: "(a::assn) < b ≡ a ≤ b ∧ a≠b"

  definition minus_assn where
  [simp]: "(a::assn) - b ≡ inf a (-b)"

  instance
    apply standard
    unfolding 
      top_assn_def bot_assn_def sup_assn_def inf_assn_def uminus_assn_def
      less_eq_assn_def less_assn_def minus_assn_def
    apply (auto 
      simp: Abs_assn_inverse conj_commute conj_ac 
      intro: Abs_assn_eqI models_in_range)
    apply rule
    apply (metis (mono_tags) Abs_assn_inverse[unfolded mem_Collect_eq]
      Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
    apply rule
    apply (metis (mono_tags)
      Abs_assn_inverse[unfolded mem_Collect_eq]
      Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
    apply rule
    apply (simp add: Abs_assn_inverse)
    apply (metis (mono_tags) 
      Abs_assn_inverse[unfolded mem_Collect_eq] 
      Rep_assn[unfolded mem_Collect_eq] bool_assn_proper(4))
    done

end

text ‹We give the operations some more standard names›
abbreviation top_assn::assn ("true") where "top_assn ≡ top"
abbreviation bot_assn::assn ("false") where "bot_assn ≡ bot"
abbreviation sup_assn::"assn⇒assn⇒assn" (infixr "∨⇩A" 61) 
  where "sup_assn ≡ sup"
abbreviation inf_assn::"assn⇒assn⇒assn" (infixr "∧⇩A" 62) 
  where "inf_assn ≡ inf"
abbreviation uminus_assn::"assn ⇒ assn" ("¬⇩A _" [81] 80) 
  where "uminus_assn ≡ uminus"

text ‹Now we prove some relations between the Boolean algebra operations
  and the (empty heap,separation conjunction) monoid›

lemma star_false_left[simp]: "false * P = false"
  unfolding times_assn_def bot_assn_def
  apply rule
  apply (auto simp add: Abs_assn_inverse)
  done

lemma star_false_right[simp]: "P * false = false"
  using star_false_left by (simp add: assn_times_comm)

lemmas star_false = star_false_left star_false_right 
  
lemma assn_basic_inequalities[simp, intro!]:
  "true ≠ emp" "emp ≠ true"
  "false ≠ emp" "emp ≠ false"
  "true ≠ false" "false ≠ true"
  subgoal 
    unfolding one_assn_def top_assn_def
    proof (subst Abs_assn_inject; simp?) 
      have "in_range (⦇arrays = (λ_ _. []), refs = (λ_ _. 0), lim = 1⦈,{0})" (is "in_range ?h")
        by (auto simp: in_range.simps)
      moreover have "¬one_assn_raw ?h" by auto
      ultimately show "in_range ≠ one_assn_raw" by auto
    qed      
  subgoal
    by (simp add: ‹true ≠ emp›)
  subgoal
  using star_false_left ‹true ≠ emp› by force
  subgoal
    by (simp add: ‹false ≠ emp›)
  subgoal
    by (metis inf_bot_right inf_top.right_neutral ‹true ≠ emp›)
  subgoal
    using ‹true ≠ false› by auto
  done
  
  
subsubsection ‹Existential Quantification›
definition ex_assn :: "('a ⇒ assn) ⇒ assn" (binder "∃⇩A" 11)
  where "(∃⇩Ax. P x) ≡ Abs_assn (λh. ∃x. h⊨P x)"

lemma ex_assn_proper[simp, intro!]: 
  "(⋀x. proper (P x)) ⟹ proper (λh. ∃x. P x h)"
  by (auto intro!: properI dest: properD1 simp: proper_iff)

lemma ex_assn_const[simp]: "(∃⇩Ax. c) = c" 
  unfolding ex_assn_def by auto

lemma ex_one_point_gen: 
  "⟦⋀h x. h⊨P x ⟹ x=v⟧ ⟹ (∃⇩Ax. P x) = (P v)"
  unfolding ex_assn_def
  apply rule
  apply auto
  done

lemma ex_distrib_star: "(∃⇩Ax. P x * Q) = (∃⇩Ax. P x) * Q"
  unfolding ex_assn_def times_assn_def
  apply rule
  apply (simp add: Abs_assn_inverse)
  apply fastforce
  done

lemma ex_distrib_and: "(∃⇩Ax. P x ∧⇩A Q) = (∃⇩Ax. P x) ∧⇩A Q"
  unfolding ex_assn_def inf_assn_def
  apply rule
  apply (simp add: Abs_assn_inverse)
  done

lemma ex_distrib_or: "(∃⇩Ax. P x ∨⇩A Q) = (∃⇩Ax. P x) ∨⇩A Q"
  unfolding ex_assn_def sup_assn_def
  apply rule
  apply (auto simp add: Abs_assn_inverse)
  done

lemma ex_join_or: "(∃⇩Ax. P x ∨⇩A (∃⇩Ax. Q x)) = (∃⇩Ax. P x ∨⇩A Q x)"
  unfolding ex_assn_def sup_assn_def
  apply rule
  apply (auto simp add: Abs_assn_inverse)
  done

subsubsection ‹Pure Assertions›
text ‹Pure assertions do not depend on any heap content.›
fun pure_assn_raw where "pure_assn_raw b (h,as) ⟷ as={} ∧ b"
definition pure_assn :: "bool ⇒ assn" ("↑") where
  "↑b ≡ Abs_assn (pure_assn_raw b)"

lemma pure_assn_proper[simp, intro!]: "proper (pure_assn_raw b)"
  by (auto intro!: properI intro: relH_in_rangeI)


    
lemma pure_true[simp]: "↑True = emp"
  unfolding pure_assn_def one_assn_def 
  apply rule
  apply (simp add: Abs_assn_inverse)
  apply (auto)
  done

lemma pure_false[simp]: "↑False = false"
  unfolding pure_assn_def bot_assn_def 
  apply rule
  apply (auto simp: Abs_assn_inverse)
  done

lemma pure_assn_eq_false_iff[simp]: "↑P = false ⟷ ¬P" by auto
  
lemma pure_assn_eq_emp_iff[simp]: "↑P = emp ⟷ P" by (cases P) auto
    
lemma merge_pure_star[simp]: 
  "↑a * ↑b = ↑(a∧b)"
  unfolding times_assn_def
  apply rule
  unfolding pure_assn_def
  apply (simp add: Abs_assn_inverse)
  apply fastforce
  done

lemma merge_true_star[simp]: "true*true = true"
  unfolding times_assn_def top_assn_def
  apply rule
  apply (simp add: Abs_assn_inverse)
  apply (fastforce simp: in_range.simps)
  done

lemma merge_pure_and[simp]:
  "↑a ∧⇩A ↑b = ↑(a∧b)"
  unfolding inf_assn_def
  apply rule
  unfolding pure_assn_def
  apply (simp add: Abs_assn_inverse)
  apply fastforce
  done

lemma merge_pure_or[simp]:
  "↑a ∨⇩A ↑b = ↑(a∨b)"
  unfolding sup_assn_def
  apply rule
  unfolding pure_assn_def
  apply (simp add: Abs_assn_inverse)
  apply fastforce
  done

    
lemma pure_assn_eq_conv[simp]: "↑P = ↑Q ⟷ P=Q" by auto
    
definition "is_pure_assn a ≡ ∃P. a=↑P"
lemma is_pure_assnE: assumes "is_pure_assn a" obtains P where "a=↑P"
  using assms
  by (auto simp: is_pure_assn_def)

lemma is_pure_assn_pure[simp, intro!]: "is_pure_assn (↑P)" 
  by (auto simp add: is_pure_assn_def)

lemma is_pure_assn_basic_simps[simp]:
  "is_pure_assn false"
  "is_pure_assn emp"
proof -
  have "is_pure_assn (↑False)" by rule thus "is_pure_assn false" by simp
  have "is_pure_assn (↑True)" by rule thus "is_pure_assn emp" by simp
qed  

lemma is_pure_assn_starI[simp,intro!]: 
  "⟦is_pure_assn a; is_pure_assn b⟧ ⟹ is_pure_assn (a*b)"
  by (auto elim!: is_pure_assnE)
    
    
    
    
subsubsection ‹Pointers›
text ‹In Imperative HOL, we have to distinguish between pointers to single
  values and pointers to arrays. For both, we define assertions that 
  describe the part of the heap that a pointer points to.›
fun sngr_assn_raw :: "'a::heap ref ⇒ 'a ⇒ assn_raw" where
  "sngr_assn_raw r x (h,as) ⟷ Ref.get h r = x ∧ as = {addr_of_ref r} ∧ 
  addr_of_ref r < lim h"

lemma sngr_assn_proper[simp, intro!]: "proper (sngr_assn_raw r x)"
  apply (auto intro!: properI simp: relH_ref)
  apply (simp add: in_range.simps)
  apply (auto simp add: in_range.simps dest: relH_in_rangeI)
  done

definition sngr_assn :: "'a::heap ref ⇒ 'a ⇒ assn" (infix "↦⇩r" 82) 
  where "r↦⇩rx ≡ Abs_assn (sngr_assn_raw r x)"

fun snga_assn_raw :: "'a::heap array ⇒ 'a list ⇒ assn_raw" 
  where "snga_assn_raw r x (h,as) 
  ⟷ Array.get h r = x ∧ as = {addr_of_array r} 
      ∧ addr_of_array r < lim h"

lemma snga_assn_proper[simp, intro!]: "proper (snga_assn_raw r x)"
  apply (auto intro!: properI simp: relH_array)
  apply (simp add: in_range.simps)
  apply (auto simp add: in_range.simps dest: relH_in_rangeI)
  done

definition 
  snga_assn :: "'a::heap array ⇒ 'a list ⇒ assn" (infix "↦⇩a" 82)
  where "r↦⇩aa ≡ Abs_assn (snga_assn_raw r a)"

text ‹Two disjoint parts of the heap cannot be pointed to by the 
  same pointer›
lemma sngr_same_false[simp]: 
  "p ↦⇩r x * p ↦⇩r y = false"
  unfolding times_assn_def bot_assn_def sngr_assn_def
  apply rule
  apply (auto simp: Abs_assn_inverse)
  done

lemma snga_same_false[simp]: 
  "p ↦⇩a x * p ↦⇩a y = false"
  unfolding times_assn_def bot_assn_def snga_assn_def
  apply rule
  apply (auto simp: Abs_assn_inverse)
  done

subsection ‹Properties of the Models-Predicate›
lemma mod_true[simp]: "h⊨true ⟷ in_range h"
  unfolding top_assn_def by (simp add: Abs_assn_inverse)
lemma mod_false[simp]: "¬ h⊨false"
  unfolding bot_assn_def by (simp add: Abs_assn_inverse)

lemma mod_emp: "h⊨emp ⟷ snd h = {}"
  unfolding one_assn_def by (cases h) (simp add: Abs_assn_inverse)
  
lemma mod_emp_simp[simp]: "(h,{})⊨emp"
  by (simp add: mod_emp)

lemma mod_pure[simp]: "h⊨↑b ⟷ snd h = {} ∧ b"
  unfolding pure_assn_def 
  apply (cases h) 
  apply (auto simp add: Abs_assn_inverse)
  done

lemma mod_ex_dist[simp]: "h⊨(∃⇩Ax. P x) ⟷ (∃x. h⊨P x)"
  unfolding ex_assn_def by (auto simp: Abs_assn_inverse)
  
lemma mod_exI: "∃x. h⊨P x ⟹ h⊨(∃⇩Ax. P x)"
  by (auto simp: mod_ex_dist)
lemma mod_exE: assumes "h⊨(∃⇩Ax. P x)" obtains x where "h⊨P x"
  using assms by (auto simp: mod_ex_dist)

(* Not declared as simp, to not interfere with precision.
  TODO: Perhaps define own connector for precision claims?
*)
lemma mod_and_dist: "h⊨P∧⇩AQ ⟷ h⊨P ∧ h⊨Q"
  unfolding inf_assn_def by (simp add: Abs_assn_inverse)

lemma mod_or_dist[simp]: "h⊨P∨⇩AQ ⟷ h⊨P ∨ h⊨Q"
  unfolding sup_assn_def by (simp add: Abs_assn_inverse)

lemma mod_not_dist[simp]: "h⊨(¬⇩AP) ⟷ in_range h ∧ ¬ h⊨P"
  unfolding uminus_assn_def by (simp add: Abs_assn_inverse)

lemma mod_pure_star_dist[simp]: "h⊨P*↑b ⟷ h⊨P ∧ b"
  by (metis (full_types) mod_false mult_1_right pure_false 
    pure_true star_false_right)

lemmas mod_dist = mod_pure mod_pure_star_dist mod_ex_dist mod_and_dist
  mod_or_dist mod_not_dist

lemma mod_star_trueI: "h⊨P ⟹ h⊨P*true"
  unfolding times_assn_def top_assn_def
  apply (simp add: Abs_assn_inverse)
  apply (cases h)
  apply auto
  done

lemma mod_star_trueE': assumes "h⊨P*true" obtains h' where 
  "fst h' = fst h" and "snd h' ⊆ snd h" and "h'⊨P"
  using assms
  unfolding times_assn_def top_assn_def
  apply (cases h)
  apply (fastforce simp add: Abs_assn_inverse)
  done

lemma mod_star_trueE: assumes "h⊨P*true" obtains h' where "h'⊨P"
  using assms by (blast elim: mod_star_trueE')

lemma mod_h_bot_iff[simp]:
  "(h,{}) ⊨ ↑b ⟷ b"
  "(h,{}) ⊨ true"
  "(h,{}) ⊨ p↦⇩rx ⟷ False"
  "(h,{}) ⊨ q↦⇩ay ⟷ False"
  "(h,{}) ⊨ P*Q ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
  "(h,{}) ⊨ P∧⇩AQ ⟷ ((h,{}) ⊨ P) ∧ ((h,{}) ⊨ Q)"
  "(h,{}) ⊨ P∨⇩AQ ⟷ ((h,{}) ⊨ P) ∨ ((h,{}) ⊨ Q)"
  "(h,{}) ⊨ (∃⇩Ax. R x) ⟷ (∃x. (h,{}) ⊨ R x)"
  apply (simp add: pure_assn_def Abs_assn_inverse)
  apply simp
  apply (simp add: sngr_assn_def Abs_assn_inverse)
  apply (simp add: snga_assn_def Abs_assn_inverse)
  apply (simp add: times_assn_def Abs_assn_inverse)
  apply (simp add: inf_assn_def Abs_assn_inverse)
  apply (simp add: sup_assn_def Abs_assn_inverse)
  apply (simp add: ex_assn_def Abs_assn_inverse)
  done

subsection ‹Entailment›
definition entails :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩A" 10)
  where "P ⟹⇩A Q ≡ ∀h. h⊨P ⟶ h⊨Q"

lemma entailsI: 
  assumes "⋀h. h⊨P ⟹ h⊨Q"
  shows "P ⟹⇩A Q" 
  using assms unfolding entails_def by auto

lemma entailsD: 
  assumes "P ⟹⇩A Q"
  assumes "h⊨P"
  shows "h⊨Q" 
  using assms unfolding entails_def by blast

subsubsection ‹Properties›
lemma ent_fwd: 
  assumes "h⊨P"
  assumes "P ⟹⇩A Q"
  shows "h⊨Q" using assms(2,1) by (rule entailsD)

lemma ent_refl[simp]: "P ⟹⇩A P"
  by (auto simp: entailsI)

lemma ent_trans[trans]: "⟦ P ⟹⇩A Q; Q ⟹⇩AR ⟧ ⟹ P ⟹⇩A R"
  by (auto intro: entailsI dest: entailsD)

lemma ent_iffI:
  assumes "A⟹⇩AB"
  assumes "B⟹⇩AA"
  shows "A=B"
  apply (subst Rep_assn_inject[symmetric])
  apply (rule ext)
  using assms unfolding entails_def
  by blast

lemma ent_false[simp]: "false ⟹⇩A P"
  by (auto intro: entailsI)
lemma ent_true[simp]: "P ⟹⇩A true"
  by (auto intro!: entailsI simp: models_in_range)

lemma ent_false_iff[simp]: "(P ⟹⇩A false) ⟷ (∀h. ¬h⊨P)"
  unfolding entails_def
  by auto

lemma ent_pure_pre_iff[simp]: "(P*↑b ⟹⇩A Q) ⟷ (b ⟶ (P ⟹⇩A Q))"
  unfolding entails_def
  by (auto simp add: mod_dist)

lemma ent_pure_pre_iff_sng[simp]: 
  "(↑b ⟹⇩A Q) ⟷ (b ⟶ (emp ⟹⇩A Q))"
  using ent_pure_pre_iff[where P=emp]
  by simp

lemma ent_pure_post_iff[simp]: 
  "(P ⟹⇩A Q*↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A Q))"
  unfolding entails_def
  by (auto simp add: mod_dist)

lemma ent_pure_post_iff_sng[simp]: 
  "(P ⟹⇩A ↑b) ⟷ ((∀h. h⊨P ⟶ b) ∧ (P ⟹⇩A emp))"
  using ent_pure_post_iff[where Q=emp]
  by simp

lemma ent_ex_preI: "(⋀x. P x ⟹⇩A Q) ⟹ ∃⇩Ax. P x ⟹⇩A Q"
  unfolding entails_def ex_assn_def
  by (auto simp: Abs_assn_inverse)

lemma ent_ex_postI: "(P ⟹⇩A Q x) ⟹ P ⟹⇩A ∃⇩Ax. Q x"
  unfolding entails_def ex_assn_def
  by (auto simp: Abs_assn_inverse)

lemma ent_mp: "(P * (P -* Q)) ⟹⇩A Q"
  apply (rule entailsI)
  unfolding times_assn_def wand_assn_def
  apply (clarsimp simp add: Abs_assn_inverse)
  apply (drule_tac x="a" in spec)
  apply (drule_tac x="as1" in spec)
  apply (auto simp: Un_ac relH_refl)
  done

lemma ent_star_mono: "⟦ P ⟹⇩A P'; Q ⟹⇩A Q'⟧ ⟹ P*Q ⟹⇩A P'*Q'"
  unfolding entails_def times_assn_def
  apply (simp add: Abs_assn_inverse)
  apply metis
  done

lemma ent_wandI:
  assumes IMP: "Q*P ⟹⇩A R"
  shows "P ⟹⇩A (Q -* R)"
  unfolding entails_def 
  apply clarsimp
  apply (rule wand_assnI)
  apply (blast intro: models_in_range)
proof -
  fix h as h' as'
  assume "(h,as)⊨P" 
    and "as∩as'={}" 
    and "relH as h h'" 
    and "in_range (h',as)" 
    and "(h',as') ⊨ Q"

  from ‹(h,as)⊨P› and ‹relH as h h'› have "(h',as)⊨P" 
    by (simp add: mod_relH)
  with ‹(h',as') ⊨ Q› and ‹as∩as'={}› have "(h',as∪as')⊨Q*P" 
    by (metis star_assnI Int_commute Un_commute)
  with IMP show "(h',as∪as') ⊨ R" by (blast dest: ent_fwd)
qed

lemma ent_disjI1:
  assumes "P ∨⇩A Q ⟹⇩A R" 
  shows "P ⟹⇩A R" using assms unfolding entails_def by simp

lemma ent_disjI2:
  assumes "P ∨⇩A Q ⟹⇩A R" 
  shows "Q ⟹⇩A R" using assms unfolding entails_def by simp

lemma ent_disjI1_direct[simp]: "A ⟹⇩A A ∨⇩A B"
  by (simp add: entails_def)

lemma ent_disjI2_direct[simp]: "B ⟹⇩A A ∨⇩A B"
  by (simp add: entails_def)
    
lemma ent_disjE: "⟦ A⟹⇩AC; B⟹⇩AC ⟧ ⟹ A∨⇩AB ⟹⇩AC"
  unfolding entails_def by auto

lemma ent_conjI: "⟦ A⟹⇩AB; A⟹⇩AC ⟧ ⟹ A ⟹⇩A B ∧⇩A C"  
  unfolding entails_def by (auto simp: mod_and_dist)

lemma ent_conjE1: "⟦A⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
  unfolding entails_def by (auto simp: mod_and_dist)
lemma ent_conjE2: "⟦B⟹⇩AC⟧ ⟹ A∧⇩AB⟹⇩AC"
  unfolding entails_def by (auto simp: mod_and_dist)



lemma star_or_dist1: 
  "(A ∨⇩A B)*C = (A*C ∨⇩A B*C)"  
  apply (rule ent_iffI) 
  unfolding entails_def
  by (auto simp add: mod_star_conv) 
  
lemma star_or_dist2: 
  "C*(A ∨⇩A B) = (C*A ∨⇩A C*B)"  
  apply (rule ent_iffI) 
  unfolding entails_def
  by (auto simp add: mod_star_conv) 

lemmas star_or_dist = star_or_dist1 star_or_dist2  
    
lemma ent_disjI1': "A⟹⇩AB ⟹ A⟹⇩AB∨⇩AC"
  by (auto simp: entails_def star_or_dist)

lemma ent_disjI2': "A⟹⇩AC ⟹ A⟹⇩AB∨⇩AC"
  by (auto simp: entails_def star_or_dist)

lemma triv_exI[simp, intro!]: "Q x ⟹⇩A ∃⇩Ax. Q x"
  by (meson ent_ex_postI ent_refl)
    
subsubsection ‹Weak Entails›    
text ‹Weakening of entails to allow arbitrary unspecified memory in conclusion›
definition entailst :: "assn ⇒ assn ⇒ bool" (infix "⟹⇩t" 10)
  where "entailst A B ≡ A ⟹⇩A B * true"

lemma enttI: "A⟹⇩AB*true ⟹ A⟹⇩tB" unfolding entailst_def .
lemma enttD: "A⟹⇩tB ⟹ A⟹⇩AB*true" unfolding entailst_def .
    
lemma entt_trans:
  "entailst A B ⟹ entailst B C ⟹ entailst A C"
  unfolding entailst_def
  apply (erule ent_trans)
  by (metis assn_times_assoc ent_star_mono ent_true merge_true_star)  

lemma entt_refl[simp, intro!]: "entailst A A"
  unfolding entailst_def
  by (simp add: entailsI mod_star_trueI)

lemma entt_true[simp, intro!]:
  "entailst A true"
  unfolding entailst_def by simp

lemma entt_emp[simp, intro!]:
  "entailst A emp"
  unfolding entailst_def by simp

lemma entt_star_true_simp[simp]:
  "entailst A (B*true) ⟷ entailst A B"
  "entailst (A*true) B ⟷ entailst A B"
  unfolding entailst_def 
  subgoal by (auto simp: assn_times_assoc)
  subgoal
    apply (intro iffI)
    subgoal using entails_def mod_star_trueI by blast  
    subgoal by (metis assn_times_assoc ent_refl ent_star_mono merge_true_star)  
    done
  done

lemma entt_star_mono: "⟦entailst A B; entailst C D⟧ ⟹ entailst (A*C) (B*D)"
  unfolding entailst_def
proof -
  assume a1: "A ⟹⇩A B * true"
  assume "C ⟹⇩A D * true"
  then have "A * C ⟹⇩A true * B * (true * D)"
    using a1 assn_times_comm ent_star_mono by force
  then show "A * C ⟹⇩A B * D * true"
    by (simp add: ab_semigroup_mult_class.mult.left_commute assn_times_comm)
qed  
    
lemma entt_frame_fwd:
  assumes "entailst P Q"
  assumes "entailst A (P*F)"
  assumes "entailst (Q*F) B"
  shows "entailst A B"
  using assms
  by (metis entt_refl entt_star_mono entt_trans)

lemma enttI_true: "P*true ⟹⇩A Q*true ⟹ P⟹⇩tQ"
  by (drule enttI) simp

lemma entt_def_true: "(P⟹⇩tQ) ≡ (P*true ⟹⇩A Q*true)"
  unfolding entailst_def
  apply (rule eq_reflection)
  using entailst_def entt_star_true_simp(2) by auto  

lemma ent_imp_entt: "P⟹⇩AQ ⟹ P⟹⇩tQ" 
  apply (rule enttI)
  apply (erule ent_trans)
  by (simp add: entailsI mod_star_trueI)  

lemma entt_disjI1_direct[simp]: "A ⟹⇩t A ∨⇩A B"
  by (rule ent_imp_entt[OF ent_disjI1_direct])

lemma entt_disjI2_direct[simp]: "B ⟹⇩t A ∨⇩A B"
  by (rule ent_imp_entt[OF ent_disjI2_direct])

lemma entt_disjI1': "A⟹⇩tB ⟹ A⟹⇩tB∨⇩AC"
  by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjI2': "A⟹⇩tC ⟹ A⟹⇩tB∨⇩AC"
  by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjE: "⟦ A⟹⇩tM; B⟹⇩tM ⟧ ⟹ A∨⇩AB ⟹⇩t M"
  using ent_disjE enttD enttI by blast  
    
lemma entt_disjD1: "A∨⇩AB⟹⇩tC ⟹ A⟹⇩tC"
  using entt_disjI1_direct entt_trans by blast

lemma entt_disjD2: "A∨⇩AB⟹⇩tC ⟹ B⟹⇩tC"
  using entt_disjI2_direct entt_trans by blast
    
    
subsection ‹Precision›
text ‹
  Precision rules describe that parts of an assertion may depend only on the
  underlying heap. For example, the data where a pointer points to is the same
  for the same heap.
›
text ‹Precision rules should have the form: 
  @{text [display] "∀x y. (h⊨(P x * F1) ∧⇩A (P y * F2)) ⟶ x=y"}›
definition "precise R ≡ ∀a a' h p F F'. 
  h ⊨ R a p * F ∧⇩A R a' p * F' ⟶ a = a'"

lemma preciseI[intro?]: 
  assumes "⋀a a' h p F F'. h ⊨ R a p * F ∧⇩A R a' p * F' ⟹ a = a'"
  shows "precise R"
  using assms unfolding precise_def by blast

lemma preciseD:
  assumes "precise R"
  assumes "h ⊨ R a p * F ∧⇩A R a' p * F'"
  shows "a=a'"
  using assms unfolding precise_def by blast

lemma preciseD':
  assumes "precise R"
  assumes "h ⊨ R a p * F" 
  assumes "h ⊨ R a' p * F'"
  shows "a=a'"
  apply (rule preciseD)
  apply (rule assms)
  apply (simp only: mod_and_dist)
  apply (blast intro: assms)
  done

lemma precise_extr_pure[simp]: 
  "precise (λx y. ↑P * R x y) ⟷ (P ⟶ precise R)"
  "precise (λx y. R x y * ↑P) ⟷ (P ⟶ precise R)"
  apply (cases P, (auto intro!: preciseI) [2])+
  done

lemma sngr_prec: "precise (λx p. p↦⇩rx)"
  apply rule
  apply (clarsimp simp: mod_and_dist)
  unfolding sngr_assn_def times_assn_def
  apply (simp add: Abs_assn_inverse)
  apply auto
  done

lemma snga_prec: "precise (λx p. p↦⇩ax)"
  apply rule
  apply (clarsimp simp: mod_and_dist)
  unfolding snga_assn_def times_assn_def
  apply (simp add: Abs_assn_inverse)
  apply auto
  done

end