1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Strengthen 8imports Main 9begin 10 11text \<open>Implementation of the @{text strengthen} tool and the @{text mk_strg} 12attribute. See the theory @{text Strengthen_Demo} for a demonstration.\<close> 13 14locale strengthen_implementation begin 15 16definition "st P rel x y = (x = y \<or> (P \<and> rel x y) \<or> (\<not> P \<and> rel y x))" 17 18definition 19 st_prop1 :: "prop \<Rightarrow> prop \<Rightarrow> prop" 20where 21 "st_prop1 (PROP P) (PROP Q) \<equiv> (PROP Q \<Longrightarrow> PROP P)" 22 23definition 24 st_prop2 :: "prop \<Rightarrow> prop \<Rightarrow> prop" 25where 26 "st_prop2 (PROP P) (PROP Q) \<equiv> (PROP P \<Longrightarrow> PROP Q)" 27 28definition "failed == True" 29 30definition elim :: "prop \<Rightarrow> prop" 31where 32 "elim (P :: prop) == P" 33 34definition "oblig (P :: prop) == P" 35 36end 37 38notation strengthen_implementation.elim ("{elim| _ |}") 39notation strengthen_implementation.oblig ("{oblig| _ |}") 40notation strengthen_implementation.failed ("<strg-failed>") 41 42syntax 43 "_ap_strg_bool" :: "['a, 'a] => 'a" ("_ =strg<--|=> _") 44 "_ap_wkn_bool" :: "['a, 'a] => 'a" ("_ =strg-->|=> _") 45 "_ap_ge_bool" :: "['a, 'a] => 'a" ("_ =strg<=|=> _") 46 "_ap_le_bool" :: "['a, 'a] => 'a" ("_ =strg>=|=> _") 47 48syntax(xsymbols) 49 "_ap_strg_bool" :: "['a, 'a] => 'a" ("_ =strg\<longleftarrow>|=> _") 50 "_ap_wkn_bool" :: "['a, 'a] => 'a" ("_ =strg\<longrightarrow>|=> _") 51 "_ap_ge_bool" :: "['a, 'a] => 'a" ("_ =strg\<le>|=> _") 52 "_ap_le_bool" :: "['a, 'a] => 'a" ("_ =strg\<ge>|=> _") 53 54translations 55 "P =strg\<longleftarrow>|=> Q" == "CONST strengthen_implementation.st (CONST False) (CONST HOL.implies) P Q" 56 "P =strg\<longrightarrow>|=> Q" == "CONST strengthen_implementation.st (CONST True) (CONST HOL.implies) P Q" 57 "P =strg\<le>|=> Q" == "CONST strengthen_implementation.st (CONST False) (CONST Orderings.less_eq) P Q" 58 "P =strg\<ge>|=> Q" == "CONST strengthen_implementation.st (CONST True) (CONST Orderings.less_eq) P Q" 59 60context strengthen_implementation begin 61 62lemma failedI: 63 "<strg-failed>" 64 by (simp add: failed_def) 65 66lemma strengthen_refl: 67 "st P rel x x" 68 by (simp add: st_def) 69 70lemma st_prop_refl: 71 "PROP (st_prop1 (PROP P) (PROP P))" 72 "PROP (st_prop2 (PROP P) (PROP P))" 73 unfolding st_prop1_def st_prop2_def 74 by safe 75 76lemma strengthenI: 77 "rel x y \<Longrightarrow> st True rel x y" 78 "rel y x \<Longrightarrow> st False rel x y" 79 by (simp_all add: st_def) 80 81lemmas imp_to_strengthen = strengthenI(2)[where rel="(\<longrightarrow>)"] 82lemmas rev_imp_to_strengthen = strengthenI(1)[where rel="(\<longrightarrow>)"] 83lemmas ord_to_strengthen = strengthenI[where rel="(\<le>)"] 84 85lemma use_strengthen_imp: 86 "st False (\<longrightarrow>) Q P \<Longrightarrow> P \<Longrightarrow> Q" 87 by (simp add: st_def) 88 89lemma use_strengthen_prop_elim: 90 "PROP P \<Longrightarrow> PROP (st_prop2 (PROP P) (PROP Q)) 91 \<Longrightarrow> (PROP Q \<Longrightarrow> PROP R) \<Longrightarrow> PROP R" 92 unfolding st_prop2_def 93 apply (drule(1) meta_mp)+ 94 apply assumption 95 done 96 97lemma strengthen_Not: 98 "st False rel x y \<Longrightarrow> st (\<not> True) rel x y" 99 "st True rel x y \<Longrightarrow> st (\<not> False) rel x y" 100 by auto 101 102lemmas gather = 103 swap_prems_eq[where A="PROP (Trueprop P)" and B="PROP (elim Q)" for P Q] 104 swap_prems_eq[where A="PROP (Trueprop P)" and B="PROP (oblig Q)" for P Q] 105 106lemma mk_True_imp: 107 "P \<equiv> True \<longrightarrow> P" 108 by simp 109 110lemma narrow_quant: 111 "(\<And>x. PROP P \<Longrightarrow> PROP (Q x)) \<equiv> (PROP P \<Longrightarrow> (\<And>x. PROP (Q x)))" 112 "(\<And>x. (R \<longrightarrow> S x)) \<equiv> PROP (Trueprop (R \<longrightarrow> (\<forall>x. S x)))" 113 "(\<And>x. (S x \<longrightarrow> R)) \<equiv> PROP (Trueprop ((\<exists>x. S x) \<longrightarrow> R))" 114 apply (simp_all add: atomize_all) 115 apply rule 116 apply assumption 117 apply assumption 118 done 119 120ML \<open> 121structure Make_Strengthen_Rule = struct 122 123fun binop_conv' cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2; 124 125val mk_elim = Conv.rewr_conv @{thm elim_def[symmetric]} 126val mk_oblig = Conv.rewr_conv @{thm oblig_def[symmetric]} 127 128fun count_vars t = Term.fold_aterms 129 (fn (Var v) => Termtab.map_default (Var v, 0) (fn x => x + 1) 130 | _ => I) t Termtab.empty 131 132fun gather_to_imp ctxt drule pattern = let 133 val pattern = (if drule then "D" :: pattern else pattern) 134 fun inner pat ct = case (head_of (Thm.term_of ct), pat) of 135 (@{term Pure.imp}, ("E" :: pat)) => binop_conv' mk_elim (inner pat) ct 136 | (@{term Pure.imp}, ("A" :: pat)) => binop_conv' mk_elim (inner pat) ct 137 | (@{term Pure.imp}, ("O" :: pat)) => binop_conv' mk_oblig (inner pat) ct 138 | (@{term Pure.imp}, _) => binop_conv' (Object_Logic.atomize ctxt) (inner (drop 1 pat)) ct 139 | (_, []) => Object_Logic.atomize ctxt ct 140 | (_, pat) => raise THM ("gather_to_imp: leftover pattern: " ^ commas pat, 1, []) 141 fun simp thms = Raw_Simplifier.rewrite ctxt false thms 142 fun ensure_imp ct = case strip_comb (Thm.term_of ct) |> apsnd (map head_of) 143 of 144 (@{term Pure.imp}, _) => Conv.arg_conv ensure_imp ct 145 | (@{term HOL.Trueprop}, [@{term HOL.implies}]) => Conv.all_conv ct 146 | (@{term HOL.Trueprop}, _) => Conv.arg_conv (Conv.rewr_conv @{thm mk_True_imp}) ct 147 | _ => raise CTERM ("gather_to_imp", [ct]) 148 val gather = simp @{thms gather} 149 then_conv (if drule then Conv.all_conv else simp @{thms atomize_conjL}) 150 then_conv simp @{thms atomize_imp} 151 then_conv ensure_imp 152 in Conv.fconv_rule (inner pattern then_conv gather) end 153 154fun imp_list t = let 155 val (x, y) = Logic.dest_implies t 156 in x :: imp_list y end handle TERM _ => [t] 157 158fun mk_ex (xnm, T) t = HOLogic.exists_const T $ Term.lambda (Var (xnm, T)) t 159fun mk_all (xnm, T) t = HOLogic.all_const T $ Term.lambda (Var (xnm, T)) t 160 161fun quantify_vars ctxt drule thm = let 162 val (lhs, rhs) = Thm.concl_of thm |> HOLogic.dest_Trueprop 163 |> HOLogic.dest_imp 164 val all_vars = count_vars (Thm.prop_of thm) 165 val new_vars = count_vars (if drule then rhs else lhs) 166 val quant = filter (fn v => Termtab.lookup new_vars v = Termtab.lookup all_vars v) 167 (Termtab.keys new_vars) 168 |> map (Thm.cterm_of ctxt) 169 in fold Thm.forall_intr quant thm 170 |> Conv.fconv_rule (Raw_Simplifier.rewrite ctxt false @{thms narrow_quant}) 171 end 172 173fun mk_strg (typ, pat) ctxt thm = let 174 val drule = typ = "D" orelse typ = "D'" 175 val imp = gather_to_imp ctxt drule pat thm 176 |> (if typ = "I'" orelse typ = "D'" 177 then quantify_vars ctxt drule else I) 178 in if typ = "I" orelse typ = "I'" 179 then imp RS @{thm imp_to_strengthen} 180 else if drule then imp RS @{thm rev_imp_to_strengthen} 181 else if typ = "lhs" then imp RS @{thm ord_to_strengthen(1)} 182 else if typ = "rhs" then imp RS @{thm ord_to_strengthen(2)} 183 else raise THM ("mk_strg: unknown type: " ^ typ, 1, [thm]) 184 end 185 186fun auto_mk ctxt thm = let 187 val concl_C = try (fst o dest_Const o head_of 188 o HOLogic.dest_Trueprop) (Thm.concl_of thm) 189 in case (Thm.nprems_of thm, concl_C) of 190 (_, SOME @{const_name failed}) => thm 191 | (_, SOME @{const_name st}) => thm 192 | (0, SOME @{const_name HOL.implies}) => (thm RS @{thm imp_to_strengthen} 193 handle THM _ => @{thm failedI}) 194 | _ => mk_strg ("I'", []) ctxt thm 195 end 196 197fun mk_strg_args (SOME (typ, pat)) ctxt thm = mk_strg (typ, pat) ctxt thm 198 | mk_strg_args NONE ctxt thm = auto_mk ctxt thm 199 200val arg_pars = Scan.option (Scan.first (map Args.$$$ ["I", "I'", "D", "D'", "lhs", "rhs"]) 201 -- Scan.repeat (Args.$$$ "A" || Args.$$$ "E" || Args.$$$ "O" || Args.$$$ "_")) 202 203val attr_pars : attribute context_parser 204 = (Scan.lift arg_pars -- Args.context) 205 >> (fn (args, ctxt) => Thm.rule_attribute [] (K (mk_strg_args args ctxt))) 206 207 208end 209\<close> 210 211end 212 213attribute_setup mk_strg = \<open>Make_Strengthen_Rule.attr_pars\<close> 214 "put rule in 'strengthen' form (see theory Strengthen_Demo)" 215 216text \<open>Quick test.\<close> 217 218lemmas foo = nat.induct[mk_strg I O O] 219 nat.induct[mk_strg D O] 220 nat.induct[mk_strg I' E] 221 exI[mk_strg I'] exI[mk_strg I] 222 223context strengthen_implementation begin 224 225lemma do_elim: 226 "PROP P \<Longrightarrow> PROP elim (PROP P)" 227 by (simp add: elim_def) 228 229lemma intro_oblig: 230 "PROP P \<Longrightarrow> PROP oblig (PROP P)" 231 by (simp add: oblig_def) 232 233ML \<open> 234 235structure Strengthen = struct 236 237structure Congs = Theory_Data 238(struct 239 type T = thm list 240 val empty = [] 241 val extend = I 242 val merge = Thm.merge_thms; 243end); 244 245val tracing = Attrib.config_bool @{binding strengthen_trace} (K false) 246 247fun map_context_total f (Context.Theory t) = (Context.Theory (f t)) 248 | map_context_total f (Context.Proof p) 249 = (Context.Proof (Context.raw_transfer (f (Proof_Context.theory_of p)) p)) 250 251val strg_add = Thm.declaration_attribute 252 (fn thm => map_context_total (Congs.map (Thm.add_thm thm))); 253 254val strg_del = Thm.declaration_attribute 255 (fn thm => map_context_total (Congs.map (Thm.del_thm thm))); 256 257val setup = 258 Attrib.setup @{binding "strg"} (Attrib.add_del strg_add strg_del) 259 "strengthening congruence rules" 260 #> snd tracing; 261 262fun goal_predicate t = let 263 val gl = Logic.strip_assums_concl t 264 val cn = head_of #> dest_Const #> fst 265 in if cn gl = @{const_name oblig} then "oblig" 266 else if cn gl = @{const_name elim} then "elim" 267 else if cn gl = @{const_name st_prop1} then "st_prop1" 268 else if cn gl = @{const_name st_prop2} then "st_prop2" 269 else if cn (HOLogic.dest_Trueprop gl) = @{const_name st} then "st" 270 else "" 271 end handle TERM _ => "" 272 273fun do_elim ctxt = SUBGOAL (fn (t, i) => if goal_predicate t = "elim" 274 then eresolve_tac ctxt @{thms do_elim} i else all_tac) 275 276fun final_oblig_strengthen ctxt = SUBGOAL (fn (t, i) => case goal_predicate t of 277 "oblig" => resolve_tac ctxt @{thms intro_oblig} i 278 | "st" => resolve_tac ctxt @{thms strengthen_refl} i 279 | "st_prop1" => resolve_tac ctxt @{thms st_prop_refl} i 280 | "st_prop2" => resolve_tac ctxt @{thms st_prop_refl} i 281 | _ => all_tac) 282 283infix 1 THEN_TRY_ALL_NEW; 284 285(* Like THEN_ALL_NEW but allows failure, although at least one subsequent 286 method must succeed. *) 287fun (tac1 THEN_TRY_ALL_NEW tac2) i st = let 288 fun inner b j st = if i > j then (if b then all_tac else no_tac) st 289 else ((tac2 j THEN inner true (j - 1)) ORELSE inner b (j - 1)) st 290 in st |> (tac1 i THEN (fn st' => 291 inner false (i + Thm.nprems_of st' - Thm.nprems_of st) st')) end 292 293fun maybe_trace_tac false _ _ = K all_tac 294 | maybe_trace_tac true ctxt msg = SUBGOAL (fn (t, _) => let 295 val tr = Pretty.big_list msg [Syntax.pretty_term ctxt t] 296 in 297 Pretty.writeln tr; 298 all_tac 299 end) 300 301fun maybe_trace_rule false _ _ rl = rl 302 | maybe_trace_rule true ctxt msg rl = let 303 val tr = Pretty.big_list msg [Syntax.pretty_term ctxt (Thm.prop_of rl)] 304 in 305 Pretty.writeln tr; 306 rl 307 end 308 309type params = {trace : bool, once : bool} 310 311fun params once ctxt = {trace = Config.get ctxt (fst tracing), once = once} 312 313fun apply_tac_as_strg ctxt (params : params) (tac : tactic) 314 = SUBGOAL (fn (t, i) => case Logic.strip_assums_concl t of 315 @{term Trueprop} $ (@{term "st False (\<longrightarrow>)"} $ x $ _) 316 => let 317 val triv = Thm.trivial (Thm.cterm_of ctxt (HOLogic.mk_Trueprop x)) 318 val trace = #trace params 319 in 320 fn thm => tac triv 321 |> Seq.map (maybe_trace_rule trace ctxt "apply_tac_as_strg: making strg") 322 |> Seq.maps (Seq.try (Make_Strengthen_Rule.auto_mk ctxt)) 323 |> Seq.maps (fn str_rl => resolve_tac ctxt [str_rl] i thm) 324 end | _ => no_tac) 325 326fun opt_tac f (SOME v) = f v 327 | opt_tac _ NONE = K no_tac 328 329fun apply_strg ctxt (params : params) congs rules tac = EVERY' [ 330 maybe_trace_tac (#trace params) ctxt "apply_strg", 331 DETERM o TRY o resolve_tac ctxt @{thms strengthen_Not}, 332 DETERM o ((resolve_tac ctxt rules THEN_ALL_NEW do_elim ctxt) 333 ORELSE' (opt_tac (apply_tac_as_strg ctxt params) tac) 334 ORELSE' (resolve_tac ctxt congs THEN_TRY_ALL_NEW 335 (fn i => apply_strg ctxt params congs rules tac i))) 336] 337 338fun setup_strg ctxt params thms meths = let 339 val congs = Congs.get (Proof_Context.theory_of ctxt) 340 val rules = map (Make_Strengthen_Rule.auto_mk ctxt) thms 341 val tac = case meths of [] => NONE 342 | _ => SOME (FIRST (map (fn meth => NO_CONTEXT_TACTIC ctxt 343 (Method.evaluate meth ctxt [])) meths)) 344 in apply_strg ctxt params congs rules tac 345 THEN_ALL_NEW final_oblig_strengthen ctxt end 346 347fun strengthen ctxt asm concl thms meths = let 348 val strg = setup_strg ctxt (params false ctxt) thms meths 349 in 350 (if not concl then K no_tac 351 else resolve_tac ctxt @{thms use_strengthen_imp} THEN' strg) 352 ORELSE' (if not asm then K no_tac 353 else eresolve_tac ctxt @{thms use_strengthen_prop_elim} THEN' strg) 354 end 355 356fun default_strengthen ctxt thms = strengthen ctxt false true thms [] 357 358val strengthen_args = 359 Attrib.thms >> curry (fn (rules, ctxt) => 360 Method.CONTEXT_METHOD (fn _ => 361 Method.RUNTIME (CONTEXT_TACTIC 362 (strengthen ctxt false true rules [] 1)) 363 ) 364 ); 365 366val strengthen_asm_args = 367 Attrib.thms >> curry (fn (rules, ctxt) => 368 Method.CONTEXT_METHOD (fn _ => 369 Method.RUNTIME (CONTEXT_TACTIC 370 (strengthen ctxt true false rules [] 1)) 371 ) 372 ); 373 374val strengthen_method_args = 375 Method.text_closure >> curry (fn (meth, ctxt) => 376 Method.CONTEXT_METHOD (fn _ => 377 Method.RUNTIME (CONTEXT_TACTIC 378 (strengthen ctxt true true [] [meth] 1)) 379 ) 380 ); 381 382end 383 384\<close> 385 386end 387 388setup "Strengthen.setup" 389 390method_setup strengthen = \<open>Strengthen.strengthen_args\<close> 391 "strengthen the goal (see theory Strengthen_Demo)" 392 393method_setup strengthen_asm = \<open>Strengthen.strengthen_asm_args\<close> 394 "apply ''strengthen'' to weaken an assumption" 395 396method_setup strengthen_method = \<open>Strengthen.strengthen_method_args\<close> 397 "use an argument method in ''strengthen'' sites" 398 399text \<open>Important strengthen congruence rules.\<close> 400 401context strengthen_implementation begin 402 403lemma strengthen_imp_imp[simp]: 404 "st True (\<longrightarrow>) A B = (A \<longrightarrow> B)" 405 "st False (\<longrightarrow>) A B = (B \<longrightarrow> A)" 406 by (simp_all add: st_def) 407 408abbreviation(input) 409 "st_ord t \<equiv> st t ((\<le>) :: ('a :: preorder) \<Rightarrow> _)" 410 411lemma strengthen_imp_ord[simp]: 412 "st_ord True A B = (A \<le> B)" 413 "st_ord False A B = (B \<le> A)" 414 by (auto simp add: st_def) 415 416lemma strengthen_imp_conj [strg]: 417 "\<lbrakk> A' \<Longrightarrow> st F (\<longrightarrow>) B B'; B \<Longrightarrow> st F (\<longrightarrow>) A A' \<rbrakk> 418 \<Longrightarrow> st F (\<longrightarrow>) (A \<and> B) (A' \<and> B')" 419 by (cases F, auto) 420 421lemma strengthen_imp_disj [strg]: 422 "\<lbrakk> \<not> A' \<Longrightarrow> st F (\<longrightarrow>) B B'; \<not> B \<Longrightarrow> st F (\<longrightarrow>) A A' \<rbrakk> 423 \<Longrightarrow> st F (\<longrightarrow>) (A \<or> B) (A' \<or> B')" 424 by (cases F, auto) 425 426lemma strengthen_imp_implies [strg]: 427 "\<lbrakk> st (\<not> F) (\<longrightarrow>) X X'; X \<Longrightarrow> st F (\<longrightarrow>) Y Y' \<rbrakk> 428 \<Longrightarrow> st F (\<longrightarrow>) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')" 429 by (cases F, auto) 430 431lemma strengthen_all[strg]: 432 "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (Q x) \<rbrakk> 433 \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x. P x) (\<forall>x. Q x)" 434 by (cases F, auto) 435 436lemma strengthen_ex[strg]: 437 "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (Q x) \<rbrakk> 438 \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x. P x) (\<exists>x. Q x)" 439 by (cases F, auto) 440 441lemma strengthen_Ball[strg]: 442 "\<lbrakk> st_ord (Not F) S S'; 443 \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x) \<rbrakk> 444 \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x \<in> S. P x) (\<forall>x \<in> S'. Q x)" 445 by (cases F, auto) 446 447lemma strengthen_Bex[strg]: 448 "\<lbrakk> st_ord F S S'; 449 \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x) \<rbrakk> 450 \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x \<in> S. P x) (\<exists>x \<in> S'. Q x)" 451 by (cases F, auto) 452 453lemma strengthen_Collect[strg]: 454 "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (P' x) \<rbrakk> 455 \<Longrightarrow> st_ord F {x. P x} {x. P' x}" 456 by (cases F, auto) 457 458lemma strengthen_mem[strg]: 459 "\<lbrakk> st_ord F S S' \<rbrakk> 460 \<Longrightarrow> st F (\<longrightarrow>) (x \<in> S) (x \<in> S')" 461 by (cases F, auto) 462 463lemma strengthen_ord[strg]: 464 "st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y' 465 \<Longrightarrow> st F (\<longrightarrow>) (x \<le> y) (x' \<le> y')" 466 by (cases F, simp_all, (metis order_trans)+) 467 468lemma strengthen_strict_ord[strg]: 469 "st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y' 470 \<Longrightarrow> st F (\<longrightarrow>) (x < y) (x' < y')" 471 by (cases F, simp_all, (metis order_le_less_trans order_less_le_trans)+) 472 473lemma strengthen_image[strg]: 474 "st_ord F S S' \<Longrightarrow> st_ord F (f ` S) (f ` S')" 475 by (cases F, auto) 476 477lemma strengthen_vimage[strg]: 478 "st_ord F S S' \<Longrightarrow> st_ord F (f -` S) (f -` S')" 479 by (cases F, auto) 480 481lemma strengthen_Int[strg]: 482 "st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<inter> B) (A' \<inter> B')" 483 by (cases F, auto) 484 485lemma strengthen_Un[strg]: 486 "st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<union> B) (A' \<union> B')" 487 by (cases F, auto) 488 489lemma strengthen_UN[strg]: 490 "st_ord F A A' \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> st_ord F (B x) (B' x)) 491 \<Longrightarrow> st_ord F (\<Union>x \<in> A. B x) (\<Union>x \<in> A'. B' x)" 492 by (cases F, auto) 493 494lemma strengthen_INT[strg]: 495 "st_ord (\<not> F) A A' \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> st_ord F (B x) (B' x)) 496 \<Longrightarrow> st_ord F (\<Inter>x \<in> A. B x) (\<Inter>x \<in> A'. B' x)" 497 by (cases F, auto) 498 499lemma strengthen_imp_strengthen_prop[strg]: 500 "st False (\<longrightarrow>) P Q \<Longrightarrow> PROP (st_prop1 (Trueprop P) (Trueprop Q))" 501 "st True (\<longrightarrow>) P Q \<Longrightarrow> PROP (st_prop2 (Trueprop P) (Trueprop Q))" 502 unfolding st_prop1_def st_prop2_def 503 by auto 504 505lemma st_prop_meta_imp[strg]: 506 "PROP (st_prop2 (PROP X) (PROP X')) 507 \<Longrightarrow> PROP (st_prop1 (PROP Y) (PROP Y')) 508 \<Longrightarrow> PROP (st_prop1 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y'))" 509 "PROP (st_prop1 (PROP X) (PROP X')) 510 \<Longrightarrow> PROP (st_prop2 (PROP Y) (PROP Y')) 511 \<Longrightarrow> PROP (st_prop2 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y'))" 512 unfolding st_prop1_def st_prop2_def 513 by (erule meta_mp | assumption)+ 514 515lemma st_prop_meta_all[strg]: 516 "(\<And>x. PROP (st_prop1 (PROP (X x)) (PROP (X' x)))) 517 \<Longrightarrow> PROP (st_prop1 (\<And>x. PROP (X x)) (\<And>x. PROP (X' x)))" 518 "(\<And>x. PROP (st_prop2 (PROP (X x)) (PROP (X' x)))) 519 \<Longrightarrow> PROP (st_prop2 (\<And>x. PROP (X x)) (\<And>x. PROP (X' x)))" 520 unfolding st_prop1_def st_prop2_def 521 apply (rule Pure.asm_rl) 522 apply (erule meta_allE, erule meta_mp) 523 apply assumption 524 apply (rule Pure.asm_rl) 525 apply (erule meta_allE, erule meta_mp) 526 apply assumption 527 done 528 529(* to think about, what more monotonic constructions can we find? *) 530 531end 532 533lemma imp_consequent: 534 "P \<longrightarrow> Q \<longrightarrow> P" by simp 535 536text \<open>Test cases.\<close> 537 538lemma 539 assumes x: "\<And>x. P x \<longrightarrow> Q x" 540 shows "{x. x \<noteq> None \<and> P (the x)} \<subseteq> {y. \<forall>x. y = Some x \<longrightarrow> Q x}" 541 apply (strengthen x) 542 apply clarsimp 543 done 544 545locale strengthen_silly_test begin 546 547definition 548 silly :: "nat \<Rightarrow> nat \<Rightarrow> bool" 549where 550 "silly x y = (x \<le> y)" 551 552lemma silly_trans: 553 "silly x y \<Longrightarrow> silly y z \<Longrightarrow> silly x z" 554 by (simp add: silly_def) 555 556lemma silly_refl: 557 "silly x x" 558 by (simp add: silly_def) 559 560lemma foo: 561 "silly x y \<Longrightarrow> silly a b \<Longrightarrow> silly b c 562 \<Longrightarrow> silly x y \<and> (\<forall>x :: nat. silly a c )" 563 using [[strengthen_trace = true]] 564 apply (strengthen silly_trans[mk_strg I E])+ 565 apply (strengthen silly_refl) 566 apply simp 567 done 568 569lemma foo_asm: 570 "silly x y \<Longrightarrow> silly y z 571 \<Longrightarrow> (silly x z \<Longrightarrow> silly a b) \<Longrightarrow> silly z z \<Longrightarrow> silly a b" 572 apply (strengthen_asm silly_trans[mk_strg I A]) 573 apply (strengthen_asm silly_trans[mk_strg I A]) 574 apply simp 575 done 576 577lemma foo_method: 578 "silly x y \<Longrightarrow> silly a b \<Longrightarrow> silly b c 579 \<Longrightarrow> silly x y \<and> (\<forall>x :: nat. z \<longrightarrow> silly a c )" 580 using [[strengthen_trace = true]] 581 apply simp 582 apply (strengthen_method \<open>rule silly_trans\<close>) 583 apply (strengthen_method \<open>rule exI[where x=b]\<close>) 584 apply simp 585 done 586 587end 588end 589