author  haftmann 
Mon, 19 Sep 2005 16:38:35 +0200  
changeset 17485  c39871c52977 
parent 17412  e26cb20ef0cc 
child 17959  8db36a108213 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

10735  4 
Author: Stefan Berghofer, TU Muenchen 
5 
Author: Markus Wenzel, TU Muenchen 

5094  6 

6424  7 
(Co)Inductive Definition module for HOL. 
5094  8 

9 
Features: 

6424  10 
* least or greatest fixedpoints 
11 
* userspecified product and sum constructions 

12 
* mutually recursive definitions 

13 
* definitions involving arbitrary monotone operators 

14 
* automatically proves introduction and elimination rules 

5094  15 

6424  16 
The recursive sets must *already* be declared as constants in the 
17 
current theory! 

5094  18 

19 
Introduction rules have the form 

8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

20 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk 
5094  21 
where M is some monotone operator (usually the identity) 
22 
P(x) is any side condition on the free variables 

23 
ti, t are any terms 

24 
Sj, Sk are two of the sets being defined in mutual recursion 

25 

6424  26 
Sums are used only for mutual recursion. Products are used only to 
27 
derive "streamlined" induction rules for relations. 

5094  28 
*) 
29 

30 
signature INDUCTIVE_PACKAGE = 

31 
sig 

6424  32 
val quiet_mode: bool ref 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

33 
val trace: bool ref 
16432  34 
val unify_consts: theory > term list > term list > term list * term list 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

35 
val split_rule_vars: term list > thm > thm 
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

36 
val get_inductive: theory > string > ({names: string list, coind: bool} * 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

37 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

38 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}) option 
12400  39 
val the_mk_cases: theory > string > string > thm 
6437  40 
val print_inductives: theory > unit 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

43 
val get_monos: theory > thm list 
10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

44 
val inductive_forall_name: string 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

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

46 
val rulify: thm > thm 
15703  47 
val inductive_cases: ((bstring * Attrib.src list) * string list) list > theory > theory 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

48 
val inductive_cases_i: ((bstring * theory attribute list) * term list) list > theory > theory 
6424  49 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
12180  50 
((bstring * term) * theory attribute list) list > thm list > theory > theory * 
6424  51 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  52 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
11628  53 
val add_inductive: bool > bool > string list > 
15703  54 
((bstring * string) * Attrib.src list) list > (thmref * Attrib.src list) list > 
12180  55 
theory > theory * 
6424  56 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  57 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
58 
val setup: (theory > theory) list 

5094  59 
end; 
60 

6424  61 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  62 
struct 
63 

9598  64 

10729  65 
(** theory context references **) 
66 

15525  67 
val mono_name = "Orderings.mono"; 
17010
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

68 
val gfp_name = "FixedPoint.gfp"; 
5abc26872268
changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp
avigad
parents:
16975
diff
changeset

69 
val lfp_name = "FixedPoint.lfp"; 
12259  70 
val vimage_name = "Set.vimage"; 
10735  71 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); 
72 

11991  73 
val inductive_forall_name = "HOL.induct_forall"; 
74 
val inductive_forall_def = thm "induct_forall_def"; 

75 
val inductive_conj_name = "HOL.induct_conj"; 

76 
val inductive_conj_def = thm "induct_conj_def"; 

77 
val inductive_conj = thms "induct_conj"; 

78 
val inductive_atomize = thms "induct_atomize"; 

79 
val inductive_rulify1 = thms "induct_rulify1"; 

80 
val inductive_rulify2 = thms "induct_rulify2"; 

10729  81 

82 

83 

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

85 

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

86 
(* data kind 'HOL/inductive' *) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

87 

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

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

89 
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

90 
induct: thm, intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

91 

16432  92 
structure InductiveData = TheoryDataFun 
93 
(struct 

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

94 
val name = "HOL/inductive"; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

95 
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

96 

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

97 
val empty = (Symtab.empty, []); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

98 
val copy = I; 
16432  99 
val extend = I; 
100 
fun merge _ ((tab1, monos1), (tab2, monos2)) = 

11502  101 
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

102 

16432  103 
fun print thy (tab, monos) = 
16364  104 
[Pretty.strs ("(co)inductives:" :: 
16432  105 
map #1 (NameSpace.extern_table (Sign.const_space thy, tab))), 
106 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)] 

8720  107 
> Pretty.chunks > Pretty.writeln; 
16432  108 
end); 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

109 

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

110 
val print_inductives = InductiveData.print; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

