author  berghofe 
Wed, 13 Nov 2002 15:28:41 +0100  
changeset 13708  a3a410782c95 
parent 13657  c1637d60a846 
child 13709  ec00ba43aee8 
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 

11834  6 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5094  7 

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

10 
Features: 

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

13 
* mutually recursive definitions 

14 
* definitions involving arbitrary monotone operators 

15 
* automatically proves introduction and elimination rules 

5094  16 

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

5094  19 

20 
Introduction rules have the form 

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

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

24 
ti, t are any terms 

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

26 

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

5094  29 
*) 
30 

31 
signature INDUCTIVE_PACKAGE = 

32 
sig 

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

34 
val trace: bool ref 
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

35 
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

36 
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

37 
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

38 
{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

39 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}) option 
12400  40 
val the_mk_cases: theory > string > string > thm 
6437  41 
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

42 
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

43 
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

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

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

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

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

48 
val inductive_cases: ((bstring * Args.src list) * string list) list > theory > theory 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12798
diff
changeset

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

5094  60 
end; 
61 

6424  62 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  63 
struct 
64 

9598  65 

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

11755  68 
val mono_name = "HOL.mono"; 
10735  69 
val gfp_name = "Gfp.gfp"; 
70 
val lfp_name = "Lfp.lfp"; 

12259  71 
val vimage_name = "Set.vimage"; 
10735  72 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); 
73 

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

76 
val inductive_conj_name = "HOL.induct_conj"; 

77 
val inductive_conj_def = thm "induct_conj_def"; 

78 
val inductive_conj = thms "induct_conj"; 

79 
val inductive_atomize = thms "induct_atomize"; 

80 
val inductive_rulify1 = thms "induct_rulify1"; 

81 
val inductive_rulify2 = thms "induct_rulify2"; 

10729  82 

83 

84 

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

86 

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

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

88 

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

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

90 
{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

91 
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

92 

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

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

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

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

96 
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

97 

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

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

99 
val copy = I; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

103 

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

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

108 
end; 
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 
structure InductiveData = TheoryDataFun(InductiveArgs); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

111 
val print_inductives = InductiveData.print; 
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 

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

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

115 

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

116 
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

117 

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

120 
None => error ("Unknown (co)inductive set " ^ quote name) 

121 
 Some info => info); 

122 

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

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

125 
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

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

127 
fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

128 
val tab_monos = foldl upd (InductiveData.get thy, names) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

129 
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

130 
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

131 

8277  132 

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

133 

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

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

135 

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

8277  138 

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

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

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

141 
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

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

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

144 
 _ => [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

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

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

147 
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

148 
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

149 
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

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

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

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

153 

8634  154 

155 
(* attributes *) 

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

156 

9831  157 
fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm); 
158 
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

159 

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

