author  wenzelm 
Wed, 13 Apr 2005 18:34:22 +0200  
changeset 15703  727ef1b8b3ee 
parent 15574  b1d1b5bfc464 
child 15705  b5edb9dcec9a 
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 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

34 
val unify_consts: Sign.sg > 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"; 
10735  68 
val gfp_name = "Gfp.gfp"; 
69 
val lfp_name = "Lfp.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 

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

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

93 
struct 
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; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

99 
val prep_ext = I; 
11502  100 
fun merge ((tab1, monos1), (tab2, monos2)) = 
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 

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

103 
fun print sg (tab, monos) = 
8720  104 
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)), 
10008  105 
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)] 
8720  106 
> Pretty.chunks > Pretty.writeln; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

108 

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

109 
structure InductiveData = TheoryDataFun(InductiveArgs); 
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 

9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

115 
fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name); 
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 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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*) 

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

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

179 
(let 
14643  180 
val tsig = Sign.tsig_of sign; 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

182 
foldl_aterms (fn (cs, Const c) => c ins cs  (cs, _) => cs); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

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

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

187 
val (i', intr_ts') = foldr varify (i, []) intr_ts; 
15570  188 
val rec_consts = Library.foldl add_term_consts_2 ([], cs'); 
189 
val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts'); 

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

190 
fun unify (env, (cname, cT)) = 
15570  191 
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts) 
192 
in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp)) 

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

193 
(env, (replicate (length consts) cT) ~~ consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

194 
end; 
15570  195 
val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts); 
8410
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset

196 
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

197 
in if T = T' then T else typ_subst_TVars_2 env T' end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

198 
val subst = fst o Type.freeze_thaw o 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

199 
(map_term_types (typ_subst_TVars_2 env)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

200 

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

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

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

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

204 

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

205 

10735  206 
(*make injections used in mutually recursive definitions*) 
5094  207 
fun mk_inj cs sumT c x = 
208 
let 

209 
fun mk_inj' T n i = 

210 
if n = 1 then x else 

211 
let val n2 = n div 2; 

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

213 
in 

214 
if i <= n2 then 

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

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

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

220 
end; 

221 

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

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

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

227 
in 

228 
Const (vimage_name, vimageT) $ 

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

230 
end; 

231 

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

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

233 

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

234 
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

235 
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

236 
 prod_factors p _ = []; 
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 mg_prod_factors ts (fs, t $ u) = if t mem ts then 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

239 
let val f = prod_factors [] u 
15570  240 
in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

241 
else mg_prod_factors ts (mg_prod_factors ts (fs, t), u) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

242 
 mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

243 
 mg_prod_factors ts (fs, _) = fs; 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

244 

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

245 
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

246 
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

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

248 
 prodT_factors _ _ T = [T]; 
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 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

251 
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

252 
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

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

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

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

256 

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

257 
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

258 
if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
15570  259 
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

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

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

262 

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

263 
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

264 
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

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

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

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

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

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

271 

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

272 
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

273 

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

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

275 
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

276 

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

277 
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

278 
rl (List.mapPartial (fn (t as Var ((a, _), _)) => 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

279 
Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl))))); 
6424  280 

281 

10729  282 
(** process rules **) 
283 

284 
local 

5094  285 