111 

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

112 

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

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

114 

17412  115 
val get_inductive = Symtab.lookup o #1 o InductiveData.get; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

116 

9598  117 
fun the_inductive thy name = 
118 
(case get_inductive thy name of 

15531  119 
NONE => error ("Unknown (co)inductive set " ^ quote name) 
120 
 SOME info => info); 

9598  121 

12400  122 
val the_mk_cases = (#mk_cases o #2) oo the_inductive; 
123 

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

124 
fun put_inductives names info thy = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

125 
let 
17412  126 
fun upd ((tab, monos), name) = (Symtab.update_new (name, info) tab, monos); 
15570  127 
val tab_monos = Library.foldl upd (InductiveData.get thy, names) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

128 
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

129 
in InductiveData.put tab_monos thy end; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

130 

8277  131 

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

132 

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

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

134 

9831  135 
val get_monos = #2 o InductiveData.get; 
136 
fun map_monos f = InductiveData.map (Library.apsnd f); 

8277  137 

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

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

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

140 
fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @ 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

141 
(case concl_of thm of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

142 
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

143 
 _ => [standard (thm' RS (thm' RS eq_to_mono2))]); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

144 
val concl = concl_of thm 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

146 
if Logic.is_equals concl then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

147 
eq2mono (thm RS meta_eq_to_obj_eq) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

148 
else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

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

152 

8634  153 

154 
(* attributes *) 

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

155 

9831  156 
fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm); 
157 
fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm); 

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

158 

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

159 
val mono_attr = 
8634  160 
(Attrib.add_del_args mono_add_global mono_del_global, 
161 
Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute); 

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

162 

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

163 

7107  164 

10735  165 
(** misc utilities **) 
6424  166 

5662  167 
val quiet_mode = ref false; 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

168 
val trace = ref false; (*for debugging*) 
10735  169 
fun message s = if ! quiet_mode then () else writeln s; 
170 
fun clean_message s = if ! quick_and_dirty then () else message s; 

5662  171 

6424  172 
fun coind_prefix true = "co" 
173 
 coind_prefix false = ""; 

174 

175 

10735  176 
(*the following code ensures that each recursive set always has the 
177 
same type in all introduction rules*) 

16432  178 
fun unify_consts thy cs intr_ts = 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

179 
(let 
16861  180 
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c  _ => I); 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

181 
fun varify (t, (i, ts)) = 
16876  182 
let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, []))) 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

183 
in (maxidx_of_term t', t'::ts) end; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

184 
val (i, cs') = foldr varify (~1, []) cs; 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

185 
val (i', intr_ts') = foldr varify (i, []) intr_ts; 
16861  186 
val rec_consts = fold add_term_consts_2 cs' []; 
187 
val intr_consts = fold add_term_consts_2 intr_ts' []; 

16934  188 
fun unify (cname, cT) = 
15570  189 
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) 
16934  190 
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end; 
191 
val (env, _) = fold unify rec_consts (Vartab.empty, i'); 

16287  192 
val subst = Type.freeze o map_term_types (Envir.norm_type env) 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

193 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

194 
in (map subst cs', map subst intr_ts') 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

195 
end) handle Type.TUNIFY => 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

196 
(warning "Occurrences of recursive constant have nonunifiable types"; (cs, intr_ts)); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

197 

75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

198 

10735  199 
(*make injections used in mutually recursive definitions*) 
5094  200 
fun mk_inj cs sumT c x = 
201 
let 

202 
fun mk_inj' T n i = 

203 
if n = 1 then x else 

204 
let val n2 = n div 2; 

205 
val Type (_, [T1, T2]) = T 

206 
in 

207 
if i <= n2 then 

15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
15032
diff
changeset

208 
Const ("Sum_Type.Inl", T1 > T) $ (mk_inj' T1 n2 i) 
5094  209 
else 
15391
797ed46d724b
converted Sum_Type to newstyle theory: Inl, Inr are NO LONGER global
paulson
parents:
15032
diff
changeset

210 
Const ("Sum_Type.Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 
5094  211 
end 
212 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) 

213 
end; 

214 

10735  215 
(*make "vimage" terms for selecting out components of mutually rec.def*) 
5094  216 
fun mk_vimage cs sumT t c = if length cs < 2 then t else 
217 
let 

218 
val cT = HOLogic.dest_setT (fastype_of c); 

219 
val vimageT = [cT > sumT, HOLogic.mk_setT sumT] > HOLogic.mk_setT cT 

220 
in 

221 
Const (vimage_name, vimageT) $ 

222 
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t 

223 
end; 

224 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

225 
(** proper splitting **) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

226 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

227 
fun prod_factors p (Const ("Pair", _) $ t $ u) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

228 
p :: prod_factors (1::p) t @ prod_factors (2::p) u 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

229 
 prod_factors p _ = []; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

230 

17485  231 
fun mg_prod_factors ts (t $ u) fs = if t mem ts then 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

232 
let val f = prod_factors [] u 
17325  233 
in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) > the_default f) fs end 
17485  234 
else mg_prod_factors ts u (mg_prod_factors ts t fs) 
235 
 mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs 

