author  wenzelm 
Thu, 13 Jul 2000 11:42:11 +0200  
changeset 9298  7d9b562a750b 
parent 9235  1f734dc2e526 
child 9315  f793f05024f6 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Stefan Berghofer, TU Muenchen 

5 
Copyright 1994 University of Cambridge 

6 
1998 TU Muenchen 

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 
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 
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

35 
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

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

37 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm}) option 
6437  38 
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

39 
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

40 
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

41 
val get_monos: theory > thm list 
6424  42 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
6521  43 
theory attribute list > ((bstring * term) * theory attribute list) list > 
44 
thm list > thm list > theory > theory * 

6424  45 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  46 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
6521  47 
val add_inductive: bool > bool > string list > Args.src list > 
48 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 

49 
(xstring * Args.src list) list > theory > theory * 

6424  50 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  51 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
7107  52 
val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text 
53 
> theory > theory 

54 
val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text 

55 
> theory > theory 

6437  56 
val setup: (theory > theory) list 
5094  57 
end; 
58 

6424  59 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  60 
struct 
61 

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

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

63 

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

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

65 

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

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

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

68 
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

69 

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

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

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

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

73 
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

74 

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

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

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

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

78 
fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2), 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

79 
Library.generic_merge Thm.eq_thm I I monos1 monos2); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

80 

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

81 
fun print sg (tab, monos) = 
8720  82 
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)), 
83 
Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)] 

84 
> Pretty.chunks > Pretty.writeln; 

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

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

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

89 

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

90 

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

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

92 

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

93 
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

94 

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

95 
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

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

97 
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

98 
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

99 
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

100 
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

101 

8277  102 

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

105 

8277  106 
val get_monos = snd o InductiveData.get; 
107 
fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy; 

108 

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

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

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

111 
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

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

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

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

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

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

117 
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

118 
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

119 
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

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

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

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

123 

8634  124 

125 
(* attributes *) 

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

126 

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

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

128 

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

129 
fun map_rules_global f thy = put_monos (f (get_monos thy)) thy; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

130 

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

131 
fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

132 
fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm); 
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 
fun mk_att f g (x, thm) = (f (g thm) x, thm); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

135 

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

136 
in 
8634  137 
val mono_add_global = mk_att map_rules_global add_mono; 
138 
val mono_del_global = mk_att map_rules_global del_mono; 

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

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

140 

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

141 
val mono_attr = 
8634  142 
(Attrib.add_del_args mono_add_global mono_del_global, 
143 
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

144 

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

145 

7107  146 

6424  147 
(** utilities **) 
148 

149 
(* messages *) 

150 

5662  151 
val quiet_mode = ref false; 
152 
fun message s = if !quiet_mode then () else writeln s; 

153 

6424  154 
fun coind_prefix true = "co" 
155 
 coind_prefix false = ""; 

156 

157 

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

158 
(* the following code ensures that each recursive set *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

159 
(* always has the same type in all introduction rules *) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

160 

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

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

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

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

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

165 
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

166 
fun varify (t, (i, ts)) = 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

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

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

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

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

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

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

174 
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

175 
in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

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

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

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

179 
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

180 
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

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

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

183 

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

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

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

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

187 

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

188 

6424  189 
(* misc *) 
190 

5094  191 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); 
192 

6394  193 
val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op ``"; 
194 
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; 

5094  195 

196 
(* make injections needed in mutually recursive definitions *) 

197 

198 
fun mk_inj cs sumT c x = 

199 
let 

200 
fun mk_inj' T n i = 

201 
if n = 1 then x else 

202 
let val n2 = n div 2; 

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

204 
in 

205 
if i <= n2 then 

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

207 
else 

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

209 
end 

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

211 
end; 

212 

213 
(* make "vimage" terms for selecting out components of mutually rec.def. *) 

214 

215 
fun mk_vimage cs sumT t c = if length cs < 2 then t else 

216 
let 

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

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

219 
in 

220 
Const (vimage_name, vimageT) $ 

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

222 
end; 

223 

6424  224 

225 

226 
(** wellformedness checks **) 

5094  227 

228 
fun err_in_rule sign t msg = error ("Illformed introduction rule\n" ^ 

229 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

230 

231 
fun err_in_prem sign t p msg = error ("Illformed premise\n" ^ 

232 
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^ 

233 
(Sign.string_of_term sign t) ^ "\n" ^ msg); 

234 

235 
val msg1 = "Conclusion of introduction rule must have form\ 

236 
\ ' t : S_i '"; 

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

237 
val msg2 = "Nonatomic premise"; 
5094  238 
val msg3 = "Recursion term on left of member symbol"; 
239 

240 
fun check_rule sign cs r = 

241 
let 

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

242 
fun check_prem prem = if can HOLogic.dest_Trueprop prem then () 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

243 
else err_in_prem sign r prem msg2; 
5094  244 

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

245 
in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

246 
(Const ("op :", _) $ t $ u) => 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

247 
if u mem cs then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

248 
if exists (Logic.occs o (rpair t)) cs then 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

251 
seq check_prem (Logic.strip_imp_prems r) 
5094  252 
else err_in_rule sign r msg1 
253 
 _ => err_in_rule sign r msg1) 

254 
end; 

255 

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

256 
fun try' f msg sign t = (case (try f t) of 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

257 
Some x => x 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

258 
 None => error (msg ^ Sign.string_of_term sign t)); 