10729  286 
fun err_in_rule sg name t msg = 
287 
error (cat_lines ["Illformed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]); 

288 

289 
fun err_in_prem sg name t p msg = 

290 
error (cat_lines ["Illformed premise", Sign.string_of_term sg p, 

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

5094  292 

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

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

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

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

297 

13197
0567f4fd1415
Changed interface of MetaSimplifier.rewrite_term.
berghofe
parents:
12922
diff
changeset

298 
fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize []; 
10729  299 

300 
in 

5094  301 

10729  302 
fun check_rule sg cs ((name, rule), att) = 
303 
let 

304 
val concl = Logic.strip_imp_concl rule; 

305 
val prems = Logic.strip_imp_prems rule; 

12798
f7e2d0d32ea7
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12709
diff
changeset

306 
val aprems = map (atomize_term sg) prems; 
10729  307 
val arule = Logic.list_implies (aprems, concl); 
5094  308 

10729  309 
fun check_prem (prem, aprem) = 
310 
if can HOLogic.dest_Trueprop aprem then () 

311 
else err_in_prem sg name rule prem "Nonatomic premise"; 

312 
in 

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

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

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

317 
err_in_rule sg name rule "Recursion term on left of member symbol" 

15570  318 
else List.app check_prem (prems ~~ aprems) 
10729  319 
else err_in_rule sg name rule bad_concl 
11358
416ea5c009f5
now checks for leading metaquantifiers and complains, instead of
paulson
parents:
11036
diff
changeset

320 
 Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed 
10729  321 
 _ => err_in_rule sg name rule bad_concl); 
322 
((name, arule), att) 

323 
end; 

5094  324 

10729  325 
val rulify = 
13709  326 
standard o 
11036  327 
hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o 
328 
hol_simplify inductive_conj; 

10729  329 

330 
end; 

331 

5094  332 

6424  333 

10735  334 
(** properties of (co)inductive sets **) 
5094  335 

10735  336 
(* elimination rules *) 
5094  337 

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

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

343 

344 
fun dest_intr r = 

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

346 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

348 

8380  349 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  350 

351 
fun mk_elim (c, T) = 

352 
let 

353 
val a = Free (aname, T); 

354 

355 
fun mk_elim_prem (_, t, ts) = 

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

356 
list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params), 
5094  357 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 
15570  358 
val c_intrs = (List.filter (equal c o #1 o #1) intrs); 
5094  359 
in 
8375  360 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
361 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  362 
end 
363 
in 

364 
map mk_elim (cs ~~ cTs) 

365 
end; 

9598  366 

6424  367 

10735  368 
(* premises and conclusions of induction rules *) 
5094  369 

370 
fun mk_indrule cs cTs params intr_ts = 

371 
let 

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

372 
val used = foldr add_term_names [] intr_ts; 
5094  373 

374 
(* predicates for induction rule *) 

375 

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

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

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

379 

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

381 

382 
fun mk_ind_prem r = 

383 
let 

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

385 

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

386 
val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds); 
5094  387 

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

388 
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

389 
(case pred_of u of 
15531  390 
NONE => (m $ fst (subst t) $ fst (subst u), NONE) 
391 
 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

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

393 
(case pred_of s of 
15531  394 
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

395 
(s, HOLogic.Collect_const (HOLogic.dest_setT 
15531  396 
(fastype_of s)) $ P), NONE) 
397 
 NONE => (case s of 

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

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

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

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

401 

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

402 
fun mk_prem (s, prems) = (case subst s of 
15531  403 
(_, 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

404 
 (t, _) => t :: prems); 
9598  405 

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

408 

409 
in list_all_free (frees, 

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

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

411 
[] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))), 
15570  412 
HOLogic.mk_Trueprop (valOf (pred_of u) $ t))) 
5094  413 
end; 
414 

415 
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

416 

15570  417 
val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems); 
5094  418 

419 
(* make conclusions for induction rules *) 

420 

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

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

15570  423 
val ps = getOpt (assoc (factors, P), []); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

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

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

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

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

430 
end; 

431 

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

432 
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

433 
(fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds)))) 
5094  434 

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

435 
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

436 
map (apfst (fst o dest_Free)) factors) 
5094  437 
end; 
438 

6424  439 

10735  440 
(* prepare cases and induct rules *) 
8316
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 
transform mutual rule: 
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

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

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

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

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

448 

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

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

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

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

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

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

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

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

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

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

458 

12172  459 
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

460 
let 
9405  461 
fun cases_spec (name, elim) thy = 
462 
thy 

463 
> Theory.add_path (Sign.base_name name) 

10279  464 
> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])]) 
9405  465 
> Theory.parent_path; 
8375  466 
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

467 

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

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

472 

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

473 

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

474 

10735  475 
(** proofs for (co)inductive sets **) 
6424  476 

10735  477 
(* prove monotonicity  NOT subject to quick_and_dirty! *) 
5094  478 

479 
fun prove_mono setT fp_fun monos thy = 

10735  480 
(message " Proving monotonicity ..."; 
11880  481 
Goals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*) 
10735  482 
(Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  483 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
15570  484 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])); 
5094  485 

6424  486 

10735  487 
(* prove introduction rules *) 
5094  488 

12180  489 
fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy = 
5094  490 
let 
10735  491 
val _ = clean_message " Proving the introduction rules ..."; 
5094  492 

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

493 
val unfold = standard' (mono RS (fp_def RS 
10186  494 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  495 

496 
fun select_disj 1 1 = [] 

497 
 select_disj _ 1 = [rtac disjI1] 

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

499 