236 
 mg_prod_factors ts _ fs = fs; 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

237 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

238 
fun prodT_factors p ps (T as Type ("*", [T1, T2])) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

239 
if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

240 
else [T] 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

241 
 prodT_factors _ _ T = [T]; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

242 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

243 
fun ap_split p ps (Type ("*", [T1, T2])) T3 u = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

244 
if p mem ps then HOLogic.split_const (T1, T2, T3) $ 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

245 
Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

246 
(prodT_factors (2::p) ps T2 > T3) (incr_boundvars 1 u) $ Bound 0)) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

247 
else u 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

248 
 ap_split _ _ _ _ u = u; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

249 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

250 
fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

251 
if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
15570  252 
mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms))) 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

253 
else t 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

254 
 mk_tuple _ _ _ (t::_) = t; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

255 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

256 
fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

257 
let val T' = prodT_factors [] ps T1 > T2 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

258 
val newt = ap_split [] ps T1 T2 (Var (v, T')) 
16432  259 
val cterm = Thm.cterm_of (Thm.theory_of_thm rl) 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

260 
in 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

261 
instantiate ([], [(cterm t, cterm newt)]) rl 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

262 
end 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

263 
 split_rule_var' (_, rl) = rl; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

264 

e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

265 
val remove_split = rewrite_rule [split_conv RS eq_reflection]; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

266 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

267 
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var' 
17485  268 
rl (mg_prod_factors vs (Thm.prop_of rl) []))); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

269 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

270 
fun split_rule vs rl = standard (remove_split (foldr split_rule_var' 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

271 
rl (List.mapPartial (fn (t as Var ((a, _), _)) => 
17485  272 
Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl))))); 
6424  273 

274 

10729  275 
(** process rules **) 
276 

277 
local 

5094  278 

16432  279 
fun err_in_rule thy name t msg = 
280 
error (cat_lines ["Illformed introduction rule " ^ quote name, 

281 
Sign.string_of_term thy t, msg]); 

10729  282 

