author | wenzelm |
Thu, 05 Mar 2009 12:08:00 +0100 | |
changeset 30280 | eb98b49ef835 |
parent 29579 | cb520b766e00 |
child 30364 | 577edc39b501 |
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 |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
13 |
val induct_tac: Proof.context -> string -> int -> tactic |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
14 |
val exhaust_tac: Proof.context -> string -> int -> tactic |
12204 | 15 |
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory |
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
24867
diff
changeset
|
16 |
val rep_datatype: Facts.ref * Attrib.src list -> Facts.ref * Attrib.src list -> |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
24867
diff
changeset
|
17 |
(Facts.ref * Attrib.src list) list -> (Facts.ref * Attrib.src list) list -> theory -> theory |
18708 | 18 |
val setup: theory -> theory |
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 |
22846 | 34 |
( |
6070 | 35 |
type T = datatype_info Symtab.table; |
36 |
val empty = Symtab.empty; |
|
6556 | 37 |
val copy = I; |
16458 | 38 |
val extend = I; |
39 |
fun merge _ tabs : T = Symtab.merge (K true) tabs; |
|
22846 | 40 |
); |
6070 | 41 |
|
42 |
||
43 |
||
44 |
(** Constructor information: needed to map constructors to datatypes **) |
|
45 |
||
46 |
type constructor_info = |
|
47 |
{big_rec_name : string, (*name of the mutually recursive set*) |
|
48 |
constructors : term list, (*the constructors, as Consts*) |
|
6141 | 49 |
free_iffs : thm list, (*freeness simprules*) |
6070 | 50 |
rec_rewrites : thm list}; (*recursor equations*) |
51 |
||
52 |
||
16458 | 53 |
structure ConstructorsData = TheoryDataFun |
22846 | 54 |
( |
6070 | 55 |
type T = constructor_info Symtab.table |
56 |
val empty = Symtab.empty |
|
6556 | 57 |
val copy = I; |
16458 | 58 |
val extend = I |
26618 | 59 |
fun merge _ tabs : T = Symtab.merge (K true) tabs; |
22846 | 60 |
); |
6070 | 61 |
|
6065 | 62 |
structure DatatypeTactics : DATATYPE_TACTICS = |
63 |
struct |
|
64 |
||
16458 | 65 |
fun datatype_info thy name = |
17412 | 66 |
(case Symtab.lookup (DatatypesData.get thy) name of |
15531 | 67 |
SOME info => info |
68 |
| NONE => error ("Unknown datatype " ^ quote name)); |
|
6065 | 69 |
|
70 |
||
71 |
(*Given a variable, find the inductive set associated it in the assumptions*) |
|
14153 | 72 |
exception Find_tname of string |
73 |
||
6065 | 74 |
fun find_tname var Bi = |
24826 | 75 |
let fun mk_pair (Const(@{const_name mem},_) $ Free (v,_) $ A) = |
6065 | 76 |
(v, #1 (dest_Const (head_of A))) |
12175 | 77 |
| mk_pair _ = raise Match |
15570 | 78 |
val pairs = List.mapPartial (try (mk_pair o FOLogic.dest_Trueprop)) |
12175 | 79 |
(#2 (strip_context Bi)) |
17314 | 80 |
in case AList.lookup (op =) pairs var of |
15531 | 81 |
NONE => raise Find_tname ("Cannot determine datatype of " ^ quote var) |
82 |
| SOME t => t |
|
6065 | 83 |
end; |
84 |
||
12175 | 85 |
(** generic exhaustion and induction tactic for datatypes |
86 |
Differences from HOL: |
|
6065 | 87 |
(1) no checking if the induction var occurs in premises, since it always |
88 |
appears in one of them, and it's hard to check for other occurrences |
|
89 |
(2) exhaustion works for VARIABLES in the premises, not general terms |
|
90 |
**) |
|
91 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
92 |
fun exhaust_induct_tac exh ctxt var i state = |
6065 | 93 |
let |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
94 |
val thy = ProofContext.theory_of ctxt |
6065 | 95 |
val (_, _, Bi, _) = dest_state (state, i) |
96 |
val tn = find_tname var Bi |
|
12175 | 97 |
val rule = |
16458 | 98 |
if exh then #exhaustion (datatype_info thy tn) |
99 |
else #induct (datatype_info thy tn) |
|
24826 | 100 |
val (Const(@{const_name mem},_) $ Var(ixn,_) $ _) = |
6112 | 101 |
(case prems_of rule of |
12175 | 102 |
[] => error "induction is not available for this datatype" |
103 |
| major::_ => FOLogic.dest_Trueprop major) |
|
6065 | 104 |
in |
27239 | 105 |
eres_inst_tac ctxt [(ixn, var)] rule i state |
14153 | 106 |
end |
107 |
handle Find_tname msg => |
|
108 |
if exh then (*try boolean case analysis instead*) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
109 |
case_tac ctxt var i state |
14153 | 110 |
else error msg; |
6065 | 111 |
|
112 |
val exhaust_tac = exhaust_induct_tac true; |
|
113 |
val induct_tac = exhaust_induct_tac false; |
|
114 |
||
6070 | 115 |
|
116 |
(**** declare non-datatype as datatype ****) |
|
117 |
||
118 |
fun rep_datatype_i elim induct case_eqns recursor_eqns thy = |
|
119 |
let |
|
120 |
(*analyze the LHS of a case equation to get a constructor*) |
|
121 |
fun const_of (Const("op =", _) $ (_ $ c) $ _) = c |
|
122 |
| const_of eqn = error ("Ill-formed case equation: " ^ |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26618
diff
changeset
|
123 |
Syntax.string_of_term_global thy eqn); |
6070 | 124 |
|
125 |
val constructors = |
|
12175 | 126 |
map (head_of o const_of o FOLogic.dest_Trueprop o |
127 |
#prop o rep_thm) case_eqns; |
|
6070 | 128 |
|
24826 | 129 |
val Const (@{const_name mem}, _) $ _ $ data = |
12175 | 130 |
FOLogic.dest_Trueprop (hd (prems_of elim)); |
131 |
||
6112 | 132 |
val Const(big_rec_name, _) = head_of data; |
133 |
||
6070 | 134 |
val simps = case_eqns @ recursor_eqns; |
135 |
||
136 |
val dt_info = |
|
12175 | 137 |
{inductive = true, |
138 |
constructors = constructors, |
|
139 |
rec_rewrites = recursor_eqns, |
|
140 |
case_rewrites = case_eqns, |
|
141 |
induct = induct, |
|
142 |
mutual_induct = TrueI, (*No need for mutual induction*) |
|
143 |
exhaustion = elim}; |
|
6070 | 144 |
|
145 |
val con_info = |
|
12175 | 146 |
{big_rec_name = big_rec_name, |
147 |
constructors = constructors, |
|
148 |
(*let primrec handle definition by cases*) |
|
149 |
free_iffs = [], (*thus we expect the necessary freeness rewrites |
|
150 |
to be in the simpset already, as is the case for |
|
151 |
Nat and disjoint sum*) |
|
152 |
rec_rewrites = (case recursor_eqns of |
|
153 |
[] => case_eqns | _ => recursor_eqns)}; |
|
6070 | 154 |
|
155 |
(*associate with each constructor the datatype name and rewrites*) |
|
156 |
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors |
|
157 |
||
158 |
in |
|
17223 | 159 |
thy |
30280 | 160 |
|> Sign.add_path (NameSpace.base_name big_rec_name) |
29579 | 161 |
|> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |
17412 | 162 |
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |
163 |
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
22846
diff
changeset
|
164 |
|> Sign.parent_path |
12204 | 165 |
end; |
6065 | 166 |
|
12204 | 167 |
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = |
24725 | 168 |
let |
169 |
val ctxt = ProofContext.init thy; |
|
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
24867
diff
changeset
|
170 |
val elim = Facts.the_single "elimination" (Attrib.eval_thms ctxt [raw_elim]); |
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
24867
diff
changeset
|
171 |
val induct = Facts.the_single "induction" (Attrib.eval_thms ctxt [raw_induct]); |
24725 | 172 |
val case_eqns = Attrib.eval_thms ctxt raw_case_eqns; |
173 |
val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns; |
|
174 |
in rep_datatype_i elim induct case_eqns recursor_eqns thy end; |
|
12175 | 175 |
|
12204 | 176 |
|
177 |
(* theory setup *) |
|
178 |
||
179 |
val setup = |
|
12175 | 180 |
Method.add_methods |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
181 |
[("induct_tac", Method.goal_args_ctxt Args.name induct_tac, |
12175 | 182 |
"induct_tac emulation (dynamic instantiation!)"), |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26939
diff
changeset
|
183 |
("case_tac", Method.goal_args_ctxt Args.name exhaust_tac, |
22846 | 184 |
"datatype case_tac emulation (dynamic instantiation!)")]; |
12204 | 185 |
|
186 |
||
187 |
(* outer syntax *) |
|
188 |
||
17057 | 189 |
local structure P = OuterParse and K = OuterKeyword in |
12204 | 190 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27239
diff
changeset
|
191 |
val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"]; |
24867 | 192 |
|
12204 | 193 |
val rep_datatype_decl = |
22101 | 194 |
(P.$$$ "elimination" |-- P.!!! SpecParse.xthm) -- |
195 |
(P.$$$ "induction" |-- P.!!! SpecParse.xthm) -- |
|
196 |
(P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) -- |
|
197 |
Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) [] |
|
12204 | 198 |
>> (fn (((x, y), z), w) => rep_datatype x y z w); |
199 |
||
24867 | 200 |
val _ = |
12204 | 201 |
OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl |
202 |
(rep_datatype_decl >> Toplevel.theory); |
|
203 |
||
204 |
end; |
|
205 |
||
206 |
end; |
|
207 |
||
208 |
||
209 |
val exhaust_tac = DatatypeTactics.exhaust_tac; |
|
210 |
val induct_tac = DatatypeTactics.induct_tac; |