11880  500 
val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs 
10735  501 
(Thm.cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  502 
[(*insert prems and underlying sets*) 
503 
cut_facts_tac prems 1, 

504 
stac unfold 1, 

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

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

507 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

5094  514 

515 
in (intrs, unfold) end; 

516 

6424  517 

10735  518 
(* prove elimination rules *) 
5094  519 

8375  520 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  521 
let 
10735  522 
val _ = clean_message " Proving the elimination rules ..."; 
5094  523 

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

524 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
10735  525 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; 
8375  526 
in 
11005  527 
mk_elims cs cTs params intr_ts intr_names > map (fn (t, cases) => 
11880  528 
quick_and_dirty_prove_goalw_cterm thy rec_sets_defs 
11005  529 
(Thm.cterm_of (Theory.sign_of thy) t) (fn prems => 
530 
[cut_facts_tac [hd prems] 1, 

531 
dtac (unfold RS subst) 1, 

532 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

533 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

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

535 
> rulify 

536 
> RuleCases.name cases) 

8375  537 
end; 
5094  538 

6424  539 

10735  540 
(* derivation of simplified elimination rules *) 
5094  541 

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

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

543 

7107  544 
(*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

545 
val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\""; 
9598  546 

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

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

548 
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

549 
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

550 
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

551 

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

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

553 
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

554 
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

555 

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

556 
in 
9598  557 

558 
fun mk_cases_i elims ss cprop = 

7107  559 
let 
560 
val prem = Thm.assume cprop; 

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

561 
val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac; 
9298  562 
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); 
7107  563 
in 
564 
(case get_first (try mk_elim) elims of 

15531  565 
SOME r => r 
566 
 NONE => error (Pretty.string_of (Pretty.block 

9598  567 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  568 
end; 
569 

6141  570 
fun mk_cases elims s = 
9598  571 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
572 

573 
fun smart_mk_cases thy ss cprop = 

574 
let 

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

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

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

578 
in mk_cases_i elims ss cprop end; 

7107  579 

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

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

581 

7107  582 

583 
(* inductive_cases(_i) *) 

584 

12609  585 
fun gen_inductive_cases prep_att prep_prop args thy = 
9598  586 
let 
12609  587 
val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy); 
588 
val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop; 

589 

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

590 
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

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

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

7107  596 

6424  597 

9598  598 
(* mk_cases_meth *) 
599 

600 
fun mk_cases_meth (ctxt, raw_props) = 

601 
let 

602 
val thy = ProofContext.theory_of ctxt; 

15032  603 
val ss = local_simpset_of ctxt; 
9598  604 
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props; 
10743  605 
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end; 
9598  606 

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

608 

609 

10735  610 
(* prove induction rule *) 
5094  611 

612 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

613 
fp_def rec_sets_defs thy = 

614 
let 

10735  615 
val _ = clean_message " Proving the induction rule ..."; 
5094  616 

6394  617 
val sign = Theory.sign_of thy; 
5094  618 

12922  619 
val sum_case_rewrites = 
15531  620 
(if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy ("sum.cases", NONE) 
12922  621 
else 
622 
(case ThyInfo.lookup_theory "Datatype" of 

15531  623 
NONE => [] 
624 
 SOME thy' => PureThy.get_thms thy' ("sum.cases", NONE))) > map mk_meta_eq; 

7293  625 

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

626 
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

627 
mk_indrule cs cTs params intr_ts; 
5094  628 

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

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

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

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

633 

5094  634 
(* make predicate for instantiation of abstract induction rule *) 
635 

636 
fun mk_ind_pred _ [P] = P 

637 
 mk_ind_pred T Ps = 

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

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

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

645 
val ind_pred = mk_ind_pred sumT preds; 

646 

647 
val ind_concl = HOLogic.mk_Trueprop 

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

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

650 

651 
(* simplification rules for vimage and Collect *) 

652 

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

11880  654 
map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign 
5094  655 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
656 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

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

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

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

661 
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

662 

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

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

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

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

666 

11880  667 
val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign 
5094  668 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 
669 
[rtac (impI RS allI) 1, 

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

670 
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

671 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  672 
fold_goals_tac rec_sets_defs, 
673 
(*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

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

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

677 
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

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

680 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  681 

11880  682 
val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign 
5094  683 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 
684 
[cut_facts_tac prems 1, 

685 
REPEAT (EVERY 

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

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

7293  688 
rewrite_goals_tac sum_case_rewrites, 
5094  689 
atac 1])]) 
690 

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

691 
in standard (split_rule factors (induct RS lemma)) end; 
5094  692 

6424  693 

694 

10735  695 
(** specification of (co)inductive sets **) 
5094  696 

10729  697 
fun cond_declare_consts declare_consts cs paramTs cnames = 
698 
if declare_consts then 

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

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

12180  702 
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

703 
params paramTs cTs cnames = 
5094  704 
let 
705 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

706 
val setT = HOLogic.mk_setT sumT; 

707 

10735  708 
val fp_name = if coind then gfp_name else lfp_name; 
5094  709 

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

710 
val used = foldr add_term_names [] intr_ts; 
5149  711 
val [sname, xname] = variantlist (["S", "x"], used); 
712 

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

715 
(* is transformed into *) 

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

717 

718 
fun transform_rule r = 

719 
let 

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

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

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

725 

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

726 
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

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

730 
(Logic.strip_imp_prems r)))) frees 
5094  731 
end 
732 

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

734 

5149  735 
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

736 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  737 

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

739 

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

740 
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

741 
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

742 
val full_rec_name = if length cs < 2 then hd cnames 
281295a1bbaa
Fixed bug in mk_ind_def that caused the inductive definition package to
berghofe
parents:
13747
diff
changeset

743 
else Sign.full_name (Theory.sign_of thy) rec_name; 
5094  744 

745 
val rec_const = list_comb 

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

747 

748 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  749 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  750 

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

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

753 

8433  754 
val (thy', [fp_def :: rec_sets_defs]) = 
755 
thy 

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

759 
> Theory.add_path rec_name 

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

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

762 
val mono = prove_mono setT fp_fun monos thy' 
5094  763 

10735  764 
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  765 

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

766 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 
12180  767 
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

768 
let 
10735  769 
val _ = 
770 
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

771 
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

772 

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

773 
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

774 

9939  775 
val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) = 
12180  776 
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

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

778 

12180  779 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1; 
5094  780 
val elims = if no_elim then [] else 
9939  781 
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

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

787 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

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

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

5094  792 

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

10735  795 
val (thy3, ([intrs'', elims'], [induct'])) = 
796 
thy2 

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

8433  803 
>> Theory.parent_path; 
9939  804 
in (thy3, 
10735  805 
{defs = fp_def :: rec_sets_defs, 
5094  806 
mono = mono, 
807 
unfold = unfold, 

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

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

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

812 
induct = induct'}) 
5094  813 
end; 
814 

6424  815 

10735  816 
(* external interfaces *) 
5094  817 

10735  818 
fun try_term f msg sign t = 
819 
(case Library.try f t of 

15531  820 
SOME x => x 
821 
 NONE => error (msg ^ Sign.string_of_term sign t)); 

5094  822 

12180  823 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy = 
5094  824 
let 
6424  825 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  826 
val sign = Theory.sign_of thy; 
5094  827 

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

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

10735  830 
val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\ 
5094  831 
\ component is not a free variable: " sign) params; 
832 

10735  833 
val cTs = map (try_term (HOLogic.dest_setT o fastype_of) 
5094  834 
"Recursive component not of type set: " sign) cs; 
835 

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

836 
val cnames = map (try_term (fst o dest_Const o head_of) 
5094  837 
"Recursive set not previously declared as constant: " sign) cs; 
838 

10729  839 
val save_sign = 
840 
thy > Theory.copy > cond_declare_consts declare_consts cs paramTs cnames > Theory.sign_of; 

841 
val intros = map (check_rule save_sign cs) pre_intros; 

8401  842 
val induct_cases = map (#1 o #1) intros; 
6437  843 

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

848 
> put_inductives cnames ({names = cnames, coind = coind}, result) 
12172  849 
> 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

850 
cnames elims induct; 
6437  851 
in (thy2, result) end; 
5094  852 

12180  853 
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy = 
5094  854 
let 
6394  855 
val sign = Theory.sign_of thy; 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12311
diff
changeset

856 
val cs = map (term_of o HOLogic.read_cterm sign) c_strings; 
6424  857 

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

9405  859 
fun read_rule s = Thm.read_cterm sign (s, propT) 
860 
handle ERROR => error ("The error(s) above occurred for " ^ s); 

861 
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs; 

6424  862 
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

863 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  864 

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

867 
add_inductive_i verbose false "" coind false false cs' 
12180  868 
((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' 
5094  869 
end; 
870 

6424  871 

872 

6437  873 
(** package setup **) 
874 

875 
(* setup theory *) 

876 

8634  877 
val setup = 
878 
[InductiveData.init, 

9625  879 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  880 
"dynamic case analysis on sets")], 
9893  881 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  882 

883 

884 
(* outer syntax *) 

6424  885 

6723  886 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  887 

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

6424  890 

891 
fun ind_decl coind = 

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

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

894 
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

895 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1) [] 
6424  896 
>> (Toplevel.theory o mk_ind coind); 
897 

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

900 

901 
val coinductiveP = 

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

6424  903 

7107  904 

905 
val ind_cases = 

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

906 
P.and_list1 (P.opt_thm_name ":"  Scan.repeat1 P.prop) 
7107  907 
>> (Toplevel.theory o inductive_cases); 
908 

909 
val inductive_casesP = 

9804  910 
OuterSyntax.command "inductive_cases" 
9598  911 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  912 

12180  913 
val _ = OuterSyntax.add_keywords ["intros", "monos"]; 
7107  914 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  915 

5094  916 
end; 
6424  917 

918 
end; 