16432  283 
fun err_in_prem thy name t p msg = 
284 
error (cat_lines ["Illformed premise", Sign.string_of_term thy p, 

285 
"in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]); 

5094  286 

10729  287 
val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\""; 
288 

11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

289 
val all_not_allowed = 
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

290 
"Introduction rule must not have a leading \"!!\" quantifier"; 
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

291 

16432  292 
fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize []; 
10729  293 

294 
in 

5094  295 

16432  296 
fun check_rule thy cs ((name, rule), att) = 
10729  297 
let 
298 
val concl = Logic.strip_imp_concl rule; 

299 
val prems = Logic.strip_imp_prems rule; 

16432  300 
val aprems = map (atomize_term thy) prems; 
10729  301 
val arule = Logic.list_implies (aprems, concl); 
5094  302 

10729  303 
fun check_prem (prem, aprem) = 
304 
if can HOLogic.dest_Trueprop aprem then () 

16432  305 
else err_in_prem thy name rule prem "Nonatomic premise"; 
10729  306 
in 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

307 
(case concl of 
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

308 
Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) => 
10729  309 
if u mem cs then 
310 
if exists (Logic.occs o rpair t) cs then 

16432  311 
err_in_rule thy name rule "Recursion term on left of member symbol" 
15570  312 
else List.app check_prem (prems ~~ aprems) 
16432  313 
else err_in_rule thy name rule bad_concl 
314 
 Const ("all", _) $ _ => err_in_rule thy name rule all_not_allowed 

315 
 _ => err_in_rule thy name rule bad_concl); 

10729  316 
((name, arule), att) 
317 
end; 

5094  318 

10729  319 
val rulify = 
13709  320 
standard o 
11036  321 
hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o 
322 
hol_simplify inductive_conj; 

10729  323 

324 
end; 

325 

5094  326 

6424  327 

10735  328 
(** properties of (co)inductive sets **) 
5094  329 

10735  330 
(* elimination rules *) 
5094  331 

8375  332 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  333 
let 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

334 
val used = foldr add_term_names [] intr_ts; 
5094  335 
val [aname, pname] = variantlist (["a", "P"], used); 
336 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 

337 

338 
fun dest_intr r = 

339 
let val Const ("op :", _) $ t $ u = 

340 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

341 
in (u, t, Logic.strip_imp_prems r) end; 

342 

8380  343 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  344 

345 
fun mk_elim (c, T) = 

346 
let 

347 
val a = Free (aname, T); 

348 

349 
fun mk_elim_prem (_, t, ts) = 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

350 
list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params), 
5094  351 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 
15570  352 
val c_intrs = (List.filter (equal c o #1 o #1) intrs); 
5094  353 
in 
8375  354 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
355 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  356 
end 
357 
in 

358 
map mk_elim (cs ~~ cTs) 

359 
end; 

9598  360 

6424  361 

10735  362 
(* premises and conclusions of induction rules *) 
5094  363 

364 
fun mk_indrule cs cTs params intr_ts = 

365 
let 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

366 
val used = foldr add_term_names [] intr_ts; 
5094  367 

368 
(* predicates for induction rule *) 

369 

370 
val preds = map Free (variantlist (if length cs < 2 then ["P"] else 

371 
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~ 

372 
map (fn T => T > HOLogic.boolT) cTs); 

373 

374 
(* transform an introduction rule into a premise for induction rule *) 

375 

376 
fun mk_ind_prem r = 

377 
let 

378 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

379 

17485  380 
val pred_of = AList.lookup (op aconv) (cs ~~ preds); 
5094  381 

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

382 
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

383 
(case pred_of u of 
15531  384 
NONE => (m $ fst (subst t) $ fst (subst u), NONE) 
385 
 SOME P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), SOME (s, P $ t))) 

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

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

387 
(case pred_of s of 
15531  388 
SOME P => (HOLogic.mk_binop "op Int" 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

389 
(s, HOLogic.Collect_const (HOLogic.dest_setT 
15531  390 
(fastype_of s)) $ P), NONE) 
391 
 NONE => (case s of 

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

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

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

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

395 

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

396 
fun mk_prem (s, prems) = (case subst s of 
15531  397 
(_, SOME (t, u)) => t :: u :: prems 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

398 
 (t, _) => t :: prems); 
9598  399 

5094  400 
val Const ("op :", _) $ t $ u = 
401 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

402 

403 
in list_all_free (frees, 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

404 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

405 
[] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))), 
15570  406 
HOLogic.mk_Trueprop (valOf (pred_of u) $ t))) 
5094  407 
end; 
408 

409 
val ind_prems = map mk_ind_prem intr_ts; 

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

410 

17485  411 
val factors = Library.fold (mg_prod_factors preds) ind_prems []; 
5094  412 

413 
(* make conclusions for induction rules *) 

414 

415 
fun mk_ind_concl ((c, P), (ts, x)) = 

416 
let val T = HOLogic.dest_setT (fastype_of c); 

17485  417 
val ps = AList.lookup (op =) factors P > the_default []; 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

418 
val Ts = prodT_factors [] ps T; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

419 
val (frees, x') = foldr (fn (T', (fs, s)) => 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

420 
((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts; 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

421 
val tuple = mk_tuple [] ps T frees; 
5094  422 
in ((HOLogic.mk_binop "op >" 
423 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') 

424 
end; 

425 

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

426 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

427 
(fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds)))) 
5094  428 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

429 
in (preds, ind_prems, mutual_ind_concl, 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

430 
map (apfst (fst o dest_Free)) factors) 
5094  431 
end; 
432 

6424  433 

10735  434 
(* prepare cases and induct rules *) 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

435 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

436 
(* 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

437 
transform mutual rule: 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

438 
HH ==> (x1:A1 > P1 x1) & ... & (xn:An > Pn xn) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

439 
into ith projection: 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

440 
xi:Ai ==> HH ==> Pi xi 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

441 
*) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

442 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

443 
fun project_rules [name] rule = [(name, rule)] 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

444 
 project_rules names mutual_rule = 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

445 
let 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

446 
val n = length names; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

447 
fun proj i = 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

448 
(if i < n then (fn th => th RS conjunct1) else I) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

449 
(Library.funpow (i  1) (fn th => th RS conjunct2) mutual_rule) 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

450 
RS mp > Thm.permute_prems 0 ~1 > Drule.standard; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

451 
in names ~~ map proj (1 upto n) end; 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

452 

12172  453 
fun add_cases_induct no_elim no_induct names elims induct = 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

454 
let 
9405  455 
fun cases_spec (name, elim) thy = 
456 
thy 

457 
> Theory.add_path (Sign.base_name name) 

10279  458 
> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])]) 
9405  459 
> Theory.parent_path; 
8375  460 
val cases_specs = if no_elim then [] else map2 cases_spec (names, elims); 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

