Session Separation_Logic_Imperative_HOL

Theory Imperative_HOL_Add

section ‹Additions to Imperative/HOL›
theory Imperative_HOL_Add
imports "HOL-Imperative_HOL.Imperative_HOL" 
begin 

text ‹This theory loads the Imperative HOL framework and provides 
        some additional lemmas needed for the separation logic framework.› 

text ‹A stronger elimination rule for ref›

lemma effect_ref[effect_elims]:
  assumes "effect (ref (x::('a::heap))) h h' r"
  obtains "r = fst (Ref.alloc x h)" and "h' = snd (Ref.alloc x h)"
proof -
  from assms have "execute (ref x) h = Some (r, h')" by (unfold effect_def)
  then have "r = fst (Ref.alloc x h)" "h' = snd (Ref.alloc x h)" 
    by (auto simp add: execute_simps)
  then show thesis ..
qed


text ‹Some lemmas about the evaluation of the limit for modifications on 
  a heap›

lemma lim_Ref_alloc[simp]: "lim (snd (Ref.alloc x h)) = Suc (lim h)"
  unfolding Ref.alloc_def
  by (simp add: Let_def)

lemma lim_Array_alloc[simp]: "lim (snd (Array.alloc x h)) = Suc (lim h)"
  unfolding Array.alloc_def Array.set_def
  by (simp add: Let_def)


lemma lim_Array_set[simp]: "lim (Array.set a xs h) = lim h"
  unfolding Array.set_def
  by (simp add: Let_def)

thm Array.update_def
lemma lim_Array_update[simp]: "lim (Array.update a i x h) = lim h"
  unfolding Array.update_def
  by (simp add: Let_def)


text ‹Simplification rules for the addresses of new allocated arrays and
  references›

lemma addr_of_ref_alloc[simp]:
  "addr_of_ref (fst (Ref.alloc x h)) = lim h"
  unfolding Ref.alloc_def
  by (simp add: Let_def)

lemma addr_of_array_alloc[simp]:
  "addr_of_array (fst (Array.alloc x h)) = lim h"
  unfolding Array.alloc_def
  by (simp add: Let_def)

end

Theory Syntax_Match

section ‹Syntactic Matching in the Simplifier›
theory Syntax_Match
imports Main
begin

subsection ‹Non-Matching›

text ‹
  We define the predicates syntax_nomatch› 
  and syntax_fo_nomatch›. The expression 
  syntax_nomatch pattern object› is simplified to true only if 
  the term pattern› syntactically matches the term object›. 
  Note that, semantically, syntax_nomatch pattern object› is always
  true. While syntax_nomatch› does higher-order matching, 
  syntax_fo_nomatch› does first-order matching.

  The intended application of these predicates are as guards for simplification
  rules, enforcing additional syntactic restrictions on the applicability of
  the simplification rule.
›
definition syntax_nomatch :: "'a  'b  bool"
  where syntax_nomatch_def: "syntax_nomatch pat obj  True"
definition syntax_fo_nomatch :: "'a  'b  bool" 
  where syntax_fo_nomatch_def: "syntax_fo_nomatch pat obj  True"

(* Prevent simplifier to simplify inside syntax_xx predicates *)
lemma [cong]: "syntax_fo_nomatch x y = syntax_fo_nomatch x y" by simp
lemma [cong]: "syntax_nomatch x y = syntax_nomatch x y" by simp

ML structure Syntax_Match = struct
  val nomatch_thm = @{thm syntax_nomatch_def};
  val fo_nomatch_thm = @{thm syntax_fo_nomatch_def};

  fun fo_nomatch_simproc ctxt credex = let
    (*val ctxt = Simplifier.the_context ss;*)
    val thy = Proof_Context.theory_of ctxt;

    val redex = Thm.term_of credex;
    val (_,[pat,obj]) = strip_comb redex;

    fun fo_matches po = (Pattern.first_order_match 
      thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
  in
    if fo_matches (pat,obj) then NONE else SOME fo_nomatch_thm
  end

  fun nomatch_simproc ctxt credex = let
    (*val ctxt = Simplifier.the_context ss;*)
    val thy = Proof_Context.theory_of ctxt;

    val redex = Thm.term_of credex;
    val (_,[pat,obj]) = strip_comb redex;
  in
    if Pattern.matches thy (pat,obj) then NONE else SOME nomatch_thm
  end
end
simproc_setup nomatch ("syntax_nomatch pat obj") 
  = ‹K Syntax_Match.nomatch_simproc
simproc_setup fo_nomatch ("syntax_fo_nomatch pat obj") 
  = ‹K Syntax_Match.fo_nomatch_simproc


subsection ‹Examples›
subsubsection ‹Ordering AC-structures›
text ‹
  Currently, the simplifier rules for ac-rewriting only work when
  associativity groups to the right. Here, we define rules that work for
  associativity grouping to the left. They are useful for operators where 
  syntax is parsed (and pretty-printed) left-associative.
›

locale ac_operator =
  fixes f
  assumes right_assoc: "f (f a b) c = f a (f b c)"
  assumes commute: "f a b = f b a"
begin
  lemmas left_assoc = right_assoc[symmetric]
  lemma left_commute: "f a (f b c) = f b (f a c)"
    apply (simp add: left_assoc)
    apply (simp add: commute)
    done

  lemmas right_ac = right_assoc left_commute commute

  lemma right_commute: "f (f a b) c = f (f a c) b"
    by (simp add: right_ac)

  lemma safe_commute: "syntax_fo_nomatch (f x y) a  f a b = f b a"
    by (simp add: right_ac)

  lemmas left_ac = left_assoc right_commute safe_commute
end

interpretation mult: ac_operator "(*) ::'a::ab_semigroup_mult  _  _"
  apply unfold_locales
  apply (simp_all add: ac_simps)
  done

interpretation add: ac_operator "(+) ::'a::ab_semigroup_add  _  _"
  apply unfold_locales
  apply (simp_all add: ac_simps)
  done

text ‹Attention: conj_assoc› is in standard simpset, it has to be 
  removed when using conj.left_ac› !›
interpretation conj: ac_operator "(∧)"
  by unfold_locales auto
interpretation disj: ac_operator "(∨)"
  by unfold_locales auto

end

Theory Run

section ‹Exception-Aware Relational Framework›
theory Run
imports "HOL-Imperative_HOL.Imperative_HOL"
begin

  text ‹
    With Imperative HOL comes a relational framework. 
    However, this can only be used if exception freeness is already assumed.
    This results in some proof duplication, because exception freeness and 
    correctness need to be shown separately.

    In this theory, we develop a relational framework that is aware of 
    exceptions, and makes it possible to show correctness and exception 
    freeness in one run.
›

  
  text ‹
    There are two types of states:
    \begin{enumerate}
      \item A normal (Some) state contains the current heap.
      \item An exception state is None
    \end{enumerate}
    The two states exactly correspond to the option monad in Imperative HOL.
›

type_synonym state = "Heap.heap option"

primrec is_exn where
  "is_exn (Some _) = False" |
  "is_exn None = True"

primrec the_state where
  "the_state (Some h) = h" 

― ‹The exception-aware, relational semantics›

inductive run :: "'a Heap  state  state  'a  bool" where
  push_exn: "is_exn σ  run c σ σ r " |
  new_exn:  "¬ is_exn σ; execute c (the_state σ) = None 
     run c σ None r" |
  regular:  "¬ is_exn σ; execute c (the_state σ) = Some (r, h') 
     run c σ (Some h') r"


subsubsection "Link with effect› and success›"

lemma run_effectE: 
  assumes "run c σ σ' r"
  assumes "¬is_exn σ'"
  obtains h h' where
    "σ=Some h" "σ' = Some h'"
    "effect c h h' r"
  using assms
  unfolding effect_def
  apply (cases σ)
  by (auto simp add: run.simps)


lemma run_effectI: 
  assumes  "run c (Some h) (Some h') r"
  shows  "effect c h h' r"
  using run_effectE[OF assms] by auto

lemma effect_run:
  assumes "effect c h h' r"
  shows "run c (Some h) (Some h') r"
  using assms
  unfolding effect_def
  by (auto intro: run.intros) 

lemma success_run:
  assumes "success f h"
  obtains h' r where "run f (Some h) (Some h') r" 
proof -
  from assms obtain r h' 
    where "Heap_Monad.execute f h = Some (r, h')" 
    unfolding success_def by auto
  then show thesis by (rule that[OF regular[of "Some h", simplified]])
qed


text ‹run always yields a result›
lemma run_complete:
  obtains σ' r where "run c σ σ' r"
  apply (cases "is_exn σ")
  apply (auto intro: run.intros)
  apply (cases "execute c (the_state σ)")  
  by (auto intro: run.intros)

lemma run_detE:
  assumes "run c σ σ' r" "run c σ τ s"
          "¬is_exn σ"
  obtains "is_exn σ'" "σ' = τ" | "¬ is_exn σ'" "σ' = τ" "r = s"
  using assms
  by (auto simp add: run.simps)
   
lemma run_detI:
  assumes "run c (Some h) (Some h') r" "run c (Some h) σ s"
  shows "σ = Some h'  r = s"
  using assms
  by (auto simp add: run.simps)

lemma run_exn: 
  assumes "run f σ σ' r"
          "is_exn σ"
  obtains "σ'=σ"
  using assms
  apply (cases σ)
  apply (auto elim!: run.cases intro: that)
  done

subsubsection ‹Elimination Rules for Basic Combinators›

named_theorems run_elims "elemination rules for run"

lemma runE[run_elims]:
  assumes "run (f  g) σ σ'' r"
  obtains σ' r' where 
    "run f σ σ' r'"
    "run (g r') σ' σ'' r"
using assms
apply (cases "is_exn σ")
apply (simp add: run.simps)
apply (cases "execute f (the_state σ)")
apply (simp add: run.simps bind_def)
by (auto simp add: bind_def run.simps)

lemma runE'[run_elims]:
  assumes "run (f  g) σ σ'' res"
  obtains σt rt where 
    "run f σ σt rt"
    "run g σt σ'' res"
  using assms
  by (rule_tac runE)


lemma run_return[run_elims]:
  assumes "run (return x) σ σ' r"
  obtains "r = x" "σ' = σ" "¬ is_exn σ" | "σ = None"
  using assms  apply (cases σ) apply (simp add: run.simps)
  by (auto simp add: run.simps execute_simps)


lemma run_raise_iff: "run (raise s) σ σ' r  (σ'=None)"
  apply (cases σ)
  by (auto simp add: run.simps execute_simps)

lemma run_raise[run_elims]:
  assumes "run (raise s) σ σ' r"
  obtains "σ' = None"
  using assms by (simp add: run_raise_iff)

lemma run_raiseI:
  "run (raise s) σ None r" by (simp add: run_raise_iff)

lemma run_if[run_elims]:
  assumes "run (if c then t else e) h h' r"
  obtains "c" "run t h h' r"
        | "¬c" "run e h h' r"
  using assms
  by (auto split: if_split_asm)
  
lemma run_case_option[run_elims]:
  assumes "run (case x of None  n | Some y  s y) σ σ' r"
          "¬is_exn σ"
  obtains "x = None" "run n σ σ' r"
        | y where "x = Some y" "run (s y) σ σ' r" 
  using assms
  by (cases x) simp_all

lemma run_heap[run_elims]:
  assumes "run (Heap_Monad.heap f) σ σ' res"
          "¬is_exn σ"
  obtains "σ' = Some (snd (f (the_state σ)))" 
  and "res = (fst (f (the_state σ)))"
  using assms
  apply (cases σ)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  
  apply (simp only: execute_simps)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (f a)" "res = fst (f a)" by simp_all
    from prems(1)[OF this] show ?thesis .
  qed
  done

subsection ‹Array Commands›

lemma run_length[run_elims]:
  assumes "run (Array.len a) σ σ' r"
          "¬is_exn σ"
  obtains "¬is_exn σ" "σ' = σ" "r = Array.length (the_state σ) a"
  using assms
  apply (cases σ)
  by (auto simp add: run.simps execute_simps)


lemma run_new_array[run_elims]:
  assumes "run (Array.new n x) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = Some (snd (Array.alloc (replicate n x) (the_state σ)))"
  and "r = fst (Array.alloc (replicate n x) (the_state σ))"
  and "Array.get (the_state σ') r = replicate n x"
  using assms 
  apply (cases σ)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (Array.alloc (replicate n x) a)" 
      "r = fst (Array.alloc (replicate n x) a)" by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_make[run_elims]:
  assumes "run (Array.make n f) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = Some (snd (Array.alloc (map f [0 ..< n]) (the_state σ)))"
          "r = fst (Array.alloc (map f [0 ..< n]) (the_state σ))"
          "Array.get (the_state σ') r = (map f [0 ..< n])"
  using assms
  apply (cases σ)
  subgoal by simp
  subgoal by (simp add: run.simps execute_simps Array.get_alloc; fastforce)
  done    

lemma run_upd[run_elims]:
  assumes "run (Array.upd i x a) σ σ' res"
          "¬is_exn σ"
  obtains "¬ i < Array.length (the_state σ) a" 
          "σ' = None" 
  |
          "i < Array.length (the_state σ) a" 
          "σ' = Some (Array.update a i x (the_state σ))" 
          "res = a"
  using assms
  apply (cases σ)
  apply simp
  apply (cases "i < Array.length (the_state σ) a")
  apply (auto simp add: run.simps)
  apply (simp_all only: execute_simps)
  prefer 3
  apply auto[2]
  apply hypsubst_thin
  subgoal premises prems for aa h'
  proof -
    from prems(3) have "h' = Array.update a i x aa" "res = a" by auto
    then show ?thesis by (rule prems(1))
  qed
  done


lemma run_nth[run_elims]:
  assumes "run (Array.nth a i) σ σ' r"
          "¬is_exn σ"
  obtains "¬is_exn σ" 
    "i < Array.length (the_state σ) a" 
    "r = (Array.get (the_state σ) a) ! i" 
    "σ' = σ" 
  | 
    "¬ i < Array.length (the_state σ) a" 
    "σ' = None"
  using assms
  apply (cases σ)
  apply simp
  apply (cases "i < Array.length (the_state σ) a")
  apply (auto simp add: run.simps)
  apply (simp_all only: execute_simps)
  prefer 3
  apply auto[2]
  apply hypsubst_thin
  subgoal premises prems for aa h'
  proof -
    from prems(3) have "r = Array.get aa a ! i" "h' = aa" by auto
    then show ?thesis by (rule prems(1))
  qed
  done


lemma run_of_list[run_elims]:
  assumes "run (Array.of_list xs) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = Some (snd (Array.alloc xs (the_state σ)))"
          "r = fst (Array.alloc xs (the_state σ))"
          "Array.get (the_state σ') r = xs"
  using assms
  apply (cases σ)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply (simp add: Array.get_alloc)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have "h' = snd (Array.alloc xs a)" 
      "r = fst (Array.alloc xs a)" by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma run_freeze[run_elims]:
  assumes "run (Array.freeze a) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = σ"
          "r = Array.get (the_state σ) a"
  using assms
  apply (cases σ)
  by (auto simp add: run.simps execute_simps)



subsection ‹Reference Commands›

lemma run_new_ref[run_elims]:
  assumes "run (ref x) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = Some (snd (Ref.alloc x (the_state σ)))"
          "r = fst (Ref.alloc x (the_state σ))"
          "Ref.get (the_state σ') r = x"
  using assms
  apply (cases σ)
  apply simp
  apply (auto simp add: run.simps)
  apply (simp add: execute_simps)
  apply hypsubst_thin
  subgoal premises prems for a h'
  proof -
    from prems(2) have 
      "h' = snd (Ref.alloc x a)" 
      "r = fst (Ref.alloc x a)"
      by (auto simp add: execute_simps)
    then show ?thesis by (rule prems(1))
  qed
  done

lemma "fst (Ref.alloc x h) = Ref (lim h)"
  unfolding alloc_def
  by (simp add: Let_def)

  
lemma run_update[run_elims]:
  assumes "run (p := x) σ σ' r"
          "¬is_exn σ"
  obtains "σ' = Some (Ref.set p x (the_state σ))" "r = ()"
  using assms
  unfolding Ref.update_def
  by (auto elim: run_heap)

lemma run_lookup[run_elims]:
  assumes "run (!p) σ σ' r"
          "¬ is_exn σ"
  obtains "¬is_exn σ" "σ' = σ" "r = Ref.get (the_state σ) p"
  using assms
  apply (cases σ)
  by (auto simp add: run.simps execute_simps)
  
end

Theory 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)  (aas. 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 (asas') 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 "hP  Rep_assn P h"


lemma models_in_range: "hP  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=as1as2  as1as2={} 
         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: "hA*B 
   (hr as1 as2. h=(hr,as1as2)  as1as2={}  (hr,as1)A  (hr,as2)B)"
  unfolding times_assn_def
  apply (cases h)
  by (auto simp: Abs_assn_inverse)

lemma mod_starD: "hA*B  h1 h2. h1A  h2B"
  by (auto simp: mod_star_conv)

lemma star_assnI:
  assumes "(h,as)P" and "(h,as')Q" and "asas'={}"
  shows "(h,asas')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="as1as1a" 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="as2aas2" 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'. asas'={}  relH as h h'  in_range (h',as)
     P (h',as')
     Q (h',asas'))"

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',asas')  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. hP  hQ)"
  definition inf_assn where "inf P Q  Abs_assn (λh. hP  hQ)"
  definition uminus_assn where 
    "-P  Abs_assn (λh. in_range h  ¬hP)"

  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  ab"

  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::"assnassnassn" (infixr "A" 61) 
  where "sup_assn  sup"
