author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 15705 | b5edb9dcec9a |
child 16122 | 864fda4a4056 |
permissions | -rw-r--r-- |
6070 | 1 |
(* Title: ZF/Tools/induct_tacs.ML |
6065 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
12204 | 6 |
Induction and exhaustion tactics for Isabelle/ZF. The theory |
7 |
information needed to support them (and to support primrec). Also a |
|
8 |
function to install other sets as if they were datatypes. |
|
6065 | 9 |
*) |
10 |
||
11 |
signature DATATYPE_TACTICS = |
|
12 |
sig |
|
12204 | 13 |
val induct_tac: string -> int -> tactic |
14 |
val exhaust_tac: string -> int -> tactic |
|
15 |
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory |
|
15703 | 16 |
val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list -> |
17 |
(thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory |
|
12204 | 18 |
val setup: (theory -> theory) list |
6065 | 19 |
end; |
20 |
||
21 |
||
6070 | 22 |
(** Datatype information, e.g. associated theorems **) |
23 |
||
24 |
type datatype_info = |
|
12175 | 25 |
{inductive: bool, (*true if inductive, not coinductive*) |
6070 | 26 |
constructors : term list, (*the constructors, as Consts*) |
27 |
rec_rewrites : thm list, (*recursor equations*) |
|
28 |
case_rewrites : thm list, (*case equations*) |
|
29 |
induct : thm, |
|
30 |
mutual_induct : thm, |
|
31 |
exhaustion : thm}; |
|
32 |
||
33 |
structure DatatypesArgs = |
|
34 |
struct |
|
35 |
val name = "ZF/datatypes"; |
|
36 |
type T = datatype_info Symtab.table; |
|
37 |
||
38 |
val empty = Symtab.empty; |
|
6556 | 39 |
val copy = I; |
6070 | 40 |
val prep_ext = I; |
41 |
val merge: T * T -> T = Symtab.merge (K true); |
|
42 |
||
43 |
fun print sg tab = |
|
44 |
Pretty.writeln (Pretty.strs ("datatypes:" :: |
|
6851 | 45 |
map #1 (Sign.cond_extern_table sg Sign.typeK tab))); |
6070 | 46 |
end; |
47 |
||
48 |
structure DatatypesData = TheoryDataFun(DatatypesArgs); |
|
49 |
||
50 |
||
51 |
(** Constructor information: needed to map constructors to datatypes **) |
|
52 |
||
53 |
type constructor_info = |
|
54 |
{big_rec_name : string, (*name of the mutually recursive set*) |
|
55 |
constructors : term list, (*the constructors, as Consts*) |
|
6141 | 56 |
free_iffs : thm list, (*freeness simprules*) |
6070 | 57 |
rec_rewrites : thm list}; (*recursor equations*) |
58 |
||
59 |
||
60 |
structure ConstructorsArgs = |
|
61 |
struct |
|
62 |
val name = "ZF/constructors" |
|
63 |
type T = constructor_info Symtab.table |
|
64 |
||
65 |
val empty = Symtab.empty |
|
6556 | 66 |
val copy = I; |
6070 | 67 |
val prep_ext = I |
68 |
val merge: T * T -> T = Symtab.merge (K true) |
|
69 |
||
70 |
fun print sg tab = () (*nothing extra to print*) |
|
71 |
end; |
|
72 |
||
73 |
structure ConstructorsData = TheoryDataFun(ConstructorsArgs); |
|
74 |
||
75 |
||
6065 | 76 |
structure DatatypeTactics : DATATYPE_TACTICS = |
77 |
struct |
|
78 |
||
79 |
fun datatype_info_sg sign name = |
|
80 |
(case Symtab.lookup (DatatypesData.get_sg sign, name) of |
|
15531 | 81 |
SOME info => info |
82 |
| NONE => error ("Unknown datatype " ^ quote name)); |
|
6065 | 83 |
|
84 |
||
85 |
(*Given a variable, find the inductive set associated it in the assumptions*) |
|
14153 | 86 |
exception Find_tname of string |
87 |
||
6065 | 88 |
fun find_tname var Bi = |
12175 | 89 |
let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) = |
6065 | 90 |
(v, #1 (dest_Const (head_of A))) |
12175 | 91 |
| mk_pair _ = raise Match |
15570 | 92 |
val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop)) |
12175 | 93 |
(#2 (strip_context Bi)) |
6065 | 94 |
in case assoc (pairs, var) of |
15531 | 95 |
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var) |
96 |
| SOME t => t |
|
6065 | 97 |
end; |
98 |
||
12175 | 99 |
(** generic exhaustion and induction tactic for datatypes |
100 |
Differences from HOL: |
|
6065 | 101 |
(1) no checking if the induction var occurs in premises, since it always |
102 |
appears in one of them, and it's hard to check for other occurrences |
|
103 |
(2) exhaustion works for VARIABLES in the premises, not general terms |
|
104 |
**) |
|
105 |
||
106 |
fun exhaust_induct_tac exh var i state = |
|
107 |
let |
|
108 |
val (_, _, Bi, _) = dest_state (state, i) |
|
109 |
val {sign, ...} = rep_thm state |
|
110 |
val tn = find_tname var Bi |
|
12175 | 111 |
val rule = |
112 |
if exh then #exhaustion (datatype_info_sg sign tn) |
|
113 |
else #induct (datatype_info_sg sign tn) |
|
114 |
val (Const("op :",_) $ Var(ixn,_) $ _) = |
|
6112 | 115 |
(case prems_of rule of |
12175 | 116 |
[] => error "induction is not available for this datatype" |
117 |
| major::_ => FOLogic.dest_Trueprop major) |
|
6065 | 118 |
in |
15462
b4208fbf9439
Eliminated hack for deleting leading question mark from induction
berghofe
parents:
14153
diff
changeset
|
119 |
Tactic.eres_inst_tac' [(ixn, var)] rule i state |
14153 | 120 |
end |
121 |
handle Find_tname msg => |
|
122 |
if exh then (*try boolean case analysis instead*) |
|
123 |
case_tac var i state |
|
124 |
else error msg; |
|
6065 | 125 |
|
126 |
val exhaust_tac = exhaust_induct_tac true; |
|
127 |
val induct_tac = exhaust_induct_tac false; |
|
128 |
||
6070 | 129 |
|
130 |
(**** declare non-datatype as datatype ****) |
|
131 |
||
132 |
fun rep_datatype_i elim induct case_eqns recursor_eqns thy = |
|
133 |
let |
|
134 |
val sign = sign_of thy; |
|
135 |
||
136 |
(*analyze the LHS of a case equation to get a constructor*) |
|
137 |
fun const_of (Const("op =", _) $ (_ $ c) $ _) = c |
|
138 |
| const_of eqn = error ("Ill-formed case equation: " ^ |
|
12175 | 139 |
Sign.string_of_term sign eqn); |
6070 | 140 |
|
141 |
val constructors = |
|
12175 | 142 |
map (head_of o const_of o FOLogic.dest_Trueprop o |
143 |
#prop o rep_thm) case_eqns; |
|
6070 | 144 |
|
6112 | 145 |
val Const ("op :", _) $ _ $ data = |
12175 | 146 |
FOLogic.dest_Trueprop (hd (prems_of elim)); |
147 |
||
6112 | 148 |
val Const(big_rec_name, _) = head_of data; |
149 |
||
6070 | 150 |
val simps = case_eqns @ recursor_eqns; |
151 |
||
152 |
val dt_info = |
|
12175 | 153 |
{inductive = true, |
154 |
constructors = constructors, |
|
155 |
rec_rewrites = recursor_eqns, |
|
156 |
case_rewrites = case_eqns, |
|
157 |
induct = induct, |
|
158 |
mutual_induct = TrueI, (*No need for mutual induction*) |
|
159 |
exhaustion = elim}; |
|
6070 | 160 |
|
161 |
val con_info = |
|
12175 | 162 |
{big_rec_name = big_rec_name, |
163 |
constructors = constructors, |
|
164 |
(*let primrec handle definition by cases*) |
|
165 |
free_iffs = [], (*thus we expect the necessary freeness rewrites |
|
166 |
to be in the simpset already, as is the case for |
|
167 |
Nat and disjoint sum*) |
|
168 |
rec_rewrites = (case recursor_eqns of |
|
169 |
[] => case_eqns | _ => recursor_eqns)}; |
|
6070 | 170 |
|
171 |
(*associate with each constructor the datatype name and rewrites*) |
|
172 |
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors |
|
173 |
||
174 |
in |
|
175 |
thy |> Theory.add_path (Sign.base_name big_rec_name) |
|
12175 | 176 |
|> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]) |
177 |
|> DatatypesData.put |
|
178 |
(Symtab.update |
|
179 |
((big_rec_name, dt_info), DatatypesData.get thy)) |
|
180 |
|> ConstructorsData.put |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
181 |
(foldr Symtab.update (ConstructorsData.get thy) con_pairs) |
12175 | 182 |
|> Theory.parent_path |
12204 | 183 |
end; |
6065 | 184 |
|
12204 | 185 |
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = |
186 |
let |
|
187 |
val (thy', (((elims, inducts), case_eqns), recursor_eqns)) = thy |
|
188 |
|> IsarThy.apply_theorems [raw_elim] |
|
189 |
|>>> IsarThy.apply_theorems [raw_induct] |
|
190 |
|>>> IsarThy.apply_theorems raw_case_eqns |
|
191 |
|>>> IsarThy.apply_theorems raw_recursor_eqns; |
|
192 |
in |
|
193 |
thy' |> rep_datatype_i (PureThy.single_thm "elimination" elims) |
|
194 |
(PureThy.single_thm "induction" inducts) case_eqns recursor_eqns |
|
195 |
end; |
|
12175 | 196 |
|
12204 | 197 |
|
198 |
(* theory setup *) |
|
199 |
||
200 |
val setup = |
|
12175 | 201 |
[DatatypesData.init, |
202 |
ConstructorsData.init, |
|
203 |
Method.add_methods |
|
204 |
[("induct_tac", Method.goal_args Args.name induct_tac, |
|
205 |
"induct_tac emulation (dynamic instantiation!)"), |
|
14153 | 206 |
("case_tac", Method.goal_args Args.name exhaust_tac, |
207 |
"datatype case_tac emulation (dynamic instantiation!)")]]; |
|
12204 | 208 |
|
209 |
||
210 |
(* outer syntax *) |
|
211 |
||
212 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
|
213 |
||
214 |
val rep_datatype_decl = |
|
215 |
(P.$$$ "elimination" |-- P.!!! P.xthm) -- |
|
216 |
(P.$$$ "induction" |-- P.!!! P.xthm) -- |
|
217 |
(P.$$$ "case_eqns" |-- P.!!! P.xthms1) -- |
|
218 |
Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) [] |
|
219 |
>> (fn (((x, y), z), w) => rep_datatype x y z w); |
|
220 |
||
221 |
val rep_datatypeP = |
|
222 |
OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl |
|
223 |
(rep_datatype_decl >> Toplevel.theory); |
|
224 |
||
225 |
val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
|
226 |
val _ = OuterSyntax.add_parsers [rep_datatypeP]; |
|
227 |
||
228 |
end; |
|
229 |
||
230 |
end; |
|
231 |
||
232 |
||
233 |
val exhaust_tac = DatatypeTactics.exhaust_tac; |
|
234 |
val induct_tac = DatatypeTactics.induct_tac; |
|
15705 | 235 |