author  wenzelm 
Fri, 14 Dec 2001 11:50:38 +0100  
changeset 12494  58848edad3c4 
parent 12400  f12f95e216e0 
child 12527  d6c91bc3e49c 
permissions  rwrr 
5094  1 
(* Title: HOL/Tools/inductive_package.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

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

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

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

10 
Features: 

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

13 
* mutually recursive definitions 

14 
* definitions involving arbitrary monotone operators 

15 
* automatically proves introduction and elimination rules 

5094  16 

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

5094  19 

20 
Introduction rules have the form 

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

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

24 
ti, t are any terms 

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

26 

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

5094  29 
*) 
30 

31 
signature INDUCTIVE_PACKAGE = 

32 
sig 

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

34 
val unify_consts: Sign.sg > term list > term list > term list * term list 
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset

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

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

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

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

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

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

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

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

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

46 
val rulify: thm > thm 
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 > 
12180  52 
((bstring * term) * theory attribute list) list > thm list > theory > theory * 
6424  53 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  54 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
11628  55 
val add_inductive: bool > bool > string list > 
6521  56 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 
12180  57 
theory > theory * 
6424  58 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  59 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
60 
val setup: (theory > theory) list 

5094  61 
end; 
62 

6424  63 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  64 
struct 
65 

9598  66 

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

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

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

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

77 
val inductive_conj_name = "HOL.induct_conj"; 

78 
val inductive_conj_def = thm "induct_conj_def"; 

79 
val inductive_conj = thms "induct_conj"; 

80 
val inductive_atomize = thms "induct_atomize"; 

81 
val inductive_rulify1 = thms "induct_rulify1"; 

82 
val inductive_rulify2 = thms "induct_rulify2"; 

10729  83 

84 

85 

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

87 

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

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

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

92 
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

93 

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

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

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

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

97 
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

98 

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

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

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

101 
val prep_ext = I; 
11502  102 
fun merge ((tab1, monos1), (tab2, monos2)) = 
103 
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); 

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

104 

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

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

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

110 

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

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

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

113 

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

114 

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

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

116 

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

117 
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

118 

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

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

122 
 Some info => info); 

123 

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

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

126 
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

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

128 
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

129 
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

130 
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

131 
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

132 

8277  133 

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

134 

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

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

136 

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

8277  139 

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

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

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

142 
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

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

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

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

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

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

148 
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

149 
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

150 
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

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

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

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

154 

8634  155 

156 
(* attributes *) 

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

157 

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

160 

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

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

164 

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

165 

7107  166 

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

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

5662  172 

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

175 

176 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

193 
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

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

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

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

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

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

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

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

201 

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

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

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

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

205 

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

206 

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

210 
fun mk_inj' T n i = 

211 
if n = 1 then x else 

212 
let val n2 = n div 2; 

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

214 
in 

215 
if i <= n2 then 

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

217 
else 

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

219 
end 

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

221 
end; 

222 

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

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

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

228 
in 

229 
Const (vimage_name, vimageT) $ 

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

231 
end; 

232 

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

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

234 

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

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

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

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

238 

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

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

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

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

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

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

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

245 

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

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

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

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

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

250 

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

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

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

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

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

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

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

257 

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

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

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

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

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

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

263 

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

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

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

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

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

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

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

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

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

272 

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

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

274 

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

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

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

277 

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

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

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

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

282 

10729  283 
(** process rules **) 
284 

285 
local 

5094  286 

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

289 

290 
fun err_in_prem sg name t p msg = 

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

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

5094  293 

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

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

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

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

298 

11781  299 
val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize; 
10729  300 

301 
in 

5094  302 

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

305 
val concl = Logic.strip_imp_concl rule; 

306 
val prems = Logic.strip_imp_prems rule; 

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

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

5094  309 

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

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

313 
in 

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

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

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

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

319 
else seq check_prem (prems ~~ aprems) 

320 
else err_in_rule sg name rule bad_concl 

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

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

324 
end; 

5094  325 

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

10729  330 

331 
end; 

332 

5094  333 

6424  334 

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

10735  337 
(* elimination rules *) 
5094  338 

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

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

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

344 

345 
fun dest_intr r = 

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

347 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

349 

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

352 
fun mk_elim (c, T) = 

353 
let 

354 
val a = Free (aname, T); 

355 

356 
fun mk_elim_prem (_, t, ts) = 

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

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

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

5094  363 
end 
364 
in 

365 
map mk_elim (cs ~~ cTs) 

366 
end; 

9598  367 

6424  368 

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

371 
fun mk_indrule cs cTs params intr_ts = 

