author  paulson 
Fri, 01 Jun 2001 11:03:50 +0200  
changeset 11358  416ea5c009f5 
parent 11036  3c30f7b97a50 
child 11502  e80a712982e1 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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

5094  6 
Copyright 1994 University of Cambridge 
9598  7 
1998 TU Muenchen 
5094  8 

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

11 
Features: 

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

14 
* mutually recursive definitions 

15 
* definitions involving arbitrary monotone operators 

16 
* automatically proves introduction and elimination rules 

5094  17 

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

5094  20 

21 
Introduction rules have the form 

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

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

25 
ti, t are any terms 

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

27 

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

5094  30 
*) 
31 

32 
signature INDUCTIVE_PACKAGE = 

33 
sig 

6424  34 
val quiet_mode: 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 
6437  40 
val print_inductives: theory > unit 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

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

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

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

46 
val rulify: thm > thm 
10735  47 
val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text 
48 
> theory > theory 

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

50 
> theory > theory 

6424  51 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
6521  52 
theory attribute list > ((bstring * term) * theory attribute list) list > 
53 
thm list > thm list > theory > theory * 

6424  54 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  55 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
6521  56 
val add_inductive: bool > bool > string list > Args.src list > 
57 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 

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

6424  59 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  60 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
61 
val setup: (theory > theory) list 

5094  62 
end; 
63 

6424  64 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  65 
struct 
66 

9598  67 

10729  68 
(** theory context references **) 
69 

10735  70 
val mono_name = "Ord.mono"; 
71 
val gfp_name = "Gfp.gfp"; 

72 
val lfp_name = "Lfp.lfp"; 

73 
val vimage_name = "Inverse_Image.vimage"; 

74 
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD); 

75 

10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

76 
val inductive_forall_name = "Inductive.forall"; 
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset

77 
val inductive_forall_def = thm "forall_def"; 
10735  78 
val inductive_conj_name = "Inductive.conj"; 
10729  79 
val inductive_conj_def = thm "conj_def"; 
80 
val inductive_conj = thms "inductive_conj"; 

81 
val inductive_atomize = thms "inductive_atomize"; 

82 
val inductive_rulify1 = thms "inductive_rulify1"; 

83 
val inductive_rulify2 = thms "inductive_rulify2"; 

84 

85 

86 

10735  87 
(** theory data **) 
7710
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 
(* data kind 'HOL/inductive' *) 
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 
type inductive_info = 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

93 
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

94 

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

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

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

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

98 
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

99 

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

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

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

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

103 
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

104 
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

105 

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

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

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

111 

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

112 
structure InductiveData = TheoryDataFun(InductiveArgs); 
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

114 

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

115 

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

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

117 

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

118 
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

119 

9598  120 
fun the_inductive thy name = 
121 
(case get_inductive thy name of 

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

123 
 Some info => info); 

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; 
10735  169 
fun message s = if ! quiet_mode then () else writeln s; 
170 
fun clean_message s = if ! quick_and_dirty then () else message s; 

5662  171 

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

174 

175 

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

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

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

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

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

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

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

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

184 
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

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

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

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

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

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

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

191 
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

192 
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

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

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

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

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

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

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

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

200 

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

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

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

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

204 

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

205 

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

209 
fun mk_inj' T n i = 

210 
if n = 1 then x else 

211 
let val n2 = n div 2; 

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

213 
in 

214 
if i <= n2 then 

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

216 
else 

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

218 
end 

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

220 
end; 

221 

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

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

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

227 
in 

228 
Const (vimage_name, vimageT) $ 

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

230 
end; 

231 

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

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

233 

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

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

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

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

237 

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

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

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

240 
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

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

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

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

244 

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

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

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

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

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

249 

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

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

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

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

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

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

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

256 

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

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

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

259 
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

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

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

262 

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

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

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

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

266 
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

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

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

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

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

271 

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

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

273 

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

274 
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

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

276 

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

277 
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

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

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

281 

10729  282 
(** process rules **) 
283 

284 
local 

5094  285 

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

288 

289 
fun err_in_prem sg name t p msg = 

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

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

5094  292 

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

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

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

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

297 

11036  298 
val atomize_cterm = hol_rewrite_cterm inductive_atomize; 
10729  299 

300 
in 

5094  301 

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

304 
val concl = Logic.strip_imp_concl rule; 

305 
val prems = Logic.strip_imp_prems rule; 

306 
val aprems = prems > map (Thm.term_of o atomize_cterm o Thm.cterm_of sg); 

