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