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