author  wenzelm 
Wed, 27 Dec 2000 18:27:19 +0100  
changeset 10743  8ea821d1e3a4 
parent 10735  dfaf75f0076f 
child 10804  306aee77eadd 
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 
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 
6437  39 
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

40 
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

41 
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

42 
val get_monos: theory > thm list 
10735  43 
val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text 
44 
> theory > theory 

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

46 
> theory > theory 

6424  47 
val add_inductive_i: bool > bool > bstring > bool > bool > bool > term list > 
6521  48 
theory attribute list > ((bstring * term) * theory attribute list) list > 
49 
thm list > thm list > theory > theory * 

6424  50 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  51 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
6521  52 
val add_inductive: bool > bool > string list > Args.src list > 
53 
((bstring * string) * Args.src list) list > (xstring * Args.src list) list > 

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

6424  55 
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, 
6437  56 
intrs: thm list, mk_cases: string > thm, mono: thm, unfold: thm} 
57 
val setup: (theory > theory) list 

5094  58 
end; 
59 

6424  60 
structure InductivePackage: INDUCTIVE_PACKAGE = 
5094  61 
struct 
62 

9598  63 

10729  64 
(** theory context references **) 
65 

10735  66 
val mono_name = "Ord.mono"; 
67 
val gfp_name = "Gfp.gfp"; 

68 
val lfp_name = "Lfp.lfp"; 

69 
val vimage_name = "Inverse_Image.vimage"; 

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

71 

72 
val inductive_conj_name = "Inductive.conj"; 

10729  73 
val inductive_conj_def = thm "conj_def"; 
74 
val inductive_conj = thms "inductive_conj"; 

75 
val inductive_atomize = thms "inductive_atomize"; 

76 
val inductive_rulify1 = thms "inductive_rulify1"; 

77 
val inductive_rulify2 = thms "inductive_rulify2"; 

78 

79 

80 

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

82 

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

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

84 

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

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

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

87 
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

88 

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

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

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

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

92 
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

93 

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

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

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

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

97 
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

98 
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

99 

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

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

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

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

108 

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

109 

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

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

111 

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

112 
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

113 

9598  114 
fun the_inductive thy name = 
115 
(case get_inductive thy name of 

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

117 
 Some info => info); 

118 

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

119 
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

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

121 
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

122 
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

123 
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

124 
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

125 

8277  126 

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

127 

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

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

129 

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

8277  132 

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

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

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

135 
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

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

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

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

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

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

141 
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

142 
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

143 
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

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

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

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

147 

8634  148 

149 
(* attributes *) 

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

150 

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

153 

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

154 
val mono_attr = 
8634  155 
(Attrib.add_del_args mono_add_global mono_del_global, 
156 
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

157 

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

158 

7107  159 

10735  160 
(** misc utilities **) 
6424  161 

5662  162 
val quiet_mode = ref false; 
10735  163 
fun message s = if ! quiet_mode then () else writeln s; 
164 
fun clean_message s = if ! quick_and_dirty then () else message s; 

5662  165 

6424  166 
fun coind_prefix true = "co" 
167 
 coind_prefix false = ""; 

168 

169 

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

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

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

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

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

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

176 
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

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

178 
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

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

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

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

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

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

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

185 
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

186 
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

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

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

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

190 
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

191 
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

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

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

194 

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

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

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

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

198 

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

199 

10735  200 
(*make injections used in mutually recursive definitions*) 
5094  201 
fun mk_inj cs sumT c x = 
202 
let 

203 
fun mk_inj' T n i = 

204 
if n = 1 then x else 

205 
let val n2 = n div 2; 

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

207 
in 

208 
if i <= n2 then 

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

210 
else 

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

212 
end 

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

214 
end; 

215 

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

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

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

221 
in 

222 
Const (vimage_name, vimageT) $ 

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

224 
end; 

225 

6424  226 

227 

10729  228 
(** process rules **) 
229 

230 
local 

5094  231 

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

234 

235 
fun err_in_prem sg name t p msg = 

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

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

5094  238 

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

241 
val atomize_cterm = InductMethod.rewrite_cterm inductive_atomize; 

242 
fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews); 

243 

244 
in 

5094  245 

10729  246 
fun check_rule sg cs ((name, rule), att) = 
247 
let 

248 
val concl = Logic.strip_imp_concl rule; 

249 
val prems = Logic.strip_imp_prems rule; 

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

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

5094  252 

10729  253 
fun check_prem (prem, aprem) = 
254 
if can HOLogic.dest_Trueprop aprem then () 

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

256 
in 