160 
val mono_attr = 
8634  161 
(Attrib.add_del_args mono_add_global mono_del_global, 
162 
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

163 

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

164 

7107  165 

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

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

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

5662  172 

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

175 

176 

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

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

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

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

181 
val {tsig, ...} = Sign.rep_sg sign; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

183 
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

184 
fun varify (t, (i, ts)) = 
12494  185 
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

186 
in (maxidx_of_term t', t'::ts) end; 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

187 
val (i, cs') = foldr varify (cs, (~1, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

188 
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

189 
val rec_consts = foldl add_term_consts_2 ([], cs'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

190 
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

191 
fun unify (env, (cname, cT)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

192 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 
12527  193 
in 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

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

195 
end; 
8410
5902c02fa122
Type.unify now uses Vartab instead of association lists.
berghofe
parents:
8401
diff
changeset

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

197 
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

198 
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

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

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

201 

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

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

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

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

205 

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

206 

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

210 
fun mk_inj' T n i = 

211 
if n = 1 then x else 

212 
let val n2 = n div 2; 

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

214 
in 

215 
if i <= n2 then 

216 
Const ("Inl", T1 > T) $ (mk_inj' T1 n2 i) 

217 
else 

218 
Const ("Inr", T2 > T) $ (mk_inj' T2 (n  n2) (i  n2)) 

219 
end 

220 
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) 

221 
end; 

222 

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

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

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

228 
in 

229 
Const (vimage_name, vimageT) $ 

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

231 
end; 

232 

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

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

234 

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

235 
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

236 
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

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

238 

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

239 
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

240 
let val f = prod_factors [] u 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

241 
in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

242 
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

243 
 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

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

245 

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

246 
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

247 
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

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

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

250 

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

251 
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

252 
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

253 
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

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

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

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

257 

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

258 
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

259 
if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

260 
mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms))) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

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

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

263 

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

264 
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

265 
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

266 
val newt = ap_split [] ps T1 T2 (Var (v, T')) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

267 
val cterm = Thm.cterm_of (#sign (rep_thm rl)) 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

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

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

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

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

272 

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

273 
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

274 

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

275 
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var' 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

276 
(mg_prod_factors vs ([], #prop (rep_thm rl)), rl))); 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

277 

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

278 
fun split_rule vs rl = standard (remove_split (foldr split_rule_var' 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

279 
(mapfilter (fn (t as Var ((a, _), _)) => 
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

280 
apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl))); 
6424  281 

282 

10729  283 
(** process rules **) 
284 

285 
local 

5094  286 

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

289 

290 
fun err_in_prem sg name t p msg = 

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

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

5094  293 

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

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

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

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

298 

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

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

301 
in 

5094  302 

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

305 
val concl = Logic.strip_imp_concl rule; 

306 
val prems = Logic.strip_imp_prems rule; 

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

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

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

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

313 
in 

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

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

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

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

319 
else seq check_prem (prems ~~ aprems) 

320 
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

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

324 
end; 

5094  325 

10729  326 
val rulify = 
12798
f7e2d0d32ea7
MetaSimplifier.rewrite_term replaces slow Tactic.rewrite_cterm;
wenzelm
parents:
12709
diff
changeset

327 
standard o Tactic.norm_hhf_rule o 
11036  328 
hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o 
329 
hol_simplify inductive_conj; 

10729  330 

331 
end; 

332 

5094  333 

6424  334 

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

10735  337 
(* elimination rules *) 
5094  338 

8375  339 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  340 
let 
341 
val used = foldr add_term_names (intr_ts, []); 

342 
val [aname, pname] = variantlist (["a", "P"], used); 

343 
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); 

344 

345 
fun dest_intr r = 

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

347 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

349 

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

352 
fun mk_elim (c, T) = 

353 
let 

354 
val a = Free (aname, T); 

355 

356 
fun mk_elim_prem (_, t, ts) = 

357 
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), 

358 
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); 

8375  359 
val c_intrs = (filter (equal c o #1 o #1) intrs); 
5094  360 
in 
8375  361 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
362 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  363 
end 
364 
in 

365 
map mk_elim (cs ~~ cTs) 

366 
end; 

9598  367 

6424  368 

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

371 
fun mk_indrule cs cTs params intr_ts = 

372 
let 

373 
val used = foldr add_term_names (intr_ts, []); 

374 

375 
(* predicates for induction rule *) 

376 

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

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

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

380 

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

382 

383 
fun mk_ind_prem r = 

384 
let 

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

386 

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

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

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

389 
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

390 
(case pred_of u of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

391 
None => (m $ fst (subst t) $ fst (subst u), None) 
10735  392 
 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

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

394 
(case pred_of s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

395 
Some P => (HOLogic.mk_binop "op Int" 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

396 
(s, HOLogic.Collect_const (HOLogic.dest_setT 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

397 
(fastype_of s)) $ P), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

398 
 None => (case s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

399 
(t $ u) => (fst (subst t) $ fst (subst u), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

400 
 (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

401 
 _ => (s, None))); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

402 

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

403 
fun mk_prem (s, prems) = (case subst s of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

404 
(_, Some (t, u)) => t :: u :: prems 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

409 

410 
in list_all_free (frees, 

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

411 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
5094  412 
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

413 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  414 
end; 
415 

416 
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

417 

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

418 
val factors = foldl (mg_prod_factors preds) ([], ind_prems); 
5094  419 

420 
(* make conclusions for induction rules *) 

421 

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

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

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

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

425 
val Ts = prodT_factors [] ps T; 
5094  426 
val (frees, x') = foldr (fn (T', (fs, s)) => 
12902  427 
((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x)); 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

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

431 
end; 

432 

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

433 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  434 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
435 

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

436 
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

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

6424  440 

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

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

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

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

447 
xi:Ai ==> HH ==> Pi xi 
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 

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

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

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

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

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

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

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

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

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

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

459 

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

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

464 
> Theory.add_path (Sign.base_name name) 

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

468 

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

12172  471 
val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct); 
9405  472 
in Library.apply (cases_specs @ induct_specs) end; 
8316
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 

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

475 

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

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

480 
fun prove_mono setT fp_fun monos thy = 

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

6424  487 

10735  488 
(* prove introduction rules *) 
5094  489 

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

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

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

497 
fun select_disj 1 1 = [] 

498 
 select_disj _ 1 = [rtac disjI1] 

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

500 

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

505 
stac unfold 1, 

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

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

508 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

5094  515 

516 
in (intrs, unfold) end; 

517 

6424  518 

10735  519 
(* prove elimination rules *) 
5094  520 

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

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

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

532 
dtac (unfold RS subst) 1, 

533 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

534 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

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

536 
> rulify 

537 
> RuleCases.name cases) 

8375  538 
end; 
5094  539 

6424  540 

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

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

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

544 

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

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

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

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

549 
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

550 
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

551 
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

552 

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

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

554 
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

555 
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

556 

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

557 
in 
9598  558 

559 
fun mk_cases_i elims ss cprop = 

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

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

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

566 
Some r => r 

567 
 None => error (Pretty.string_of (Pretty.block 

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

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

574 
fun smart_mk_cases thy ss cprop = 

575 
let 

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

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

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

579 
in mk_cases_i elims ss cprop end; 

7107  580 

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

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

582 

7107  583 

584 
(* inductive_cases(_i) *) 

585 

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

590 

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

591 
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

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

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

7107  597 

6424  598 

9598  599 
(* mk_cases_meth *) 
600 

601 
fun mk_cases_meth (ctxt, raw_props) = 

602 
let 

603 
val thy = ProofContext.theory_of ctxt; 

604 
val ss = Simplifier.get_local_simpset ctxt; 

605 
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props; 

10743  606 
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end; 
9598  607 

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

609 

610 

10735  611 
(* prove induction rule *) 
5094  612 

613 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

614 
fp_def rec_sets_defs thy = 

615 
let 

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

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

12922  620 
val sum_case_rewrites = 
621 
(if PureThy.get_name thy = "Datatype" then PureThy.get_thms thy "sum.cases" 

622 
else 

623 
(case ThyInfo.lookup_theory "Datatype" of 

624 
None => [] 

625 
 Some thy' => PureThy.get_thms thy' "sum.cases")) > map mk_meta_eq; 

7293  626 

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

627 
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

628 
mk_indrule cs cTs params intr_ts; 
5094  629 

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

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

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

632 
seq (writeln o Sign.string_of_term sign) ind_prems) 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

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

634 

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

637 
fun mk_ind_pred _ [P] = P 

638 
 mk_ind_pred T Ps = 

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

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

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

644 
end; 

645 

646 
val ind_pred = mk_ind_pred sumT preds; 

647 

648 
val ind_concl = HOLogic.mk_Trueprop 

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

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

651 

652 
(* simplification rules for vimage and Collect *) 

653 

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

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

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

659 
nth_elem (find_index_eq c cs, preds))))) 

10735  660 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs; 
5094  661 

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

662 
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

663 

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

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

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

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

667 

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

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

671 
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

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

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

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

678 
REPEAT (FIRSTGOAL (etac conjE)), 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

679 
ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)), 
5094  680 
EVERY (map (fn prem => 
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

681 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1 APPEND 
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset

682 
hyp_subst_tac 1)) prems)]); 
5094  683 

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

687 
REPEAT (EVERY 

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

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

7293  690 
rewrite_goals_tac sum_case_rewrites, 
5094  691 
atac 1])]) 
692 

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

