Theory Sep_Tactics_Test

(* Authors: Gerwin Klein and Rafal Kolanski, 2012
   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
                Rafal Kolanski <rafal.kolanski at nicta.com.au>
*)

theory Sep_Tactics_Test
imports "../Sep_Tactics"
begin

text ‹Substitution and forward/backward reasoning›

typedecl p
typedecl val
typedecl heap

axiomatization where heap_sep_algebra: "OFCLASS(heap, sep_algebra_class)"
instance heap :: sep_algebra by (rule heap_sep_algebra)

axiomatization
  points_to :: "p ⇒ val ⇒ heap ⇒ bool" and
  val :: "heap ⇒ p ⇒ val"
where
  points_to: "(points_to p v ** P) h ⟹ val h p = v"


lemma
  "⟦ Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h ⟧
   ⟹ Q (val h p) (val h p)"
  apply (sep_subst (2) points_to)
  apply (sep_subst (asm) points_to)
  apply (sep_subst points_to)
  oops

lemma
  "⟦ Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h ⟧
   ⟹ Q (val h p) (val h p)"
  apply (sep_drule points_to)
  apply simp
  oops

lemma
  "⟦ Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h ⟧
   ⟹ Q (val h p) (val h p)"
  apply (sep_frule points_to)
  apply simp
  oops

consts
  update :: "p ⇒ val ⇒ heap ⇒ heap"

schematic_goal
  assumes a: "⋀P. (stuff p ** P) H ⟹ (other_stuff p v ** P) (update p v H)"
  shows "(X ** Y ** other_stuff p ?v) (update p v H)"
  apply (sep_rule a)
  oops


text ‹Example of low-level rewrites›

lemma "⟦ unrelated s ; (P ** Q ** R) s ⟧ ⟹ (A ** B ** Q ** P) s"
  apply (tactic ‹dresolve_tac @{context} [mk_sep_select_rule @{context} true (3, 1)] 1›)
  apply (tactic ‹resolve_tac @{context} [mk_sep_select_rule @{context} false (4, 2)] 1›)
  (* now sep_conj_impl1 can be used *)
  apply (erule (1) sep_conj_impl)
  oops


text ‹Conjunct selection›

lemma "(A ** B ** Q ** P) s"
  apply (sep_select 1)
  apply (sep_select 3)
  apply (sep_select 4)
  oops

lemma "⟦ also unrelated; (A ** B ** Q ** P) s ⟧ ⟹ unrelated"
  apply (sep_select_asm 2)
  oops


section ‹Test cases for ‹sep_cancel›.›

lemma
  assumes forward: "⋀s g p v. A g p v s ⟹ AA g p s "
  shows "⋀xv yv P s y x s. (A g x yv ** A g y yv ** P) s ⟹ (AA g y ** sep_true) s"
  by (sep_cancel add: forward)

lemma
  assumes forward: "⋀s. generic s ⟹ instance s"
  shows "(A ** generic ** B) s ⟹ (instance ** sep_true) s"
  by (sep_cancel add: forward)

lemma "⟦ (A ** B) sa ; (A ** Y) s ⟧ ⟹ (A ** X) s"
  apply (sep_cancel)
  oops

lemma "⟦ (A ** B) sa ; (A ** Y) s ⟧ ⟹ (λs. (A ** X) s) s"
  apply (sep_cancel)
  oops

schematic_goal "⟦ (B ** A ** C) s ⟧ ⟹ (λs. (A ** ?X) s) s"
  by (sep_cancel)

(* test backtracking on premises with same state *)
lemma
  assumes forward: "⋀s. generic s ⟹ instance s"
  shows "⟦ (A ** B) s ; (generic ** Y) s ⟧ ⟹ (X ** instance) s"
  apply (sep_cancel add: forward)
  oops

lemma
  assumes forward: "⋀s. generic s ⟹ instance s"
  shows "generic s ⟹ instance s"
  by (sep_cancel add: forward)

lemma
  assumes forward: "⋀s. generic s ⟹ instance s"
  assumes forward2: "⋀s. instance s ⟹ instance2 s"
  shows "generic s ⟹ (instance2 ** sep_true) s"
  by (sep_cancel_blast add: forward forward2)

end