5094  259 

6424  260 

5094  261 

6424  262 
(*** properties of (co)inductive sets ***) 
263 

264 
(** elimination rules **) 

5094  265 

8375  266 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  267 
let 
268 
val used = foldr add_term_names (intr_ts, []); 

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

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

271 

272 
fun dest_intr r = 

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

274 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

276 

8380  277 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  278 

279 
fun mk_elim (c, T) = 

280 
let 

281 
val a = Free (aname, T); 

282 

283 
fun mk_elim_prem (_, t, ts) = 

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

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

8375  286 
val c_intrs = (filter (equal c o #1 o #1) intrs); 
5094  287 
in 
8375  288 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
289 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  290 
end 
291 
in 

292 
map mk_elim (cs ~~ cTs) 

293 
end; 

294 

6424  295 

296 

297 
(** premises and conclusions of induction rules **) 

5094  298 

299 
fun mk_indrule cs cTs params intr_ts = 

300 
let 

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

302 

303 
(* predicates for induction rule *) 

304 

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

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

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

308 

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

310 

311 
fun mk_ind_prem r = 

312 
let 

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

314 

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

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

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

317 
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

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

319 
None => (m $ 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

320 
 Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t))) 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

323 
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

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

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

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

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

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

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

330 

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

331 
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

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

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

334 

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

337 

338 
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

339 
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem 
5094  340 
(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

341 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  342 
end; 
343 

344 
val ind_prems = map mk_ind_prem intr_ts; 

345 

346 
(* make conclusions for induction rules *) 

347 

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

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

350 
val Ts = HOLogic.prodT_factors T; 

351 
val (frees, x') = foldr (fn (T', (fs, s)) => 

352 
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); 

353 
val tuple = HOLogic.mk_tuple T frees; 

354 
in ((HOLogic.mk_binop "op >" 

355 
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') 

356 
end; 

357 

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

358 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  359 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
360 

361 
in (preds, ind_prems, mutual_ind_concl) 

362 
end; 

363 

6424  364 

5094  365 

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

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

367 

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

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

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

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

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

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

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

374 

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

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

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

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

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

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

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

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

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

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

384 

8375  385 
fun add_cases_induct no_elim no_ind names elims induct induct_cases = 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

386 
let 
8375  387 
fun cases_spec (name, elim) = (("", elim), [InductMethod.cases_set_global name]); 
388 
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

389 

8375  390 
fun induct_spec (name, th) = 
8380  391 
(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]); 
8401  392 
val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); 
8433  393 
in #1 o PureThy.add_thms (cases_specs @ induct_specs) end; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

394 

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

395 

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

396 

6424  397 
(*** proofs for (co)inductive sets ***) 
398 

399 
(** prove monotonicity **) 

5094  400 

401 
fun prove_mono setT fp_fun monos thy = 

402 
let 

6427  403 
val _ = message " Proving monotonicity ..."; 
5094  404 

6394  405 
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 
5094  406 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

407 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]) 
5094  408 

409 
in mono end; 

410 

6424  411 

412 

413 
(** prove introduction rules **) 

5094  414 

415 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

416 
let 

6427  417 
val _ = message " Proving the introduction rules ..."; 
5094  418 

419 
val unfold = standard (mono RS (fp_def RS 

420 
(if coind then def_gfp_Tarski else def_lfp_Tarski))); 

421 

422 
fun select_disj 1 1 = [] 

423 
 select_disj _ 1 = [rtac disjI1] 

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

425 

426 
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs 

