1 (* Authors: Gerwin Klein and Rafal Kolanski, 2012

     2    Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>

     3                 Rafal Kolanski <rafal.kolanski at nicta.com.au>

     4 *)

     5 

     6 theory Sep_Tactics_Test

     7 imports "../Sep_Tactics"

     8 begin

     9 

    10 text {* Substitution and forward/backward reasoning *}

    11 

    12 typedecl p

    13 typedecl val

    14 typedecl heap

    15 

    16 arities heap :: sep_algebra

    17 

    18 axiomatization

    19   points_to :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> bool" and

    20   val :: "heap \<Rightarrow> p \<Rightarrow> val"

    21 where

    22   points_to: "(points_to p v ** P) h \<Longrightarrow> val h p = v"

    23 

    24 

    25 lemma

    26   "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>

    27    \<Longrightarrow> Q (val h p) (val h p)"

    28   apply (sep_subst (2) points_to)

    29   apply (sep_subst (asm) points_to)

    30   apply (sep_subst points_to)

    31   oops

    32 

    33 lemma

    34   "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>

    35    \<Longrightarrow> Q (val h p) (val h p)"

    36   apply (sep_drule points_to)

    37   apply simp

    38   oops

    39 

    40 lemma

    41   "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>

    42    \<Longrightarrow> Q (val h p) (val h p)"

    43   apply (sep_frule points_to)

    44   apply simp

    45   oops

    46 

    47 consts

    48   update :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> heap"

    49 

    50 schematic_lemma

    51   assumes a: "\<And>P. (stuff p ** P) H \<Longrightarrow> (other_stuff p v ** P) (update p v H)"

    52   shows "(X ** Y ** other_stuff p ?v) (update p v H)"

    53   apply (sep_rule a)

    54   oops

    55 

    56 

    57 text {* Example of low-level rewrites *}

    58 

    59 lemma "\<lbrakk> unrelated s ; (P ** Q ** R) s \<rbrakk> \<Longrightarrow> (A ** B ** Q ** P) s"

    60   apply (tactic {* dtac (mk_sep_select_rule @{context} true (3,1)) 1 *})

    61   apply (tactic {* rtac (mk_sep_select_rule @{context} false (4,2)) 1 *})

    62   (* now sep_conj_impl1 can be used *)

    63   apply (erule (1) sep_conj_impl)

    64   oops

    65 

    66 

    67 text {* Conjunct selection *}

    68 

    69 lemma "(A ** B ** Q ** P) s"

    70   apply (sep_select 1)

    71   apply (sep_select 3)

    72   apply (sep_select 4)

    73   oops

    74 

    75 lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated"

    76   apply (sep_select_asm 2)

    77   oops

    78 

    79 

    80 section {* Test cases for @{text sep_cancel}. *}

    81 

    82 lemma

    83   assumes forward: "\<And>s g p v. A g p v s \<Longrightarrow> AA g p s "

    84   shows "\<And>xv yv P s y x s. (A g x yv ** A g y yv ** P) s \<Longrightarrow> (AA g y ** sep_true) s"

    85   by (sep_cancel add: forward)

    86 

    87 lemma

    88   assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"

    89   shows "(A ** generic ** B) s \<Longrightarrow> (instance ** sep_true) s"

    90   by (sep_cancel add: forward)

    91 

    92 lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s"

    93   apply (sep_cancel)

    94   oops

    95 

    96 lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s"

    97   apply (sep_cancel)

    98   oops

    99 

   100 schematic_lemma "\<lbrakk> (B ** A ** C) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** ?X) s) s"

   101   by (sep_cancel)

   102 

   103 (* test backtracking on premises with same state *)

   104 lemma

   105   assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"

   106   shows "\<lbrakk> (A ** B) s ; (generic ** Y) s \<rbrakk> \<Longrightarrow> (X ** instance) s"

   107   apply (sep_cancel add: forward)

   108   oops

   109 

   110 lemma

   111   assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"

   112   shows "generic s \<Longrightarrow> instance s"

   113   by (sep_cancel add: forward)

   114 

   115 lemma

   116   assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"

   117   assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"

   118   shows "generic s \<Longrightarrow> (instance2 ** sep_true) s"

   119   by (sep_cancel_blast add: forward forward2)

   120 

   121 end

   122