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