307 
val arule = Logic.list_implies (aprems, concl); 

5094  308 

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

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

312 
in 

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

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

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

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

318 
else seq check_prem (prems ~~ aprems) 

319 
else err_in_rule sg name rule bad_concl 

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

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

323 
end; 

5094  324 

10729  325 
val rulify = 
10804  326 
standard o Tactic.norm_hhf o 
11036  327 
hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o 
328 
hol_simplify inductive_conj; 

10729  329 

330 
end; 

331 

5094  332 

6424  333 

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

10735  336 
(* elimination rules *) 
5094  337 

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

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

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

343 

344 
fun dest_intr r = 

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

346 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

348 

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

351 
fun mk_elim (c, T) = 

352 
let 

353 
val a = Free (aname, T); 

354 

355 
fun mk_elim_prem (_, t, ts) = 

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

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

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

5094  362 
end 
363 
in 

364 
map mk_elim (cs ~~ cTs) 

365 
end; 

9598  366 

6424  367 

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

370 
fun mk_indrule cs cTs params intr_ts = 

371 
let 

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

373 

374 
(* predicates for induction rule *) 

375 

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

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

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

379 

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

381 

382 
fun mk_ind_prem r = 

383 
let 

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

385 

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

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

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

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

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

390 
None => (m $ fst (subst t) $ fst (subst u), None) 
10735  391 
 Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t))) 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

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

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

394 
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

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

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

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

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

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

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

401 

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

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

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

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

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

408 

409 
in list_all_free (frees, 

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

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

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

415 
val ind_prems = map mk_ind_prem intr_ts; 

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

416 
val factors = foldl (mg_prod_factors preds) ([], ind_prems); 
5094  417 

418 
(* make conclusions for induction rules *) 

419 

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

421 
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

422 
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

423 
val Ts = prodT_factors [] ps T; 
5094  424 
val (frees, x') = foldr (fn (T', (fs, s)) => 
425 
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); 

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

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

429 
end; 

430 

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

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

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

434 
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

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

6424  438 

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

440 

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

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

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

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

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

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

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

447 

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

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

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

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

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

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

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

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

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

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

457 

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

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

462 
> Theory.add_path (Sign.base_name name) 

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

466 

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

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

471 

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

472 

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

473 

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

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

478 
fun prove_mono setT fp_fun monos thy = 

10735  479 
(message " Proving monotonicity ..."; 
480 
Goals.prove_goalw_cterm [] (*NO SkipProof.prove_goalw_cterm here!*) 

481 
(Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop 

5094  482 
(Const (mono_name, (setT > setT) > HOLogic.boolT) $ fp_fun))) 
10735  483 
(fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])); 
5094  484 

6424  485 

10735  486 
(* prove introduction rules *) 
5094  487 

488 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

489 
let 

10735  490 
val _ = clean_message " Proving the introduction rules ..."; 
5094  491 

492 
val unfold = standard (mono RS (fp_def RS 

10186  493 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  494 

495 
fun select_disj 1 1 = [] 

496 
 select_disj _ 1 = [rtac disjI1] 

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

498 

10735  499 
val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs 
500 
(Thm.cterm_of (Theory.sign_of thy) intr) (fn prems => 

5094  501 
[(*insert prems and underlying sets*) 
502 
cut_facts_tac prems 1, 

503 
stac unfold 1, 

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

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

506 
EVERY1 (select_disj (length intr_ts) i), 

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

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

10735  509 
DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), 
5094  510 
(*Now solve the equations like Inl 0 = Inl ?b2*) 
511 
rewrite_goals_tac con_defs, 

10729  512 
REPEAT (rtac refl 1)]) 
513 
> rulify) (1 upto (length intr_ts) ~~ intr_ts) 

5094  514 

515 
in (intrs, unfold) end; 

516 

6424  517 

10735  518 
(* prove elimination rules *) 
5094  519 

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

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

