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