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