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