372 
let 

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

374 

375 
(* predicates for induction rule *) 

376 

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

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

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

380 

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

382 

383 
fun mk_ind_prem r = 

384 
let 

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

386 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

402 

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

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

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

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

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

409 

410 
in list_all_free (frees, 

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

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

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

416 
val ind_prems = map mk_ind_prem intr_ts; 

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

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

419 
(* make conclusions for induction rules *) 

420 

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

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

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

423 
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

424 
val Ts = prodT_factors [] ps T; 
5094  425 
val (frees, x') = foldr (fn (T', (fs, s)) => 
426 
((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

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

430 
end; 

431 

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

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

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

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

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

6424  439 

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

441 

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

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

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

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

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

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

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

448 

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

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

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

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

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

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

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

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

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

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

458 

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

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

463 
> Theory.add_path (Sign.base_name name) 

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

467 

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

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

472 

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

473 

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

474 

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

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

479 
fun prove_mono setT fp_fun monos thy = 

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

6424  486 

10735  487 
(* prove introduction rules *) 
5094  488 

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

493 
val unfold = standard (mono RS (fp_def RS 

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

496 
fun select_disj 1 1 = [] 

497 
 select_disj _ 1 = [rtac disjI1] 

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

499 

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

504 
stac unfold 1, 

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

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

507 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

5094  514 

515 
in (intrs, unfold) end; 

516 

6424  517 

10735  518 
(* prove elimination rules *) 
5094  519 

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

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

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

531 
dtac (unfold RS subst) 1, 

532 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

533 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

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

535 
> rulify 

536 
> RuleCases.name cases) 

8375  537 
end; 
5094  538 

6424  539 

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

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

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

543 

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

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

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

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

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

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

550 
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls; 
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset

551 

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

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

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

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

555 

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

556 
in 
9598  557 

558 
fun mk_cases_i elims ss cprop = 

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

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

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

565 
Some r => r 

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

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

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

573 
fun smart_mk_cases thy ss cprop = 

574 
let 

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

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

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

578 
in mk_cases_i elims ss cprop end; 

7107  579 

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

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

581 

7107  582 

583 
(* inductive_cases(_i) *) 

584 

12172  585 
fun gen_inductive_cases prep_att prep_prop (((name, raw_atts), raw_props), comment) thy = 
9598  586 
let 
587 
val ss = Simplifier.simpset_of thy; 

588 
val sign = Theory.sign_of thy; 

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

590 
val atts = map (prep_att thy) raw_atts; 

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

11740  592 
in 
593 
thy > 

594 
IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)] 

595 
end; 

5094  596 

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

7107  599 

6424  600 

9598  601 
(* mk_cases_meth *) 
602 

603 
fun mk_cases_meth (ctxt, raw_props) = 

604 
let 

605 
val thy = ProofContext.theory_of ctxt; 

606 
val ss = Simplifier.get_local_simpset ctxt; 

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

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

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

611 

612 

10735  613 
(* prove induction rule *) 
5094  614 

615 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

616 
fp_def rec_sets_defs thy = 

617 
let 

10735  618 
val _ = clean_message " Proving the induction rule ..."; 
5094  619 

6394  620 
val sign = Theory.sign_of thy; 
5094  621 

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

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

625 

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

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

627 
mk_indrule cs cTs params intr_ts; 
5094  628 

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

630 

631 
fun mk_ind_pred _ [P] = P 

632 
 mk_ind_pred T Ps = 

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

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

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

638 
end; 

639 

640 
val ind_pred = mk_ind_pred sumT preds; 

641 

642 
val ind_concl = HOLogic.mk_Trueprop 

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

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

645 

646 
(* simplification rules for vimage and Collect *) 

647 

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

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

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

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

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

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

10202  659 
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

660 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  661 
fold_goals_tac rec_sets_defs, 
662 
(*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

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

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

666 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  667 
rewrite_goals_tac sum_case_rewrites, 
5094  668 
EVERY (map (fn prem => 
5149  669 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  670 

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

674 
REPEAT (EVERY 

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

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

7293  677 
rewrite_goals_tac sum_case_rewrites, 
5094  678 
atac 1])]) 
679 

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

680 
in standard (split_rule factors (induct RS lemma)) end; 
5094  681 

6424  682 

683 

10735  684 
(** specification of (co)inductive sets **) 
5094  685 

10729  686 
fun cond_declare_consts declare_consts cs paramTs cnames = 
687 
if declare_consts then 

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

689 
else I; 

690 

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

692 
params paramTs cTs cnames = 
5094  693 
let 
694 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

695 
val setT = HOLogic.mk_setT sumT; 

696 

10735  697 
val fp_name = if coind then gfp_name else lfp_name; 
5094  698 

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

701 

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

704 
(* is transformed into *) 

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

706 

707 
fun transform_rule r = 

708 
let 

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

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

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

714 

715 
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

716 
(frees, foldr1 HOLogic.mk_conj 
5149  717 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  718 
(map (subst o HOLogic.dest_Trueprop) 
719 
(Logic.strip_imp_prems r)))) 

720 
end 

721 

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

723 

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

725 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  726 

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

728 

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

6394  730 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  731 

732 
val rec_const = list_comb 

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

734 

735 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  736 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  737 

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

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

740 

8433  741 
val (thy', [fp_def :: rec_sets_defs]) = 
742 
thy 

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

746 
> Theory.add_path rec_name 

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

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

749 
val mono = prove_mono setT fp_fun monos thy' 
5094  750 

10735  751 
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  752 

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

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

755 
let 
10735  756 
val _ = 
757 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 

758 
commas_quote cnames) else (); 

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

759 

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

760 
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

761 

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

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

765 

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

769 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  770 
if coind then standard (rule_by_tactic 
5553  771 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  772 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
773 
else 

774 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

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

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

5094  779 

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

10735  782 
val (thy3, ([intrs'', elims'], [induct'])) = 
783 
thy2 

11005  784 
> PureThy.add_thmss 
11628  785 
[(("intros", intrs'), []), 
11005  786 
(("elims", elims), [RuleCases.consumes 1])] 
10735  787 
>>> PureThy.add_thms 
12165  788 
[((coind_prefix coind ^ "induct", rulify (#1 induct)), 
789 
(RuleCases.case_names induct_cases :: #2 induct))] 

8433  790 
>> Theory.parent_path; 
9939  791 
in (thy3, 
10735  792 
{defs = fp_def :: rec_sets_defs, 
5094  793 
mono = mono, 
794 
unfold = unfold, 

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

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

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

799 
induct = induct'}) 
5094  800 
end; 
801 

6424  802 

10735  803 
(* external interfaces *) 
5094  804 

10735  805 
fun try_term f msg sign t = 
806 
(case Library.try f t of 

807 
Some x => x 

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

5094  809 

12180  810 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy = 
5094  811 
let 
6424  812 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  813 
val sign = Theory.sign_of thy; 
5094  814 

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

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

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

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

10735  823 
val full_cnames = map (try_term (fst o dest_Const o head_of) 
5094  824 
"Recursive set not previously declared as constant: " sign) cs; 
6437  825 
val cnames = map Sign.base_name full_cnames; 
5094  826 

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

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

8401  830 
val induct_cases = map (#1 o #1) intros; 
6437  831 

9405  832 
val (thy1, result as {elims, induct, ...}) = 
11628  833 
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos 
12180  834 
thy params paramTs cTs cnames induct_cases; 
8307  835 
val thy2 = thy1 
836 
> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) 

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

6437  839 
in (thy2, result) end; 
5094  840 

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

844 
val cs = map (term_of o HOLogic.read_cterm sign) c_strings; 
6424  845 

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

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

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

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

851 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  852 

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

855 
add_inductive_i verbose false "" coind false false cs' 
12180  856 
((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' 
5094  857 
end; 
858 

6424  859 

860 

6437  861 
(** package setup **) 
862 

863 
(* setup theory *) 

864 

8634  865 
val setup = 
866 
[InductiveData.init, 

9625  867 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  868 
"dynamic case analysis on sets")], 
9893  869 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  870 

871 

872 
(* outer syntax *) 

6424  873 

6723  874 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  875 

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

6424  878 

879 
fun ind_decl coind = 

6729  880 
(Scan.repeat1 P.term  P.marg_comment)  
9598  881 
(P.$$$ "intros"  
11628  882 
P.!!! (Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
12180  883 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) [] 
6424  884 
>> (Toplevel.theory o mk_ind coind); 
885 

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

888 

889 
val coinductiveP = 

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

6424  891 

7107  892 

893 
val ind_cases = 

9625  894 
P.opt_thm_name ":"  Scan.repeat1 P.prop  P.marg_comment 
7107  895 
>> (Toplevel.theory o inductive_cases); 
896 

897 
val inductive_casesP = 

9804  898 
OuterSyntax.command "inductive_cases" 
9598  899 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  900 

12180  901 
val _ = OuterSyntax.add_keywords ["intros", "monos"]; 
7107  902 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  903 

5094  904 
end; 
6424  905 

906 
end; 