1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6theory WPFix 7 8imports 9 Datatype_Schematic 10 Strengthen 11 12begin 13 14text \<open> 15WPFix handles four issues which are annoying with precondition schematics: 16 1. Schematics in obligation (postcondition) positions which remain unset 17after goals are solved. They should be instantiated to True. 18 2. Schematics which appear in multiple precondition positions. They should 19be instantiated to a conjunction and then separated. 20 3/4. Schematics applied to datatype expressions such as @{term True} or 21@{term "Some x"}. See @{theory "Lib.Datatype_Schematic"} for details. 22\<close> 23 24lemma use_strengthen_prop_intro: 25 "PROP P \<Longrightarrow> PROP (strengthen_implementation.st_prop1 (PROP Q) (PROP P)) 26 \<Longrightarrow> PROP Q" 27 unfolding strengthen_implementation.st_prop1_def 28 apply (drule(1) meta_mp)+ 29 apply assumption 30 done 31 32definition 33 target_var :: "int \<Rightarrow> 'a \<Rightarrow> 'a" 34where 35 "target_var n x = x" 36 37lemma strengthen_to_conjunct1_target: 38 "strengthen_implementation.st True (\<longrightarrow>) 39 (target_var n (P \<and> Q)) (target_var n P)" 40 by (simp add: strengthen_implementation.st_def target_var_def) 41 42lemma strengthen_to_conjunct2_target_trans: 43 "strengthen_implementation.st True (\<longrightarrow>) 44 (target_var n Q) R 45 \<Longrightarrow> strengthen_implementation.st True (\<longrightarrow>) 46 (target_var n (P \<and> Q)) R" 47 by (simp add: strengthen_implementation.st_def target_var_def) 48 49lemma target_var_drop_func: 50 "target_var n f = (\<lambda>x. target_var n (f x))" 51 by (simp add: target_var_def) 52 53named_theorems wp_fix_strgs 54 55lemma strg_target_to_true: 56 "strengthen_implementation.st F (\<longrightarrow>) (target_var n True) True" 57 by (simp add: target_var_def strengthen_implementation.strengthen_refl) 58 59ML \<open> 60structure WPFix = struct 61 62val st_refl = @{thm strengthen_implementation.strengthen_refl} 63val st_refl_True = @{thm strengthen_implementation.strengthen_refl[where x=True]} 64val st_refl_target_True = @{thm strg_target_to_true} 65val st_refl_non_target 66 = @{thm strengthen_implementation.strengthen_refl[where x="target_var (-1) v" for v]} 67 68val conv_to_target = mk_meta_eq @{thm target_var_def[symmetric]} 69 70val tord = Term_Ord.fast_term_ord 71fun has_var vars t = not (null (Ord_List.inter tord vars 72 (Ord_List.make tord (map Var (Term.add_vars t []))))) 73 74fun get_vars prop = map Var (Term.add_vars prop []) 75 |> Ord_List.make tord 76 |> filter (fn v => snd (strip_type (fastype_of v)) = HOLogic.boolT) 77 78val st_intro = @{thm use_strengthen_prop_intro} 79val st_not = @{thms strengthen_implementation.strengthen_Not} 80val st_conj2_trans = @{thm strengthen_to_conjunct2_target_trans} 81val st_conj1 = @{thm strengthen_to_conjunct1_target} 82 83(* assumes Strengthen.goal_predicate g is "st" *) 84fun dest_strg g = case Strengthen.goal_predicate g of 85 "st" => (case HOLogic.dest_Trueprop (Logic.strip_assums_concl g) of 86 (Const _ $ mode $ rel $ lhs $ rhs) => ("st", SOME (mode, rel, lhs, rhs)) 87 | _ => error ("dest_strg " ^ @{make_string} g) 88 ) 89 | nm => (nm, NONE) 90 91fun get_target (Const (@{const_name target_var}, _) $ n $ _) 92 = (try (HOLogic.dest_number #> snd) n) 93 | get_target _ = NONE 94 95fun is_target P t = case get_target t of NONE => false 96 | SOME v => P v 97 98fun is_target_head P (f $ v) = is_target P (f $ v) orelse is_target_head P f 99 | is_target_head _ _ = false 100 101fun has_target P (f $ v) = is_target P (f $ v) 102 orelse has_target P f orelse has_target P v 103 | has_target P (Abs (_, _, t)) = has_target P t 104 | has_target _ _ = false 105 106fun apply_strgs congs ctxt = SUBGOAL (fn (t, i) => case 107 dest_strg t of 108 ("st_prop1", _) => resolve_tac ctxt congs i 109 | ("st_prop2", _) => resolve_tac ctxt congs i 110 | ("st", SOME (_, _, lhs, _)) => resolve_tac ctxt st_not i 111 ORELSE eresolve_tac ctxt [thin_rl] i 112 ORELSE resolve_tac ctxt [st_refl_non_target] i 113 ORELSE (if is_target_head (fn v => v >= 0) lhs 114 then no_tac 115 else if not (has_target (fn v => v >= 0) lhs) 116 then resolve_tac ctxt [st_refl] i 117 else if is_Const (head_of lhs) 118 then (resolve_tac ctxt congs i ORELSE resolve_tac ctxt [st_refl] i) 119 else resolve_tac ctxt [st_refl] i 120 ) 121 | _ => no_tac 122 ) 123 124fun strg_proc ctxt = let 125 val congs1 = Named_Theorems.get ctxt @{named_theorems wp_fix_strgs} 126 val thy = Proof_Context.theory_of ctxt 127 val congs2 = Strengthen.Congs.get thy 128 val strg = apply_strgs (congs1 @ congs2) ctxt 129 in REPEAT_ALL_NEW strg end 130 131fun target_var_conv vars ctxt ct = case Thm.term_of ct of 132 Abs _ => Conv.sub_conv (target_var_conv vars) ctxt ct 133 | Var v => Conv.rewr_conv (Drule.infer_instantiate ctxt 134 [(("n", 1), Thm.cterm_of ctxt (HOLogic.mk_number @{typ int} 135 (find_index (fn v2 => v2 = Var v) vars)))] conv_to_target) ct 136 | _ $ _ => Datatype_Schematic.combs_conv (target_var_conv vars) ctxt ct 137 | _ => raise Option 138 139fun st_intro_tac ctxt = CSUBGOAL (fn (ct, i) => fn thm => let 140 val intro = Drule.infer_instantiate ctxt [(("Q", 0), ct)] 141 (Thm.incr_indexes (Thm.maxidx_of thm + 1) st_intro) 142 in compose_tac ctxt (false, intro, 2) i 143 end thm) 144 145fun intro_tac ctxt vs = SUBGOAL (fn (t, i) => if has_var vs t 146 then CONVERSION (target_var_conv vs ctxt) i 147 THEN CONVERSION (Simplifier.full_rewrite (clear_simpset ctxt 148 addsimps @{thms target_var_drop_func} 149 )) i 150 THEN st_intro_tac ctxt i 151 else all_tac) 152 153fun classify v thm = let 154 val has_t = has_target (fn v' => v' = v) 155 val relevant = filter (has_t o fst) 156 (Thm.prems_of thm ~~ (1 upto Thm.nprems_of thm)) 157 |> map (apfst (Logic.strip_assums_concl #> Envir.beta_eta_contract)) 158 fun class t = case dest_strg t of 159 ("st", SOME (@{term True}, @{term "(-->)"}, lhs, _)) 160 => if has_t lhs then SOME true else NONE 161 | ("st", SOME (@{term False}, @{term "(-->)"}, lhs, _)) 162 => if has_t lhs then SOME false else NONE 163 | _ => NONE 164 val classn = map (apfst class) relevant 165 fun get k = map snd (filter (fn (k', _) => k' = k) classn) 166 in if (null relevant) then NONE 167 else if not (null (get NONE)) 168 then NONE 169 else if null (get (SOME true)) 170 then SOME ("to_true", map snd relevant) 171 else if length (get (SOME true)) > 1 172 then SOME ("to_conj", get (SOME true)) 173 else NONE 174 end 175 176fun ONGOALS tac is = let 177 val is = rev (sort int_ord is) 178 in EVERY (map tac is) end 179 180fun act_on ctxt ("to_true", is) 181 = ONGOALS (resolve_tac ctxt [st_refl_target_True]) is 182 | act_on ctxt ("to_conj", is) 183 = ONGOALS (resolve_tac ctxt [st_conj2_trans]) (drop 1 is) 184 THEN (if length is > 2 then act_on ctxt ("to_conj", drop 1 is) 185 else ONGOALS (resolve_tac ctxt [st_refl]) (drop 1 is)) 186 THEN ONGOALS (resolve_tac ctxt [st_conj1]) (take 1 is) 187 | act_on _ (s, _) = error ("act_on: " ^ s) 188 189fun act ctxt check vs thm = let 190 val acts = map_filter (fn v => classify v thm) vs 191 in if null acts 192 then (if check then no_tac else all_tac) thm 193 else (act_on ctxt (hd acts) THEN act ctxt false vs) thm end 194 195fun cleanup ctxt = SUBGOAL (fn (t, i) => case Strengthen.goal_predicate t of 196 "st" => resolve_tac ctxt [st_refl] i 197 | _ => all_tac) 198 199fun tac ctxt = SUBGOAL (fn (t, _) => let 200 val vs = get_vars t 201 in if null vs then no_tac else ALLGOALS (intro_tac ctxt vs) 202 THEN ALLGOALS (TRY o strg_proc ctxt) 203 THEN act ctxt true (0 upto (length vs - 1)) 204 THEN ALLGOALS (cleanup ctxt) 205 THEN Local_Defs.unfold_tac ctxt @{thms target_var_def} 206 end) 207 208fun both_tac ctxt = (Datatype_Schematic.tac ctxt THEN' (TRY o tac ctxt)) 209 ORELSE' tac ctxt 210 211val method = 212 Method.sections [Datatype_Schematic.add_section] >> 213 (fn _ => fn ctxt => Method.SIMPLE_METHOD' (both_tac ctxt)); 214 215end 216\<close> 217 218method_setup wpfix = \<open>WPFix.method\<close> 219 220lemma demo1: 221 "(\<exists>Ia Ib Ic Id Ra. 222 (Ia (Suc 0) \<longrightarrow> Qa) 223 \<and> (Ib \<longrightarrow> Qb) 224 \<and> (Ic \<longrightarrow> Ra) 225 \<and> (Id \<longrightarrow> Qc) 226 \<and> (Id \<longrightarrow> Qd) 227 \<and> (Qa \<and> Qb \<and> Qc \<and> Qd \<longrightarrow> Ia v \<and> Ib \<and> Ic \<and> Id))" 228 apply (intro exI conjI impI) 229 (* apply assumption+ won't work here, since it will pick Id 230 incorrectly. the presence of the goal ?Ra is also dangerous. 231 wpfix handles this by setting Ra to True and splitting 232 Id into a conjunction. *) 233 apply (wpfix | assumption)+ 234 apply auto 235 done 236 237lemma demo2: 238 assumes P: "\<And>x. P (x + Suc x) \<longrightarrow> R (Inl x)" 239 "\<And>x. P ((x * 2) - 1) \<longrightarrow> R (Inr x)" 240 assumes P17: "P 17" 241 shows "\<exists>I. I (Some 9) 242 \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y))) 243 \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1))))" 244 apply (intro exI conjI[rotated] allI) 245 apply (case_tac x; simp) 246 apply wpfix 247 apply (rule P) 248 apply wpfix 249 apply (rule P) 250 apply (case_tac x; simp) 251 apply wpfix 252 apply (rule P) 253 apply wpfix 254 apply (rule P) 255 apply (simp add: P17) 256 done 257 258\<comment> \<open> 259 Shows how to use @{attribute datatype_schematic} rules as "accessors". 260\<close> 261lemma (in datatype_schem_demo) demo3: 262 "\<exists>x. \<forall>a b. x (basic a b) = a" 263 apply (rule exI, (rule allI)+) 264 apply (wpfix add: get_basic_0.simps) \<comment> \<open>Only exposes `a` to the schematic.\<close> 265 by (rule refl) 266 267end 268