257 
(case HOLogic.dest_Trueprop concl of 

258 
(Const ("op :", _) $ t $ u) => 

259 
if u mem cs then 

260 
if exists (Logic.occs o rpair t) cs then 

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

262 
else seq check_prem (prems ~~ aprems) 

263 
else err_in_rule sg name rule bad_concl 

264 
 _ => err_in_rule sg name rule bad_concl); 

265 
((name, arule), att) 

266 
end; 

5094  267 

10729  268 
val rulify = 
269 
standard o full_simplify [Drule.norm_hhf_eq] o 

270 
full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o 

271 
full_simplify inductive_conj; 

272 

273 
end; 

274 

5094  275 

6424  276 

10735  277 
(** properties of (co)inductive sets **) 
5094  278 

10735  279 
(* elimination rules *) 
5094  280 

8375  281 
fun mk_elims cs cTs params intr_ts intr_names = 
5094  282 
let 
283 
val used = foldr add_term_names (intr_ts, []); 

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

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

286 

287 
fun dest_intr r = 

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

289 
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) 

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

291 

8380  292 
val intrs = map dest_intr intr_ts ~~ intr_names; 
5094  293 

294 
fun mk_elim (c, T) = 

295 
let 

296 
val a = Free (aname, T); 

297 

298 
fun mk_elim_prem (_, t, ts) = 

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

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

8375  301 
val c_intrs = (filter (equal c o #1 o #1) intrs); 
5094  302 
in 
8375  303 
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: 
304 
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs) 

5094  305 
end 
306 
in 

307 
map mk_elim (cs ~~ cTs) 

308 
end; 

9598  309 

6424  310 

10735  311 
(* premises and conclusions of induction rules *) 
5094  312 

313 
fun mk_indrule cs cTs params intr_ts = 

314 
let 

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

316 

317 
(* predicates for induction rule *) 

318 

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

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

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

322 

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

324 

325 
fun mk_ind_prem r = 

326 
let 

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

328 

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

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

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

331 
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

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

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

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

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

337 
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

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

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

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

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

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

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

344 

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

345 
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

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

347 
 (t, _) => t :: prems); 
9598  348 

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

351 

352 
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

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

355 
HOLogic.mk_Trueprop (the (pred_of u) $ t))) 
5094  356 
end; 
357 

358 
val ind_prems = map mk_ind_prem intr_ts; 

359 

360 
(* make conclusions for induction rules *) 

361 

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

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

364 
val Ts = HOLogic.prodT_factors T; 

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

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

367 
val tuple = HOLogic.mk_tuple T frees; 

368 
in ((HOLogic.mk_binop "op >" 

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

370 
end; 

371 

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

372 
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj 
5094  373 
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) 
374 

375 
in (preds, ind_prems, mutual_ind_concl) 

376 
end; 

377 

6424  378 

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

380 

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

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

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

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

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

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

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

387 

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

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

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

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

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

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

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

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

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

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

397 

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

399 
let 
9405  400 
fun cases_spec (name, elim) thy = 
401 
thy 

402 
> Theory.add_path (Sign.base_name name) 

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

406 

9405  407 
fun induct_spec (name, th) = (#1 o PureThy.add_thms 
10279  408 
[(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]); 
8401  409 
val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct); 
9405  410 
in Library.apply (cases_specs @ induct_specs) end; 
8316
74639e19eca0
add_cases_induct: project_rules accomodates mutual induction;
wenzelm
parents:
8312
diff
changeset

411 

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

412 

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

413 

10735  414 
(** proofs for (co)inductive sets **) 
6424  415 

10735  416 
(* prove monotonicity  NOT subject to quick_and_dirty! *) 
5094  417 

418 
fun prove_mono setT fp_fun monos thy = 

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

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

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

6424  425 

10735  426 
(* prove introduction rules *) 
5094  427 

428 
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = 

429 
let 

10735  430 
val _ = clean_message " Proving the introduction rules ..."; 
5094  431 

432 
val unfold = standard (mono RS (fp_def RS 

10186  433 
(if coind then def_gfp_unfold else def_lfp_unfold))); 
5094  434 

435 
fun select_disj 1 1 = [] 

436 
 select_disj _ 1 = [rtac disjI1] 

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

438 

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

5094  441 
[(*insert prems and underlying sets*) 
442 
cut_facts_tac prems 1, 

443 
stac unfold 1, 

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

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

446 
EVERY1 (select_disj (length intr_ts) i), 

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

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

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

10729  452 
REPEAT (rtac refl 1)]) 
453 
> rulify) (1 upto (length intr_ts) ~~ intr_ts) 

5094  454 

455 
in (intrs, unfold) end; 

456 

6424  457 

10735  458 
(* prove elimination rules *) 
5094  459 

