berghofe@5094
|
1 |
(* Title: HOL/Tools/inductive_package.ML
|
berghofe@5094
|
2 |
ID: $Id$
|
berghofe@5094
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
wenzelm@10735
|
4 |
Author: Stefan Berghofer, TU Muenchen
|
wenzelm@10735
|
5 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@11834
|
6 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
berghofe@5094
|
7 |
|
wenzelm@6424
|
8 |
(Co)Inductive Definition module for HOL.
|
berghofe@5094
|
9 |
|
berghofe@5094
|
10 |
Features:
|
wenzelm@6424
|
11 |
* least or greatest fixedpoints
|
wenzelm@6424
|
12 |
* user-specified product and sum constructions
|
wenzelm@6424
|
13 |
* mutually recursive definitions
|
wenzelm@6424
|
14 |
* definitions involving arbitrary monotone operators
|
wenzelm@6424
|
15 |
* automatically proves introduction and elimination rules
|
berghofe@5094
|
16 |
|
wenzelm@6424
|
17 |
The recursive sets must *already* be declared as constants in the
|
wenzelm@6424
|
18 |
current theory!
|
berghofe@5094
|
19 |
|
berghofe@5094
|
20 |
Introduction rules have the form
|
wenzelm@8316
|
21 |
[| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
|
berghofe@5094
|
22 |
where M is some monotone operator (usually the identity)
|
berghofe@5094
|
23 |
P(x) is any side condition on the free variables
|
berghofe@5094
|
24 |
ti, t are any terms
|
berghofe@5094
|
25 |
Sj, Sk are two of the sets being defined in mutual recursion
|
berghofe@5094
|
26 |
|
wenzelm@6424
|
27 |
Sums are used only for mutual recursion. Products are used only to
|
wenzelm@6424
|
28 |
derive "streamlined" induction rules for relations.
|
berghofe@5094
|
29 |
*)
|
berghofe@5094
|
30 |
|
berghofe@5094
|
31 |
signature INDUCTIVE_PACKAGE =
|
berghofe@5094
|
32 |
sig
|
wenzelm@6424
|
33 |
val quiet_mode: bool ref
|
berghofe@7020
|
34 |
val unify_consts: Sign.sg -> term list -> term list -> term list * term list
|
berghofe@10988
|
35 |
val split_rule_vars: term list -> thm -> thm
|
berghofe@9116
|
36 |
val get_inductive: theory -> string -> ({names: string list, coind: bool} *
|
berghofe@9116
|
37 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
|
berghofe@9116
|
38 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
|
wenzelm@12400
|
39 |
val the_mk_cases: theory -> string -> string -> thm
|
wenzelm@6437
|
40 |
val print_inductives: theory -> unit
|
berghofe@7710
|
41 |
val mono_add_global: theory attribute
|
berghofe@7710
|
42 |
val mono_del_global: theory attribute
|
berghofe@7710
|
43 |
val get_monos: theory -> thm list
|
wenzelm@10910
|
44 |
val inductive_forall_name: string
|
wenzelm@10910
|
45 |
val inductive_forall_def: thm
|
wenzelm@10910
|
46 |
val rulify: thm -> thm
|
wenzelm@12876
|
47 |
val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory
|
wenzelm@12876
|
48 |
val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
|
wenzelm@6424
|
49 |
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
|
wenzelm@12180
|
50 |
((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
|
wenzelm@6424
|
51 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
|
wenzelm@6437
|
52 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
|
wenzelm@11628
|
53 |
val add_inductive: bool -> bool -> string list ->
|
wenzelm@6521
|
54 |
((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
|
wenzelm@12180
|
55 |
theory -> theory *
|
wenzelm@6424
|
56 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
|
wenzelm@6437
|
57 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
|
wenzelm@6437
|
58 |
val setup: (theory -> theory) list
|
berghofe@5094
|
59 |
end;
|
berghofe@5094
|
60 |
|
wenzelm@6424
|
61 |
structure InductivePackage: INDUCTIVE_PACKAGE =
|
berghofe@5094
|
62 |
struct
|
berghofe@5094
|
63 |
|
wenzelm@9598
|
64 |
|
wenzelm@10729
|
65 |
(** theory context references **)
|
wenzelm@10729
|
66 |
|
wenzelm@11755
|
67 |
val mono_name = "HOL.mono";
|
wenzelm@10735
|
68 |
val gfp_name = "Gfp.gfp";
|
wenzelm@10735
|
69 |
val lfp_name = "Lfp.lfp";
|
wenzelm@12259
|
70 |
val vimage_name = "Set.vimage";
|
wenzelm@10735
|
71 |
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
|
wenzelm@10735
|
72 |
|
wenzelm@11991
|
73 |
val inductive_forall_name = "HOL.induct_forall";
|
wenzelm@11991
|
74 |
val inductive_forall_def = thm "induct_forall_def";
|
wenzelm@11991
|
75 |
val inductive_conj_name = "HOL.induct_conj";
|
wenzelm@11991
|
76 |
val inductive_conj_def = thm "induct_conj_def";
|
wenzelm@11991
|
77 |
val inductive_conj = thms "induct_conj";
|
wenzelm@11991
|
78 |
val inductive_atomize = thms "induct_atomize";
|
wenzelm@11991
|
79 |
val inductive_rulify1 = thms "induct_rulify1";
|
wenzelm@11991
|
80 |
val inductive_rulify2 = thms "induct_rulify2";
|
wenzelm@10729
|
81 |
|
wenzelm@10729
|
82 |
|
wenzelm@10729
|
83 |
|
wenzelm@10735
|
84 |
(** theory data **)
|
berghofe@7710
|
85 |
|
berghofe@7710
|
86 |
(* data kind 'HOL/inductive' *)
|
berghofe@7710
|
87 |
|
berghofe@7710
|
88 |
type inductive_info =
|
berghofe@7710
|
89 |
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
|
berghofe@7710
|
90 |
induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
|
berghofe@7710
|
91 |
|
berghofe@7710
|
92 |
structure InductiveArgs =
|
berghofe@7710
|
93 |
struct
|
berghofe@7710
|
94 |
val name = "HOL/inductive";
|
berghofe@7710
|
95 |
type T = inductive_info Symtab.table * thm list;
|
berghofe@7710
|
96 |
|
berghofe@7710
|
97 |
val empty = (Symtab.empty, []);
|
berghofe@7710
|
98 |
val copy = I;
|
berghofe@7710
|
99 |
val prep_ext = I;
|
wenzelm@11502
|
100 |
fun merge ((tab1, monos1), (tab2, monos2)) =
|
wenzelm@11502
|
101 |
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
|
berghofe@7710
|
102 |
|
berghofe@7710
|
103 |
fun print sg (tab, monos) =
|
wenzelm@8720
|
104 |
[Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
|
wenzelm@10008
|
105 |
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
|
wenzelm@8720
|
106 |
|> Pretty.chunks |> Pretty.writeln;
|
berghofe@7710
|
107 |
end;
|
berghofe@7710
|
108 |
|
berghofe@7710
|
109 |
structure InductiveData = TheoryDataFun(InductiveArgs);
|
berghofe@7710
|
110 |
val print_inductives = InductiveData.print;
|
berghofe@7710
|
111 |
|
berghofe@7710
|
112 |
|
berghofe@7710
|
113 |
(* get and put data *)
|
berghofe@7710
|
114 |
|
berghofe@9116
|
115 |
fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
|
berghofe@7710
|
116 |
|
wenzelm@9598
|
117 |
fun the_inductive thy name =
|
wenzelm@9598
|
118 |
(case get_inductive thy name of
|
wenzelm@9598
|
119 |
None => error ("Unknown (co)inductive set " ^ quote name)
|
wenzelm@9598
|
120 |
| Some info => info);
|
wenzelm@9598
|
121 |
|
wenzelm@12400
|
122 |
val the_mk_cases = (#mk_cases o #2) oo the_inductive;
|
wenzelm@12400
|
123 |
|
berghofe@7710
|
124 |
fun put_inductives names info thy =
|
berghofe@7710
|
125 |
let
|
berghofe@7710
|
126 |
fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
|
berghofe@7710
|
127 |
val tab_monos = foldl upd (InductiveData.get thy, names)
|
berghofe@7710
|
128 |
handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
|
berghofe@7710
|
129 |
in InductiveData.put tab_monos thy end;
|
berghofe@7710
|
130 |
|
berghofe@7710
|
131 |
|
berghofe@7710
|
132 |
|
berghofe@7710
|
133 |
(** monotonicity rules **)
|
berghofe@7710
|
134 |
|
wenzelm@9831
|
135 |
val get_monos = #2 o InductiveData.get;
|
wenzelm@9831
|
136 |
fun map_monos f = InductiveData.map (Library.apsnd f);
|
wenzelm@8277
|
137 |
|
berghofe@7710
|
138 |
fun mk_mono thm =
|
berghofe@7710
|
139 |
let
|
berghofe@7710
|
140 |
fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
|
berghofe@7710
|
141 |
(case concl_of thm of
|
berghofe@7710
|
142 |
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
|
berghofe@7710
|
143 |
| _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
|
berghofe@7710
|
144 |
val concl = concl_of thm
|
berghofe@7710
|
145 |
in
|
berghofe@7710
|
146 |
if Logic.is_equals concl then
|
berghofe@7710
|
147 |
eq2mono (thm RS meta_eq_to_obj_eq)
|
berghofe@7710
|
148 |
else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
|
berghofe@7710
|
149 |
eq2mono thm
|
berghofe@7710
|
150 |
else [thm]
|
berghofe@7710
|
151 |
end;
|
berghofe@7710
|
152 |
|
wenzelm@8634
|
153 |
|
wenzelm@8634
|
154 |
(* attributes *)
|
berghofe@7710
|
155 |
|
wenzelm@9831
|
156 |
fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
|
wenzelm@9831
|
157 |
fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
|
berghofe@7710
|
158 |
|
berghofe@7710
|
159 |
val mono_attr =
|
wenzelm@8634
|
160 |
(Attrib.add_del_args mono_add_global mono_del_global,
|
wenzelm@8634
|
161 |
Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
|
berghofe@7710
|
162 |
|
berghofe@7710
|
163 |
|
wenzelm@7107
|
164 |
|
wenzelm@10735
|
165 |
(** misc utilities **)
|
wenzelm@6424
|
166 |
|
berghofe@5662
|
167 |
val quiet_mode = ref false;
|
wenzelm@10735
|
168 |
fun message s = if ! quiet_mode then () else writeln s;
|
wenzelm@10735
|
169 |
fun clean_message s = if ! quick_and_dirty then () else message s;
|
berghofe@5662
|
170 |
|
wenzelm@6424
|
171 |
fun coind_prefix true = "co"
|
wenzelm@6424
|
172 |
| coind_prefix false = "";
|
wenzelm@6424
|
173 |
|
wenzelm@6424
|
174 |
|
wenzelm@10735
|
175 |
(*the following code ensures that each recursive set always has the
|
wenzelm@10735
|
176 |
same type in all introduction rules*)
|
berghofe@7020
|
177 |
fun unify_consts sign cs intr_ts =
|
berghofe@7020
|
178 |
(let
|
berghofe@7020
|
179 |
val {tsig, ...} = Sign.rep_sg sign;
|
berghofe@7020
|
180 |
val add_term_consts_2 =
|
berghofe@7020
|
181 |
foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
|
berghofe@7020
|
182 |
fun varify (t, (i, ts)) =
|
wenzelm@12494
|
183 |
let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
|
berghofe@7020
|
184 |
in (maxidx_of_term t', t'::ts) end;
|
berghofe@7020
|
185 |
val (i, cs') = foldr varify (cs, (~1, []));
|
berghofe@7020
|
186 |
val (i', intr_ts') = foldr varify (intr_ts, (i, []));
|
berghofe@7020
|
187 |
val rec_consts = foldl add_term_consts_2 ([], cs');
|
berghofe@7020
|
188 |
val intr_consts = foldl add_term_consts_2 ([], intr_ts');
|
berghofe@7020
|
189 |
fun unify (env, (cname, cT)) =
|
berghofe@7020
|
190 |
let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
|
wenzelm@12527
|
191 |
in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
|
berghofe@7020
|
192 |
(env, (replicate (length consts) cT) ~~ consts)
|
berghofe@7020
|
193 |
end;
|
berghofe@8410
|
194 |
val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
|
berghofe@8410
|
195 |
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
|
berghofe@7020
|
196 |
in if T = T' then T else typ_subst_TVars_2 env T' end;
|
berghofe@7020
|
197 |
val subst = fst o Type.freeze_thaw o
|
berghofe@7020
|
198 |
(map_term_types (typ_subst_TVars_2 env))
|
berghofe@7020
|
199 |
|
berghofe@7020
|
200 |
in (map subst cs', map subst intr_ts')
|
berghofe@7020
|
201 |
end) handle Type.TUNIFY =>
|
berghofe@7020
|
202 |
(warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
|
berghofe@7020
|
203 |
|
berghofe@7020
|
204 |
|
wenzelm@10735
|
205 |
(*make injections used in mutually recursive definitions*)
|
berghofe@5094
|
206 |
fun mk_inj cs sumT c x =
|
berghofe@5094
|
207 |
let
|
berghofe@5094
|
208 |
fun mk_inj' T n i =
|
berghofe@5094
|
209 |
if n = 1 then x else
|
berghofe@5094
|
210 |
let val n2 = n div 2;
|
berghofe@5094
|
211 |
val Type (_, [T1, T2]) = T
|
berghofe@5094
|
212 |
in
|
berghofe@5094
|
213 |
if i <= n2 then
|
berghofe@5094
|
214 |
Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
|
berghofe@5094
|
215 |
else
|
berghofe@5094
|
216 |
Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
|
berghofe@5094
|
217 |
end
|
berghofe@5094
|
218 |
in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
|
berghofe@5094
|
219 |
end;
|
berghofe@5094
|
220 |
|
wenzelm@10735
|
221 |
(*make "vimage" terms for selecting out components of mutually rec.def*)
|
berghofe@5094
|
222 |
fun mk_vimage cs sumT t c = if length cs < 2 then t else
|
berghofe@5094
|
223 |
let
|
berghofe@5094
|
224 |
val cT = HOLogic.dest_setT (fastype_of c);
|
berghofe@5094
|
225 |
val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
|
berghofe@5094
|
226 |
in
|
berghofe@5094
|
227 |
Const (vimage_name, vimageT) $
|
berghofe@5094
|
228 |
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
|
berghofe@5094
|
229 |
end;
|
berghofe@5094
|
230 |
|
berghofe@10988
|
231 |
(** proper splitting **)
|
berghofe@10988
|
232 |
|
berghofe@10988
|
233 |
fun prod_factors p (Const ("Pair", _) $ t $ u) =
|
berghofe@10988
|
234 |
p :: prod_factors (1::p) t @ prod_factors (2::p) u
|
berghofe@10988
|
235 |
| prod_factors p _ = [];
|
berghofe@10988
|
236 |
|
berghofe@10988
|
237 |
fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
|
berghofe@10988
|
238 |
let val f = prod_factors [] u
|
berghofe@10988
|
239 |
in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
|
berghofe@10988
|
240 |
else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
|
berghofe@10988
|
241 |
| mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
|
berghofe@10988
|
242 |
| mg_prod_factors ts (fs, _) = fs;
|
berghofe@10988
|
243 |
|
berghofe@10988
|
244 |
fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
|
berghofe@10988
|
245 |
if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
|
berghofe@10988
|
246 |
else [T]
|
berghofe@10988
|
247 |
| prodT_factors _ _ T = [T];
|
berghofe@10988
|
248 |
|
berghofe@10988
|
249 |
fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
|
berghofe@10988
|
250 |
if p mem ps then HOLogic.split_const (T1, T2, T3) $
|
berghofe@10988
|
251 |
Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
|
berghofe@10988
|
252 |
(prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
|
berghofe@10988
|
253 |
else u
|
berghofe@10988
|
254 |
| ap_split _ _ _ _ u = u;
|
berghofe@10988
|
255 |
|
berghofe@10988
|
256 |
fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
|
berghofe@10988
|
257 |
if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
|
berghofe@10988
|
258 |
mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
|
berghofe@10988
|
259 |
else t
|
berghofe@10988
|
260 |
| mk_tuple _ _ _ (t::_) = t;
|
berghofe@10988
|
261 |
|
berghofe@10988
|
262 |
fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
|
berghofe@10988
|
263 |
let val T' = prodT_factors [] ps T1 ---> T2
|
berghofe@10988
|
264 |
val newt = ap_split [] ps T1 T2 (Var (v, T'))
|
berghofe@10988
|
265 |
val cterm = Thm.cterm_of (#sign (rep_thm rl))
|
berghofe@10988
|
266 |
in
|
berghofe@10988
|
267 |
instantiate ([], [(cterm t, cterm newt)]) rl
|
berghofe@10988
|
268 |
end
|
berghofe@10988
|
269 |
| split_rule_var' (_, rl) = rl;
|
berghofe@10988
|
270 |
|
berghofe@10988
|
271 |
val remove_split = rewrite_rule [split_conv RS eq_reflection];
|
berghofe@10988
|
272 |
|
berghofe@10988
|
273 |
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
|
berghofe@10988
|
274 |
(mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
|
berghofe@10988
|
275 |
|
berghofe@10988
|
276 |
fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
|
berghofe@10988
|
277 |
(mapfilter (fn (t as Var ((a, _), _)) =>
|
berghofe@10988
|
278 |
apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
|
wenzelm@6424
|
279 |
|
wenzelm@6424
|
280 |
|
wenzelm@10729
|
281 |
(** process rules **)
|
berghofe@5094
|
282 |
|
wenzelm@10729
|
283 |
local
|
berghofe@5094
|
284 |
|
wenzelm@10729
|
285 |
fun err_in_rule sg name t msg =
|
wenzelm@10729
|
286 |
error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
|
berghofe@5094
|
287 |
|
wenzelm@10729
|
288 |
fun err_in_prem sg name t p msg =
|
wenzelm@10729
|
289 |
error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
|
wenzelm@10729
|
290 |
"in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
|
berghofe@5094
|
291 |
|
wenzelm@10729
|
292 |
val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
|
wenzelm@10729
|
293 |
|
paulson@11358
|
294 |
val all_not_allowed =
|
paulson@11358
|
295 |
"Introduction rule must not have a leading \"!!\" quantifier";
|
paulson@11358
|
296 |
|
wenzelm@12798
|
297 |
fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
|
wenzelm@10729
|
298 |
|
wenzelm@10729
|
299 |
in
|
wenzelm@10729
|
300 |
|
wenzelm@10729
|
301 |
fun check_rule sg cs ((name, rule), att) =
|
berghofe@5094
|
302 |
let
|
wenzelm@10729
|
303 |
val concl = Logic.strip_imp_concl rule;
|
wenzelm@10729
|
304 |
val prems = Logic.strip_imp_prems rule;
|
wenzelm@12798
|
305 |
val aprems = map (atomize_term sg) prems;
|
wenzelm@10729
|
306 |
val arule = Logic.list_implies (aprems, concl);
|
berghofe@5094
|
307 |
|
wenzelm@10729
|
308 |
fun check_prem (prem, aprem) =
|
wenzelm@10729
|
309 |
if can HOLogic.dest_Trueprop aprem then ()
|
wenzelm@10729
|
310 |
else err_in_prem sg name rule prem "Non-atomic premise";
|
wenzelm@10729
|
311 |
in
|
paulson@11358
|
312 |
(case concl of
|
paulson@11358
|
313 |
Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
|
wenzelm@10729
|
314 |
if u mem cs then
|
wenzelm@10729
|
315 |
if exists (Logic.occs o rpair t) cs then
|
wenzelm@10729
|
316 |
err_in_rule sg name rule "Recursion term on left of member symbol"
|
wenzelm@10729
|
317 |
else seq check_prem (prems ~~ aprems)
|
wenzelm@10729
|
318 |
else err_in_rule sg name rule bad_concl
|
paulson@11358
|
319 |
| Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
|
wenzelm@10729
|
320 |
| _ => err_in_rule sg name rule bad_concl);
|
wenzelm@10729
|
321 |
((name, arule), att)
|
berghofe@5094
|
322 |
end;
|
berghofe@5094
|
323 |
|
wenzelm@10729
|
324 |
val rulify =
|
wenzelm@12798
|
325 |
standard o Tactic.norm_hhf_rule o
|
wenzelm@11036
|
326 |
hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
|
wenzelm@11036
|
327 |
hol_simplify inductive_conj;
|
wenzelm@10729
|
328 |
|
wenzelm@10729
|
329 |
end;
|
wenzelm@10729
|
330 |
|
wenzelm@10729
|
331 |
|
berghofe@5094
|
332 |
|
wenzelm@10735
|
333 |
(** properties of (co)inductive sets **)
|
berghofe@5094
|
334 |
|
wenzelm@10735
|
335 |
(* elimination rules *)
|
berghofe@5094
|
336 |
|
wenzelm@8375
|
337 |
fun mk_elims cs cTs params intr_ts intr_names =
|
berghofe@5094
|
338 |
let
|
berghofe@5094
|
339 |
val used = foldr add_term_names (intr_ts, []);
|
berghofe@5094
|
340 |
val [aname, pname] = variantlist (["a", "P"], used);
|
berghofe@5094
|
341 |
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
|
berghofe@5094
|
342 |
|
berghofe@5094
|
343 |
fun dest_intr r =
|
berghofe@5094
|
344 |
let val Const ("op :", _) $ t $ u =
|
berghofe@5094
|
345 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
|
berghofe@5094
|
346 |
in (u, t, Logic.strip_imp_prems r) end;
|
berghofe@5094
|
347 |
|
wenzelm@8380
|
348 |
val intrs = map dest_intr intr_ts ~~ intr_names;
|
berghofe@5094
|
349 |
|
berghofe@5094
|
350 |
fun mk_elim (c, T) =
|
berghofe@5094
|
351 |
let
|
berghofe@5094
|
352 |
val a = Free (aname, T);
|
berghofe@5094
|
353 |
|
berghofe@5094
|
354 |
fun mk_elim_prem (_, t, ts) =
|
berghofe@5094
|
355 |
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
|
berghofe@5094
|
356 |
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
|
wenzelm@8375
|
357 |
val c_intrs = (filter (equal c o #1 o #1) intrs);
|
berghofe@5094
|
358 |
in
|
wenzelm@8375
|
359 |
(Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
|
wenzelm@8375
|
360 |
map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
|
berghofe@5094
|
361 |
end
|
berghofe@5094
|
362 |
in
|
berghofe@5094
|
363 |
map mk_elim (cs ~~ cTs)
|
berghofe@5094
|
364 |
end;
|
wenzelm@9598
|
365 |
|
wenzelm@6424
|
366 |
|
wenzelm@10735
|
367 |
(* premises and conclusions of induction rules *)
|
berghofe@5094
|
368 |
|
berghofe@5094
|
369 |
fun mk_indrule cs cTs params intr_ts =
|
berghofe@5094
|
370 |
let
|
berghofe@5094
|
371 |
val used = foldr add_term_names (intr_ts, []);
|
berghofe@5094
|
372 |
|
berghofe@5094
|
373 |
(* predicates for induction rule *)
|
berghofe@5094
|
374 |
|
berghofe@5094
|
375 |
val preds = map Free (variantlist (if length cs < 2 then ["P"] else
|
berghofe@5094
|
376 |
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
|
berghofe@5094
|
377 |
map (fn T => T --> HOLogic.boolT) cTs);
|
berghofe@5094
|
378 |
|
berghofe@5094
|
379 |
(* transform an introduction rule into a premise for induction rule *)
|
berghofe@5094
|
380 |
|
berghofe@5094
|
381 |
fun mk_ind_prem r =
|
berghofe@5094
|
382 |
let
|
berghofe@5094
|
383 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
|
berghofe@5094
|
384 |
|
berghofe@7710
|
385 |
val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
|
berghofe@5094
|
386 |
|
berghofe@7710
|
387 |
fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
|
berghofe@7710
|
388 |
(case pred_of u of
|
berghofe@7710
|
389 |
None => (m $ fst (subst t) $ fst (subst u), None)
|
wenzelm@10735
|
390 |
| Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
|
berghofe@7710
|
391 |
| subst s =
|
berghofe@7710
|
392 |
(case pred_of s of
|
berghofe@7710
|
393 |
Some P => (HOLogic.mk_binop "op Int"
|
berghofe@7710
|
394 |
(s, HOLogic.Collect_const (HOLogic.dest_setT
|
berghofe@7710
|
395 |
(fastype_of s)) $ P), None)
|
berghofe@7710
|
396 |
| None => (case s of
|
berghofe@7710
|
397 |
(t $ u) => (fst (subst t) $ fst (subst u), None)
|
berghofe@7710
|
398 |
| (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
|
berghofe@7710
|
399 |
| _ => (s, None)));
|
berghofe@7710
|
400 |
|
berghofe@7710
|
401 |
fun mk_prem (s, prems) = (case subst s of
|
berghofe@7710
|
402 |
(_, Some (t, u)) => t :: u :: prems
|
berghofe@7710
|
403 |
| (t, _) => t :: prems);
|
wenzelm@9598
|
404 |
|
berghofe@5094
|
405 |
val Const ("op :", _) $ t $ u =
|
berghofe@5094
|
406 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
|
berghofe@5094
|
407 |
|
berghofe@5094
|
408 |
in list_all_free (frees,
|
berghofe@7710
|
409 |
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
|
berghofe@5094
|
410 |
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
|
berghofe@7710
|
411 |
HOLogic.mk_Trueprop (the (pred_of u) $ t)))
|
berghofe@5094
|
412 |
end;
|
berghofe@5094
|
413 |
|
berghofe@5094
|
414 |
val ind_prems = map mk_ind_prem intr_ts;
|
berghofe@10988
|
415 |
val factors = foldl (mg_prod_factors preds) ([], ind_prems);
|
berghofe@5094
|
416 |
|
berghofe@5094
|
417 |
(* make conclusions for induction rules *)
|
berghofe@5094
|
418 |
|
berghofe@5094
|
419 |
fun mk_ind_concl ((c, P), (ts, x)) =
|
berghofe@5094
|
420 |
let val T = HOLogic.dest_setT (fastype_of c);
|
berghofe@10988
|
421 |
val ps = if_none (assoc (factors, P)) [];
|
berghofe@10988
|
422 |
val Ts = prodT_factors [] ps T;
|
berghofe@5094
|
423 |
val (frees, x') = foldr (fn (T', (fs, s)) =>
|
wenzelm@12902
|
424 |
((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
|
berghofe@10988
|
425 |
val tuple = mk_tuple [] ps T frees;
|
berghofe@5094
|
426 |
in ((HOLogic.mk_binop "op -->"
|
berghofe@5094
|
427 |
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
|
berghofe@5094
|
428 |
end;
|
berghofe@5094
|
429 |
|
berghofe@7710
|
430 |
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
berghofe@5094
|
431 |
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
|
berghofe@5094
|
432 |
|
berghofe@10988
|
433 |
in (preds, ind_prems, mutual_ind_concl,
|
berghofe@10988
|
434 |
map (apfst (fst o dest_Free)) factors)
|
berghofe@5094
|
435 |
end;
|
berghofe@5094
|
436 |
|
berghofe@5094
|
437 |
|
wenzelm@10735
|
438 |
(* prepare cases and induct rules *)
|
wenzelm@8316
|
439 |
|
wenzelm@8316
|
440 |
(*
|
wenzelm@8316
|
441 |
transform mutual rule:
|
wenzelm@8316
|
442 |
HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
|
wenzelm@8316
|
443 |
into i-th projection:
|
wenzelm@8316
|
444 |
xi:Ai ==> HH ==> Pi xi
|
wenzelm@8316
|
445 |
*)
|
wenzelm@8316
|
446 |
|
wenzelm@8316
|
447 |
fun project_rules [name] rule = [(name, rule)]
|
wenzelm@8316
|
448 |
| project_rules names mutual_rule =
|
wenzelm@8316
|
449 |
let
|
wenzelm@8316
|
450 |
val n = length names;
|
wenzelm@8316
|
451 |
fun proj i =
|
wenzelm@8316
|
452 |
(if i < n then (fn th => th RS conjunct1) else I)
|
wenzelm@8316
|
453 |
(Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
|
wenzelm@8316
|
454 |
RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
|
wenzelm@8316
|
455 |
in names ~~ map proj (1 upto n) end;
|
wenzelm@8316
|
456 |
|
wenzelm@12172
|
457 |
fun add_cases_induct no_elim no_induct names elims induct =
|
wenzelm@8316
|
458 |
let
|
wenzelm@9405
|
459 |
fun cases_spec (name, elim) thy =
|
wenzelm@9405
|
460 |
thy
|
wenzelm@9405
|
461 |
|> Theory.add_path (Sign.base_name name)
|
wenzelm@10279
|
462 |
|> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
|
wenzelm@9405
|
463 |
|> Theory.parent_path;
|
wenzelm@8375
|
464 |
val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
|
wenzelm@8316
|
465 |
|
wenzelm@11005
|
466 |
fun induct_spec (name, th) = #1 o PureThy.add_thms
|
wenzelm@11005
|
467 |
[(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
|
wenzelm@12172
|
468 |
val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
|
wenzelm@9405
|
469 |
in Library.apply (cases_specs @ induct_specs) end;
|
wenzelm@8316
|
470 |
|
wenzelm@8316
|
471 |
|
wenzelm@8316
|
472 |
|
wenzelm@10735
|
473 |
(** proofs for (co)inductive sets **)
|
wenzelm@6424
|
474 |
|
wenzelm@10735
|
475 |
(* prove monotonicity -- NOT subject to quick_and_dirty! *)
|
berghofe@5094
|
476 |
|
berghofe@5094
|
477 |
fun prove_mono setT fp_fun monos thy =
|
wenzelm@10735
|
478 |
(message " Proving monotonicity ...";
|
wenzelm@11880
|
479 |
Goals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*)
|
wenzelm@10735
|
480 |
(Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
|
wenzelm@10735
|
481 |
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
|
wenzelm@11502
|
482 |
(fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
|
berghofe@5094
|
483 |
|
berghofe@5094
|
484 |
|
wenzelm@10735
|
485 |
(* prove introduction rules *)
|
berghofe@5094
|
486 |
|
wenzelm@12180
|
487 |
fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
|
berghofe@5094
|
488 |
let
|
wenzelm@10735
|
489 |
val _ = clean_message " Proving the introduction rules ...";
|
berghofe@5094
|
490 |
|
berghofe@5094
|
491 |
val unfold = standard (mono RS (fp_def RS
|
nipkow@10186
|
492 |
(if coind then def_gfp_unfold else def_lfp_unfold)));
|
berghofe@5094
|
493 |
|
berghofe@5094
|
494 |
fun select_disj 1 1 = []
|
berghofe@5094
|
495 |
| select_disj _ 1 = [rtac disjI1]
|
berghofe@5094
|
496 |
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
|
berghofe@5094
|
497 |
|
wenzelm@11880
|
498 |
val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
|
wenzelm@10735
|
499 |
(Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
|
berghofe@5094
|
500 |
[(*insert prems and underlying sets*)
|
berghofe@5094
|
501 |
cut_facts_tac prems 1,
|
berghofe@5094
|
502 |
stac unfold 1,
|
berghofe@5094
|
503 |
REPEAT (resolve_tac [vimageI2, CollectI] 1),
|
berghofe@5094
|
504 |
(*Now 1-2 subgoals: the disjunction, perhaps equality.*)
|
berghofe@5094
|
505 |
EVERY1 (select_disj (length intr_ts) i),
|
berghofe@5094
|
506 |
(*Not ares_tac, since refl must be tried before any equality assumptions;
|
berghofe@5094
|
507 |
backtracking may occur if the premises have extra variables!*)
|
wenzelm@10735
|
508 |
DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
|
berghofe@5094
|
509 |
(*Now solve the equations like Inl 0 = Inl ?b2*)
|
wenzelm@10729
|
510 |
REPEAT (rtac refl 1)])
|
wenzelm@10729
|
511 |
|> rulify) (1 upto (length intr_ts) ~~ intr_ts)
|
berghofe@5094
|
512 |
|
berghofe@5094
|
513 |
in (intrs, unfold) end;
|
berghofe@5094
|
514 |
|
wenzelm@6424
|
515 |
|
wenzelm@10735
|
516 |
(* prove elimination rules *)
|
berghofe@5094
|
517 |
|
wenzelm@8375
|
518 |
fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
|
berghofe@5094
|
519 |
let
|
wenzelm@10735
|
520 |
val _ = clean_message " Proving the elimination rules ...";
|
berghofe@5094
|
521 |
|
berghofe@7710
|
522 |
val rules1 = [CollectE, disjE, make_elim vimageD, exE];
|
wenzelm@10735
|
523 |
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
|
wenzelm@8375
|
524 |
in
|
wenzelm@11005
|
525 |
mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
|
wenzelm@11880
|
526 |
quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
|
wenzelm@11005
|
527 |
(Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
|
wenzelm@11005
|
528 |
[cut_facts_tac [hd prems] 1,
|
wenzelm@11005
|
529 |
dtac (unfold RS subst) 1,
|
wenzelm@11005
|
530 |
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
|
wenzelm@11005
|
531 |
REPEAT (FIRSTGOAL (eresolve_tac rules2)),
|
wenzelm@11005
|
532 |
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
|
wenzelm@11005
|
533 |
|> rulify
|
wenzelm@11005
|
534 |
|> RuleCases.name cases)
|
wenzelm@8375
|
535 |
end;
|
berghofe@5094
|
536 |
|
wenzelm@6424
|
537 |
|
wenzelm@10735
|
538 |
(* derivation of simplified elimination rules *)
|
berghofe@5094
|
539 |
|
wenzelm@11682
|
540 |
local
|
wenzelm@11682
|
541 |
|
wenzelm@7107
|
542 |
(*cprop should have the form t:Si where Si is an inductive set*)
|
wenzelm@11682
|
543 |
val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
|
wenzelm@9598
|
544 |
|
wenzelm@11682
|
545 |
(*delete needless equality assumptions*)
|
wenzelm@11682
|
546 |
val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
|
wenzelm@11682
|
547 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
|
wenzelm@11682
|
548 |
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
|
wenzelm@11682
|
549 |
|
wenzelm@11682
|
550 |
fun simp_case_tac solved ss i =
|
wenzelm@11682
|
551 |
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
|
wenzelm@11682
|
552 |
THEN_MAYBE (if solved then no_tac else all_tac);
|
wenzelm@11682
|
553 |
|
wenzelm@11682
|
554 |
in
|
wenzelm@9598
|
555 |
|
wenzelm@9598
|
556 |
fun mk_cases_i elims ss cprop =
|
wenzelm@7107
|
557 |
let
|
wenzelm@7107
|
558 |
val prem = Thm.assume cprop;
|
wenzelm@11682
|
559 |
val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
|
wenzelm@9298
|
560 |
fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
|
wenzelm@7107
|
561 |
in
|
wenzelm@7107
|
562 |
(case get_first (try mk_elim) elims of
|
wenzelm@7107
|
563 |
Some r => r
|
wenzelm@7107
|
564 |
| None => error (Pretty.string_of (Pretty.block
|
wenzelm@9598
|
565 |
[Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
|
wenzelm@7107
|
566 |
end;
|
wenzelm@7107
|
567 |
|
paulson@6141
|
568 |
fun mk_cases elims s =
|
wenzelm@9598
|
569 |
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
|
wenzelm@9598
|
570 |
|
wenzelm@9598
|
571 |
fun smart_mk_cases thy ss cprop =
|
wenzelm@9598
|
572 |
let
|
wenzelm@9598
|
573 |
val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
|
wenzelm@9598
|
574 |
(Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
|
wenzelm@9598
|
575 |
val (_, {elims, ...}) = the_inductive thy c;
|
wenzelm@9598
|
576 |
in mk_cases_i elims ss cprop end;
|
wenzelm@7107
|
577 |
|
wenzelm@11682
|
578 |
end;
|
wenzelm@11682
|
579 |
|
wenzelm@7107
|
580 |
|
wenzelm@7107
|
581 |
(* inductive_cases(_i) *)
|
wenzelm@7107
|
582 |
|
wenzelm@12609
|
583 |
fun gen_inductive_cases prep_att prep_prop args thy =
|
wenzelm@9598
|
584 |
let
|
wenzelm@12609
|
585 |
val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
|
wenzelm@12609
|
586 |
val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
|
wenzelm@12609
|
587 |
|
wenzelm@12876
|
588 |
val facts = args |> map (fn ((a, atts), props) =>
|
wenzelm@12876
|
589 |
((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
|
wenzelm@12709
|
590 |
in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
|
berghofe@5094
|
591 |
|
wenzelm@12172
|
592 |
val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
|
wenzelm@12172
|
593 |
val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
|
wenzelm@7107
|
594 |
|
wenzelm@6424
|
595 |
|
wenzelm@9598
|
596 |
(* mk_cases_meth *)
|
wenzelm@9598
|
597 |
|
wenzelm@9598
|
598 |
fun mk_cases_meth (ctxt, raw_props) =
|
wenzelm@9598
|
599 |
let
|
wenzelm@9598
|
600 |
val thy = ProofContext.theory_of ctxt;
|
wenzelm@9598
|
601 |
val ss = Simplifier.get_local_simpset ctxt;
|
wenzelm@9598
|
602 |
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
|
wenzelm@10743
|
603 |
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
|
wenzelm@9598
|
604 |
|
wenzelm@9598
|
605 |
val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
|
wenzelm@9598
|
606 |
|
wenzelm@9598
|
607 |
|
wenzelm@10735
|
608 |
(* prove induction rule *)
|
berghofe@5094
|
609 |
|
berghofe@5094
|
610 |
fun prove_indrule cs cTs sumT rec_const params intr_ts mono
|
berghofe@5094
|
611 |
fp_def rec_sets_defs thy =
|
berghofe@5094
|
612 |
let
|
wenzelm@10735
|
613 |
val _ = clean_message " Proving the induction rule ...";
|
berghofe@5094
|
614 |
|
wenzelm@6394
|
615 |
val sign = Theory.sign_of thy;
|
berghofe@5094
|
616 |
|
berghofe@7293
|
617 |
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
|
berghofe@7293
|
618 |
None => []
|
berghofe@7293
|
619 |
| Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
|
berghofe@7293
|
620 |
|
berghofe@10988
|
621 |
val (preds, ind_prems, mutual_ind_concl, factors) =
|
berghofe@10988
|
622 |
mk_indrule cs cTs params intr_ts;
|
berghofe@5094
|
623 |
|
berghofe@5094
|
624 |
(* make predicate for instantiation of abstract induction rule *)
|
berghofe@5094
|
625 |
|
berghofe@5094
|
626 |
fun mk_ind_pred _ [P] = P
|
berghofe@5094
|
627 |
| mk_ind_pred T Ps =
|
berghofe@5094
|
628 |
let val n = (length Ps) div 2;
|
berghofe@5094
|
629 |
val Type (_, [T1, T2]) = T
|
berghofe@7293
|
630 |
in Const ("Datatype.sum.sum_case",
|
berghofe@5094
|
631 |
[T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
|
berghofe@5094
|
632 |
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
|
berghofe@5094
|
633 |
end;
|
berghofe@5094
|
634 |
|
berghofe@5094
|
635 |
val ind_pred = mk_ind_pred sumT preds;
|
berghofe@5094
|
636 |
|
berghofe@5094
|
637 |
val ind_concl = HOLogic.mk_Trueprop
|
berghofe@5094
|
638 |
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
|
berghofe@5094
|
639 |
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
|
berghofe@5094
|
640 |
|
berghofe@5094
|
641 |
(* simplification rules for vimage and Collect *)
|
berghofe@5094
|
642 |
|
berghofe@5094
|
643 |
val vimage_simps = if length cs < 2 then [] else
|
wenzelm@11880
|
644 |
map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
|
berghofe@5094
|
645 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq
|
berghofe@5094
|
646 |
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
|
berghofe@5094
|
647 |
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
|
berghofe@5094
|
648 |
nth_elem (find_index_eq c cs, preds)))))
|
wenzelm@10735
|
649 |
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
|
berghofe@5094
|
650 |
|
wenzelm@11880
|
651 |
val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
|
berghofe@5094
|
652 |
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
|
berghofe@5094
|
653 |
[rtac (impI RS allI) 1,
|
nipkow@10202
|
654 |
DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
|
berghofe@7710
|
655 |
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
|
berghofe@5094
|
656 |
fold_goals_tac rec_sets_defs,
|
berghofe@5094
|
657 |
(*This CollectE and disjE separates out the introduction rules*)
|
berghofe@7710
|
658 |
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
|
berghofe@5094
|
659 |
(*Now break down the individual cases. No disjE here in case
|
berghofe@5094
|
660 |
some premise involves disjunction.*)
|
berghofe@7710
|
661 |
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
|
berghofe@7293
|
662 |
rewrite_goals_tac sum_case_rewrites,
|
berghofe@5094
|
663 |
EVERY (map (fn prem =>
|
berghofe@5149
|
664 |
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
|
berghofe@5094
|
665 |
|
wenzelm@11880
|
666 |
val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
|
berghofe@5094
|
667 |
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
|
berghofe@5094
|
668 |
[cut_facts_tac prems 1,
|
berghofe@5094
|
669 |
REPEAT (EVERY
|
berghofe@5094
|
670 |
[REPEAT (resolve_tac [conjI, impI] 1),
|
berghofe@5094
|
671 |
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
|
berghofe@7293
|
672 |
rewrite_goals_tac sum_case_rewrites,
|
berghofe@5094
|
673 |
atac 1])])
|
berghofe@5094
|
674 |
|
berghofe@10988
|
675 |
in standard (split_rule factors (induct RS lemma)) end;
|
berghofe@5094
|
676 |
|
wenzelm@6424
|
677 |
|
wenzelm@6424
|
678 |
|
wenzelm@10735
|
679 |
(** specification of (co)inductive sets **)
|
berghofe@5094
|
680 |
|
wenzelm@10729
|
681 |
fun cond_declare_consts declare_consts cs paramTs cnames =
|
wenzelm@10729
|
682 |
if declare_consts then
|
wenzelm@10729
|
683 |
Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
|
wenzelm@10729
|
684 |
else I;
|
wenzelm@10729
|
685 |
|
wenzelm@12180
|
686 |
fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
|
berghofe@9072
|
687 |
params paramTs cTs cnames =
|
berghofe@5094
|
688 |
let
|
berghofe@5094
|
689 |
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
|
berghofe@5094
|
690 |
val setT = HOLogic.mk_setT sumT;
|
berghofe@5094
|
691 |
|
wenzelm@10735
|
692 |
val fp_name = if coind then gfp_name else lfp_name;
|
berghofe@5094
|
693 |
|
berghofe@5149
|
694 |
val used = foldr add_term_names (intr_ts, []);
|
berghofe@5149
|
695 |
val [sname, xname] = variantlist (["S", "x"], used);
|
berghofe@5149
|
696 |
|
berghofe@5094
|
697 |
(* transform an introduction rule into a conjunction *)
|
berghofe@5094
|
698 |
(* [| t : ... S_i ... ; ... |] ==> u : S_j *)
|
berghofe@5094
|
699 |
(* is transformed into *)
|
berghofe@5094
|
700 |
(* x = Inj_j u & t : ... Inj_i -`` S ... & ... *)
|
berghofe@5094
|
701 |
|
berghofe@5094
|
702 |
fun transform_rule r =
|
berghofe@5094
|
703 |
let
|
berghofe@5094
|
704 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
|
berghofe@5149
|
705 |
val subst = subst_free
|
berghofe@5149
|
706 |
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
|
berghofe@5094
|
707 |
val Const ("op :", _) $ t $ u =
|
berghofe@5094
|
708 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
|
berghofe@5094
|
709 |
|
berghofe@5094
|
710 |
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
|
berghofe@7710
|
711 |
(frees, foldr1 HOLogic.mk_conj
|
berghofe@5149
|
712 |
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
|
berghofe@5094
|
713 |
(map (subst o HOLogic.dest_Trueprop)
|
berghofe@5094
|
714 |
(Logic.strip_imp_prems r))))
|
berghofe@5094
|
715 |
end
|
berghofe@5094
|
716 |
|
berghofe@5094
|
717 |
(* make a disjunction of all introduction rules *)
|
berghofe@5094
|
718 |
|
berghofe@5149
|
719 |
val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
|
berghofe@7710
|
720 |
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
|
berghofe@5094
|
721 |
|
berghofe@5094
|
722 |
(* add definiton of recursive sets to theory *)
|
berghofe@5094
|
723 |
|
berghofe@5094
|
724 |
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
|
wenzelm@6394
|
725 |
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
|
berghofe@5094
|
726 |
|
berghofe@5094
|
727 |
val rec_const = list_comb
|
berghofe@5094
|
728 |
(Const (full_rec_name, paramTs ---> setT), params);
|
berghofe@5094
|
729 |
|
berghofe@5094
|
730 |
val fp_def_term = Logic.mk_equals (rec_const,
|
wenzelm@10735
|
731 |
Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
|
berghofe@5094
|
732 |
|
berghofe@5094
|
733 |
val def_terms = fp_def_term :: (if length cs < 2 then [] else
|
berghofe@5094
|
734 |
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
|
berghofe@5094
|
735 |
|
wenzelm@8433
|
736 |
val (thy', [fp_def :: rec_sets_defs]) =
|
wenzelm@8433
|
737 |
thy
|
wenzelm@10729
|
738 |
|> cond_declare_consts declare_consts cs paramTs cnames
|
wenzelm@8433
|
739 |
|> (if length cs < 2 then I
|
wenzelm@8433
|
740 |
else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
|
wenzelm@8433
|
741 |
|> Theory.add_path rec_name
|
wenzelm@9315
|
742 |
|> PureThy.add_defss_i false [(("defs", def_terms), [])];
|
berghofe@5094
|
743 |
|
berghofe@9072
|
744 |
val mono = prove_mono setT fp_fun monos thy'
|
berghofe@5094
|
745 |
|
wenzelm@10735
|
746 |
in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
|
berghofe@5094
|
747 |
|
berghofe@9072
|
748 |
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
|
wenzelm@12180
|
749 |
intros monos thy params paramTs cTs cnames induct_cases =
|
berghofe@9072
|
750 |
let
|
wenzelm@10735
|
751 |
val _ =
|
wenzelm@10735
|
752 |
if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
|
wenzelm@10735
|
753 |
commas_quote cnames) else ();
|
berghofe@9072
|
754 |
|
berghofe@9072
|
755 |
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
|
berghofe@9072
|
756 |
|
wenzelm@9939
|
757 |
val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
|
wenzelm@12180
|
758 |
mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
|
berghofe@9072
|
759 |
params paramTs cTs cnames;
|
berghofe@9072
|
760 |
|
wenzelm@12180
|
761 |
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
|
berghofe@5094
|
762 |
val elims = if no_elim then [] else
|
wenzelm@9939
|
763 |
prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
|
wenzelm@8312
|
764 |
val raw_induct = if no_ind then Drule.asm_rl else
|
berghofe@5094
|
765 |
if coind then standard (rule_by_tactic
|
oheimb@5553
|
766 |
(rewrite_tac [mk_meta_eq vimage_Un] THEN
|
berghofe@5094
|
767 |
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
|
berghofe@5094
|
768 |
else
|
berghofe@5094
|
769 |
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
|
wenzelm@9939
|
770 |
rec_sets_defs thy1;
|
wenzelm@12165
|
771 |
val induct =
|
wenzelm@12165
|
772 |
if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
|
wenzelm@12165
|
773 |
else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
|
berghofe@5094
|
774 |
|
wenzelm@9939
|
775 |
val (thy2, intrs') =
|
wenzelm@9939
|
776 |
thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
|
wenzelm@10735
|
777 |
val (thy3, ([intrs'', elims'], [induct'])) =
|
wenzelm@10735
|
778 |
thy2
|
wenzelm@11005
|
779 |
|> PureThy.add_thmss
|
wenzelm@11628
|
780 |
[(("intros", intrs'), []),
|
wenzelm@11005
|
781 |
(("elims", elims), [RuleCases.consumes 1])]
|
wenzelm@10735
|
782 |
|>>> PureThy.add_thms
|
wenzelm@12165
|
783 |
[((coind_prefix coind ^ "induct", rulify (#1 induct)),
|
wenzelm@12165
|
784 |
(RuleCases.case_names induct_cases :: #2 induct))]
|
wenzelm@8433
|
785 |
|>> Theory.parent_path;
|
wenzelm@9939
|
786 |
in (thy3,
|
wenzelm@10735
|
787 |
{defs = fp_def :: rec_sets_defs,
|
berghofe@5094
|
788 |
mono = mono,
|
berghofe@5094
|
789 |
unfold = unfold,
|
wenzelm@9939
|
790 |
intrs = intrs'',
|
wenzelm@7798
|
791 |
elims = elims',
|
wenzelm@7798
|
792 |
mk_cases = mk_cases elims',
|
wenzelm@10729
|
793 |
raw_induct = rulify raw_induct,
|
wenzelm@7798
|
794 |
induct = induct'})
|
berghofe@5094
|
795 |
end;
|
berghofe@5094
|
796 |
|
wenzelm@6424
|
797 |
|
wenzelm@10735
|
798 |
(* external interfaces *)
|
wenzelm@6424
|
799 |
|
wenzelm@10735
|
800 |
fun try_term f msg sign t =
|
wenzelm@10735
|
801 |
(case Library.try f t of
|
wenzelm@10735
|
802 |
Some x => x
|
wenzelm@10735
|
803 |
| None => error (msg ^ Sign.string_of_term sign t));
|
berghofe@5094
|
804 |
|
wenzelm@12180
|
805 |
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
|
berghofe@5094
|
806 |
let
|
wenzelm@6424
|
807 |
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
|
wenzelm@6394
|
808 |
val sign = Theory.sign_of thy;
|
berghofe@5094
|
809 |
|
berghofe@5094
|
810 |
(*parameters should agree for all mutually recursive components*)
|
berghofe@5094
|
811 |
val (_, params) = strip_comb (hd cs);
|
wenzelm@10735
|
812 |
val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
|
berghofe@5094
|
813 |
\ component is not a free variable: " sign) params;
|
berghofe@5094
|
814 |
|
wenzelm@10735
|
815 |
val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
|
berghofe@5094
|
816 |
"Recursive component not of type set: " sign) cs;
|
berghofe@5094
|
817 |
|
wenzelm@10735
|
818 |
val full_cnames = map (try_term (fst o dest_Const o head_of)
|
berghofe@5094
|
819 |
"Recursive set not previously declared as constant: " sign) cs;
|
wenzelm@6437
|
820 |
val cnames = map Sign.base_name full_cnames;
|
berghofe@5094
|
821 |
|
wenzelm@10729
|
822 |
val save_sign =
|
wenzelm@10729
|
823 |
thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
|
wenzelm@10729
|
824 |
val intros = map (check_rule save_sign cs) pre_intros;
|
wenzelm@8401
|
825 |
val induct_cases = map (#1 o #1) intros;
|
wenzelm@6437
|
826 |
|
wenzelm@9405
|
827 |
val (thy1, result as {elims, induct, ...}) =
|
wenzelm@11628
|
828 |
add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
|
wenzelm@12180
|
829 |
thy params paramTs cTs cnames induct_cases;
|
wenzelm@8307
|
830 |
val thy2 = thy1
|
wenzelm@8307
|
831 |
|> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
|
wenzelm@12172
|
832 |
|> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
|
wenzelm@12172
|
833 |
full_cnames elims induct;
|
wenzelm@6437
|
834 |
in (thy2, result) end;
|
berghofe@5094
|
835 |
|
wenzelm@12180
|
836 |
fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
|
berghofe@5094
|
837 |
let
|
wenzelm@6394
|
838 |
val sign = Theory.sign_of thy;
|
wenzelm@12338
|
839 |
val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
|
wenzelm@6424
|
840 |
|
wenzelm@6424
|
841 |
val intr_names = map (fst o fst) intro_srcs;
|
wenzelm@9405
|
842 |
fun read_rule s = Thm.read_cterm sign (s, propT)
|
wenzelm@9405
|
843 |
handle ERROR => error ("The error(s) above occurred for " ^ s);
|
wenzelm@9405
|
844 |
val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
|
wenzelm@6424
|
845 |
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
|
berghofe@7020
|
846 |
val (cs', intr_ts') = unify_consts sign cs intr_ts;
|
berghofe@5094
|
847 |
|
wenzelm@12180
|
848 |
val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
|
wenzelm@6424
|
849 |
in
|
berghofe@7020
|
850 |
add_inductive_i verbose false "" coind false false cs'
|
wenzelm@12180
|
851 |
((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
|
berghofe@5094
|
852 |
end;
|
berghofe@5094
|
853 |
|
wenzelm@6424
|
854 |
|
wenzelm@6424
|
855 |
|
wenzelm@6437
|
856 |
(** package setup **)
|
wenzelm@6437
|
857 |
|
wenzelm@6437
|
858 |
(* setup theory *)
|
wenzelm@6437
|
859 |
|
wenzelm@8634
|
860 |
val setup =
|
wenzelm@8634
|
861 |
[InductiveData.init,
|
wenzelm@9625
|
862 |
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
|
wenzelm@9598
|
863 |
"dynamic case analysis on sets")],
|
wenzelm@9893
|
864 |
Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
|
wenzelm@6437
|
865 |
|
wenzelm@6437
|
866 |
|
wenzelm@6437
|
867 |
(* outer syntax *)
|
wenzelm@6424
|
868 |
|
wenzelm@6723
|
869 |
local structure P = OuterParse and K = OuterSyntax.Keyword in
|
wenzelm@6424
|
870 |
|
wenzelm@12180
|
871 |
fun mk_ind coind ((sets, intrs), monos) =
|
wenzelm@12180
|
872 |
#1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
|
wenzelm@6424
|
873 |
|
wenzelm@6424
|
874 |
fun ind_decl coind =
|
wenzelm@12876
|
875 |
Scan.repeat1 P.term --
|
wenzelm@9598
|
876 |
(P.$$$ "intros" |--
|
wenzelm@12876
|
877 |
P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
|
wenzelm@12876
|
878 |
Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
|
wenzelm@6424
|
879 |
>> (Toplevel.theory o mk_ind coind);
|
wenzelm@6424
|
880 |
|
wenzelm@6723
|
881 |
val inductiveP =
|
wenzelm@6723
|
882 |
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
|
wenzelm@6723
|
883 |
|
wenzelm@6723
|
884 |
val coinductiveP =
|
wenzelm@6723
|
885 |
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
|
wenzelm@6424
|
886 |
|
wenzelm@7107
|
887 |
|
wenzelm@7107
|
888 |
val ind_cases =
|
wenzelm@12876
|
889 |
P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
|
wenzelm@7107
|
890 |
>> (Toplevel.theory o inductive_cases);
|
wenzelm@7107
|
891 |
|
wenzelm@7107
|
892 |
val inductive_casesP =
|
wenzelm@9804
|
893 |
OuterSyntax.command "inductive_cases"
|
wenzelm@9598
|
894 |
"create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
|
wenzelm@7107
|
895 |
|
wenzelm@12180
|
896 |
val _ = OuterSyntax.add_keywords ["intros", "monos"];
|
wenzelm@7107
|
897 |
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
|
wenzelm@6424
|
898 |
|
berghofe@5094
|
899 |
end;
|
wenzelm@6424
|
900 |
|
wenzelm@6424
|
901 |
end;
|