461 

11005  462 
fun induct_spec (name, th) = #1 o PureThy.add_thms 
463 
[(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])]; 

12172  464 
val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct); 
9405  465 
in Library.apply (cases_specs @ induct_specs) end; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

466 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

467 

74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

468 

10735  469 
(** proofs for (co)inductive sets **) 
6424  470 

10735  471 
(* prove monotonicity  NOT subject to quick_and_dirty! *) 
5094  472 

473 
fun prove_mono setT fp_fun monos thy = 

10735  474 
(message " Proving monotonicity ..."; 
11880  475 
Goals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*) 
16432  476 
(Thm.cterm_of thy (HOLogic.mk_Trueprop 
5094  477 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
15570  478 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])); 
5094  479 

6424  480 

10735  481 
(* prove introduction rules *) 
5094  482 

12180  483 
fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy = 
5094  484 
let 
10735  485 
val _ = clean_message " Proving the introduction rules ..."; 
5094  486 

13657
c1637d60a846
Now applies standard' to "unfold" theorem (due to flexflex constraints).
berghofe
parents:
13626
diff
changeset

487 
val unfold = standard' (mono RS (fp_def RS 
10186  488 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  489 

490 
fun select_disj 1 1 = [] 

491 
 select_disj _ 1 = [rtac disjI1] 

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

493 

11880  494 
val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs 
16432  495 
(Thm.cterm_of thy intr) (fn prems => 
5094  496 
[(*insert prems and underlying sets*) 
497 
cut_facts_tac prems 1, 

498 
stac unfold 1, 

499 
REPEAT (resolve_tac [vimageI2, CollectI] 1), 

500 
(*Now 12 subgoals: the disjunction, perhaps equality.*) 

501 
EVERY1 (select_disj (length intr_ts) i), 

502 
(*Not ares_tac, since refl must be tried before any equality assumptions; 

503 
backtracking may occur if the premises have extra variables!*) 

10735  504 
DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), 
5094  505 
(*Now solve the equations like Inl 0 = Inl ?b2*) 
10729  506 
REPEAT (rtac refl 1)]) 
507 
> rulify) (1 upto (length intr_ts) ~~ intr_ts) 

5094  508 

509 
in (intrs, unfold) end; 

510 

6424  511 

10735  512 
(* prove elimination rules *) 
5094  513 

8375  514 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  515 
let 
10735  516 
val _ = clean_message " Proving the elimination rules ..."; 
5094  517 

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

518 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
10735  519 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; 
8375  520 
in 
11005  521 
mk_elims cs cTs params intr_ts intr_names > map (fn (t, cases) => 
11880  522 
quick_and_dirty_prove_goalw_cterm thy rec_sets_defs 
16432  523 
(Thm.cterm_of thy t) (fn prems => 
11005  524 
[cut_facts_tac [hd prems] 1, 
525 
dtac (unfold RS subst) 1, 

526 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

527 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

528 
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) 

529 
> rulify 

530 
> RuleCases.name cases) 

8375  531 
end; 
5094  532 

6424  533 

10735  534 
(* derivation of simplified elimination rules *) 
5094  535 

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

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

537 

7107  538 
(*cprop should have the form t:Si where Si is an inductive set*) 
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

539 
val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\""; 
9598  540 

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

541 
(*delete needless equality assumptions*) 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

542 
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]); 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

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

544 
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

545 

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

546 
fun simp_case_tac solved ss i = 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

547 
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

548 
THEN_MAYBE (if solved then no_tac else all_tac); 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

549 

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

550 
in 
9598  551 

552 
fun mk_cases_i elims ss cprop = 

7107  553 
let 
554 
val prem = Thm.assume cprop; 

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