8375  460 
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy = 
5094  461 
let 
10735  462 
val _ = clean_message " Proving the elimination rules ..."; 
5094  463 

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

464 
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; 
10735  465 
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject]; 
8375  466 
in 
10735  467 
map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs 
468 
(Thm.cterm_of (Theory.sign_of thy) t) (fn prems => 

5094  469 
[cut_facts_tac [hd prems] 1, 
470 
dtac (unfold RS subst) 1, 

471 
REPEAT (FIRSTGOAL (eresolve_tac rules1)), 

472 
REPEAT (FIRSTGOAL (eresolve_tac rules2)), 

10735  473 
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]) 
10729  474 
> rulify 
8375  475 
> RuleCases.name cases) 
476 
(mk_elims cs cTs params intr_ts intr_names) 

477 
end; 

5094  478 

6424  479 

10735  480 
(* derivation of simplified elimination rules *) 
5094  481 

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

9598  483 
the given defs. Cannot simply use the local con_defs because con_defs=[] 
10735  484 
for inference systems. (??) *) 
5094  485 

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

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

490 
fun mk_cases_i elims ss cprop = 

7107  491 
let 
492 
val prem = Thm.assume cprop; 

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

497 
Some r => r 

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

9598  499 
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop]))) 
7107  500 
end; 
501 

6141  502 
fun mk_cases elims s = 
9598  503 
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); 
504 

505 
fun smart_mk_cases thy ss cprop = 

506 
let 

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

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

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

510 
in mk_cases_i elims ss cprop end; 

7107  511 

512 

513 
(* inductive_cases(_i) *) 

514 

515 
fun gen_inductive_cases prep_att prep_const prep_prop 

9598  516 
(((name, raw_atts), raw_props), comment) thy = 
517 
let 

518 
val ss = Simplifier.simpset_of thy; 

519 
val sign = Theory.sign_of thy; 

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

521 
val atts = map (prep_att thy) raw_atts; 

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

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

5094  524 

7107  525 
val inductive_cases = 
526 
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; 

527 

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

529 

6424  530 

9598  531 
(* mk_cases_meth *) 
532 

533 
fun mk_cases_meth (ctxt, raw_props) = 

534 
let 

535 
val thy = ProofContext.theory_of ctxt; 

536 
val ss = Simplifier.get_local_simpset ctxt; 

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

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

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

541 

542 

10735  543 
(* prove induction rule *) 
5094  544 

545 
fun prove_indrule cs cTs sumT rec_const params intr_ts mono 

546 
fp_def rec_sets_defs thy = 

547 
let 

10735  548 
val _ = clean_message " Proving the induction rule ..."; 
5094  549 

6394  550 
val sign = Theory.sign_of thy; 
5094  551 

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

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

555 

5094  556 
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; 
557 

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

559 

560 
fun mk_ind_pred _ [P] = P 

561 
 mk_ind_pred T Ps = 

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

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

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

567 
end; 

568 

569 
val ind_pred = mk_ind_pred sumT preds; 

570 

571 
val ind_concl = HOLogic.mk_Trueprop 

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

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

574 

575 
(* simplification rules for vimage and Collect *) 

576 

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

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

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

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

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

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

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

589 
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), 
5094  590 
fold_goals_tac rec_sets_defs, 
591 
(*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

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

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

595 
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), 
7293  596 
rewrite_goals_tac sum_case_rewrites, 
5094  597 
EVERY (map (fn prem => 
5149  598 
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); 
5094  599 

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

603 
REPEAT (EVERY 

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

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

7293  606 
rewrite_goals_tac sum_case_rewrites, 
5094  607 
atac 1])]) 
608 

10729  609 
in standard (split_rule (induct RS lemma)) end; 
5094  610 

6424  611 

612 

10735  613 
(** specification of (co)inductive sets **) 
5094  614 

10729  615 
fun cond_declare_consts declare_consts cs paramTs cnames = 
616 
if declare_consts then 

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

618 
else I; 

619 

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

620 
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

621 
params paramTs cTs cnames = 
5094  622 
let 
623 
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; 

624 
val setT = HOLogic.mk_setT sumT; 

625 

10735  626 
val fp_name = if coind then gfp_name else lfp_name; 
5094  627 

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

630 

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

633 
(* is transformed into *) 

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

635 

636 
fun transform_rule r = 

637 
let 

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

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

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

643 

644 
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

645 
(frees, foldr1 HOLogic.mk_conj 
5149  646 
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: 
5094  647 
(map (subst o HOLogic.dest_Trueprop) 
648 
(Logic.strip_imp_prems r)))) 

649 
end 

650 

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

652 

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

654 
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); 
5094  655 

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

657 

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

