1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* 8What is crunch? Crunch is for proving easily proved properties over various 9functions within a (shallow monadic) specification. Suppose we have a toplevel 10specification function f and some simple notion of correctness, P \<turnstile> f, which 11we want to prove. However f is defined in terms of subfunctions g etc. 12To prove P \<turnstile> f, we will first show many lemmas P \<turnstile> g, which crunch lets us 13do easily. 14 15As a first step, crunch must discover "crunch rules" which structure the proof. 16For instance, if f is a constant with a definition, crunch may discover the 17definition "f == f_body" and derive the crunch rule "P \<turnstile> f_body \<Longrightarrow> P \<turnstile> f". 18A crunch rule will be used if all its premises are either proofs of the 19same notion of correctness (P \<turnstile> ?f) or can be solved trivially by wp/simp. 20 21The user can supply crunch rules with the rule: section or crunch_rule 22attribute, which will be tried both as rewrites and 23as introduction rules. Crunch also has a number of builtin strategies 24for finding definitional rules in the context. 25 26Once a crunch rule for P \<turnstile> f is found, crunch will recursively apply to 27almost all monadic constants in all of the premises. (The exploration 28terminates where crunch rules can be found without premises.) Crunch 29will obtain proofs e.g. P \<turnstile> g for all f's dependencies, then finally 30try to prove P \<turnstile> f using the crunch rule, wp (with the given dependencies) 31and simp. Additional wp and simp rules can also be given with the wp: and 32simp: sections. 33 34When obtaining proofs for f's dependencies, crunch will first determine 35whether a rule already exists for that goal (P \<turnstile> g). It does this by 36checking whether a) crunch has already proven a rule for that constant, 37b) a rule in the wp set can be used to solve the goal, or c) a rule 38already exists with the name that crunch would use. In the case of c), 39crunch will fail if the found rule cannot be applied to the goal. 40 41There are some monadic constants that it does not make sense to apply 42crunch to. These are added to a crunch_ignore set, and are removed from 43f's dependencies if they are ever found. The command crunch_ignore (add: ) 44can be used to add new constants, along with the ignore: section of a 45specific crunch invocation. 46 47*) 48 49(* Tracing debug. *) 50val crunch_debug = Unsynchronized.ref false 51fun debug_trace_pf pref f = 52 if (!crunch_debug) then 53 tracing (pref ^ f ()) 54 else 55 () 56fun debug_trace s = 57 if (!crunch_debug) then 58 tracing s 59 else 60 () 61fun debug_trace_bl bl = 62 if (!crunch_debug) then 63 tracing (Pretty.string_of (Pretty.block 64 (map (fn f => f ()) bl))) 65 else 66 () 67 68fun funkysplit [_,b,c] = [b,c] 69 | funkysplit [_,c] = [c] 70 | funkysplit l = l 71 72fun real_base_name name = name |> Long_Name.explode |> funkysplit |> Long_Name.implode (*Handles locales properly-ish*) 73 74fun handle_int exn func = if Exn.is_interrupt exn then Exn.reraise exn else func 75 76val Thm : (Facts.ref * Token.src list) -> ((Facts.ref * Token.src list), xstring) sum = Inl 77val Constant : xstring -> ((Facts.ref * Token.src list), xstring) sum = Inr 78val thms = lefts 79val constants = rights 80 81val wp_sect = ("wp", Parse.thm >> Thm); 82val wp_del_sect = ("wp_del", Parse.thm >> Thm); 83val wps_sect = ("wps", Parse.thm >> Thm); 84val ignore_sect = ("ignore", Parse.const >> Constant); 85val ignore_del_sect = ("ignore_del", Parse.const >> Constant); 86val simp_sect = ("simp", Parse.thm >> Thm); 87val simp_del_sect = ("simp_del", Parse.thm >> Thm); 88val rule_sect = ("rule", Parse.thm >> Thm); 89val rule_del_sect = ("rule_del", Parse.thm >> Thm); 90 91fun read_const ctxt = Proof_Context.read_const {proper = true, strict = false} ctxt; 92 93fun gen_term_eq (f $ x, f' $ x') = gen_term_eq (f, f') andalso gen_term_eq (x, x') 94 | gen_term_eq (Abs (_, _, t), Abs (_, _, t')) = gen_term_eq (t, t') 95 | gen_term_eq (Const (nm, _), Const (nm', _)) = (nm = nm') 96 | gen_term_eq (Free (nm, _), Free (nm', _)) = (nm = nm') 97 | gen_term_eq (Var (nm, _), Var (nm', _)) = (nm = nm') 98 | gen_term_eq (Bound i, Bound j) = (i = j) 99 | gen_term_eq _ = false 100fun ae_conv (t, t') = gen_term_eq 101 (Envir.beta_eta_contract t, Envir.beta_eta_contract t') 102 103(* 104Crunch can be instantiated to prove different properties about monadic 105specifications. For several examples of this instantiation see 106Crunch_Instances_NonDet. 107*) 108signature CrunchInstance = 109sig 110 (* The name of the property. *) 111 val name : string; 112 (* The type of any parameters of the property beyond a (optional) precondition 113 and the function being crunched. *) 114 type extra; 115 (* Equality of the extra parameter, often uses ae_conv. *) 116 val eq_extra : extra * extra -> bool; 117 (* How to parse anything after the list of specifications to be crunched, 118 returns a precondition and extra field. *) 119 val parse_extra : Proof.context -> string -> term * extra; 120 (* Whether the property has preconditions. *) 121 val has_preconds : bool; 122 (* Construct the property out of a precondition, function and extra. *) 123 val mk_term : term -> term -> extra -> term; 124 (* Deconstruct the property. *) 125 val dest_term : term -> (term * term * extra) option; 126 (* Put a new precondition into an instance of the property. *) 127 val put_precond : term -> term -> term; 128 (* Theorems used to modify the precondition of the property. An empty list 129 if the property has no preconditions. *) 130 val pre_thms : thm list; 131 (* The wpc_tactic used, normally wp_cases_tactic_weak. See BCorres_UL for 132 an alternative. *) 133 val wpc_tactic : Proof.context -> int -> tactic; 134 (* The wps_tactic used, normally wps_tac when applicable and no_tac when not. *) 135 val wps_tactic : Proof.context -> thm list -> int -> tactic; 136 val magic : term; 137 (* Get the type of the state a monadic specification is operating on. Returns 138 NONE when given the wrong type. See get_nondet_monad_state_type in 139 Crunch_Instances_NonDet for an example. *) 140 val get_monad_state_type : typ -> typ option 141end 142 143signature CRUNCH = 144sig 145 type extra; 146 (* Crunch configuration: theory, naming scheme, name space, wp rules, wps_rules, 147 constants to ignore, simp rules, constants to not ignore, unfold rules*) 148 type crunch_cfg = {ctxt: local_theory, prp_name: string, nmspce: string option, 149 wp_rules: (string * thm) list, wps_rules: thm list, igs: string list, simps: thm list, 150 ig_dels: string list, rules: thm list}; 151 152 (* Crunch takes a configuration, a precondition, any extra information needed, a debug stack, 153 a constant name, and a list of previously proven theorems, and returns a theorem for 154 this constant and a list of new theorems (which may be empty if the result 155 had already been proven). *) 156 val crunch : 157 crunch_cfg -> term -> extra -> string list -> string 158 -> (string * thm) list -> (thm option * (string * thm) list); 159 160 val crunch_x : Token.src list -> string -> string 161 -> (string * ((Facts.ref * Token.src list), xstring) sum) list 162 -> string list -> local_theory -> local_theory; 163 164 val crunch_ignore_add_del : string list -> string list -> theory -> theory 165 166 val mism_term_trace : (term * extra) list Unsynchronized.ref 167end 168 169functor Crunch (Instance : CrunchInstance) = 170struct 171 172type extra = Instance.extra; 173 174type crunch_cfg = {ctxt: local_theory, prp_name: string, nmspce: string option, 175 wp_rules: (string * thm) list, wps_rules: thm list, igs: string list, simps: thm list, 176 ig_dels: string list, rules: thm list}; 177 178structure CrunchIgnore = Theory_Data 179(struct 180 type T = string list 181 val empty = [] 182 val extend = I 183 val merge = Library.merge (op =); 184end); 185 186fun crunch_ignore_add thms thy = 187 CrunchIgnore.map (curry (Library.merge (op =)) thms) thy 188 189fun crunch_ignore_del thms thy = 190 CrunchIgnore.map (Library.subtract (op =) thms) thy 191 192fun crunch_ignore_add_del adds dels = 193 crunch_ignore_add adds #> crunch_ignore_del dels 194 195fun crunch_ignores cfg ctxt = 196 subtract (op =) (#ig_dels cfg) (#igs cfg @ CrunchIgnore.get (Proof_Context.theory_of ctxt)) 197 198val def_sfx = "_def"; 199val induct_sfx = ".induct"; 200val simps_sfx = ".simps"; 201val param_name = "param_a"; 202val dummy_monad_name = "__dummy__"; 203 204fun def_of n = n ^ def_sfx; 205fun induct_of n = n ^ induct_sfx; 206fun simps_of n = n ^ simps_sfx; 207 208fun num_args t = length (binder_types t) - 1; 209 210fun real_const_from_name const nmspce ctxt = 211 let 212 val qual::locale::nm::nil = Long_Name.explode const; 213 val SOME some_nmspce = nmspce; 214 val nm = Long_Name.implode (some_nmspce :: nm :: nil); 215 val _ = read_const ctxt nm; 216 in 217 nm 218 end 219 handle exn => handle_int exn const; 220 221 222fun get_monad ctxt f xs = if is_Const f then 223 (* we need the type of the underlying constant to avoid polymorphic 224 constants like If, case_option, K_bind being considered monadic *) 225 let val T = dest_Const f |> fst |> read_const ctxt |> type_of; 226 227 fun is_product v p = 228 Option.getOpt (Option.map (fn v' => v = v') (Instance.get_monad_state_type p), 229 false) 230 231 fun num_args (Type ("fun", [v,p])) n = 232 if is_product v p then SOME n else num_args p (n + 1) 233 | num_args _ _ = NONE 234 235 in case num_args T 0 of NONE => [] 236 | SOME n => [list_comb (f, Library.take n (xs @ map Bound (1 upto n)))] 237 end 238 else []; 239 240fun monads_of ctxt t = case strip_comb t of 241 (Const f, xs) => get_monad ctxt (Const f) xs @ maps (monads_of ctxt) xs 242 | (Abs (_, _, t), []) => monads_of ctxt t 243 | (Abs a, xs) => monads_of ctxt (betapplys (Abs a, xs)) 244 | (_, xs) => maps (monads_of ctxt) xs; 245 246 247val get_thm = Proof_Context.get_thm 248 249val get_thms = Proof_Context.get_thms 250 251val get_thms_from_facts = Attrib.eval_thms 252 253fun maybe_thms thy name = get_thms thy name handle ERROR _ => [] 254fun thy_maybe_thms thy name = Global_Theory.get_thms thy name handle ERROR _ => [] 255 256fun add_thm thm atts name ctxt = 257 Local_Theory.notes [((Binding.name name, atts), [([thm], atts)])] ctxt |> #2 258 259fun get_thm_name (cfg : crunch_cfg) const_name 260 = if read_const (#ctxt cfg) (Long_Name.base_name const_name) 261 = read_const (#ctxt cfg) const_name 262 then Long_Name.base_name const_name ^ "_" ^ (#prp_name cfg) 263 else space_implode "_" (space_explode "." const_name @ [#prp_name cfg]) 264 265fun get_stored cfg n = get_thm (#ctxt cfg) (get_thm_name cfg n) 266 267fun mapM _ [] y = y 268 | mapM f (x::xs) y = mapM f xs (f x y) 269 270fun dest_equals t = t |> Logic.dest_equals 271 handle TERM _ => t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq; 272 273fun const_is_lhs const nmspce ctxt def = 274 let 275 val (lhs, _) = def |> Thm.prop_of |> dest_equals; 276 val (nm, _) = dest_Const const; 277 val (nm', _) = dest_Const (head_of lhs); 278 in 279 (real_const_from_name nm nmspce ctxt) = (real_const_from_name nm' nmspce ctxt) 280 end handle TERM _ => false 281 282fun deep_search_thms ctxt defn const nmspce = 283 let 284 val thy = Proof_Context.theory_of ctxt 285 val thys = thy :: Theory.ancestors_of thy; 286 val filt = filter (const_is_lhs const nmspce ctxt); 287 288 fun search [] = error("not found: const: " ^ @{make_string} const ^ " defn: " ^ @{make_string} defn) 289 | search (t::ts) = (case (filt (thy_maybe_thms t defn)) of 290 [] => search ts 291 | thms => thms); 292 in 293 case filt (maybe_thms ctxt defn) of 294 [] => search thys 295 | defs => defs 296 end; 297 298(* 299When making recursive crunch calls we want to identify and collect preconditions 300about parameters of the functions we are crunching. To assist with this we 301attempt to turn bound variables into free variables by simplifying with rules 302like Let_def, return_bind and bind_assoc. One example of this named_theorem 303being populated can be found in Crunch_Instances_NonDet. 304*) 305fun unfold_get_params ctxt = 306 Named_Theorems.get ctxt @{named_theorems crunch_param_rules} 307 308fun def_from_ctxt ctxt const = 309 let 310 val crunch_defs = Named_Theorems.get ctxt @{named_theorems crunch_def} 311 val abs_def = Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def; 312 fun do_filter thm = 313 try (abs_def #> Thm.prop_of #> Logic.dest_equals #> fst #> dest_Const #> fst) thm 314 = SOME const 315 in 316 case crunch_defs |> filter do_filter of 317 [x] => SOME x 318 | [] => NONE 319 | _ => raise Fail ("Multiple definitions declared for:" ^ const) 320 end 321 322fun unfold ctxt const triple nmspce = 323 let 324 val _ = debug_trace "unfold" 325 val const_term = read_const ctxt const; 326 val const_defn = const |> Long_Name.base_name |> def_of; 327 val const_def = deep_search_thms ctxt const_defn const_term nmspce 328 |> hd |> Simpdata.safe_mk_meta_eq; 329 val _ = debug_trace_bl [K (Pretty.str "const_def:"), 330 fn () => Pretty.str (@{make_string} const_defn), fn () => Thm.pretty_thm ctxt const_def] 331 val trivial_rule = Thm.trivial triple 332 val _ = debug_trace_bl [K (Pretty.str "trivial_rule :"), 333 fn () => Thm.pretty_thm ctxt trivial_rule] 334 val unfold_rule = trivial_rule 335 |> Simplifier.rewrite_goals_rule ctxt [const_def]; 336 val _ = debug_trace_bl [K (Pretty.str "unfold_rule :"), 337 fn () => Thm.pretty_thm ctxt unfold_rule] 338 val ms = unfold_rule 339 |> Simplifier.rewrite_goals_rule ctxt (unfold_get_params ctxt) 340 |> Thm.prems_of |> maps (monads_of ctxt); 341 in if Thm.eq_thm_prop (trivial_rule, unfold_rule) 342 then error ("Unfold rule generated for " ^ const ^ " does not apply") 343 else (ms, unfold_rule) end 344 345fun mk_apps t n m = 346 if n = 0 347 then t 348 else mk_apps t (n-1) (m+1) $ Bound m 349 350fun mk_abs t n = 351 if n = 0 352 then t 353 else Abs ("_", dummyT, mk_abs t (n-1)) 354 355fun eq_cname (Const (s, _)) (Const (t, _)) = (s = t) 356 | eq_cname _ _ = false 357 358fun resolve_abbreviated ctxt abbrev = 359 let 360 val (abbrevn,_) = dest_Const abbrev 361 val origin = (head_of (snd ((Consts.the_abbreviation o Proof_Context.consts_of) ctxt abbrevn))); 362 val (originn,_) = dest_Const origin; 363 val (_::_::_::nil) = Long_Name.explode originn; 364 in origin end handle exn => handle_int exn abbrev 365 366fun map_consts f = 367 let 368 fun map_aux (Const a) = f (Const a) 369 | map_aux (t $ u) = map_aux t $ map_aux u 370 | map_aux x = x 371 in map_aux end; 372 373fun map_unvarifyT t = map_types Logic.unvarifyT_global t 374 375fun dummy_fix ctxt vars = let 376 val nns = Name.invent Name.context "dummy_var_a" (length vars) 377 val frees = map Free (nns ~~ map fastype_of vars) 378 |> map (Thm.cterm_of ctxt) 379 in Drule.infer_instantiate ctxt (map (fst o dest_Var) vars ~~ frees) end 380 381fun induct_inst ctxt const goal nmspce = 382 let 383 val _ = debug_trace "induct_inst" 384 val base_const = Long_Name.base_name const; 385 val _ = debug_trace_pf "base_const: " (fn () => @{make_string} base_const) 386 val induct_thm = base_const |> induct_of |> get_thm ctxt; 387 val _ = debug_trace_pf "induct_thm: " (fn () => @{make_string} induct_thm) 388 val act_goal = HOLogic.dest_Trueprop (Thm.term_of goal) 389 val goal_f = case Instance.dest_term act_goal of 390 NONE => (warning "induct_inst: dest_term failed"; error "induct_inst: dest_term failed") 391 | SOME (_, goal_f, _) => goal_f 392 val params = map_filter (fn Free (s, _) => 393 (if String.isPrefix "param" s then SOME s else NONE) | _ => NONE) 394 (snd (strip_comb goal_f)) 395 val _ = debug_trace ("induct_inst params: " ^ commas params) 396 val induct_thm_params = induct_thm |> Thm.concl_of 397 |> HOLogic.dest_Trueprop |> strip_comb |> snd 398 val induct_thm_inst = dummy_fix ctxt (drop (length params) induct_thm_params) induct_thm 399 val trivial_rule = Thm.trivial goal; 400 val tac = Induct_Tacs.induct_tac ctxt [map SOME params] (SOME [induct_thm_inst]) 1 401 val induct_inst = tac trivial_rule |> Seq.hd 402 val _ = debug_trace_pf "induct_inst: " (fn () => Syntax.string_of_term ctxt (Thm.prop_of induct_inst)) 403 val simp_thms = deep_search_thms ctxt (base_const |> simps_of) (head_of goal_f) nmspce; 404 val induct_inst_simplified = induct_inst 405 |> Simplifier.rewrite_goals_rule ctxt (map Simpdata.safe_mk_meta_eq simp_thms); 406 val ms = maps (monads_of ctxt) (Thm.prems_of induct_inst_simplified); 407 val ms' = filter_out (eq_cname (resolve_abbreviated ctxt (head_of goal_f)) o head_of) ms; 408 in if Thm.eq_thm_prop (trivial_rule, induct_inst) 409 then error ("Unfold rule generated for " ^ const ^ " does not apply") 410 else (ms', induct_inst_simplified) end 411 412fun unfold_data ctxt constn goal nmspce NONE = ( 413 induct_inst ctxt constn goal nmspce handle exn => handle_int exn 414 unfold ctxt constn goal nmspce handle exn => handle_int exn 415 error ("unfold_data: couldn't find defn or induct rule for " ^ constn)) 416 | unfold_data ctxt constn goal _ (SOME thm) = 417 let 418 val trivial_rule = Thm.trivial goal 419 val unfold_rule = Simplifier.rewrite_goals_rule ctxt [safe_mk_meta_eq thm] trivial_rule; 420 val ms = unfold_rule 421 |> Simplifier.rewrite_goals_rule ctxt (unfold_get_params ctxt) 422 |> Thm.prems_of |> maps (monads_of ctxt); 423 in if Thm.eq_thm_prop (trivial_rule, unfold_rule) 424 then error ("Unfold rule given for " ^ constn ^ " does not apply") 425 else (ms, unfold_rule) end 426 427fun get_unfold_rule ctxt const cgoal namespace = 428 unfold_data ctxt const cgoal namespace (def_from_ctxt ctxt const) 429 430val split_if = @{thm "if_split"} 431 432fun maybe_cheat_tac ctxt thm = 433 if (Goal.skip_proofs_enabled ()) 434 then ALLGOALS (Skip_Proof.cheat_tac ctxt) thm 435 else all_tac thm; 436 437fun get_precond t = 438 if Instance.has_preconds 439 then case Instance.dest_term t of 440 SOME (pre, _, _) => pre 441 | _ => error ("get_precond: not a " ^ Instance.name ^ " term") 442 else error ("crunch (" ^ Instance.name ^ ") should not be calling get_precond") 443 444fun var_precond v = 445 if Instance.has_preconds 446 then Instance.put_precond (Var (("Precond", 0), get_precond v |> fastype_of)) v 447 else v; 448 449fun is_proof_of cfg const (name, _) = 450 get_thm_name cfg const = name 451 452fun get_inst_precond ctxt pre extra (mapply, goal) = let 453 val (c, xs) = strip_comb mapply; 454 fun replace_vars (t, n) = 455 if exists_subterm (fn t => is_Bound t orelse is_Var t) t 456 then Free ("ignore_me" ^ string_of_int n, dummyT) 457 else t 458 val ys = map replace_vars (xs ~~ (1 upto (length xs))); 459 val goal2 = Instance.mk_term pre (list_comb (c, ys)) extra 460 |> Syntax.check_term ctxt |> var_precond 461 |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt; 462 val spec = goal RS Thm.trivial goal2; 463 val precond = Thm.concl_of spec |> HOLogic.dest_Trueprop |> get_precond; 464 in SOME precond end 465 (* in rare cases the tuple extracted from the naming scheme doesn't 466 match what we were trying to prove, thus a THM exception from RS *) 467 handle THM _ => NONE; 468 469fun split_precond (Const (@{const_name pred_conj}, _) $ P $ Q) 470 = split_precond P @ split_precond Q 471 | split_precond (Abs (n, T, @{const "HOL.conj"} $ P $ Q)) 472 = maps (split_precond o Envir.eta_contract) [Abs (n, T, P), Abs (n, T, Q)] 473 | split_precond t = [t]; 474 475val precond_implication_term 476 = Syntax.parse_term @{context} 477 "%P Q. (!! s. (P s ==> Q s))"; 478 479fun precond_needed ctxt pre css pre' = let 480 val imp = Syntax.check_term ctxt (precond_implication_term $ pre $ pre'); 481 in not (can (Goal.prove ctxt [] [] imp) 482 (fn _ => clarsimp_tac css 1)) end 483 484fun combine_preconds ctxt pre pres = let 485 val pres' = maps (split_precond o Envir.beta_eta_contract) pres 486 |> filter_out (exists_subterm (fn t => is_Var t orelse 487 (is_Free t andalso 488 is_prefix (op =) (String.explode "ignore_me") 489 (String.explode (fst (dest_Free t)))))) 490 |> remove (op aconv) pre |> distinct (op aconv) 491 |> filter (precond_needed ctxt pre ctxt); 492 val T = fastype_of pre; 493 val conj = Const (@{const_name pred_conj}, T --> T --> T) 494 in case pres' of 495 [] => pre 496 | _ => let val precond = foldl1 (fn (a, b) => conj $ a $ b) pres' 497 in if precond_needed ctxt precond ctxt pre then conj $ pre $ precond else precond end 498 end; 499 500(* the crunch function is designed to be foldable with this custom fold 501 to crunch over a list of constants *) 502fun funkyfold _ [] _ = ([], []) 503 | funkyfold f (x :: xs) thms = let 504 val (z, thms') = f x thms 505 val (zs, thms'') = funkyfold f xs (thms' @ thms) 506 in (z :: zs, thms' @ thms'') end 507 508exception WrongType 509 510fun make_goal const_term const pre extra ctxt = 511 let val nns = const_term |> fastype_of |> num_args |> 512 Name.invent Name.context param_name; 513 val parse = Syntax.parse_term ctxt; 514 val check = Syntax.check_term ctxt; 515 val body = parse (String.concat (separate " " (const :: nns))); 516 in check (Instance.mk_term pre body extra) end; 517 518fun unify_helper rs n t = 519 case 520 Thm.cprem_of t n |> Thm.term_of |> snd (#trips rs) (Thm.theory_of_thm t) 521 |> Envir.beta_eta_contract |> Logic.strip_assums_concl 522 handle THM _ => @{const True} 523 of 524 Const (@{const_name Trueprop}, _) $ 525 (Const (@{const_name triple_judgement}, _) $ _ $ f $ _) => SOME f 526 | _ => NONE 527 528fun get_wp_rules ctxt n goal = 529 let 530 val wp_data = WeakestPre.debug_get ctxt 531 val f = unify_helper wp_data n goal 532 in case f of 533 SOME f => Net.unify_term (#1 (#rules wp_data)) f |> order_list |> rev 534 | NONE => map snd (#3 (#rules wp_data)) end 535 536(*rule can either solve thm or can be applied and refers to the same const*) 537fun can_solve_or_apply ctxt goal thm rule = 538 let 539 fun body term = term |> Instance.dest_term 540 |> Option.map (Term.term_name o Term.head_of o #2) 541 val const' = rule |> Thm.concl_of |> HOLogic.dest_Trueprop |> body 542 handle TERM _ => NONE 543 val thm' = SINGLE (resolve_tac ctxt [rule] 1) thm 544 fun changed st' = not (Thm.eq_thm (thm, st')); 545 fun solved st' = Thm.nprems_of st' < Thm.nprems_of thm 546 in if is_some thm' 547 then solved (the thm') orelse 548 (body goal = const' andalso changed (the thm')) 549 else false end 550 551fun test_thm_applies ctxt goal thm = SINGLE (CHANGED (resolve_tac ctxt [thm] 1)) goal 552 553fun crunch_known_rule cfg const thms goal = 554 let 555 val ctxt = #ctxt cfg 556 val vgoal_prop = goal |> var_precond |> HOLogic.mk_Trueprop 557 val cgoal_in = Goal.init (Thm.cterm_of ctxt vgoal_prop) 558 559 (*first option: previously crunched thm*) 560 val thms_proof = Seq.filter (is_proof_of cfg const) (Seq.of_list thms) 561 562 fun used_rule thm = 563 (Pretty.writeln (Pretty.big_list "found a rule for this constant:" 564 [ThmExtras.pretty_thm false ctxt thm]); thm) 565 566 (*second option: thm with same name*) 567 val stored_rule = try (get_stored cfg) const 568 val stored_rule_applies = 569 Option.mapPartial (test_thm_applies ctxt cgoal_in) stored_rule |> is_some 570 val stored_rule_error = 571 if is_some stored_rule andalso not stored_rule_applies 572 then Pretty.big_list "the generated goal does not match the existing rule:" 573 [ThmExtras.pretty_thm false ctxt (the stored_rule)] 574 |> Pretty.string_of |> SOME 575 else NONE 576 val stored = 577 if stored_rule_applies 578 then Seq.single (the stored_rule) |> Seq.map used_rule 579 else Seq.empty 580 581 (*third option: thm in wp set*) 582 val wp_rules = get_wp_rules ctxt 1 cgoal_in 583 val rules = map snd (thms @ #wp_rules cfg) @ wp_rules 584 val wps = filter (can_solve_or_apply ctxt goal cgoal_in) rules 585 val wps' = Seq.map used_rule (Seq.of_list wps) 586 587 (*error if no thm found and thm with same name does not apply*) 588 fun error'' (SOME opt) = SOME opt 589 | error'' NONE = Option.mapPartial error stored_rule_error 590 591 val seq = Seq.append (Seq.map snd thms_proof) (Seq.append stored wps') 592 in Seq.pull seq |> Option.map fst |> error'' end 593 594val mism_term_trace = Unsynchronized.ref [] 595 596fun seq_try_apply f x = Seq.map_filter (try f) (Seq.single x) 597 598fun wp ctxt rules = WeakestPre.apply_rules_tac_n false ctxt rules 599 600fun wpsimp ctxt wp_rules simp_rules = 601 let val ctxt' = Config.put Method.old_section_parser true ctxt 602 in NO_CONTEXT_TACTIC ctxt' 603 (Method_Closure.apply_method ctxt' @{method wpsimp} [] [wp_rules, [], simp_rules] [] ctxt' []) 604 end 605 606fun crunch_rule cfg const goal extra thms = 607 let 608 (* first option: produce a trivial rule as constant is being ignored *) 609 val ctxt = #ctxt cfg 610 val goal_prop = goal |> HOLogic.mk_Trueprop 611 val ignore_seq = 612 if member (op =) (crunch_ignores cfg ctxt) const 613 then goal_prop |> Thm.cterm_of ctxt |> Thm.trivial |> Seq.single |> Seq.map (pair NONE) 614 else Seq.empty 615 616 (* second option: produce a terminal rule via wpsimp *) 617 fun wpsimp' rules = wpsimp ctxt (map snd (thms @ #wp_rules cfg) @ rules) (#simps cfg) 618 val vgoal_prop = goal |> var_precond |> HOLogic.mk_Trueprop 619 val ctxt' = Proof_Context.augment goal_prop (Proof_Context.augment vgoal_prop ctxt) 620 val wp_seq = seq_try_apply (Goal.prove ctxt' [] [] goal_prop) 621 (fn _ => TRY (wpsimp' [])) 622 |> Seq.map (singleton (Proof_Context.export ctxt' ctxt)) 623 |> Seq.map (pair NONE) 624 625 (* third option: apply a supplied rule *) 626 val cgoal = vgoal_prop |> Thm.cterm_of ctxt 627 val base_rule = Thm.trivial cgoal 628 fun app_rew r t = Seq.single (Simplifier.rewrite_goals_rule ctxt [r] t) 629 |> Seq.filter (fn t' => not (Thm.eq_thm_prop (t, t'))) 630 val supplied_apps = Seq.of_list (#rules cfg) 631 |> Seq.maps (fn r => resolve_tac ctxt [r] 1 base_rule) 632 val supplied_app_rews = Seq.of_list (#rules cfg) 633 |> Seq.maps (fn r => app_rew r base_rule) 634 val supplied_seq = Seq.append supplied_apps supplied_app_rews 635 |> Seq.map (pair NONE) 636 637 (* fourth option: builtins *) 638 val builtin_seq = seq_try_apply (get_unfold_rule ctxt' const cgoal) (#nmspce cfg) 639 |> Seq.map (apfst SOME) 640 641 val seq = foldr1 (uncurry Seq.append) [ignore_seq, wp_seq, supplied_seq, builtin_seq] 642 643 fun fail_tac t _ _ = (writeln "discarding crunch rule, unsolved premise:"; 644 Syntax.pretty_term ctxt t |> Pretty.writeln; 645 mism_term_trace := (t, extra) :: (! mism_term_trace); 646 Seq.empty) 647 val goal_extra = goal |> Instance.dest_term |> the |> #3 648 val finalise = ALLGOALS (SUBGOAL (fn (t, i) 649 => if try (Logic.strip_assums_concl #> HOLogic.dest_Trueprop 650 #> Instance.dest_term #> the #> #3 #> curry Instance.eq_extra goal_extra) 651 t = SOME true 652 then all_tac 653 else DETERM (((fn i => wpsimp' []) 654 THEN_ALL_NEW fail_tac t) i))) 655 656 val seq = Seq.maps (fn (ms, t) => Seq.map (pair ms) (finalise t)) seq 657 658 val (ms, thm) = case Seq.pull seq of SOME ((ms, thm), _) => (ms, thm) 659 | NONE => error ("could not find crunch rule for " ^ const) 660 661 val _ = debug_trace_bl [K (Pretty.str "crunch rule: "), fn () => Thm.pretty_thm ctxt thm] 662 663 val ms = case ms of SOME ms => ms 664 | NONE => Thm.prems_of thm |> maps (monads_of ctxt) 665 in (ms, thm) end 666 667fun warn_helper_thms wp ctxt t = 668 let val simp_thms = maybe_thms ctxt "crunch_simps" 669 val ctxt' = ctxt addsimps simp_thms 670 val wp_thms = maybe_thms ctxt "crunch_wps" 671 fun can_tac tac = (is_some o SINGLE (HEADGOAL (CHANGED_GOAL tac))) t 672 in if can_tac (clarsimp_tac ctxt') 673 then warning "Using crunch_simps makes more progress" 674 else (); 675 if can_tac (wp wp_thms) 676 then warning "Using crunch_wps makes more progress" 677 else () 678 end; 679 680fun warn_const_ignored const cfg ctxt = 681 if member (op =) (crunch_ignores cfg ctxt) const 682 then warning ("constant " ^ const ^ " is being ignored") 683 else (); 684 685fun warn_stack const stack ctxt = 686 Pretty.big_list "Crunch call stack:" 687 (map (Proof_Context.pretty_const ctxt) (const::stack)) 688 |> Pretty.string_of |> warning; 689 690fun proof_failed_warnings const stack cfg wp ctxt t = 691 if Thm.no_prems t 692 then all_tac t 693 else (warn_const_ignored const cfg ctxt; warn_helper_thms wp ctxt t; 694 warn_stack const stack ctxt; all_tac t) 695 696fun crunch cfg pre extra stack const' thms = 697 let 698 val ctxt = #ctxt cfg |> Context_Position.set_visible false; 699 val const = real_const_from_name const' (#nmspce cfg) ctxt; 700 in 701 let 702 val _ = "crunching constant: " ^ const |> writeln; 703 val const_term = read_const ctxt const; 704 val goal = make_goal const_term const pre extra ctxt 705 handle exn => handle_int exn (raise WrongType); 706 val goal_prop = HOLogic.mk_Trueprop goal; 707 in (* first check: has this constant already been done or supplied? *) 708 case crunch_known_rule cfg const thms goal 709 of SOME thm => (SOME thm, []) 710 | NONE => let (* not already known, find a crunch rule. *) 711 val (ms, rule) = crunch_rule cfg const goal extra thms 712 (* and now crunch *) 713 val ctxt' = Proof_Context.augment goal ctxt; 714 val ms = ms 715 |> map (fn t => (real_const_from_name (fst (dest_Const (head_of t))) (#nmspce cfg) ctxt', t)) 716 |> subtract (fn (a, b) => a = (fst b)) (crunch_ignores cfg ctxt) 717 |> filter_out (fn (s, _) => s = const'); 718 val stack' = const :: stack; 719 val _ = if (length stack' > 20) then 720 (writeln "Crunch call stack:"; 721 map writeln (const::stack); 722 error("probably infinite loop")) else (); 723 val (goals, thms') = funkyfold (crunch cfg pre extra stack') (map fst ms) thms; 724 val goals' = map_filter I goals 725 val ctxt'' = ctxt' addsimps ((#simps cfg) @ goals') 726 |> Splitter.del_split split_if 727 728 fun collect_preconds pre = 729 let val preconds = map_filter (fn (x, SOME y) => SOME (x, y) | (_, NONE) => NONE) (map snd ms ~~ goals) 730 |> map_filter (get_inst_precond ctxt'' pre extra); 731 val precond = combine_preconds ctxt'' (get_precond goal) preconds; 732 in Instance.put_precond precond goal |> HOLogic.mk_Trueprop end; 733 val goal_prop2 = if Instance.has_preconds then collect_preconds pre else goal_prop; 734 735 val ctxt''' = ctxt'' |> Proof_Context.augment goal_prop2 736 val _ = writeln ("attempting: " ^ Syntax.string_of_term ctxt''' goal_prop2); 737 738 fun wp' wp_rules = wp ctxt (map snd (thms @ #wp_rules cfg) @ goals' @ wp_rules) 739 740 val thm = Goal.prove_future ctxt''' [] [] goal_prop2 741 ( (*DupSkip.goal_prove_wrapper *) (fn _ => 742 resolve_tac ctxt''' [rule] 1 743 THEN maybe_cheat_tac ctxt''' 744 THEN ALLGOALS (simp_tac ctxt''') 745 THEN ALLGOALS (fn n => 746 TRY (resolve_tac ctxt''' Instance.pre_thms n) 747 THEN 748 REPEAT_DETERM (( 749 WPFix.tac ctxt 750 ORELSE' 751 wp' [] 752 ORELSE' 753 CHANGED_GOAL (clarsimp_tac ctxt''') 754 ORELSE' 755 assume_tac ctxt''' 756 ORELSE' 757 Instance.wpc_tactic ctxt''' 758 ORELSE' 759 Instance.wps_tactic ctxt''' (#wps_rules cfg) 760 ORELSE' 761 SELECT_GOAL (safe_tac ctxt''') 762 ORELSE' 763 CHANGED_GOAL (simp_tac ctxt''') 764 ) n)) 765 THEN proof_failed_warnings const stack cfg wp' ctxt''' 766 )) |> singleton (Proof_Context.export ctxt''' ctxt) 767 in (SOME thm, (get_thm_name cfg const, thm) :: thms') end 768 end 769 handle WrongType => 770 let val _ = writeln ("The constant " ^ const ^ " has the wrong type and is being ignored") 771 in (NONE, []) end 772 end 773 774(*Todo: Remember mapping from locales to theories*) 775fun get_locale_origins full_const_names ctxt = 776 let 777 fun get_locale_origin abbrev = 778 let 779 (*Check if the given const is an abbreviation*) 780 val (origin,_) = dest_Const (head_of (snd ((Consts.the_abbreviation o Proof_Context.consts_of) ctxt abbrev))); 781 (*Check that the origin can be broken into 3 parts (i.e. it is from a locale) *) 782 val [_,_,_] = Long_Name.explode origin; 783 (*Remember the theory for the abbreviation*) 784 785 val [qual,nm] = Long_Name.explode abbrev 786 in SOME qual end handle exn => handle_int exn NONE 787 in fold (curry (fn (abbrev,qual) => case (get_locale_origin abbrev) of 788 SOME q => SOME q 789 | NONE => NONE)) full_const_names NONE 790 end 791 792fun crunch_x atts extra prp_name wpigs consts ctxt = 793 let 794 fun const_name const = dest_Const (read_const ctxt const) |> #1 795 796 val wp_rules' = wpigs |> filter (fn (s,_) => s = #1 wp_sect) |> map #2 |> thms 797 798 val wp_dels' = wpigs |> filter (fn (s,_) => s = #1 wp_del_sect) |> map #2 |> thms 799 800 val wps_rules = wpigs |> filter (fn (s,_) => s = #1 wps_sect) |> map #2 |> thms 801 |> get_thms_from_facts ctxt 802 803 val simps = wpigs |> filter (fn (s,_) => s = #1 simp_sect) |> map #2 |> thms 804 |> get_thms_from_facts ctxt 805 806 val simp_dels = wpigs |> filter (fn (s,_) => s = #1 simp_del_sect) |> map #2 |> thms 807 |> get_thms_from_facts ctxt 808 809 val igs = wpigs |> filter (fn (s,_) => s = #1 ignore_sect) |> map #2 |> constants 810 |> map const_name 811 812 val ig_dels = wpigs |> filter (fn (s,_) => s = #1 ignore_del_sect) |> map #2 |> constants 813 |> map const_name 814 815 val rules = wpigs |> filter (fn (s,_) => s = #1 rule_sect) |> map #2 |> thms 816 |> get_thms_from_facts ctxt 817 val rules = rules @ Named_Theorems.get ctxt @{named_theorems crunch_rules} 818 819 fun mk_wp thm = 820 let val ms = Thm.prop_of thm |> monads_of ctxt; 821 val m = if length ms = 1 822 then hd ms |> head_of |> dest_Const |> fst 823 else dummy_monad_name; 824 in (m, thm) end; 825 826 val wp_rules = get_thms_from_facts ctxt wp_rules' |> map mk_wp; 827 val full_const_names = map const_name consts; 828 829 val nmspce = get_locale_origins full_const_names ctxt; 830 val (pre', extra') = Instance.parse_extra ctxt extra 831 handle ERROR s => error ("parsing parameters for " ^ prp_name ^ ": " ^ s) 832 833 (* check that the given constants match the type of the given property*) 834 val const_terms = map (read_const ctxt) full_const_names; 835 val _ = map (fn (const_term, const) => make_goal const_term const pre' extra' ctxt) 836 (const_terms ~~ full_const_names) 837 838 val wp_dels = get_thms_from_facts ctxt wp_dels'; 839 val ctxt' = fold (fn thm => fn ctxt => Thm.proof_attributes [WeakestPre.wp_del] thm ctxt |> snd) 840 wp_dels ctxt; 841 842 val ctxt'' = ctxt' delsimps simp_dels; 843 844 val (_, thms) = funkyfold (crunch {ctxt = ctxt'', prp_name = prp_name, nmspce = nmspce, 845 wp_rules = wp_rules, wps_rules = wps_rules, igs = igs, simps = simps, 846 ig_dels = ig_dels, rules = rules} pre' extra' []) 847 full_const_names []; 848 val _ = if null thms then warning "crunch: no theorems proven" else (); 849 850 val atts' = map (Attrib.check_src ctxt) atts; 851 852 val ctxt''' = fold (fn (name, thm) => add_thm thm atts' name) thms ctxt; 853 in 854 Pretty.writeln 855 (Pretty.big_list "proved:" 856 (map (fn (n,t) => 857 Pretty.block 858 [Pretty.str (n ^ ": "), 859 Syntax.pretty_term ctxt (Thm.prop_of t)]) 860 thms)); 861 ctxt''' 862 end 863 864end 865