555 
val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac; 
9298  556 
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); 
7107  557 
in 
558 
(case get_first (try mk_elim) elims of 

15531  559 
SOME r => r 
560 
 NONE => error (Pretty.string_of (Pretty.block 

9598  561 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  562 
end; 
563 

6141  564 
fun mk_cases elims s = 
16432  565 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT)); 
9598  566 

567 
fun smart_mk_cases thy ss cprop = 

568 
let 

569 
val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop 

570 
(Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err; 

571 
val (_, {elims, ...}) = the_inductive thy c; 

572 
in mk_cases_i elims ss cprop end; 

7107  573 

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

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

575 

7107  576 

577 
(* inductive_cases(_i) *) 

578 

12609  579 
fun gen_inductive_cases prep_att prep_prop args thy = 
9598  580 
let 
16432  581 
val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy); 
12609  582 
val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop; 
583 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

584 
val facts = args > map (fn ((a, atts), props) => 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

585 
((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props)); 
12709  586 
in thy > IsarThy.theorems_i Drule.lemmaK facts > #1 end; 
5094  587 

12172  588 
val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop; 
589 
val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop; 

7107  590 

6424  591 

9598  592 
(* mk_cases_meth *) 
593 

594 
fun mk_cases_meth (ctxt, raw_props) = 

595 
let 

596 
val thy = ProofContext.theory_of ctxt; 

15032  597 
val ss = local_simpset_of ctxt; 
16432  598 
val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props; 
10743  599 
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end; 
9598  600 

601 
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name)); 

602 

603 

10735  604 
(* prove induction rule *) 
5094  605 

606 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

607 
fp_def rec_sets_defs thy = 

608 
let 

10735  609 
val _ = clean_message " Proving the induction rule ..."; 
5094  610 

12922  611 
val sum_case_rewrites = 
16432  612 
(if Context.theory_name thy = "Datatype" then 
16486  613 
PureThy.get_thms thy (Name "sum.cases") 
16432  614 
else 
615 
(case ThyInfo.lookup_theory "Datatype" of 

616 
NONE => [] 

16975  617 
 SOME thy' => 
618 
if Theory.subthy (thy', thy) then 

619 
PureThy.get_thms thy' (Name "sum.cases") 

620 
else [])) 

16432  621 
> map mk_meta_eq; 
7293  622 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

623 
val (preds, ind_prems, mutual_ind_concl, factors) = 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

624 
mk_indrule cs cTs params intr_ts; 
5094  625 

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

626 
val dummy = if !trace then 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

627 
(writeln "ind_prems = "; 
16432  628 
List.app (writeln o Sign.string_of_term thy) ind_prems) 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

629 
else (); 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

630 

5094  631 
(* make predicate for instantiation of abstract induction rule *) 
632 

633 
fun mk_ind_pred _ [P] = P 

634 
 mk_ind_pred T Ps = 

635 
let val n = (length Ps) div 2; 

636 
val Type (_, [T1, T2]) = T 

7293  637 
in Const ("Datatype.sum.sum_case", 
5094  638 
[T1 > HOLogic.boolT, T2 > HOLogic.boolT, T] > HOLogic.boolT) $ 
15570  639 
mk_ind_pred T1 (Library.take (n, Ps)) $ mk_ind_pred T2 (Library.drop (n, Ps)) 
5094  640 
end; 
641 

642 
val ind_pred = mk_ind_pred sumT preds; 

643 

644 
val ind_concl = HOLogic.mk_Trueprop 

645 
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op >" 

646 
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0))); 

647 

648 
(* simplification rules for vimage and Collect *) 

649 

650 
val vimage_simps = if length cs < 2 then [] else 

16432  651 
map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy 
5094  652 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
653 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

654 
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ 

15570  655 
List.nth (preds, find_index_eq c cs))))) 
10735  656 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs; 
5094  657 

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

658 
val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct)); 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

659 

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

660 
val dummy = if !trace then 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

661 
(writeln "raw_fp_induct = "; print_thm raw_fp_induct) 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

662 
else (); 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

663 

16432  664 
val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy 
5094  665 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 
666 
[rtac (impI RS allI) 1, 

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

667 
DETERM (etac raw_fp_induct 1), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

668 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  669 
fold_goals_tac rec_sets_defs, 
670 
(*This CollectE and disjE separates out the introduction rules*) 

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

671 
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])), 
5094  672 
(*Now break down the individual cases. No disjE here in case 
673 
some premise involves disjunction.*) 

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

674 
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)), 
15416
db69af736ebb
Further fix to a bug (involving equational premises) in inductive definitions
paulson
parents:
15391
diff
changeset

