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