1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(* Authors: Gerwin Klein and Rafal Kolanski, 2012
8   Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au>
9                Rafal Kolanski <rafal.kolanski at nicta.com.au>
10*)
11
12theory Sep_Tactics_Test
13imports Sep_Tactics
14begin
15
16text \<open>Substitution and forward/backward reasoning\<close>
17
18typedecl p
19typedecl val
20typedecl heap
21
22axiomatization where
23  heap_algebra: "OFCLASS(heap, sep_algebra_class)"
24
25instantiation heap :: sep_algebra
26begin
27  instance by (rule heap_algebra)
28end
29
30axiomatization
31  points_to :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> bool" and
32  val :: "heap \<Rightarrow> p \<Rightarrow> val"
33where
34  points_to: "(points_to p v ** P) h \<Longrightarrow> val h p = v"
35
36consts
37  update :: "p \<Rightarrow> val \<Rightarrow> heap \<Rightarrow> heap"
38
39(* FIXME: revive
40lemma
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_subst (2) points_to)
44  apply (sep_subst (asm) points_to)
45  apply (sep_subst points_to)
46  oops
47*)
48
49lemma
50  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
51   \<Longrightarrow> Q (val h p) (val h p)"
52  apply (sep_drule (direct) points_to)
53  apply simp
54  oops
55
56lemma
57  "\<lbrakk> Q2 (val h p); (K ** T ** blub ** P ** points_to p v ** P ** J) h \<rbrakk>
58   \<Longrightarrow> Q (val h p) (val h p)"
59  apply (sep_frule (direct) points_to)
60  apply simp
61  oops
62
63schematic_goal
64  assumes a: "\<And>P. (stuff p ** P) H \<Longrightarrow> (other_stuff p v ** P) (update p v H)"
65  shows "(X ** Y ** other_stuff p ?v) (update p v H)"
66  apply (sep_rule (direct) a)
67  oops
68
69
70
71text \<open>Conjunct selection\<close>
72
73lemma "(A ** B ** Q ** P) s"
74  apply (sep_select 1)
75  apply (sep_select 3)
76  apply (sep_select 4)
77  oops
78
79lemma "\<lbrakk> also unrelated; (A ** B ** Q ** P) s \<rbrakk> \<Longrightarrow> unrelated"
80  apply (sep_select_asm 2)
81  oops
82
83
84section \<open>Test cases for @{text sep_cancel}.\<close>
85
86lemma
87  assumes forward: "\<And>s g p v. A g p v s \<Longrightarrow> AA g p s "
88  shows "\<And>yv P y x s. (A g x yv ** A g y yv ** P) s \<Longrightarrow> (AA g y ** sep_true) s"
89  by (sep_solve add: forward)
90
91lemma
92  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
93  shows "(A ** generic ** B) s \<Longrightarrow> (instance ** sep_true) s"
94  by (sep_solve add: forward)
95
96lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (A ** X) s"
97  apply (sep_cancel)
98  oops
99
100lemma "\<lbrakk> (A ** B) sa ; (A ** Y) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** X) s) s"
101  apply (sep_cancel)
102  oops
103
104schematic_goal "\<lbrakk> (B ** A ** C) s \<rbrakk> \<Longrightarrow> (\<lambda>s. (A ** ?X) s) s"
105  by (sep_cancel)
106
107(* test backtracking on premises with same state *)
108lemma
109  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
110  shows "\<lbrakk> (A ** B) s ; (generic ** Y) s \<rbrakk> \<Longrightarrow> (X ** instance) s"
111  apply (sep_cancel add: forward)
112  oops
113
114lemma f1:
115  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
116  shows "generic s \<Longrightarrow> instance s"
117  by (sep_cancel add: forward)
118
119declare sep_conj_true[sep_cancel]
120
121lemma boxo: "P s \<Longrightarrow> (P \<and>* \<box>) s"
122  by (erule sep_conj_sep_emptyI)
123
124lemma f2:
125  assumes forward: "\<And>s. generic s \<Longrightarrow> instance s"
126  assumes forward2: "\<And>s. instance s \<Longrightarrow> instance2 s"
127  shows "generic s \<Longrightarrow> (instance2 ** \<box>) s"
128  apply (drule forward forward2)+
129  apply (sep_erule_concl (direct) boxo)
130  done
131
132end
133