675 
ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)), 
5094  676 
EVERY (map (fn prem => 
13747
bf308fcfd08e
Better treatment of equality in premises of inductive definitions. Less
paulson
parents:
13709
diff
changeset

677 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  678 

16432  679 
val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy 
5094  680 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 
681 
[cut_facts_tac prems 1, 

682 
REPEAT (EVERY 

683 
[REPEAT (resolve_tac [conjI, impI] 1), 

684 
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, 

7293  685 
rewrite_goals_tac sum_case_rewrites, 
5094  686 
atac 1])]) 
687 

10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

688 
in standard (split_rule factors (induct RS lemma)) end; 
5094  689 

6424  690 

691 

10735  692 
(** specification of (co)inductive sets **) 
5094  693 

10729  694 
fun cond_declare_consts declare_consts cs paramTs cnames = 
695 
if declare_consts then 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

696 
Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 
10729  697 
else I; 
698 

12180  699 
fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

700 
params paramTs cTs cnames = 
5094  701 
let 
702 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

703 
val setT = HOLogic.mk_setT sumT; 

704 

10735  705 
val fp_name = if coind then gfp_name else lfp_name; 
5094  706 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

707 
val used = foldr add_term_names [] intr_ts; 
5149  708 
val [sname, xname] = variantlist (["S", "x"], used); 
709 

5094  710 
(* transform an introduction rule into a conjunction *) 
711 
(* [ t : ... S_i ... ; ... ] ==> u : S_j *) 

712 
(* is transformed into *) 

713 
(* x = Inj_j u & t : ... Inj_i `` S ... & ... *) 

714 

715 
fun transform_rule r = 

716 
let 

717 
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); 

5149  718 
val subst = subst_free 
719 
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs)); 

5094  720 
val Const ("op :", _) $ t $ u = 
721 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

722 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

723 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

724 
(foldr1 HOLogic.mk_conj 
5149  725 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  726 
(map (subst o HOLogic.dest_Trueprop) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

727 
(Logic.strip_imp_prems r)))) frees 
5094  728 
end 
729 

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

731 

5149  732 
val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $ 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

733 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  734 

735 
(* add definiton of recursive sets to theory *) 

736 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

737 
val rec_name = if alt_name = "" then 
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

738 
space_implode "_" (map Sign.base_name cnames) else alt_name; 
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

739 
val full_rec_name = if length cs < 2 then hd cnames 
16432  740 
else Sign.full_name thy rec_name; 
5094  741 

742 
val rec_const = list_comb 

743 
(Const (full_rec_name, paramTs > setT), params); 

744 

745 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  746 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  747 

748 
val def_terms = fp_def_term :: (if length cs < 2 then [] else 

749 
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); 

750 

8433  751 
val (thy', [fp_def :: rec_sets_defs]) = 
752 
thy 

10729  753 
> cond_declare_consts declare_consts cs paramTs cnames 
8433  754 
> (if length cs < 2 then I 
755 
else Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) 

756 
> Theory.add_path rec_name 

9315  757 
> PureThy.add_defss_i false [(("defs", def_terms), [])]; 
5094  758 

9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

759 
val mono = prove_mono setT fp_fun monos thy' 
5094  760 

10735  761 
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  762 

9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

763 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 
12180  764 
intros monos thy params paramTs cTs cnames induct_cases = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

765 
let 
10735  766 
val _ = 
767 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

768 
commas_quote (map Sign.base_name cnames)) else (); 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

769 

a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

770 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

771 

9939  772 
val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) = 
12180  773 
mk_ind_def declare_consts alt_name coind cs intr_ts monos thy 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

774 
params paramTs cTs cnames; 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

775 

12180  776 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1; 
5094  777 
val elims = if no_elim then [] else 
9939  778 
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

779 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  780 
if coind then standard (rule_by_tactic 
5553  781 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  782 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
783 
else 

784 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

9939  785 
rec_sets_defs thy1; 
12165  786 
val induct = 
787 
if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0]) 

788 
else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]); 

5094  789 

9939  790 
val (thy2, intrs') = 
791 
thy1 > PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts); 

10735  792 
val (thy3, ([intrs'', elims'], [induct'])) = 
793 
thy2 

