author | traytel |
Tue, 03 Mar 2015 19:08:04 +0100 | |
changeset 59580 | cbc38731d42f |
parent 59532 | 82ab8168d940 |
child 59582 | 0fbed69ff081 |
permissions | -rw-r--r-- |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
1 |
(* Title: HOL/Tools/inductive.ML |
5094 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
3 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
5094 | 4 |
|
6424 | 5 |
(Co)Inductive Definition module for HOL. |
5094 | 6 |
|
7 |
Features: |
|
6424 | 8 |
* least or greatest fixedpoints |
9 |
* mutually recursive definitions |
|
10 |
* definitions involving arbitrary monotone operators |
|
11 |
* automatically proves introduction and elimination rules |
|
5094 | 12 |
|
13 |
Introduction rules have the form |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
14 |
[| M Pj ti, ..., Q x, ... |] ==> Pk t |
5094 | 15 |
where M is some monotone operator (usually the identity) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
16 |
Q x is any side condition on the free variables |
5094 | 17 |
ti, t are any terms |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
18 |
Pj, Pk are two of the predicates being defined in mutual recursion |
5094 | 19 |
*) |
20 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
21 |
signature BASIC_INDUCTIVE = |
5094 | 22 |
sig |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
23 |
type inductive_result = |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
24 |
{preds: term list, elims: thm list, raw_induct: thm, |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
25 |
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list} |
45290 | 26 |
val transform_result: morphism -> inductive_result -> inductive_result |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
27 |
type inductive_info = {names: string list, coind: bool} * inductive_result |
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
28 |
val the_inductive: Proof.context -> string -> inductive_info |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
29 |
val print_inductives: Proof.context -> unit |
45651 | 30 |
val get_monos: Proof.context -> thm list |
18728 | 31 |
val mono_add: attribute |
32 |
val mono_del: attribute |
|
53994 | 33 |
val mk_cases_tac: Proof.context -> tactic |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
34 |
val mk_cases: Proof.context -> term -> thm |
10910
058775a575db
export inductive_forall_name, inductive_forall_def, rulify;
wenzelm
parents:
10804
diff
changeset
|
35 |
val inductive_forall_def: thm |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
36 |
val rulify: Proof.context -> thm -> thm |
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents:
28791
diff
changeset
|
37 |
val inductive_cases: (Attrib.binding * string list) list -> local_theory -> |
53995 | 38 |
(string * thm list) list * local_theory |
28839
32d498cf7595
eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
wenzelm
parents:
28791
diff
changeset
|
39 |
val inductive_cases_i: (Attrib.binding * term list) list -> local_theory -> |
53995 | 40 |
(string * thm list) list * local_theory |
41 |
val inductive_simps: (Attrib.binding * string list) list -> local_theory -> |
|
42 |
(string * thm list) list * local_theory |
|
43 |
val inductive_simps_i: (Attrib.binding * term list) list -> local_theory -> |
|
44 |
(string * thm list) list * local_theory |
|
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
45 |
type inductive_flags = |
33669 | 46 |
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, |
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
47 |
no_elim: bool, no_ind: bool, skip_mono: bool} |
24815
f7093e90f36c
tuned internal interfaces: flags record, added kind for results;
wenzelm
parents:
24744
diff
changeset
|
48 |
val add_inductive_i: |
29581 | 49 |
inductive_flags -> ((binding * typ) * mixfix) list -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
50 |
(string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory -> |
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
51 |
inductive_result * local_theory |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
52 |
val add_inductive: bool -> bool -> |
29581 | 53 |
(binding * string option * mixfix) list -> |
54 |
(binding * string option * mixfix) list -> |
|
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
55 |
(Attrib.binding * string) list -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
56 |
(Facts.ref * Token.src list) list -> |
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
57 |
local_theory -> inductive_result * local_theory |
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
58 |
val add_inductive_global: inductive_flags -> |
29581 | 59 |
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
60 |
thm list -> theory -> inductive_result * theory |
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
61 |
val arities_of: thm -> (string * int) list |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
62 |
val params_of: thm -> term list |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
63 |
val partition_rules: thm -> thm list -> (string * thm list) list |
25822 | 64 |
val partition_rules': thm -> (thm * 'a) list -> (string * (thm * 'a) list) list |
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
65 |
val unpartition_rules: thm list -> (string * 'a list) list -> 'a list |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
66 |
val infer_intro_vars: thm -> int -> thm list -> term list list |
5094 | 67 |
end; |
68 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
69 |
signature INDUCTIVE = |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
70 |
sig |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
71 |
include BASIC_INDUCTIVE |
59532 | 72 |
val select_disj_tac: Proof.context -> int -> int -> int -> tactic |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
73 |
type add_ind_def = |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
74 |
inductive_flags -> |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
75 |
term list -> (Attrib.binding * term) list -> thm list -> |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
76 |
term list -> (binding * mixfix) list -> |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
77 |
local_theory -> inductive_result * local_theory |
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset
|
78 |
val declare_rules: binding -> bool -> bool -> string list -> term list -> |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
79 |
thm list -> binding list -> Token.src list list -> (thm * string list * int) list -> |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
80 |
thm list -> thm -> local_theory -> thm list * thm list * thm list * thm * thm list * local_theory |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
81 |
val add_ind_def: add_ind_def |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
82 |
val gen_add_inductive_i: add_ind_def -> inductive_flags -> |
29581 | 83 |
((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list -> |
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
84 |
thm list -> local_theory -> inductive_result * local_theory |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
85 |
val gen_add_inductive: add_ind_def -> bool -> bool -> |
29581 | 86 |
(binding * string option * mixfix) list -> |
87 |
(binding * string option * mixfix) list -> |
|
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56334
diff
changeset
|
88 |
(Attrib.binding * string) list -> (Facts.ref * Token.src list) list -> |
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
89 |
local_theory -> inductive_result * local_theory |
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
90 |
val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
91 |
end; |
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
92 |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
93 |
structure Inductive: INDUCTIVE = |
5094 | 94 |
struct |
95 |
||
10729 | 96 |
(** theory context references **) |
97 |
||
32602 | 98 |
val inductive_forall_def = @{thm induct_forall_def}; |
11991 | 99 |
val inductive_conj_name = "HOL.induct_conj"; |
32602 | 100 |
val inductive_conj_def = @{thm induct_conj_def}; |
101 |
val inductive_conj = @{thms induct_conj}; |
|
102 |
val inductive_atomize = @{thms induct_atomize}; |
|
103 |
val inductive_rulify = @{thms induct_rulify}; |
|
104 |
val inductive_rulify_fallback = @{thms induct_rulify_fallback}; |
|
10729 | 105 |
|
45649 | 106 |
val simp_thms1 = |
107 |
map mk_meta_eq |
|
108 |
@{lemma "(~ True) = False" "(~ False) = True" |
|
109 |
"(True --> P) = P" "(False --> P) = True" |
|
110 |
"(P & True) = P" "(True & P) = P" |
|
111 |
by (fact simp_thms)+}; |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
112 |
|
45649 | 113 |
val simp_thms2 = |
114 |
map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1; |
|
32652 | 115 |
|
45649 | 116 |
val simp_thms3 = |
117 |
map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}]; |
|
10729 | 118 |
|
119 |
||
45647 | 120 |
|
10735 | 121 |
(** misc utilities **) |
6424 | 122 |
|
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
123 |
fun message quiet_mode s = if quiet_mode then () else writeln s; |
52059 | 124 |
|
125 |
fun clean_message ctxt quiet_mode s = |
|
126 |
if Config.get ctxt quick_and_dirty then () else message quiet_mode s; |
|
5662 | 127 |
|
6424 | 128 |
fun coind_prefix true = "co" |
129 |
| coind_prefix false = ""; |
|
130 |
||
45651 | 131 |
fun log (b: int) m n = if m >= n then 0 else 1 + log b (b * m) n; |
6424 | 132 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
133 |
fun make_bool_args f g [] i = [] |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
134 |
| make_bool_args f g (x :: xs) i = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
135 |
(if i mod 2 = 0 then f x else g x) :: make_bool_args f g xs (i div 2); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
136 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
137 |
fun make_bool_args' xs = |
45740 | 138 |
make_bool_args (K @{term False}) (K @{term True}) xs; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
139 |
|
33957 | 140 |
fun arg_types_of k c = drop k (binder_types (fastype_of c)); |
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset
|
141 |
|
40316
665862241968
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
39248
diff
changeset
|
142 |
fun find_arg T x [] = raise Fail "find_arg" |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
143 |
| find_arg T x ((p as (_, (SOME _, _))) :: ps) = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
144 |
apsnd (cons p) (find_arg T x ps) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
145 |
| find_arg T x ((p as (U, (NONE, y))) :: ps) = |
23577 | 146 |
if (T: typ) = U then (y, (U, (SOME x, y)) :: ps) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
147 |
else apsnd (cons p) (find_arg T x ps); |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
148 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
149 |
fun make_args Ts xs = |
28524 | 150 |
map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
151 |
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts)); |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
152 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
153 |
fun make_args' Ts xs Us = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
154 |
fst (fold_map (fn T => find_arg T ()) Us (Ts ~~ map (pair NONE) xs)); |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
155 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
156 |
fun dest_predicate cs params t = |
5094 | 157 |
let |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
158 |
val k = length params; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
159 |
val (c, ts) = strip_comb t; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
160 |
val (xs, ys) = chop k ts; |
31986 | 161 |
val i = find_index (fn c' => c' = c) cs; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
162 |
in |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
163 |
if xs = params andalso i >= 0 then |
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset
|
164 |
SOME (c, i, ys, chop (length ys) (arg_types_of k c)) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
165 |
else NONE |
5094 | 166 |
end; |
167 |
||
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
168 |
fun mk_names a 0 = [] |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
169 |
| mk_names a 1 = [a] |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
170 |
| mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n); |
10988
e0016a009c17
Splitting of arguments of product types in induction rules is now less
berghofe
parents:
10910
diff
changeset
|
171 |
|
59532 | 172 |
fun select_disj_tac ctxt = |
173 |
let |
|
174 |
fun tacs 1 1 = [] |
|
175 |
| tacs _ 1 = [resolve_tac ctxt @{thms disjI1}] |
|
176 |
| tacs n i = resolve_tac ctxt @{thms disjI2} :: tacs (n - 1) (i - 1); |
|
177 |
in fn n => fn i => EVERY' (tacs n i) end; |
|
45647 | 178 |
|
6424 | 179 |
|
180 |
||
45651 | 181 |
(** context data **) |
182 |
||
183 |
type inductive_result = |
|
184 |
{preds: term list, elims: thm list, raw_induct: thm, |
|
185 |
induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}; |
|
186 |
||
187 |
fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} = |
|
188 |
let |
|
189 |
val term = Morphism.term phi; |
|
190 |
val thm = Morphism.thm phi; |
|
191 |
val fact = Morphism.fact phi; |
|
192 |
in |
|
193 |
{preds = map term preds, elims = fact elims, raw_induct = thm raw_induct, |
|
194 |
induct = thm induct, inducts = fact inducts, intrs = fact intrs, eqs = fact eqs} |
|
195 |
end; |
|
196 |
||
197 |
type inductive_info = {names: string list, coind: bool} * inductive_result; |
|
198 |
||
199 |
val empty_equations = |
|
45652
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
200 |
Item_Net.init Thm.eq_thm_prop |
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
201 |
(single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of); |
45651 | 202 |
|
203 |
datatype data = Data of |
|
204 |
{infos: inductive_info Symtab.table, |
|
205 |
monos: thm list, |
|
206 |
equations: thm Item_Net.T}; |
|
207 |
||
208 |
fun make_data (infos, monos, equations) = |
|
209 |
Data {infos = infos, monos = monos, equations = equations}; |
|
210 |
||
211 |
structure Data = Generic_Data |
|
212 |
( |
|
213 |
type T = data; |
|
214 |
val empty = make_data (Symtab.empty, [], empty_equations); |
|
215 |
val extend = I; |
|
216 |
fun merge (Data {infos = infos1, monos = monos1, equations = equations1}, |
|
217 |
Data {infos = infos2, monos = monos2, equations = equations2}) = |
|
218 |
make_data (Symtab.merge (K true) (infos1, infos2), |
|
219 |
Thm.merge_thms (monos1, monos2), |
|
220 |
Item_Net.merge (equations1, equations2)); |
|
221 |
); |
|
222 |
||
223 |
fun map_data f = |
|
224 |
Data.map (fn Data {infos, monos, equations} => make_data (f (infos, monos, equations))); |
|
225 |
||
226 |
fun rep_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data rep => rep); |
|
227 |
||
228 |
fun print_inductives ctxt = |
|
229 |
let |
|
230 |
val {infos, monos, ...} = rep_data ctxt; |
|
231 |
val space = Consts.space_of (Proof_Context.consts_of ctxt); |
|
232 |
in |
|
50301 | 233 |
[Pretty.block |
234 |
(Pretty.breaks |
|
235 |
(Pretty.str "(co)inductives:" :: |
|
56052 | 236 |
map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))), |
51584 | 237 |
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] |
56334
6b3739fee456
some shortcuts for chunks, which sometimes avoid bulky string output;
wenzelm
parents:
56249
diff
changeset
|
238 |
end |> Pretty.writeln_chunks; |
45651 | 239 |
|
240 |
||
241 |
(* inductive info *) |
|
242 |
||
243 |
fun the_inductive ctxt name = |
|
244 |
(case Symtab.lookup (#infos (rep_data ctxt)) name of |
|
245 |
NONE => error ("Unknown (co)inductive predicate " ^ quote name) |
|
246 |
| SOME info => info); |
|
247 |
||
248 |
fun put_inductives names info = |
|
249 |
map_data (fn (infos, monos, equations) => |
|
250 |
(fold (fn name => Symtab.update (name, info)) names infos, monos, equations)); |
|
251 |
||
252 |
||
253 |
(* monotonicity rules *) |
|
254 |
||
255 |
val get_monos = #monos o rep_data; |
|
256 |
||
257 |
fun mk_mono ctxt thm = |
|
258 |
let |
|
259 |
fun eq_to_mono thm' = thm' RS (thm' RS @{thm eq_to_mono}); |
|
260 |
fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD}) |
|
261 |
handle THM _ => thm RS @{thm le_boolD} |
|
262 |
in |
|
263 |
(case concl_of thm of |
|
56245 | 264 |
Const (@{const_name Pure.eq}, _) $ _ $ _ => eq_to_mono (thm RS meta_eq_to_obj_eq) |
45651 | 265 |
| _ $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => eq_to_mono thm |
266 |
| _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) => |
|
267 |
dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
268 |
(resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}])) thm)) |
45651 | 269 |
| _ => thm) |
270 |
end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm ctxt thm); |
|
271 |
||
272 |
val mono_add = |
|
273 |
Thm.declaration_attribute (fn thm => fn context => |
|
274 |
map_data (fn (infos, monos, equations) => |
|
275 |
(infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); |
|
276 |
||
277 |
val mono_del = |
|
278 |
Thm.declaration_attribute (fn thm => fn context => |
|
279 |
map_data (fn (infos, monos, equations) => |
|
280 |
(infos, Thm.del_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context); |
|
281 |
||
58815 | 282 |
val _ = |
283 |
Theory.setup |
|
284 |
(Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del) |
|
285 |
"declaration of monotonicity rule"); |
|
286 |
||
45651 | 287 |
|
288 |
(* equations *) |
|
289 |
||
290 |
val get_equations = #equations o rep_data; |
|
291 |
||
45652
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
292 |
val equation_add_permissive = |
45651 | 293 |
Thm.declaration_attribute (fn thm => |
45652
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
294 |
map_data (fn (infos, monos, equations) => |
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
295 |
(infos, monos, perhaps (try (Item_Net.update thm)) equations))); |
45651 | 296 |
|
297 |
||
298 |
||
10729 | 299 |
(** process rules **) |
300 |
||
301 |
local |
|
5094 | 302 |
|
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
303 |
fun err_in_rule ctxt name t msg = |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset
|
304 |
error (cat_lines ["Ill-formed introduction rule " ^ Binding.print name, |
24920 | 305 |
Syntax.string_of_term ctxt t, msg]); |
10729 | 306 |
|
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
307 |
fun err_in_prem ctxt name t p msg = |
24920 | 308 |
error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p, |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset
|
309 |
"in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]); |
5094 | 310 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
311 |
val bad_concl = "Conclusion of introduction rule must be an inductive predicate"; |
10729 | 312 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
313 |
val bad_ind_occ = "Inductive predicate occurs in argument of inductive predicate"; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
314 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
315 |
val bad_app = "Inductive predicate must be applied to parameter(s) "; |
11358
416ea5c009f5
now checks for leading meta-quantifiers and complains, instead of
paulson
parents:
11036
diff
changeset
|
316 |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41075
diff
changeset
|
317 |
fun atomize_term thy = Raw_Simplifier.rewrite_term thy inductive_atomize []; |
10729 | 318 |
|
319 |
in |
|
5094 | 320 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
321 |
fun check_rule ctxt cs params ((binding, att), rule) = |
10729 | 322 |
let |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
323 |
val params' = Term.variant_frees rule (Logic.strip_params rule); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
324 |
val frees = rev (map Free params'); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
325 |
val concl = subst_bounds (frees, Logic.strip_assums_concl rule); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
326 |
val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule); |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
327 |
val rule' = Logic.list_implies (prems, concl); |
42361 | 328 |
val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems; |
46215
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
329 |
val arule = fold_rev (Logic.all o Free) params' (Logic.list_implies (aprems, concl)); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
330 |
|
45647 | 331 |
fun check_ind err t = |
332 |
(case dest_predicate cs params t of |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
333 |
NONE => err (bad_app ^ |
24920 | 334 |
commas (map (Syntax.string_of_term ctxt) params)) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
335 |
| SOME (_, _, ys, _) => |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
336 |
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs |
45647 | 337 |
then err bad_ind_occ else ()); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
338 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
339 |
fun check_prem' prem t = |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36642
diff
changeset
|
340 |
if member (op =) cs (head_of t) then |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset
|
341 |
check_ind (err_in_prem ctxt binding rule prem) t |
45647 | 342 |
else |
343 |
(case t of |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
344 |
Abs (_, _, t) => check_prem' prem t |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
345 |
| t $ u => (check_prem' prem t; check_prem' prem u) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
346 |
| _ => ()); |
5094 | 347 |
|
10729 | 348 |
fun check_prem (prem, aprem) = |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
349 |
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem |
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset
|
350 |
else err_in_prem ctxt binding rule prem "Non-atomic premise"; |
45647 | 351 |
|
352 |
val _ = |
|
353 |
(case concl of |
|
354 |
Const (@{const_name Trueprop}, _) $ t => |
|
355 |
if member (op =) cs (head_of t) then |
|
42381
309ec68442c6
added Binding.print convenience, which includes quote already;
wenzelm
parents:
42364
diff
changeset
|
356 |
(check_ind (err_in_rule ctxt binding rule') t; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
357 |
List.app check_prem (prems ~~ aprems)) |
45647 | 358 |
else err_in_rule ctxt binding rule' bad_concl |
359 |
| _ => err_in_rule ctxt binding rule' bad_concl); |
|
360 |
in |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
361 |
((binding, att), arule) |
10729 | 362 |
end; |
5094 | 363 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
364 |
fun rulify ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
365 |
hol_simplify ctxt inductive_conj |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
366 |
#> hol_simplify ctxt inductive_rulify |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
367 |
#> hol_simplify ctxt inductive_rulify_fallback |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
368 |
#> Simplifier.norm_hhf ctxt; |
10729 | 369 |
|
370 |
end; |
|
371 |
||
5094 | 372 |
|
6424 | 373 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
374 |
(** proofs for (co)inductive predicates **) |
6424 | 375 |
|
26534 | 376 |
(* prove monotonicity *) |
5094 | 377 |
|
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
378 |
fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt = |
52059 | 379 |
(message (quiet_mode orelse skip_mono andalso Config.get ctxt quick_and_dirty) |
26534 | 380 |
" Proving monotonicity ..."; |
51551 | 381 |
(if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt |
36642 | 382 |
[] [] |
17985 | 383 |
(HOLogic.mk_Trueprop |
24815
f7093e90f36c
tuned internal interfaces: flags record, added kind for results;
wenzelm
parents:
24744
diff
changeset
|
384 |
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
385 |
(fn _ => EVERY [resolve_tac ctxt @{thms monoI} 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
386 |
REPEAT (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}] 1), |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
387 |
REPEAT (FIRST |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58936
diff
changeset
|
388 |
[assume_tac ctxt 1, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
389 |
resolve_tac ctxt (map (mk_mono ctxt) monos @ get_monos ctxt) 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
390 |
eresolve_tac ctxt @{thms le_funE} 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
391 |
dresolve_tac ctxt @{thms le_boolD} 1])])); |
5094 | 392 |
|
6424 | 393 |
|
10735 | 394 |
(* prove introduction rules *) |
5094 | 395 |
|
36642 | 396 |
fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' = |
5094 | 397 |
let |
52059 | 398 |
val _ = clean_message ctxt quiet_mode " Proving the introduction rules ..."; |
5094 | 399 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
400 |
val unfold = funpow k (fn th => th RS fun_cong) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
401 |
(mono RS (fp_def RS |
32652 | 402 |
(if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold}))); |
5094 | 403 |
|
45648 | 404 |
val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
405 |
|
36642 | 406 |
val intrs = map_index (fn (i, intr) => |
51551 | 407 |
Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
408 |
[rewrite_goals_tac ctxt rec_preds_defs, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
409 |
resolve_tac ctxt [unfold RS iffD2] 1, |
59532 | 410 |
select_disj_tac ctxt (length intr_ts) (i + 1) 1, |
17985 | 411 |
(*Not ares_tac, since refl must be tried before any equality assumptions; |
412 |
backtracking may occur if the premises have extra variables!*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
413 |
DEPTH_SOLVE_1 (resolve_tac ctxt rules 1 APPEND assume_tac ctxt 1)]) |
42361 | 414 |
|> singleton (Proof_Context.export ctxt ctxt')) intr_ts |
5094 | 415 |
|
416 |
in (intrs, unfold) end; |
|
417 |
||
6424 | 418 |
|
10735 | 419 |
(* prove elimination rules *) |
5094 | 420 |
|
36642 | 421 |
fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' = |
5094 | 422 |
let |
52059 | 423 |
val _ = clean_message ctxt quiet_mode " Proving the elimination rules ..."; |
5094 | 424 |
|
36642 | 425 |
val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
426 |
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
427 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
428 |
fun dest_intr r = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
429 |
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
430 |
Logic.strip_assums_hyp r, Logic.strip_params r); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
431 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
432 |
val intrs = map dest_intr intr_ts ~~ intr_names; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
433 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
434 |
val rules1 = [disjE, exE, FalseE]; |
45648 | 435 |
val rules2 = [conjE, FalseE, @{lemma "~ True ==> R" by (rule notE [OF _ TrueI])}]; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
436 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
437 |
fun prove_elim c = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
438 |
let |
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset
|
439 |
val Ts = arg_types_of (length params) c; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
440 |
val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt'; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
441 |
val frees = map Free (anames ~~ Ts); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
442 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
443 |
fun mk_elim_prem ((_, _, us, _), ts, params') = |
46218
ecf6375e2abb
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
wenzelm
parents:
46215
diff
changeset
|
444 |
Logic.list_all (params', |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
445 |
Logic.list_implies (map (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
446 |
(frees ~~ us) @ ts, P)); |
33317 | 447 |
val c_intrs = filter (equal c o #1 o #1 o #1) intrs; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
448 |
val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) :: |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
449 |
map mk_elim_prem (map #1 c_intrs) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
450 |
in |
51551 | 451 |
(Goal.prove_sorry ctxt'' [] prems P |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
452 |
(fn {context = ctxt4, prems} => EVERY |
46708
b138dee7bed3
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
wenzelm
parents:
46219
diff
changeset
|
453 |
[cut_tac (hd prems) 1, |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
454 |
rewrite_goals_tac ctxt4 rec_preds_defs, |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
455 |
dresolve_tac ctxt4 [unfold RS iffD1] 1, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
456 |
REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules1)), |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
457 |
REPEAT (FIRSTGOAL (eresolve_tac ctxt4 rules2)), |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
458 |
EVERY (map (fn prem => |
59499 | 459 |
DEPTH_SOLVE_1 (assume_tac ctxt4 1 ORELSE |
460 |
resolve_tac ctxt [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1)) |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
461 |
(tl prems))]) |
42361 | 462 |
|> singleton (Proof_Context.export ctxt'' ctxt'''), |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset
|
463 |
map #2 c_intrs, length Ts) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
464 |
end |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
465 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
466 |
in map prove_elim cs end; |
5094 | 467 |
|
45647 | 468 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
469 |
(* prove simplification equations *) |
6424 | 470 |
|
45647 | 471 |
fun prove_eqs quiet_mode cs params intr_ts intrs |
472 |
(elims: (thm * bstring list * int) list) ctxt ctxt'' = (* FIXME ctxt'' ?? *) |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
473 |
let |
52059 | 474 |
val _ = clean_message ctxt quiet_mode " Proving the simplification rules ..."; |
45647 | 475 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
476 |
fun dest_intr r = |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
477 |
(the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))), |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
478 |
Logic.strip_assums_hyp r, Logic.strip_params r); |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
479 |
val intr_ts' = map dest_intr intr_ts; |
45647 | 480 |
|
37901 | 481 |
fun prove_eq c (elim: thm * 'a * 'b) = |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
482 |
let |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
483 |
val Ts = arg_types_of (length params) c; |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
484 |
val (anames, ctxt') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt; |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
485 |
val frees = map Free (anames ~~ Ts); |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
486 |
val c_intrs = filter (equal c o #1 o #1 o #1) (intr_ts' ~~ intrs); |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
487 |
fun mk_intr_conj (((_, _, us, _), ts, params'), _) = |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
488 |
let |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
489 |
fun list_ex ([], t) = t |
45647 | 490 |
| list_ex ((a, T) :: vars, t) = |
491 |
HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t)); |
|
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
492 |
val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
493 |
in |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
494 |
list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
495 |
end; |
45647 | 496 |
val lhs = list_comb (c, params @ frees); |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
497 |
val rhs = |
45647 | 498 |
if null c_intrs then @{term False} |
499 |
else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); |
|
500 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
501 |
fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} => |
59532 | 502 |
select_disj_tac ctxt'' (length c_intrs) (i + 1) 1 THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
503 |
EVERY (replicate (length params) (resolve_tac ctxt'' @{thms exI} 1)) THEN |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
504 |
(if null prems then resolve_tac ctxt'' @{thms TrueI} 1 |
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
505 |
else |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
506 |
let |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
507 |
val (prems', last_prem) = split_last prems; |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
508 |
in |
58839 | 509 |
EVERY (map (fn prem => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
510 |
(resolve_tac ctxt'' @{thms conjI} 1 THEN resolve_tac ctxt'' [prem] 1)) prems') |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
511 |
THEN resolve_tac ctxt'' [last_prem] 1 |
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
512 |
end)) ctxt' 1; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
513 |
fun prove_intr2 (((_, _, us, _), ts, params'), intr) = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
514 |
EVERY (replicate (length params') (eresolve_tac ctxt' @{thms exE} 1)) THEN |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
515 |
(if null ts andalso null us then resolve_tac ctxt' [intr] 1 |
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
516 |
else |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
517 |
EVERY (replicate (length ts + length us - 1) (eresolve_tac ctxt' @{thms conjE} 1)) THEN |
59059 | 518 |
Subgoal.FOCUS_PREMS (fn {context = ctxt'', prems, ...} => |
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
519 |
let |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
520 |
val (eqs, prems') = chop (length us) prems; |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
521 |
val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; |
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
522 |
in |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
523 |
rewrite_goal_tac ctxt'' rew_thms 1 THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
524 |
resolve_tac ctxt'' [intr] 1 THEN |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
525 |
EVERY (map (fn p => resolve_tac ctxt'' [p] 1) prems') |
47876
0521ee2e504d
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
wenzelm
parents:
46961
diff
changeset
|
526 |
end) ctxt' 1); |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
527 |
in |
51551 | 528 |
Goal.prove_sorry ctxt' [] [] eq (fn _ => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
529 |
resolve_tac ctxt' @{thms iffI} 1 THEN |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
530 |
eresolve_tac ctxt' [#1 elim] 1 THEN |
45647 | 531 |
EVERY (map_index prove_intr1 c_intrs) THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
532 |
(if null c_intrs then eresolve_tac ctxt' @{thms FalseE} 1 |
45647 | 533 |
else |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
534 |
let val (c_intrs', last_c_intr) = split_last c_intrs in |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
535 |
EVERY (map (fn ci => eresolve_tac ctxt' @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
536 |
THEN prove_intr2 last_c_intr |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
537 |
end)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
538 |
|> rulify ctxt' |
42361 | 539 |
|> singleton (Proof_Context.export ctxt' ctxt'') |
45647 | 540 |
end; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
541 |
in |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
542 |
map2 prove_eq cs elims |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
543 |
end; |
45647 | 544 |
|
545 |
||
10735 | 546 |
(* derivation of simplified elimination rules *) |
5094 | 547 |
|
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
548 |
local |
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
549 |
|
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
550 |
(*delete needless equality assumptions*) |
29064 | 551 |
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"} |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58936
diff
changeset
|
552 |
(fn {context = ctxt, ...} => assume_tac ctxt 1); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
553 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE]; |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
554 |
fun elim_tac ctxt = REPEAT o eresolve_tac ctxt elim_rls; |
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
555 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
556 |
fun simp_case_tac ctxt i = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
557 |
EVERY' [elim_tac ctxt, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
558 |
asm_full_simp_tac ctxt, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
559 |
elim_tac ctxt, |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
560 |
REPEAT o bound_hyp_subst_tac ctxt] i; |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
561 |
|
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
562 |
in |
9598 | 563 |
|
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
564 |
fun mk_cases_tac ctxt = ALLGOALS (simp_case_tac ctxt) THEN prune_params_tac ctxt; |
53994 | 565 |
|
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
566 |
fun mk_cases ctxt prop = |
7107 | 567 |
let |
42361 | 568 |
val thy = Proof_Context.theory_of ctxt; |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
569 |
|
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
570 |
fun err msg = |
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
571 |
error (Pretty.string_of (Pretty.block |
24920 | 572 |
[Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop])); |
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
573 |
|
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset
|
574 |
val elims = Induct.find_casesP ctxt prop; |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
575 |
|
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
576 |
val cprop = Thm.cterm_of thy prop; |
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
577 |
fun mk_elim rl = |
53994 | 578 |
Thm.implies_intr cprop |
579 |
(Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl)) |
|
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
580 |
|> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); |
7107 | 581 |
in |
582 |
(case get_first (try mk_elim) elims of |
|
15531 | 583 |
SOME r => r |
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
584 |
| NONE => err "Proposition not an inductive predicate:") |
7107 | 585 |
end; |
586 |
||
11682
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
587 |
end; |
d9063229b4a1
simp_case_tac is back again from induct_method.ML;
wenzelm
parents:
11628
diff
changeset
|
588 |
|
45647 | 589 |
|
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
590 |
(* inductive_cases *) |
7107 | 591 |
|
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
592 |
fun gen_inductive_cases prep_att prep_prop args lthy = |
9598 | 593 |
let |
46915 | 594 |
val thmss = |
595 |
map snd args |
|
58993
302104d8366b
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
wenzelm
parents:
58963
diff
changeset
|
596 |
|> burrow (grouped 10 Par_List.map_independent (mk_cases lthy o prep_prop lthy)); |
46915 | 597 |
val facts = |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55111
diff
changeset
|
598 |
map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])])) |
46915 | 599 |
args thmss; |
53995 | 600 |
in lthy |> Local_Theory.notes facts end; |
5094 | 601 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55111
diff
changeset
|
602 |
val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop; |
24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24133
diff
changeset
|
603 |
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; |
7107 | 604 |
|
58815 | 605 |
val _ = |
606 |
Theory.setup |
|
607 |
(Method.setup @{binding ind_cases} |
|
608 |
(Scan.lift (Scan.repeat1 Args.name_inner_syntax -- |
|
609 |
Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >> |
|
610 |
(fn (raw_props, fixes) => fn ctxt => |
|
611 |
let |
|
612 |
val (_, ctxt') = Variable.add_fixes_binding fixes ctxt; |
|
613 |
val props = Syntax.read_props ctxt' raw_props; |
|
614 |
val ctxt'' = fold Variable.declare_term props ctxt'; |
|
615 |
val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props) |
|
616 |
in Method.erule ctxt 0 rules end)) |
|
617 |
"dynamic case analysis on predicates"); |
|
9598 | 618 |
|
45647 | 619 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
620 |
(* derivation of simplified equation *) |
9598 | 621 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
622 |
fun mk_simp_eq ctxt prop = |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
623 |
let |
45647 | 624 |
val thy = Proof_Context.theory_of ctxt; |
625 |
val ctxt' = Variable.auto_fixes prop ctxt; |
|
626 |
val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of; |
|
627 |
val substs = |
|
45649 | 628 |
Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop) |
38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
629 |
|> map_filter |
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
630 |
(fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop) |
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
631 |
(Vartab.empty, Vartab.empty), eq) |
45647 | 632 |
handle Pattern.MATCH => NONE); |
633 |
val (subst, eq) = |
|
634 |
(case substs of |
|
38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
635 |
[s] => s |
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
636 |
| _ => error |
45647 | 637 |
("equations matching pattern " ^ Syntax.string_of_term ctxt prop ^ " is not unique")); |
638 |
val inst = |
|
639 |
map (fn v => (cterm_of thy (Var v), cterm_of thy (Envir.subst_term subst (Var v)))) |
|
640 |
(Term.add_vars (lhs_of eq) []); |
|
641 |
in |
|
45651 | 642 |
Drule.cterm_instantiate inst eq |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
643 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt))) |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
644 |
|> singleton (Variable.export ctxt' ctxt) |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
645 |
end |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
646 |
|
45647 | 647 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
648 |
(* inductive simps *) |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
649 |
|
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
650 |
fun gen_inductive_simps prep_att prep_prop args lthy = |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
651 |
let |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
652 |
val facts = args |> map (fn ((a, atts), props) => |
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55111
diff
changeset
|
653 |
((a, map (prep_att lthy) atts), |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
654 |
map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props)); |
53995 | 655 |
in lthy |> Local_Theory.notes facts end; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
656 |
|
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55111
diff
changeset
|
657 |
val inductive_simps = gen_inductive_simps Attrib.check_src Syntax.read_prop; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
658 |
val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop; |
40902 | 659 |
|
45647 | 660 |
|
10735 | 661 |
(* prove induction rule *) |
5094 | 662 |
|
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
663 |
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono |
45647 | 664 |
fp_def rec_preds_defs ctxt ctxt''' = (* FIXME ctxt''' ?? *) |
5094 | 665 |
let |
52059 | 666 |
val _ = clean_message ctxt quiet_mode " Proving the induction rule ..."; |
5094 | 667 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
668 |
(* predicates for induction rule *) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
669 |
|
36642 | 670 |
val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt; |
45647 | 671 |
val preds = |
672 |
map2 (curry Free) pnames |
|
673 |
(map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs); |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
674 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
675 |
(* transform an introduction rule into a premise for induction rule *) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
676 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
677 |
fun mk_ind_prem r = |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
678 |
let |
33669 | 679 |
fun subst s = |
680 |
(case dest_predicate cs params s of |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
681 |
SOME (_, i, ys, (_, Ts)) => |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
682 |
let |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
683 |
val k = length Ts; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
684 |
val bs = map Bound (k - 1 downto 0); |
42364 | 685 |
val P = list_comb (nth preds i, map (incr_boundvars k) ys @ bs); |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
686 |
val Q = |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
687 |
fold_rev Term.abs (mk_names "x" k ~~ Ts) |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
688 |
(HOLogic.mk_binop inductive_conj_name |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
689 |
(list_comb (incr_boundvars k s, bs), P)); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
690 |
in (Q, case Ts of [] => SOME (s, P) | _ => NONE) end |
33669 | 691 |
| NONE => |
692 |
(case s of |
|
45647 | 693 |
t $ u => (fst (subst t) $ fst (subst u), NONE) |
694 |
| Abs (a, T, t) => (Abs (a, T, fst (subst t)), NONE) |
|
33669 | 695 |
| _ => (s, NONE))); |
7293 | 696 |
|
33338 | 697 |
fun mk_prem s prems = |
698 |
(case subst s of |
|
699 |
(_, SOME (t, u)) => t :: u :: prems |
|
700 |
| (t, _) => t :: prems); |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
701 |
|
45647 | 702 |
val SOME (_, i, ys, _) = |
703 |
dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); |
|
42364 | 704 |
in |
46215
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
705 |
fold_rev (Logic.all o Free) (Logic.strip_params r) |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
706 |
(Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem |
42364 | 707 |
(map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []), |
708 |
HOLogic.mk_Trueprop (list_comb (nth preds i, ys)))) |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
709 |
end; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
710 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
711 |
val ind_prems = map mk_ind_prem intr_ts; |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
712 |
|
21526
1e6bd5ed7abc
added morh_result, the_inductive, add_inductive_global;
wenzelm
parents:
21508
diff
changeset
|
713 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
714 |
(* make conclusions for induction rules *) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
715 |
|
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
716 |
val Tss = map (binder_types o fastype_of) preds; |
45647 | 717 |
val (xnames, ctxt'') = Variable.variant_fixes (mk_names "x" (length (flat Tss))) ctxt'; |
718 |
val mutual_ind_concl = |
|
719 |
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
720 |
(map (fn (((xnames, Ts), c), P) => |
45647 | 721 |
let val frees = map Free (xnames ~~ Ts) |
722 |
in HOLogic.mk_imp (list_comb (c, params @ frees), list_comb (P, frees)) end) |
|
723 |
(unflat Tss xnames ~~ Tss ~~ cs ~~ preds))); |
|
5094 | 724 |
|
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset
|
725 |
|
5094 | 726 |
(* make predicate for instantiation of abstract induction rule *) |
727 |
||
45647 | 728 |
val ind_pred = |
729 |
fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj |
|
730 |
(map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp) |
|
731 |
(make_bool_args HOLogic.mk_not I bs i) |
|
732 |
(list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds)); |
|
5094 | 733 |
|
45647 | 734 |
val ind_concl = |
735 |
HOLogic.mk_Trueprop |
|
736 |
(HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred)); |
|
5094 | 737 |
|
45647 | 738 |
val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); |
13626
282fbabec862
Fixed bug involving inductive definitions having equalities in the premises,
paulson
parents:
13197
diff
changeset
|
739 |
|
51551 | 740 |
val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
741 |
(fn {context = ctxt3, prems} => EVERY |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
742 |
[rewrite_goals_tac ctxt3 [inductive_conj_def], |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
743 |
DETERM (resolve_tac ctxt3 [raw_fp_induct] 1), |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
744 |
REPEAT (resolve_tac ctxt3 [@{thm le_funI}, @{thm le_boolI}] 1), |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
745 |
rewrite_goals_tac ctxt3 simp_thms2, |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
746 |
(*This disjE separates out the introduction rules*) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
747 |
REPEAT (FIRSTGOAL (eresolve_tac ctxt3 [disjE, exE, FalseE])), |
5094 | 748 |
(*Now break down the individual cases. No disjE here in case |
749 |
some premise involves disjunction.*) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
750 |
REPEAT (FIRSTGOAL (eresolve_tac ctxt3 [conjE] ORELSE' bound_hyp_subst_tac ctxt3)), |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
751 |
REPEAT (FIRSTGOAL |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
752 |
(resolve_tac ctxt3 [conjI, impI] ORELSE' |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
753 |
(eresolve_tac ctxt3 [notE] THEN' assume_tac ctxt3))), |
59499 | 754 |
EVERY (map (fn prem => |
755 |
DEPTH_SOLVE_1 (assume_tac ctxt3 1 ORELSE |
|
756 |
resolve_tac ctxt3 |
|
757 |
[rewrite_rule ctxt3 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, |
|
758 |
conjI, refl] 1)) prems)]); |
|
5094 | 759 |
|
51551 | 760 |
val lemma = Goal.prove_sorry ctxt'' [] [] |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
761 |
(Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
762 |
[rewrite_goals_tac ctxt3 rec_preds_defs, |
5094 | 763 |
REPEAT (EVERY |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
764 |
[REPEAT (resolve_tac ctxt3 [conjI, impI] 1), |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59060
diff
changeset
|
765 |
REPEAT (eresolve_tac ctxt3 [@{thm le_funE}, @{thm le_boolE}] 1), |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58936
diff
changeset
|
766 |
assume_tac ctxt3 1, |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
767 |
rewrite_goals_tac ctxt3 simp_thms1, |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58936
diff
changeset
|
768 |
assume_tac ctxt3 1])]); |
5094 | 769 |
|
42361 | 770 |
in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; |
5094 | 771 |
|
6424 | 772 |
|
773 |
||
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
774 |
(** specification of (co)inductive predicates **) |
10729 | 775 |
|
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
776 |
fun mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts monos params cnames_syn lthy = |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
777 |
let |
24915 | 778 |
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; |
5094 | 779 |
|
33077
3c9cf88ec841
arg_types_of auxiliary function; using multiset operations
haftmann
parents:
33056
diff
changeset
|
780 |
val argTs = fold (combine (op =) o arg_types_of (length params)) cs []; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
781 |
val k = log 2 1 (length cs); |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
782 |
val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT; |
45647 | 783 |
val p :: xs = |
784 |
map Free (Variable.variant_frees lthy intr_ts |
|
785 |
(("p", predT) :: (mk_names "x" (length argTs) ~~ argTs))); |
|
786 |
val bs = |
|
787 |
map Free (Variable.variant_frees lthy (p :: xs @ intr_ts) |
|
788 |
(map (rpair HOLogic.boolT) (mk_names "b" k))); |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
789 |
|
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
790 |
fun subst t = |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
791 |
(case dest_predicate cs params t of |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
792 |
SOME (_, i, ts, (Ts, Us)) => |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
793 |
let |
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
794 |
val l = length Us; |
33669 | 795 |
val zs = map Bound (l - 1 downto 0); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
796 |
in |
46219
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
797 |
fold_rev (Term.abs o pair "z") Us |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
798 |
(list_comb (p, |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
799 |
make_bool_args' bs i @ make_args argTs |
426ed18eba43
discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset
|
800 |
((map (incr_boundvars l) ts ~~ Ts) @ (zs ~~ Us)))) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
801 |
end |
33669 | 802 |
| NONE => |
803 |
(case t of |
|
804 |
t1 $ t2 => subst t1 $ subst t2 |
|
805 |
| Abs (x, T, u) => Abs (x, T, subst u) |
|
806 |
| _ => t)); |
|
5149 | 807 |
|
5094 | 808 |
(* transform an introduction rule into a conjunction *) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
809 |
(* [| p_i t; ... |] ==> p_j u *) |
5094 | 810 |
(* is transformed into *) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
811 |
(* b_j & x_j = u & p b_j t & ... *) |
5094 | 812 |
|
813 |
fun transform_rule r = |
|
814 |
let |
|
45647 | 815 |
val SOME (_, i, ts, (Ts, _)) = |
816 |
dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)); |
|
817 |
val ps = |
|
818 |
make_bool_args HOLogic.mk_not I bs i @ |
|
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
819 |
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ |
45647 | 820 |
map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r); |
33338 | 821 |
in |
822 |
fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P)) |
|
823 |
(Logic.strip_params r) |
|
45740 | 824 |
(if null ps then @{term True} else foldr1 HOLogic.mk_conj ps) |
45647 | 825 |
end; |
5094 | 826 |
|
827 |
(* make a disjunction of all introduction rules *) |
|
828 |
||
45647 | 829 |
val fp_fun = |
830 |
fold_rev lambda (p :: bs @ xs) |
|
45740 | 831 |
(if null intr_ts then @{term False} |
45647 | 832 |
else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)); |
5094 | 833 |
|
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
834 |
(* add definiton of recursive predicates to theory *) |
5094 | 835 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
836 |
val rec_name = |
28965 | 837 |
if Binding.is_empty alt_name then |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
838 |
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn)) |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
839 |
else alt_name; |
5094 | 840 |
|
59060
5f060de2dfd6
do not conceal inductive predicate names properly, following 4a3747517552
haftmann
parents:
59059
diff
changeset
|
841 |
val is_auxiliary = length cs >= 2; |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
842 |
val ((rec_const, (_, fp_def)), lthy') = lthy |
59060
5f060de2dfd6
do not conceal inductive predicate names properly, following 4a3747517552
haftmann
parents:
59059
diff
changeset
|
843 |
|> is_auxiliary ? Local_Theory.conceal |
33766
c679f05600cd
adapted Local_Theory.define -- eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset
|
844 |
|> Local_Theory.define |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
845 |
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn), |
59060
5f060de2dfd6
do not conceal inductive predicate names properly, following 4a3747517552
haftmann
parents:
59059
diff
changeset
|
846 |
((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}), |
45592 | 847 |
fold_rev lambda params |
848 |
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun))) |
|
59060
5f060de2dfd6
do not conceal inductive predicate names properly, following 4a3747517552
haftmann
parents:
59059
diff
changeset
|
849 |
||> is_auxiliary ? Local_Theory.restore_naming lthy; |
45647 | 850 |
val fp_def' = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
851 |
Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def]) |
59580 | 852 |
(Proof_Context.cterm_of lthy' (list_comb (rec_const, params))); |
33278 | 853 |
val specs = |
854 |
if length cs < 2 then [] |
|
855 |
else |
|
856 |
map_index (fn (i, (name_mx, c)) => |
|
857 |
let |
|
858 |
val Ts = arg_types_of (length params) c; |
|
45647 | 859 |
val xs = |
860 |
map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts)); |
|
33278 | 861 |
in |
39248
4a3747517552
only conceal primitive definition theorems, not predicate names
haftmann
parents:
38864
diff
changeset
|
862 |
(name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs) |
33278 | 863 |
(list_comb (rec_const, params @ make_bool_args' bs i @ |
864 |
make_args argTs (xs ~~ Ts))))) |
|
865 |
end) (cnames_syn ~~ cs); |
|
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
866 |
val (consts_defs, lthy'') = lthy' |
39248
4a3747517552
only conceal primitive definition theorems, not predicate names
haftmann
parents:
38864
diff
changeset
|
867 |
|> fold_map Local_Theory.define specs; |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
868 |
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs); |
5094 | 869 |
|
36642 | 870 |
val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy''; |
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
871 |
val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy'''; |
36642 | 872 |
val (_, lthy'''') = |
873 |
Local_Theory.note (apfst Binding.conceal Attrib.empty_binding, |
|
42361 | 874 |
Proof_Context.export lthy''' lthy'' [mono]) lthy''; |
5094 | 875 |
|
36642 | 876 |
in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs, |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
877 |
list_comb (rec_const, params), preds, argTs, bs, xs) |
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
878 |
end; |
5094 | 879 |
|
33669 | 880 |
fun declare_rules rec_binding coind no_ind cnames |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
881 |
preds intrs intr_bindings intr_atts elims eqs raw_induct lthy = |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
882 |
let |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
883 |
val rec_name = Binding.name_of rec_binding; |
32773 | 884 |
fun rec_qualified qualified = Binding.qualify qualified rec_name; |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
885 |
val intr_names = map Binding.name_of intr_bindings; |
33368 | 886 |
val ind_case_names = Rule_Cases.case_names intr_names; |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
887 |
val induct = |
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
888 |
if coind then |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
889 |
(raw_induct, |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
890 |
[Rule_Cases.case_names [rec_name], |
33368 | 891 |
Rule_Cases.case_conclusion (rec_name, intr_names), |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
892 |
Rule_Cases.consumes (1 - Thm.nprems_of raw_induct), |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
893 |
Induct.coinduct_pred (hd cnames)]) |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
894 |
else if no_ind orelse length cnames > 1 then |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
895 |
(raw_induct, |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
896 |
[ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]) |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
897 |
else |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
898 |
(raw_induct RSN (2, rev_mp), |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
899 |
[ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))]); |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
900 |
|
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
901 |
val (intrs', lthy1) = |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
902 |
lthy |> |
35757
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset
|
903 |
Spec_Rules.add |
c2884bec5463
adding Spec_Rules to definitional package inductive and inductive_set
bulwahn
parents:
35646
diff
changeset
|
904 |
(if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |> |
33671 | 905 |
Local_Theory.notes |
33278 | 906 |
(map (rec_qualified false) intr_bindings ~~ intr_atts ~~ |
907 |
map (fn th => [([th], |
|
37264
8b931fb51cc6
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
blanchet
parents:
36960
diff
changeset
|
908 |
[Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>> |
24744
dcb8cf5fc99c
- add_inductive_i now takes typ instead of typ option as argument
berghofe
parents:
24721
diff
changeset
|
909 |
map (hd o snd); |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
910 |
val (((_, elims'), (_, [induct'])), lthy2) = |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
911 |
lthy1 |> |
33671 | 912 |
Local_Theory.note ((rec_qualified true (Binding.name "intros"), []), intrs') ||>> |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset
|
913 |
fold_map (fn (name, (elim, cases, k)) => |
33671 | 914 |
Local_Theory.note |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
915 |
((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
916 |
[Attrib.internal (K (Rule_Cases.case_names cases)), |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
917 |
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim))), |
34986
7f7939c9370f
Added "constraints" tag / attribute for specifying the number of equality
berghofe
parents:
33966
diff
changeset
|
918 |
Attrib.internal (K (Rule_Cases.constraints k)), |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
919 |
Attrib.internal (K (Induct.cases_pred name)), |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
920 |
Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #> |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
921 |
apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> |
33671 | 922 |
Local_Theory.note |
32773 | 923 |
((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
924 |
map (Attrib.internal o K) (#2 induct)), [rulify lthy1 (#1 induct)]); |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
925 |
|
45647 | 926 |
val (eqs', lthy3) = lthy2 |> |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
927 |
fold_map (fn (name, eq) => Local_Theory.note |
38665
e92223c886f8
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
bulwahn
parents:
38388
diff
changeset
|
928 |
((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"), |
45652
18214436e1d3
permissive update for improved "tool compliance";
wenzelm
parents:
45651
diff
changeset
|
929 |
[Attrib.internal (K equation_add_permissive)]), [eq]) |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
930 |
#> apfst (hd o snd)) |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
931 |
(if null eqs then [] else (cnames ~~ eqs)) |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
932 |
val (inducts, lthy4) = |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
933 |
if no_ind orelse coind then ([], lthy3) |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
934 |
else |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
935 |
let val inducts = cnames ~~ Project_Rule.projects lthy3 (1 upto length cnames) induct' in |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
936 |
lthy3 |> |
33671 | 937 |
Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
938 |
inducts |> map (fn (name, th) => ([th], |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
939 |
[Attrib.internal (K ind_case_names), |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
50302
diff
changeset
|
940 |
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), |
35646 | 941 |
Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
942 |
end; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
943 |
in (intrs', elims', eqs', induct', inducts, lthy4) end; |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
944 |
|
26534 | 945 |
type inductive_flags = |
33669 | 946 |
{quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool, |
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
947 |
no_elim: bool, no_ind: bool, skip_mono: bool}; |
26534 | 948 |
|
949 |
type add_ind_def = |
|
950 |
inductive_flags -> |
|
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset
|
951 |
term list -> (Attrib.binding * term) list -> thm list -> |
29581 | 952 |
term list -> (binding * mixfix) list -> |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
953 |
local_theory -> inductive_result * local_theory; |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
954 |
|
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
955 |
fun add_ind_def {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono} |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
956 |
cs intros monos params cnames_syn lthy = |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
957 |
let |
25288 | 958 |
val _ = null cnames_syn andalso error "No inductive predicates given"; |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
959 |
val names = map (Binding.name_of o fst) cnames_syn; |
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
960 |
val _ = message (quiet_mode andalso not verbose) |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
961 |
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names); |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
962 |
|
33671 | 963 |
val cnames = map (Local_Theory.full_name lthy o #1) cnames_syn; (* FIXME *) |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
964 |
val ((intr_names, intr_atts), intr_ts) = |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
965 |
apfst split_list (split_list (map (check_rule lthy cs params) intros)); |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
966 |
|
36642 | 967 |
val (lthy1, lthy2, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, |
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
968 |
argTs, bs, xs) = mk_ind_def quiet_mode skip_mono alt_name coind cs intr_ts |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
969 |
monos params cnames_syn lthy; |
9072
a4896cf23638
Now also proves monotonicity when in quick_and_dirty mode.
berghofe
parents:
8720
diff
changeset
|
970 |
|
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
971 |
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs) |
36642 | 972 |
intr_ts rec_preds_defs lthy2 lthy1; |
33459 | 973 |
val elims = |
974 |
if no_elim then [] |
|
975 |
else |
|
976 |
prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names) |
|
36642 | 977 |
unfold rec_preds_defs lthy2 lthy1; |
22605
41b092e7d89a
- Removed occurrences of ProofContext.export in add_ind_def that
berghofe
parents:
22460
diff
changeset
|
978 |
val raw_induct = zero_var_indexes |
33459 | 979 |
(if no_ind then Drule.asm_rl |
980 |
else if coind then |
|
42361 | 981 |
singleton (Proof_Context.export lthy2 lthy1) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
982 |
(rotate_prems ~1 (Object_Logic.rulify lthy2 |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
983 |
(fold_rule lthy2 rec_preds_defs |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
53995
diff
changeset
|
984 |
(rewrite_rule lthy2 simp_thms3 |
32652 | 985 |
(mono RS (fp_def RS @{thm def_coinduct})))))) |
21024
63ab84bb64d1
Completely rewrote inductive definition package. Now allows to
berghofe
parents:
20901
diff
changeset
|
986 |
else |
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
987 |
prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def |
36642 | 988 |
rec_preds_defs lthy2 lthy1); |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
989 |
val eqs = |
45647 | 990 |
if no_elim then [] else prove_eqs quiet_mode cs params intr_ts intrs elims lthy2 lthy1; |
5094 | 991 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
992 |
val elims' = map (fn (th, ns, i) => (rulify lthy1 th, ns, i)) elims; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
993 |
val intrs' = map (rulify lthy1) intrs; |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
994 |
|
45647 | 995 |
val (intrs'', elims'', eqs', induct, inducts, lthy3) = |
996 |
declare_rules rec_name coind no_ind |
|
997 |
cnames preds intrs' intr_names intr_atts elims' eqs raw_induct lthy1; |
|
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
998 |
|
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
999 |
val result = |
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
1000 |
{preds = preds, |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1001 |
intrs = intrs'', |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1002 |
elims = elims'', |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51658
diff
changeset
|
1003 |
raw_induct = rulify lthy3 raw_induct, |
35646 | 1004 |
induct = induct, |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1005 |
inducts = inducts, |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1006 |
eqs = eqs'}; |
21367
7a0cc1bb4dcc
inductive: canonical specification syntax (flattened result only);
wenzelm
parents:
21350
diff
changeset
|
1007 |
|
36642 | 1008 |
val lthy4 = lthy3 |
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset
|
1009 |
|> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => |
45290 | 1010 |
let val result' = transform_result phi result; |
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset
|
1011 |
in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end); |
36642 | 1012 |
in (result, lthy4) end; |
5094 | 1013 |
|
6424 | 1014 |
|
10735 | 1015 |
(* external interfaces *) |
5094 | 1016 |
|
26477
ecf06644f6cb
eliminated quiete_mode ref (turned into proper argument);
wenzelm
parents:
26336
diff
changeset
|
1017 |
fun gen_add_inductive_i mk_def |
59059 | 1018 |
flags cnames_syn pnames spec monos lthy = |
5094 | 1019 |
let |
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset
|
1020 |
|
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1021 |
(* abbrevs *) |
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1022 |
|
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1023 |
val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy; |
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset
|
1024 |
|
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1025 |
fun get_abbrev ((name, atts), t) = |
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1026 |
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then |
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1027 |
let |
29006 | 1028 |
val _ = Binding.is_empty name andalso null atts orelse |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1029 |
error "Abbreviations may not have names or attributes"; |
35624 | 1030 |
val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t)); |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
1031 |
val var = |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1032 |
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1033 |
NONE => error ("Undeclared head of abbreviation " ^ quote x) |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
1034 |
| SOME ((b, T'), mx) => |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1035 |
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x) |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
1036 |
else (b, mx)); |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27882
diff
changeset
|
1037 |
in SOME (var, rhs) end |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1038 |
else NONE; |
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset
|
1039 |
|
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1040 |
val abbrevs = map_filter get_abbrev spec; |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1041 |
val bs = map (Binding.name_of o fst o fst) abbrevs; |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1042 |
|
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset
|
1043 |
|
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1044 |
(* predicates *) |
21766
3eb48154388e
Abbreviations can now be specified simultaneously
berghofe
parents:
21658
diff
changeset
|
1045 |
|
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1046 |
val pre_intros = filter_out (is_some o get_abbrev) spec; |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1047 |
val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn; |
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1048 |
val cs = map (Free o apfst Binding.name_of o fst) cnames_syn'; |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1049 |
val ps = map Free pnames; |
5094 | 1050 |
|
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1051 |
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn'); |
35624 | 1052 |
val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs; |
1053 |
val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs; |
|
42361 | 1054 |
val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy; |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1055 |
|
46215
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1056 |
fun close_rule r = |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1057 |
fold (Logic.all o Free) (fold_aterms |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1058 |
(fn t as Free (v as (s, _)) => |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1059 |
if Variable.is_fixed ctxt1 s orelse |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1060 |
member (op =) ps t then I else insert (op =) v |
0da9433f959e
discontinued old-style Term.list_all_free in favour of plain Logic.all;
wenzelm
parents:
45740
diff
changeset
|
1061 |
| _ => I) r []) r; |
5094 | 1062 |
|
26736
e6091328718f
added explicit check phase after reading of specification
haftmann
parents:
26534
diff
changeset
|
1063 |
val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros; |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1064 |
val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn'; |
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
1065 |
in |
25029
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1066 |
lthy |
3a72718c5ddd
gen_add_inductive_i: treat abbrevs as local defs, expand by export;
wenzelm
parents:
25016
diff
changeset
|
1067 |
|> mk_def flags cs intros monos ps preds |
33671 | 1068 |
||> fold (snd oo Local_Theory.abbrev Syntax.mode_default) abbrevs |
21048
e57e91f72831
Restructured and repaired code dealing with case names
berghofe
parents:
21024
diff
changeset
|
1069 |
end; |
5094 | 1070 |
|
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
1071 |
fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy = |
5094 | 1072 |
let |
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset
|
1073 |
val ((vars, intrs), _) = lthy |
42361 | 1074 |
|> Proof_Context.set_mode Proof_Context.mode_abbrev |
30486
9cdc7ce0e389
simplified preparation and outer parsing of specification;
wenzelm
parents:
30435
diff
changeset
|
1075 |
|> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs; |
24721 | 1076 |
val (cs, ps) = chop (length cnames_syn) vars; |
1077 |
val monos = Attrib.eval_thms lthy raw_monos; |
|
49170
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
1078 |
val flags = |
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
1079 |
{quiet_mode = false, verbose = verbose, alt_name = Binding.empty, |
03bee3a6a1b7
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
wenzelm
parents:
47876
diff
changeset
|
1080 |
coind = coind, no_elim = false, no_ind = false, skip_mono = false}; |
26128 | 1081 |
in |
1082 |
lthy |
|
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30218
diff
changeset
|
1083 |
|> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos |
26128 | 1084 |
end; |
5094 | 1085 |
|
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1086 |
val add_inductive_i = gen_add_inductive_i add_ind_def; |
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1087 |
val add_inductive = gen_add_inductive add_ind_def; |
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1088 |
|
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
1089 |
fun add_inductive_global flags cnames_syn pnames pre_intros monos thy = |
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset
|
1090 |
let |
29006 | 1091 |
val name = Sign.full_name thy (fst (fst (hd cnames_syn))); |
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset
|
1092 |
val ctxt' = thy |
38388 | 1093 |
|> Named_Target.theory_init |
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset
|
1094 |
|> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |
33671 | 1095 |
|> Local_Theory.exit; |
25380
03201004c77e
put_inductives: be permissive about multiple versions
wenzelm
parents:
25365
diff
changeset
|
1096 |
val info = #2 (the_inductive ctxt' name); |
42361 | 1097 |
in (info, Proof_Context.theory_of ctxt') end; |
6424 | 1098 |
|
1099 |
||
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1100 |
(* read off arities of inductive predicates from raw induction rule *) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1101 |
fun arities_of induct = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1102 |
map (fn (_ $ t $ u) => |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1103 |
(fst (dest_Const (head_of t)), length (snd (strip_comb u)))) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1104 |
(HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1105 |
|
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1106 |
(* read off parameters of inductive predicate from raw induction rule *) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1107 |
fun params_of induct = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1108 |
let |
45647 | 1109 |
val (_ $ t $ u :: _) = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)); |
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1110 |
val (_, ts) = strip_comb t; |
45647 | 1111 |
val (_, us) = strip_comb u; |
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1112 |
in |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1113 |
List.take (ts, length ts - length us) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1114 |
end; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1115 |
|
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1116 |
val pname_of_intr = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1117 |
concl_of #> HOLogic.dest_Trueprop #> head_of #> dest_Const #> fst; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1118 |
|
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1119 |
(* partition introduction rules according to predicate name *) |
25822 | 1120 |
fun gen_partition_rules f induct intros = |
1121 |
fold_rev (fn r => AList.map_entry op = (pname_of_intr (f r)) (cons r)) intros |
|
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1122 |
(map (rpair [] o fst) (arities_of induct)); |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1123 |
|
25822 | 1124 |
val partition_rules = gen_partition_rules I; |
1125 |
fun partition_rules' induct = gen_partition_rules fst induct; |
|
1126 |
||
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1127 |
fun unpartition_rules intros xs = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1128 |
fold_map (fn r => AList.map_entry_yield op = (pname_of_intr r) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1129 |
(fn x :: xs => (x, xs)) #>> the) intros xs |> fst; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1130 |
|
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1131 |
(* infer order of variables in intro rules from order of quantifiers in elim rule *) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1132 |
fun infer_intro_vars elim arity intros = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1133 |
let |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1134 |
val thy = theory_of_thm elim; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1135 |
val _ :: cases = prems_of elim; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1136 |
val used = map (fst o fst) (Term.add_vars (prop_of elim) []); |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1137 |
fun mtch (t, u) = |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1138 |
let |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1139 |
val params = Logic.strip_params t; |
45647 | 1140 |
val vars = |
1141 |
map (Var o apfst (rpair 0)) |
|
1142 |
(Name.variant_list used (map fst params) ~~ map snd params); |
|
1143 |
val ts = |
|
1144 |
map (curry subst_bounds (rev vars)) |
|
1145 |
(List.drop (Logic.strip_assums_hyp t, arity)); |
|
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1146 |
val us = Logic.strip_imp_prems u; |
45647 | 1147 |
val tab = |
1148 |
fold (Pattern.first_order_match thy) (ts ~~ us) (Vartab.empty, Vartab.empty); |
|
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1149 |
in |
32035 | 1150 |
map (Envir.subst_term tab) vars |
22789
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1151 |
end |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1152 |
in |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1153 |
map (mtch o apsnd prop_of) (cases ~~ intros) |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1154 |
end; |
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1155 |
|
4d03dc1cad04
Added functions arities_of, params_of, partition_rules, and
berghofe
parents:
22675
diff
changeset
|
1156 |
|
25978 | 1157 |
|
58815 | 1158 |
(** outer syntax **) |
6424 | 1159 |
|
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1160 |
fun gen_ind_decl mk_def coind = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset
|
1161 |
Parse.fixes -- Parse.for_fixes -- |
36954 | 1162 |
Scan.optional Parse_Spec.where_alt_specs [] -- |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
1163 |
Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] |
26988
742e26213212
more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents:
26928
diff
changeset
|
1164 |
>> (fn (((preds, params), specs), monos) => |
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
1165 |
(snd o gen_add_inductive mk_def true coind preds params specs monos)); |
23762
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1166 |
|
24eef53a9ad3
Reorganization due to introduction of inductive_set wrapper.
berghofe
parents:
23577
diff
changeset
|
1167 |
val ind_decl = gen_ind_decl add_ind_def; |
6424 | 1168 |
|
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
1169 |
val _ = |
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
1170 |
Outer_Syntax.local_theory @{command_spec "inductive"} "define inductive predicates" |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
1171 |
(ind_decl false); |
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
1172 |
|
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
1173 |
val _ = |
49324
4f28543ae7fa
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
wenzelm
parents:
49170
diff
changeset
|
1174 |
Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates" |
33458
ae1f5d89b082
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
wenzelm
parents:
33457
diff
changeset
|
1175 |
(ind_decl true); |
6723 | 1176 |
|
24867 | 1177 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
1178 |
Outer_Syntax.local_theory @{command_spec "inductive_cases"} |
50214 | 1179 |
"create simplified instances of elimination rules" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36958
diff
changeset
|
1180 |
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases)); |
7107 | 1181 |
|
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1182 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
1183 |
Outer_Syntax.local_theory @{command_spec "inductive_simps"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset
|
1184 |
"create simplification rules for inductive predicates" |
37734
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1185 |
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps)); |
489ac1ecb9f1
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
bulwahn
parents:
37264
diff
changeset
|
1186 |
|
50302 | 1187 |
val _ = |
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58839
diff
changeset
|
1188 |
Outer_Syntax.command @{command_spec "print_inductives"} |
50302 | 1189 |
"print (co)inductive definitions and monotonicity rules" |
51658
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51584
diff
changeset
|
1190 |
(Scan.succeed (Toplevel.unknown_context o |
21c10672633b
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51584
diff
changeset
|
1191 |
Toplevel.keep (print_inductives o Toplevel.context_of))); |
50302 | 1192 |
|
5094 | 1193 |
end; |