6394  427 
(cterm_of (Theory.sign_of thy) intr) (fn prems => 
5094  428 
[(*insert prems and underlying sets*) 
429 
cut_facts_tac prems 1, 

430 
stac unfold 1, 

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

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

433 
EVERY1 (select_disj (length intr_ts) i), 

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

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

436 
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1), 

437 
(*Now solve the equations like Inl 0 = Inl ?b2*) 

438 
rewrite_goals_tac con_defs, 

439 
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts) 

440 

441 
in (intrs, unfold) end; 

442 

6424  443 

444 

445 
(** prove elimination rules **) 

5094  446 

8375  447 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  448 
let 
6427  449 
val _ = message " Proving the elimination rules ..."; 
5094  450 

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

451 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

452 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ 
5094  453 
map make_elim [Inl_inject, Inr_inject]; 
8375  454 
in 
455 
map (fn (t, cases) => prove_goalw_cterm rec_sets_defs 

6394  456 
(cterm_of (Theory.sign_of thy) t) (fn prems => 
5094  457 
[cut_facts_tac [hd prems] 1, 
458 
dtac (unfold RS subst) 1, 

459 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

460 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

461 
EVERY (map (fn prem => 

8375  462 
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) 
463 
> RuleCases.name cases) 

464 
(mk_elims cs cTs params intr_ts intr_names) 

465 
end; 

5094  466 

6424  467 

5094  468 
(** derivation of simplified elimination rules **) 
469 

470 
(*Applies freeness of the given constructors, which *must* be unfolded by 

471 
the given defs. Cannot simply use the local con_defs because con_defs=[] 

472 
for inference systems. 

473 
*) 

474 

7107  475 
(*cprop should have the form t:Si where Si is an inductive set*) 
8336
fdf3ac335f77
mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
wenzelm
parents:
8316
diff
changeset

476 
fun mk_cases_i solved elims ss cprop = 
7107  477 
let 
478 
val prem = Thm.assume cprop; 

9298  479 
val tac = ALLGOALS (InductMethod.simp_case_tac solved ss) THEN prune_params_tac; 
480 
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl)); 

7107  481 
in 
482 
(case get_first (try mk_elim) elims of 

483 
Some r => r 

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

485 
[Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk, 

486 
Display.pretty_cterm cprop]))) 

487 
end; 

488 

6141  489 
fun mk_cases elims s = 
8336
fdf3ac335f77
mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)tac;
wenzelm
parents:
8316
diff
changeset

490 
mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
7107  491 

492 

493 
(* inductive_cases(_i) *) 

494 

495 
fun gen_inductive_cases prep_att prep_const prep_prop 

496 
((((name, raw_atts), raw_set), raw_props), comment) thy = 

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

497 
let val sign = Theory.sign_of thy; 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

498 
in (case get_inductive thy (prep_const sign raw_set) of 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

499 
None => error ("Unknown (co)inductive set " ^ quote name) 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

500 
 Some (_, {elims, ...}) => 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

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

502 
val atts = map (prep_att thy) raw_atts; 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

503 
val cprops = map 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

504 
(Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

505 
val thms = map 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

506 
(mk_cases_i true elims (Simplifier.simpset_of thy)) cprops; 
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

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

508 
thy > IsarThy.have_theorems_i 
9201  509 
[(((name, atts), map Thm.no_attributes thms), comment)] 
9116
9df44b5c610b
get_inductive now returns None instead of raising an exception.
berghofe
parents:
9072
diff
changeset

510 
end) 
5094  511 
end; 
512 

7107  513 
val inductive_cases = 
514 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

515 

516 
val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; 

517 

6424  518 

519 

520 
(** prove induction rule **) 

5094  521 

522 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

523 
fp_def rec_sets_defs thy = 

524 
let 

6427  525 
val _ = message " Proving the induction rule ..."; 
5094  526 

6394  527 
val sign = Theory.sign_of thy; 
5094  528 

7293  529 
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of 
530 
None => [] 

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

532 

5094  533 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
534 

535 
(* make predicate for instantiation of abstract induction rule *) 

536 

537 
fun mk_ind_pred _ [P] = P 

538 
 mk_ind_pred T Ps = 

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

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

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

544 
end; 

545 

546 
val ind_pred = mk_ind_pred sumT preds; 

547 

548 
val ind_concl = HOLogic.mk_Trueprop 

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

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

551 

552 
(* simplification rules for vimage and Collect *) 

553 

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

555 
map (fn c => prove_goalw_cterm [] (cterm_of sign 

556 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 

557 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

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

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

7293  560 
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, 
5094  561 
rtac refl 1])) cs; 
562 