abbreviation inf_assn::"assnassnassn" (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. hP 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. hP 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 = (ab)"
  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 = (ab)"
  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 = (ab)"
  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 "rrx  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 "raa  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]: "htrue  in_range h"
  unfolding top_assn_def by (simp add: Abs_assn_inverse)
lemma mod_false[simp]: "¬ hfalse"
  unfolding bot_assn_def by (simp add: Abs_assn_inverse)

lemma mod_emp: "hemp  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]: "hb  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. hP x)"
  unfolding ex_assn_def by (auto simp: Abs_assn_inverse)
  
lemma mod_exI: "x. hP x  h(Ax. P x)"
  by (auto simp: mod_ex_dist)
lemma mod_exE: assumes "h(Ax. P x)" obtains x where "hP 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: "hPAQ  hP  hQ"
  unfolding inf_assn_def by (simp add: Abs_assn_inverse)

lemma mod_or_dist[simp]: "hPAQ  hP  hQ"
  unfolding sup_assn_def by (simp add: Abs_assn_inverse)

lemma mod_not_dist[simp]: "h(¬AP)  in_range h  ¬ hP"
  unfolding uminus_assn_def by (simp add: Abs_assn_inverse)

lemma mod_pure_star_dist[simp]: "hP*b  hP  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: "hP  hP*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 "hP*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 "hP*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,{})  prx  False"
  "(h,{})  qay  False"
  "(h,{})  P*Q  ((h,{})  P)  ((h,{})  Q)"
  "(h,{})  PAQ  ((h,{})  P)  ((h,{})  Q)"
  "(h,{})  PAQ  ((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. hP  hQ"

lemma entailsI: 
  assumes "h. hP  hQ"
  shows "P A Q" 
  using assms unfolding entails_def by auto

lemma entailsD: 
  assumes "P A Q"
  assumes "hP"
  shows "hQ" 
  using assms unfolding entails_def by blast

subsubsection ‹Properties›
lemma ent_fwd: 
  assumes "hP"
  assumes "P A Q"
  shows "hQ" 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 "AAB"
  assumes "BAA"
  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. ¬hP)"
  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. hP  b)  (P A Q))"
  unfolding entails_def
  by (auto simp add: mod_dist)

lemma ent_pure_post_iff_sng[simp]: 
  "(P A b)  ((h. hP  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 "asas'={}" 
    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 asas'={} have "(h',asas')Q*P" 
    by (metis star_assnI Int_commute Un_commute)
  with IMP show "(h',asas')  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: " AAC; BAC   AAB AC"
  unfolding entails_def by auto

lemma ent_conjI: " AAB; AAC   A A B A C"  
  unfolding entails_def by (auto simp: mod_and_dist)

lemma ent_conjE1: "AAC  AABAC"
  unfolding entails_def by (auto simp: mod_and_dist)
lemma ent_conjE2: "BAC  AABAC"
  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': "AAB  AABAC"
  by (auto simp: entails_def star_or_dist)

lemma ent_disjI2': "AAC  AABAC"
  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: "AAB*true  AtB" unfolding entailst_def .
lemma enttD: "AtB  AAB*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  PtQ"
  by (drule enttI) simp

lemma entt_def_true: "(PtQ)  (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: "PAQ  PtQ" 
  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': "AtB  AtBAC"
  by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjI2': "AtC  AtBAC"
  by (auto simp: entailst_def entails_def star_or_dist)

lemma entt_disjE: " AtM; BtM   AAB t M"
  using ent_disjE enttD enttI by blast  
    
lemma entt_disjD1: "AABtC  AtC"
  using entt_disjI1_direct entt_trans by blast

lemma entt_disjD2: "AABtC  BtC"
  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. prx)"
  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. pax)"
  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

Theory Hoare_Triple

section ‹Hoare-Triples›
theory Hoare_Triple
imports Run Assertions
begin

text ‹In this theory, we define Hoare-Triples, which are our basic tool
  for specifying properties of Imperative HOL programs.›

subsection ‹Definition›

text ‹Analyze the heap before and after executing a command, to add
  the allocated addresses to the covered address range.›
definition new_addrs :: "heap  addr set  heap  addr set" where
  "new_addrs h as h' = as  {a. lim h  a  a < lim h'}"

lemma new_addr_refl[simp]: "new_addrs h as h = as"
  unfolding new_addrs_def by auto

text ‹
  Apart from correctness of the program wrt. the pre- and post condition,
  a Hoare-triple also encodes some well-formedness conditions of the command:
  The command must not change addresses outside the address range of the 
  precondition, and it must not decrease the heap limit. 

  Note that we do not require that the command only reads from heap locations
  inside the precondition's address range, as this condition would be quite
  complicated to express with the heap model of Imperative/HOL, and is not 
  necessary in our formalization of partial heaps, that always contain the 
  information for all addresses.
›
definition hoare_triple 
  :: "assn  'a Heap  ('a  assn)  bool" ("<_>/ _/ <_>")
  where
  "<P> c <Q>  h as σ r. (h,as)P  run c (Some h) σ r 
   (let h'=the_state σ; as'=new_addrs h as h' in  
    ¬is_exn σ  (h',as')Q r  relH ({a . a<lim h  aas}) h h' 
     lim h  lim h')"

text ‹Sanity checking theorems for Hoare-Triples›  
lemma
  assumes "<P> c <Q>"
  assumes "(h,as)P"
  shows hoare_triple_success: "success c h" 
    and hoare_triple_effect: "h' r. effect c h h' r  (h',new_addrs h as h')Q r"
  using assms 
  unfolding hoare_triple_def success_def effect_def
  apply -
  apply (auto simp: Let_def run.simps) apply fastforce
  by (metis is_exn.simps(2) not_Some_eq2 the_state.simps)

    
lemma hoare_tripleD:
  fixes h h' as as' σ r
  assumes "<P> c <Q>"
  assumes "(h,as)P"
  assumes "run c (Some h) σ r"
  defines "h'the_state σ" and "as'new_addrs h as h'"
  shows "¬is_exn σ" 
  and "(h',as')Q r"
  and "relH ({a . a<lim h  aas}) h h'"
  and "lim h  lim h'"
  using assms 
  unfolding hoare_triple_def h'_def as'_def 
  by (auto simp: Let_def)

text ‹For garbage-collected languages, specifications usually allow for some
  arbitrary heap parts in the postcondition. The following abbreviation defines
  a handy shortcut notation for such specifications.›
abbreviation hoare_triple' 
  :: "assn  'r Heap  ('r  assn)  bool" ("<_> _ <_>t") 
  where "<P> c <Q>t  <P> c <λr. Q r * true>"

subsection ‹Rules›
text ‹
  In this section, we provide a set of rules to prove Hoare-Triples correct.
›
subsubsection ‹Basic Rules›

lemma hoare_triple_preI: 
  assumes "h. hP  <P> c <Q>"
  shows "<P> c <Q>"
  using assms
  unfolding hoare_triple_def
  by auto


lemma frame_rule: 
  assumes A: "<P> c <Q>"
  shows "<P*R> c <λx. Q x * R>"
  unfolding hoare_triple_def Let_def
  apply (intro allI impI)
  apply (elim conjE)
  apply (intro conjI)
proof -
  fix h as
  assume "(h,as)  P * R"
  then obtain as1 as2 where [simp]: "as=as1as2" and DJ: "as1as2={}"
    and M1: "(h,as1)P" and M2: "(h,as2)R"
    unfolding times_assn_def
    by (auto simp: Abs_assn_inverse)

  fix σ r
  assume RUN: "run c (Some h) σ r"
  from hoare_tripleD(1)[OF A M1 RUN] show "¬ is_exn σ" .
  from hoare_tripleD(4)[OF A M1 RUN] 
  show "lim h  lim (the_state σ)" .

  from hoare_tripleD(3)[OF A M1 RUN] have 
    RH1: "relH {a. a < lim h  a  as1} h (the_state σ)" .
  moreover have "{a. a < lim h  a  as}  {a. a < lim h  a  as1}"
    by auto
  ultimately show "relH {a. a < lim h  a  as} h (the_state σ)" 
    by (blast intro: relH_subset)
    
  from hoare_tripleD(2)[OF A M1 RUN] have 
    "(the_state σ, new_addrs h as1 (the_state σ))  Q r" .
  moreover have DJN: "new_addrs h as1 (the_state σ)  as2 = {}"
    using DJ models_in_range[OF M2]
    by (auto simp: in_range.simps new_addrs_def)
  moreover have "as2  {a. a < lim h  a  as1}" 
    using DJ models_in_range[OF M2]
    by (auto simp: in_range.simps)
  hence "relH as2 h (the_state σ)" using RH1
    by (blast intro: relH_subset)
  with M2 have "(the_state σ, as2)R"
    by (metis mem_Collect_eq Rep_assn  
      proper_iff relH_in_rangeI(2))
  moreover have "new_addrs h as (the_state σ) 
    = new_addrs h as1 (the_state σ)  as2"
    by (auto simp: new_addrs_def)
  ultimately show 
    "(the_state σ, new_addrs h as (the_state σ))  Q r * R"
    unfolding times_assn_def
    apply (simp add: Abs_assn_inverse)
    apply blast
    done
qed


lemma false_rule[simp, intro!]: "<false> c <Q>"
  unfolding hoare_triple_def by simp

  
lemma cons_rule:
  assumes CPRE: "P A P'"
  assumes CPOST: "x. Q x A Q' x"
  assumes R: "<P'> c <Q>"
  shows "<P> c <Q'>"
  unfolding hoare_triple_def Let_def
  using hoare_tripleD[OF R entailsD[OF CPRE]] entailsD[OF CPOST]
  by blast

lemmas cons_pre_rule = cons_rule[OF _ ent_refl]
lemmas cons_post_rule = cons_rule[OF ent_refl, rotated]

lemma cons_rulet: "PtP'; x. Q x t Q' x; <P'> c <Q>t   <P> c <Q'>t"
  unfolding entailst_def
  apply (rule cons_pre_rule)
  apply assumption
  apply (rule cons_post_rule)
  apply (erule frame_rule)
  by (simp add: enttD enttI)  

lemmas cons_pre_rulet = cons_rulet[OF _ entt_refl]
lemmas cons_post_rulet = cons_rulet[OF entt_refl, rotated]

  
  
lemma norm_pre_ex_rule:
  assumes A: "x. <P x> f <Q>"
  shows "<Ax. P x> f <Q>"
  unfolding hoare_triple_def Let_def
  apply (intro allI impI, elim conjE mod_exE)
  using hoare_tripleD[OF A]
  by blast

lemma norm_pre_pure_iff[simp]:
  "<P*b> f <Q>  (b  <P> f <Q>)"
  unfolding hoare_triple_def Let_def
  by auto

lemma norm_pre_pure_iff_sng[simp]:
  "<b> f <Q>  (b  <emp> f <Q>)"
  using norm_pre_pure_iff[where P=emp]
  by simp

lemma norm_pre_pure_rule1: 
  "b  <P> f <Q>  <P*b> f <Q>" by simp

lemma norm_pre_pure_rule2:
  " b  <emp> f <Q>   <b> f <Q>" by simp

lemmas norm_pre_pure_rule = norm_pre_pure_rule1 norm_pre_pure_rule2

lemma post_exI_rule: "<P> c <λr. Q r x>  <P> c <λr. Ax. Q r x>"
  by (blast intro: cons_post_rule ent_ex_postI ent_refl)


subsubsection ‹Rules for Atomic Commands›
lemma ref_rule:
  "<emp> ref x <λr. r r x>"
  unfolding one_assn_def sngr_assn_def hoare_triple_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (intro allI impI)
  apply (elim conjE run_elims)
  apply simp
  apply (auto 
    simp: new_addrs_def Ref.alloc_def Let_def
    Ref.set_def Ref.get_def relH_def in_range.simps)
  done

lemma lookup_rule:
  "<p r x> !p <λr. p r x * (r = x)>"
  unfolding hoare_triple_def sngr_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto elim: run_elims simp add: relH_refl in_range.simps new_addrs_def)
  done

lemma update_rule:
  "<p r y> p := x <λr. p r x>"
  unfolding hoare_triple_def sngr_assn_def
  apply (auto elim!: run_update 
    simp: Let_def Abs_assn_inverse new_addrs_def in_range.simps 
    intro!: relH_set_ref)
  done

lemma update_wp_rule:
  "<r r y * ((r r x) -* (Q ()))> r := x <Q>"
  apply (rule cons_post_rule)
  apply (rule frame_rule[OF update_rule[where p=r and x=x], 
    where R="((r r x) -* (Q ()))"])
  apply (rule ent_trans)
  apply (rule ent_mp)
  by simp

lemma new_rule:
  "<emp> Array.new n x <λr. r a replicate n x>"
  unfolding hoare_triple_def snga_assn_def one_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps
  )
  done

lemma make_rule: "<emp> Array.make n f <λr. r a (map f [0 ..< n])>"
  unfolding hoare_triple_def snga_assn_def one_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps
  )
  done
    
lemma of_list_rule: "<emp> Array.of_list xs <λr. r a xs>"
  unfolding hoare_triple_def snga_assn_def one_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps
  )
  done

lemma length_rule:
  "<a a xs> Array.len a <λr. a a xs * (r = length xs)>"
  unfolding hoare_triple_def snga_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps Array.length_def
  )
  done

text ‹Note that the Boolean expression is placed at meta level and not 
  inside the precondition. This makes frame inference simpler.›
lemma nth_rule:
  "i < length xs  <a a xs> Array.nth a i <λr. a a xs * (r = xs ! i)>"
  unfolding hoare_triple_def snga_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps Array.length_def
  )
  done

lemma upd_rule:
  "i < length xs  
  <a a xs> 
  Array.upd i x a 
  <λr. (a a (list_update xs i x)) * (r = a)>"
  unfolding hoare_triple_def snga_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps Array.length_def Array.update_def comp_def
  )
  done

lemma freeze_rule:
  "<a a xs> Array.freeze a <λr. a a xs * (r = xs)>"
  unfolding hoare_triple_def snga_assn_def
  apply (simp add: Let_def Abs_assn_inverse)
  apply (auto 
    elim!: run_elims
    simp: Let_def new_addrs_def Array.get_def Array.set_def Array.alloc_def
      relH_def in_range.simps Array.length_def Array.update_def
  )
  done
  
lemma return_wp_rule:
  "<Q x> return x <Q>"
  unfolding hoare_triple_def Let_def
  apply (auto elim!: run_elims)
  apply (rule relH_refl)
  apply (simp add: in_range.simps)
  done

lemma return_sp_rule:
  "<P> return x <λr. P * (r = x)>"
  unfolding hoare_triple_def Let_def
  apply (simp add: Abs_assn_inverse)
  apply (auto elim!: run_elims intro!: relH_refl intro: models_in_range)
  apply (simp add: in_range.simps)
  done

lemma raise_iff: 
  "<P> raise s <Q>  P = false"
  unfolding hoare_triple_def Let_def
  apply (rule iffI)
  apply (unfold bot_assn_def) []
  apply rule
  apply (auto simp add: run_raise_iff) []

  apply (auto simp add: run_raise_iff) []
  done

lemma raise_rule: "<false> raise s <Q>"
  by (simp add: raise_iff)

subsubsection ‹Rules for Composed Commands›
lemma bind_rule: 
  assumes T1: "<P> f <R>"
  assumes T2: "x. <R x> g x <Q>"
  shows "<P> bind f g <Q>"
  unfolding hoare_triple_def Let_def
  apply (intro allI impI)
  apply (elim conjE run_elims)
  apply (intro conjI)