6394  659 
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; 
5094  660 

661 
val rec_const = list_comb 

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

663 

664 
val fp_def_term = Logic.mk_equals (rec_const, 

10735  665 
Const (fp_name, (setT > setT) > setT) $ fp_fun); 
5094  666 

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

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

669 

8433  670 
val (thy', [fp_def :: rec_sets_defs]) = 
671 
thy 

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

675 
> Theory.add_path rec_name 

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

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

678 
val mono = prove_mono setT fp_fun monos thy' 
5094  679 

10735  680 
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; 
5094  681 

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

682 
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

683 
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

684 
let 
10735  685 
val _ = 
686 
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ 

687 
commas_quote cnames) else (); 

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

688 

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

689 
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

690 

9939  691 
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

692 
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

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

694 

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

699 
val raw_induct = if no_ind then Drule.asm_rl else 
5094  700 
if coind then standard (rule_by_tactic 
5553  701 
(rewrite_tac [mk_meta_eq vimage_Un] THEN 
5094  702 
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) 
703 
else 

704 
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def 

9939  705 
rec_sets_defs thy1; 
5108  706 
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct 
5094  707 
else standard (raw_induct RSN (2, rev_mp)); 
708 

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

10735  711 
val (thy3, ([intrs'', elims'], [induct'])) = 
712 
thy2 

713 
> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])] 

714 
>>> PureThy.add_thms 

715 
[((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])] 

8433  716 
>> Theory.parent_path; 
9939  717 
in (thy3, 
10735  718 
{defs = fp_def :: rec_sets_defs, 
5094  719 
mono = mono, 
720 
unfold = unfold, 

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

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

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

725 
induct = induct'}) 
5094  726 
end; 
727 

6424  728 

10735  729 
(* external interfaces *) 
5094  730 

10735  731 
fun try_term f msg sign t = 
732 
(case Library.try f t of 

733 
Some x => x 

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

5094  735 

736 
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs 

10729  737 
atts pre_intros monos con_defs thy = 
5094  738 
let 
6424  739 
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); 
6394  740 
val sign = Theory.sign_of thy; 
5094  741 

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

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

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

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

10735  750 
val full_cnames = map (try_term (fst o dest_Const o head_of) 
5094  751 
"Recursive set not previously declared as constant: " sign) cs; 
6437  752 
val cnames = map Sign.base_name full_cnames; 
5094  753 

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

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

8401  757 
val induct_cases = map (#1 o #1) intros; 
6437  758 

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

9405  764 
> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases; 
6437  765 
in (thy2, result) end; 
5094  766 

6521  767 
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = 
5094  768 
let 
6394  769 
val sign = Theory.sign_of thy; 
8100  770 
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; 
6424  771 

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

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

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

778 
val (cs', intr_ts') = unify_consts sign cs intr_ts; 
5094  779 

6424  780 
val ((thy', con_defs), monos) = thy 
781 
> IsarThy.apply_theorems raw_monos 

782 
> apfst (IsarThy.apply_theorems raw_con_defs); 

783 
in 

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

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

785 
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' 
5094  786 
end; 
787 

6424  788 

789 

6437  790 
(** package setup **) 
791 

792 
(* setup theory *) 

793 

8634  794 
val setup = 
795 
[InductiveData.init, 

9625  796 
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args, 
9598  797 
"dynamic case analysis on sets")], 
9893  798 
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]]; 
6437  799 

800 

801 
(* outer syntax *) 

6424  802 

6723  803 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6424  804 

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

808 
fun ind_decl coind = 

6729  809 
(Scan.repeat1 P.term  P.marg_comment)  
9598  810 
(P.$$$ "intros"  
7152  811 
P.!!! (P.opt_attribs  Scan.repeat1 (P.opt_thm_name ":"  P.prop  P.marg_comment)))  
6729  812 
Scan.optional (P.$$$ "monos"  P.!!! P.xthms1  P.marg_comment) []  
813 
Scan.optional (P.$$$ "con_defs"  P.!!! P.xthms1  P.marg_comment) [] 

6424  814 
>> (Toplevel.theory o mk_ind coind); 
815 

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

818 

819 
val coinductiveP = 

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

6424  821 

7107  822 

823 
val ind_cases = 

9625  824 
P.opt_thm_name ":"  Scan.repeat1 P.prop  P.marg_comment 
7107  825 
>> (Toplevel.theory o inductive_cases); 
826 

827 
val inductive_casesP = 

9804  828 
OuterSyntax.command "inductive_cases" 
9598  829 
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases; 
7107  830 

9643  831 
val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"]; 
7107  832 
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; 
6424  833 

5094  834 
end; 
6424  835 

836 
end; 