563 
val induct = prove_goalw_cterm [] (cterm_of sign 

564 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 

565 
[rtac (impI RS allI) 1, 

566 
DETERM (etac (mono RS (fp_def RS def_induct)) 1), 

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

567 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  568 
fold_goals_tac rec_sets_defs, 
569 
(*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

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

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

573 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  574 
rewrite_goals_tac sum_case_rewrites, 
5094  575 
EVERY (map (fn prem => 
5149  576 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  577 

578 
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign 

579 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 

580 
[cut_facts_tac prems 1, 

581 
REPEAT (EVERY 

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

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

7293  584 
rewrite_goals_tac sum_case_rewrites, 
5094  585 
atac 1])]) 
586 

587 
in standard (split_rule (induct RS lemma)) 

588 
end; 

589 

6424  590 

591 

592 
(*** specification of (co)inductive sets ****) 

593 

594 
(** definitional introduction of (co)inductive sets **) 

5094  595 

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

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

597 
params paramTs cTs cnames = 
5094  598 
let 
599 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

600 
val setT = HOLogic.mk_setT sumT; 

601 

6394  602 
val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" 
603 
else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; 

5094  604 

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

607 

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

610 
(* is transformed into *) 

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

612 

613 
fun transform_rule r = 

614 
let 

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

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

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

620 

621 
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

622 
(frees, foldr1 HOLogic.mk_conj 
5149  623 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  624 
(map (subst o HOLogic.dest_Trueprop) 
625 
(Logic.strip_imp_prems r)))) 

626 
end 

627 

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

629 

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

631 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  632 

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

634 

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

6394  636 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  637 

638 
val rec_const = list_comb 

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

640 

641 
val fp_def_term = Logic.mk_equals (rec_const, 

642 
Const (fp_name, (setT > setT) > setT) $ fp_fun) 

643 

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

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

646 

8433  647 
val (thy', [fp_def :: rec_sets_defs]) = 
648 
thy 

649 
> (if declare_consts then 

650 
Theory.add_consts_i (map (fn (c, n) => 

651 
(n, paramTs > fastype_of c, NoSyn)) (cs ~~ cnames)) 

652 
else I) 

653 
> (if length cs < 2 then I 

654 
else Theory.add_consts_i [(rec_name, paramTs > setT, NoSyn)]) 

655 
> Theory.add_path rec_name 

656 
> PureThy.add_defss_i [(("defs", def_terms), [])]; 

5094  657 

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

658 
val mono = prove_mono setT fp_fun monos thy' 
5094  659 

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

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

661 
(thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

662 
end; 
5094  663 

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

664 
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

665 
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

667 
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

668 
commas_quote cnames) else (); 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

669 

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

670 
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

671 

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

672 
val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

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

675 

5094  676 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 
677 
rec_sets_defs thy'; 

678 
val elims = if no_elim then [] else 

8375  679 
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy'; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

680 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  681 
if coind then standard (rule_by_tactic 
5553  682 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  683 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
684 
else 

685 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

686 
rec_sets_defs thy'; 

5108  687 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  688 
else standard (raw_induct RSN (2, rev_mp)); 
689 

8433  690 
val (thy'', [intrs']) = 
691 
thy' 

6521  692 
> PureThy.add_thmss [(("intrs", intrs), atts)] 
8433  693 
>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)) 
694 
>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])]) 

695 
>> (if no_ind then I else #1 o PureThy.add_thms 

8401  696 
[((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])]) 
8433  697 
>> Theory.parent_path; 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

698 
val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims"; (* FIXME improve *) 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

699 
val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct"); (* FIXME improve *) 
5094  700 
in (thy'', 
701 
{defs = fp_def::rec_sets_defs, 

702 
mono = mono, 

703 
unfold = unfold, 

7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

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

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

706 
mk_cases = mk_cases elims', 
5094  707 
raw_induct = raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

708 
induct = induct'}) 
5094  709 
end; 
710 

6424  711 

712 

713 
(** axiomatic introduction of (co)inductive sets **) 

5094  714 

715 
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs 

8401  716 
atts intros monos con_defs thy params paramTs cTs cnames induct_cases = 
5094  717 
let 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

718 
val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames); 
5094  719 

6424  720 
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); 
9235  721 
val (thy', _, fp_def, rec_sets_defs, _, _) = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

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

723 
params paramTs cTs cnames; 
8375  724 
val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names); 
5094  725 
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
726 
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); 

727 

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

728 
val thy'' = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

729 
thy' 
8433  730 
> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])]) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