11005  794 
> PureThy.add_thmss 
11628  795 
[(("intros", intrs'), []), 
11005  796 
(("elims", elims), [RuleCases.consumes 1])] 
10735  797 
>>> PureThy.add_thms 
12165  798 
[((coind_prefix coind ^ "induct", rulify (#1 induct)), 
799 
(RuleCases.case_names induct_cases :: #2 induct))] 

8433  800 
>> Theory.parent_path; 
9939  801 
in (thy3, 
10735  802 
{defs = fp_def :: rec_sets_defs, 
5094  803 
mono = mono, 
804 
unfold = unfold, 

13709  805 
intrs = intrs', 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

806 
elims = elims', 
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

807 
mk_cases = mk_cases elims', 
10729  808 
raw_induct = rulify raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

809 
induct = induct'}) 
5094  810 
end; 
811 

6424  812 

10735  813 
(* external interfaces *) 
5094  814 

16432  815 
fun try_term f msg thy t = 
10735  816 
(case Library.try f t of 
15531  817 
SOME x => x 
16432  818 
 NONE => error (msg ^ Sign.string_of_term thy t)); 
5094  819 

12180  820 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy = 
5094  821 
let 
6424  822 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
5094  823 

824 
(*parameters should agree for all mutually recursive components*) 

825 
val (_, params) = strip_comb (hd cs); 

10735  826 
val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\ 
16432  827 
\ component is not a free variable: " thy) params; 
5094  828 

10735  829 
val cTs = map (try_term (HOLogic.dest_setT o fastype_of) 
16432  830 
"Recursive component not of type set: " thy) cs; 
5094  831 

14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

832 
val cnames = map (try_term (fst o dest_Const o head_of) 
16432  833 
"Recursive set not previously declared as constant: " thy) cs; 
5094  834 

16432  835 
val save_thy = thy 
836 
> Theory.copy > cond_declare_consts declare_consts cs paramTs cnames; 

837 
val intros = map (check_rule save_thy cs) pre_intros; 

8401  838 
val induct_cases = map (#1 o #1) intros; 
6437  839 

9405  840 
val (thy1, result as {elims, induct, ...}) = 
11628  841 
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos 
12180  842 
thy params paramTs cTs cnames induct_cases; 
8307  843 
val thy2 = thy1 
14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

844 
> put_inductives cnames ({names = cnames, coind = coind}, result) 
12172  845 
> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1) 
14235
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

846 
cnames elims induct; 
6437  847 
in (thy2, result) end; 
5094  848 

12180  849 
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy = 
5094  850 
let 
16975  851 
val cs = map (Sign.read_term thy) c_strings; 
6424  852 

853 
val intr_names = map (fst o fst) intro_srcs; 

16432  854 
fun read_rule s = Thm.read_cterm thy (s, propT) 
9405  855 
handle ERROR => error ("The error(s) above occurred for " ^ s); 
856 
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs; 

6424  857 
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; 
16432  858 
val (cs', intr_ts') = unify_consts thy cs intr_ts; 
5094  859 

12180  860 
val (thy', monos) = thy > IsarThy.apply_theorems raw_monos; 
6424  861 
in 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

862 
add_inductive_i verbose false "" coind false false cs' 
12180  863 
((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' 
5094  864 
end; 
865 

6424  866 

867 

6437  868 
(** package setup **) 
869 

870 
(* setup theory *) 

871 

8634  872 
val setup = 
873 
[InductiveData.init, 

9625  874 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  875 
"dynamic case analysis on sets")], 
9893  876 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  877 

878 

879 
(* outer syntax *) 

6424  880 

17057  881 
local structure P = OuterParse and K = OuterKeyword in 
6424  882 

12180  883 
fun mk_ind coind ((sets, intrs), monos) = 
884 
#1 o add_inductive true coind sets (map P.triple_swap intrs) monos; 

6424  885 

886 
fun ind_decl coind = 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

887 
Scan.repeat1 P.term  
9598  888 
(P.$$$ "intros"  
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

889 
P.!!! (Scan.repeat1 (P.opt_thm_name ":"  P.prop)))  
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

890 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1) [] 
6424  891 
>> (Toplevel.theory o mk_ind coind); 
892 

6723  893 
val inductiveP = 
894 
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); 

895 

896 
val coinductiveP = 

897 
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); 

6424  898 

7107  899 

900 
val ind_cases = 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

901 
P.and_list1 (P.opt_thm_name ":"  Scan.repeat1 P.prop) 
7107  902 
>> (Toplevel.theory o inductive_cases); 
903 

904 
val inductive_casesP = 

9804  905 
OuterSyntax.command "inductive_cases" 
9598  906 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  907 

12180  908 
val _ = OuterSyntax.add_keywords ["intros", "monos"]; 
7107  909 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  910 

5094  911 
end; 
6424  912 

913 
end; 

15705  914 