author  wenzelm 
Sun, 27 Nov 2011 22:03:22 +0100  
changeset 45651  172aa230ce69 
parent 45649  2d995773da1a 
child 45652  18214436e1d3 
permissions  rwrr 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

1 
(* Title: HOL/Tools/inductive.ML 
5094  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
5094  4 

6424  5 
(Co)Inductive Definition module for HOL. 
5094  6 

7 
Features: 

6424  8 
* least or greatest fixedpoints 
9 
* mutually recursive definitions 

10 
* definitions involving arbitrary monotone operators 

11 
* automatically proves introduction and elimination rules 

5094  12 

13 
Introduction rules have the form 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

14 
[ M Pj ti, ..., Q x, ... ] ==> Pk t 
5094  15 
where M is some monotone operator (usually the identity) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

16 
Q x is any side condition on the free variables 
5094  17 
ti, t are any terms 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

18 
Pj, Pk are two of the predicates being defined in mutual recursion 
5094  19 
*) 
20 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

21 
signature BASIC_INDUCTIVE = 
5094  22 
sig 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

23 
type inductive_result = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

24 
{preds: term list, elims: thm list, raw_induct: thm, 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

25 
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} 
45290  26 
val transform_result: morphism > inductive_result > inductive_result 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

27 
type inductive_info = {names: string list, coind: bool} * inductive_result 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

28 
val the_inductive: Proof.context > string > inductive_info 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

29 
val print_inductives: Proof.context > unit 
45651  30 
val get_monos: Proof.context > thm list 
18728  31 
val mono_add: attribute 
32 
val mono_del: attribute 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

33 
val mk_cases: Proof.context > term > thm 
10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

34 
val inductive_forall_def: thm 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

35 
val rulify: thm > thm 
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28791
diff
changeset

36 
val inductive_cases: (Attrib.binding * string list) list > local_theory > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

37 
thm list list * local_theory 
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28791
diff
changeset

38 
val inductive_cases_i: (Attrib.binding * term list) list > local_theory > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

39 
thm list list * local_theory 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

40 
type inductive_flags = 
33669  41 
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 
42 
no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool} 

24815
f7093e90f36c
tuned internal interfaces: flags record, added kind for results;
wenzelm
parents:
24744
diff
changeset

43 
val add_inductive_i: 
29581  44 
inductive_flags > ((binding * typ) * mixfix) list > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

45 
(string * typ) list > (Attrib.binding * term) list > thm list > local_theory > 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

46 
inductive_result * local_theory 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

47 
val add_inductive: bool > bool > 
29581  48 
(binding * string option * mixfix) list > 
49 
(binding * string option * mixfix) list > 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

50 
(Attrib.binding * string) list > 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

51 
(Facts.ref * Attrib.src list) list > 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

52 
bool > local_theory > inductive_result * local_theory 
33726
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

53 
val add_inductive_global: inductive_flags > 
29581  54 
((binding * typ) * mixfix) list > (string * typ) list > (Attrib.binding * term) list > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

55 
thm list > theory > inductive_result * theory 
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

56 
val arities_of: thm > (string * int) list 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

57 
val params_of: thm > term list 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

58 
val partition_rules: thm > thm list > (string * thm list) list 
25822  59 
val partition_rules': thm > (thm * 'a) list > (string * (thm * 'a) list) list 
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

60 
val unpartition_rules: thm list > (string * 'a list) list > 'a list 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

61 
val infer_intro_vars: thm > int > thm list > term list list 
18708  62 
val setup: theory > theory 
5094  63 
end; 
64 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

65 
signature INDUCTIVE = 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

66 
sig 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

67 
include BASIC_INDUCTIVE 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

68 
type add_ind_def = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

69 
inductive_flags > 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

70 
term list > (Attrib.binding * term) list > thm list > 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

71 
term list > (binding * mixfix) list > 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

72 
local_theory > inductive_result * local_theory 
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset

73 
val declare_rules: binding > bool > bool > string list > term list > 
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset

74 
thm list > binding list > Attrib.src list list > (thm * string list * int) list > 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

75 
thm list > thm > local_theory > thm list * thm list * thm list * thm * thm list * local_theory 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

76 
val add_ind_def: add_ind_def 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

77 
val gen_add_inductive_i: add_ind_def > inductive_flags > 
29581  78 
((binding * typ) * mixfix) list > (string * typ) list > (Attrib.binding * term) list > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

79 
thm list > local_theory > inductive_result * local_theory 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

80 
val gen_add_inductive: add_ind_def > bool > bool > 
29581  81 
(binding * string option * mixfix) list > 
82 
(binding * string option * mixfix) list > 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

83 
(Attrib.binding * string) list > (Facts.ref * Attrib.src list) list > 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

84 
bool > local_theory > inductive_result * local_theory 
36958  85 
val gen_ind_decl: add_ind_def > bool > (bool > local_theory > local_theory) parser 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

86 
end; 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

87 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset

88 
structure Inductive: INDUCTIVE = 
5094  89 
struct 
90 

10729  91 
(** theory context references **) 
92 

32602  93 
val inductive_forall_def = @{thm induct_forall_def}; 
11991  94 
val inductive_conj_name = "HOL.induct_conj"; 
32602  95 
val inductive_conj_def = @{thm induct_conj_def}; 
96 
val inductive_conj = @{thms induct_conj}; 

97 
val inductive_atomize = @{thms induct_atomize}; 

98 
val inductive_rulify = @{thms induct_rulify}; 

99 
val inductive_rulify_fallback = @{thms induct_rulify_fallback}; 

10729  100 

45649  101 
val simp_thms1 = 
102 
map mk_meta_eq 

103 
@{lemma "(~ True) = False" "(~ False) = True" 

104 
"(True > P) = P" "(False > P) = True" 

105 
"(P & True) = P" "(True & P) = P" 

106 
by (fact simp_thms)+}; 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

107 

45649  108 
val simp_thms2 = 
109 
map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1; 

32652  110 

45649  111 
val simp_thms3 = 
112 
map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; 

10729  113 

114 

45647  115 

10735  116 
(** misc utilities **) 
6424  117 

26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

118 
fun message quiet_mode s = if quiet_mode then () else writeln s; 
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

119 
fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s; 
5662  120 

6424  121 
fun coind_prefix true = "co" 
122 
 coind_prefix false = ""; 

123 

45651  124 
fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n; 
6424  125 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

126 
fun make_bool_args f g [] i = [] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

127 
 make_bool_args f g (x :: xs) i = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

128 
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

129 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

130 
fun make_bool_args' xs = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

131 
make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

132 

33957  133 
fun arg_types_of k c = drop k (binder_types (fastype_of c)); 
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

134 

40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
39248
diff
changeset

135 
fun find_arg T x [] = raise Fail "find_arg" 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

136 
 find_arg T x ((p as (_, (SOME _, _))) :: ps) = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

137 
apsnd (cons p) (find_arg T x ps) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

138 
 find_arg T x ((p as (U, (NONE, y))) :: ps) = 
23577  139 
if (T: typ) = U then (y, (U, (SOME x, y)) :: ps) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

140 
else apsnd (cons p) (find_arg T x ps); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

141 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

142 
fun make_args Ts xs = 
28524  143 
map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T)  (_, (SOME t, ())) => t) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

144 
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts)); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

