author  bulwahn 
Fri, 12 Mar 2010 12:14:31 +0100  
changeset 35757  c2884bec5463 
parent 35646  b32d6c1bdb4d 
child 36468  d7cd6a5aa9c9 
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, 
35646  25 
induct: thm, inducts: thm list, intrs: thm list} 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

26 
val morph_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 
18728  30 
val mono_add: attribute 
31 
val mono_del: attribute 

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

32 
val get_monos: Proof.context > thm list 
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_name: string 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

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

36 
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

37 
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

38 
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

39 
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

40 
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

41 
type inductive_flags = 
33669  42 
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 
43 
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

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

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

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

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

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

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

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

53 
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

54 
val add_inductive_global: inductive_flags > 
29581  55 
((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

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

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

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

59 
val partition_rules: thm > thm list > (string * thm list) list 
25822  60 
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

61 
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

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

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

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

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

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

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

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

71 
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

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

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

74 
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

75 
thm list > binding list > Attrib.src list list > (thm * string list * int) list > 
35646  76 
thm > local_theory > thm list * thm list * thm * thm list * local_theory 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

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

78 
val gen_add_inductive_i: add_ind_def > inductive_flags > 
29581  79 
((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

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

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

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

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

85 
bool > local_theory > inductive_result * local_theory 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26928
diff
changeset

86 
val gen_ind_decl: add_ind_def > bool > 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

87 
OuterParse.token list > (bool > local_theory > local_theory) * OuterParse.token list 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

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

89 

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

90 
structure Inductive: INDUCTIVE = 
5094  91 
struct 
92 

9598  93 

10729  94 
(** theory context references **) 
95 

11991  96 
val inductive_forall_name = "HOL.induct_forall"; 
32602  97 
val inductive_forall_def = @{thm induct_forall_def}; 
11991  98 
val inductive_conj_name = "HOL.induct_conj"; 
32602  99 
val inductive_conj_def = @{thm induct_conj_def}; 
100 
val inductive_conj = @{thms induct_conj}; 

101 
val inductive_atomize = @{thms induct_atomize}; 

102 
val inductive_rulify = @{thms induct_rulify}; 

103 
val inductive_rulify_fallback = @{thms induct_rulify_fallback}; 

10729  104 

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

105 
val notTrueE = TrueI RSN (2, notE); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

106 
val notFalseI = Seq.hd (atac 1 notI); 
32181  107 

108 
val simp_thms' = map mk_meta_eq 

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

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

111 
"(P & True) = P" "(True & P) = P" 

112 
by (fact simp_thms)+}; 

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

113 

32652  114 
val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms'; 
115 

116 
val simp_thms''' = map mk_meta_eq 

117 
[@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}]; 

10729  118 

119 

22846  120 
(** context data **) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

121 

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

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

123 
{preds: term list, elims: thm list, raw_induct: thm, 
35646  124 
induct: thm, inducts: thm list, intrs: thm list}; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

125 

35646  126 
fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs} = 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

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

128 
val term = Morphism.term phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

129 
val thm = Morphism.thm phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

130 
val fact = Morphism.fact phi; 
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

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

132 
{preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, 
35646  133 
induct = thm induct, inducts = fact inducts, intrs = fact intrs} 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

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

135 

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

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

137 
{names: string list, coind: bool} * inductive_result; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

138 

33519  139 
structure InductiveData = Generic_Data 
22846  140 
( 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

141 
type T = inductive_info Symtab.table * thm list; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

142 
val empty = (Symtab.empty, []); 
16432  143 
val extend = I; 
33519  144 
fun merge ((tab1, monos1), (tab2, monos2)) : T = 
24039
273698405054
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23881
diff
changeset

145 
(Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2)); 
22846  146 
); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

147 

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

148 
val get_inductives = InductiveData.get o Context.Proof; 
22846  149 

150 
fun print_inductives ctxt = 

151 
let 

152 
val (tab, monos) = get_inductives ctxt; 

153 
val space = Consts.space_of (ProofContext.consts_of ctxt); 

154 
in 

33095
bbd52d2f8696
renamed NameSpace to Name_Space  also to emphasize its subtle change in semantics;
wenzelm
parents:
33077
diff
changeset

155 
[Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))), 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

156 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] 
22846  157 
> Pretty.chunks > Pretty.writeln 
158 
end; 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

159 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

160 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

161 
(* get and put data *) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

162 

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

163 
fun the_inductive ctxt name = 
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset

164 
(case Symtab.lookup (#1 (get_inductives ctxt)) name of 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

165 
NONE => error ("Unknown (co)inductive predicate " ^ quote name) 
15531  166 
 SOME info => info); 
9598  167 

25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

168 
fun put_inductives names info = InductiveData.map 
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

169 
(apfst (fold (fn name => Symtab.update (name, info)) names)); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

170 

8277  171 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

172 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

173 
(** monotonicity rules **) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

174 

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

175 
val get_monos = #2 o get_inductives; 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

176 
val map_monos = InductiveData.map o apsnd; 
8277  177 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

178 
fun mk_mono thm = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

179 
let 
33933  180 
fun eq2mono thm' = thm' RS (thm' RS eq_to_mono); 
32652  181 
fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) 
182 
handle THM _ => thm RS @{thm le_boolD} 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

183 
in 
33933  184 
case concl_of thm of 
22275
51411098e49b
 Improved handling of monotonicity rules involving <=
berghofe
parents:
22102
diff
changeset

185 
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq) 
35364  186 
 _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
34991
diff
changeset

187 
 _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => 
33933  188 
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL 
189 
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm)) 

190 
 _ => thm 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

191 
end handle THM _ => 
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32035
diff
changeset

192 
error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

193 

33933  194 
val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono); 
195 
val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono); 

7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

196 

bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

197 

7107  198 

10735  199 
(** misc utilities **) 
6424  200 

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

201 
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

202 
fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s; 
5662  203 

6424  204 
fun coind_prefix true = "co" 
205 
 coind_prefix false = ""; 

206 

24133
75063f96618f
added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents:
24039
diff
changeset

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

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

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

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

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

212 

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

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

214 
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

215 

33957  216 
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

217 

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

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

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

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

221 
 find_arg T x ((p as (U, (NONE, y))) :: ps) = 
23577  222 
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

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

224 

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

225 
fun make_args Ts xs = 
28524  226 
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

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

228 

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

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

230 
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

231 

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

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

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

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

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

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

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

240 
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

241 
else NONE 
5094  242 
end; 
243 

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

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

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

246 
 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

247 

6424  248 

249 

10729  250 
(** process rules **) 
251 

252 
local 

5094  253 

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

254 
fun err_in_rule ctxt name t msg = 
16432  255 
error (cat_lines ["Illformed introduction rule " ^ quote name, 
24920  256 
Syntax.string_of_term ctxt t, msg]); 
10729  257 

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

258 
fun err_in_prem ctxt name t p msg = 
24920  259 
error (cat_lines ["Illformed premise", Syntax.string_of_term ctxt p, 
260 
"in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]); 

5094  261 

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

262 
val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; 
10729  263 

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

264 
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

265 

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

266 
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

267 

16432  268 
fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; 
10729  269 

270 
in 

5094  271 

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

272 
fun check_rule ctxt cs params ((binding, att), rule) = 
10729  273 
let 
30218  274 
val err_name = Binding.str_of binding; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

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

278 
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

279 
val rule' = Logic.list_implies (prems, concl); 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

280 
val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

281 
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

282 

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

283 
fun check_ind err t = case dest_predicate cs params t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

287 
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

288 
then err bad_ind_occ else (); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

289 

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

290 
fun check_prem' prem t = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

291 
if head_of t mem cs then 
29006  292 
check_ind (err_in_prem ctxt err_name rule prem) t 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

293 
else (case t of 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

296 
 _ => ()); 
5094  297 

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

299 
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem 
29006  300 
else err_in_prem ctxt err_name rule prem "Nonatomic premise"; 
10729  301 
in 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

302 
(case concl of 
35364  303 
Const (@{const_name Trueprop}, _) $ t => 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

304 
if head_of t mem cs then 
29006  305 
(check_ind (err_in_rule ctxt err_name rule') t; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

306 
List.app check_prem (prems ~~ aprems)) 
29006  307 
else err_in_rule ctxt err_name rule' bad_concl 
308 
 _ => err_in_rule ctxt err_name rule' bad_concl); 

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

309 
((binding, att), arule) 
10729  310 
end; 
5094  311 

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

312 
val rulify = 
18222  313 
hol_simplify inductive_conj 
18463  314 
#> hol_simplify inductive_rulify 
315 
#> hol_simplify inductive_rulify_fallback 

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

316 
#> Simplifier.norm_hhf; 
10729  317 

318 
end; 

319 

5094  320 

6424  321 

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

322 
(** proofs for (co)inductive predicates **) 
6424  323 

26534  324 
(* prove monotonicity *) 
5094  325 

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

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

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

329 
(if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt 
29388
79eb3649ca9e
added fork_mono flag, which is usually enabled in batchmode only;
wenzelm
parents:
29064
diff
changeset

330 
[] [] 
17985  331 
(HOLogic.mk_Trueprop 
24815
f7093e90f36c
tuned internal interfaces: flags record, added kind for results;
wenzelm
parents:
24744
diff
changeset

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

333 
(fn _ => EVERY [rtac @{thm monoI} 1, 
32652  334 
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

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

336 
[atac 1, 
33933  337 
resolve_tac (map mk_mono monos @ get_monos ctxt) 1, 
32652  338 
etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])); 
5094  339 

6424  340 

10735  341 
(* prove introduction rules *) 
5094  342 

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

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

345 
val _ = clean_message quiet_mode " Proving the introduction rules ..."; 
5094  346 

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

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

348 
(mono RS (fp_def RS 
32652  349 
(if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); 
5094  350 

351 
fun select_disj 1 1 = [] 

352 
 select_disj _ 1 = [rtac disjI1] 

353 
 select_disj n i = (rtac disjI2)::(select_disj (n  1) (i  1)); 

354 

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

355 
val rules = [refl, TrueI, notFalseI, exI, conjI]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

356 

22605
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

357 
val intrs = map_index (fn (i, intr) => rulify 
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32952
diff
changeset

358 
(Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

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

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

364 
DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts 
5094  365 

366 
in (intrs, unfold) end; 

367 

6424  368 

10735  369 
(* prove elimination rules *) 
5094  370 

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

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

373 
val _ = clean_message quiet_mode " Proving the elimination rules ..."; 
5094  374 

22605
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

375 
val ([pname], ctxt') = ctxt > 
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

376 
Variable.add_fixes (map (fst o dest_Free) params) > snd > 
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

377 
Variable.variant_fixes ["P"]; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

379 

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

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

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

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

383 

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

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

385 

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

386 
val rules1 = [disjE, exE, FalseE]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

387 
val rules2 = [conjE, FalseE, notTrueE]; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

388 

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

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

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

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

392 
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

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

394 

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

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

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

397 
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

398 
(frees ~~ us) @ ts, P)); 
33317  399 
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

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

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

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

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

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

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

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

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

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

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

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

411 
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))]) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

413 
> singleton (ProofContext.export ctxt'' ctxt), 
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset

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

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

416 

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

417 
in map prove_elim cs end; 
5094  418 

6424  419 

10735  420 
(* derivation of simplified elimination rules *) 
5094  421 

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

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

423 

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

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

427 
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

428 
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

429 

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

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

431 
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

432 

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

433 
in 
9598  434 

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

435 
fun mk_cases ctxt prop = 
7107  436 
let 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

437 
val thy = ProofContext.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

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

439 

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

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

441 
error (Pretty.string_of (Pretty.block 
24920  442 
[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

443 

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

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

445 

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

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

447 
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

448 
fun mk_elim rl = 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

449 
Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl)) 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

450 
> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); 
7107  451 
in 
452 
(case get_first (try mk_elim) elims of 

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

454 
 NONE => err "Proposition not an inductive predicate:") 
7107  455 
end; 
456 

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

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

458 

7107  459 

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

460 
(* inductive_cases *) 
7107  461 

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

462 
fun gen_inductive_cases prep_att prep_prop args lthy = 
9598  463 
let 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

464 
val thy = ProofContext.theory_of lthy; 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

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

466 
((a, map (prep_att thy) atts), 
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

467 
map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); 
33671  468 
in lthy > Local_Theory.notes facts >> map snd end; 
5094  469 

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

470 
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

471 
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; 
7107  472 

6424  473 

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

474 
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

475 
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

476 
(Scan.lift (Scan.repeat1 Args.name_source  
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

477 
Scan.optional (Args.$$$ "for"  Scan.repeat1 Args.name) []) >> 
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

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

479 
let 
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

480 
val (_, ctxt') = Variable.add_fixes fixes 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

481 
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

482 
val ctxt'' = fold Variable.declare_term props 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

483 
val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') 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

484 
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

485 
"dynamic case analysis on predicates"; 
9598  486 

487 

10735  488 
(* prove induction rule *) 
5094  489 

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

490 
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

491 
fp_def rec_preds_defs ctxt = 
5094  492 
let 
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset

493 
val _ = clean_message quiet_mode " Proving the induction rule ..."; 
20047  494 
val thy = ProofContext.theory_of ctxt; 
5094  495 

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

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

497 

22605
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

498 
val (pnames, ctxt') = ctxt > 
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

499 
Variable.add_fixes (map (fst o dest_Free) params) > snd > 
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

500 
Variable.variant_fixes (mk_names "P" (length cs)); 
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

501 
val preds = map2 (curry Free) pnames 
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset

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

503 

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

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

505 

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

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

507 
let 
33669  508 
fun subst s = 
509 
(case dest_predicate cs params s of 

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

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

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

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

513 
val bs = map Bound (k  1 downto 0); 
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

514 
val P = list_comb (List.nth (preds, i), 
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset

515 
map (incr_boundvars k) ys @ bs); 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

518 
(list_comb (incr_boundvars k s, bs), P)) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

519 
in (Q, case Ts of [] => SOME (s, P)  _ => NONE) end 
33669  520 
 NONE => 
521 
(case s of 

522 
(t $ u) => (fst (subst t) $ fst (subst u), NONE) 

523 
 (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE) 

524 
 _ => (s, NONE))); 

7293  525 

33338  526 
fun mk_prem s prems = 
527 
(case subst s of 

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

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

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

530 

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

531 
val SOME (_, i, ys, _) = dest_predicate cs params 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

532 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

533 

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

534 
in list_all_free (Logic.strip_params r, 
33338  535 
Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem 
536 
(map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), 

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

537 
HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys)))) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

539 

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

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

541 

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

542 

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

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

544 

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

545 
val Tss = map (binder_types o fastype_of) preds; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

546 
val (xnames, ctxt'') = 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

547 
Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

548 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

549 
(map (fn (((xnames, Ts), c), P) => 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

552 
(list_comb (c, params @ frees), list_comb (P, frees)) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

553 
end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); 
5094  554 

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

555 

5094  556 
(* make predicate for instantiation of abstract induction rule *) 
557 

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

558 
val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj 
33338  559 
(map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) 
560 
(make_bool_args HOLogic.mk_not I bs i) 

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

5094  562 

563 
val ind_concl = HOLogic.mk_Trueprop 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
34991
diff
changeset

564 
(HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); 
5094  565 

32652  566 
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

567 

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

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

571 
DETERM (rtac raw_fp_induct 1), 
32652  572 
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1), 
32610
c477b0a62ce9
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
haftmann
parents:
32602
diff
changeset

573 
rewrite_goals_tac simp_thms'', 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

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

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

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

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

581 
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule 
32610
c477b0a62ce9
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
haftmann
parents:
32602
diff
changeset

582 
(inductive_conj_def :: rec_preds_defs @ simp_thms'') prem, 
22980
1226d861eefb
Fixed bug that caused proof of induction theorem to fail if
berghofe
parents:
22846
diff
changeset

583 
conjI, refl] 1)) prems)]); 
5094  584 

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

585 
val lemma = Skip_Proof.prove ctxt'' [] [] 
17985  586 
(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

587 
[rewrite_goals_tac rec_preds_defs, 
5094  588 
REPEAT (EVERY 
589 
[REPEAT (resolve_tac [conjI, impI] 1), 

32652  590 
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

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

592 
rewrite_goals_tac simp_thms', 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

593 
atac 1])]) 
5094  594 

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

595 
in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end; 
5094  596 

6424  597 

598 

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

599 
(** specification of (co)inductive predicates **) 
10729  600 

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

601 
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

602 
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

603 
let 
24915  604 
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; 
5094  605 

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

606 
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

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

608 
val predT = replicate k HOLogic.boolT > argTs > HOLogic.boolT; 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

609 
val p :: xs = map Free (Variable.variant_frees lthy intr_ts 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

610 
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

611 
val bs = map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

612 
(map (rpair HOLogic.boolT) (mk_names "b" k))); 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

613 

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

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

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

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

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

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

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

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

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

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

624 
end 
33669  625 
 NONE => 
626 
(case t of 

627 
t1 $ t2 => subst t1 $ subst t2 

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

629 
 _ => t)); 

5149  630 

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

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

634 
(* b_j & x_j = u & p b_j t & ... *) 
5094  635 

636 
fun transform_rule r = 

637 
let 

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

638 
val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

639 
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

640 
val ps = make_bool_args HOLogic.mk_not I bs i @ 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

641 
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

642 
map (subst o HOLogic.dest_Trueprop) 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

643 
(Logic.strip_assums_hyp r) 
33338  644 
in 
645 
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) 

646 
(Logic.strip_params r) 

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

5094  648 
end 
649 

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

651 

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

652 
val fp_fun = fold_rev lambda (p :: bs @ xs) 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

653 
(if null intr_ts then HOLogic.false_const 
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

654 
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); 
5094  655 

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

656 
(* add definiton of recursive predicates to theory *) 
5094  657 

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

658 
val rec_name = 
28965  659 
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

660 
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

661 
else alt_name; 
5094  662 

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

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

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

666 
((rec_name, case cnames_syn of [(_, syn)] => syn  _ => NoSyn), 
33577
ea36b70a6c1c
added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
blanchet
parents:
33317
diff
changeset

667 
((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]), 
ea36b70a6c1c
added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
blanchet
parents:
33317
diff
changeset

668 
fold_rev lambda params 
33278  669 
(Const (fp_name, (predT > predT) > predT) $ fp_fun))) 
33671  670 
> Local_Theory.restore_naming lthy; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

671 
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def]) 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

672 
(cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params))); 
33278  673 
val specs = 
674 
if length cs < 2 then [] 

675 
else 

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

677 
let 

678 
val Ts = arg_types_of (length params) c; 

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

679 
val xs = map Free (Variable.variant_frees lthy intr_ts 
33278  680 
(mk_names "x" (length Ts) ~~ Ts)) 
681 
in 

682 
(name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs) 

683 
(list_comb (rec_const, params @ make_bool_args' bs i @ 

684 
make_args argTs (xs ~~ Ts))))) 

685 
end) (cnames_syn ~~ cs); 

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

686 
val (consts_defs, lthy'') = lthy' 
33671  687 
> Local_Theory.conceal 
33766
c679f05600cd
adapted Local_Theory.define  eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset

688 
> fold_map Local_Theory.define specs 
33671  689 
> Local_Theory.restore_naming lthy'; 
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset

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

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

692 
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''; 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

693 
val ((_, [mono']), lthy''') = 
33671  694 
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy''; 
5094  695 

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

696 
in (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

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

698 
end; 
5094  699 

33669  700 
fun declare_rules rec_binding coind no_ind cnames 
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset

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

702 
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

703 
val rec_name = Binding.name_of rec_binding; 
32773  704 
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

705 
val intr_names = map Binding.name_of intr_bindings; 
33368  706 
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

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

708 
if coind then 
33368  709 
(raw_induct, [Rule_Cases.case_names [rec_name], 
710 
Rule_Cases.case_conclusion (rec_name, intr_names), 

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

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

712 
else if no_ind orelse length cnames > 1 then 
33368  713 
(raw_induct, [ind_case_names, Rule_Cases.consumes 0]) 
714 
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

715 

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

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

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

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

719 
(if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) > 
33671  720 
Local_Theory.notes 
33278  721 
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~ 
722 
map (fn th => [([th], 

33369  723 
[Attrib.internal (K (Context_Rules.intro_query NONE)), 
33056
791a4655cae3
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
blanchet
parents:
33051
diff
changeset

724 
Attrib.internal (K Nitpick_Intros.add)])]) intrs) >> 
24744
dcb8cf5fc99c
 add_inductive_i now takes typ instead of typ option as argument
berghofe
parents:
24721
diff
changeset

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

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

727 
lthy1 > 
33671  728 
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

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

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

732 
[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

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

734 
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

735 
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

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

737 
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) >> 
33671  738 
Local_Theory.note 
32773  739 
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), 
28107  740 
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

741 

35646  742 
val (inducts, lthy3) = 
743 
if no_ind orelse coind then ([], lthy2) 

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

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

745 
let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

746 
lthy2 > 
33671  747 
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

748 
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

749 
[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

750 
Attrib.internal (K (Rule_Cases.consumes 1)), 
35646  751 
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

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

754 

26534  755 
type inductive_flags = 
33669  756 
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, 
757 
no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}; 

26534  758 

759 
type add_ind_def = 

760 
inductive_flags > 

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

761 
term list > (Attrib.binding * term) list > thm list > 
29581  762 
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

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

764 

33669  765 
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

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

767 
let 
25288  768 
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

769 
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

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

771 
("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

772 

33671  773 
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

774 
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

775 
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

776 

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

777 
val (lthy1, 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

778 
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

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

780 

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

781 
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs) 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

782 
params intr_ts rec_preds_defs lthy1; 
33459  783 
val elims = 
784 
if no_elim then [] 

785 
else 

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

787 
unfold rec_preds_defs lthy1; 

22605
41b092e7d89a
 Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset

788 
val raw_induct = zero_var_indexes 
33459  789 
(if no_ind then Drule.asm_rl 
790 
else if coind then 

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

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

792 
(snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1) 
35625  793 
(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

794 
(fold_rule rec_preds_defs 
32652  795 
(rewrite_rule simp_thms''' 
796 
(mono RS (fp_def RS @{thm def_coinduct})))))) 

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

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

798 
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

799 
rec_preds_defs lthy1); 
5094  800 

35646  801 
val (intrs', elims', induct, inducts, lthy2) = declare_rules rec_name coind no_ind 
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset

802 
cnames preds intrs intr_names intr_atts elims raw_induct lthy1; 
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

803 

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

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

805 
{preds = preds, 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

806 
intrs = intrs', 
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset

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

808 
raw_induct = rulify raw_induct, 
35646  809 
induct = induct, 
810 
inducts = inducts}; 

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

811 

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

812 
val lthy3 = lthy2 
33671  813 
> Local_Theory.declaration false (fn phi => 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

814 
let val result' = morph_result phi result; 
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

815 
in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end); 
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

816 
in (result, lthy3) end; 
5094  817 

6424  818 

10735  819 
(* external interfaces *) 
5094  820 

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

821 
fun gen_add_inductive_i mk_def 
33669  822 
(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

823 
cnames_syn pnames spec monos lthy = 
5094  824 
let 
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset

825 
val thy = ProofContext.theory_of lthy; 
6424  826 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
5094  827 

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

828 

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

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

830 

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

831 
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

832 

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

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

834 
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

835 
let 
29006  836 
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

837 
error "Abbreviations may not have names or attributes"; 
35624  838 
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

839 
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

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

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

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

843 
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

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

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

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

847 

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

848 
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

849 
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

850 

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

851 

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

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

853 

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

854 
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

855 
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

856 
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

857 
val ps = map Free pnames; 
5094  858 

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

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

25143
2a1acc88a180
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
wenzelm
parents:
25114
diff
changeset

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

863 

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

864 
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

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

866 
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

867 
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

868 
 _ => I) r []), r); 
5094  869 

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

870 
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

871 
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

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

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

874 
> mk_def flags cs intros monos ps preds 
33671  875 
> 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

876 
end; 
5094  877 

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

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

880 
val ((vars, intrs), _) = lthy 
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

881 
> ProofContext.set_mode ProofContext.mode_abbrev 
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

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

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

26128  887 
in 
888 
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

889 
> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos 
26128  890 
end; 
5094  891 

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

892 
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

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

894 

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

895 
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

896 
let 
29006  897 
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

898 
val ctxt' = thy 
33553  899 
> Theory_Target.init NONE 
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

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

902 
val info = #2 (the_inductive ctxt' name); 
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset

903 
in (info, ProofContext.theory_of ctxt') end; 
6424  904 

905 

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

906 
(* 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

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

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

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

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

911 

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

912 
(* 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

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

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

915 
val (_ $ t $ u :: _) = 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

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

917 
val (_, ts) = strip_comb t; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

918 
val (_, us) = strip_comb u 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

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

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

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

922 

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

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

924 
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

925 

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

926 
(* partition introduction rules according to predicate name *) 
25822  927 
fun gen_partition_rules f induct intros = 
928 
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

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

930 

25822  931 
val partition_rules = gen_partition_rules I; 
932 
fun partition_rules' induct = gen_partition_rules fst induct; 

933 

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

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

935 
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

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

937 

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

938 
(* 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

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

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

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

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

943 
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

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

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

946 
val params = Logic.strip_params t; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

947 
val vars = map (Var o apfst (rpair 0)) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

948 
(Name.variant_list used (map fst params) ~~ map snd params); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

949 
val ts = map (curry subst_bounds (rev vars)) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

950 
(List.drop (Logic.strip_assums_hyp t, arity)); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

951 
val us = Logic.strip_imp_prems u; 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

952 
val tab = fold (Pattern.first_order_match thy) (ts ~~ us) 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

953 
(Vartab.empty, Vartab.empty); 
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset

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

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

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

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

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

960 

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

961 

25978  962 

6437  963 
(** package setup **) 
964 

965 
(* setup theory *) 

966 

8634  967 
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

968 
ind_cases_setup #> 
30528  969 
Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del) 
970 
"declaration of monotonicity rule"; 

6437  971 

972 

973 
(* outer syntax *) 

6424  974 

17057  975 
local structure P = OuterParse and K = OuterKeyword in 
6424  976 

27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27252
diff
changeset

977 
val _ = OuterKeyword.keyword "monos"; 
24867  978 

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

979 
fun gen_ind_decl mk_def coind = 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

980 
P.fixes  P.for_fixes  
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

981 
Scan.optional SpecParse.where_alt_specs []  
22102  982 
Scan.optional (P.$$$ "monos"  P.!!! SpecParse.xthms1) [] 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26928
diff
changeset

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

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

985 

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

986 
val ind_decl = gen_ind_decl add_ind_def; 
6424  987 

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

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

989 
OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

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

991 

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

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

993 
OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl 
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset

994 
(ind_decl true); 
6723  995 

24867  996 
val _ = 
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26928
diff
changeset

997 
OuterSyntax.local_theory "inductive_cases" 
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset

998 
"create simplified instances of elimination rules (improper)" K.thy_script 
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset

999 
(P.and_list1 SpecParse.specs >> (snd oo inductive_cases)); 
7107  1000 

5094  1001 
end; 
6424  1002 

1003 
end; 