proof -
  fix h as σ'' r'' σ' r'
  assume M: "(h,as)  P" 
    and R1: "run f (Some h) σ' r'" 
    and R2: "run (g r') σ' σ'' r''"

  from hoare_tripleD[OF T1 M R1] have NO_E: "¬ is_exn σ'" 
    and M': "(the_state σ', new_addrs h as (the_state σ'))  R r'"
    and RH': "relH {a. a < lim h  a  as} h (the_state σ')"
    and LIM: "lim h  lim (the_state σ')"
    by auto

  from NO_E have [simp]: "Some (the_state σ') = σ'" by (cases σ') auto

  from hoare_tripleD[OF T2 M', simplified, OF R2] have 
    NO_E'': "¬ is_exn σ''"
    and M'': "(the_state σ'',
      new_addrs (the_state σ') 
        (new_addrs h as (the_state σ')) (the_state σ'')) 
       Q r''"
    and RH'': 
    "relH 
      {a. a < lim (the_state σ') 
         a  new_addrs h as (the_state σ')
      }
      (the_state σ') (the_state σ'')"
    and LIM': "lim (the_state σ')  lim (the_state σ'')" by auto
  
  show "¬ is_exn σ''" by fact

  have  
    "new_addrs 
      (the_state σ') 
      (new_addrs h as (the_state σ')) 
      (the_state σ'') 
    = new_addrs h as (the_state σ'')" 
    using LIM LIM' 
    by (auto simp add: new_addrs_def)
  with M'' show 
    "(the_state σ'', new_addrs h as (the_state σ''))  Q r''"
    by simp

  note RH'
  also have "relH {a. a < lim h  a  as} (the_state σ') (the_state σ'')"
    apply (rule relH_subset[OF RH''])
    using LIM LIM'
    by (auto simp: new_addrs_def)
  finally show "relH {a. a < lim h  a  as} h (the_state σ'')" .

  note LIM
  also note LIM'
  finally show "lim h  lim (the_state σ'')" .
qed

lemma if_rule:
  assumes  "b  <P> f <Q>"
  assumes  "¬b  <P> g <Q>"
  shows "<P> if b then f else g <Q>"
  using assms by auto

lemma if_rule_split:
  assumes  B: "b  <P> f <Q1>"
  assumes  NB: "¬b  <P> g <Q2>"
  assumes M: "x. (Q1 x * b) A (Q2 x * (¬b)) A Q x"
  shows "<P> if b then f else g <Q>"
  apply (cases b)
  apply simp_all
  apply (rule cons_post_rule)
  apply (erule B)
  apply (rule ent_trans[OF _ ent_disjI1[OF M]])
  apply simp

  apply (rule cons_post_rule)
  apply (erule NB)
  apply (rule ent_trans[OF _ ent_disjI2[OF M]])
  apply simp
  done

lemma split_rule: 
  assumes P: "<P> c <R>"
  assumes Q: "<Q> c <R>"
  shows "<P A Q> c <R>"
  unfolding hoare_triple_def
  apply (intro allI impI)
  apply (elim conjE)
  apply simp
  apply (erule disjE)
  using hoare_tripleD[OF P] apply simp
  using hoare_tripleD[OF Q] apply simp
  done

lemmas decon_if_split = if_rule_split split_rule
  ― ‹Use with care: Complete splitting of if statements›

lemma case_prod_rule: 
  "(a b. x = (a, b)  <P> f a b <Q>)  <P> case x of (a, b)  f a b <Q>"
  by (auto split: prod.split)

lemma case_list_rule:
  " l=[]  <P> fn <Q>; x xs. l=x#xs  <P> fc x xs <Q>   
  <P> case_list fn fc l <Q>"
  by (auto split: list.split)

lemma case_option_rule:
  " v=None  <P> fn <Q>; x. v=Some x  <P> fs x <Q>  
   <P> case_option fn fs v <Q>"
  by (auto split: option.split)

lemma case_sum_rule:
  " x. v=Inl x  <P> fl x <Q>; 
     x. v=Inr x  <P> fr x <Q>  
   <P> case_sum fl fr v <Q>"
  by (auto split: sum.split)

lemma let_rule: "(x. x = t  <P> f x <Q>)  <P> Let t f <Q>"
  by (auto)

end

Theory Automation

section ‹Automation›
theory Automation
imports Hoare_Triple (*"../Lib/Refine_Util"*)
begin

text ‹
  In this theory, we provide a set of tactics and a simplifier setup for easy
  reasoning with our separation logic.
›

subsection ‹Normalization of Assertions›
text ‹
  In this section, we provide a set of lemmas and a simplifier
  setup to bring assertions to a normal form. We provide a simproc that
  detects pure parts of assertions and duplicate pointers. Moreover,
  we provide ac-rules for assertions. See Section~\ref{sec:auto:overview}
  for a short overview of the available proof methods.
›

lemmas assn_aci =   
  inf_aci[where 'a=assn] 
  sup_aci[where 'a=assn] 
  mult.left_ac[where 'a=assn] 

lemmas star_assoc = mult.assoc[where 'a=assn] 
lemmas assn_assoc = 
  mult.left_assoc inf_assoc[where 'a=assn] sup_assoc[where 'a=assn] 

lemma merge_true_star_ctx: "true * (true * P) = true * P"
  by (simp add: mult.left_ac)
  
lemmas star_aci = 
  mult.assoc[where 'a=assn] mult.commute[where 'a=assn] mult.left_commute[where 'a=assn]
  assn_one_left mult_1_right[where 'a=assn]
  merge_true_star merge_true_star_ctx

text ‹Move existential quantifiers to the front of assertions›
lemma ex_assn_move_out[simp]:
  "Q R. (Ax. Q x) * R = (Ax. (Q x * R))"
  "Q R. R * (Ax. Q x) = (Ax. (R * Q x))"

  "P Q. (Ax. Q x) A P = (Ax. (Q x A P)) "
  "P Q. Q A (Ax. P x) = (Ax. (Q A P x))"

  "P Q. (Ax. Q x) A P = (Ax. (Q x A P))"
  "P Q. Q A (Ax. P x) = (Ax. (Q A P x))"
  apply -
  apply (simp add: ex_distrib_star)
  apply (subst mult.commute)
  apply (subst (2) mult.commute)
  apply (simp add: ex_distrib_star)

  apply (simp add: ex_distrib_and)
  apply (subst inf_commute)
  apply (subst (2) inf_commute)
  apply (simp add: ex_distrib_and)

  apply (simp add: ex_distrib_or)
  apply (subst sup_commute)
  apply (subst (2) sup_commute)
  apply (simp add: ex_distrib_or)
  done

text ‹Extract pure assertions from and-clauses›
lemma and_extract_pure_left_iff[simp]: "b A Q = (empAQ)*b"
  by (cases b) auto

lemma and_extract_pure_left_ctx_iff[simp]: "P*b A Q = (PAQ)*b"
  by (cases b) auto

lemma and_extract_pure_right_iff[simp]: "P A b = (empAP)*b"
  by (cases b) (auto simp: assn_aci)

lemma and_extract_pure_right_ctx_iff[simp]: "P A Q*b = (PAQ)*b"
  by (cases b) auto

lemmas and_extract_pure_iff = 
  and_extract_pure_left_iff and_extract_pure_left_ctx_iff
  and_extract_pure_right_iff and_extract_pure_right_ctx_iff

lemmas norm_assertion_simps =
  (* Neutral elements *)
  mult_1[where 'a=assn] mult_1_right[where 'a=assn]
  inf_top_left[where 'a=assn] inf_top_right[where 'a=assn]
  sup_bot_left[where 'a=assn] sup_bot_right[where 'a=assn]

  (* Zero elements *)
  star_false_left star_false_right
  inf_bot_left[where 'a=assn] inf_bot_right[where 'a=assn]
  sup_top_left[where 'a=assn] sup_top_right[where 'a=assn]

  (* Associativity *)
  mult.left_assoc[where 'a=assn]
  inf_assoc[where 'a=assn]
  sup_assoc[where 'a=assn]

  (* Existential Quantifiers *)
  ex_assn_move_out ex_assn_const

  (* Extract pure assertions from conjunctions *)
  and_extract_pure_iff

  (* Merging *)
  merge_pure_star merge_pure_and merge_pure_or
  merge_true_star 
  inf_idem[where 'a=assn] sup_idem[where 'a=assn]

  (* Duplicated References *)
  sngr_same_false snga_same_false


subsubsection ‹Simplifier Setup Fine-Tuning›
text ‹Imperative HOL likes to simplify pointer inequations to this strange
  operator. We do some additional simplifier setup here›
lemma not_same_noteqr[simp]: "¬ a=!=a"
  by (metis Ref.unequal)
declare Ref.noteq_irrefl[dest!]

lemma not_same_noteqa[simp]: "¬ a=!!=a"
  by (metis Array.unequal)
declare Array.noteq_irrefl[dest!]

text ‹However, it is safest to disable this rewriting, as there is
  a working standard simplifier setup for (≠)›
declare Ref.unequal[simp del]
declare Array.unequal[simp del]


subsection ‹Normalization of Entailments›

text ‹Used by existential quantifier extraction tactic›
lemma enorm_exI': (* Incomplete, as chosen x may depend on heap! *)
  "(x. Z x  (P A Q x))  (x. Z x)  (P A (Ax. Q x))"
  by (metis ent_ex_postI)
  
text ‹Example of how to build an extraction lemma.›
thm enorm_exI'[OF enorm_exI'[OF imp_refl]]

lemmas ent_triv = ent_true ent_false

text ‹Dummy rule to detect Hoare triple goal›
lemma is_hoare_triple: "<P> c <Q>  <P> c <Q>" .
text ‹Dummy rule to detect entailment goal›
lemma is_entails: "PAQ  P AQ" .

subsection ‹Frame Matcher›
text ‹Given star-lists P,Q and a frame F, this method tries to match 
  all elements of Q with corresponding elements of P. The result is a 
  partial match, that contains matching pairs and the unmatched content.›

text ‹The frame-matcher internally uses syntactic lists separated by
  star, and delimited by the special symbol SLN›, which is defined
  to be emp›.›
definition [simp]: "SLN  emp"
lemma SLN_left: "SLN * P = P" by simp
lemma SLN_right: "P * SLN = P" by simp

lemmas SLN_normalize = SLN_right mult.left_assoc[where 'a=assn]
lemmas SLN_strip = SLN_right SLN_left mult.left_assoc[where 'a=assn]

text ‹A query to the frame matcher. Contains the assertions
  P and Q that shall be matched, as well as a frame F, that is not 
  touched.›

definition [simp]: "FI_QUERY P Q F  P A Q*F"

abbreviation "fi_m_fst M  foldr (*) (map fst M) emp"
abbreviation "fi_m_snd M  foldr (*) (map snd M) emp"
abbreviation "fi_m_match M  ((p,q)set M. p A q)"

text ‹A result of the frame matcher. Contains a list of matching pairs,
  as well as the unmatched parts of P and Q, and the frame F.
›
definition [simp]: "FI_RESULT M UP UQ F  
  fi_m_match M  (fi_m_fst M * UP A fi_m_snd M * UQ * F)"

text ‹Internal structure used by the frame matcher: 
  m contains the matched pairs; p,q the assertions that still needs to be 
  matched; up,uq the assertions that could not be matched; and f the frame.
  p and q are SLN-delimited syntactic lists. 
›

definition [simp]: "FI m p q up uq f  
  fi_m_match m  (fi_m_fst m * p * up A fi_m_snd m * q * uq * f)"

text ‹Initialize processing of query›
lemma FI_init: 
  assumes "FI [] (SLN*P) (SLN*Q) SLN SLN F"
  shows "FI_QUERY P Q F"
  using assms by simp

text ‹Construct result from internal representation›
lemma FI_finalize:
  assumes "FI_RESULT m (p*up) (q*uq) f"
  shows "FI m p q up uq f"
  using assms by (simp add: assn_aci)

text ‹Auxiliary lemma to show that all matching pairs together form
  an entailment. This is required for most applications.›
lemma fi_match_entails:
  assumes "fi_m_match m"
  shows "fi_m_fst m A fi_m_snd m"
  using assms apply (induct m)
  apply (simp_all split: prod.split_asm add: ent_star_mono)
  done

text ‹Internally, the frame matcher tries to match the first assertion
  of q with the first assertion of p. If no match is found, the first
  assertion of p is discarded. If no match for any assertion in p can be
  found, the first assertion of q is discarded.›

text ‹Match›
lemma FI_match:
  assumes "p A q"
  assumes "FI ((p,q)#m) (ps*up) (qs*uq) SLN SLN f"
  shows "FI m (ps*p) (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci)

text ‹No match›
lemma FI_p_nomatch:
  assumes "FI m ps (qs*q) (p*up) uq f"
  shows "FI m (ps*p) (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci)
  
text ‹Head of q could not be matched›
lemma FI_q_nomatch:
  assumes "FI m (SLN*up) qs SLN (q*uq) f"
  shows "FI m SLN (qs*q) up uq f"
  using assms unfolding FI_def
  by (simp add: assn_aci) 

subsection ‹Frame Inference›
lemma frame_inference_init:
  assumes "FI_QUERY P Q F"
  shows "P A Q * F"
  using assms by simp

lemma frame_inference_finalize:
  shows "FI_RESULT M F emp F"
  apply simp
  apply rule
  apply (drule fi_match_entails)
  apply (rule ent_star_mono[OF _ ent_refl])
  apply assumption
  done

subsection ‹Entailment Solver›
lemma entails_solve_init:
  "FI_QUERY P Q true  P A Q * true"
  "FI_QUERY P Q emp  P A Q"
  by (simp_all add: assn_aci)

lemma entails_solve_finalize:
  "FI_RESULT M P emp true"
  "FI_RESULT M emp emp emp"
  by (auto simp add: fi_match_entails intro: ent_star_mono)

lemmas solve_ent_preprocess_simps = 
  ent_pure_post_iff ent_pure_post_iff_sng ent_pure_pre_iff ent_pure_pre_iff_sng
  
subsection ‹Verification Condition Generator›

lemmas normalize_rules = norm_pre_ex_rule norm_pre_pure_rule

(* Originally we introduced backwards-reasoning here, via
  cons_pre_rule[OF _ return_wp_rule] (old name: complete_return_cons). 
  This only works, if the postcondition is not schematic! However, for 
  forward reasoning, one usually assumes a schematic postcondition!
  *)
text ‹May be useful in simple, manual proofs, where the postcondition
  is no schematic variable.›
lemmas return_cons_rule = cons_pre_rule[OF _ return_wp_rule]

text ‹Useful frame-rule variant for manual proof:›
lemma frame_rule_left:
  "<P> c <Q>  <R * P> c <λx. R * Q x>"
  using frame_rule by (simp add: assn_aci)

lemmas deconstruct_rules = 
  bind_rule if_rule false_rule return_sp_rule let_rule 
  case_prod_rule case_list_rule case_option_rule case_sum_rule

lemmas heap_rules = 
  ref_rule
  lookup_rule
  update_rule
  new_rule
  make_rule
  of_list_rule
  length_rule
  nth_rule
  upd_rule
  freeze_rule

lemma fi_rule:
  assumes CMD: "<P> c <Q>"
  assumes FRAME: "Ps A P * F"
  shows "<Ps> c <λx. Q x * F>"
  apply (rule cons_pre_rule[rotated])
  apply (rule frame_rule)
  apply (rule CMD)
  apply (rule FRAME)
  done


subsection ‹ML-setup›

named_theorems sep_dflt_simps "Seplogic: Default simplification rules for automated solvers"
named_theorems sep_eintros "Seplogic: Intro rules for entailment solver"
named_theorems sep_heap_rules "Seplogic: VCG heap rules"
named_theorems sep_decon_rules "Seplogic: VCG deconstruct rules"

ML infix 1 THEN_IGNORE_NEWGOALS

structure Seplogic_Auto =
struct

  (***********************************)
  (*             Tools               *)
  (***********************************)

  (* Repeat tac on subgoal. Determinize each step. 
     Stop if tac fails or subgoal is solved. *)
  fun REPEAT_DETERM' tac i st = let
    val n = Thm.nprems_of st 
  in
    REPEAT_DETERM (COND (has_fewer_prems n) no_tac (tac i)) st
  end


  (***********************************)
  (*             Debugging           *)
  (***********************************)
  fun tr_term t = Pretty.string_of (Syntax.pretty_term @{context} t);


  (***********************************)
  (*        Custom Tacticals         *)
  (***********************************)

  (* Apply tac1, and then tac2 with an offset such that anything left 
     over by tac1 is skipped.

     The typical usage of this tactic is, if a theorem is instantiated
     with another theorem that produces additional goals that should 
     be ignored first. Here, it is used in the vcg to ensure that 
     frame inference is done before additional premises (that may 
     depend on the frame) are discharged.
  *)
  fun (tac1 THEN_IGNORE_NEWGOALS tac2) i st = let
    val np = Thm.nprems_of st
  in
    (tac1 i THEN (fn st' => let val np' = Thm.nprems_of st' in
      if np'<np then tac2 i st'
      else tac2 (i+(np'-np)+1) st'
    end)) st
  end;


  (***********************************)
  (*     Assertion Normalization     *)
  (***********************************)
  (* Find two terms in a list whose key is equal *)
  fun find_similar (key_of:term -> term) (ts:term list) = let
    fun frec _ [] = NONE
    | frec tab (t::ts) = let val k=key_of t in
      if Termtab.defined tab k then
        SOME (the (Termtab.lookup tab k),t)
      else frec (Termtab.update (k,t) tab) ts
    end
  in
    frec Termtab.empty ts
  end;

  (* Perform DFS over term with binary operator opN, threading through
    a state. Atomic terms are transformed by tr. Supports omission of
    terms from the result structure by transforming them to NONE. *)
  fun dfs_opr opN (tr:'state -> term -> ('state*term option)) 
    d (t as ((op_t as Const (fN,_))$t1$t2)) =
    if fN = opN then let
        val (d1,t1') = dfs_opr opN tr d t1;
        val (d2,t2') = dfs_opr opN tr d1 t2;
      in
        case (t1',t2') of
          (NONE,NONE) => (d2,NONE)
        | (SOME t1',NONE) => (d2,SOME t1')
        | (NONE,SOME t2') => (d2,SOME t2')
        | (SOME t1',SOME t2') => (d2,SOME (op_t$t1'$t2'))
      end
    else tr d t
  | dfs_opr _ tr d t = tr d t;
    
  (* Replace single occurrence of (atomic) ot in t by nt. 
    Returns new term or NONE if nothing was removed. *)
  fun dfs_replace_atomic opN ot nt t = let
    fun tr d t = if not d andalso t=ot then (true,SOME nt) else (d,SOME t);
    val (success,SOME t') = dfs_opr opN tr false t; 
  in
    if success then SOME t' else NONE
  end;

  fun assn_simproc_fun ctxt credex = let
    val ([redex],ctxt') = Variable.import_terms true [Thm.term_of credex] ctxt;
    (*val _ = tracing (tr_term redex);*)
    val export = singleton (Variable.export ctxt' ctxt)

    fun mk_star t1 t2 = @{term "(*)::assn  _  _"}$t2$t1;

    fun mk_star' NONE NONE = NONE
    | mk_star' (SOME t1) NONE  = SOME t1
    | mk_star' NONE (SOME t2) = SOME t2
    | mk_star' (SOME t1) (SOME t2) = SOME (mk_star t1 t2);

    fun ptrs_key (_$k$_) = k;

    fun remove_term pt t = case
      dfs_replace_atomic @{const_name "Groups.times_class.times"} pt 
        @{term emp} t 
    of
      SOME t' => t';  

    fun normalize t = let

      fun ep_tr (has_true,ps,ptrs) t = case t of 
        Const (@{const_name "Assertions.pure_assn"},_)$_ 
        => ((has_true,t::ps,ptrs),NONE)
      | Const (@{const_name "Assertions.sngr_assn"},_)$_$_ 
        => ((has_true,ps,t::ptrs),SOME t)
      | Const (@{const_name "Assertions.snga_assn"},_)$_$_
        => ((has_true,ps,t::ptrs),SOME t)
      | Const (@{const_name "Orderings.top_class.top"},_)
        => ((true,ps,ptrs),NONE)
      | (inf_op as Const (@{const_name "Lattices.inf_class.inf"},_))$t1$t2
        => ((has_true,ps,ptrs),SOME (inf_op$normalize t1$normalize t2))
      | _ => ((has_true,ps,ptrs),SOME t);

      fun normalizer t = case dfs_opr @{const_name "Groups.times_class.times"}
        ep_tr (false,[],[]) t 
      of 
        ((has_true,ps,ptrs),rt) => ((has_true,rev ps,ptrs),rt);

      fun normalize_core t = let 
        val ((has_true,pures,ptrs),rt) = normalizer t;
        val similar = find_similar ptrs_key ptrs;
        val true_t = if has_true then SOME @{term "Assertions.top_assn"} 
          else NONE;
        val pures' = case pures of 
            [] => NONE
          | p::ps => SOME (fold mk_star ps p);
      in
        case similar of NONE => the (mk_star' pures' (mk_star' true_t rt))
        | SOME (t1,t2) => let
            val t_stripped = remove_term t1 (remove_term t2 t);
          in mk_star t_stripped (mk_star t1 t2) end
      end;

      fun skip_ex ((exq as Const (@{const_name "ex_assn"},_))$(Abs (n,ty,t))) =
        exq$Abs (n,ty,skip_ex t)
      | skip_ex t = normalize_core t;

      val (bs,t') = strip_abs t;
      val ty = fastype_of1 (map #2 bs,t');
    in
      if ty = @{typ assn} then
        Logic.rlist_abs (bs,skip_ex t')
      else t
    end;

    (*val _ = tracing (tr_term redex);*)
    val (f,terms) = strip_comb redex;
    val nterms = map (fn t => let
        (*val _ = tracing (tr_term t); *)
        val t'=normalize t; 
        (*val _ = tracing (tr_term t');*)
      in t' end) terms;
    val new_form = list_comb (f,nterms);

    val res_ss = (put_simpset HOL_basic_ss ctxt addsimps @{thms star_aci});
    val result = Option.map (export o mk_meta_eq) (Arith_Data.prove_conv_nohyps
      [simp_tac res_ss 1] ctxt' (redex,new_form)
    );

  in 
    result
  end handle exc =>
    if Exn.is_interrupt exc then Exn.reraise exc
    else
      (tracing ("assn_simproc failed with exception\n:" ^ Runtime.exn_message exc);
        NONE) (* Fail silently *);
  
  val assn_simproc =
    Simplifier.make_simproc @{context} "assn_simproc"
     {lhss =
      [@{term "h  P"},
       @{term "P A Q"},
       @{term "P t Q"},
       @{term "Hoare_Triple.hoare_triple P c Q"},
       @{term "(P::assn) = Q"}],
      proc = K assn_simproc_fun};



  (***********************************)
  (*     Default Simplifications     *)
  (***********************************)

  (* Default simplification. MUST contain assertion normalization!
    Tactic must not fail! *)
  fun dflt_tac ctxt = asm_full_simp_tac
    (put_simpset HOL_ss ctxt
      addsimprocs [assn_simproc] 
      addsimps @{thms norm_assertion_simps}
      addsimps (Named_Theorems.get ctxt @{named_theorems sep_dflt_simps})
      |> fold Splitter.del_split @{thms if_split}
    );

  (***********************************)
  (*         Frame Matcher           *)
  (***********************************)

  (* Do frame matching
    imp_solve_tac - tactic used to discharge first assumption of match-rule
      cf. lemma FI_match.
  *)
  fun match_frame_tac imp_solve_tac ctxt = let
    (* Normalize star-lists *)
    val norm_tac = simp_tac (
      put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_normalize});

    (* Strip star-lists *)
    val strip_tac = 
      simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_strip}) THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms SLN_def});

    (* Do a match step *)
    val match_tac = resolve_tac ctxt @{thms FI_match} (* Separate p,q*)
      THEN' SOLVED' imp_solve_tac (* Solve implication *)
      THEN' norm_tac;

    (* Do a no-match step *)
    val nomatch_tac = resolve_tac ctxt @{thms FI_p_nomatch} ORELSE' 
      (resolve_tac ctxt @{thms FI_q_nomatch} THEN' norm_tac);
  in
    resolve_tac ctxt @{thms FI_init} THEN' norm_tac 
    THEN' REPEAT_DETERM' (FIRST' [
      CHANGED o dflt_tac ctxt,
      (match_tac ORELSE' nomatch_tac)])
    THEN' resolve_tac ctxt @{thms FI_finalize} THEN' strip_tac
  end;


  (***********************************)
  (*         Frame Inference         *)
  (***********************************)

  fun frame_inference_tac ctxt =
    resolve_tac ctxt @{thms frame_inference_init} 
    THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
    THEN' resolve_tac ctxt @{thms frame_inference_finalize};


  (***********************************)
  (*       Entailment Solver         *)
  (***********************************)

  (* Extract existential quantifiers from entailment goal *)
  fun extract_ex_tac ctxt i st = let
    fun count_ex (Const (@{const_name Assertions.entails},_)$_$c) = 
      count_ex c RS @{thm HOL.mp}
    | count_ex (Const (@{const_name Assertions.ex_assn},_)$Abs (_,_,t))
      = count_ex t RS @{thm enorm_exI'}
    | count_ex _ = @{thm imp_refl};

    val concl = Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop;
    val thm = count_ex concl;
  in
    (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms ent_ex_preI}) THEN'
     resolve_tac ctxt [thm]) i st
  end;


  (* Solve Entailment *)
  fun solve_entails_tac ctxt = let
    val preprocess_entails_tac = 
      dflt_tac ctxt 
      THEN' extract_ex_tac ctxt
      THEN' simp_tac 
        (put_simpset HOL_ss ctxt addsimps @{thms solve_ent_preprocess_simps});

    val match_entails_tac =
      resolve_tac ctxt @{thms entails_solve_init} 
      THEN' match_frame_tac (resolve_tac ctxt @{thms ent_refl}) ctxt
      THEN' resolve_tac ctxt @{thms entails_solve_finalize};
  in
    preprocess_entails_tac
    THEN' (TRY o
      REPEAT_ALL_NEW (match_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems sep_eintros}))))
    THEN_ALL_NEW (dflt_tac ctxt THEN' 
      TRY o (match_tac ctxt @{thms ent_triv} 
        ORELSE' resolve_tac ctxt @{thms ent_refl}
        ORELSE' match_entails_tac))
  end;


  (***********************************)
  (* Verification Condition Generator*)
  (***********************************)

  fun heap_rule_tac ctxt h_thms = 
    resolve_tac ctxt h_thms ORELSE' (
    resolve_tac ctxt @{thms fi_rule} THEN' (resolve_tac ctxt h_thms THEN_IGNORE_NEWGOALS
    frame_inference_tac ctxt));

  fun vcg_step_tac ctxt = let
    val h_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules});
    val d_thms = rev (Named_Theorems.get ctxt @{named_theorems sep_decon_rules});
    val heap_rule_tac = heap_rule_tac ctxt h_thms

    (* Apply consequence rule if postcondition is not a schematic var *)
    fun app_post_cons_tac i st = 
      case Logic.concl_of_goal (Thm.prop_of st) i |> HOLogic.dest_Trueprop of
        Const (@{const_name Hoare_Triple.hoare_triple},_)$_$_$qt =>
          if is_Var (head_of qt) then no_tac st
          else resolve_tac ctxt @{thms cons_post_rule} i st
      | _ => no_tac st;

  in
    CSUBGOAL (snd #> (FIRST' [
      CHANGED o dflt_tac ctxt,
      REPEAT_ALL_NEW (resolve_tac ctxt @{thms normalize_rules}),
      CHANGED o (FIRST' [resolve_tac ctxt d_thms, heap_rule_tac]
        ORELSE' (app_post_cons_tac THEN' 
          FIRST' [resolve_tac ctxt d_thms, heap_rule_tac])) 
    ]))
  end;

  fun vcg_tac ctxt = REPEAT_DETERM' (vcg_step_tac ctxt)

  (***********************************)
  (*        Automatic Solver         *)
  (***********************************)

  fun sep_autosolve_tac do_pre do_post ctxt = let
    val pre_tacs = [
      CHANGED o clarsimp_tac ctxt,
      CHANGED o REPEAT_ALL_NEW (match_tac ctxt @{thms ballI allI impI conjI})
    ];
    val main_tacs = [
      match_tac ctxt @{thms is_hoare_triple} THEN' CHANGED o vcg_tac ctxt,
      match_tac ctxt @{thms is_entails} THEN' CHANGED o solve_entails_tac ctxt
    ];
    val post_tacs = [SELECT_GOAL (auto_tac ctxt)];
    val tacs = (if do_pre then pre_tacs else [])
      @ main_tacs 
      @ (if do_post then post_tacs else []);
  in
    REPEAT_DETERM' (CHANGED o FIRST' tacs)
  end;


  (***********************************)
  (*          Method Setup           *)
  (***********************************)

  val dflt_simps_modifiers = [
    Args.$$$ "dflt_simps" -- Scan.option Args.add -- Args.colon 
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_dflt_simps}) ),
    Args.$$$ "dflt_simps" -- Scan.option Args.del -- Args.colon 
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_dflt_simps}) )
  ];
  val heap_modifiers = [
    Args.$$$ "heap" -- Scan.option Args.add -- Args.colon 
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_heap_rules}) ),
    Args.$$$ "heap" -- Scan.option Args.del -- Args.colon 
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_heap_rules}) )
  ];
  val decon_modifiers = [
    Args.$$$ "decon" -- Scan.option Args.add -- Args.colon 
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_decon_rules}) ),
    Args.$$$ "decon" -- Scan.option Args.del -- Args.colon 
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_decon_rules}) )
  ];

  val eintros_modifiers = [
    Args.$$$ "eintros" -- Scan.option Args.add -- Args.colon 
      >> K (Method.modifier (Named_Theorems.add @{named_theorems sep_eintros}) ),
    Args.$$$ "eintros" -- Scan.option Args.del -- Args.colon 
      >> K (Method.modifier (Named_Theorems.del @{named_theorems sep_eintros}) )
  ];


  val solve_entails_modifiers = dflt_simps_modifiers @ eintros_modifiers;

  val vcg_modifiers = 
    heap_modifiers @ decon_modifiers @ dflt_simps_modifiers;

  val sep_auto_modifiers = 
    clasimp_modifiers @ vcg_modifiers @ eintros_modifiers;

end;

simproc_setup assn_simproc 
  ("hP" | "PAQ" | "PtQ" | "<P> c <R>" | "(P::assn) = Q") 
  = ‹K Seplogic_Auto.assn_simproc_fun

method_setup assn_simp =‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.dflt_tac ctxt
))) "Seplogic: Simplification of assertions"

method_setup frame_inference = ‹Scan.succeed (fn ctxt => (SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.frame_inference_tac ctxt
))) "Seplogic: Frame inference"

method_setup solve_entails = Method.sections Seplogic_Auto.solve_entails_modifiers >>
  (fn _ => fn ctxt => SIMPLE_METHOD' (
  CHANGED o Seplogic_Auto.solve_entails_tac ctxt
)) "Seplogic: Entailment Solver"

