1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 *) 10 11(* 12 * Term subst method: substitution with a given term as the equation. 13 * The equation will be added as a subgoal. 14 * See example at the end of this file. 15 *) 16 17theory TSubst 18imports 19 Main 20begin 21 22method_setup tsubst = \<open> 23 Scan.lift (Args.mode "asm" -- 24 Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0] -- 25 Parse.term) 26 >> (fn ((asm,occs),t) => (fn ctxt => 27 Method.SIMPLE_METHOD (Subgoal.FOCUS_PARAMS (fn focus => (fn thm => 28 let 29 (* This code used to use Thm.certify_inst in 2014, which was removed. 30 The following is just a best guess for what it did. *) 31 fun certify_inst ctxt (typ_insts, term_insts) = 32 (typ_insts 33 |> map (fn (tvar, inst) => 34 (Thm.ctyp_of ctxt (TVar tvar), 35 Thm.ctyp_of ctxt inst)), 36 term_insts 37 |> map (fn (var, inst) => 38 (Thm.cterm_of ctxt (Var var), 39 Thm.cterm_of ctxt inst))) 40 41 val ctxt' = #context focus 42 43 val ((_, schematic_terms), ctxt2) = 44 Variable.import_inst true [(#concl focus) |> Thm.term_of] ctxt' 45 |>> certify_inst ctxt' 46 47 val ctxt3 = fold (fn (t,t') => Variable.bind_term (Thm.term_of t |> Term.dest_Var |> fst, (t' |> Thm.term_of))) schematic_terms ctxt2 48 49 50 val athm = Syntax.read_term ctxt3 t 51 |> Object_Logic.ensure_propT ctxt' 52 |> Thm.cterm_of ctxt' 53 |> Thm.trivial 54 55 val thm' = Thm.instantiate ([], map (apfst (Thm.term_of #> dest_Var)) schematic_terms) thm 56 57 in 58 (if asm then EqSubst.eqsubst_asm_tac else EqSubst.eqsubst_tac) 59 ctxt3 occs [athm] 1 thm' 60 |> Seq.map (singleton (Variable.export ctxt3 ctxt')) 61 end)) ctxt 1))) 62 \<close> "subst, with term instead of theorem as equation" 63 64schematic_goal 65 assumes a: "\<And>x y. P x \<Longrightarrow> P y" 66 fixes x :: 'b 67 shows "\<And>x ::'a :: type. ?Q x \<Longrightarrow> P x \<and> ?Q x" 68 apply (tsubst (asm) "?Q x = (P x \<and> P x)") 69 apply (rule refl) 70 apply (tsubst "P x = P y",simp add:a)+ 71 apply (tsubst (2) "P y = P x", simp add:a) 72 apply (clarsimp simp: a) 73 done 74 75end 76