1(* 2 * 3 * Copyright 2017, Data61, CSIRO 4 * 5 * This software may be distributed and modified according to the terms of 6 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 7 * See "LICENSE_BSD2.txt" for details. 8 * 9 * @TAG(DATA61_BSD) 10 *) 11 12theory Corres_Adjust_Preconds 13 14imports 15 "Corres_UL" 16 17begin 18 19text {* 20Gadget for adjusting preconditions in a corres rule or similar. 21 22Probably only useful for predicates with two or more related 23preconditions, such as corres. 24 25Used to do some_corres_rule[adj_corres some_intro_rule], 26given e.g. some_intro_rule: @{prop "(s, t) \<in> sr \<Longrightarrow> P s \<Longrightarrow> Q t"} 27Will apply this rule to solve @{prop "Q t"} components in either 28precondition or any sub-conjunct, and will then try to put the 29assumptions @{prop "P s"}, @{prop "(s, t) \<in> sr"} into the right 30places. The premises of the rule can be in any given order. 31 32Concrete example at the bottom. 33*} 34 35named_theorems corres_adjust_precond_structures 36 37locale corres_adjust_preconds begin 38 39text {* Worker predicates. Broadly speaking, a goal 40of the form "preconds ?A ?B ?C ?D ==> P" expects to 41establish P by instantiating ?A, or failing that ?B, 42etc. 43 44A goal of the form finalise_preconds A exists to 45make sure that schematic conjuncts of A are resolved 46to True. *} 47definition 48 preconds :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" 49where 50 "preconds A B C D = (A \<and> B \<and> C \<and> D)" 51 52definition 53 finalise_preconds :: "bool \<Rightarrow> bool" 54where 55 "finalise_preconds A = True" 56 57text {* Use a precond directly to establish goal. *} 58lemma consume_preconds: 59 "preconds A True True True \<Longrightarrow> A" 60 "preconds True B True True \<Longrightarrow> B" 61 "preconds True True C True \<Longrightarrow> C" 62 "preconds True True True D \<Longrightarrow> D" 63 by (simp_all add: preconds_def) 64 65lemmas consume_preconds_True = consume_preconds(1)[where A=True] 66 67text {* For use as a drule, split a set of schematic preconds 68to give two sets that can be instantiated separately. *} 69lemma split_preconds_left: 70 "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A B C D" 71 "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A B C True" 72 "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A B True True" 73 "preconds (A \<and> A') True True True \<Longrightarrow> preconds A True True True" 74 by (simp_all add: preconds_def) 75 76lemma split_preconds_right: 77 "preconds (A \<and> A') (B \<and> B') (C \<and> C') (D \<and> D') \<Longrightarrow> preconds A' B' C' D'" 78 "preconds (A \<and> A') (B \<and> B') (C \<and> C') True \<Longrightarrow> preconds A' B' C' True" 79 "preconds (A \<and> A') (B \<and> B') True True \<Longrightarrow> preconds A' B' True True" 80 "preconds (A \<and> A') True True True \<Longrightarrow> preconds A' True True True" 81 by (simp_all add: preconds_def) 82 83text {* For use as an erule. Initiate the precond process, 84creating a finalise goal to be solved later. *} 85lemma preconds_goal_initiate: 86 "preconds A B C D \<Longrightarrow> (preconds A B C D \<Longrightarrow> Q) 87 \<Longrightarrow> finalise_preconds (A \<and> B \<and> C \<and> D) \<Longrightarrow> Q" 88 by simp 89 90text {* Finalise preconds, trying to replace conjuncts with 91True if they are not yet instantiated. *} 92lemma finalise_preconds: 93 "finalise_preconds True" 94 "finalise_preconds A \<Longrightarrow> finalise_preconds B \<Longrightarrow> finalise_preconds (A \<and> B)" 95 "finalise_preconds X" 96 by (simp_all add: finalise_preconds_def) 97 98text {* Shape of the whole process for application to regular corres goals. *} 99lemma corres_adjust_pre: 100 "corres_underlying R nf nf' rs P Q f f' 101 \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (P1 s) (Q1 s') True True \<Longrightarrow> P s) 102 \<Longrightarrow> (\<And>s s'. (s, s') \<in> R \<Longrightarrow> preconds (Q2 s') (P2 s) True True \<Longrightarrow> Q s') 103 \<Longrightarrow> corres_underlying R nf nf' rs (\<lambda>s. P1 s \<and> P2 s) (\<lambda>s'. Q1 s' \<and> Q2 s') f f'" 104 apply (erule stronger_corres_guard_imp) 105 apply (simp add: preconds_def)+ 106 done 107 108ML {* 109 110structure Corres_Adjust_Preconds = struct 111 112val def_intros = @{thms conjI pred_conj_app[THEN iffD2] 113 bipred_conj_app[THEN fun_cong, THEN iffD2]} 114 115(* apply an intro rule, splitting preconds assumptions to 116 provide unique assumptions for each goal. *) 117fun intro_split ctxt intros i = 118 ((resolve_tac ctxt intros 119 THEN_ALL_NEW (TRY o assume_tac ctxt)) 120 THEN_ALL_NEW (fn j => (EVERY (replicate (j - i) (dresolve_tac ctxt @{thms split_preconds_left} j))) 121 THEN dresolve_tac ctxt @{thms split_preconds_right} j)) i 122 123fun handle_preconds ctxt intros = 124 TRY o (eresolve_tac ctxt [@{thm preconds_goal_initiate}] 125 THEN' REPEAT_ALL_NEW (eresolve_tac ctxt @{thms consume_preconds_True} 126 ORELSE' intro_split ctxt (intros @ def_intros) 127 ORELSE' eresolve_tac ctxt @{thms consume_preconds}) 128 THEN' REPEAT_ALL_NEW (resolve_tac ctxt @{thms finalise_preconds}) 129 ) 130 131fun mk_adj_preconds ctxt intros rule = let 132 val xs = [rule] RL (Named_Theorems.get ctxt @{named_theorems corres_adjust_precond_structures}) 133 val x = case xs of 134 [] => raise THM ("no unifier with corres_adjust_precond_structures", 1, [rule]) 135 | xs => hd xs 136 in x 137 |> ALLGOALS (handle_preconds ctxt intros) 138 |> Seq.hd 139 |> Simplifier.simplify (clear_simpset ctxt addsimps @{thms conj_assoc simp_thms(21-22)}) 140 end 141 142val setup = 143 Attrib.setup @{binding "adj_corres"} 144 ((Attrib.thms -- Args.context) 145 >> (fn (intros, ctxt) => Thm.rule_attribute [] (K (mk_adj_preconds ctxt intros)))) 146 "use argument theorems to adjust a corres theorem." 147 148end 149 150*} 151 152end 153 154declare corres_adjust_preconds.corres_adjust_pre[corres_adjust_precond_structures] 155 156setup Corres_Adjust_Preconds.setup 157 158experiment begin 159 160definition 161 test_sr :: "(nat \<times> nat) set" 162where 163 "test_sr = {(x, y). y = 2 * x}" 164 165lemma test_corres: 166 "corres_underlying test_sr nf nf' dc (\<lambda>x. x < 40) (\<lambda>y. y < 30 \<and> y = 6) 167 (modify (\<lambda>x. x + 2)) (modify (\<lambda>y. 10))" 168 by (simp add: corres_underlying_def simpler_modify_def test_sr_def) 169 170lemma test_adj_precond: 171 "(x, y) \<in> test_sr \<Longrightarrow> x = 3 \<Longrightarrow> y = 6" 172 by (simp add: test_sr_def) 173 174ML {* 175Corres_Adjust_Preconds.mk_adj_preconds @{context} [@{thm test_adj_precond}] @{thm test_corres} 176*} 177 178lemma foo_adj_corres: 179 "corres_underlying test_sr nf nf' dc (\<lambda>s. s < 40 \<and> s = 3) (\<lambda>s'. s' < 30) (modify (\<lambda>x. x + 2)) 180 (modify (\<lambda>y. 10))" 181 by (rule test_corres[adj_corres test_adj_precond]) 182 183text {* A more general demo of what it does. *} 184lemma 185 assumes my_corres: "corres_underlying my_sr nf nf' rvrel P Q a c" 186 assumes my_adj: "\<And>s s'. (s,s') \<in> my_sr \<Longrightarrow> P s \<Longrightarrow> Q s'" 187 shows "corres_underlying my_sr nf nf' rvrel (\<lambda>s. P s \<and> P s) (\<lambda>s'. True) a c" 188 apply (rule my_corres[adj_corres my_adj]) 189 done 190 191end 192 193end 194