145 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

146 
fun make_args' Ts xs Us = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

147 
fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs)); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

148 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

149 
fun dest_predicate cs params t = 
5094  150 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

151 
val k = length params; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

152 
val (c, ts) = strip_comb t; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

153 
val (xs, ys) = chop k ts; 
31986  154 
val i = find_index (fn c' => c' = c) cs; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

155 
in 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

156 
if xs = params andalso i >= 0 then 
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

157 
SOME (c, i, ys, chop (length ys) (arg_types_of k c)) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

158 
else NONE 
5094  159 
end; 
160 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

161 
fun mk_names a 0 = [] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

162 
 mk_names a 1 = [a] 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

163 
 mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

164 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

165 
fun select_disj 1 1 = [] 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

166 
 select_disj _ 1 = [rtac disjI1] 
45647  167 
 select_disj n i = rtac disjI2 :: select_disj (n  1) (i  1); 
168 

6424  169 

170 

45651  171 
(** context data **) 
172 

173 
type inductive_result = 

174 
{preds: term list, elims: thm list, raw_induct: thm, 

175 
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; 

176 

177 
fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} = 

178 
let 

179 
val term = Morphism.term phi; 

180 
val thm = Morphism.thm phi; 

181 
val fact = Morphism.fact phi; 

182 
in 

183 
{preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, 

184 
induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs} 

185 
end; 

186 

187 
type inductive_info = {names: string list, coind: bool} * inductive_result; 

188 

189 
val empty_equations = 

190 
Item_Net.init 

191 
(op aconv o pairself Thm.prop_of) 

192 
(single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); (* FIXME fragile wrt. morphisms *) 

193 

194 
datatype data = Data of 

195 
{infos: inductive_info Symtab.table, 

196 
monos: thm list, 

197 
equations: thm Item_Net.T}; 

198 

199 
fun make_data (infos, monos, equations) = 

200 
Data {infos = infos, monos = monos, equations = equations}; 

201 

202 
structure Data = Generic_Data 

203 
( 

204 
type T = data; 

205 
val empty = make_data (Symtab.empty, [], empty_equations); 

206 
val extend = I; 

207 
fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, 

208 
Data {infos = infos2, monos = monos2, equations = equations2}) = 

209 
make_data (Symtab.merge (K true) (infos1, infos2), 

210 
Thm.merge_thms (monos1, monos2), 

211 
Item_Net.merge (equations1, equations2)); 

212 
); 

213 

214 
fun map_data f = 

215 
Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations))); 

216 

217 
fun rep_data ctxt = Data.get (Context.Proof ctxt) > (fn Data rep => rep); 

218 

219 
fun print_inductives ctxt = 

220 
let 

221 
val {infos, monos, ...} = rep_data ctxt; 

222 
val space = Consts.space_of (Proof_Context.consts_of ctxt); 

223 
in 

224 
[Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, infos))), 

225 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] 

226 
> Pretty.chunks > Pretty.writeln 

227 
end; 

228 

229 

230 
(* inductive info *) 

231 

232 
fun the_inductive ctxt name = 

233 
(case Symtab.lookup (#infos (rep_data ctxt)) name of 

234 
NONE => error ("Unknown (co)inductive predicate " ^ quote name) 

235 
 SOME info => info); 

236 

237 
fun put_inductives names info = 

238 
map_data (fn (infos, monos, equations) => 

239 
(fold (fn name => Symtab.update (name, info)) names infos, monos, equations)); 

240 

241 

242 
(* monotonicity rules *) 

243 

244 
val get_monos = #monos o rep_data; 

245 

246 
fun mk_mono ctxt thm = 

247 
let 

248 
fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono}); 

249 
fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) 

250 
handle THM _ => thm RS @{thm le_boolD} 

251 
in 

252 
(case concl_of thm of 

253 
Const ("==", _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) 

254 
 _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm 

255 
 _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => 

256 
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL 

257 
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) 

258 
 _ => thm) 

259 
end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); 

260 

261 
val mono_add = 

