1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory WPC 8imports "WP_Pre" 9keywords "wpc_setup" :: thy_decl 10 11begin 12 13definition 14 wpc_helper :: "(('a \<Rightarrow> bool) \<times> 'b set) 15 \<Rightarrow> (('a \<Rightarrow> bool) \<times> 'b set) \<Rightarrow> bool \<Rightarrow> bool" where 16 "wpc_helper \<equiv> \<lambda>(P, P') (Q, Q') R. ((\<forall>s. P s \<longrightarrow> Q s) \<and> P' \<subseteq> Q') \<longrightarrow> R" 17 18lemma wpc_conj_process: 19 "\<lbrakk> wpc_helper (P, P') (A, A') C; wpc_helper (P, P') (B, B') D \<rbrakk> 20 \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. A s \<and> B s, A' \<inter> B') (C \<and> D)" 21 by (clarsimp simp add: wpc_helper_def) 22 23lemma wpc_all_process: 24 "\<lbrakk> \<And>x. wpc_helper (P, P') (Q x, Q' x) (R x) \<rbrakk> 25 \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. \<forall>x. Q x s, {s. \<forall>x. s \<in> Q' x}) (\<forall>x. R x)" 26 by (clarsimp simp: wpc_helper_def subset_iff) 27 28lemma wpc_all_process_very_weak: 29 "\<lbrakk> \<And>x. wpc_helper (P, P') (Q, Q') (R x) \<rbrakk> \<Longrightarrow> wpc_helper (P, P') (Q, Q') (\<forall>x. R x)" 30 by (clarsimp simp: wpc_helper_def) 31 32lemma wpc_imp_process: 33 "\<lbrakk> Q \<Longrightarrow> wpc_helper (P, P') (R, R') S \<rbrakk> 34 \<Longrightarrow> wpc_helper (P, P') (\<lambda>s. Q \<longrightarrow> R s, {s. Q \<longrightarrow> s \<in> R'}) (Q \<longrightarrow> S)" 35 by (clarsimp simp add: wpc_helper_def subset_iff) 36 37lemma wpc_imp_process_weak: 38 "\<lbrakk> wpc_helper (P, P') (R, R') S \<rbrakk> \<Longrightarrow> wpc_helper (P, P') (R, R') (Q \<longrightarrow> S)" 39 by (clarsimp simp add: wpc_helper_def) 40 41lemmas wpc_processors 42 = wpc_conj_process wpc_all_process wpc_imp_process 43lemmas wpc_weak_processors 44 = wpc_conj_process wpc_all_process wpc_imp_process_weak 45lemmas wpc_vweak_processors 46 = wpc_conj_process wpc_all_process_very_weak wpc_imp_process_weak 47 48lemma wpc_helperI: 49 "wpc_helper (P, P') (P, P') Q \<Longrightarrow> Q" 50 by (simp add: wpc_helper_def) 51 52lemma wpc_foo: "\<lbrakk> undefined x; False \<rbrakk> \<Longrightarrow> P x" 53 by simp 54 55lemma foo: 56 assumes foo_elim: "\<And>P Q h. \<lbrakk> foo Q h; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> foo P h" 57 shows 58 "\<lbrakk> \<And>x. foo (Q x) (f x); foo R g \<rbrakk> \<Longrightarrow> 59 foo (\<lambda>s. (\<forall>x. Q x s) \<and> (y = None \<longrightarrow> R s)) 60 (case y of Some x \<Rightarrow> f x | None \<Rightarrow> g)" 61 by (auto split: option.split intro: foo_elim) 62 63ML \<open> 64 65signature WPC = sig 66 exception WPCFailed of string * term list * thm list; 67 68 val foo_thm: thm; 69 val iffd2_thm: thm; 70 val wpc_helperI: thm; 71 72 val instantiate_concl_pred: Proof.context -> cterm -> thm -> thm; 73 74 val detect_term: Proof.context -> int -> thm -> cterm -> (cterm * term) list; 75 val detect_terms: Proof.context -> (term -> cterm -> thm -> int -> tactic) -> int -> tactic; 76 77 val split_term: thm list -> Proof.context -> term -> cterm -> thm -> int -> tactic; 78 79 val wp_cases_tac: thm list -> Proof.context -> int -> tactic; 80 val wp_debug_tac: thm list -> Proof.context -> int -> tactic; 81 val wp_cases_method: thm list -> (Proof.context -> Method.method) context_parser; 82 83end; 84 85structure WPCPredicateAndFinals = Theory_Data 86(struct 87 type T = (cterm * thm) list 88 val empty = [] 89 val extend = I 90 fun merge (xs, ys) = 91 (* Order of predicates is important, so we can't reorder *) 92 let val tms = map (Thm.term_of o fst) xs 93 fun inxs x = exists (fn y => x aconv y) tms 94 val ys' = filter (not o inxs o Thm.term_of o fst) ys 95 in 96 xs @ ys' 97 end 98end); 99 100structure WeakestPreCases : WPC = 101struct 102 103exception WPCFailed of string * term list * thm list; 104 105val iffd2_thm = @{thm "iffD2"}; 106val wpc_helperI = @{thm "wpc_helperI"}; 107val foo_thm = @{thm "wpc_foo"}; 108 109(* it looks like cterm_instantiate would do the job better, 110 but this handles the case where ?'a must be instantiated 111 to ?'a \<times> ?'b *) 112fun instantiate_concl_pred ctxt pred thm = 113let 114 val get_concl_pred = (fst o strip_comb o HOLogic.dest_Trueprop o Thm.concl_of); 115 val get_concl_predC = (Thm.cterm_of ctxt o get_concl_pred); 116 117 val get_pred_tvar = domain_type o Thm.typ_of o Thm.ctyp_of_cterm; 118 val thm_pred = get_concl_predC thm; 119 val thm_pred_tvar = Term.dest_TVar (get_pred_tvar thm_pred); 120 val pred_tvar = Thm.ctyp_of ctxt (get_pred_tvar pred); 121 122 val thm2 = Thm.instantiate ([(thm_pred_tvar, pred_tvar)], []) thm; 123 124 val thm2_pred = Term.dest_Var (get_concl_pred thm2); 125in 126 Thm.instantiate ([], [(thm2_pred, pred)]) thm2 127end; 128 129fun detect_term ctxt n thm tm = 130let 131 val foo_thm_tm = instantiate_concl_pred ctxt tm foo_thm; 132 val matches = resolve_tac ctxt [foo_thm_tm] n thm; 133 val outcomes = Seq.list_of matches; 134 val get_goalterm = (HOLogic.dest_Trueprop o Logic.strip_assums_concl 135 o Envir.beta_eta_contract o hd o Thm.prems_of); 136 val get_argument = hd o snd o strip_comb; 137in 138 map (pair tm o get_argument o get_goalterm) outcomes 139end; 140 141fun detect_terms ctxt tactic2 n thm = 142let 143 val pfs = WPCPredicateAndFinals.get (Proof_Context.theory_of ctxt); 144 val detects = map (fn (tm, rl) => (detect_term ctxt n thm tm, rl)) pfs; 145 val detects2 = filter (not o null o fst) detects; 146 val ((pred, arg), fin) = case detects2 of 147 [] => raise WPCFailed ("detect_terms: no match", [], [thm]) 148 | ((d3, fin) :: _) => (hd d3, fin) 149in 150 tactic2 arg pred fin n thm 151end; 152 153(* give each rule in the list one possible resolution outcome *) 154fun resolve_each_once_tac ctxt thms i 155 = fold (curry (APPEND')) 156 (map (DETERM oo resolve_tac ctxt o single) thms) 157 (K no_tac) i 158 159fun resolve_single_tac ctxt rules n thm = 160 case Seq.chop 2 (resolve_each_once_tac ctxt rules n thm) 161 of ([], _) => raise WPCFailed 162 ("resolve_single_tac: no rules could apply", 163 [], thm :: rules) 164 | (_ :: _ :: _, _) => raise WPCFailed 165 ("resolve_single_tac: multiple rules applied", 166 [], thm :: rules) 167 | ([x], _) => Seq.single x; 168 169fun split_term processors ctxt target pred fin = 170let 171 val hdTarget = head_of target; 172 val (constNm, _) = dest_Const hdTarget handle TERM (_, tms) 173 => raise WPCFailed ("split_term: couldn't dest_Const", tms, []); 174 val split = case (Ctr_Sugar.ctr_sugar_of_case ctxt constNm) of 175 SOME sugar => #split sugar 176 | _ => raise WPCFailed ("split_term: not a case", [hdTarget], []); 177 val subst = split RS iffd2_thm; 178 val subst2 = instantiate_concl_pred ctxt pred subst; 179in 180 (resolve_tac ctxt [subst2]) 181 THEN' 182 (resolve_tac ctxt [wpc_helperI]) 183 THEN' 184 (REPEAT_ALL_NEW (resolve_tac ctxt processors) 185 THEN_ALL_NEW 186 resolve_single_tac ctxt [fin]) 187end; 188 189(* n.b. need to concretise the lazy sequence via a list to ensure exceptions 190 have been raised already and catch them *) 191fun wp_cases_tac processors ctxt n thm = 192 detect_terms ctxt (split_term processors ctxt) n thm 193 |> Seq.list_of |> Seq.of_list 194 handle WPCFailed _ => no_tac thm; 195 196fun wp_debug_tac processors ctxt n thm = 197 detect_terms ctxt (split_term processors ctxt) n thm 198 |> Seq.list_of |> Seq.of_list 199 handle WPCFailed e => (warning (@{make_string} (WPCFailed e)); no_tac thm); 200 201fun wp_cases_method processors = Scan.succeed (fn ctxt => 202 Method.SIMPLE_METHOD' (wp_cases_tac processors ctxt)); 203 204local structure P = Parse and K = Keyword in 205 206fun add_wpc tm thm lthy = let 207 val ctxt = Local_Theory.target_of lthy 208 val tm' = (Syntax.read_term ctxt tm) |> Thm.cterm_of ctxt o Logic.varify_global 209 val thm' = Proof_Context.get_thm ctxt thm 210in 211 Local_Theory.background_theory (WPCPredicateAndFinals.map (fn xs => (tm', thm') :: xs)) lthy 212end; 213 214val _ = 215 Outer_Syntax.command 216 @{command_keyword "wpc_setup"} 217 "Add wpc stuff" 218 (P.term -- P.name >> (fn (tm, thm) => Toplevel.local_theory NONE NONE (add_wpc tm thm))) 219 220end; 221end; 222 223\<close> 224 225ML \<open> 226 227val wp_cases_tactic_weak = WeakestPreCases.wp_cases_tac @{thms wpc_weak_processors}; 228val wp_cases_method_strong = WeakestPreCases.wp_cases_method @{thms wpc_processors}; 229val wp_cases_method_weak = WeakestPreCases.wp_cases_method @{thms wpc_weak_processors}; 230val wp_cases_method_vweak = WeakestPreCases.wp_cases_method @{thms wpc_vweak_processors}; 231 232\<close> 233 234method_setup wpc0 = \<open>wp_cases_method_strong\<close> 235 "case splitter for weakest-precondition proofs" 236 237method_setup wpcw0 = \<open>wp_cases_method_weak\<close> 238 "weak-form case splitter for weakest-precondition proofs" 239 240method wpc = (wp_pre, wpc0) 241method wpcw = (wp_pre, wpcw0) 242 243definition 244 wpc_test :: "'a set \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'b set \<Rightarrow> bool" 245 where 246 "wpc_test P R S \<equiv> (R `` P) \<subseteq> S" 247 248lemma wpc_test_weaken: 249 "\<lbrakk> wpc_test Q R S; P \<subseteq> Q \<rbrakk> \<Longrightarrow> wpc_test P R S" 250 by (simp add: wpc_test_def, blast) 251 252lemma wpc_helper_validF: 253 "wpc_test Q' R S \<Longrightarrow> wpc_helper (P, P') (Q, Q') (wpc_test P' R S)" 254 by (simp add: wpc_test_def wpc_helper_def, blast) 255 256setup \<open> 257let 258 val tm = Thm.cterm_of @{context} (Logic.varify_global @{term "\<lambda>R. wpc_test P R S"}); 259 val thm = @{thm wpc_helper_validF}; 260in 261 WPCPredicateAndFinals.map (fn xs => (tm, thm) :: xs) 262end 263\<close> 264 265lemma set_conj_Int_simp: 266 "{s \<in> S. P s} = S \<inter> {s. P s}" 267 by auto 268 269lemma case_options_weak_wp: 270 "\<lbrakk> wpc_test P R S; \<And>x. wpc_test P' (R' x) S \<rbrakk> 271 \<Longrightarrow> wpc_test (P \<inter> P') (case opt of None \<Rightarrow> R | Some x \<Rightarrow> R' x) S" 272 apply (rule wpc_test_weaken) 273 apply wpcw 274 apply assumption 275 apply assumption 276 apply simp 277 done 278 279 280end 281