haftmann@31723
|
1 |
(* Title: HOL/Tools/inductive.ML
|
berghofe@5094
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
wenzelm@21367
|
3 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
|
berghofe@5094
|
4 |
|
wenzelm@6424
|
5 |
(Co)Inductive Definition module for HOL.
|
berghofe@5094
|
6 |
|
berghofe@5094
|
7 |
Features:
|
wenzelm@6424
|
8 |
* least or greatest fixedpoints
|
wenzelm@6424
|
9 |
* mutually recursive definitions
|
wenzelm@6424
|
10 |
* definitions involving arbitrary monotone operators
|
wenzelm@6424
|
11 |
* automatically proves introduction and elimination rules
|
berghofe@5094
|
12 |
|
berghofe@5094
|
13 |
Introduction rules have the form
|
berghofe@21024
|
14 |
[| M Pj ti, ..., Q x, ... |] ==> Pk t
|
berghofe@5094
|
15 |
where M is some monotone operator (usually the identity)
|
berghofe@21024
|
16 |
Q x is any side condition on the free variables
|
berghofe@5094
|
17 |
ti, t are any terms
|
berghofe@21024
|
18 |
Pj, Pk are two of the predicates being defined in mutual recursion
|
berghofe@5094
|
19 |
*)
|
berghofe@5094
|
20 |
|
haftmann@31723
|
21 |
signature BASIC_INDUCTIVE =
|
berghofe@5094
|
22 |
sig
|
wenzelm@33464
|
23 |
type inductive_result =
|
wenzelm@33464
|
24 |
{preds: term list, elims: thm list, raw_induct: thm,
|
wenzelm@33464
|
25 |
induct: thm, intrs: thm list}
|
wenzelm@21526
|
26 |
val morph_result: morphism -> inductive_result -> inductive_result
|
wenzelm@33464
|
27 |
type inductive_info = {names: string list, coind: bool} * inductive_result
|
wenzelm@21526
|
28 |
val the_inductive: Proof.context -> string -> inductive_info
|
wenzelm@21367
|
29 |
val print_inductives: Proof.context -> unit
|
wenzelm@18728
|
30 |
val mono_add: attribute
|
wenzelm@18728
|
31 |
val mono_del: attribute
|
wenzelm@21367
|
32 |
val get_monos: Proof.context -> thm list
|
wenzelm@21367
|
33 |
val mk_cases: Proof.context -> term -> thm
|
wenzelm@10910
|
34 |
val inductive_forall_name: string
|
wenzelm@10910
|
35 |
val inductive_forall_def: thm
|
wenzelm@10910
|
36 |
val rulify: thm -> thm
|
wenzelm@28839
|
37 |
val inductive_cases: (Attrib.binding * string list) list -> local_theory ->
|
wenzelm@28084
|
38 |
thm list list * local_theory
|
wenzelm@28839
|
39 |
val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
|
wenzelm@28084
|
40 |
thm list list * local_theory
|
wenzelm@33464
|
41 |
type inductive_flags =
|
wenzelm@33671
|
42 |
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
|
wenzelm@33671
|
43 |
no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
|
wenzelm@24815
|
44 |
val add_inductive_i:
|
haftmann@29581
|
45 |
inductive_flags -> ((binding * typ) * mixfix) list ->
|
wenzelm@28084
|
46 |
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
|
wenzelm@28084
|
47 |
inductive_result * local_theory
|
wenzelm@28083
|
48 |
val add_inductive: bool -> bool ->
|
haftmann@29581
|
49 |
(binding * string option * mixfix) list ->
|
haftmann@29581
|
50 |
(binding * string option * mixfix) list ->
|
wenzelm@28084
|
51 |
(Attrib.binding * string) list ->
|
wenzelm@28083
|
52 |
(Facts.ref * Attrib.src list) list ->
|
wenzelm@29412
|
53 |
bool -> local_theory -> inductive_result * local_theory
|
wenzelm@33736
|
54 |
val add_inductive_global: inductive_flags ->
|
haftmann@29581
|
55 |
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
|
wenzelm@28084
|
56 |
thm list -> theory -> inductive_result * theory
|
berghofe@22789
|
57 |
val arities_of: thm -> (string * int) list
|
berghofe@22789
|
58 |
val params_of: thm -> term list
|
berghofe@22789
|
59 |
val partition_rules: thm -> thm list -> (string * thm list) list
|
berghofe@25822
|
60 |
val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list
|
berghofe@22789
|
61 |
val unpartition_rules: thm list -> (string * 'a list) list -> 'a list
|
berghofe@22789
|
62 |
val infer_intro_vars: thm -> int -> thm list -> term list list
|
wenzelm@18708
|
63 |
val setup: theory -> theory
|
berghofe@5094
|
64 |
end;
|
berghofe@5094
|
65 |
|
haftmann@31723
|
66 |
signature INDUCTIVE =
|
berghofe@23762
|
67 |
sig
|
haftmann@31723
|
68 |
include BASIC_INDUCTIVE
|
wenzelm@33464
|
69 |
type add_ind_def =
|
wenzelm@33464
|
70 |
inductive_flags ->
|
wenzelm@33464
|
71 |
term list -> (Attrib.binding * term) list -> thm list ->
|
wenzelm@33464
|
72 |
term list -> (binding * mixfix) list ->
|
wenzelm@33464
|
73 |
local_theory -> inductive_result * local_theory
|
wenzelm@33671
|
74 |
val declare_rules: binding -> bool -> bool -> string list ->
|
berghofe@34973
|
75 |
thm list -> binding list -> Attrib.src list list -> (thm * string list * int) list ->
|
berghofe@23762
|
76 |
thm -> local_theory -> thm list * thm list * thm * local_theory
|
berghofe@23762
|
77 |
val add_ind_def: add_ind_def
|
wenzelm@28083
|
78 |
val gen_add_inductive_i: add_ind_def -> inductive_flags ->
|
haftmann@29581
|
79 |
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
|
wenzelm@28084
|
80 |
thm list -> local_theory -> inductive_result * local_theory
|
wenzelm@28083
|
81 |
val gen_add_inductive: add_ind_def -> bool -> bool ->
|
haftmann@29581
|
82 |
(binding * string option * mixfix) list ->
|
haftmann@29581
|
83 |
(binding * string option * mixfix) list ->
|
wenzelm@28084
|
84 |
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
|
wenzelm@29412
|
85 |
bool -> local_theory -> inductive_result * local_theory
|
wenzelm@26988
|
86 |
val gen_ind_decl: add_ind_def -> bool ->
|
wenzelm@29412
|
87 |
OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
|
berghofe@23762
|
88 |
end;
|
berghofe@23762
|
89 |
|
haftmann@31723
|
90 |
structure Inductive: INDUCTIVE =
|
berghofe@5094
|
91 |
struct
|
berghofe@5094
|
92 |
|
wenzelm@9598
|
93 |
|
wenzelm@10729
|
94 |
(** theory context references **)
|
wenzelm@10729
|
95 |
|
wenzelm@11991
|
96 |
val inductive_forall_name = "HOL.induct_forall";
|
haftmann@32602
|
97 |
val inductive_forall_def = @{thm induct_forall_def};
|
wenzelm@11991
|
98 |
val inductive_conj_name = "HOL.induct_conj";
|
haftmann@32602
|
99 |
val inductive_conj_def = @{thm induct_conj_def};
|
haftmann@32602
|
100 |
val inductive_conj = @{thms induct_conj};
|
haftmann@32602
|
101 |
val inductive_atomize = @{thms induct_atomize};
|
haftmann@32602
|
102 |
val inductive_rulify = @{thms induct_rulify};
|
haftmann@32602
|
103 |
val inductive_rulify_fallback = @{thms induct_rulify_fallback};
|
wenzelm@10729
|
104 |
|
berghofe@21024
|
105 |
val notTrueE = TrueI RSN (2, notE);
|
berghofe@21024
|
106 |
val notFalseI = Seq.hd (atac 1 notI);
|
wenzelm@32181
|
107 |
|
wenzelm@32181
|
108 |
val simp_thms' = map mk_meta_eq
|
wenzelm@32181
|
109 |
@{lemma "(~True) = False" "(~False) = True"
|
wenzelm@32181
|
110 |
"(True --> P) = P" "(False --> P) = True"
|
wenzelm@32181
|
111 |
"(P & True) = P" "(True & P) = P"
|
wenzelm@32181
|
112 |
by (fact simp_thms)+};
|
berghofe@21024
|
113 |
|
haftmann@32652
|
114 |
val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
|
haftmann@32652
|
115 |
|
haftmann@32652
|
116 |
val simp_thms''' = map mk_meta_eq
|
haftmann@32652
|
117 |
[@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
|
wenzelm@10729
|
118 |
|
wenzelm@10729
|
119 |
|
wenzelm@22846
|
120 |
(** context data **)
|
berghofe@7710
|
121 |
|
berghofe@21024
|
122 |
type inductive_result =
|
berghofe@23762
|
123 |
{preds: term list, elims: thm list, raw_induct: thm,
|
berghofe@23762
|
124 |
induct: thm, intrs: thm list};
|
berghofe@21024
|
125 |
|
berghofe@23762
|
126 |
fun morph_result phi {preds, elims, raw_induct: thm, induct, intrs} =
|
wenzelm@21526
|
127 |
let
|
wenzelm@21526
|
128 |
val term = Morphism.term phi;
|
wenzelm@21526
|
129 |
val thm = Morphism.thm phi;
|
wenzelm@21526
|
130 |
val fact = Morphism.fact phi;
|
wenzelm@21526
|
131 |
in
|
berghofe@23762
|
132 |
{preds = map term preds, elims = fact elims, raw_induct = thm raw_induct,
|
berghofe@23762
|
133 |
induct = thm induct, intrs = fact intrs}
|
wenzelm@21526
|
134 |
end;
|
wenzelm@21526
|
135 |
|
berghofe@7710
|
136 |
type inductive_info =
|
berghofe@21024
|
137 |
{names: string list, coind: bool} * inductive_result;
|
berghofe@7710
|
138 |
|
wenzelm@33519
|
139 |
structure InductiveData = Generic_Data
|
wenzelm@22846
|
140 |
(
|
berghofe@7710
|
141 |
type T = inductive_info Symtab.table * thm list;
|
berghofe@7710
|
142 |
val empty = (Symtab.empty, []);
|
wenzelm@16432
|
143 |
val extend = I;
|
wenzelm@33519
|
144 |
fun merge ((tab1, monos1), (tab2, monos2)) : T =
|
wenzelm@24039
|
145 |
(Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
|
wenzelm@22846
|
146 |
);
|
berghofe@7710
|
147 |
|
wenzelm@21526
|
148 |
val get_inductives = InductiveData.get o Context.Proof;
|
wenzelm@22846
|
149 |
|
wenzelm@22846
|
150 |
fun print_inductives ctxt =
|
wenzelm@22846
|
151 |
let
|
wenzelm@22846
|
152 |
val (tab, monos) = get_inductives ctxt;
|
wenzelm@22846
|
153 |
val space = Consts.space_of (ProofContext.consts_of ctxt);
|
wenzelm@22846
|
154 |
in
|
wenzelm@33100
|
155 |
[Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
|
wenzelm@32111
|
156 |
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
|
wenzelm@22846
|
157 |
|> Pretty.chunks |> Pretty.writeln
|
wenzelm@22846
|
158 |
end;
|
berghofe@7710
|
159 |
|
berghofe@7710
|
160 |
|
berghofe@7710
|
161 |
(* get and put data *)
|
berghofe@7710
|
162 |
|
wenzelm@21367
|
163 |
fun the_inductive ctxt name =
|
wenzelm@21526
|
164 |
(case Symtab.lookup (#1 (get_inductives ctxt)) name of
|
berghofe@21024
|
165 |
NONE => error ("Unknown (co)inductive predicate " ^ quote name)
|
skalberg@15531
|
166 |
| SOME info => info);
|
wenzelm@9598
|
167 |
|
wenzelm@25380
|
168 |
fun put_inductives names info = InductiveData.map
|
wenzelm@25380
|
169 |
(apfst (fold (fn name => Symtab.update (name, info)) names));
|
berghofe@7710
|
170 |
|
berghofe@7710
|
171 |
|
berghofe@7710
|
172 |
|
berghofe@7710
|
173 |
(** monotonicity rules **)
|
berghofe@7710
|
174 |
|
wenzelm@21526
|
175 |
val get_monos = #2 o get_inductives;
|
wenzelm@21367
|
176 |
val map_monos = InductiveData.map o apsnd;
|
wenzelm@8277
|
177 |
|
berghofe@7710
|
178 |
fun mk_mono thm =
|
berghofe@7710
|
179 |
let
|
berghofe@33899
|
180 |
fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
|
haftmann@32652
|
181 |
fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
|
haftmann@32652
|
182 |
handle THM _ => thm RS @{thm le_boolD}
|
berghofe@7710
|
183 |
in
|
berghofe@33899
|
184 |
case concl_of thm of
|
berghofe@22275
|
185 |
Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
|
wenzelm@35364
|
186 |
| _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
|
haftmann@35092
|
187 |
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
|
berghofe@33899
|
188 |
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
|
berghofe@33899
|
189 |
(resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
|
berghofe@33899
|
190 |
| _ => thm
|
wenzelm@32111
|
191 |
end handle THM _ =>
|
wenzelm@32111
|
192 |
error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
|
berghofe@7710
|
193 |
|
berghofe@33899
|
194 |
val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
|
berghofe@33899
|
195 |
val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
|
berghofe@7710
|
196 |
|
berghofe@7710
|
197 |
|
wenzelm@7107
|
198 |
|
wenzelm@10735
|
199 |
(** misc utilities **)
|
wenzelm@6424
|
200 |
|
wenzelm@26477
|
201 |
fun message quiet_mode s = if quiet_mode then () else writeln s;
|
wenzelm@26477
|
202 |
fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
|
berghofe@5662
|
203 |
|
wenzelm@6424
|
204 |
fun coind_prefix true = "co"
|
wenzelm@6424
|
205 |
| coind_prefix false = "";
|
wenzelm@6424
|
206 |
|
wenzelm@24133
|
207 |
fun log (b:int) m n = if m >= n then 0 else 1 + log b (b * m) n;
|
wenzelm@6424
|
208 |
|
berghofe@21024
|
209 |
fun make_bool_args f g [] i = []
|
berghofe@21024
|
210 |
| make_bool_args f g (x :: xs) i =
|
berghofe@21024
|
211 |
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2);
|
berghofe@7020
|
212 |
|
berghofe@21024
|
213 |
fun make_bool_args' xs =
|
berghofe@21024
|
214 |
make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
|
berghofe@7020
|
215 |
|
haftmann@33956
|
216 |
fun arg_types_of k c = drop k (binder_types (fastype_of c));
|
haftmann@33077
|
217 |
|
berghofe@21024
|
218 |
fun find_arg T x [] = sys_error "find_arg"
|
berghofe@21024
|
219 |
| find_arg T x ((p as (_, (SOME _, _))) :: ps) =
|
berghofe@21024
|
220 |
apsnd (cons p) (find_arg T x ps)
|
berghofe@21024
|
221 |
| find_arg T x ((p as (U, (NONE, y))) :: ps) =
|
wenzelm@23577
|
222 |
if (T: typ) = U then (y, (U, (SOME x, y)) :: ps)
|
berghofe@21024
|
223 |
else apsnd (cons p) (find_arg T x ps);
|
berghofe@7020
|
224 |
|
berghofe@21024
|
225 |
fun make_args Ts xs =
|
haftmann@28524
|
226 |
map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t)
|
berghofe@21024
|
227 |
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
|
berghofe@21024
|
228 |
|
berghofe@21024
|
229 |
fun make_args' Ts xs Us =
|
berghofe@21024
|
230 |
fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs));
|
berghofe@21024
|
231 |
|
berghofe@21024
|
232 |
fun dest_predicate cs params t =
|
berghofe@5094
|
233 |
let
|
berghofe@21024
|
234 |
val k = length params;
|
berghofe@21024
|
235 |
val (c, ts) = strip_comb t;
|
berghofe@21024
|
236 |
val (xs, ys) = chop k ts;
|
haftmann@31986
|
237 |
val i = find_index (fn c' => c' = c) cs;
|
berghofe@21024
|
238 |
in
|
berghofe@21024
|
239 |
if xs = params andalso i >= 0 then
|
haftmann@33077
|
240 |
SOME (c, i, ys, chop (length ys) (arg_types_of k c))
|
berghofe@21024
|
241 |
else NONE
|
berghofe@5094
|
242 |
end;
|
berghofe@5094
|
243 |
|
berghofe@21024
|
244 |
fun mk_names a 0 = []
|
berghofe@21024
|
245 |
| mk_names a 1 = [a]
|
berghofe@21024
|
246 |
| mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
|
berghofe@5094
|
247 |
|
wenzelm@6424
|
248 |
|
wenzelm@6424
|
249 |
|
wenzelm@10729
|
250 |
(** process rules **)
|
berghofe@5094
|
251 |
|
wenzelm@10729
|
252 |
local
|
berghofe@5094
|
253 |
|
berghofe@23762
|
254 |
fun err_in_rule ctxt name t msg =
|
wenzelm@16432
|
255 |
error (cat_lines ["Ill-formed introduction rule " ^ quote name,
|
wenzelm@24920
|
256 |
Syntax.string_of_term ctxt t, msg]);
|
berghofe@5094
|
257 |
|
berghofe@23762
|
258 |
fun err_in_prem ctxt name t p msg =
|
wenzelm@24920
|
259 |
error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
|
wenzelm@24920
|
260 |
"in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
|
berghofe@5094
|
261 |
|
berghofe@21024
|
262 |
val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
|
wenzelm@10729
|
263 |
|
berghofe@21024
|
264 |
val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate";
|
berghofe@21024
|
265 |
|
berghofe@21024
|
266 |
val bad_app = "Inductive predicate must be applied to parameter(s) ";
|
paulson@11358
|
267 |
|
wenzelm@16432
|
268 |
fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
|
wenzelm@10729
|
269 |
|
wenzelm@10729
|
270 |
in
|
wenzelm@10729
|
271 |
|
wenzelm@28083
|
272 |
fun check_rule ctxt cs params ((binding, att), rule) =
|
berghofe@5094
|
273 |
let
|
wenzelm@30222
|
274 |
val err_name = Binding.str_of binding;
|
berghofe@21024
|
275 |
val params' = Term.variant_frees rule (Logic.strip_params rule);
|
berghofe@21024
|
276 |
val frees = rev (map Free params');
|
berghofe@21024
|
277 |
val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
|
berghofe@21024
|
278 |
val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
|
berghofe@23762
|
279 |
val rule' = Logic.list_implies (prems, concl);
|
berghofe@23762
|
280 |
val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems;
|
berghofe@21024
|
281 |
val arule = list_all_free (params', Logic.list_implies (aprems, concl));
|
berghofe@21024
|
282 |
|
berghofe@21024
|
283 |
fun check_ind err t = case dest_predicate cs params t of
|
berghofe@21024
|
284 |
NONE => err (bad_app ^
|
wenzelm@24920
|
285 |
commas (map (Syntax.string_of_term ctxt) params))
|
berghofe@21024
|
286 |
| SOME (_, _, ys, _) =>
|
berghofe@21024
|
287 |
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
|
berghofe@21024
|
288 |
then err bad_ind_occ else ();
|
berghofe@21024
|
289 |
|
berghofe@21024
|
290 |
fun check_prem' prem t =
|
berghofe@21024
|
291 |
if head_of t mem cs then
|
haftmann@28999
|
292 |
check_ind (err_in_prem ctxt err_name rule prem) t
|
berghofe@21024
|
293 |
else (case t of
|
berghofe@21024
|
294 |
Abs (_, _, t) => check_prem' prem t
|
berghofe@21024
|
295 |
| t $ u => (check_prem' prem t; check_prem' prem u)
|
berghofe@21024
|
296 |
| _ => ());
|
berghofe@5094
|
297 |
|
wenzelm@10729
|
298 |
fun check_prem (prem, aprem) =
|
berghofe@21024
|
299 |
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
|
haftmann@28999
|
300 |
else err_in_prem ctxt err_name rule prem "Non-atomic premise";
|
wenzelm@10729
|
301 |
in
|
paulson@11358
|
302 |
(case concl of
|
wenzelm@35364
|
303 |
Const (@{const_name Trueprop}, _) $ t =>
|
berghofe@21024
|
304 |
if head_of t mem cs then
|
haftmann@28999
|
305 |
(check_ind (err_in_rule ctxt err_name rule') t;
|
berghofe@21024
|
306 |
List.app check_prem (prems ~~ aprems))
|
haftmann@28999
|
307 |
else err_in_rule ctxt err_name rule' bad_concl
|
haftmann@28999
|
308 |
| _ => err_in_rule ctxt err_name rule' bad_concl);
|
wenzelm@28083
|
309 |
((binding, att), arule)
|
berghofe@5094
|
310 |
end;
|
berghofe@5094
|
311 |
|
berghofe@24744
|
312 |
val rulify =
|
wenzelm@18222
|
313 |
hol_simplify inductive_conj
|
wenzelm@18463
|
314 |
#> hol_simplify inductive_rulify
|
wenzelm@18463
|
315 |
#> hol_simplify inductive_rulify_fallback
|
wenzelm@30554
|
316 |
#> Simplifier.norm_hhf;
|
wenzelm@10729
|
317 |
|
wenzelm@10729
|
318 |
end;
|
wenzelm@10729
|
319 |
|
wenzelm@10729
|
320 |
|
berghofe@5094
|
321 |
|
berghofe@21024
|
322 |
(** proofs for (co)inductive predicates **)
|
wenzelm@6424
|
323 |
|
berghofe@26534
|
324 |
(* prove monotonicity *)
|
berghofe@5094
|
325 |
|
wenzelm@29412
|
326 |
fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
|
wenzelm@29412
|
327 |
(message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
|
berghofe@26534
|
328 |
" Proving monotonicity ...";
|
wenzelm@32970
|
329 |
(if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
|
wenzelm@29412
|
330 |
[] []
|
wenzelm@17985
|
331 |
(HOLogic.mk_Trueprop
|
wenzelm@24815
|
332 |
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
|
wenzelm@25380
|
333 |
(fn _ => EVERY [rtac @{thm monoI} 1,
|
haftmann@32652
|
334 |
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
|
berghofe@21024
|
335 |
REPEAT (FIRST
|
berghofe@21024
|
336 |
[atac 1,
|
berghofe@33899
|
337 |
resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
|
haftmann@32652
|
338 |
etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
|
berghofe@5094
|
339 |
|
berghofe@5094
|
340 |
|
wenzelm@10735
|
341 |
(* prove introduction rules *)
|
berghofe@5094
|
342 |
|
wenzelm@26477
|
343 |
fun prove_intrs quiet_mode coind mono fp_def k params intr_ts rec_preds_defs ctxt =
|
berghofe@5094
|
344 |
let
|
wenzelm@26477
|
345 |
val _ = clean_message quiet_mode " Proving the introduction rules ...";
|
berghofe@5094
|
346 |
|
berghofe@21024
|
347 |
val unfold = funpow k (fn th => th RS fun_cong)
|
berghofe@21024
|
348 |
(mono RS (fp_def RS
|
haftmann@32652
|
349 |
(if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
|
berghofe@5094
|
350 |
|
berghofe@5094
|
351 |
fun select_disj 1 1 = []
|
berghofe@5094
|
352 |
| select_disj _ 1 = [rtac disjI1]
|
berghofe@5094
|
353 |
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
|
berghofe@5094
|
354 |
|
berghofe@21024
|
355 |
val rules = [refl, TrueI, notFalseI, exI, conjI];
|
berghofe@21024
|
356 |
|
berghofe@22605
|
357 |
val intrs = map_index (fn (i, intr) => rulify
|
wenzelm@32970
|
358 |
(Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
|
berghofe@21024
|
359 |
[rewrite_goals_tac rec_preds_defs,
|
berghofe@21024
|
360 |
rtac (unfold RS iffD2) 1,
|
berghofe@21024
|
361 |
EVERY1 (select_disj (length intr_ts) (i + 1)),
|
wenzelm@17985
|
362 |
(*Not ares_tac, since refl must be tried before any equality assumptions;
|
wenzelm@17985
|
363 |
backtracking may occur if the premises have extra variables!*)
|
berghofe@21024
|
364 |
DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]))) intr_ts
|
berghofe@5094
|
365 |
|
berghofe@5094
|
366 |
in (intrs, unfold) end;
|
berghofe@5094
|
367 |
|
wenzelm@6424
|
368 |
|
wenzelm@10735
|
369 |
(* prove elimination rules *)
|
berghofe@5094
|
370 |
|
wenzelm@26477
|
371 |
fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt =
|
berghofe@5094
|
372 |
let
|
wenzelm@26477
|
373 |
val _ = clean_message quiet_mode " Proving the elimination rules ...";
|
berghofe@5094
|
374 |
|
berghofe@22605
|
375 |
val ([pname], ctxt') = ctxt |>
|
berghofe@22605
|
376 |
Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
|
berghofe@22605
|
377 |
Variable.variant_fixes ["P"];
|
berghofe@21024
|
378 |
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
|
berghofe@21024
|
379 |
|
berghofe@21024
|
380 |
fun dest_intr r =
|
berghofe@21024
|
381 |
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
|
berghofe@21024
|
382 |
Logic.strip_assums_hyp r, Logic.strip_params r);
|
berghofe@21024
|
383 |
|
berghofe@21024
|
384 |
val intrs = map dest_intr intr_ts ~~ intr_names;
|
berghofe@21024
|
385 |
|
berghofe@21024
|
386 |
val rules1 = [disjE, exE, FalseE];
|
berghofe@21024
|
387 |
val rules2 = [conjE, FalseE, notTrueE];
|
berghofe@21024
|
388 |
|
berghofe@21024
|
389 |
fun prove_elim c =
|
berghofe@21024
|
390 |
let
|
haftmann@33077
|
391 |
val Ts = arg_types_of (length params) c;
|
berghofe@21024
|
392 |
val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt';
|
berghofe@21024
|
393 |
val frees = map Free (anames ~~ Ts);
|
berghofe@21024
|
394 |
|
berghofe@21024
|
395 |
fun mk_elim_prem ((_, _, us, _), ts, params') =
|
berghofe@21024
|
396 |
list_all (params',
|
berghofe@21024
|
397 |
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq)
|
berghofe@21024
|
398 |
(frees ~~ us) @ ts, P));
|
wenzelm@33325
|
399 |
val c_intrs = filter (equal c o #1 o #1 o #1) intrs;
|
berghofe@21024
|
400 |
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
|
berghofe@21024
|
401 |
map mk_elim_prem (map #1 c_intrs)
|
berghofe@21024
|
402 |
in
|
wenzelm@32970
|
403 |
(Skip_Proof.prove ctxt'' [] prems P
|
berghofe@21024
|
404 |
(fn {prems, ...} => EVERY
|
berghofe@21024
|
405 |
[cut_facts_tac [hd prems] 1,
|
berghofe@21024
|
406 |
rewrite_goals_tac rec_preds_defs,
|
berghofe@21024
|
407 |
dtac (unfold RS iffD1) 1,
|
berghofe@21024
|
408 |
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
|
berghofe@21024
|
409 |
REPEAT (FIRSTGOAL (eresolve_tac rules2)),
|
berghofe@21024
|
410 |
EVERY (map (fn prem =>
|
berghofe@21024
|
411 |
DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
|
berghofe@21024
|
412 |
|> rulify
|
berghofe@21048
|
413 |
|> singleton (ProofContext.export ctxt'' ctxt),
|
berghofe@34973
|
414 |
map #2 c_intrs, length Ts)
|
berghofe@21024
|
415 |
end
|
berghofe@21024
|
416 |
|
berghofe@21024
|
417 |
in map prove_elim cs end;
|
berghofe@5094
|
418 |
|
wenzelm@6424
|
419 |
|
wenzelm@10735
|
420 |
(* derivation of simplified elimination rules *)
|
berghofe@5094
|
421 |
|
wenzelm@11682
|
422 |
local
|
wenzelm@11682
|
423 |
|
wenzelm@11682
|
424 |
(*delete needless equality assumptions*)
|
wenzelm@29064
|
425 |
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
|
haftmann@22838
|
426 |
(fn _ => assume_tac 1);
|
berghofe@21024
|
427 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
|
wenzelm@11682
|
428 |
val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
|
wenzelm@11682
|
429 |
|
berghofe@23762
|
430 |
fun simp_case_tac ss i =
|
berghofe@23762
|
431 |
EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i;
|
wenzelm@21367
|
432 |
|
wenzelm@11682
|
433 |
in
|
wenzelm@9598
|
434 |
|
wenzelm@21367
|
435 |
fun mk_cases ctxt prop =
|
wenzelm@7107
|
436 |
let
|
wenzelm@21367
|
437 |
val thy = ProofContext.theory_of ctxt;
|
wenzelm@32149
|
438 |
val ss = simpset_of ctxt;
|
wenzelm@21367
|
439 |
|
wenzelm@21526
|
440 |
fun err msg =
|
wenzelm@21526
|
441 |
error (Pretty.string_of (Pretty.block
|
wenzelm@24920
|
442 |
[Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
|
wenzelm@21526
|
443 |
|
wenzelm@24861
|
444 |
val elims = Induct.find_casesP ctxt prop;
|
wenzelm@21367
|
445 |
|
wenzelm@21367
|
446 |
val cprop = Thm.cterm_of thy prop;
|
berghofe@23762
|
447 |
val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac;
|
wenzelm@21367
|
448 |
fun mk_elim rl =
|
wenzelm@21367
|
449 |
Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl))
|
wenzelm@21367
|
450 |
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt);
|
wenzelm@7107
|
451 |
in
|
wenzelm@7107
|
452 |
(case get_first (try mk_elim) elims of
|
skalberg@15531
|
453 |
SOME r => r
|
wenzelm@21526
|
454 |
| NONE => err "Proposition not an inductive predicate:")
|
wenzelm@7107
|
455 |
end;
|
wenzelm@7107
|
456 |
|
wenzelm@11682
|
457 |
end;
|
wenzelm@11682
|
458 |
|
wenzelm@7107
|
459 |
|
wenzelm@21367
|
460 |
(* inductive_cases *)
|
wenzelm@7107
|
461 |
|
wenzelm@21367
|
462 |
fun gen_inductive_cases prep_att prep_prop args lthy =
|
wenzelm@9598
|
463 |
let
|
wenzelm@21367
|
464 |
val thy = ProofContext.theory_of lthy;
|
wenzelm@21367
|
465 |
val facts = args |> map (fn ((a, atts), props) =>
|
wenzelm@21367
|
466 |
((a, map (prep_att thy) atts),
|
wenzelm@21367
|
467 |
map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
|
wenzelm@33673
|
468 |
in lthy |> Local_Theory.notes facts |>> map snd end;
|
wenzelm@12609
|
469 |
|
wenzelm@24509
|
470 |
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
|
wenzelm@24509
|
471 |
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
|
wenzelm@7107
|
472 |
|
wenzelm@6424
|
473 |
|
wenzelm@30722
|
474 |
val ind_cases_setup =
|
wenzelm@30722
|
475 |
Method.setup @{binding ind_cases}
|
wenzelm@30722
|
476 |
(Scan.lift (Scan.repeat1 Args.name_source --
|
wenzelm@30722
|
477 |
Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
|
wenzelm@30722
|
478 |
(fn (raw_props, fixes) => fn ctxt =>
|
wenzelm@30722
|
479 |
let
|
wenzelm@30722
|
480 |
val (_, ctxt') = Variable.add_fixes fixes ctxt;
|
wenzelm@30722
|
481 |
val props = Syntax.read_props ctxt' raw_props;
|
wenzelm@30722
|
482 |
val ctxt'' = fold Variable.declare_term props ctxt';
|
wenzelm@30722
|
483 |
val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
|
wenzelm@30722
|
484 |
in Method.erule 0 rules end))
|
wenzelm@30722
|
485 |
"dynamic case analysis on predicates";
|
wenzelm@9598
|
486 |
|
wenzelm@9598
|
487 |
|
wenzelm@10735
|
488 |
(* prove induction rule *)
|
berghofe@5094
|
489 |
|
wenzelm@26477
|
490 |
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
|
berghofe@21024
|
491 |
fp_def rec_preds_defs ctxt =
|
berghofe@5094
|
492 |
let
|
wenzelm@26477
|
493 |
val _ = clean_message quiet_mode " Proving the induction rule ...";
|
wenzelm@20047
|
494 |
val thy = ProofContext.theory_of ctxt;
|
berghofe@5094
|
495 |
|
berghofe@21024
|
496 |
(* predicates for induction rule *)
|
berghofe@7293
|
497 |
|
berghofe@22605
|
498 |
val (pnames, ctxt') = ctxt |>
|
berghofe@22605
|
499 |
Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
|
berghofe@22605
|
500 |
Variable.variant_fixes (mk_names "P" (length cs));
|
haftmann@33077
|
501 |
val preds = map2 (curry Free) pnames
|
haftmann@33077
|
502 |
(map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
|
berghofe@21024
|
503 |
|
berghofe@21024
|
504 |
(* transform an introduction rule into a premise for induction rule *)
|
berghofe@21024
|
505 |
|
berghofe@21024
|
506 |
fun mk_ind_prem r =
|
berghofe@21024
|
507 |
let
|
wenzelm@33671
|
508 |
fun subst s =
|
wenzelm@33671
|
509 |
(case dest_predicate cs params s of
|
berghofe@21024
|
510 |
SOME (_, i, ys, (_, Ts)) =>
|
berghofe@21024
|
511 |
let
|
berghofe@21024
|
512 |
val k = length Ts;
|
berghofe@21024
|
513 |
val bs = map Bound (k - 1 downto 0);
|
berghofe@23762
|
514 |
val P = list_comb (List.nth (preds, i),
|
berghofe@23762
|
515 |
map (incr_boundvars k) ys @ bs);
|
berghofe@21024
|
516 |
val Q = list_abs (mk_names "x" k ~~ Ts,
|
berghofe@23762
|
517 |
HOLogic.mk_binop inductive_conj_name
|
berghofe@23762
|
518 |
(list_comb (incr_boundvars k s, bs), P))
|
berghofe@21024
|
519 |
in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end
|
wenzelm@33671
|
520 |
| NONE =>
|
wenzelm@33671
|
521 |
(case s of
|
wenzelm@33671
|
522 |
(t $ u) => (fst (subst t) $ fst (subst u), NONE)
|
wenzelm@33671
|
523 |
| (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
|
wenzelm@33671
|
524 |
| _ => (s, NONE)));
|
berghofe@21024
|
525 |
|
wenzelm@33345
|
526 |
fun mk_prem s prems =
|
wenzelm@33345
|
527 |
(case subst s of
|
wenzelm@33345
|
528 |
(_, SOME (t, u)) => t :: u :: prems
|
wenzelm@33345
|
529 |
| (t, _) => t :: prems);
|
berghofe@21024
|
530 |
|
berghofe@21024
|
531 |
val SOME (_, i, ys, _) = dest_predicate cs params
|
berghofe@21024
|
532 |
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
|
berghofe@21024
|
533 |
|
berghofe@21024
|
534 |
in list_all_free (Logic.strip_params r,
|
wenzelm@33345
|
535 |
Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
|
wenzelm@33345
|
536 |
(map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
|
berghofe@21024
|
537 |
HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
|
berghofe@21024
|
538 |
end;
|
berghofe@21024
|
539 |
|
berghofe@21024
|
540 |
val ind_prems = map mk_ind_prem intr_ts;
|
berghofe@21024
|
541 |
|
wenzelm@21526
|
542 |
|
berghofe@21024
|
543 |
(* make conclusions for induction rules *)
|
berghofe@21024
|
544 |
|
berghofe@21024
|
545 |
val Tss = map (binder_types o fastype_of) preds;
|
berghofe@21024
|
546 |
val (xnames, ctxt'') =
|
berghofe@21024
|
547 |
Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt';
|
berghofe@21024
|
548 |
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
berghofe@21024
|
549 |
(map (fn (((xnames, Ts), c), P) =>
|
berghofe@21024
|
550 |
let val frees = map Free (xnames ~~ Ts)
|
berghofe@21024
|
551 |
in HOLogic.mk_imp
|
berghofe@21024
|
552 |
(list_comb (c, params @ frees), list_comb (P, frees))
|
berghofe@21024
|
553 |
end) (unflat Tss xnames ~~ Tss ~~ cs ~~ preds)));
|
berghofe@5094
|
554 |
|
paulson@13626
|
555 |
|
berghofe@5094
|
556 |
(* make predicate for instantiation of abstract induction rule *)
|
berghofe@5094
|
557 |
|
berghofe@21024
|
558 |
val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
|
wenzelm@33345
|
559 |
(map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
|
wenzelm@33345
|
560 |
(make_bool_args HOLogic.mk_not I bs i)
|
wenzelm@33345
|
561 |
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
|
berghofe@5094
|
562 |
|
berghofe@5094
|
563 |
val ind_concl = HOLogic.mk_Trueprop
|
haftmann@35092
|
564 |
(HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
|
berghofe@5094
|
565 |
|
haftmann@32652
|
566 |
val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
|
paulson@13626
|
567 |
|
wenzelm@32970
|
568 |
val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
|
wenzelm@20248
|
569 |
(fn {prems, ...} => EVERY
|
wenzelm@17985
|
570 |
[rewrite_goals_tac [inductive_conj_def],
|
berghofe@21024
|
571 |
DETERM (rtac raw_fp_induct 1),
|
haftmann@32652
|
572 |
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
|
haftmann@32610
|
573 |
rewrite_goals_tac simp_thms'',
|
berghofe@21024
|
574 |
(*This disjE separates out the introduction rules*)
|
berghofe@21024
|
575 |
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
|
berghofe@5094
|
576 |
(*Now break down the individual cases. No disjE here in case
|
berghofe@5094
|
577 |
some premise involves disjunction.*)
|
paulson@13747
|
578 |
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
|
berghofe@21024
|
579 |
REPEAT (FIRSTGOAL
|
berghofe@21024
|
580 |
(resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
|
berghofe@21024
|
581 |
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
|
haftmann@32610
|
582 |
(inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
|
berghofe@22980
|
583 |
conjI, refl] 1)) prems)]);
|
berghofe@5094
|
584 |
|
wenzelm@32970
|
585 |
val lemma = Skip_Proof.prove ctxt'' [] []
|
wenzelm@17985
|
586 |
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
|
berghofe@21024
|
587 |
[rewrite_goals_tac rec_preds_defs,
|
berghofe@5094
|
588 |
REPEAT (EVERY
|
berghofe@5094
|
589 |
[REPEAT (resolve_tac [conjI, impI] 1),
|
haftmann@32652
|
590 |
REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
|
berghofe@21024
|
591 |
atac 1,
|
berghofe@21024
|
592 |
rewrite_goals_tac simp_thms',
|
berghofe@21024
|
593 |
atac 1])])
|
berghofe@5094
|
594 |
|
berghofe@21024
|
595 |
in singleton (ProofContext.export ctxt'' ctxt) (induct RS lemma) end;
|
berghofe@5094
|
596 |
|
wenzelm@6424
|
597 |
|
wenzelm@6424
|
598 |
|
berghofe@21024
|
599 |
(** specification of (co)inductive predicates **)
|
berghofe@5094
|
600 |
|
wenzelm@33464
|
601 |
fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind
|
wenzelm@33464
|
602 |
cs intr_ts monos params cnames_syn lthy =
|
wenzelm@33464
|
603 |
let
|
haftmann@24915
|
604 |
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
|
berghofe@5094
|
605 |
|
haftmann@33077
|
606 |
val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
|
berghofe@21024
|
607 |
val k = log 2 1 (length cs);
|
berghofe@21024
|
608 |
val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
|
wenzelm@33464
|
609 |
val p :: xs = map Free (Variable.variant_frees lthy intr_ts
|
berghofe@21024
|
610 |
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs)));
|
wenzelm@33464
|
611 |
val bs = map Free (Variable.variant_frees lthy (p :: xs @ intr_ts)
|
berghofe@21024
|
612 |
(map (rpair HOLogic.boolT) (mk_names "b" k)));
|
berghofe@21024
|
613 |
|
wenzelm@33464
|
614 |
fun subst t =
|
wenzelm@33464
|
615 |
(case dest_predicate cs params t of
|
berghofe@21024
|
616 |
SOME (_, i, ts, (Ts, Us)) =>
|
berghofe@23762
|
617 |
let
|
berghofe@23762
|
618 |
val l = length Us;
|
wenzelm@33671
|
619 |
val zs = map Bound (l - 1 downto 0);
|
berghofe@21024
|
620 |
in
|
berghofe@21024
|
621 |
list_abs (map (pair "z") Us, list_comb (p,
|
berghofe@23762
|
622 |
make_bool_args' bs i @ make_args argTs
|
berghofe@23762
|
623 |
((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us))))
|
berghofe@21024
|
624 |
end
|
wenzelm@33671
|
625 |
| NONE =>
|
wenzelm@33671
|
626 |
(case t of
|
wenzelm@33671
|
627 |
t1 $ t2 => subst t1 $ subst t2
|
wenzelm@33671
|
628 |
| Abs (x, T, u) => Abs (x, T, subst u)
|
wenzelm@33671
|
629 |
| _ => t));
|
berghofe@5149
|
630 |
|
berghofe@5094
|
631 |
(* transform an introduction rule into a conjunction *)
|
berghofe@21024
|
632 |
(* [| p_i t; ... |] ==> p_j u *)
|
berghofe@5094
|
633 |
(* is transformed into *)
|
berghofe@21024
|
634 |
(* b_j & x_j = u & p b_j t & ... *)
|
berghofe@5094
|
635 |
|
berghofe@5094
|
636 |
fun transform_rule r =
|
berghofe@5094
|
637 |
let
|
berghofe@21024
|
638 |
val SOME (_, i, ts, (Ts, _)) = dest_predicate cs params
|
berghofe@21048
|
639 |
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r));
|
berghofe@21048
|
640 |
val ps = make_bool_args HOLogic.mk_not I bs i @
|
berghofe@21048
|
641 |
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
|
berghofe@21048
|
642 |
map (subst o HOLogic.dest_Trueprop)
|
berghofe@21048
|
643 |
(Logic.strip_assums_hyp r)
|
wenzelm@33345
|
644 |
in
|
wenzelm@33345
|
645 |
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
|
wenzelm@33345
|
646 |
(Logic.strip_params r)
|
wenzelm@33345
|
647 |
(if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
|
berghofe@5094
|
648 |
end
|
berghofe@5094
|
649 |
|
berghofe@5094
|
650 |
(* make a disjunction of all introduction rules *)
|
berghofe@5094
|
651 |
|
berghofe@21024
|
652 |
val fp_fun = fold_rev lambda (p :: bs @ xs)
|
berghofe@21024
|
653 |
(if null intr_ts then HOLogic.false_const
|
berghofe@21024
|
654 |
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts));
|
berghofe@5094
|
655 |
|
berghofe@21024
|
656 |
(* add definiton of recursive predicates to theory *)
|
berghofe@5094
|
657 |
|
wenzelm@28083
|
658 |
val rec_name =
|
haftmann@28965
|
659 |
if Binding.is_empty alt_name then
|
wenzelm@30227
|
660 |
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
|
wenzelm@28083
|
661 |
else alt_name;
|
berghofe@5094
|
662 |
|
wenzelm@33464
|
663 |
val ((rec_const, (_, fp_def)), lthy') = lthy
|
wenzelm@33673
|
664 |
|> Local_Theory.conceal
|
wenzelm@33812
|
665 |
|> Local_Theory.define
|
berghofe@21024
|
666 |
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
|
blanchet@33568
|
667 |
((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
|
blanchet@33568
|
668 |
fold_rev lambda params
|
wenzelm@33278
|
669 |
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
|
wenzelm@33673
|
670 |
||> Local_Theory.restore_naming lthy;
|
berghofe@21024
|
671 |
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
|
wenzelm@33464
|
672 |
(cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
|
wenzelm@33278
|
673 |
val specs =
|
wenzelm@33278
|
674 |
if length cs < 2 then []
|
wenzelm@33278
|
675 |
else
|
wenzelm@33278
|
676 |
map_index (fn (i, (name_mx, c)) =>
|
wenzelm@33278
|
677 |
let
|
wenzelm@33278
|
678 |
val Ts = arg_types_of (length params) c;
|
wenzelm@33464
|
679 |
val xs = map Free (Variable.variant_frees lthy intr_ts
|
wenzelm@33278
|
680 |
(mk_names "x" (length Ts) ~~ Ts))
|
wenzelm@33278
|
681 |
in
|
wenzelm@33278
|
682 |
(name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
|
wenzelm@33278
|
683 |
(list_comb (rec_const, params @ make_bool_args' bs i @
|
wenzelm@33278
|
684 |
make_args argTs (xs ~~ Ts)))))
|
wenzelm@33278
|
685 |
end) (cnames_syn ~~ cs);
|
wenzelm@33464
|
686 |
val (consts_defs, lthy'') = lthy'
|
wenzelm@33673
|
687 |
|> Local_Theory.conceal
|
wenzelm@33812
|
688 |
|> fold_map Local_Theory.define specs
|
wenzelm@33673
|
689 |
||> Local_Theory.restore_naming lthy';
|
berghofe@21024
|
690 |
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
|
berghofe@5094
|
691 |
|
wenzelm@33464
|
692 |
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
|
wenzelm@33464
|
693 |
val ((_, [mono']), lthy''') =
|
wenzelm@33673
|
694 |
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
|
berghofe@5094
|
695 |
|
wenzelm@33464
|
696 |
in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
|
berghofe@21024
|
697 |
list_comb (rec_const, params), preds, argTs, bs, xs)
|
berghofe@21024
|
698 |
end;
|
berghofe@5094
|
699 |
|
wenzelm@33671
|
700 |
fun declare_rules rec_binding coind no_ind cnames
|
wenzelm@33671
|
701 |
intrs intr_bindings intr_atts elims raw_induct lthy =
|
berghofe@23762
|
702 |
let
|
wenzelm@30227
|
703 |
val rec_name = Binding.name_of rec_binding;
|
haftmann@32773
|
704 |
fun rec_qualified qualified = Binding.qualify qualified rec_name;
|
wenzelm@30227
|
705 |
val intr_names = map Binding.name_of intr_bindings;
|
wenzelm@33368
|
706 |
val ind_case_names = Rule_Cases.case_names intr_names;
|
berghofe@23762
|
707 |
val induct =
|
berghofe@23762
|
708 |
if coind then
|
wenzelm@33368
|
709 |
(raw_induct, [Rule_Cases.case_names [rec_name],
|
wenzelm@33368
|
710 |
Rule_Cases.case_conclusion (rec_name, intr_names),
|
wenzelm@33368
|
711 |
Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
|
berghofe@23762
|
712 |
else if no_ind orelse length cnames > 1 then
|
wenzelm@33368
|
713 |
(raw_induct, [ind_case_names, Rule_Cases.consumes 0])
|
wenzelm@33368
|
714 |
else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
|
berghofe@23762
|
715 |
|
wenzelm@33464
|
716 |
val (intrs', lthy1) =
|
wenzelm@33464
|
717 |
lthy |>
|
wenzelm@33673
|
718 |
Local_Theory.notes
|
wenzelm@33278
|
719 |
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~
|
wenzelm@33278
|
720 |
map (fn th => [([th],
|
wenzelm@33369
|
721 |
[Attrib.internal (K (Context_Rules.intro_query NONE)),
|
blanchet@33056
|
722 |
Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
|
berghofe@24744
|
723 |
map (hd o snd);
|
wenzelm@33464
|
724 |
val (((_, elims'), (_, [induct'])), lthy2) =
|
wenzelm@33464
|
725 |
lthy1 |>
|
wenzelm@33673
|
726 |
Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
|
berghofe@34973
|
727 |
fold_map (fn (name, (elim, cases, k)) =>
|
wenzelm@33673
|
728 |
Local_Theory.note
|
wenzelm@33464
|
729 |
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
|
wenzelm@33464
|
730 |
[Attrib.internal (K (Rule_Cases.case_names cases)),
|
wenzelm@33464
|
731 |
Attrib.internal (K (Rule_Cases.consumes 1)),
|
berghofe@34973
|
732 |
Attrib.internal (K (Rule_Cases.constraints k)),
|
wenzelm@33464
|
733 |
Attrib.internal (K (Induct.cases_pred name)),
|
wenzelm@33464
|
734 |
Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
|
berghofe@23762
|
735 |
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
|
wenzelm@33673
|
736 |
Local_Theory.note
|
haftmann@32773
|
737 |
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
|
wenzelm@28107
|
738 |
map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
|
berghofe@23762
|
739 |
|
wenzelm@33464
|
740 |
val lthy3 =
|
wenzelm@33464
|
741 |
if no_ind orelse coind then lthy2
|
wenzelm@33464
|
742 |
else
|
wenzelm@33464
|
743 |
let val inducts = cnames ~~ Project_Rule.projects lthy2 (1 upto length cnames) induct' in
|
wenzelm@33464
|
744 |
lthy2 |>
|
wenzelm@33673
|
745 |
Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []),
|
wenzelm@33464
|
746 |
inducts |> map (fn (name, th) => ([th],
|
wenzelm@33464
|
747 |
[Attrib.internal (K ind_case_names),
|
wenzelm@33464
|
748 |
Attrib.internal (K (Rule_Cases.consumes 1)),
|
wenzelm@33464
|
749 |
Attrib.internal (K (Induct.induct_pred name))])))] |> snd
|
wenzelm@33464
|
750 |
end;
|
wenzelm@33464
|
751 |
in (intrs', elims', induct', lthy3) end;
|
berghofe@23762
|
752 |
|
berghofe@26534
|
753 |
type inductive_flags =
|
wenzelm@33671
|
754 |
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
|
wenzelm@33671
|
755 |
no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool};
|
berghofe@26534
|
756 |
|
wenzelm@24815
|
757 |
type add_ind_def =
|
berghofe@26534
|
758 |
inductive_flags ->
|
wenzelm@28084
|
759 |
term list -> (Attrib.binding * term) list -> thm list ->
|
haftmann@29581
|
760 |
term list -> (binding * mixfix) list ->
|
wenzelm@33464
|
761 |
local_theory -> inductive_result * local_theory;
|
berghofe@23762
|
762 |
|
wenzelm@33671
|
763 |
fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
|
wenzelm@33464
|
764 |
cs intros monos params cnames_syn lthy =
|
berghofe@9072
|
765 |
let
|
wenzelm@25288
|
766 |
val _ = null cnames_syn andalso error "No inductive predicates given";
|
wenzelm@30227
|
767 |
val names = map (Binding.name_of o fst) cnames_syn;
|
wenzelm@26477
|
768 |
val _ = message (quiet_mode andalso not verbose)
|
wenzelm@28083
|
769 |
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
|
berghofe@9072
|
770 |
|
wenzelm@33673
|
771 |
val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *)
|
berghofe@23762
|
772 |
val ((intr_names, intr_atts), intr_ts) =
|
wenzelm@33464
|
773 |
apfst split_list (split_list (map (check_rule lthy cs params) intros));
|
berghofe@9072
|
774 |
|
wenzelm@33464
|
775 |
val (lthy1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds,
|
wenzelm@29412
|
776 |
argTs, bs, xs) = mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts
|
wenzelm@33464
|
777 |
monos params cnames_syn lthy;
|
berghofe@9072
|
778 |
|
wenzelm@26477
|
779 |
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
|
wenzelm@33464
|
780 |
params intr_ts rec_preds_defs lthy1;
|
wenzelm@33465
|
781 |
val elims =
|
wenzelm@33465
|
782 |
if no_elim then []
|
wenzelm@33465
|
783 |
else
|
wenzelm@33465
|
784 |
prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
|
wenzelm@33465
|
785 |
unfold rec_preds_defs lthy1;
|
berghofe@22605
|
786 |
val raw_induct = zero_var_indexes
|
wenzelm@33465
|
787 |
(if no_ind then Drule.asm_rl
|
wenzelm@33465
|
788 |
else if coind then
|
berghofe@23762
|
789 |
singleton (ProofContext.export
|
wenzelm@33464
|
790 |
(snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
|
wenzelm@35625
|
791 |
(rotate_prems ~1 (Object_Logic.rulify
|
wenzelm@28839
|
792 |
(fold_rule rec_preds_defs
|
haftmann@32652
|
793 |
(rewrite_rule simp_thms'''
|
haftmann@32652
|
794 |
(mono RS (fp_def RS @{thm def_coinduct}))))))
|
berghofe@21024
|
795 |
else
|
wenzelm@26477
|
796 |
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
|
wenzelm@33464
|
797 |
rec_preds_defs lthy1);
|
berghofe@5094
|
798 |
|
wenzelm@33671
|
799 |
val (intrs', elims', induct, lthy2) = declare_rules rec_name coind no_ind
|
wenzelm@33464
|
800 |
cnames intrs intr_names intr_atts elims raw_induct lthy1;
|
berghofe@21048
|
801 |
|
berghofe@21048
|
802 |
val result =
|
berghofe@21048
|
803 |
{preds = preds,
|
berghofe@21048
|
804 |
intrs = intrs',
|
berghofe@21048
|
805 |
elims = elims',
|
berghofe@21048
|
806 |
raw_induct = rulify raw_induct,
|
berghofe@23762
|
807 |
induct = induct};
|
wenzelm@21367
|
808 |
|
wenzelm@33464
|
809 |
val lthy3 = lthy2
|
wenzelm@33673
|
810 |
|> Local_Theory.declaration false (fn phi =>
|
wenzelm@25380
|
811 |
let val result' = morph_result phi result;
|
wenzelm@25380
|
812 |
in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
|
wenzelm@33464
|
813 |
in (result, lthy3) end;
|
berghofe@5094
|
814 |
|
wenzelm@6424
|
815 |
|
wenzelm@10735
|
816 |
(* external interfaces *)
|
wenzelm@6424
|
817 |
|
wenzelm@26477
|
818 |
fun gen_add_inductive_i mk_def
|
wenzelm@33671
|
819 |
(flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
|
wenzelm@25029
|
820 |
cnames_syn pnames spec monos lthy =
|
berghofe@5094
|
821 |
let
|
wenzelm@25029
|
822 |
val thy = ProofContext.theory_of lthy;
|
wenzelm@6424
|
823 |
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
|
berghofe@5094
|
824 |
|
berghofe@21766
|
825 |
|
wenzelm@25029
|
826 |
(* abbrevs *)
|
berghofe@21766
|
827 |
|
wenzelm@30227
|
828 |
val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;
|
berghofe@21766
|
829 |
|
wenzelm@25029
|
830 |
fun get_abbrev ((name, atts), t) =
|
wenzelm@25029
|
831 |
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
|
wenzelm@25029
|
832 |
let
|
haftmann@28999
|
833 |
val _ = Binding.is_empty name andalso null atts orelse
|
wenzelm@25029
|
834 |
error "Abbreviations may not have names or attributes";
|
wenzelm@35624
|
835 |
val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
|
wenzelm@28083
|
836 |
val var =
|
wenzelm@30227
|
837 |
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
|
wenzelm@25029
|
838 |
NONE => error ("Undeclared head of abbreviation " ^ quote x)
|
wenzelm@28083
|
839 |
| SOME ((b, T'), mx) =>
|
wenzelm@25029
|
840 |
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
|
wenzelm@28083
|
841 |
else (b, mx));
|
wenzelm@28083
|
842 |
in SOME (var, rhs) end
|
wenzelm@25029
|
843 |
else NONE;
|
berghofe@21766
|
844 |
|
wenzelm@25029
|
845 |
val abbrevs = map_filter get_abbrev spec;
|
wenzelm@30227
|
846 |
val bs = map (Binding.name_of o fst o fst) abbrevs;
|
berghofe@21766
|
847 |
|
wenzelm@25029
|
848 |
|
wenzelm@25029
|
849 |
(* predicates *)
|
wenzelm@25029
|
850 |
|
wenzelm@25029
|
851 |
val pre_intros = filter_out (is_some o get_abbrev) spec;
|
wenzelm@30227
|
852 |
val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn;
|
wenzelm@30227
|
853 |
val cs = map (Free o apfst Binding.name_of o fst) cnames_syn';
|
wenzelm@25029
|
854 |
val ps = map Free pnames;
|
berghofe@5094
|
855 |
|
wenzelm@30227
|
856 |
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
|
wenzelm@35624
|
857 |
val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
|
wenzelm@35624
|
858 |
val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
|
wenzelm@25143
|
859 |
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
|
wenzelm@25029
|
860 |
|
wenzelm@25029
|
861 |
fun close_rule r = list_all_free (rev (fold_aterms
|
berghofe@21024
|
862 |
(fn t as Free (v as (s, _)) =>
|
wenzelm@25029
|
863 |
if Variable.is_fixed ctxt1 s orelse
|
wenzelm@25029
|
864 |
member (op =) ps t then I else insert (op =) v
|
wenzelm@25029
|
865 |
| _ => I) r []), r);
|
berghofe@5094
|
866 |
|
haftmann@26736
|
867 |
val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
|
wenzelm@25029
|
868 |
val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
|
berghofe@21048
|
869 |
in
|
wenzelm@25029
|
870 |
lthy
|
wenzelm@25029
|
871 |
|> mk_def flags cs intros monos ps preds
|
wenzelm@33673
|
872 |
||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs
|
berghofe@21048
|
873 |
end;
|
berghofe@5094
|
874 |
|
wenzelm@29412
|
875 |
fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
|
berghofe@5094
|
876 |
let
|
wenzelm@30488
|
877 |
val ((vars, intrs), _) = lthy
|
wenzelm@30488
|
878 |
|> ProofContext.set_mode ProofContext.mode_abbrev
|
wenzelm@30488
|
879 |
|> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
|
wenzelm@24721
|
880 |
val (cs, ps) = chop (length cnames_syn) vars;
|
wenzelm@24721
|
881 |
val monos = Attrib.eval_thms lthy raw_monos;
|
wenzelm@33671
|
882 |
val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
|
wenzelm@33671
|
883 |
coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
|
wenzelm@26128
|
884 |
in
|
wenzelm@26128
|
885 |
lthy
|
wenzelm@30227
|
886 |
|> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
|
wenzelm@26128
|
887 |
end;
|
berghofe@5094
|
888 |
|
berghofe@23762
|
889 |
val add_inductive_i = gen_add_inductive_i add_ind_def;
|
berghofe@23762
|
890 |
val add_inductive = gen_add_inductive add_ind_def;
|
berghofe@23762
|
891 |
|
wenzelm@33736
|
892 |
fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
|
wenzelm@25380
|
893 |
let
|
haftmann@28999
|
894 |
val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
|
wenzelm@25380
|
895 |
val ctxt' = thy
|
wenzelm@33595
|
896 |
|> Theory_Target.init NONE
|
wenzelm@25380
|
897 |
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
|
wenzelm@33673
|
898 |
|> Local_Theory.exit;
|
wenzelm@25380
|
899 |
val info = #2 (the_inductive ctxt' name);
|
wenzelm@25380
|
900 |
in (info, ProofContext.theory_of ctxt') end;
|
wenzelm@6424
|
901 |
|
wenzelm@6424
|
902 |
|
berghofe@22789
|
903 |
(* read off arities of inductive predicates from raw induction rule *)
|
berghofe@22789
|
904 |
fun arities_of induct =
|
berghofe@22789
|
905 |
map (fn (_ $ t $ u) =>
|
berghofe@22789
|
906 |
(fst (dest_Const (head_of t)), length (snd (strip_comb u))))
|
berghofe@22789
|
907 |
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
|
berghofe@22789
|
908 |
|
berghofe@22789
|
909 |
(* read off parameters of inductive predicate from raw induction rule *)
|
berghofe@22789
|
910 |
fun params_of induct =
|
berghofe@22789
|
911 |
let
|
berghofe@22789
|
912 |
val (_ $ t $ u :: _) =
|
berghofe@22789
|
913 |
HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct));
|
berghofe@22789
|
914 |
val (_, ts) = strip_comb t;
|
berghofe@22789
|
915 |
val (_, us) = strip_comb u
|
berghofe@22789
|
916 |
in
|
berghofe@22789
|
917 |
List.take (ts, length ts - length us)
|
berghofe@22789
|
918 |
end;
|
berghofe@22789
|
919 |
|
berghofe@22789
|
920 |
val pname_of_intr =
|
berghofe@22789
|
921 |
concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst;
|
berghofe@22789
|
922 |
|
berghofe@22789
|
923 |
(* partition introduction rules according to predicate name *)
|
berghofe@25822
|
924 |
fun gen_partition_rules f induct intros =
|
berghofe@25822
|
925 |
fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros
|
berghofe@22789
|
926 |
(map (rpair [] o fst) (arities_of induct));
|
berghofe@22789
|
927 |
|
berghofe@25822
|
928 |
val partition_rules = gen_partition_rules I;
|
berghofe@25822
|
929 |
fun partition_rules' induct = gen_partition_rules fst induct;
|
berghofe@25822
|
930 |
|
berghofe@22789
|
931 |
fun unpartition_rules intros xs =
|
berghofe@22789
|
932 |
fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r)
|
berghofe@22789
|
933 |
(fn x :: xs => (x, xs)) #>> the) intros xs |> fst;
|
berghofe@22789
|
934 |
|
berghofe@22789
|
935 |
(* infer order of variables in intro rules from order of quantifiers in elim rule *)
|
berghofe@22789
|
936 |
fun infer_intro_vars elim arity intros =
|
berghofe@22789
|
937 |
let
|
berghofe@22789
|
938 |
val thy = theory_of_thm elim;
|
berghofe@22789
|
939 |
val _ :: cases = prems_of elim;
|
berghofe@22789
|
940 |
val used = map (fst o fst) (Term.add_vars (prop_of elim) []);
|
berghofe@22789
|
941 |
fun mtch (t, u) =
|
berghofe@22789
|
942 |
let
|
berghofe@22789
|
943 |
val params = Logic.strip_params t;
|
berghofe@22789
|
944 |
val vars = map (Var o apfst (rpair 0))
|
berghofe@22789
|
945 |
(Name.variant_list used (map fst params) ~~ map snd params);
|
berghofe@22789
|
946 |
val ts = map (curry subst_bounds (rev vars))
|
berghofe@22789
|
947 |
(List.drop (Logic.strip_assums_hyp t, arity));
|
berghofe@22789
|
948 |
val us = Logic.strip_imp_prems u;
|
berghofe@22789
|
949 |
val tab = fold (Pattern.first_order_match thy) (ts ~~ us)
|
berghofe@22789
|
950 |
(Vartab.empty, Vartab.empty);
|
berghofe@22789
|
951 |
in
|
wenzelm@32046
|
952 |
map (Envir.subst_term tab) vars
|
berghofe@22789
|
953 |
end
|
berghofe@22789
|
954 |
in
|
berghofe@22789
|
955 |
map (mtch o apsnd prop_of) (cases ~~ intros)
|
berghofe@22789
|
956 |
end;
|
berghofe@22789
|
957 |
|
berghofe@22789
|
958 |
|
wenzelm@25978
|
959 |
|
wenzelm@6437
|
960 |
(** package setup **)
|
wenzelm@6437
|
961 |
|
wenzelm@6437
|
962 |
(* setup theory *)
|
wenzelm@6437
|
963 |
|
wenzelm@8634
|
964 |
val setup =
|
wenzelm@30722
|
965 |
ind_cases_setup #>
|
wenzelm@30530
|
966 |
Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
|
wenzelm@30530
|
967 |
"declaration of monotonicity rule";
|
wenzelm@6437
|
968 |
|
wenzelm@6437
|
969 |
|
wenzelm@6437
|
970 |
(* outer syntax *)
|
wenzelm@6424
|
971 |
|
wenzelm@17057
|
972 |
local structure P = OuterParse and K = OuterKeyword in
|
wenzelm@6424
|
973 |
|
wenzelm@27353
|
974 |
val _ = OuterKeyword.keyword "monos";
|
wenzelm@24867
|
975 |
|
berghofe@23762
|
976 |
fun gen_ind_decl mk_def coind =
|
wenzelm@21367
|
977 |
P.fixes -- P.for_fixes --
|
wenzelm@30488
|
978 |
Scan.optional SpecParse.where_alt_specs [] --
|
wenzelm@22102
|
979 |
Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) []
|
wenzelm@26988
|
980 |
>> (fn (((preds, params), specs), monos) =>
|
wenzelm@30488
|
981 |
(snd oo gen_add_inductive mk_def true coind preds params specs monos));
|
berghofe@23762
|
982 |
|
berghofe@23762
|
983 |
val ind_decl = gen_ind_decl add_ind_def;
|
wenzelm@6424
|
984 |
|
wenzelm@33464
|
985 |
val _ =
|
wenzelm@33464
|
986 |
OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
|
wenzelm@33464
|
987 |
(ind_decl false);
|
wenzelm@33464
|
988 |
|
wenzelm@33464
|
989 |
val _ =
|
wenzelm@33464
|
990 |
OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
|
wenzelm@33464
|
991 |
(ind_decl true);
|
wenzelm@6723
|
992 |
|
wenzelm@24867
|
993 |
val _ =
|
wenzelm@26988
|
994 |
OuterSyntax.local_theory "inductive_cases"
|
wenzelm@21367
|
995 |
"create simplified instances of elimination rules (improper)" K.thy_script
|
wenzelm@30488
|
996 |
(P.and_list1 SpecParse.specs >> (snd oo inductive_cases));
|
wenzelm@7107
|
997 |
|
berghofe@5094
|
998 |
end;
|
wenzelm@6424
|
999 |
|
wenzelm@6424
|
1000 |
end;
|