author | wenzelm |
Tue, 22 Feb 2000 21:45:20 +0100 | |
changeset 8277 | 493707fcd8a6 |
parent 8100 | 6186ee807f2e |
child 8293 | 4a0e17cf8f70 |
permissions | -rw-r--r-- |
5094 | 1 |
(* Title: HOL/Tools/inductive_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Stefan Berghofer, TU Muenchen |
|
5 |
Copyright 1994 University of Cambridge |
|
6 |
1998 TU Muenchen |
|
7 |
||
6424 | 8 |
(Co)Inductive Definition module for HOL. |
5094 | 9 |
|
10 |
Features: |
|
6424 | 11 |
* least or greatest fixedpoints |
12 |
* user-specified product and sum constructions |
|
13 |
* mutually recursive definitions |
|
14 |
* definitions involving arbitrary monotone operators |
|
15 |
* automatically proves introduction and elimination rules |
|
5094 | 16 |
|
6424 | 17 |
The recursive sets must *already* be declared as constants in the |
18 |
current theory! |
|
5094 | 19 |
|
20 |
Introduction rules have the form |
|
21 |
[| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |] |
|
22 |
where M is some monotone operator (usually the identity) |
|
23 |
P(x) is any side condition on the free variables |
|
24 |
ti, t are any terms |
|
25 |
Sj, Sk are two of the sets being defined in mutual recursion |
|
26 |
||
6424 | 27 |
Sums are used only for mutual recursion. Products are used only to |
28 |
derive "streamlined" induction rules for relations. |
|
5094 | 29 |
*) |
30 |
||
31 |
signature INDUCTIVE_PACKAGE = |
|
32 |
sig |
|
6424 | 33 |
val quiet_mode: bool ref |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
34 |
val unify_consts: Sign.sg -> term list -> term list -> term list * term list |
6437 | 35 |
val get_inductive: theory -> string -> |
36 |
{names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
|
37 |
induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
|
38 |
val print_inductives: theory -> unit |
|
8277 | 39 |
val cases_of: Sign.sg -> string -> thm |
40 |
val cases: Sign.sg -> thm list |
|
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 |
6424 | 44 |
val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
6521 | 45 |
theory attribute list -> ((bstring * term) * theory attribute list) list -> |
46 |
thm list -> thm list -> theory -> theory * |
|
6424 | 47 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
6437 | 48 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
6521 | 49 |
val add_inductive: bool -> bool -> string list -> Args.src list -> |
50 |
((bstring * string) * Args.src list) list -> (xstring * Args.src list) list -> |
|
51 |
(xstring * Args.src list) list -> theory -> theory * |
|
6424 | 52 |
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
6437 | 53 |
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
7107 | 54 |
val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text |
55 |
-> theory -> theory |
|
56 |
val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text |
|
57 |
-> theory -> theory |
|
6437 | 58 |
val setup: (theory -> theory) list |
5094 | 59 |
end; |
60 |
||
6424 | 61 |
structure InductivePackage: INDUCTIVE_PACKAGE = |
5094 | 62 |
struct |
63 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
64 |
(*** theory data ***) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
65 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
66 |
(* data kind 'HOL/inductive' *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
67 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
68 |
type inductive_info = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
69 |
{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
|
70 |
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
|
71 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
72 |
structure InductiveArgs = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
73 |
struct |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
74 |
val name = "HOL/inductive"; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
75 |
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
|
76 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
77 |
val empty = (Symtab.empty, []); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
78 |
val copy = I; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
79 |
val prep_ext = I; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
80 |
fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2), |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
81 |
Library.generic_merge Thm.eq_thm I I monos1 monos2); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
82 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
83 |
fun print sg (tab, monos) = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
84 |
(Pretty.writeln (Pretty.strs ("(co)inductives:" :: |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
85 |
map #1 (Sign.cond_extern_table sg Sign.constK tab))); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
86 |
Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos))); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
87 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
88 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
89 |
structure InductiveData = TheoryDataFun(InductiveArgs); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
90 |
val print_inductives = InductiveData.print; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
91 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
92 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
93 |
(* get and put data *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
94 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
95 |
fun get_inductive thy name = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
96 |
(case Symtab.lookup (fst (InductiveData.get thy), name) of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
97 |
Some info => info |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
98 |
| None => error ("Unknown (co)inductive set " ^ quote name)); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
99 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
100 |
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
|
101 |
let |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
102 |
fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
103 |
val tab_monos = foldl upd (InductiveData.get thy, names) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
104 |
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
|
105 |
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
|
106 |
|
8277 | 107 |
|
108 |
(* cases rules *) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
109 |
|
8277 | 110 |
fun cases_of sg name = |
111 |
let |
|
112 |
fun find (None, (_, ({names, ...}, {elims, ...}): inductive_info)) = |
|
113 |
assoc (names ~~ elims, name) |
|
114 |
| find (some, _) = some; |
|
115 |
val (tab, _) = InductiveData.get_sg sg; |
|
116 |
in |
|
117 |
(case Symtab.foldl find (None, tab) of |
|
118 |
None => error ("Unknown (co)inductive set " ^ quote name) |
|
119 |
| Some thm => thm) |
|
120 |
end; |
|
121 |
||
122 |
fun cases sg = flat (map (#elims o #2 o #2) (Symtab.dest (#1 (InductiveData.get_sg sg)))); |
|
123 |
||
124 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
125 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
126 |
(** monotonicity rules **) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
127 |
|
8277 | 128 |
val get_monos = snd o InductiveData.get; |
129 |
fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy; |
|
130 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
131 |
fun mk_mono thm = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
132 |
let |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
133 |
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
|
134 |
(case concl_of thm of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
135 |
(_ $ (_ $ (Const ("Not", _) $ _) $ _)) => [] |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
136 |
| _ => [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
|
137 |
val concl = concl_of thm |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
138 |
in |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
eq2mono thm |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
143 |
else [thm] |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
144 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
145 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
146 |
(* mono add/del *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
147 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
148 |
local |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
149 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
150 |
fun map_rules_global f thy = put_monos (f (get_monos thy)) thy; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
151 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
152 |
fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
153 |
fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
154 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
155 |
fun mk_att f g (x, thm) = (f (g thm) x, thm); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
156 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
157 |
in |
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_add_global = mk_att map_rules_global add_mono; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
160 |
val mono_del_global = mk_att map_rules_global del_mono; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
161 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
162 |
end; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
163 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
164 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
165 |
(* concrete syntax *) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
166 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
167 |
val monoN = "mono"; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
168 |
val addN = "add"; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
169 |
val delN = "del"; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
170 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
171 |
fun mono_att add del = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
172 |
Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add)); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
173 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
174 |
val mono_attr = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
175 |
(mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
176 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
177 |
|
7107 | 178 |
|
6424 | 179 |
(** utilities **) |
180 |
||
181 |
(* messages *) |
|
182 |
||
5662 | 183 |
val quiet_mode = ref false; |
184 |
fun message s = if !quiet_mode then () else writeln s; |
|
185 |
||
6424 | 186 |
fun coind_prefix true = "co" |
187 |
| coind_prefix false = ""; |
|
188 |
||
189 |
||
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
190 |
(* the following code ensures that each recursive set *) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
191 |
(* always has the same type in all introduction rules *) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
192 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
193 |
fun unify_consts sign cs intr_ts = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
194 |
(let |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
195 |
val {tsig, ...} = Sign.rep_sg sign; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
196 |
val add_term_consts_2 = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
197 |
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
|
198 |
fun varify (t, (i, ts)) = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
199 |
let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, [])) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
200 |
in (maxidx_of_term t', t'::ts) end; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
201 |
val (i, cs') = foldr varify (cs, (~1, [])); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
202 |
val (i', intr_ts') = foldr varify (intr_ts, (i, [])); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
203 |
val rec_consts = foldl add_term_consts_2 ([], cs'); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
204 |
val intr_consts = foldl add_term_consts_2 ([], intr_ts'); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
205 |
fun unify (env, (cname, cT)) = |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
206 |
let val consts = map snd (filter (fn c => fst c = cname) intr_consts) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
207 |
in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp)) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
208 |
(env, (replicate (length consts) cT) ~~ consts) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
209 |
end; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
210 |
val (env, _) = foldl unify (([], i'), rec_consts); |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
211 |
fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
212 |
in if T = T' then T else typ_subst_TVars_2 env T' end; |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
213 |
val subst = fst o Type.freeze_thaw o |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
214 |
(map_term_types (typ_subst_TVars_2 env)) |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
215 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
216 |
in (map subst cs', map subst intr_ts') |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
217 |
end) handle Type.TUNIFY => |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
218 |
(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
|
219 |
|
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
220 |
|
6424 | 221 |
(* misc *) |
222 |
||
5094 | 223 |
val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD); |
224 |
||
225 |
(*Delete needless equality assumptions*) |
|
226 |
val refl_thin = prove_goal HOL.thy "!!P. [| a=a; P |] ==> P" |
|
227 |
(fn _ => [assume_tac 1]); |
|
228 |
||
229 |
(*For simplifying the elimination rule*) |
|
5120
f7f5442c934a
Removed disjE from list of rules used to simplify elimination
berghofe
parents:
5108
diff
changeset
|
230 |
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject]; |
5094 | 231 |
|
6394 | 232 |
val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``"; |
233 |
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono"; |
|
5094 | 234 |
|
235 |
(* make injections needed in mutually recursive definitions *) |
|
236 |
||
237 |
fun mk_inj cs sumT c x = |
|
238 |
let |
|
239 |
fun mk_inj' T n i = |
|
240 |
if n = 1 then x else |
|
241 |
let val n2 = n div 2; |
|
242 |
val Type (_, [T1, T2]) = T |
|
243 |
in |
|
244 |
if i <= n2 then |
|
245 |
Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i) |
|
246 |
else |
|
247 |
Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) |
|
248 |
end |
|
249 |
in mk_inj' sumT (length cs) (1 + find_index_eq c cs) |
|
250 |
end; |
|
251 |
||
252 |
(* make "vimage" terms for selecting out components of mutually rec.def. *) |
|
253 |
||
254 |
fun mk_vimage cs sumT t c = if length cs < 2 then t else |
|
255 |
let |
|
256 |
val cT = HOLogic.dest_setT (fastype_of c); |
|
257 |
val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT |
|
258 |
in |
|
259 |
Const (vimage_name, vimageT) $ |
|
260 |
Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t |
|
261 |
end; |
|
262 |
||
6424 | 263 |
|
264 |
||
265 |
(** well-formedness checks **) |
|
5094 | 266 |
|
267 |
fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^ |
|
268 |
(Sign.string_of_term sign t) ^ "\n" ^ msg); |
|
269 |
||
270 |
fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^ |
|
271 |
(Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^ |
|
272 |
(Sign.string_of_term sign t) ^ "\n" ^ msg); |
|
273 |
||
274 |
val msg1 = "Conclusion of introduction rule must have form\ |
|
275 |
\ ' t : S_i '"; |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
276 |
val msg2 = "Non-atomic premise"; |
5094 | 277 |
val msg3 = "Recursion term on left of member symbol"; |
278 |
||
279 |
fun check_rule sign cs r = |
|
280 |
let |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
281 |
fun check_prem prem = if can HOLogic.dest_Trueprop prem then () |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
282 |
else err_in_prem sign r prem msg2; |
5094 | 283 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
284 |
in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
285 |
(Const ("op :", _) $ t $ u) => |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
286 |
if u mem cs then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
287 |
if exists (Logic.occs o (rpair t)) cs then |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
288 |
err_in_rule sign r msg3 |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
289 |
else |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
290 |
seq check_prem (Logic.strip_imp_prems r) |
5094 | 291 |
else err_in_rule sign r msg1 |
292 |
| _ => err_in_rule sign r msg1) |
|
293 |
end; |
|
294 |
||
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
295 |
fun try' f msg sign t = (case (try f t) of |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
296 |
Some x => x |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
297 |
| None => error (msg ^ Sign.string_of_term sign t)); |
5094 | 298 |
|
6424 | 299 |
|
5094 | 300 |
|
6424 | 301 |
(*** properties of (co)inductive sets ***) |
302 |
||
303 |
(** elimination rules **) |
|
5094 | 304 |
|
305 |
fun mk_elims cs cTs params intr_ts = |
|
306 |
let |
|
307 |
val used = foldr add_term_names (intr_ts, []); |
|
308 |
val [aname, pname] = variantlist (["a", "P"], used); |
|
309 |
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT)); |
|
310 |
||
311 |
fun dest_intr r = |
|
312 |
let val Const ("op :", _) $ t $ u = |
|
313 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
314 |
in (u, t, Logic.strip_imp_prems r) end; |
|
315 |
||
316 |
val intrs = map dest_intr intr_ts; |
|
317 |
||
318 |
fun mk_elim (c, T) = |
|
319 |
let |
|
320 |
val a = Free (aname, T); |
|
321 |
||
322 |
fun mk_elim_prem (_, t, ts) = |
|
323 |
list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params), |
|
324 |
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P)); |
|
325 |
in |
|
326 |
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) :: |
|
327 |
map mk_elim_prem (filter (equal c o #1) intrs), P) |
|
328 |
end |
|
329 |
in |
|
330 |
map mk_elim (cs ~~ cTs) |
|
331 |
end; |
|
332 |
||
6424 | 333 |
|
334 |
||
335 |
(** premises and conclusions of induction rules **) |
|
5094 | 336 |
|
337 |
fun mk_indrule cs cTs params intr_ts = |
|
338 |
let |
|
339 |
val used = foldr add_term_names (intr_ts, []); |
|
340 |
||
341 |
(* predicates for induction rule *) |
|
342 |
||
343 |
val preds = map Free (variantlist (if length cs < 2 then ["P"] else |
|
344 |
map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~ |
|
345 |
map (fn T => T --> HOLogic.boolT) cTs); |
|
346 |
||
347 |
(* transform an introduction rule into a premise for induction rule *) |
|
348 |
||
349 |
fun mk_ind_prem r = |
|
350 |
let |
|
351 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); |
|
352 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
353 |
val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds); |
5094 | 354 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
355 |
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
|
356 |
(case pred_of u of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
357 |
None => (m $ fst (subst t) $ fst (subst u), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
358 |
| Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t))) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
359 |
| subst s = |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
360 |
(case pred_of s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
361 |
Some P => (HOLogic.mk_binop "op Int" |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
362 |
(s, HOLogic.Collect_const (HOLogic.dest_setT |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
363 |
(fastype_of s)) $ P), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
364 |
| None => (case s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
365 |
(t $ u) => (fst (subst t) $ fst (subst u), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
366 |
| (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None) |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
367 |
| _ => (s, None))); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
368 |
|
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
369 |
fun mk_prem (s, prems) = (case subst s of |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
370 |
(_, Some (t, u)) => t :: u :: prems |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
371 |
| (t, _) => t :: prems); |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
372 |
|
5094 | 373 |
val Const ("op :", _) $ t $ u = |
374 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
375 |
||
376 |
in list_all_free (frees, |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
377 |
Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem |
5094 | 378 |
(map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])), |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
379 |
HOLogic.mk_Trueprop (the (pred_of u) $ t))) |
5094 | 380 |
end; |
381 |
||
382 |
val ind_prems = map mk_ind_prem intr_ts; |
|
383 |
||
384 |
(* make conclusions for induction rules *) |
|
385 |
||
386 |
fun mk_ind_concl ((c, P), (ts, x)) = |
|
387 |
let val T = HOLogic.dest_setT (fastype_of c); |
|
388 |
val Ts = HOLogic.prodT_factors T; |
|
389 |
val (frees, x') = foldr (fn (T', (fs, s)) => |
|
390 |
((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); |
|
391 |
val tuple = HOLogic.mk_tuple T frees; |
|
392 |
in ((HOLogic.mk_binop "op -->" |
|
393 |
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') |
|
394 |
end; |
|
395 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
396 |
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
5094 | 397 |
(fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa"))))) |
398 |
||
399 |
in (preds, ind_prems, mutual_ind_concl) |
|
400 |
end; |
|
401 |
||
6424 | 402 |
|
5094 | 403 |
|
6424 | 404 |
(*** proofs for (co)inductive sets ***) |
405 |
||
406 |
(** prove monotonicity **) |
|
5094 | 407 |
|
408 |
fun prove_mono setT fp_fun monos thy = |
|
409 |
let |
|
6427 | 410 |
val _ = message " Proving monotonicity ..."; |
5094 | 411 |
|
6394 | 412 |
val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop |
5094 | 413 |
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))) |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
414 |
(fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]) |
5094 | 415 |
|
416 |
in mono end; |
|
417 |
||
6424 | 418 |
|
419 |
||
420 |
(** prove introduction rules **) |
|
5094 | 421 |
|
422 |
fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = |
|
423 |
let |
|
6427 | 424 |
val _ = message " Proving the introduction rules ..."; |
5094 | 425 |
|
426 |
val unfold = standard (mono RS (fp_def RS |
|
427 |
(if coind then def_gfp_Tarski else def_lfp_Tarski))); |
|
428 |
||
429 |
fun select_disj 1 1 = [] |
|
430 |
| select_disj _ 1 = [rtac disjI1] |
|
431 |
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1)); |
|
432 |
||
433 |
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs |
|
6394 | 434 |
(cterm_of (Theory.sign_of thy) intr) (fn prems => |
5094 | 435 |
[(*insert prems and underlying sets*) |
436 |
cut_facts_tac prems 1, |
|
437 |
stac unfold 1, |
|
438 |
REPEAT (resolve_tac [vimageI2, CollectI] 1), |
|
439 |
(*Now 1-2 subgoals: the disjunction, perhaps equality.*) |
|
440 |
EVERY1 (select_disj (length intr_ts) i), |
|
441 |
(*Not ares_tac, since refl must be tried before any equality assumptions; |
|
442 |
backtracking may occur if the premises have extra variables!*) |
|
443 |
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1), |
|
444 |
(*Now solve the equations like Inl 0 = Inl ?b2*) |
|
445 |
rewrite_goals_tac con_defs, |
|
446 |
REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts) |
|
447 |
||
448 |
in (intrs, unfold) end; |
|
449 |
||
6424 | 450 |
|
451 |
||
452 |
(** prove elimination rules **) |
|
5094 | 453 |
|
454 |
fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy = |
|
455 |
let |
|
6427 | 456 |
val _ = message " Proving the elimination rules ..."; |
5094 | 457 |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
458 |
val rules1 = [CollectE, disjE, make_elim vimageD, exE]; |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
459 |
val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ |
5094 | 460 |
map make_elim [Inl_inject, Inr_inject]; |
461 |
||
462 |
val elims = map (fn t => prove_goalw_cterm rec_sets_defs |
|
6394 | 463 |
(cterm_of (Theory.sign_of thy) t) (fn prems => |
5094 | 464 |
[cut_facts_tac [hd prems] 1, |
465 |
dtac (unfold RS subst) 1, |
|
466 |
REPEAT (FIRSTGOAL (eresolve_tac rules1)), |
|
467 |
REPEAT (FIRSTGOAL (eresolve_tac rules2)), |
|
468 |
EVERY (map (fn prem => |
|
5149 | 469 |
DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])) |
5094 | 470 |
(mk_elims cs cTs params intr_ts) |
471 |
||
472 |
in elims end; |
|
473 |
||
6424 | 474 |
|
5094 | 475 |
(** derivation of simplified elimination rules **) |
476 |
||
477 |
(*Applies freeness of the given constructors, which *must* be unfolded by |
|
478 |
the given defs. Cannot simply use the local con_defs because con_defs=[] |
|
479 |
for inference systems. |
|
480 |
*) |
|
6141 | 481 |
fun con_elim_tac ss = |
5094 | 482 |
let val elim_tac = REPEAT o (eresolve_tac elim_rls) |
483 |
in ALLGOALS(EVERY'[elim_tac, |
|
6141 | 484 |
asm_full_simp_tac ss, |
485 |
elim_tac, |
|
486 |
REPEAT o bound_hyp_subst_tac]) |
|
5094 | 487 |
THEN prune_params_tac |
488 |
end; |
|
489 |
||
7107 | 490 |
(*cprop should have the form t:Si where Si is an inductive set*) |
491 |
fun mk_cases_i elims ss cprop = |
|
492 |
let |
|
493 |
val prem = Thm.assume cprop; |
|
494 |
fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl)); |
|
495 |
in |
|
496 |
(case get_first (try mk_elim) elims of |
|
497 |
Some r => r |
|
498 |
| None => error (Pretty.string_of (Pretty.block |
|
499 |
[Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk, |
|
500 |
Display.pretty_cterm cprop]))) |
|
501 |
end; |
|
502 |
||
6141 | 503 |
fun mk_cases elims s = |
7107 | 504 |
mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT)); |
505 |
||
506 |
||
507 |
(* inductive_cases(_i) *) |
|
508 |
||
509 |
fun gen_inductive_cases prep_att prep_const prep_prop |
|
510 |
((((name, raw_atts), raw_set), raw_props), comment) thy = |
|
511 |
let |
|
512 |
val sign = Theory.sign_of thy; |
|
513 |
||
514 |
val atts = map (prep_att thy) raw_atts; |
|
515 |
val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set); |
|
516 |
val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props; |
|
517 |
val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops; |
|
518 |
in |
|
519 |
thy |
|
520 |
|> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment) |
|
5094 | 521 |
end; |
522 |
||
7107 | 523 |
val inductive_cases = |
524 |
gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop; |
|
525 |
||
526 |
val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop; |
|
527 |
||
6424 | 528 |
|
529 |
||
530 |
(** prove induction rule **) |
|
5094 | 531 |
|
532 |
fun prove_indrule cs cTs sumT rec_const params intr_ts mono |
|
533 |
fp_def rec_sets_defs thy = |
|
534 |
let |
|
6427 | 535 |
val _ = message " Proving the induction rule ..."; |
5094 | 536 |
|
6394 | 537 |
val sign = Theory.sign_of thy; |
5094 | 538 |
|
7293 | 539 |
val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of |
540 |
None => [] |
|
541 |
| Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases")); |
|
542 |
||
5094 | 543 |
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; |
544 |
||
545 |
(* make predicate for instantiation of abstract induction rule *) |
|
546 |
||
547 |
fun mk_ind_pred _ [P] = P |
|
548 |
| mk_ind_pred T Ps = |
|
549 |
let val n = (length Ps) div 2; |
|
550 |
val Type (_, [T1, T2]) = T |
|
7293 | 551 |
in Const ("Datatype.sum.sum_case", |
5094 | 552 |
[T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $ |
553 |
mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps)) |
|
554 |
end; |
|
555 |
||
556 |
val ind_pred = mk_ind_pred sumT preds; |
|
557 |
||
558 |
val ind_concl = HOLogic.mk_Trueprop |
|
559 |
(HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->" |
|
560 |
(HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0))); |
|
561 |
||
562 |
(* simplification rules for vimage and Collect *) |
|
563 |
||
564 |
val vimage_simps = if length cs < 2 then [] else |
|
565 |
map (fn c => prove_goalw_cterm [] (cterm_of sign |
|
566 |
(HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
567 |
(mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c, |
|
568 |
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $ |
|
569 |
nth_elem (find_index_eq c cs, preds))))) |
|
7293 | 570 |
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, |
5094 | 571 |
rtac refl 1])) cs; |
572 |
||
573 |
val induct = prove_goalw_cterm [] (cterm_of sign |
|
574 |
(Logic.list_implies (ind_prems, ind_concl))) (fn prems => |
|
575 |
[rtac (impI RS allI) 1, |
|
576 |
DETERM (etac (mono RS (fp_def RS def_induct)) 1), |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
577 |
rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)), |
5094 | 578 |
fold_goals_tac rec_sets_defs, |
579 |
(*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
|
580 |
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])), |
5094 | 581 |
(*Now break down the individual cases. No disjE here in case |
582 |
some premise involves disjunction.*) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
583 |
REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)), |
7293 | 584 |
rewrite_goals_tac sum_case_rewrites, |
5094 | 585 |
EVERY (map (fn prem => |
5149 | 586 |
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]); |
5094 | 587 |
|
588 |
val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign |
|
589 |
(Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems => |
|
590 |
[cut_facts_tac prems 1, |
|
591 |
REPEAT (EVERY |
|
592 |
[REPEAT (resolve_tac [conjI, impI] 1), |
|
593 |
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1, |
|
7293 | 594 |
rewrite_goals_tac sum_case_rewrites, |
5094 | 595 |
atac 1])]) |
596 |
||
597 |
in standard (split_rule (induct RS lemma)) |
|
598 |
end; |
|
599 |
||
6424 | 600 |
|
601 |
||
602 |
(*** specification of (co)inductive sets ****) |
|
603 |
||
604 |
(** definitional introduction of (co)inductive sets **) |
|
5094 | 605 |
|
606 |
fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs |
|
6521 | 607 |
atts intros monos con_defs thy params paramTs cTs cnames = |
5094 | 608 |
let |
6424 | 609 |
val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ |
610 |
commas_quote cnames) else (); |
|
5094 | 611 |
|
612 |
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; |
|
613 |
val setT = HOLogic.mk_setT sumT; |
|
614 |
||
6394 | 615 |
val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp" |
616 |
else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp"; |
|
5094 | 617 |
|
6424 | 618 |
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); |
619 |
||
5149 | 620 |
val used = foldr add_term_names (intr_ts, []); |
621 |
val [sname, xname] = variantlist (["S", "x"], used); |
|
622 |
||
5094 | 623 |
(* transform an introduction rule into a conjunction *) |
624 |
(* [| t : ... S_i ... ; ... |] ==> u : S_j *) |
|
625 |
(* is transformed into *) |
|
626 |
(* x = Inj_j u & t : ... Inj_i -`` S ... & ... *) |
|
627 |
||
628 |
fun transform_rule r = |
|
629 |
let |
|
630 |
val frees = map dest_Free ((add_term_frees (r, [])) \\ params); |
|
5149 | 631 |
val subst = subst_free |
632 |
(cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs)); |
|
5094 | 633 |
val Const ("op :", _) $ t $ u = |
634 |
HOLogic.dest_Trueprop (Logic.strip_imp_concl r) |
|
635 |
||
636 |
in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P)) |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
637 |
(frees, foldr1 HOLogic.mk_conj |
5149 | 638 |
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t)):: |
5094 | 639 |
(map (subst o HOLogic.dest_Trueprop) |
640 |
(Logic.strip_imp_prems r)))) |
|
641 |
end |
|
642 |
||
643 |
(* make a disjunction of all introduction rules *) |
|
644 |
||
5149 | 645 |
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
|
646 |
absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts))); |
5094 | 647 |
|
648 |
(* add definiton of recursive sets to theory *) |
|
649 |
||
650 |
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; |
|
6394 | 651 |
val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name; |
5094 | 652 |
|
653 |
val rec_const = list_comb |
|
654 |
(Const (full_rec_name, paramTs ---> setT), params); |
|
655 |
||
656 |
val fp_def_term = Logic.mk_equals (rec_const, |
|
657 |
Const (fp_name, (setT --> setT) --> setT) $ fp_fun) |
|
658 |
||
659 |
val def_terms = fp_def_term :: (if length cs < 2 then [] else |
|
660 |
map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs); |
|
661 |
||
662 |
val thy' = thy |> |
|
663 |
(if declare_consts then |
|
664 |
Theory.add_consts_i (map (fn (c, n) => |
|
665 |
(n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) |
|
666 |
else I) |> |
|
667 |
(if length cs < 2 then I else |
|
668 |
Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |> |
|
669 |
Theory.add_path rec_name |> |
|
670 |
PureThy.add_defss_i [(("defs", def_terms), [])]; |
|
671 |
||
672 |
(* get definitions from theory *) |
|
673 |
||
6424 | 674 |
val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs"; |
5094 | 675 |
|
676 |
(* prove and store theorems *) |
|
677 |
||
678 |
val mono = prove_mono setT fp_fun monos thy'; |
|
679 |
val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs |
|
680 |
rec_sets_defs thy'; |
|
681 |
val elims = if no_elim then [] else |
|
682 |
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy'; |
|
683 |
val raw_induct = if no_ind then TrueI else |
|
684 |
if coind then standard (rule_by_tactic |
|
5553 | 685 |
(rewrite_tac [mk_meta_eq vimage_Un] THEN |
5094 | 686 |
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct))) |
687 |
else |
|
688 |
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def |
|
689 |
rec_sets_defs thy'; |
|
5108 | 690 |
val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct |
5094 | 691 |
else standard (raw_induct RSN (2, rev_mp)); |
692 |
||
6424 | 693 |
val thy'' = thy' |
6521 | 694 |
|> PureThy.add_thmss [(("intrs", intrs), atts)] |
6424 | 695 |
|> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |
696 |
|> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) |
|
697 |
|> (if no_ind then I else PureThy.add_thms |
|
698 |
[((coind_prefix coind ^ "induct", induct), [])]) |
|
699 |
|> Theory.parent_path; |
|
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
700 |
val intrs' = PureThy.get_thms thy'' "intrs"; |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
701 |
val elims' = PureThy.get_thms thy'' "elims"; |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
702 |
val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct"); |
5094 | 703 |
in (thy'', |
704 |
{defs = fp_def::rec_sets_defs, |
|
705 |
mono = mono, |
|
706 |
unfold = unfold, |
|
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
707 |
intrs = intrs', |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
708 |
elims = elims', |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
709 |
mk_cases = mk_cases elims', |
5094 | 710 |
raw_induct = raw_induct, |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
711 |
induct = induct'}) |
5094 | 712 |
end; |
713 |
||
6424 | 714 |
|
715 |
||
716 |
(** axiomatic introduction of (co)inductive sets **) |
|
5094 | 717 |
|
718 |
fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs |
|
6521 | 719 |
atts intros monos con_defs thy params paramTs cTs cnames = |
5094 | 720 |
let |
721 |
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; |
|
722 |
||
6424 | 723 |
val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); |
5094 | 724 |
val elim_ts = mk_elims cs cTs params intr_ts; |
725 |
||
726 |
val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts; |
|
727 |
val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl); |
|
728 |
||
6424 | 729 |
val thy' = thy |
730 |
|> (if declare_consts then |
|
731 |
Theory.add_consts_i |
|
732 |
(map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) |
|
733 |
else I) |
|
734 |
|> Theory.add_path rec_name |
|
6521 | 735 |
|> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])] |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
736 |
|> (if coind then I else |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
737 |
PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]); |
5094 | 738 |
|
6424 | 739 |
val intrs = PureThy.get_thms thy' "intrs"; |
740 |
val elims = PureThy.get_thms thy' "elims"; |
|
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
741 |
val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct"; |
5094 | 742 |
val induct = if coind orelse length cs > 1 then raw_induct |
743 |
else standard (raw_induct RSN (2, rev_mp)); |
|
744 |
||
6424 | 745 |
val thy'' = |
746 |
thy' |
|
747 |
|> (if coind then I else PureThy.add_thms [(("induct", induct), [])]) |
|
748 |
|> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |
|
749 |
|> Theory.parent_path; |
|
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
750 |
val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct"; |
5094 | 751 |
in (thy'', |
752 |
{defs = [], |
|
753 |
mono = TrueI, |
|
754 |
unfold = TrueI, |
|
755 |
intrs = intrs, |
|
756 |
elims = elims, |
|
757 |
mk_cases = mk_cases elims, |
|
758 |
raw_induct = raw_induct, |
|
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7710
diff
changeset
|
759 |
induct = induct'}) |
5094 | 760 |
end; |
761 |
||
6424 | 762 |
|
763 |
||
764 |
(** introduction of (co)inductive sets **) |
|
5094 | 765 |
|
766 |
fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs |
|
6521 | 767 |
atts intros monos con_defs thy = |
5094 | 768 |
let |
6424 | 769 |
val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); |
6394 | 770 |
val sign = Theory.sign_of thy; |
5094 | 771 |
|
772 |
(*parameters should agree for all mutually recursive components*) |
|
773 |
val (_, params) = strip_comb (hd cs); |
|
774 |
val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\ |
|
775 |
\ component is not a free variable: " sign) params; |
|
776 |
||
777 |
val cTs = map (try' (HOLogic.dest_setT o fastype_of) |
|
778 |
"Recursive component not of type set: " sign) cs; |
|
779 |
||
6437 | 780 |
val full_cnames = map (try' (fst o dest_Const o head_of) |
5094 | 781 |
"Recursive set not previously declared as constant: " sign) cs; |
6437 | 782 |
val cnames = map Sign.base_name full_cnames; |
5094 | 783 |
|
6424 | 784 |
val _ = seq (check_rule sign cs o snd o fst) intros; |
6437 | 785 |
|
786 |
val (thy1, result) = |
|
787 |
(if ! quick_and_dirty then add_ind_axm else add_ind_def) |
|
6521 | 788 |
verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos |
6437 | 789 |
con_defs thy params paramTs cTs cnames; |
790 |
val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result); |
|
791 |
in (thy2, result) end; |
|
5094 | 792 |
|
6424 | 793 |
|
5094 | 794 |
|
6424 | 795 |
(** external interface **) |
796 |
||
6521 | 797 |
fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = |
5094 | 798 |
let |
6394 | 799 |
val sign = Theory.sign_of thy; |
8100 | 800 |
val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; |
6424 | 801 |
|
6521 | 802 |
val atts = map (Attrib.global_attribute thy) srcs; |
6424 | 803 |
val intr_names = map (fst o fst) intro_srcs; |
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
804 |
val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs; |
6424 | 805 |
val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
806 |
val (cs', intr_ts') = unify_consts sign cs intr_ts; |
5094 | 807 |
|
6424 | 808 |
val ((thy', con_defs), monos) = thy |
809 |
|> IsarThy.apply_theorems raw_monos |
|
810 |
|> apfst (IsarThy.apply_theorems raw_con_defs); |
|
811 |
in |
|
7020
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
812 |
add_inductive_i verbose false "" coind false false cs' |
75ff179df7b7
Exported function unify_consts (workaround to avoid inconsistently
berghofe
parents:
6851
diff
changeset
|
813 |
atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' |
5094 | 814 |
end; |
815 |
||
6424 | 816 |
|
817 |
||
6437 | 818 |
(** package setup **) |
819 |
||
820 |
(* setup theory *) |
|
821 |
||
7710
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
822 |
val setup = [InductiveData.init, |
bf8cb3fc5d64
Monotonicity rules for inductive definitions can now be added to a theory via
berghofe
parents:
7349
diff
changeset
|
823 |
Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]]; |
6437 | 824 |
|
825 |
||
826 |
(* outer syntax *) |
|
6424 | 827 |
|
6723 | 828 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6424 | 829 |
|
6521 | 830 |
fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = |
6723 | 831 |
#1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; |
6424 | 832 |
|
833 |
fun ind_decl coind = |
|
6729 | 834 |
(Scan.repeat1 P.term --| P.marg_comment) -- |
835 |
(P.$$$ "intrs" |-- |
|
7152 | 836 |
P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- |
6729 | 837 |
Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- |
838 |
Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] |
|
6424 | 839 |
>> (Toplevel.theory o mk_ind coind); |
840 |
||
6723 | 841 |
val inductiveP = |
842 |
OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); |
|
843 |
||
844 |
val coinductiveP = |
|
845 |
OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); |
|
6424 | 846 |
|
7107 | 847 |
|
848 |
val ind_cases = |
|
849 |
P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment |
|
850 |
>> (Toplevel.theory o inductive_cases); |
|
851 |
||
852 |
val inductive_casesP = |
|
853 |
OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules" |
|
854 |
K.thy_decl ind_cases; |
|
855 |
||
6424 | 856 |
val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; |
7107 | 857 |
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; |
6424 | 858 |
|
5094 | 859 |
end; |
6424 | 860 |
|
861 |
||
862 |
end; |