author | wenzelm |
Wed, 30 Nov 2005 15:24:32 +0100 | |
changeset 18299 | af72dfc4b9f9 |
parent 18297 | 116fe71fad51 |
child 18311 | b83b00cbaecf |
permissions | -rw-r--r-- |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
1 |
(* ID: $Id$ |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
2 |
Author: Christian Urban and Makarius |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
3 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
4 |
The nominal induct proof method. |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
5 |
*) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
6 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
7 |
structure NominalInduct: |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
8 |
sig |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
9 |
val nominal_induct_tac: Proof.context -> (string option * term) option list -> |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
10 |
(string * typ) list -> (string * typ) list list -> thm -> |
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
11 |
thm list -> int -> RuleCases.cases_tactic |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
12 |
val nominal_induct_method: Method.src -> Proof.context -> Method.method |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
13 |
end = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
14 |
struct |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
15 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
16 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
17 |
(* proper tuples -- nested left *) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
18 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
19 |
fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
20 |
fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
21 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
22 |
fun tuple_fun Ts (xi, T) = |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
23 |
Library.funpow (length Ts) HOLogic.mk_split |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
24 |
(Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
25 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
26 |
val split_all_tuples = |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
27 |
Simplifier.full_simplify (HOL_basic_ss addsimps |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
28 |
[split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
29 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
30 |
|
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
31 |
(* prepare rule *) |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
32 |
|
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
33 |
(*conclusion: ?P fresh_struct ... insts*) |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
34 |
fun inst_rule thy insts fresh rule = |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
35 |
let |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
36 |
val vars = InductAttrib.vars_of (Thm.concl_of rule); |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
37 |
val m = length vars and n = length insts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
38 |
val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule"; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
39 |
val P :: x :: ys = vars; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
40 |
val zs = Library.drop (m - n - 2, ys); |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
41 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
42 |
val subst = |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
43 |
(P, tuple_fun (map #2 fresh) (Term.dest_Var P)) :: |
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
44 |
(x, tuple (map Free fresh)) :: |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
45 |
List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ insts); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
46 |
in |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
47 |
rule |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
48 |
|> Drule.cterm_instantiate (map (pairself (Thm.cterm_of thy)) subst) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
49 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
50 |
|
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
51 |
fun rename_params_rule internal xs rule = |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
52 |
let |
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
53 |
val tune = |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
54 |
if internal then Syntax.internal |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
55 |
else fn x => the_default x (try Syntax.dest_internal x); |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
56 |
val n = length xs; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
57 |
fun rename prem = |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
58 |
let |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
59 |
val ps = Logic.strip_params prem; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
60 |
val p = length ps; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
61 |
val ys = |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
62 |
if p < n then [] |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
63 |
else map (tune o #1) (Library.take (p - n, ps)) @ xs; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
64 |
in Logic.list_rename_params (ys, prem) end; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
65 |
fun rename_prems prop = |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
66 |
let val (As, C) = Logic.strip_horn (Thm.prop_of rule) |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
67 |
in Logic.list_implies (map rename As, C) end; |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
68 |
in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
69 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
70 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
71 |
(* nominal_induct_tac *) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
72 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
73 |
fun nominal_induct_tac ctxt def_insts fresh fixing rule facts = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
74 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
75 |
val thy = ProofContext.theory_of ctxt; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
76 |
val cert = Thm.cterm_of thy; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
77 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
78 |
val ((insts, defs), defs_ctxt) = InductMethod.add_defs def_insts ctxt; |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
79 |
val atomized_defs = map ObjectLogic.atomize_thm defs; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
80 |
|
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
81 |
val finish_rule = |
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
82 |
split_all_tuples |
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
83 |
#> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o #1) fresh); |
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
84 |
fun rule_cases r = RuleCases.make true (SOME (Thm.prop_of r)) (InductMethod.rulified_term r); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
85 |
in |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
86 |
(fn i => fn st => |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
87 |
rule |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
88 |
|> `RuleCases.get |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
89 |
||> inst_rule thy insts fresh |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
90 |
|> RuleCases.consume defs facts |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
91 |
|> Seq.maps (fn ((cases, (k, more_facts)), r) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
92 |
(CONJUNCTS (ALLGOALS (fn j => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
93 |
Method.insert_tac (more_facts @ atomized_defs) j |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
94 |
THEN InductMethod.fix_tac defs_ctxt k (Library.nth_list fixing (j - 1)) j)) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
95 |
THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' => |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
96 |
InductMethod.guess_instance (finish_rule r) i st' |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
97 |
|> Seq.maps (fn r' => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
98 |
CASES (rule_cases r' cases) |
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset
|
99 |
(Tactic.rtac (rename_params_rule false [] r') i THEN |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
100 |
PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st')))) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
101 |
THEN_ALL_NEW_CASES InductMethod.rulify_tac |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
102 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
103 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
104 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
105 |
(* concrete syntax *) |
17870 | 106 |
|
107 |
local |
|
108 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
109 |
val freshN = "fresh"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
110 |
val fixingN = "fixing"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
111 |
val ruleN = "rule"; |
17870 | 112 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
113 |
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME; |
17870 | 114 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
115 |
val def_inst = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
116 |
((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
117 |
-- Args.local_term) >> SOME || |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
118 |
inst >> Option.map (pair NONE); |
18099 | 119 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
120 |
val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
121 |
error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t)); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
122 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
123 |
fun unless_more_args scan = Scan.unless (Scan.lift |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
124 |
((Args.$$$ freshN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
125 |
|
17870 | 126 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
127 |
val def_insts = Scan.repeat (unless_more_args def_inst); |
17870 | 128 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
129 |
val fresh = Scan.optional (Scan.lift (Args.$$$ freshN -- Args.colon) |-- |
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset
|
130 |
Scan.repeat (unless_more_args free)) []; |
17870 | 131 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
132 |
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |-- |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
133 |
Args.and_list1 (Scan.repeat (unless_more_args free))) []; |
17870 | 134 |
|
135 |
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm; |
|
136 |
||
137 |
in |
|
138 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
139 |
fun nominal_induct_method src = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
140 |
Method.syntax (def_insts -- fresh -- fixing -- rule_spec) src |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
141 |
#> (fn (ctxt, (((x, y), z), w)) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
142 |
Method.RAW_METHOD_CASES (fn facts => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
143 |
HEADGOAL (nominal_induct_tac ctxt x y z w facts))); |
17870 | 144 |
|
145 |
end; |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
146 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
147 |
end; |