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