method_setup heap_rule = Attrib.thms >>
  (fn thms => fn ctxt => SIMPLE_METHOD' ( 
    let
      val thms = case thms of [] => rev (Named_Theorems.get ctxt @{named_theorems sep_heap_rules})
        | _ => thms
    in
      CHANGED o Seplogic_Auto.heap_rule_tac ctxt thms
    end
)) "Seplogic: Apply rule with frame inference"


method_setup vcg = ‹
  Scan.lift (Args.mode "ss") --
  Method.sections Seplogic_Auto.vcg_modifiers >>
  (fn (ss,_) => fn ctxt => SIMPLE_METHOD' (
  CHANGED o (
    if ss then Seplogic_Auto.vcg_step_tac ctxt 
    else Seplogic_Auto.vcg_tac ctxt
  )
)) "Seplogic: Verification Condition Generator"

method_setup sep_auto = 
  ‹Scan.lift (Args.mode "nopre" -- Args.mode "nopost" -- Args.mode "plain") 
      --| Method.sections Seplogic_Auto.sep_auto_modifiers >>
  (fn ((nopre,nopost),plain) => fn ctxt => SIMPLE_METHOD' (
    CHANGED o Seplogic_Auto.sep_autosolve_tac 
      ((not nopre) andalso (not plain)) 
      ((not nopost) andalso (not plain)) ctxt
  )) "Seplogic: Automatic solver"

lemmas [sep_dflt_simps] = split

declare deconstruct_rules[sep_decon_rules]
declare heap_rules[sep_heap_rules]

lemmas [sep_eintros] = impI conjI exI

subsection ‹Semi-Automatic Reasoning›
text ‹In this section, we provide some lemmas for semi-automatic reasoning›

text ‹Forward reasoning with frame. Use frame_inference›-method 
  to discharge second assumption.›
lemma ent_frame_fwd:
  assumes R: "P A R"
  assumes F: "Ps A P*F"
  assumes I: "R*F A Q"
  shows "Ps A Q"
  using assms
  by (metis ent_refl ent_star_mono ent_trans)

lemma mod_frame_fwd:
  assumes M: "hPs"
  assumes R: "PAR"
  assumes F: "Ps A P*F"
  shows "hR*F"
  using assms
  by (metis ent_star_mono entails_def)


text ‹Apply precision rule with frame inference.›
lemma prec_frame:
  assumes PREC: "precise P"
  assumes M1: "h(R1 A R2)"
  assumes F1: "R1 A P x p * F1"
  assumes F2: "R2 A P y p * F2"
  shows "x=y"
  using preciseD[OF PREC] M1 F1 F2
  by (metis entailsD mod_and_dist)

lemma prec_frame_expl:
  assumes PREC: "x y. (h(P x * F1) A (P y * F2))  x=y"
  assumes M1: "h(R1 A R2)"
  assumes F1: "R1 A P x * F1"
  assumes F2: "R2 A P y * F2"
  shows "x=y"
  using assms
  by (metis entailsD mod_and_dist)


text ‹Variant that is useful within induction proofs, where induction
  goes over x› or y›
lemma prec_frame':
  assumes PREC: "(h(P x * F1) A (P y * F2))  x=y"
  assumes M1: "h(R1 A R2)"
  assumes F1: "R1 A P x * F1"
  assumes F2: "R2 A P y * F2"
  shows "x=y"
  using assms
  by (metis entailsD mod_and_dist)


lemma ent_wand_frameI:
  assumes "(Q -* R) * F A S"
  assumes "P A F * X"
  assumes "Q*X A R"
  shows "P A S"
  using assms
  by (metis ent_frame_fwd ent_wandI mult.commute)

subsubsection ‹Manual Frame Inference›

lemma ent_true_drop: 
  "PAQ*true  P*RAQ*true"
  "PAQ  PAQ*true"
  apply (metis assn_times_comm ent_star_mono ent_true merge_true_star_ctx)
  apply (metis assn_one_left ent_star_mono ent_true star_aci(2))
  done