262 
Thm.declaration_attribute (fn thm => fn context => 

263 
map_data (fn (infos, monos, equations) => 

264 
(infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); 

265 

266 
val mono_del = 

267 
Thm.declaration_attribute (fn thm => fn context => 

268 
map_data (fn (infos, monos, equations) => 

269 
(infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); 

270 

271 

272 
(* equations *) 

273 

274 
val get_equations = #equations o rep_data; 

275 

276 
val equation_add = 

277 
Thm.declaration_attribute (fn thm => 

278 
map_data (fn (infos, monos, equations) => (infos, monos, Item_Net.update thm equations))); 

279 

280 

281 

10729  282 
(** process rules **) 
283 

284 
local 

5094  285 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

286 
fun err_in_rule ctxt name t msg = 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset

287 
error (cat_lines ["Illformed introduction rule " ^ Binding.print name, 
24920  288 
Syntax.string_of_term ctxt t, msg]); 
10729  289 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

290 
fun err_in_prem ctxt name t p msg = 
24920  291 
error (cat_lines ["Illformed premise", Syntax.string_of_term ctxt p, 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset

292 
"in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]); 
5094  293 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

294 
val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; 
10729  295 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

296 
val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

297 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

298 
val bad_app = "Inductive predicate must be applied to parameter(s) "; 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

299 

41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41075
diff
changeset

300 
fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize []; 
10729  301 

302 
in 

5094  303 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

304 
fun check_rule ctxt cs params ((binding, att), rule) = 
10729  305 
let 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

306 
val params' = Term.variant_frees rule (Logic.strip_params rule); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

307 
val frees = rev (map Free params'); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

308 
val concl = subst_bounds (frees, Logic.strip_assums_concl rule); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

309 
val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

310 
val rule' = Logic.list_implies (prems, concl); 
42361  311 
val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

312 
val arule = list_all_free (params', Logic.list_implies (aprems, concl)); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

313 

45647  314 
fun check_ind err t = 
315 
(case dest_predicate cs params t of 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

316 
NONE => err (bad_app ^ 
24920  317 
commas (map (Syntax.string_of_term ctxt) params)) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

318 
 SOME (_, _, ys, _) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

319 
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs 
45647  320 
then err bad_ind_occ else ()); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

321 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

322 
fun check_prem' prem t = 
36692
54b64d4ad524
farewell to oldstyle mem infixes  type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36642
diff
changeset

323 
if member (op =) cs (head_of t) then 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset

324 
check_ind (err_in_prem ctxt binding rule prem) t 
45647  325 
else 
326 
(case t of 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

327 
Abs (_, _, t) => check_prem' prem t 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

328 
 t $ u => (check_prem' prem t; check_prem' prem u) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

329 
 _ => ()); 
5094  330 

10729  331 
fun check_prem (prem, aprem) = 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

332 
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem 
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset

333 
else err_in_prem ctxt binding rule prem "Nonatomic premise"; 
45647  334 

335 
val _ = 

336 
(case concl of 

337 
Const (@{const_name Trueprop}, _) $ t => 

338 
if member (op =) cs (head_of t) then 

42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset

339 
(check_ind (err_in_rule ctxt binding rule') t; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

340 
List.app check_prem (prems ~~ aprems)) 
45647  341 
else err_in_rule ctxt binding rule' bad_concl 
342 
 _ => err_in_rule ctxt binding rule' bad_concl); 

343 
in 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

344 
((binding, att), arule) 
10729  345 
end; 
5094  346 

24744
dcb8cf5fc99c
 add_inductive_i now takes typ instead of typ option as argument
berghofe
parents:
24721
diff
changeset

347 
val rulify = 
18222  348 
hol_simplify inductive_conj 
18463  349 
#> hol_simplify inductive_rulify 
350 
#> hol_simplify inductive_rulify_fallback 

30552
58db56278478
provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
wenzelm
parents:
30528
diff
changeset

351 
#> Simplifier.norm_hhf; 
10729  352 

353 
end; 

354 

5094  355 

6424  356 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

357 
(** proofs for (co)inductive predicates **) 
6424  358 

26534  359 
(* prove monotonicity *) 
5094  360 

36642  361 
fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt = 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

362 
(message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono) 
26534  363 
" Proving monotonicity ..."; 
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32952
diff
changeset

364 
(if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt 
36642  365 
[] [] 
17985  366 
(HOLogic.mk_Trueprop 
24815
f7093e90f36c
tuned internal interfaces: flags record, added kind for results;
wenzelm
parents:
24744
diff
changeset

367 
(Const (@{const_name Orderings.mono}, (predT > predT) > HOLogic.boolT) $ fp_fun)) 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

368 
(fn _ => EVERY [rtac @{thm monoI} 1, 
32652  369 
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1), 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

370 
REPEAT (FIRST 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

371 
[atac 1, 
42439
9efdd0af15ac
eliminated Display.string_of_thm_without_context;
wenzelm
parents:
42381
diff
changeset

372 
resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1, 
32652  373 
etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])); 
5094  374 

6424  375 

10735  376 
(* prove introduction rules *) 
5094  377 

36642  378 
fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' = 
5094  379 
let 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

380 
val _ = clean_message quiet_mode " Proving the introduction rules ..."; 
5094  381 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

382 
val unfold = funpow k (fn th => th RS fun_cong) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

383 
(mono RS (fp_def RS 
32652  384 
(if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); 
5094  385 

45648  386 
val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

387 

36642  388 
val intrs = map_index (fn (i, intr) => 
389 
Skip_Proof.prove ctxt [] [] intr (fn _ => EVERY 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

390 
[rewrite_goals_tac rec_preds_defs, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

391 
rtac (unfold RS iffD2) 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

392 
EVERY1 (select_disj (length intr_ts) (i + 1)), 
17985  393 
(*Not ares_tac, since refl must be tried before any equality assumptions; 
394 
backtracking may occur if the premises have extra variables!*) 

36642  395 
DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) 
42361  396 
> singleton (Proof_Context.export ctxt ctxt')) intr_ts 
5094  397 

398 
in (intrs, unfold) end; 

399 

6424  400 

10735  401 
(* prove elimination rules *) 
5094  402 

36642  403 
fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' = 
5094  404 
let 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

405 
val _ = clean_message quiet_mode " Proving the elimination rules ..."; 
5094  406 

36642  407 
val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

408 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

409 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

410 
fun dest_intr r = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

411 
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

412 
Logic.strip_assums_hyp r, Logic.strip_params r); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

413 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

414 
val intrs = map dest_intr intr_ts ~~ intr_names; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

415 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

416 
val rules1 = [disjE, exE, FalseE]; 
45648  417 
val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}]; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

418 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

419 
fun prove_elim c = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

420 
let 
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

421 
val Ts = arg_types_of (length params) c; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

422 
val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt'; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

423 
val frees = map Free (anames ~~ Ts); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

424 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

425 
fun mk_elim_prem ((_, _, us, _), ts, params') = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

426 
list_all (params', 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

427 
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

428 
(frees ~~ us) @ ts, P)); 
33317  429 
val c_intrs = filter (equal c o #1 o #1 o #1) intrs; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

430 
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) :: 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

431 
map mk_elim_prem (map #1 c_intrs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

432 
in 
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32952
diff
changeset

433 
(Skip_Proof.prove ctxt'' [] prems P 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

434 
(fn {prems, ...} => EVERY 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

435 
[cut_facts_tac [hd prems] 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

436 
rewrite_goals_tac rec_preds_defs, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

437 
dtac (unfold RS iffD1) 1, 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

438 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

439 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

440 
EVERY (map (fn prem => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

441 
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) 
42361  442 
> singleton (Proof_Context.export ctxt'' ctxt'''), 
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset

443 
map #2 c_intrs, length Ts) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

444 
end 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

445 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

446 
in map prove_elim cs end; 
5094  447 

45647  448 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

449 
(* prove simplification equations *) 
6424  450 

45647  451 
fun prove_eqs quiet_mode cs params intr_ts intrs 
452 
(elims: (thm * bstring list * int) list) ctxt ctxt'' = (* FIXME ctxt'' ?? *) 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

453 
let 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

454 
val _ = clean_message quiet_mode " Proving the simplification rules ..."; 
45647  455 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

456 
fun dest_intr r = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

457 
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

458 
Logic.strip_assums_hyp r, Logic.strip_params r); 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

459 
val intr_ts' = map dest_intr intr_ts; 
45647  460 

37901  461 
fun prove_eq c (elim: thm * 'a * 'b) = 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

462 
let 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

463 
val Ts = arg_types_of (length params) c; 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

464 
val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt; 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

465 
val frees = map Free (anames ~~ Ts); 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

466 
val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs); 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

467 
fun mk_intr_conj (((_, _, us, _), ts, params'), _) = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

468 
let 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

469 
fun list_ex ([], t) = t 
45647  470 
 list_ex ((a, T) :: vars, t) = 
471 
HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t)); 

472 
val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts); 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

473 
in 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

474 
list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

475 
end; 
45647  476 
val lhs = list_comb (c, params @ frees); 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

477 
val rhs = 
45647  478 
if null c_intrs then @{term False} 
479 
else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); 

480 
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

481 
fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

482 
let 
45647  483 
val (prems', last_prem) = split_last prems; 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

484 
in 
45647  485 
EVERY1 (select_disj (length c_intrs) (i + 1)) THEN 
486 
EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN 

487 
EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN 

488 
rtac last_prem 1 

489 
end) ctxt' 1; 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

490 
fun prove_intr2 (((_, _, us, _), ts, params'), intr) = 
45647  491 
EVERY (replicate (length params') (etac @{thm exE} 1)) THEN 
492 
EVERY (replicate (length ts + length us  1) (etac @{thm conjE} 1)) THEN 

493 
Subgoal.FOCUS_PREMS (fn {params, prems, ...} => 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

494 
let 
45647  495 
val (eqs, prems') = chop (length us) prems; 
496 
val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

497 
in 
45647  498 
rewrite_goal_tac rew_thms 1 THEN 
499 
rtac intr 1 THEN 

500 
EVERY (map (fn p => rtac p 1) prems') 

501 
end) ctxt' 1; 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

502 
in 
45647  503 
Skip_Proof.prove ctxt' [] [] eq (fn _ => 
504 
rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN 

505 
EVERY (map_index prove_intr1 c_intrs) THEN 

506 
(if null c_intrs then etac @{thm FalseE} 1 

507 
else 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

508 
let val (c_intrs', last_c_intr) = split_last c_intrs in 
45647  509 
EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN 
510 
prove_intr2 last_c_intr 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

511 
end)) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

512 
> rulify 
42361  513 
> singleton (Proof_Context.export ctxt' ctxt'') 
45647  514 
end; 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

515 
in 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

516 
map2 prove_eq cs elims 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

517 
end; 
45647  518 

519 

10735  520 
(* derivation of simplified elimination rules *) 
5094  521 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

522 
local 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

523 

d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

524 
(*delete needless equality assumptions*) 
29064  525 
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} 
22838  526 
(fn _ => assume_tac 1); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

527 
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; 
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

528 
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

529 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

530 
fun simp_case_tac ss i = 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

531 
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

532 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

533 
in 
9598  534 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

535 
fun mk_cases ctxt prop = 
7107  536 
let 
42361  537 
val thy = Proof_Context.theory_of ctxt; 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32091
diff
changeset

538 
val ss = simpset_of ctxt; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

539 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

540 
fun err msg = 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

541 
error (Pretty.string_of (Pretty.block 
24920  542 
[Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop])); 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

543 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset

544 
val elims = Induct.find_casesP ctxt prop; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

545 

7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

546 
val cprop = Thm.cterm_of thy prop; 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

547 
val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

548 
fun mk_elim rl = 
36546  549 
Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl)) 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

550 
> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); 
7107  551 
in 
552 
(case get_first (try mk_elim) elims of 

15531  553 
SOME r => r 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

554 
 NONE => err "Proposition not an inductive predicate:") 
7107  555 
end; 
556 

11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

557 
end; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

558 

45647  559 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

560 
(* inductive_cases *) 
7107  561 

21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

562 
fun gen_inductive_cases prep_att prep_prop args lthy = 
9598  563 
let 
42361  564 
val thy = Proof_Context.theory_of lthy; 
37957
00e848690339
inductive_cases: crude parallelization via Par_List.map;
wenzelm
parents:
37901
diff
changeset

565 
val facts = args > Par_List.map (fn ((a, atts), props) => 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

566 
((a, map (prep_att thy) atts), 
37957
00e848690339
inductive_cases: crude parallelization via Par_List.map;
wenzelm
parents:
37901
diff
changeset

567 
Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); 
33671  568 
in lthy > Local_Theory.notes facts >> map snd end; 
5094  569 

24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24133
diff
changeset

570 
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop; 
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24133
diff
changeset

571 
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; 
7107  572 

6424  573 

30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

574 
val ind_cases_setup = 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

575 
Method.setup @{binding ind_cases} 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

576 
(Scan.lift (Scan.repeat1 Args.name_source  
42491
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42439
diff
changeset

577 
Scan.optional (Args.$$$ "for"  Scan.repeat1 Args.binding) []) >> 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

578 
(fn (raw_props, fixes) => fn ctxt => 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

579 
let 
42491
4bb5de0aae66
more precise position information via Variable.add_fixes_binding;
wenzelm
parents:
42439
diff
changeset

580 
val (_, ctxt') = Variable.add_fixes_binding fixes ctxt; 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

581 
val props = Syntax.read_props ctxt' raw_props; 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

582 
val ctxt'' = fold Variable.declare_term props ctxt'; 
42361  583 
val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props) 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

584 
in Method.erule 0 rules end)) 
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

585 
"dynamic case analysis on predicates"; 
9598  586 

45647  587 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

588 
(* derivation of simplified equation *) 
9598  589 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

590 
fun mk_simp_eq ctxt prop = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

591 
let 
45647  592 
val thy = Proof_Context.theory_of ctxt; 
593 
val ctxt' = Variable.auto_fixes prop ctxt; 

594 
val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of; 

595 
val substs = 

45649  596 
Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop) 
38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

597 
> map_filter 
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

598 
(fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop) 
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

599 
(Vartab.empty, Vartab.empty), eq) 
45647  600 
handle Pattern.MATCH => NONE); 
601 
val (subst, eq) = 

602 
(case substs of 

38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

603 
[s] => s 
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

604 
 _ => error 
45647  605 
("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")); 
606 
val inst = 

607 
map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) 

608 
(Term.add_vars (lhs_of eq) []); 

609 
in 

45651  610 
Drule.cterm_instantiate inst eq 
45647  611 
> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite (simpset_of ctxt)))) 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

612 
> singleton (Variable.export ctxt' ctxt) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

613 
end 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

614 

45647  615 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

616 
(* inductive simps *) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

617 

489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

618 
fun gen_inductive_simps prep_att prep_prop args lthy = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

619 
let 
42361  620 
val thy = Proof_Context.theory_of lthy; 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

621 
val facts = args > map (fn ((a, atts), props) => 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

622 
((a, map (prep_att thy) atts), 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

623 
map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

624 
in lthy > Local_Theory.notes facts >> map snd end; 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

625 

489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

626 
val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop; 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

627 
val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop; 
40902  628 

45647  629 

10735  630 
(* prove induction rule *) 
5094  631 

26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

632 
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono 
45647  633 
fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *) 
5094  634 
let 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

635 
val _ = clean_message quiet_mode " Proving the induction rule ..."; 
5094  636 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

637 
(* predicates for induction rule *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

638 

36642  639 
val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt; 
45647  640 
val preds = 
641 
map2 (curry Free) pnames 

642 
(map (fn c => arg_types_of (length params) c > HOLogic.boolT) cs); 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

643 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

644 
(* transform an introduction rule into a premise for induction rule *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

645 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

646 
fun mk_ind_prem r = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

647 
let 
33669  648 
fun subst s = 
649 
(case dest_predicate cs params s of 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

650 
SOME (_, i, ys, (_, Ts)) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

651 
let 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

652 
val k = length Ts; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

653 
val bs = map Bound (k  1 downto 0); 
42364  654 
val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

655 
val Q = list_abs (mk_names "x" k ~~ Ts, 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

656 
HOLogic.mk_binop inductive_conj_name 
45647  657 
(list_comb (incr_boundvars k s, bs), P)); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

658 
in (Q, case Ts of [] => SOME (s, P)  _ => NONE) end 
33669  659 
 NONE => 
660 
(case s of 

45647  661 
t $ u => (fst (subst t) $ fst (subst u), NONE) 
662 
 Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE) 

33669  663 
 _ => (s, NONE))); 
7293  664 

33338  665 
fun mk_prem s prems = 
666 
(case subst s of 

667 
(_, SOME (t, u)) => t :: u :: prems 

668 
 (t, _) => t :: prems); 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

669 

45647  670 
val SOME (_, i, ys, _) = 
671 
dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 

42364  672 
in 
673 
list_all_free (Logic.strip_params r, 

674 
Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem 

675 
(map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), 

676 
HOLogic.mk_Trueprop (list_comb (nth preds i, ys)))) 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

677 
end; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

678 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

679 
val ind_prems = map mk_ind_prem intr_ts; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

680 

21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

681 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

682 
(* make conclusions for induction rules *) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

683 

63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

684 
val Tss = map (binder_types o fastype_of) preds; 
45647  685 
val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; 
686 
val mutual_ind_concl = 

687 
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

688 
(map (fn (((xnames, Ts), c), P) => 
45647  689 
let val frees = map Free (xnames ~~ Ts) 
690 
in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end) 

691 
(unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); 

5094  692 

13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

693 

5094  694 
(* make predicate for instantiation of abstract induction rule *) 
695 

45647  696 
val ind_pred = 
697 
fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj 

698 
(map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) 

699 
(make_bool_args HOLogic.mk_not I bs i) 

700 
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); 

5094  701 

45647  702 
val ind_concl = 
703 
HOLogic.mk_Trueprop 

704 
(HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); 

5094  705 

45647  706 
val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

707 

32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32952
diff
changeset

708 
val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl 
20248  709 
(fn {prems, ...} => EVERY 
17985  710 
[rewrite_goals_tac [inductive_conj_def], 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

711 
DETERM (rtac raw_fp_induct 1), 
32652  712 
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1), 
45649  713 
rewrite_goals_tac simp_thms2, 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

714 
(*This disjE separates out the introduction rules*) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

715 
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), 
5094  716 
(*Now break down the individual cases. No disjE here in case 
717 
some premise involves disjunction.*) 

13747
bf308fcfd08e
Better treatment of equality in premises of inductive definitions. Less
paulson
parents:
13709
diff
changeset

718 
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

719 
REPEAT (FIRSTGOAL 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

720 
(resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

721 
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule 
45649  722 
(inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, 
22980
1226d861eefb
Fixed bug that caused proof of induction theorem to fail if
berghofe
parents:
22846
diff
changeset

723 
conjI, refl] 1)) prems)]); 
5094  724 

32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32952
diff
changeset

725 
val lemma = Skip_Proof.prove ctxt'' [] [] 
17985  726 
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

727 
[rewrite_goals_tac rec_preds_defs, 
5094  728 
REPEAT (EVERY 
729 
[REPEAT (resolve_tac [conjI, impI] 1), 

32652  730 
REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

731 
atac 1, 
45649  732 
rewrite_goals_tac simp_thms1, 
45647  733 
atac 1])]); 
5094  734 

42361  735 
in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; 
5094  736 

6424  737 

738 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

739 
(** specification of (co)inductive predicates **) 
10729  740 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

741 
fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

742 
cs intr_ts monos params cnames_syn lthy = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

743 
let 
24915  744 
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; 
5094  745 

33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

746 
val argTs = fold (combine (op =) o arg_types_of (length params)) cs []; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

747 
val k = log 2 1 (length cs); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

748 
val predT = replicate k HOLogic.boolT > argTs > HOLogic.boolT; 
45647  749 
val p :: xs = 
750 
map Free (Variable.variant_frees lthy intr_ts 

751 
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); 

752 
val bs = 

753 
map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) 

754 
(map (rpair HOLogic.boolT) (mk_names "b" k))); 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

755 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

756 
fun subst t = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

757 
(case dest_predicate cs params t of 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

758 
SOME (_, i, ts, (Ts, Us)) => 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

759 
let 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

760 
val l = length Us; 
33669  761 
val zs = map Bound (l  1 downto 0); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

762 
in 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

763 
list_abs (map (pair "z") Us, list_comb (p, 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

764 
make_bool_args' bs i @ make_args argTs 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

765 
((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us)))) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

766 
end 
33669  767 
 NONE => 
768 
(case t of 

769 
t1 $ t2 => subst t1 $ subst t2 

770 
 Abs (x, T, u) => Abs (x, T, subst u) 

771 
 _ => t)); 

5149  772 

5094  773 
(* transform an introduction rule into a conjunction *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

774 
(* [ p_i t; ... ] ==> p_j u *) 
5094  775 
(* is transformed into *) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

776 
(* b_j & x_j = u & p b_j t & ... *) 
5094  777 

778 
fun transform_rule r = 

779 
let 

45647  780 
val SOME (_, i, ts, (Ts, _)) = 
781 
dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 

782 
val ps = 

783 
make_bool_args HOLogic.mk_not I bs i @ 

21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

784 
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ 
45647  785 
map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r); 
33338  786 
in 
787 
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) 

788 
(Logic.strip_params r) 

789 
(if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps) 

45647  790 
end; 
5094  791 

792 
(* make a disjunction of all introduction rules *) 

793 

45647  794 
val fp_fun = 
795 
fold_rev lambda (p :: bs @ xs) 

796 
(if null intr_ts then HOLogic.false_const 

797 
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); 

5094  798 

21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

799 
(* add definiton of recursive predicates to theory *) 
5094  800 

28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

801 
val rec_name = 
28965  802 
if Binding.is_empty alt_name then 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

803 
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

804 
else alt_name; 
5094  805 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

806 
val ((rec_const, (_, fp_def)), lthy') = lthy 
33671  807 
> Local_Theory.conceal 
33766
c679f05600cd
adapted Local_Theory.define  eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset

808 
> Local_Theory.define 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

809 
((rec_name, case cnames_syn of [(_, syn)] => syn  _ => NoSyn), 
45592  810 
((Binding.empty, @{attributes [nitpick_unfold]}), 
811 
fold_rev lambda params 

812 
(Const (fp_name, (predT > predT) > predT) $ fp_fun))) 

33671  813 
> Local_Theory.restore_naming lthy; 
45647  814 
val fp_def' = 
815 
Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) 

816 
(cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params))); 

33278  817 
val specs = 
818 
if length cs < 2 then [] 

819 
else 

820 
map_index (fn (i, (name_mx, c)) => 

821 
let 

822 
val Ts = arg_types_of (length params) c; 

45647  823 
val xs = 
824 
map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts)); 

33278  825 
in 
39248
4a3747517552
only conceal primitive definition theorems, not predicate names
haftmann
parents:
38864
diff
changeset

826 
(name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs) 
33278  827 
(list_comb (rec_const, params @ make_bool_args' bs i @ 
828 
make_args argTs (xs ~~ Ts))))) 

829 
end) (cnames_syn ~~ cs); 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

830 
val (consts_defs, lthy'') = lthy' 
39248
4a3747517552
only conceal primitive definition theorems, not predicate names
haftmann
parents:
38864
diff
changeset

831 
> fold_map Local_Theory.define specs; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

832 
val preds = (case cs of [_] => [rec_const]  _ => map #1 consts_defs); 
5094  833 

36642  834 
val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; 
835 
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'''; 

836 
val (_, lthy'''') = 

837 
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, 

42361  838 
Proof_Context.export lthy''' lthy'' [mono]) lthy''; 
5094  839 

36642  840 
in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs, 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

841 
list_comb (rec_const, params), preds, argTs, bs, xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

842 
end; 
5094  843 

33669  844 
fun declare_rules rec_binding coind no_ind cnames 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

845 
preds intrs intr_bindings intr_atts elims eqs raw_induct lthy = 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

846 
let 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

847 
val rec_name = Binding.name_of rec_binding; 
32773  848 
fun rec_qualified qualified = Binding.qualify qualified rec_name; 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

849 
val intr_names = map Binding.name_of intr_bindings; 
33368  850 
val ind_case_names = Rule_Cases.case_names intr_names; 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

851 
val induct = 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

852 
if coind then 
33368  853 
(raw_induct, [Rule_Cases.case_names [rec_name], 
854 
Rule_Cases.case_conclusion (rec_name, intr_names), 

855 
Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)]) 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

856 
else if no_ind orelse length cnames > 1 then 
33368  857 
(raw_induct, [ind_case_names, Rule_Cases.consumes 0]) 
858 
else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]); 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

859 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

860 
val (intrs', lthy1) = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

861 
lthy > 
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset

862 
Spec_Rules.add 
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset

863 
(if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) > 
33671  864 
Local_Theory.notes 
33278  865 
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~ 
866 
map (fn th => [([th], 

37264
8b931fb51cc6
removed "nitpick_intro" attribute  Nitpick noew uses Spec_Rules instead
blanchet
parents:
36960
diff
changeset

867 
[Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) >> 
24744
dcb8cf5fc99c
 add_inductive_i now takes typ instead of typ option as argument
berghofe
parents:
24721
diff
changeset

868 
map (hd o snd); 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

869 
val (((_, elims'), (_, [induct'])), lthy2) = 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

870 
lthy1 > 
33671  871 
Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') >> 
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset

872 
fold_map (fn (name, (elim, cases, k)) => 
33671  873 
Local_Theory.note 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

874 
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

875 
[Attrib.internal (K (Rule_Cases.case_names cases)), 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

876 
Attrib.internal (K (Rule_Cases.consumes 1)), 
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset

877 
Attrib.internal (K (Rule_Cases.constraints k)), 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

878 
Attrib.internal (K (Induct.cases_pred name)), 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

879 
Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #> 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

880 
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) >> 
33671  881 
Local_Theory.note 
32773  882 
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), 
28107  883 
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

884 

45647  885 
val (eqs', lthy3) = lthy2 > 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

886 
fold_map (fn (name, eq) => Local_Theory.note 
38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset

887 
((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), 
45651  888 
[Attrib.internal (K equation_add)]), [eq]) 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

889 
#> apfst (hd o snd)) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

890 
(if null eqs then [] else (cnames ~~ eqs)) 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

891 
val (inducts, lthy4) = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

892 
if no_ind orelse coind then ([], lthy3) 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

893 
else 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

894 
let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

895 
lthy3 > 
33671  896 
Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

897 
inducts > map (fn (name, th) => ([th], 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

898 
[Attrib.internal (K ind_case_names), 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

899 
Attrib.internal (K (Rule_Cases.consumes 1)), 
35646  900 
Attrib.internal (K (Induct.induct_pred name))])))] >> snd o hd 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

901 
end; 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

902 
in (intrs', elims', eqs', induct', inducts, lthy4) end; 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

903 

26534  904 
type inductive_flags = 
33669  905 
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 
906 
no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}; 

26534  907 

908 
type add_ind_def = 

909 
inductive_flags > 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

910 
term list > (Attrib.binding * term) list > thm list > 
29581  911 
term list > (binding * mixfix) list > 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

912 
local_theory > inductive_result * local_theory; 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

913 

33669  914 
fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono} 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

915 
cs intros monos params cnames_syn lthy = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

916 
let 
25288  917 
val _ = null cnames_syn andalso error "No inductive predicates given"; 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

918 
val names = map (Binding.name_of o fst) cnames_syn; 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

919 
val _ = message (quiet_mode andalso not verbose) 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

920 
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

921 

33671  922 
val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *) 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

923 
val ((intr_names, intr_atts), intr_ts) = 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

924 
apfst split_list (split_list (map (check_rule lthy cs params) intros)); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

925 

36642  926 
val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

927 
argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

928 
monos params cnames_syn lthy; 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

929 

26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

930 
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs) 
36642  931 
intr_ts rec_preds_defs lthy2 lthy1; 
33459  932 
val elims = 
933 
if no_elim then [] 

934 
else 

935 
prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names) 

36642  936 
unfold rec_preds_defs lthy2 lthy1; 
22605
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

937 
val raw_induct = zero_var_indexes 
33459  938 
(if no_ind then Drule.asm_rl 
939 
else if coind then 

42361  940 
singleton (Proof_Context.export lthy2 lthy1) 
35625  941 
(rotate_prems ~1 (Object_Logic.rulify 
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not wellformed tactics due to change of main conclusion;
wenzelm
parents:
28791
diff
changeset

942 
(fold_rule rec_preds_defs 
45649  943 
(rewrite_rule simp_thms3 
32652  944 
(mono RS (fp_def RS @{thm def_coinduct})))))) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

945 
else 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

946 
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def 
36642  947 
rec_preds_defs lthy2 lthy1); 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

948 
val eqs = 
45647  949 
if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1; 
5094  950 

45647  951 
val elims' = map (fn (th, ns, i) => (rulify th, ns, i)) elims; 
952 
val intrs' = map rulify intrs; 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

953 

45647  954 
val (intrs'', elims'', eqs', induct, inducts, lthy3) = 
955 
declare_rules rec_name coind no_ind 

956 
cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1; 

21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

957 

e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

958 
val result = 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

959 
{preds = preds, 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

960 
intrs = intrs'', 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

961 
elims = elims'', 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

962 
raw_induct = rulify raw_induct, 
35646  963 
induct = induct, 
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

964 
inducts = inducts, 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

965 
eqs = eqs'}; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

966 

36642  967 
val lthy4 = lthy3 
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset

968 
> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => 
45290  969 
let val result' = transform_result phi result; 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

970 
in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end); 
36642  971 
in (result, lthy4) end; 
5094  972 

6424  973 

10735  974 
(* external interfaces *) 
5094  975 

26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

976 
fun gen_add_inductive_i mk_def 
33669  977 
(flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}) 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

978 
cnames_syn pnames spec monos lthy = 
5094  979 
let 
42361  980 
val thy = Proof_Context.theory_of lthy; 
6424  981 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
5094  982 

21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

983 

25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

984 
(* abbrevs *) 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

985 

30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

986 
val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy; 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

987 

25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

988 
fun get_abbrev ((name, atts), t) = 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

989 
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

990 
let 
29006  991 
val _ = Binding.is_empty name andalso null atts orelse 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

992 
error "Abbreviations may not have names or attributes"; 
35624  993 
val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t)); 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

994 
val var = 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

995 
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

996 
NONE => error ("Undeclared head of abbreviation " ^ quote x) 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

997 
 SOME ((b, T'), mx) => 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

998 
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x) 
28083
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

999 
else (b, mx)); 
103d9282a946
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27882
diff
changeset

1000 
in SOME (var, rhs) end 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1001 
else NONE; 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

1002 

25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1003 
val abbrevs = map_filter get_abbrev spec; 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

1004 
val bs = map (Binding.name_of o fst o fst) abbrevs; 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1005 

21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

1006 

25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1007 
(* predicates *) 
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset

1008 

25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1009 
val pre_intros = filter_out (is_some o get_abbrev) spec; 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

1010 
val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn; 
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

1011 
val cs = map (Free o apfst Binding.name_of o fst) cnames_syn'; 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1012 
val ps = map Free pnames; 
5094  1013 

30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

1014 
val (_, ctxt2) = lthy > Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn'); 
35624  1015 
val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs; 
1016 
val ctxt3 = ctxt2 > fold (snd oo Local_Defs.fixed_abbrev) abbrevs; 

42361  1017 
val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy; 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1018 

3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1019 
fun close_rule r = list_all_free (rev (fold_aterms 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

1020 
(fn t as Free (v as (s, _)) => 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1021 
if Variable.is_fixed ctxt1 s orelse 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1022 
member (op =) ps t then I else insert (op =) v 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1023 
 _ => I) r []), r); 
5094  1024 

26736
e6091328718f
added explicit check phase after reading of specification
haftmann
parents:
26534
diff
changeset

1025 
val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros; 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1026 
val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn'; 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

1027 
in 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1028 
lthy 
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

1029 
> mk_def flags cs intros monos ps preds 
33671  1030 
> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

1031 
end; 
5094  1032 

29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

1033 
fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy = 
5094  1034 
let 
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

1035 
val ((vars, intrs), _) = lthy 
42361  1036 
> Proof_Context.set_mode Proof_Context.mode_abbrev 
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

1037 
> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs; 
24721  1038 
val (cs, ps) = chop (length cnames_syn) vars; 
1039 
val monos = Attrib.eval_thms lthy raw_monos; 

33669  1040 
val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty, 
1041 
coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int}; 

26128  1042 
in 
1043 
lthy 

30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset

1044 
> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos 
26128  1045 
end; 
5094  1046 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1047 
val add_inductive_i = gen_add_inductive_i add_ind_def; 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1048 
val add_inductive = gen_add_inductive add_ind_def; 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1049 

33726
0878aecbf119
eliminated slightly odd name space grouping  now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset

1050 
fun add_inductive_global flags cnames_syn pnames pre_intros monos thy = 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

1051 
let 
29006  1052 
val name = Sign.full_name thy (fst (fst (hd cnames_syn))); 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

1053 
val ctxt' = thy 
38388  1054 
> Named_Target.theory_init 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

1055 
> add_inductive_i flags cnames_syn pnames pre_intros monos > snd 
33671  1056 
> Local_Theory.exit; 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

1057 
val info = #2 (the_inductive ctxt' name); 
42361  1058 
in (info, Proof_Context.theory_of ctxt') end; 
6424  1059 

1060 

22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1061 
(* read off arities of inductive predicates from raw induction rule *) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1062 
fun arities_of induct = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1063 
map (fn (_ $ t $ u) => 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1064 
(fst (dest_Const (head_of t)), length (snd (strip_comb u)))) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1065 
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1066 

4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1067 
(* read off parameters of inductive predicate from raw induction rule *) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1068 
fun params_of induct = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1069 
let 
45647  1070 
val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); 
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1071 
val (_, ts) = strip_comb t; 
45647  1072 
val (_, us) = strip_comb u; 
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1073 
in 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1074 
List.take (ts, length ts  length us) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1075 
end; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1076 

4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1077 
val pname_of_intr = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1078 
concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1079 

4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1080 
(* partition introduction rules according to predicate name *) 
25822  1081 
fun gen_partition_rules f induct intros = 
1082 
fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros 

22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1083 
(map (rpair [] o fst) (arities_of induct)); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1084 

25822  1085 
val partition_rules = gen_partition_rules I; 
1086 
fun partition_rules' induct = gen_partition_rules fst induct; 

1087 

22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1088 
fun unpartition_rules intros xs = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1089 
fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1090 
(fn x :: xs => (x, xs)) #>> the) intros xs > fst; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1091 

4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1092 
(* infer order of variables in intro rules from order of quantifiers in elim rule *) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1093 
fun infer_intro_vars elim arity intros = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1094 
let 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1095 
val thy = theory_of_thm elim; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1096 
val _ :: cases = prems_of elim; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1097 
val used = map (fst o fst) (Term.add_vars (prop_of elim) []); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1098 
fun mtch (t, u) = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1099 
let 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1100 
val params = Logic.strip_params t; 
45647  1101 
val vars = 
1102 
map (Var o apfst (rpair 0)) 

1103 
(Name.variant_list used (map fst params) ~~ map snd params); 

1104 
val ts = 

1105 
map (curry subst_bounds (rev vars)) 

1106 
(List.drop (Logic.strip_assums_hyp t, arity)); 

22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1107 
val us = Logic.strip_imp_prems u; 
45647  1108 
val tab = 
1109 
fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty); 

22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1110 
in 
32035  1111 
map (Envir.subst_term tab) vars 
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1112 
end 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1113 
in 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1114 
map (mtch o apsnd prop_of) (cases ~~ intros) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1115 
end; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1116 

4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

1117 

25978  1118 

6437  1119 
(** package setup **) 
1120 

1121 
(* setup theory *) 

1122 

8634  1123 
val setup = 
30722
623d4831c8cf
simplified attribute and method setup: eliminating bottomup styles makes it easier to keep things in one place, and also SML/NJ happy;
wenzelm
parents:
30552
diff
changeset

1124 
ind_cases_setup #> 
30528  1125 
Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del) 
1126 
"declaration of monotonicity rule"; 

6437  1127 

1128 

1129 
(* outer syntax *) 

6424  1130 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1131 
val _ = Keyword.keyword "monos"; 
24867  1132 

23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1133 
fun gen_ind_decl mk_def coind = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1134 
Parse.fixes  Parse.for_fixes  
36954  1135 
Scan.optional Parse_Spec.where_alt_specs []  
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1136 
Scan.optional (Parse.$$$ "monos"  Parse.!!! Parse_Spec.xthms1) [] 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26928
diff
changeset

1137 
>> (fn (((preds, params), specs), monos) => 
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

1138 
(snd oo gen_add_inductive mk_def true coind preds params specs monos)); 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1139 

24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

1140 
val ind_decl = gen_ind_decl add_ind_def; 
6424  1141 

33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

1142 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1143 
Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

1144 
(ind_decl false); 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

1145 

ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

1146 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1147 
Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

1148 
(ind_decl true); 
6723  1149 

24867  1150 
val _ = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1151 
Outer_Syntax.local_theory "inductive_cases" 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1152 
"create simplified instances of elimination rules (improper)" Keyword.thy_script 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset

1153 
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases)); 
7107  1154 

37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

1155 
val _ = 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

1156 
Outer_Syntax.local_theory "inductive_simps" 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

1157 
"create simplification rules for inductive predicates" Keyword.thy_script 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

1158 
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); 
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset

1159 

5094  1160 
end; 