524 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
10735  525 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; 
8375  526 
in 
11005  527 
mk_elims cs cTs params intr_ts intr_names > map (fn (t, cases) => 
528 
SkipProof.prove_goalw_cterm thy rec_sets_defs 

529 
(Thm.cterm_of (Theory.sign_of thy) t) (fn prems => 

530 
[cut_facts_tac [hd prems] 1, 

531 
dtac (unfold RS subst) 1, 

532 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

533 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

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

535 
> rulify 

536 
> RuleCases.name cases) 

8375  537 
end; 
5094  538 

6424  539 

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

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

9598  543 
the given defs. Cannot simply use the local con_defs because con_defs=[] 
10735  544 
for inference systems. (??) *) 
5094  545 

7107  546 
(*cprop should have the form t:Si where Si is an inductive set*) 
9598  547 

10735  548 
val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\""; 
9598  549 

550 
fun mk_cases_i elims ss cprop = 

7107  551 
let 
552 
val prem = Thm.assume cprop; 

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

557 
Some r => r 

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

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

6141  562 
fun mk_cases elims s = 
9598  563 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
564 

565 
fun smart_mk_cases thy ss cprop = 

566 
let 

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

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

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

570 
in mk_cases_i elims ss cprop end; 

7107  571 

572 

573 
(* inductive_cases(_i) *) 

574 

575 
fun gen_inductive_cases prep_att prep_const prep_prop 

9598  576 
(((name, raw_atts), raw_props), comment) thy = 
577 
let 

578 
val ss = Simplifier.simpset_of thy; 

579 
val sign = Theory.sign_of thy; 

580 
val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; 

581 
val atts = map (prep_att thy) raw_atts; 

582 
val thms = map (smart_mk_cases thy ss) cprops; 

583 
in thy > IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end; 

5094  584 

7107  585 
val inductive_cases = 
586 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

587 

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

589 

6424  590 

9598  591 
(* mk_cases_meth *) 
592 

593 
fun mk_cases_meth (ctxt, raw_props) = 

594 
let 

595 
val thy = ProofContext.theory_of ctxt; 

596 
val ss = Simplifier.get_local_simpset ctxt; 

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

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

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

601 

602 

10735  603 
(* prove induction rule *) 
5094  604 

605 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

606 
fp_def rec_sets_defs thy = 

607 
let 

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

6394  610 
val sign = Theory.sign_of thy; 
5094  611 

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

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

615 

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

616 
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

617 
mk_indrule cs cTs params intr_ts; 
5094  618 

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

620 

621 
fun mk_ind_pred _ [P] = P 

622 
 mk_ind_pred T Ps = 

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

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

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

628 
end; 

629 

630 
val ind_pred = mk_ind_pred sumT preds; 

631 

632 
val ind_concl = HOLogic.mk_Trueprop 

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

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

635 

636 
(* simplification rules for vimage and Collect *) 

637 

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

10735  639 
map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign 
5094  640 
(HOLogic.mk_Trueprop (HOLogic.mk_eq 
641 
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, 

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

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

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

10735  646 
val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign 
5094  647 
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => 
648 
[rtac (impI RS allI) 1, 

10202  649 
DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1), 
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset

650 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  651 
fold_goals_tac rec_sets_defs, 
652 
(*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

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

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

656 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  657 
rewrite_goals_tac sum_case_rewrites, 
5094  658 
EVERY (map (fn prem => 
5149  659 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  660 

10735  661 
val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign 
5094  662 
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => 
663 
[cut_facts_tac prems 1, 

664 
REPEAT (EVERY 

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

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

7293  667 
rewrite_goals_tac sum_case_rewrites, 
5094  668 
atac 1])]) 
669 

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

670 
in standard (split_rule factors (induct RS lemma)) end; 
5094  671 

6424  672 

673 

10735  674 
(** specification of (co)inductive sets **) 
5094  675 

10729  676 
fun cond_declare_consts declare_consts cs paramTs cnames = 
677 
if declare_consts then 

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

679 
else I; 

680 

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

681 
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

682 
params paramTs cTs cnames = 
5094  683 
let 
684 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

685 
val setT = HOLogic.mk_setT sumT; 

686 

10735  687 
val fp_name = if coind then gfp_name else lfp_name; 
5094  688 

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

691 

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

694 
(* is transformed into *) 

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

696 

697 
fun transform_rule r = 

698 
let 

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

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

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

704 

705 
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

706 
(frees, foldr1 HOLogic.mk_conj 
5149  707 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  708 
(map (subst o HOLogic.dest_Trueprop) 
709 
(Logic.strip_imp_prems r)))) 

710 
end 

711 

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

713 

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

715 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  716 

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

718 

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

6394  720 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  721 

722 
val rec_const = list_comb 

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

724 

725 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  726 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  727 

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

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

730 

8433  731 
val (thy', [fp_def :: rec_sets_defs]) = 
732 
thy 

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

736 
> Theory.add_path rec_name 

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

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

739 
val mono = prove_mono setT fp_fun monos thy' 
5094  740 

10735  741 
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  742 

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

743 
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

744 
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

745 
let 
10735  746 
val _ = 
747 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 

748 
commas_quote cnames) else (); 

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

749 

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

750 
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

751 

9939  752 
val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) = 
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset

753 
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

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

755 

5094  756 
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs 
9939  757 
rec_sets_defs thy1; 
5094  758 
val elims = if no_elim then [] else 
9939  759 
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

760 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  761 
if coind then standard (rule_by_tactic 
5553  762 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  763 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
764 
else 

765 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

9939  766 
rec_sets_defs thy1; 
5108  767 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  768 
else standard (raw_induct RSN (2, rev_mp)); 
769 

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

10735  772 
val (thy3, ([intrs'', elims'], [induct'])) = 
773 
thy2 

11005  774 
> PureThy.add_thmss 
775 
[(("intros", intrs'), atts), 

776 
(("elims", elims), [RuleCases.consumes 1])] 

10735  777 
>>> PureThy.add_thms 
11005  778 
[((coind_prefix coind ^ "induct", rulify induct), 
779 
[RuleCases.case_names induct_cases, 

780 
RuleCases.consumes 1])] 

8433  781 
>> Theory.parent_path; 
9939  782 
in (thy3, 
10735  783 
{defs = fp_def :: rec_sets_defs, 
5094  784 
mono = mono, 
785 
unfold = unfold, 

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

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

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

790 
induct = induct'}) 
5094  791 
end; 
792 

6424  793 

10735  794 
(* external interfaces *) 
5094  795 

10735  796 
fun try_term f msg sign t = 
797 
(case Library.try f t of 

798 
Some x => x 

799 
 None => error (msg ^ Sign.string_of_term sign t)); 

5094  800 

801 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

10729  802 
atts pre_intros monos con_defs thy = 
5094  803 
let 
6424  804 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  805 
val sign = Theory.sign_of thy; 
5094  806 

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

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

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

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

10735  815 
val full_cnames = map (try_term (fst o dest_Const o head_of) 
5094  816 
"Recursive set not previously declared as constant: " sign) cs; 
6437  817 
val cnames = map Sign.base_name full_cnames; 
5094  818 

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

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

8401  822 
val induct_cases = map (#1 o #1) intros; 
6437  823 

9405  824 
val (thy1, result as {elims, induct, ...}) = 
10735  825 
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos 
8401  826 
con_defs thy params paramTs cTs cnames induct_cases; 
8307  827 
val thy2 = thy1 
828 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

11005  829 
> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct; 
6437  830 
in (thy2, result) end; 
5094  831 

6521  832 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  833 
let 
6394  834 
val sign = Theory.sign_of thy; 
8100  835 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  836 

6521  837 
val atts = map (Attrib.global_attribute thy) srcs; 
6424  838 
val intr_names = map (fst o fst) intro_srcs; 
9405  839 
fun read_rule s = Thm.read_cterm sign (s, propT) 
840 
handle ERROR => error ("The error(s) above occurred for " ^ s); 

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

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

843 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  844 

6424  845 
val ((thy', con_defs), monos) = thy 
846 
> IsarThy.apply_theorems raw_monos 

847 
> apfst (IsarThy.apply_theorems raw_con_defs); 

848 
in 

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

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

850 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  851 
end; 
852 

6424  853 

854 

6437  855 
(** package setup **) 
856 

857 
(* setup theory *) 

858 

8634  859 
val setup = 
860 
[InductiveData.init, 

9625  861 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  862 
"dynamic case analysis on sets")], 
9893  863 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  864 

865 

866 
(* outer syntax *) 

6424  867 

6723  868 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  869 

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

873 
fun ind_decl coind = 

6729  874 
(Scan.repeat1 P.term  P.marg_comment)  
9598  875 
(P.$$$ "intros"  
7152  876 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  877 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
878 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  879 
>> (Toplevel.theory o mk_ind coind); 
880 

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

883 

884 
val coinductiveP = 

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

6424  886 

7107  887 

888 
val ind_cases = 

9625  889 
P.opt_thm_name ":"  Scan.repeat1 P.prop  P.marg_comment 
7107  890 
>> (Toplevel.theory o inductive_cases); 
891 

892 
val inductive_casesP = 

9804  893 
OuterSyntax.command "inductive_cases" 
9598  894 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  895 

9643  896 
val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"]; 
7107  897 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  898 

5094  899 
end; 
6424  900 

901 
end; 