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