lemma fr_refl: "AAB  A*C AB*C"
  by (blast intro: ent_star_mono ent_refl)

lemma fr_rot: "(A*B A C)  (B*A A C)" 
  by (simp add: assn_aci)

lemma fr_rot_rhs: "(A A B*C)  (A A C*B)" 
  by (simp add: assn_aci)

lemma ent_star_mono_true: 
  assumes "A A A' * true"
  assumes "B A B' * true"
  shows "A*B*true A A'*B'*true"
  using ent_star_mono[OF assms] apply simp
  using ent_true_drop(1) by blast

lemma ent_refl_true: "A A A * true"
  by (simp add: ent_true_drop(2)) 
    
lemma entt_fr_refl: "FtF'  F*A t F'*A" by (rule entt_star_mono) auto
lemma entt_fr_drop: "FtF'  F*A t F'"
  using ent_true_drop(1) enttD enttI by blast 
    
    
method_setup fr_rot = let
    fun rot_tac ctxt = 
      resolve_tac ctxt @{thms fr_rot} THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt 
        addsimps @{thms star_assoc[symmetric]})

  in
    Scan.lift Parse.nat >> 
      (fn n => fn ctxt => SIMPLE_METHOD' (
        fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

  end

method_setup fr_rot_rhs = let
    fun rot_tac ctxt = 
      resolve_tac ctxt @{thms fr_rot_rhs} THEN'
      simp_tac (put_simpset HOL_basic_ss ctxt 
        addsimps @{thms star_assoc[symmetric]})

  in
    Scan.lift Parse.nat >> 
      (fn n => fn ctxt => SIMPLE_METHOD' (
        fn i => REPEAT_DETERM_N n (rot_tac ctxt i)))

  end



(*<*)
subsection ‹Test Cases›

lemma "x. A x * true * Q x A true * A x * Q x"
  apply simp
  done

lemma "A * (true * B) A true * A * B"
  apply (simp)
  done
  
lemma "htrue*P*true  hP*true"
  by simp

lemma "A * true * (b  c) * true * B A b * c * true *A * B"
  by simp

lemma "y c. Ax. P x * (R x * Q y) *  (b  c) A (Ax. b * (P x * (R x * Q y) * c))"
  apply simp
  done

lemma "A * B * (c * B * C * D * a * true * d) * (Ax. E x * F * b) * true A (Ax.  (c  a  d  b) *
          true * A * B * (true * B * C * D) * (E x * F))"
  apply simp
  done

lemma "<P> c <λr. Q r * true * (b r) * true * a> 
   <P> c <λr. Q r * true * (b r  a)>"
  apply simp
  done


lemma "(h((A*B*b*true*c*true) A ((p=q)*P*Q)))
   h  A * B * true A P * Q  b  c  p = q"
  apply simp
  done

lemma assumes "FI_RESULT [(B, B), (A, A)] C D F" 
  shows "FI_QUERY (A*B*C) (D*B*A) F"
  apply (tactic Seplogic_Auto.match_frame_tac 
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1)
  by (rule assms)

lemma 
  assumes "FI_RESULT [(B,B), (A,A)] C emp F"
  shows "FI_QUERY (A*B*C) (B*A) F"
  apply (tactic Seplogic_Auto.match_frame_tac 
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1)
  by (rule assms)

lemma 
  assumes "FI_RESULT [(B, B), (A, A)] emp emp F"
  shows "FI_QUERY (A*B) (B*A) F"
  apply (tactic Seplogic_Auto.match_frame_tac 
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1)
  by (rule assms)

lemma 
  assumes "FI_RESULT [(A, A)] emp emp F"
  shows "FI_QUERY (A) (A) F"
  apply (tactic Seplogic_Auto.match_frame_tac 
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1)
  by (rule assms)

lemma 
  assumes "FI_RESULT [(A, A)] (B * C * D) emp F"
  shows "FI_QUERY (B*C*D*A) (A) F"
  apply (tactic Seplogic_Auto.match_frame_tac 
    (resolve_tac @{context} @{thms ent_refl}) @{context} 1)
  by (rule assms)


schematic_goal 
  "P1 * P2 * P3 * P4 A P3 * ?R1"
  "P1 * (P2 * (P3 * P4)) A P1 * ?R2"
  "P4 * (P2 * (P1 * P3)) A P1 * ?R2'"
  "P1 * P2 * P3 * P4 A P4 * ?R3"
  "P1 * P2 A P1 * ?R4"
  "P1 * P2 A P2 * ?R5"
  "P1 A P1 * ?R6"
  "P1 * P2 A emp * ?R7"
  by frame_inference+


lemma "A; B; C; b 17  
  Q 1 5 3 A (Ax y z. Aa. Q x y z * (b a) * (y=5))"
  by solve_entails

thm nth_rule
lemma "<P * xa[1,2,3]> 
  do { vArray.nth x 1; return v } 
  <λr. P * xa[1,2,3] * (r=2)>"
  apply sep_auto
  done

(*>*)

subsection ‹Quick Overview of Proof Methods› 
  text_raw ‹\label{sec:auto:overview}›
text ‹
  In this section, we give a quick overview of the available proof methods 
  and options. The most versatile proof method that we provide is
  sep_auto›. It tries to solve the first subgoal, invoking appropriate
  proof methods as required. If it cannot solve the subgoal completely, it
  stops at the intermediate state that it could not handle any more. 

  sep_auto› can be configured by 
  section-arguments for the simplifier, the classical reasoner, and all
  section-arguments for the verification condition generator and 
  entailment solver. Moreover, it takes an optional mode argument (mode), where
  valid modes are:
  \begin{description}
    \item[(nopre)] No preprocessing of goal. The preprocessor tries to clarify
      and simplify the goal before the main method is invoked.
    \item[(nopost)] No postprocessing of goal. The postprocessor tries to 
      solve or simplify goals left over by verification condition generation or
      entailment solving.
    \item[(plain)] Neither pre- nor postprocessing. Just applies vcg and 
      entailment solver.  
  \end{description}

  \paragraph{Entailment Solver.} The entailment solver processes goals of the
  form P ⟹A Q›. It is invoked by the method solve_entails›.
  It first tries to pull out pure parts of
  P› and Q›. This may introduce quantifiers, conjunction,
  and implication into the goal, that are eliminated by resolving with rules
  declared as sep_eintros› (method argument: eintros[add/del]:).
  Moreover, it simplifies with rules declared as sep_dflt_simps› 
  (section argument: dflt_simps[add/del]:›).

  Now, P› and Q› should have the form X1*…*Xn.
  Then, the frame-matcher is used to match all items of P› with items
  of Q›, and thus solve the implication. Matching is currently done 
  syntactically, but can instantiate schematic variables.

  Note that, by default, existential introduction is declared as 
  sep_eintros›-rule. This introduces schematic variables, that can
  later be matched against. However, in some cases, the matching may instantiate
  the schematic variables in an undesired way. In this case, the argument 
  eintros del: exI› should be passed to the entailment solver, and
  the existential quantifier should be instantiated manually.

  \paragraph{Frame Inference}
  The method frame_inference› tries to solve a goal of the 
  form P⟹Q*?F›, by matching Q› against the parts of 
  P›, and instantiating ?F› accordingly. 
  Matching is done syntactically, possibly 
  instantiating schematic variables. P› and Q› should be 
  assertions separated by *›. Note that frame inference does no 
  simplification or other kinds of normalization.

  The method heap_rule› applies the specified heap rules, using
  frame inference if necessary. If no rules are specified, the default 
  heap rules are used.

  \paragraph{Verification Condition Generator}
  The verification condition generator processes goals of the form 
  <P>c<Q>›. It is invoked by the method vcg›.
  First, it tries to pull out pure parts and simplifies with
  the default simplification rules. Then, it tries to resolve the goal with
  deconstruct rules (attribute: sep_decon_rules›, 
  section argument: decon[add/del]:›), and if this does not succeed, 
  it tries
  to resolve the goal with heap rules (attribute: sep_heap_rules›, 
  section argument: heap[add/del]:›), using the frame rule and 
  frame inference.
  If resolving is not possible, it also tries to apply the consequence rule to
  make the postcondition a schematic variable.
›


(*<*)
subsection ‹Hiding of internal stuff›
hide_const (open) FI SLN
(*>*)

end

Theory Sep_Main

section ‹Separation Logic Framework Entrypoint›
theory Sep_Main
imports Automation
begin
  text ‹Import this theory to make available Imperative/HOL with 
    separation logic.›
end

Theory Imp_List_Spec

section ‹Interface for Lists›
theory Imp_List_Spec
imports "../Sep_Main"
begin
text ‹
  This file specifies an abstract interface for list data structures. It can
  be implemented by concrete list data structures, as demonstrated in the open
  and circular singly linked list examples.
›

locale imp_list =
  fixes is_list :: "'a list  'l  assn"
  assumes precise: "precise is_list"
    (*"∀l l'. h⊨(is_list l p * F1) ∧A (is_list l' p * F2) ⟶ l=l'"*)

locale imp_list_empty = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes empty :: "'l Heap"
  assumes empty_rule[sep_heap_rules]: "<emp> empty <is_list []>t"

locale imp_list_is_empty = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes is_empty :: "'l  bool Heap"
  assumes is_empty_rule[sep_heap_rules]: 
    "<is_list l p> is_empty p <λr. is_list l p * (r  l=[])>t"

locale imp_list_append = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes append :: "'a  'l  'l Heap"
  assumes append_rule[sep_heap_rules]: 
    "<is_list l p> append a p <is_list (l@[a])>t"

locale imp_list_prepend = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes prepend :: "'a  'l  'l Heap"
  assumes prepend_rule[sep_heap_rules]: 
    "<is_list l p> prepend a p <is_list (a#l)>t"
    
locale imp_list_head = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes head :: "'l  'a Heap"
  assumes head_rule[sep_heap_rules]: 
    "l[]  <is_list l p> head p <λr. is_list l p * (r=hd l)>t"

locale imp_list_pop = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes pop :: "'l  ('a×'l) Heap"
  assumes pop_rule[sep_heap_rules]: 
    "l[]  
      <is_list l p> 
      pop p 
      <λ(r,p'). is_list (tl l) p' * (r=hd l)>t"

locale imp_list_rotate = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes rotate :: "'l  'l Heap"
  assumes rotate_rule[sep_heap_rules]: 
    "<is_list l p> rotate p <is_list (rotate1 l)>t"

locale imp_list_reverse = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes reverse :: "'l  'l Heap"
  assumes reverse_rule[sep_heap_rules]: 
    "<is_list l p> reverse p <is_list (rev l)>t"

locale imp_list_iterate = imp_list +
  constrains is_list :: "'a list  'l  assn"
  fixes is_it :: "'a list  'l  'a list  'it  assn"
  fixes it_init :: "'l  ('it) Heap"
  fixes it_has_next :: "'it  bool Heap"
  fixes it_next :: "'it  ('a×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_list l p> it_init p <is_it l p l>t"
  assumes it_next_rule[sep_heap_rules]: "l'[]  
    <is_it l p l' it> 
      it_next it 
    <λ(a,it'). is_it l p (tl l') it' * (a=hd l')>"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it l p l' it> 
       it_has_next it 
     <λr. is_it l p l' it * (rl'[])>"
  assumes quit_iteration:
    "is_it l p l' it A is_list l p * true"

end

Theory List_Seg

section ‹Singly Linked List Segments›
theory List_Seg
imports "../Sep_Main"
begin

subsection ‹Nodes›
text ‹
  We define a node of a list to contain a data value and a next pointer.
  As Imperative HOL does not support null-pointers, we make the next-pointer
  an optional value, None› representing a null pointer.

  Unfortunately, Imperative HOL requires some boilerplate code to define 
  a datatype.
›
setup ‹Sign.add_const_constraint 
  (@{const_name Ref}, SOME @{typ "nat  'a::type ref"})

datatype 'a node = Node "'a" "'a node ref option"

setup ‹Sign.add_const_constraint 
  (@{const_name Ref}, SOME @{typ "nat  'a::heap ref"})

setup ‹Sign.add_const_constraint (@{const_name Node}, 
  SOME @{typ "'a::heap  'a node ref option  'a node"})

text ‹Selector Functions›
primrec val :: "'a::heap node  'a" where
  [sep_dflt_simps]: "val (Node x _) = x"

primrec "next" :: "'a::heap node  'a node ref option" where
  [sep_dflt_simps]: "next (Node _ r) = r"

text ‹Encoding to natural numbers, as required by Imperative/HOL›
fun
  node_encode :: "'a::heap node  nat"
where
  "node_encode (Node x r) = to_nat (x, r)"

instance node :: (heap) heap
  apply (rule heap_class.intro)
  apply (rule countable_classI [of "node_encode"])
  apply (case_tac x, simp_all, case_tac y, simp_all)
  ..

subsection ‹List Segment Assertion›
text ‹
  Intuitively, lseg l p s› describes a list starting at p› and
  ending with a pointer s›. The content of the list are l›.
  Note that the pointer s› may also occur earlier in the list, in which
  case it is handled as a usual next-pointer.
›
fun lseg 
  :: "'a::heap list  'a node ref option  'a node ref option  assn"
  where
  "lseg [] p s = (p=s)"
| "lseg (x#l) (Some p) s = (Aq. p r Node x q * lseg l q s)"
| "lseg (_#_) None _ = false"

lemma lseg_if_splitf1[simp, sep_dflt_simps]: 
  "lseg l None None = (l=[])"
  apply (cases l, simp_all)
  done

lemma lseg_if_splitf2[simp, sep_dflt_simps]: 
  "lseg (x#xs) p q 
    = (App n. pp r (Node x n) * lseg xs n q * (p=Some pp))"
  apply (cases p, simp_all)
  (* TODO: One-point simproc for assertions! *)
  apply (rule ent_iffI)
  apply solve_entails
  apply solve_entails
  done


subsection ‹Lemmas›

subsubsection ‹Concatenation›
lemma lseg_prepend: 
  "prNode x q * lseg l q s A lseg (x#l) (Some p) s"
  by sep_auto

lemma lseg_append: 
  "lseg l p (Some s) * srNode x q A lseg (l@[x]) p q"
proof (induction l arbitrary: p)
  case Nil thus ?case by sep_auto
next
  case (Cons y l)
  show ?case
    apply (cases p)
    apply simp
    apply (sep_auto)
    apply (rule ent_frame_fwd[OF Cons.IH])
    apply frame_inference
    apply solve_entails
    done
qed

lemma lseg_conc: "lseg l1 p q * lseg l2 q r A lseg (l1@l2) p r"
proof (induct l1 arbitrary: p)
  case Nil thus ?case by simp
next
  case (Cons x l1)
  show ?case
    apply simp
    apply sep_auto
    apply (rule ent_frame_fwd[OF Cons.hyps])
    apply frame_inference
    apply solve_entails
    done
qed

subsubsection ‹Splitting›
lemma lseg_split: 
  "lseg (l1@l2) p r A Aq. lseg l1 p q * lseg l2 q r"
proof (induct l1 arbitrary: p)
  case Nil thus ?case by sep_auto
next
  case (Cons x l1)

  have "lseg ((x # l1) @ l2) p r 
    A App n. pp r Node x n * lseg (l1 @ l2) n r *  (p = Some pp)"
    by simp
  also have " A 
    App n q. pp r Node x n 
      * lseg l1 n q 
      * lseg l2 q r 
      * (p = Some pp)"
    apply (intro ent_ex_preI)
    apply clarsimp
    apply (rule ent_frame_fwd[OF Cons.hyps])
    apply frame_inference
    apply sep_auto
    done
  also have " A Aq. lseg (x#l1) p q * lseg l2 q r"
    by sep_auto
  finally show ?case .
qed