693 
in standard (split_rule factors (induct RS lemma)) end; 
5094  694 

6424  695 

696 

10735  697 
(** specification of (co)inductive sets **) 
5094  698 

10729  699 
fun cond_declare_consts declare_consts cs paramTs cnames = 
700 
if declare_consts then 

701 
Theory.add_consts_i (map (fn (c, n) => (n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

702 
else I; 

703 

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

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

708 
val setT = HOLogic.mk_setT sumT; 

709 

10735  710 
val fp_name = if coind then gfp_name else lfp_name; 
5094  711 

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

714 

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

717 
(* is transformed into *) 

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

719 

720 
fun transform_rule r = 

721 
let 

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

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

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

727 

728 
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) 

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

729 
(frees, foldr1 HOLogic.mk_conj 
5149  730 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  731 
(map (subst o HOLogic.dest_Trueprop) 
732 
(Logic.strip_imp_prems r)))) 

733 
end 

734 

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

736 

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

738 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  739 

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

741 

742 
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; 

6394  743 
val full_rec_name = 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) " ^ 

771 
commas_quote 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, 

9939  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 

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 

10735  836 
val full_cnames = map (try_term (fst o dest_Const o head_of) 
5094  837 
"Recursive set not previously declared as constant: " sign) cs; 
6437  838 
val cnames = map Sign.base_name full_cnames; 
5094  839 

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

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

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

9405  845 
val (thy1, result as {elims, induct, ...}) = 
11628  846 
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos 
12180  847 
thy params paramTs cTs cnames induct_cases; 
8307  848 
val thy2 = thy1 
849 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

12172  850 
> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1) 
851 
full_cnames elims induct; 

6437  852 
in (thy2, result) end; 
5094  853 

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

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

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

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

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

6424  863 
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

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

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

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

6424  872 

873 

6437  874 
(** package setup **) 
875 

876 
(* setup theory *) 

877 

8634  878 
val setup = 
879 
[InductiveData.init, 

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

884 

885 
(* outer syntax *) 

6424  886 

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

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

6424  891 

892 
fun ind_decl coind = 

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

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

895 
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

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

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

901 

902 
val coinductiveP = 

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

6424  904 

7107  905 

906 
val ind_cases = 

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

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

910 
val inductive_casesP = 

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

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

5094  917 
end; 
6424  918 

919 
end; 