731 
> (if coind then I else 
8433  732 
#1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); 
5094  733 

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

734 
val intrs = PureThy.get_thms thy'' "intrs"; 
8375  735 
val elims = map2 (fn (th, cases) => RuleCases.name cases th) 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

736 
(PureThy.get_thms thy'' "raw_elims", elim_cases); 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

737 
val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct"; 
5094  738 
val induct = if coind orelse length cs > 1 then raw_induct 
739 
else standard (raw_induct RSN (2, rev_mp)); 

740 

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

741 
val (thy''', ([elims'], intrs')) = 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

742 
thy'' 
8375  743 
> PureThy.add_thmss [(("elims", elims), [])] 
8433  744 
>> (if coind then I 
745 
else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])]) 

746 
>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) 

747 
>> Theory.parent_path; 

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

748 
val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct"; 
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

749 
in (thy''', 
9235  750 
{defs = fp_def :: rec_sets_defs, 
8312
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

751 
mono = Drule.asm_rl, 
b470bc28b59d
add_cases_induct: accomodate no_elim and no_ind flags;
wenzelm
parents:
8307
diff
changeset

752 
unfold = Drule.asm_rl, 
8433  753 
intrs = intrs', 
754 
elims = elims', 

755 
mk_cases = mk_cases elims', 

5094  756 
raw_induct = raw_induct, 
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset

757 
induct = induct'}) 
5094  758 
end; 
759 

6424  760 

761 

762 
(** introduction of (co)inductive sets **) 

5094  763 

764 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

6521  765 
atts intros monos con_defs thy = 
5094  766 
let 
6424  767 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  768 
val sign = Theory.sign_of thy; 
5094  769 

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

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

772 
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ 

773 
\ component is not a free variable: " sign) params; 

774 

775 
val cTs = map (try' (HOLogic.dest_setT o fastype_of) 

776 
"Recursive component not of type set: " sign) cs; 

777 

6437  778 
val full_cnames = map (try' (fst o dest_Const o head_of) 
5094  779 
"Recursive set not previously declared as constant: " sign) cs; 
6437  780 
val cnames = map Sign.base_name full_cnames; 
5094  781 

6424  782 
val _ = seq (check_rule sign cs o snd o fst) intros; 
8401  783 
val induct_cases = map (#1 o #1) intros; 
6437  784 

785 
val (thy1, result) = 

786 
(if ! quick_and_dirty then add_ind_axm else add_ind_def) 

6521  787 
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
8401  788 
con_defs thy params paramTs cTs cnames induct_cases; 
8307  789 
val thy2 = thy1 
790 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

8401  791 
> add_cases_induct no_elim (no_ind orelse coind) full_cnames 
792 
(#elims result) (#induct result) induct_cases; 

6437  793 
in (thy2, result) end; 
5094  794 

6424  795 

5094  796 

6424  797 
(** external interface **) 
798 

6521  799 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  800 
let 
6394  801 
val sign = Theory.sign_of thy; 
8100  802 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  803 

6521  804 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  805 
val intr_names = map (fst o fst) intro_srcs; 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

806 
val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs; 
6424  807 
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

808 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  809 

6424  810 
val ((thy', con_defs), monos) = thy 
811 
> IsarThy.apply_theorems raw_monos 

812 
> apfst (IsarThy.apply_theorems raw_con_defs); 

813 
in 

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

814 
add_inductive_i verbose false "" coind false false cs' 
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset

815 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  816 
end; 
817 

6424  818 

819 

6437  820 
(** package setup **) 
821 

822 
(* setup theory *) 

823 

8634  824 
val setup = 
825 
[InductiveData.init, 

826 
Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]]; 

6437  827 

828 

829 
(* outer syntax *) 

6424  830 

6723  831 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  832 

6521  833 
fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = 
6723  834 
#1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; 
6424  835 

836 
fun ind_decl coind = 

6729  837 
(Scan.repeat1 P.term  P.marg_comment)  
838 
(P.$$$ "intrs"  

7152  839 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  840 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
841 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  842 
>> (Toplevel.theory o mk_ind coind); 
843 

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

846 

847 
val coinductiveP = 

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

6424  849 

7107  850 

851 
val ind_cases = 

852 
P.opt_thm_name "="  P.xname  P.$$$ ":"  Scan.repeat1 P.prop  P.marg_comment 

853 
>> (Toplevel.theory o inductive_cases); 

854 

855 
val inductive_casesP = 

856 
OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules" 

857 
K.thy_decl ind_cases; 

858 

6424  859 
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; 
7107  860 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  861 

5094  862 
end; 
6424  863 

864 

865 
end; 