author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45328  e5b33eecbf6e 
child 51717  9e7d1c139569 
permissions  rwrr 
30092
9c3b1c136d1f
Added lemmas for normalizing freshness results involving fresh_star.
berghofe
parents:
29581
diff
changeset

1 
(* Author: Christian Urban and Makarius 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

2 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

3 
The nominal induct proof method. 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

4 
*) 
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 
structure NominalInduct: 
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

7 
sig 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

8 
val nominal_induct_tac: Proof.context > bool > (binding option * (term * bool)) option list list > 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

9 
(string * typ) list > (string * typ) list list > thm list > 
33368  10 
thm list > int > Rule_Cases.cases_tactic 
30549  11 
val nominal_induct_method: (Proof.context > Proof.method) context_parser 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

12 
end = 
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

13 
struct 
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

14 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

15 
(* proper tuples  nested left *) 
18283
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 
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

18 
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

19 

feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

20 
fun tuple_fun Ts (xi, T) = 
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

21 
Library.funpow (length Ts) HOLogic.mk_split 
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

22 
(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

23 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

24 
val split_all_tuples = 
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

25 
Simplifier.full_simplify (HOL_basic_ss addsimps 
37137  26 
[@{thm split_conv}, @{thm split_paired_all}, @{thm unit_all_eq1}, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @ 
30092
9c3b1c136d1f
Added lemmas for normalizing freshness results involving fresh_star.
berghofe
parents:
29581
diff
changeset

27 
@{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim}); 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

28 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

29 

18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset

30 
(* prepare rule *) 
18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

31 

19903  32 
fun inst_mutual_rule ctxt insts avoiding rules = 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

33 
let 
33368  34 
val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules; 
22072  35 
val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule); 
33368  36 
val (cases, consumes) = Rule_Cases.get joined_rule; 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

37 

96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

38 
val l = length rules; 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

39 
val _ = 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

40 
if length insts = l then () 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

41 
else error ("Bad number of instantiations for " ^ string_of_int l ^ " rules"); 
18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

42 

22072  43 
fun subst inst concl = 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

44 
let 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
23591
diff
changeset

45 
val vars = Induct.vars_of concl; 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

46 
val m = length vars and n = length inst; 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

47 
val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule"; 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

48 
val P :: x :: ys = vars; 
33957  49 
val zs = drop (m  n  2) ys; 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

50 
in 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

51 
(P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) :: 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

52 
(x, tuple (map Free avoiding)) :: 
32952  53 
map_filter (fn (z, SOME t) => SOME (z, t)  _ => NONE) (zs ~~ inst) 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

54 
end; 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

55 
val substs = 
32952  56 
map2 subst insts concls > flat > distinct (op =) 
42361  57 
> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt))); 
22072  58 
in 
59 
(((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 

60 
end; 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

61 

18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

62 
fun rename_params_rule internal xs rule = 
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset

63 
let 
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

64 
val tune = 
20072  65 
if internal then Name.internal 
66 
else fn x => the_default x (try Name.dest_internal x); 

18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

67 
val n = length xs; 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

68 
fun rename prem = 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

69 
let 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

70 
val ps = Logic.strip_params prem; 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

71 
val p = length ps; 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

72 
val ys = 
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

73 
if p < n then [] 
33957  74 
else map (tune o #1) (take (p  n) ps) @ xs; 
45328  75 
in Logic.list_rename_params ys prem end; 
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

76 
fun rename_prems prop = 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

77 
let val (As, C) = Logic.strip_horn prop 
18299
af72dfc4b9f9
added rename_params_rule: recover orginal fresh names in subgoals/cases;
wenzelm
parents:
18297
diff
changeset

78 
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

79 
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

80 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

81 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

82 
(* nominal_induct_tac *) 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

83 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

84 
fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts = 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

85 
let 
42361  86 
val thy = Proof_Context.theory_of ctxt; 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

87 
val cert = Thm.cterm_of thy; 
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

88 

24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
23591
diff
changeset

89 
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt >> split_list; 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

90 
val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

91 

19115  92 
val finish_rule = 
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset

93 
split_all_tuples 
26712
e2dcda7b0401
adapted to ProofContext.revert_skolem: extra Name.clean required;
wenzelm
parents:
25985
diff
changeset

94 
#> rename_params_rule true 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42361
diff
changeset

95 
(map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

96 

b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

97 
fun rule_cases ctxt r = 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

98 
let val r' = if simp then Induct.simplified_rule ctxt r else r 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

99 
in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

100 
in 
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset

101 
(fn i => fn st => 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

102 
rules 
19903  103 
> inst_mutual_rule ctxt insts avoiding 
33368  104 
> Rule_Cases.consume (flat defs) facts 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

105 
> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) => 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

106 
(PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j => 
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

107 
(CONJUNCTS (ALLGOALS 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

108 
let 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

109 
val adefs = nth_list atomized_defs (j  1); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

110 
val frees = fold (Term.add_frees o prop_of) adefs []; 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

111 
val xs = nth_list fixings (j  1); 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

112 
val k = nth concls (j  1) + more_consumes 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

113 
in 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

114 
Method.insert_tac (more_facts @ adefs) THEN' 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

115 
(if simp then 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

116 
Induct.rotate_tac k (length adefs) THEN' 
45132  117 
Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs > op @) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

118 
else 
45132  119 
Induct.arbitrary_tac defs_ctxt k xs) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

120 
end) 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
23591
diff
changeset

121 
THEN' Induct.inner_atomize_tac) j)) 
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
23591
diff
changeset

122 
THEN' Induct.atomize_tac) i st > Seq.maps (fn st' => 
26940  123 
Induct.guess_instance ctxt 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
23591
diff
changeset

124 
(finish_rule (Induct.internalize more_consumes rule)) i st' 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

125 
> Seq.maps (fn rule' => 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

126 
CASES (rule_cases ctxt rule' cases) 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

127 
(Tactic.rtac (rename_params_rule false [] rule') i THEN 
42361  128 
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

129 
THEN_ALL_NEW_CASES 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

130 
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

131 
else K all_tac) 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

132 
THEN_ALL_NEW Induct.rulify_tac) 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

133 
end; 
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

134 

f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

135 

18288
feb79a6b274b
proper treatment of tuple/tuple_fun  nest to the left!
wenzelm
parents:
18283
diff
changeset

136 
(* concrete syntax *) 
17870  137 

138 
local 

139 

18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

140 
val avoidingN = "avoiding"; 
20998
714a08286899
To be consistent with "induct", I renamed "fixing" to "arbitrary".
urbanc
parents:
20288
diff
changeset

141 
val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *) 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

142 
val ruleN = "rule"; 
17870  143 

34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

144 
val inst = Scan.lift (Args.$$$ "_") >> K NONE  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

145 
Args.term >> (SOME o rpair false)  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

146 
Scan.lift (Args.$$$ "(")  (Args.term >> (SOME o rpair true))  
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

147 
Scan.lift (Args.$$$ ")"); 
17870  148 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

149 
val def_inst = 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27809
diff
changeset

150 
((Scan.lift (Args.binding  (Args.$$$ "\<equiv>"  Args.$$$ "==")) >> SOME) 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

151 
 (Args.term >> rpair false)) >> SOME  
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

152 
inst >> Option.map (pair NONE); 
18099  153 

27370  154 
val free = Args.context  Args.term >> (fn (_, Free v) => v  (ctxt, t) => 
155 
error ("Bad free variable: " ^ Syntax.string_of_term ctxt t)); 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

156 

f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

157 
fun unless_more_args scan = Scan.unless (Scan.lift 
18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

158 
((Args.$$$ avoidingN  Args.$$$ fixingN  Args.$$$ ruleN)  Args.colon)) scan; 
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

159 

17870  160 

18583
96e1ef2f806f
proper handling of simultaneous goals and mutual rules;
wenzelm
parents:
18311
diff
changeset

161 
val avoiding = Scan.optional (Scan.lift (Args.$$$ avoidingN  Args.colon)  
18297
116fe71fad51
fresh: frees instead of terms, rename corresponding params in rule;
wenzelm
parents:
18288
diff
changeset

162 
Scan.repeat (unless_more_args free)) []; 
17870  163 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

164 
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN  Args.colon)  
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
34907
diff
changeset

165 
Parse.and_list' (Scan.repeat (unless_more_args free))) []; 
17870  166 

19036  167 
val rule_spec = Scan.lift (Args.$$$ "rule"  Args.colon)  Attrib.thms; 
17870  168 

169 
in 

170 

30549  171 
val nominal_induct_method = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
34907
diff
changeset

172 
Args.mode Induct.no_simpN  (Parse.and_list' (Scan.repeat (unless_more_args def_inst))  
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

173 
avoiding  fixing  rule_spec) >> 
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

174 
(fn (no_simp, (((x, y), z), w)) => fn ctxt => 
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30092
diff
changeset

175 
RAW_METHOD_CASES (fn facts => 
34907
b0aaec87751c
Added infrastructure for simplifying equality constraints.
berghofe
parents:
33957
diff
changeset

176 
HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts))); 
17870  177 

178 
end; 

18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

179 

f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset

180 
end; 