subsubsection ‹Precision›
lemma lseg_prec1: 
  "l l'. (h
      (lseg l p (Some q) * q r x * F1) 
       A (lseg l' p (Some q) * q r x * F2)) 
     l=l'"
  apply (intro allI)
  subgoal for l l'
  proof (induct l arbitrary: p l' F1 F2)
    case Nil thus ?case
      apply simp_all
      apply (cases l')
      apply simp
      apply auto
      done
  next
    case (Cons y l)
    from Cons.prems show ?case
      apply (cases l')
      apply auto []
      apply (cases p)
      apply simp
      
      apply (clarsimp)

      apply (subgoal_tac "y=a  na=n", simp)

      using Cons.hyps apply (erule prec_frame')
      apply frame_inference
      apply frame_inference

      apply (drule_tac p=aa in prec_frame[OF sngr_prec])
      apply frame_inference
      apply frame_inference
      apply simp
      done
  qed
  done

lemma lseg_prec2: 
  "l l'. (h
      (lseg l p None * F1) A (lseg l' p None * F2)) 
     l=l'"
  apply (intro allI)
  subgoal for l l'
  proof (induct l arbitrary: p l' F1 F2)
    case Nil thus ?case
      apply simp_all
      apply (cases l')
      apply simp
      apply (cases p)
      apply auto
      done
  next
    case (Cons y l)
    from Cons.prems show ?case
      apply (cases p)
      apply simp
      apply (cases l')
      apply (auto) []
      
      apply (clarsimp)

      apply (subgoal_tac "y=aa  na=n", simp)

      using Cons.hyps apply (erule prec_frame')
      apply frame_inference
      apply frame_inference

      apply (drule_tac p=a in prec_frame[OF sngr_prec])
      apply frame_inference
      apply frame_inference
      apply simp
      done
  qed
  done

lemma lseg_prec3: 
  "q q'. h  (lseg l p q * F1) A (lseg l p q' * F2)  q=q'"
  apply (intro allI)
proof (induct l arbitrary: p F1 F2)
  case Nil thus ?case by auto
next
  case (Cons x l)
  show ?case
    apply auto

    apply (subgoal_tac "na=n")
    using Cons.hyps apply (erule prec_frame')
    apply frame_inference
    apply frame_inference

    apply (drule prec_frame[OF sngr_prec])
    apply frame_inference
    apply frame_inference
    apply simp
    done
qed

end

Theory Open_List

section ‹Open Singly Linked Lists›
theory Open_List
imports List_Seg Imp_List_Spec
begin

subsection ‹Definitions›
type_synonym 'a os_list = "'a node ref option"

abbreviation os_list :: "'a list  ('a::heap) os_list  assn" where
  "os_list l p  lseg l p None"

subsection ‹Precision›
lemma os_prec: 
  "precise os_list"
  by rule (simp add: lseg_prec2)

lemma os_imp_list_impl: "imp_list os_list"
  apply unfold_locales
  apply (rule os_prec)
  done
interpretation os: imp_list os_list by (rule os_imp_list_impl)

subsection ‹Operations›
subsubsection ‹Allocate Empty List›

definition os_empty :: "'a::heap os_list Heap" where
  "os_empty  return None"

lemma os_empty_rule: "<emp> os_empty <os_list []>"
  unfolding os_empty_def
  apply sep_auto
  done

lemma os_empty_impl: "imp_list_empty os_list os_empty"
  apply unfold_locales
  apply (sep_auto heap add: os_empty_rule)
  done
interpretation os: imp_list_empty os_list os_empty by (rule os_empty_impl)
  
subsubsection ‹Emptiness check›
text ‹A linked list is empty, iff it is the null pointer.›

definition os_is_empty :: "'a::heap os_list  bool Heap" where
  "os_is_empty b  return (b = None)"

lemma os_is_empty_rule: 
  "<os_list xs b> os_is_empty b <λr. os_list xs b * (r  xs = [])>"
  unfolding os_is_empty_def
  apply sep_auto
  done

lemma os_is_empty_impl: "imp_list_is_empty os_list os_is_empty"
  apply unfold_locales
  apply (sep_auto heap add: os_is_empty_rule)
  done
interpretation os: imp_list_is_empty os_list os_is_empty
  by (rule os_is_empty_impl)

subsubsection ‹Prepend›

text ‹To push an element to the front of a list we allocate a new node which
  stores the element and the old list as successor. The new list is the new 
  allocated reference.›

definition os_prepend :: "'a  'a::heap os_list  'a os_list Heap" where
  "os_prepend a n = do { p  ref (Node a n); return (Some p) }"

lemma os_prepend_rule:
  "<os_list xs n> os_prepend x n <os_list (x # xs)>"
  unfolding os_prepend_def
  apply sep_auto
  done

lemma os_prepend_impl: "imp_list_prepend os_list os_prepend"
  apply unfold_locales
  apply (sep_auto heap add: os_prepend_rule)
  done
interpretation os: imp_list_prepend os_list os_prepend 
  by (rule os_prepend_impl)

subsubsection‹Pop›
text ‹To pop the first element out of the list we look up the value and the
  reference of the node and return the pair of those.›

fun os_pop :: "'a::heap os_list  ('a × 'a os_list) Heap" where
  "os_pop None   = raise STR ''Empty Os_list''" |
  "os_pop (Some p) = do {m  !p; return (val m, next m)}"

declare os_pop.simps[simp del]

lemma os_pop_rule:
  "xs  []  <os_list xs r> 
  os_pop r 
  <λ(x,r'). os_list (tl xs) r' * (the r) r (Node x r') * (x = hd xs)>"

  apply (cases r, simp_all)
  apply (cases xs, simp_all)

  apply (sep_auto simp: os_pop.simps)
  done

lemma os_pop_impl: "imp_list_pop os_list os_pop"
  apply unfold_locales
  apply (sep_auto heap add: os_pop_rule)
  done
interpretation os: imp_list_pop os_list os_pop by (rule os_pop_impl)

subsubsection ‹Reverse›

text ‹The following reversal function is equivalent to the one from 
  Imperative HOL. And gives a more difficult example.›

partial_function (heap) os_reverse_aux 
  :: "'a::heap os_list  'a os_list  'a os_list Heap" 
  where [code]:
  "os_reverse_aux q p = (case p of 
    None  return q |
    Some r  do {
      v  !r;
      r := Node (val v) q;
      os_reverse_aux p (next v) })"

lemma [simp, sep_dflt_simps]:
  "os_reverse_aux q None = return q"
  "os_reverse_aux q (Some r) = do {
      v  !r;
      r := Node (val v) q;
      os_reverse_aux (Some r) (next v) }"
  apply (subst os_reverse_aux.simps)
  apply simp
  apply (subst os_reverse_aux.simps)
  apply simp
  done

definition "os_reverse p = os_reverse_aux None p"

lemma os_reverse_aux_rule: 
  "<os_list xs p * os_list ys q> 
    os_reverse_aux q p 
  <os_list ((rev xs) @ ys) >"
proof (induct xs arbitrary: p q ys)
  case Nil thus ?case
    apply sep_auto
    done
next
  case (Cons x xs)
  show ?case
    apply (cases p, simp_all)
    apply (sep_auto heap add: cons_pre_rule[OF _ Cons.hyps])
    done
qed

lemma os_reverse_rule: "<os_list xs p> os_reverse p <os_list (rev xs)>"
  unfolding os_reverse_def
  apply (auto simp: os_reverse_aux_rule[where ys="[]", simplified, rule_format])
  done

lemma os_reverse_impl: "imp_list_reverse os_list os_reverse"
  apply unfold_locales
  apply (sep_auto heap add: os_reverse_rule)
  done
interpretation os: imp_list_reverse os_list os_reverse
  by (rule os_reverse_impl)

subsubsection ‹Remove›
 
text ‹Remove all appearances of an element from a linked list.›

partial_function (heap) os_rem 
  :: "'a::heap  'a node ref option  'a node ref option Heap" 
  where [code]:
  "os_rem x b = (case b of 
     None  return None |
     Some p  do { 
       n  !p;
       q  os_rem x (next n);
       (if (val n = x) 
         then return q
         else do { 
           p := Node (val n) q; 
           return (Some p) }) })"

lemma [simp, sep_dflt_simps]: 
  "os_rem x None = return None"
  "os_rem x (Some p) = do { 
       n  !p;
       q  os_rem x (next n);
       (if (val n = x) 
         then return q
         else do { 
           p := Node (val n) q; 
           return (Some p) }) }"
  apply (subst os_rem.simps, simp)+
  done

lemma os_rem_rule[sep_heap_rules]: 
  "<os_list xs b> os_rem x b <λr. os_list (removeAll x xs) r * true>"
proof (induct xs arbitrary: b x) (* Have to generalize over x, as 
    sep_auto preprocessor introduces a new variable. Alternative: 
    No preprocessing. (See alternative proof below) *)
  case Nil show ?case
    apply sep_auto
    done
next
  case (Cons y xs) 
  show ?case by (sep_auto heap add: Cons.hyps)
qed

lemma os_rem_rule_alt_proof: 
  "<os_list xs b> os_rem x b <λr. os_list (removeAll x xs) r * true>"
proof (induct xs arbitrary: b) 
  case Nil show ?case
    apply sep_auto
    done
next
  case (Cons y xs)
  show ?case 
    by (sep_auto (nopre) heap add: Cons.hyps) (* Switching off preprocessor *)
qed

subsubsection ‹Iterator›

type_synonym 'a os_list_it = "'a os_list"
definition "os_is_it l p l2 it 
   Al1. (l=l1@l2) * lseg l1 p it * os_list l2 it"

definition os_it_init :: "'a os_list  ('a os_list_it) Heap" 
  where "os_it_init l = return l"

fun os_it_next where 
  "os_it_next (Some p) = do {
    n  !p;
    return (val n,next n)
  }"

definition os_it_has_next :: "'a os_list_it  bool Heap" where
  "os_it_has_next it  return (itNone)"

lemma os_iterate_impl: 
  "imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next"
  apply unfold_locales
  unfolding os_it_init_def os_is_it_def[abs_def] 
  apply sep_auto

  apply (case_tac it, simp)
  apply (case_tac l', simp)
  apply sep_auto
  apply (rule ent_frame_fwd[OF lseg_append])
    apply frame_inference
    apply simp

  unfolding os_it_has_next_def
  apply (sep_auto elim!: neq_NilE)

  apply solve_entails
  apply (rule ent_frame_fwd[OF lseg_conc])
    apply frame_inference
    apply solve_entails
  done
interpretation os: 
  imp_list_iterate os_list os_is_it os_it_init os_it_has_next os_it_next
  by (rule os_iterate_impl)

subsubsection ‹List-Sum›

partial_function (heap) os_sum' :: "int os_list_it  int  int Heap" 
  where [code]:
  "os_sum' it s = do {
    b  os_it_has_next it;
    if b then do {
      (x,it')  os_it_next it;
      os_sum' it' (s+x)
    } else return s
  }"

lemma os_sum'_rule[sep_heap_rules]: 
  "<os_is_it l p l' it> 
    os_sum' it s 
  <λr. os_list l p * (r = s + sum_list l')>t"
proof (induct l' arbitrary: it s)
  case Nil thus ?case
    apply (subst os_sum'.simps)
    apply (sep_auto intro: os.quit_iteration)
    done
next
  case (Cons x l')
  show ?case
    apply (subst os_sum'.simps)
    apply (sep_auto heap: Cons.hyps)
    done
qed

definition "os_sum p  do { 
  it  os_it_init p;
  os_sum' it 0}"

lemma os_sum_rule[sep_heap_rules]: 
  "<os_list l p> os_sum p <λr. os_list l p * (r=sum_list l)>t"
  unfolding os_sum_def
  by sep_auto

end

Theory Circ_List

section ‹Circular Singly Linked Lists›
theory Circ_List
imports List_Seg Imp_List_Spec
begin

text ‹
  Example of circular lists, with efficient append, prepend, pop, and rotate
  operations.
›

subsection ‹Datatype Definition›

type_synonym 'a cs_list = "'a node ref option"

text ‹A circular list is described by a list segment, with special
  cases for the empty list:›
fun cs_list :: "'a::heap list  'a node ref option  assn" where
  "cs_list [] None = emp"
| "cs_list (x#l) (Some p) = lseg (x#l) (Some p) (Some p)"
| "cs_list _ _ = false"

lemma [simp]: "cs_list l None = (l=[])"
  by (cases l) auto

lemma [simp]: 
  "cs_list l (Some p) 
  = (Ax ls. (l=x#ls) * lseg (x#ls) (Some p) (Some p))"
  apply (rule ent_iffI)
  apply (cases l) 
  apply simp
  apply sep_auto
  apply (cases l) 
  apply simp
  apply sep_auto
  done

subsection ‹Precision›
lemma cs_prec: 
  "precise cs_list"
  apply rule
  apply (case_tac p)
  apply clarsimp

  apply clarsimp
  apply (subgoal_tac "x=xa  n=na", simp)

  apply (erule prec_frame_expl[OF lseg_prec1])
  apply frame_inference
  apply frame_inference

  apply (drule prec_frame[OF sngr_prec])
  apply frame_inference
  apply frame_inference
  apply simp
  done

lemma cs_imp_list_impl: "imp_list cs_list"
  apply unfold_locales
  apply (rule cs_prec)
  done
interpretation cs: imp_list cs_list by (rule cs_imp_list_impl)

subsection ‹Operations›
subsubsection ‹Allocate Empty List›
definition cs_empty :: "'a::heap cs_list Heap" where
  "cs_empty  return None"

lemma cs_empty_rule: "<emp> cs_empty <cs_list []>"
  unfolding cs_empty_def
  by sep_auto

lemma cs_empty_impl: "imp_list_empty cs_list cs_empty" 
  by unfold_locales (sep_auto heap: cs_empty_rule)
interpretation cs: imp_list_empty cs_list cs_empty by (rule cs_empty_impl)

subsubsection ‹Prepend Element›
fun cs_prepend :: "'a  'a::heap cs_list  'a cs_list Heap" where
  "cs_prepend x None = do {
    p  ref (Node x None); 
    p:=Node x (Some p); 
    return (Some p)
  }"
| "cs_prepend x (Some p) = do {
    n  !p;
    q  ref (Node (val n) (next n));
    p := Node x (Some q);
    return (Some p)
  }"

declare cs_prepend.simps [simp del]

lemma cs_prepend_rule: 
  "<cs_list l p> cs_prepend x p <cs_list (x#l)>"
  apply (cases p)
  apply simp_all
  apply (sep_auto simp: cs_prepend.simps)

  apply (sep_auto simp: cs_prepend.simps)
  done

lemma cs_prepend_impl: "imp_list_prepend cs_list cs_prepend"
  by unfold_locales (sep_auto heap: cs_prepend_rule)
interpretation cs: imp_list_prepend cs_list cs_prepend 
  by (rule cs_prepend_impl)

subsubsection ‹Append Element›
fun cs_append :: "'a  'a::heap cs_list  'a cs_list Heap" where
  "cs_append x None = do { 
    p  ref (Node x None); 
    p:=Node x (Some p); 
    return (Some p) }"
| "cs_append x (Some p) = do {
    n  !p;
    q  ref (Node (val n) (next n));
    p := Node x (Some q);
    return (Some q)
  }"

declare cs_append.simps [simp del]

lemma cs_append_rule: 
  "<cs_list l p> cs_append x p <cs_list (l@[x])>"
  apply (cases p)
  apply simp_all
  apply (sep_auto simp: cs_append.simps)

  apply (sep_auto simp: cs_append.simps)
  apply (rule ent_frame_fwd)
  apply (rule_tac s=a in lseg_append) (* frame_inference does no backtracking
    on instantiating schematics, hence we have to give it some help here. *)
  apply frame_inference
  apply (sep_auto)
  done

lemma cs_append_impl: "imp_list_append cs_list cs_append"
  by unfold_locales (sep_auto heap: cs_append_rule)
interpretation cs: imp_list_append cs_list cs_append
  by (rule cs_append_impl)

subsubsection ‹Pop First Element›
fun cs_pop :: "'a::heap cs_list  ('a×'a cs_list) Heap" where
  "cs_pop None = raise STR ''Pop from empty list''"
| "cs_pop (Some p) = do {
    n1  !p;
    if next n1 = Some p then
      return (val n1,None) ― ‹Singleton list becomes empty list›
    else do {
      let p2 = the (next n1);
      n2  !p2;
      p := Node (val n2) (next n2);
      return (val n1,Some p)
    }
  }"

declare cs_pop.simps[simp del]

lemma cs_pop_rule: 
  "<cs_list (x#l) p> cs_pop p <λ(y,p'). cs_list l p' * true * (y=x)>"
  apply (cases p)
  apply (sep_auto simp: cs_pop.simps)

  apply (cases l)
  apply (sep_auto simp: cs_pop.simps dflt_simps: option.sel)

  apply (sep_auto 
    simp: cs_pop.simps 
    dflt_simps: option.sel 
    eintros del: exI)
  (* Some unfortunate quantifier fiddling :( *)
  apply (rule_tac x=aa in exI)
  apply (rule_tac x=list in exI)
  apply (rule_tac x=a in exI)
  apply clarsimp
  apply (rule exI)
  apply sep_auto
  done

lemma cs_pop_impl: "imp_list_pop cs_list cs_pop"
  apply unfold_locales 
  apply (sep_auto heap: cs_pop_rule elim!: neq_NilE)
  done
interpretation cs: imp_list_pop cs_list cs_pop by (rule cs_pop_impl)

subsubsection ‹Rotate›
fun cs_rotate :: "'a::heap cs_list  'a cs_list Heap" where
  "cs_rotate None = return None"
| "cs_rotate (Some p) = do {
    n  !p;
    return (next n)
  }"

declare cs_rotate.simps [simp del]

lemma cs_rotate_rule: 
  "<cs_list l p> cs_rotate p <cs_list (rotate1 l)>"
  apply (cases p)
  apply (sep_auto simp: cs_rotate.simps)

  apply (cases l)
  apply simp

  apply (case_tac list)
  apply simp
  apply (sep_auto simp: cs_rotate.simps)

  apply (sep_auto simp: cs_rotate.simps)
  apply (rule ent_frame_fwd)
  apply (rule_tac s="a" in lseg_append)
  apply frame_inference
  apply sep_auto
  done

lemma cs_rotate_impl: "imp_list_rotate cs_list cs_rotate"
  apply unfold_locales 
  apply (sep_auto heap: cs_rotate_rule)
  done
interpretation cs: imp_list_rotate cs_list cs_rotate by (rule cs_rotate_impl)

subsection ‹Test›
definition "test  do {
  l  cs_empty;
  l  cs_append ''a'' l;
  l  cs_append ''b'' l;
  l  cs_append ''c'' l;
  l  cs_prepend ''0'' l;
  l  cs_rotate l;
  (v1,l)cs_pop l;
  (v2,l)cs_pop l;
  (v3,l)cs_pop l;
  (v4,l)cs_pop l;
  return [v1,v2,v3,v4]
}"

definition "test_result  [''a'', ''b'', ''c'', ''0'']"

lemma "<emp> test <λr. (r=test_result) * true>"
  unfolding test_def test_result_def
  apply (sep_auto)
  done
  
export_code test checking SML_imp

ML_val val res = @{code test} ();
  if res = @{code test_result} then () else raise Match;

hide_const (open) test test_result

end

Theory Imp_Map_Spec

section ‹Interface for Maps›
theory Imp_Map_Spec
imports "../Sep_Main"
begin
text ‹
  This file specifies an abstract interface for map data structures. It can
  be implemented by concrete map data structures, as demonstrated in the 
  hash map example.
›

locale imp_map = 
  fixes is_map :: "('k  'v)  'm  assn"
  assumes precise: "precise is_map"

locale imp_map_empty = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes empty :: "'m Heap"
  assumes empty_rule[sep_heap_rules]: "<emp> empty <is_map Map.empty>t"

locale imp_map_is_empty = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes is_empty :: "'m  bool Heap"
  assumes is_empty_rule[sep_heap_rules]: 
    "<is_map m p> is_empty p <λr. is_map m p * (r  m=Map.empty)>t"

locale imp_map_lookup = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes lookup :: "'k  'm  ('v option) Heap"
  assumes lookup_rule[sep_heap_rules]: 
    "<is_map m p> lookup k p <λr. is_map m p * (r = m k)>t"

locale imp_map_update = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes update :: "'k  'v  'm  'm Heap"
  assumes update_rule[sep_heap_rules]: 
    "<is_map m p> update k v p <is_map (m(k  v))>t"
    
locale imp_map_delete = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes delete :: "'k  'm  'm Heap"
  assumes delete_rule[sep_heap_rules]: 
    "<is_map m p> delete k p <is_map (m |` (-{k}))>t"

locale imp_map_add = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes add :: "'m  'm  'm Heap"
  assumes add_rule[sep_heap_rules]: 
    "<is_map m p * is_map m' p'> add p p' 
     <λr. is_map m p * is_map m' p' * is_map (m ++ m') r>t"


locale imp_map_size = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes size :: "'m  nat Heap"
  assumes size_rule[sep_heap_rules]: 
    "<is_map m p> size p <λr. is_map m p * (r = card (dom m))>t"

locale imp_map_iterate = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes is_it :: "('k  'v)  'm  ('k  'v)  'it  assn"
  fixes it_init :: "'m  ('it) Heap"
  fixes it_has_next :: "'it  bool Heap"
  fixes it_next :: "'it  (('k×'v)×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_map s p> it_init p <is_it s p s>t"
  assumes it_next_rule[sep_heap_rules]: "m'Map.empty  
    <is_it m p m' it> 
      it_next it 
    <λ((k,v),it'). is_it m p (m' |` (-{k})) it' * (m' k = Some v)>"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it m p m' it> it_has_next it <λr. is_it m p m' it * (rm'Map.empty)>"
  assumes quit_iteration:
    "is_it m p m' it A is_map m p * true"

locale imp_map_iterate' = imp_map +
  constrains is_map :: "('k  'v)  'm  assn"
  fixes is_it :: "('k  'v)  'm  ('k×'v) list  'it  assn"
  fixes it_init :: "'m  ('it) Heap"
  fixes it_has_next :: "'it  bool Heap"
  fixes it_next :: "'it  (('k×'v)×'it) Heap"
  assumes it_init_rule[sep_heap_rules]: 
    "<is_map s p> it_init p <λr. Al. (map_of l = s) * is_it s p l r>t"
  assumes it_next_rule[sep_heap_rules]: " 
    <is_it m p (kv#l) it> 
      it_next it 
    <λ(kv',it'). is_it m p l it' * (kv'=kv)>"
  assumes it_has_next_rule[sep_heap_rules]: 
    "<is_it m p l it> it_has_next it <λr. is_it m p l it * (rl[])>"
  assumes quit_iteration:
    "is_it m p l it A is_map m p * true"

end

Theory Hash_Table

section "Hash-Tables"
theory Hash_Table
imports
  Collections.HashCode
  Collections.Code_Target_ICF
  "../Sep_Main"
begin

subsection ‹Datatype›

subsubsection ‹Definition›

datatype ('k, 'v) hashtable = HashTable "('k × 'v) list array" nat

primrec the_array :: "('k, 'v) hashtable  ('k × 'v) list array"
  where "the_array (HashTable a _) = a"

primrec the_size :: "('k, 'v) hashtable  nat"
  where "the_size (HashTable _ n) = n"


subsubsection ‹Storable on Heap›

fun hs_encode :: "('k::countable, 'v::countable) hashtable  nat"
  where "hs_encode (HashTable a n) = to_nat (n, a)"

instance hashtable :: (countable, countable) countable
proof (rule countable_classI[of "hs_encode"])
  fix x y :: "('a, 'b) hashtable"
  assume "hs_encode x = hs_encode y"
  then show "x = y" by (cases x, cases y) auto
qed

instance hashtable :: (heap, heap) heap ..


subsection ‹Assertions›

subsubsection ‹Assertion for Hashtable›

definition ht_table :: "('k::heap × 'v::heap) list list  ('k, 'v) hashtable  assn"
  where "ht_table l ht = (the_array ht) a l"

definition ht_size :: "'a list list  nat  bool"
  where "ht_size l n  n = sum_list (map length l)"

definition ht_hash :: "('k::hashable × 'v) list list  bool" where
  "ht_hash l  i<length l. xset (l!i).
    bounded_hashcode_nat (length l) (fst x) = i"

definition ht_distinct :: "('k × 'v) list list  bool" where
  "ht_distinct l  i<length l. distinct (map fst (l!i))"


definition is_hashtable :: "('k::{heap,hashable} × 'v::heap) list list
     ('k, 'v) hashtable  assn"
where
  "is_hashtable l ht =
  (the_array ht a l) *
  (ht_size l (the_size ht)
     ht_hash l
     ht_distinct l
     1 < length l)"

lemma is_hashtable_prec: "precise is_hashtable"
  apply (rule preciseI)
  unfolding is_hashtable_def
  apply (auto simp add: preciseD[OF snga_prec])
  done

text ‹These rules are quite useful for automated methods, to avoid unfolding
  of definitions, that might be used folded in other lemmas,
  like induction hypothesis. However, they show in some sense a possibility for
  modularization improvement, as it should be enough to show an implication
  and know that the nth› and len› operations do not change
  the heap.›
lemma ht_array_nth_rule[sep_heap_rules]:
    "i<length l  <is_hashtable l ht>
      Array.nth (the_array ht) i
      <λr. is_hashtable l ht * (r = l!i)>"
  unfolding is_hashtable_def
  by sep_auto

lemma ht_array_length_rule[sep_heap_rules]:
    "<is_hashtable l ht>
      Array.len (the_array ht)
      <λr. is_hashtable l ht * (r = length l)>"
  unfolding is_hashtable_def
  by sep_auto


subsection ‹New›

subsubsection ‹Definition›

definition ht_new_sz :: "nat  ('k::{heap,hashable}, 'v::heap) hashtable Heap"
where
  "ht_new_sz n  do { let l = replicate n [];
  a  Array.of_list l;
  return (HashTable a 0) }"


definition ht_new :: "('k::{heap,hashable}, 'v::heap) hashtable Heap"
  where "ht_new  ht_new_sz (def_hashmap_size TYPE('k))"


subsubsection ‹Complete Correctness›

lemma ht_hash_replicate[simp, intro!]: "ht_hash (replicate n [])"
  apply (induct n)
  apply (auto simp add: ht_hash_def)
  apply (case_tac i)
  apply auto
  done

lemma ht_distinct_replicate[simp, intro!]: "ht_distinct (replicate n [])"
  apply (induct n)
  apply (auto simp add: ht_distinct_def)
  apply (case_tac i)
  apply auto
  done

lemma ht_size_replicate[simp, intro!]: "ht_size (replicate n []) 0"
  by (simp add: ht_size_def)

 ― ‹We can't create hash tables with a size of zero›
lemma complete_ht_new_sz: "1 < n  <emp> ht_new_sz n <is_hashtable (replicate n [])>"
  apply (unfold ht_new_sz_def)
  apply (simp del: replicate.simps)
  apply (rule bind_rule)
  apply (rule of_list_rule)
  apply (rule return_cons_rule)
  apply (simp add: is_hashtable_def)
  done

lemma complete_ht_new:
  "<emp>
     ht_new::('k::{heap,hashable}, 'v::heap) hashtable Heap
   <is_hashtable (replicate (def_hashmap_size TYPE('k)) [])>"
  unfolding ht_new_def
  by (simp add: complete_ht_new_sz[OF def_hashmap_size])


subsection ‹Lookup›

subsubsection ‹Definition›

fun ls_lookup :: "'k  ('k × 'v) list  'v option"
where
  "ls_lookup x [] = None" |
  "ls_lookup x ((k, v) # l) = (if x = k then Some v else ls_lookup x l)"

definition ht_lookup :: "'k  ('k::{heap,hashable}, 'v::heap) hashtable  'v option Heap"
where
  "ht_lookup x ht = do {
    m  Array.len (the_array ht);
    let i = bounded_hashcode_nat m x;
    l  Array.nth (the_array ht) i;
    return (ls_lookup x l)
  }"


subsubsection ‹Complete Correctness›

lemma complete_ht_lookup:
  "<is_hashtable l ht> ht_lookup x ht
     <λr. is_hashtable l ht *
        (r = ls_lookup x (l!(bounded_hashcode_nat (length l) x))) >"
  apply (cases ht)
  apply (clarsimp simp: is_hashtable_def)
  apply (simp add: ht_lookup_def)
  apply (rule bind_rule)
  apply (rule length_rule)
  apply (rule norm_pre_pure_rule)
  apply (rule bind_rule)
  apply (rule nth_rule)
  apply (simp add: bounded_hashcode_nat_bounds)
  apply (rule norm_pre_pure_rule)
  apply (rule return_cons_rule)
  apply simp
  done

text ‹Alternative, more automatic proof›
lemma complete_ht_lookup_alt_proof:
  "<is_hashtable l ht> ht_lookup x ht
    <λr. is_hashtable l ht *
      (r = ls_lookup x (l!(bounded_hashcode_nat (length l) x)))>"
  unfolding is_hashtable_def ht_lookup_def
  apply (cases ht)
  apply (sep_auto simp: bounded_hashcode_nat_bounds)
  done


subsection ‹Update›

subsubsection ‹Definition›

fun ls_update :: "'k  'v  ('k × 'v) list  (('k × 'v) list × bool)"
where
  "ls_update k v [] = ([(k, v)], False)" |
  "ls_update k v ((l, w) # ls) = (
    if k = l then
      ((k, v) # ls, True)
    else
      (let r = ls_update k v ls in ((l, w) # fst r, snd r))
  )"

definition abs_update
  :: "'k::hashable  'v  ('k × 'v) list list  ('k × 'v) list list"
  where
  "abs_update k v l =
    l[bounded_hashcode_nat (length l) k
      := fst (ls_update k v (l ! bounded_hashcode_nat (length l) k))]"

lemma ls_update_snd_set: "snd (ls_update k v l)  k  set (map fst l)"
  by (induct l rule: ls_update.induct) simp_all

lemma ls_update_fst_set: "set (fst (ls_update k v l))  insert (k, v) (set l)"
  apply (induct l rule: ls_update.induct)
  apply simp
  apply (auto simp add: Let_def)
  done

lemma ls_update_fst_map_set: "set (map fst (fst (ls_update k v l))) = insert k (set (map fst l))"
  apply (induct l rule: ls_update.induct)
  apply simp
  apply (auto simp add: Let_def)
  done

lemma ls_update_distinct: "distinct (map fst l)  distinct (map fst (fst (ls_update k v l)))"
proof (induct l rule: ls_update.induct)
  case 1 thus ?case by simp
next
  case (2 k v l w ls) show ?case
  proof (cases "k = l")
    case True
    with 2 show ?thesis by simp
  next
    case False
    with 2 have d: "distinct (map fst (fst (ls_update k v ls)))"
      by simp
    from 2(2) have "l  set (map fst ls)" by simp
    with False have "l  set (map fst (fst (ls_update k v ls)))"
      by (simp only: ls_update_fst_map_set) simp
    with d False show ?thesis by (simp add: Let_def)
  qed
qed

lemma ls_update_length: "length (fst (ls_update k v l))
  = (if (k  set (map fst l)) then length l else Suc (length l))"
  by (induct l rule: ls_update.induct) (auto simp add: Let_def)

lemma ls_update_length_snd_True:
  "snd (ls_update k v l)  length (fst (ls_update k v l)) = length l"
  by (simp add: ls_update_length ls_update_snd_set)

lemma ls_update_length_snd_False:
  "¬ snd (ls_update k v l)  length (fst (ls_update k v l)) = Suc (length l)"
  by (simp add: ls_update_length ls_update_snd_set)


definition ht_upd
  :: "'k  'v
     ('k::{heap,hashable}, 'v::heap) hashtable
     ('k, 'v) hashtable Heap"
  where
  "ht_upd k v ht = do {
      m  Array.len (the_array ht);
      let i = bounded_hashcode_nat m k;
      l  Array.nth (the_array ht) i;
      let l = ls_update k v l;
      Array.upd i (fst l) (the_array ht);
      let n = (if (snd l) then the_size ht else Suc (the_size ht));
      return (HashTable (the_array ht) n)
    }"


subsubsection ‹Complete Correctness›

lemma ht_hash_update:
  assumes "ht_hash ls"
  shows "ht_hash (abs_update k v ls)"
  unfolding ht_hash_def abs_update_def
  apply (intro allI ballI impI)
  apply simp
  subgoal premises prems for i x
  proof (cases "i = bounded_hashcode_nat (length ls) k")
    case True
    note i = True
    show ?thesis
    proof (cases "fst x = k")
      case True
      with i show ?thesis by simp
    next
      case False
      with prems i
      have
        "x  set (fst (ls_update k v
                         (ls ! bounded_hashcode_nat (length ls) k)))"
        by auto
      with
        ls_update_fst_set[
          of k v "ls ! bounded_hashcode_nat (length ls) k"]
        False
      have "x  insert (k, v)
                  (set (ls ! bounded_hashcode_nat (length ls) k))"
        by auto
      with False have "x  set (ls ! bounded_hashcode_nat (length ls) k)"
        by auto
      with i prems assms[unfolded ht_hash_def] show ?thesis by simp
    qed
  next
    case False
    with prems have "x  set (ls ! i)" by simp
    with prems assms[unfolded ht_hash_def] show ?thesis by simp
  qed
  done


lemma ht_distinct_update:
  assumes "ht_distinct l"
  shows "ht_distinct (abs_update k v l)"
  unfolding ht_distinct_def abs_update_def
  apply (intro allI impI)
  apply simp
  subgoal premises prems for i
  proof (cases "i = bounded_hashcode_nat (length l) k")
    case True
    with prems assms[unfolded ht_distinct_def]
    have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
      by simp
    from ls_update_distinct[OF this, of k v] True prems
    show ?thesis by simp
  next
    case False
    with prems assms[unfolded ht_distinct_def] show ?thesis by simp
  qed
  done


lemma length_update:
  assumes "1 < length l"
  shows "1 < length (abs_update k v l)"
  using assms
  by (simp add: abs_update_def)

lemma ht_size_update1:
  assumes size: "ht_size l n"
  assumes i: "i < length l"
  assumes snd: "snd (ls_update k v (l ! i))"
  shows "ht_size (l[i := fst (ls_update k v (l!i))]) n"
proof -
  have "(map length (l[i := fst (ls_update k v (l ! i))]))
    = (map length l)[i := length (fst (ls_update k v (l ! i)))]"
    by (simp add: map_update) also
  from sum_list_update[of i "map length l", simplified, OF i,
    of "length (fst (ls_update k v (l ! i)))"]
    ls_update_length_snd_True[OF snd]
  have
    "sum_list ((map length l)[i := length (fst (ls_update k v (l ! i)))])
    = sum_list (map length l)" by simp
  finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma ht_size_update2:
  assumes size: "ht_size l n"
  assumes i: "i < length l"
  assumes snd: "¬ snd (ls_update k v (l ! i))"
  shows "ht_size (l[i := fst (ls_update k v (l!i))]) (Suc n)"
proof -
  have "(map length (l[i := fst (ls_update k v (l ! i))]))
    = (map length l)[i := length (fst (ls_update k v (l ! i)))]"
    by (simp add: map_update) also
  from sum_list_update[of i "map length l", simplified, OF i,
    of "length (fst (ls_update k v (l ! i)))"]
    ls_update_length_snd_False[OF snd]
  have
    "sum_list ((map length l)[i := length (fst (ls_update k v (l ! i)))])
    = Suc (sum_list (map length l))" by simp
  finally show ?thesis using assms by (simp add: ht_size_def assms)
qed


lemma complete_ht_upd: "<is_hashtable l ht> ht_upd k v ht
  <is_hashtable (abs_update k v l)>"
  unfolding ht_upd_def is_hashtable_def
  apply (rule norm_pre_pure_rule)
  apply (rule bind_rule)
  apply (rule length_rule)
  apply (rule norm_pre_pure_rule)
  apply (simp add: Let_def)
  apply (rule bind_rule)
  apply (rule nth_rule)
  apply (simp add: bounded_hashcode_nat_bounds)
  apply (rule norm_pre_pure_rule)
  apply (rule bind_rule)
  apply (rule upd_rule)
  apply (simp add: bounded_hashcode_nat_bounds)
  apply (rule return_cons_rule)
  apply (auto
    simp add: ht_size_update1 ht_size_update2 bounded_hashcode_nat_bounds
              is_hashtable_def ht_hash_update[unfolded abs_update_def]
              ht_distinct_update[unfolded abs_update_def] abs_update_def)
  done

text ‹Alternative, more automatic proof›
lemma complete_ht_upd_alt_proof:
  "<is_hashtable l ht> ht_upd k v ht <is_hashtable (abs_update k v l)>"
  unfolding ht_upd_def is_hashtable_def Let_def
  (* TODO: Is this huge simp-step really necessary? *)
  apply (sep_auto
    simp: ht_size_update1 ht_size_update2 bounded_hashcode_nat_bounds
              is_hashtable_def ht_hash_update[unfolded abs_update_def]
              ht_distinct_update[unfolded abs_update_def] abs_update_def)
  done


subsection ‹Delete›

subsubsection ‹Definition›

fun ls_delete :: "'k  ('k × 'v) list  (('k × 'v) list × bool)" where
  "ls_delete k [] = ([], False)" |
  "ls_delete k ((l, w) # ls) = (
    if k = l then
      (ls, True)
    else
      (let r = ls_delete k ls in ((l, w) # fst r, snd r)))"

lemma ls_delete_snd_set: "snd (ls_delete k l)  k  set (map fst l)"
  by (induct l rule: ls_delete.induct) simp_all

lemma ls_delete_fst_set: "set (fst (ls_delete k l))  set l"
  apply (induct l rule: ls_delete.induct)
  apply simp
  apply (auto simp add: Let_def)
  done

lemma ls_delete_fst_map_set:
  "distinct (map fst l) 
  set (map fst (fst (ls_delete k l))) = (set (map fst l)) - {k}"
  apply (induct l rule: ls_delete.induct)
  apply simp
  apply (auto simp add: Let_def)
  done

lemma ls_delete_distinct: "distinct (map fst l)  distinct (map fst (fst (ls_delete k l)))"
proof (induct l rule: ls_delete.induct)
  case 1 thus ?case by simp
next
  case (2 k l w ls) show ?case
  proof (cases "k = l")
    case True
    with 2 show ?thesis by simp
  next
    case False
    with 2 have d: "distinct (map fst (fst (ls_delete k ls)))"
      by simp
    from 2 have d2: "distinct (map fst ls)" by simp
    from 2(2) have "l  set (map fst ls)" by simp
    with False 2 ls_delete_fst_map_set[OF d2, of k]
    have "l  set (map fst (fst (ls_delete k ls)))"
      by simp
    with d False show ?thesis by (simp add: Let_def)
  qed
qed

lemma ls_delete_length:
  "length (fst (ls_delete k l)) = (
    if (k  set (map fst l)) then
      (length l - 1)
    else
      length l)"
proof (induct l rule: ls_delete.induct)
  case 1
  then show ?case by simp
next
  case (2 k l w ls)
  then show ?case by (cases ls) (auto simp add: Let_def)
qed

lemma ls_delete_length_snd_True:
  "snd (ls_delete k l)  length (fst (ls_delete k l)) = length l - 1"
  by (simp add: ls_delete_length ls_delete_snd_set)

lemma ls_delete_length_snd_False:
  "¬ snd (ls_delete k l)  length (fst (ls_delete k l)) = length l"
  by (simp add: ls_delete_length ls_delete_snd_set)


definition ht_delete
  :: "'k
     ('k::{heap,hashable}, 'v::heap) hashtable
     ('k, 'v) hashtable Heap"
  where
  "ht_delete k ht = do {
      m  Array.len (the_array ht);
      let i = bounded_hashcode_nat m k;
      l  Array.nth (the_array ht) i;
      let l = ls_delete k l;
      Array.upd i (fst l) (the_array ht);
      let n = (if (snd l) then (the_size ht - 1) else the_size ht);
      return (HashTable (the_array ht) n)
    }"


subsubsection ‹Complete Correctness›

lemma ht_hash_delete:
  assumes "ht_hash ls"
  shows "ht_hash (
    ls[bounded_hashcode_nat (length ls) k
      := fst (ls_delete k
               (ls ! bounded_hashcode_nat (length ls) k)
             )
      ]
  )"
  unfolding ht_hash_def
  apply (intro allI ballI impI)
  apply simp
  subgoal premises prems for i x
  proof (cases "i = bounded_hashcode_nat (length ls) k")
    case i: True
    show ?thesis
    proof (cases "fst x = k")
      case True
      with i show ?thesis by simp
    next
      case False
      with prems i
      have
        "x  set (fst (ls_delete k
                        (ls ! bounded_hashcode_nat (length ls) k)))"
        by auto
      with
        ls_delete_fst_set[
          of k "ls ! bounded_hashcode_nat (length ls) k"]
        False
      have "x  (set (ls ! bounded_hashcode_nat (length ls) k))" by auto
      with i prems assms[unfolded ht_hash_def] show ?thesis by simp
    qed
  next
    case False
    with prems have "x  set (ls ! i)" by simp
    with prems assms[unfolded ht_hash_def] show ?thesis by simp
  qed
  done

lemma ht_distinct_delete:
  assumes "ht_distinct l"
  shows "ht_distinct (
    l[bounded_hashcode_nat (length l) k
      := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])"
  unfolding ht_distinct_def
  apply (intro allI impI)
  apply simp
  subgoal premises prems for i
  proof (cases "i = bounded_hashcode_nat (length l) k")
    case True
    with prems assms[unfolded ht_distinct_def]
    have "distinct (map fst (l ! bounded_hashcode_nat (length l) k))"
      by simp
    from ls_delete_distinct[OF this, of k] True prems
    show ?thesis by simp
  next
    case False
    with prems assms[unfolded ht_distinct_def] show ?thesis by simp
  qed
  done

lemma ht_size_delete1:
  assumes size: "ht_size l n"
  assumes i: "i < length l"
  assumes snd: "snd (ls_delete k (l ! i))"
  shows "ht_size (l[i := fst (ls_delete k (l!i))]) (n - 1)"
proof -
  have "(map length (l[i := fst (ls_delete k (l ! i))]))
    = (map length l)[i := length (fst (ls_delete k (l ! i)))]"
    by (simp add: map_update) also
  from sum_list_update[of i "map length l", simplified, OF i,
    of "length (fst (ls_delete k (l ! i)))"]
    ls_delete_length_snd_True[OF snd] snd
  have "sum_list ((map length l)[i := length (fst (ls_delete k (l ! i)))])
    = sum_list (map length l) - 1"
    by (cases "length (l ! i)") (simp_all add: ls_delete_snd_set)
  finally show ?thesis using assms by (simp add: ht_size_def assms)
qed

lemma ht_size_delete2:
  assumes size: "ht_size l n"
  assumes i: "i < length l"
  assumes snd: "¬ snd (ls_delete k (l ! i))"
  shows "ht_size (l[i := fst (ls_delete k (l!i))]) n"
proof -
  have "(map length (l[i := fst (ls_delete k (l ! i))]))
    = (map length l)[i := length (fst (ls_delete k (l ! i)))]"
    by (simp add: map_update) also
  from sum_list_update[of i "map length l", simplified, OF i,
    of "length (fst (ls_delete k (l ! i)))"]
    ls_delete_length_snd_False[OF snd]
  have "sum_list ((map length l)[i := length (fst (ls_delete k (l ! i)))])
    = sum_list (map length l)" by simp
  finally show ?thesis using assms by (simp add: ht_size_def assms)
qed


lemma complete_ht_delete: "<is_hashtable l ht> ht_delete k ht
  <is_hashtable (l[bounded_hashcode_nat (length l) k
    := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])>"
  unfolding ht_delete_def is_hashtable_def
  apply (rule norm_pre_pure_rule)
  apply (rule bind_rule)
  apply (rule length_rule)
  apply (rule norm_pre_pure_rule)
  apply (simp add: Let_def)
  apply (rule bind_rule)
  apply (rule nth_rule)
  apply (simp add: bounded_hashcode_nat_bounds)
  apply (rule norm_pre_pure_rule)
  apply (rule bind_rule)
  apply (rule upd_rule)
  apply (simp add: bounded_hashcode_nat_bounds)
  apply (rule return_cons_rule)
  apply (auto
    simp add: ht_size_delete1 ht_size_delete2 bounded_hashcode_nat_bounds
              is_hashtable_def ht_hash_delete ht_distinct_delete)
  using ht_size_delete1[OF _ bounded_hashcode_nat_bounds[of "length l" k], of "the_size ht"]
  apply simp
  done

text ‹Alternative, more automatic proof›
lemma "<is_hashtable l ht> ht_delete k ht
  <is_hashtable (l[bounded_hashcode_nat (length l)
    k := fst (ls_delete k (l ! bounded_hashcode_nat (length l) k))])>"
  unfolding ht_delete_def is_hashtable_def Let_def
  using ht_size_delete1[OF _ bounded_hashcode_nat_bounds[of "length l" k],
    of "the_size ht"]
  apply (sep_auto simp:
    ht_size_delete1 ht_size_delete2 bounded_hashcode_nat_bounds
    is_hashtable_def ht_hash_delete ht_distinct_delete)
  done


subsection ‹Re-Hashing›

subsubsection ‹Auxiliary Functions›

text ‹\paragraph{Insert List}›
fun ht_insls
  :: "('k × 'v) list
     ('k::{heap,hashable}, 'v::heap) hashtable
     ('k, 'v::heap) hashtable Heap"
  where
  "ht_insls [] ht = return ht" |
  "ht_insls ((k, v) # l) ht = do { h  ht_upd k v ht; ht_insls l h }"

text "Abstract version"
fun ls_insls :: "('k::hashable × 'v) list
   ('k × 'v) list list  ('k × 'v) list list"
where
  "ls_insls [] l = l" |
  "ls_insls ((k, v) # ls) l =
    ls_insls ls (abs_update k v l)"

lemma ht_hash_ls_insls:
  assumes "ht_hash l"
  shows "ht_hash (ls_insls ls l)"
  using assms
  apply (induct l rule: ls_insls.induct)
  apply simp
  apply (simp add: ht_hash_update)
  done

lemma ht_distinct_ls_insls:
  assumes "ht_distinct l"
  shows "ht_distinct (ls_insls ls l)"
  using assms
  apply (induct l rule: ls_insls.induct)
  apply simp
  apply (simp add: ht_distinct_update)
  done

lemma length_ls_insls:
  assumes "1 < length l"
  shows "1 < length (ls_insls ls l)"
  using assms
proof (induct l rule: ls_insls.induct)
  case 1
  then show ?case by simp
next
  case (2 k v ls l)
  from 2(1)[OF length_update[OF 2(2), of k v]] show ?case
    by simp
qed

lemma complete_ht_insls:
  "<is_hashtable ls ht> ht_insls xs ht <is_hashtable (ls_insls xs ls)>"
proof (induct xs arbitrary: ls ht)
  case Nil
  show ?case by (auto intro: return_cons_rule)
next
  case (Cons x xs)
  show ?case
  proof (cases x)
    case (Pair k v)
    then show ?thesis
      apply simp
      apply (rule bind_rule)
      apply (rule complete_ht_upd)
      apply (simp add: Cons)
      done
  qed
qed

text ‹\paragraph{Copy}›
fun ht_copy :: "nat  ('k::{heap,hashable}, 'v::heap) hashtable
   ('k, 'v) hashtable  ('k, 'v) hashtable Heap"
  where
  "ht_copy 0 src dst = return dst" |
  "ht_copy (Suc n) src dst = do {
    l  Array.nth (the_array src) n;
    ht  ht_insls l dst;
    ht_copy n src ht
  }"

text "Abstract version"
fun ls_copy :: "nat  ('k::hashable × 'v) list list
   ('k × 'v) list list  ('k × 'v) list list"
  where
  "ls_copy 0 ss ds = ds" |
  "ls_copy (Suc n) ss ds = ls_copy n ss (ls_insls (ss ! n) ds)"

lemma ht_hash_ls_copy:
  assumes "ht_hash l"
  shows "ht_hash (ls_copy n ss l)"
  using assms
  apply (induct n arbitrary: l)
  apply simp
  apply (simp add: ht_hash_ls_insls)
  done

lemma ht_distinct_ls_copy:
  assumes "ht_distinct l"
  shows "ht_distinct (ls_copy n ss l)"
  using assms
  apply (induct n arbitrary: l)
  apply simp
  apply (simp add: ht_distinct_ls_insls)
  done

lemma length_ls_copy:
  assumes "1 < length l"
  shows "1 < length (ls_copy n ss l)"
  using assms
proof (induct n arbitrary: l)
  case 0
  then show ?case by simp
next
  case (Suc n)
  from Suc(1)[OF length_ls_insls[OF Suc(2)]] show ?case by simp
qed

lemma complete_ht_copy: "n  List.length ss 
  <is_hashtable ss src * is_hashtable ds dst>
  ht_copy n src dst
  <λr. is_hashtable ss src * is_hashtable (ls_copy n ss ds) r>"
proof (induct n arbitrary: ds dst)
  case 0
  show ?case by (auto intro!: return_cons_rule)
next
  case (Suc n)
  then have n: "n < length ss" by simp
  then have "n  length ss" by simp
  note IH = Suc(1)[OF this]
  show ?case
    apply simp
    apply (rule bind_rule)
    apply (rule frame_rule)
    apply (subgoal_tac "<is_hashtable ss src>
      Array.nth (the_array src) n
      <λr. is_hashtable ss src * (r = ss ! n)>")
    apply simp
    apply (simp add: is_hashtable_def)
    apply (auto intro!: nth_rule simp add: n)[]
    apply clarsimp
    apply (rule bind_rule)
    apply (rule frame_rule_left)
    apply (rule complete_ht_insls)
    apply (simp add: IH)
    done
qed

text ‹Alternative, more automatic proof›
lemma complete_ht_copy_alt_proof: "n  List.length ss 
  <is_hashtable ss src * is_hashtable ds dst>
  ht_copy n src dst
  <λr. is_hashtable ss src * is_hashtable (ls_copy n ss ds) r>"
proof (induct n arbitrary: ds dst)
  case 0
  show ?case by (sep_auto)
next
  case (Suc n)
  then have N_LESS: "n < length ss" by simp
  then have N_LE: "n  length ss" by simp
  note IH = Suc(1)[OF this]
  show ?case
    by (sep_auto simp: N_LESS N_LE heap: complete_ht_insls IH)
qed

definition ht_rehash
  :: "('k::{heap,hashable}, 'v::heap) hashtable  ('k, 'v) hashtable Heap"
  where
  "ht_rehash ht = do {
    n  Array.len (the_array ht);
    h  ht_new_sz (2 * n);
    ht_copy n ht h
  }"

text "Operation on Abstraction"
definition ls_rehash :: "('k::hashable × 'v) list list  ('k × 'v) list list"
  where "ls_rehash l = ls_copy (List.length l) l (replicate (2 * length l) [])"

lemma ht_hash_ls_rehash: "ht_hash (ls_rehash l)"
  by (simp add: ht_hash_ls_copy ls_rehash_def)

lemma ht_distinct_ls_rehash: "ht_distinct (ls_rehash l)"
  by (simp add: ht_distinct_ls_copy ls_rehash_def)

lemma length_ls_rehash:
  assumes "1 < length l"
  shows "1 < length (ls_rehash l)"
proof -
  from assms have "1 < length (replicate (2 * length l) [])" by simp
  from length_ls_copy[OF this, of "length l" l] show ?thesis
    by (simp add: ls_rehash_def)
qed

lemma ht_imp_len: "is_hashtable l ht A is_hashtable l ht * (length l > 0)"
  unfolding is_hashtable_def
  by sep_auto

lemma complete_ht_rehash:
  "<is_hashtable l ht> ht_rehash ht
  <λr. is_hashtable l ht * is_hashtable (ls_rehash l) r>"
  apply (rule cons_pre_rule[OF ht_imp_len])
  unfolding ht_rehash_def
  apply (sep_auto heap: complete_ht_new_sz)
  apply (cases l; simp)
  apply (sep_auto heap: complete_ht_copy simp: ls_rehash_def)
  done

definition load_factor :: nat ― ‹in percent›
  where "load_factor = 75"

definition ht_update
  :: "'k::{heap,hashable}  'v::heap