author  wenzelm 
Fri, 19 Jan 2007 22:08:08 +0100  
changeset 22101  6d13239d5f52 
parent 21350  6e58289b6685 
child 22846  fb79144af9a3 
permissions  rwrr 
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 

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 
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 = 
17412  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)) 
17314  87 
in case AList.lookup (op =) 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 nondatatype 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 ("Illformed 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 

17223  166 
thy 
167 
> Theory.add_path (Sign.base_name big_rec_name) 

18728  168 
> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] > snd 
17412  169 
> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) 
170 
> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) 

17223  171 
> Theory.parent_path 
12204  172 
end; 
6065  173 

12204  174 
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy = 
18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

175 
thy 
21350  176 
> IsarCmd.apply_theorems [raw_elim] 
177 
>> IsarCmd.apply_theorems [raw_induct] 

178 
>> IsarCmd.apply_theorems raw_case_eqns 

179 
>> IsarCmd.apply_theorems raw_recursor_eqns 

18418
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

180 
> (fn (((elims, inducts), case_eqns), recursor_eqns) => 
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

181 
rep_datatype_i (PureThy.single_thm "elimination" elims) 
bf448d999b7e
rearranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset

182 
(PureThy.single_thm "induction" inducts) case_eqns recursor_eqns); 
12175  183 

12204  184 

185 
(* theory setup *) 

186 

187 
val setup = 

18708  188 
(DatatypesData.init #> 
189 
ConstructorsData.init #> 

12175  190 
Method.add_methods 
191 
[("induct_tac", Method.goal_args Args.name induct_tac, 

192 
"induct_tac emulation (dynamic instantiation!)"), 

14153  193 
("case_tac", Method.goal_args Args.name exhaust_tac, 
18708  194 
"datatype case_tac emulation (dynamic instantiation!)")]); 
12204  195 

196 

197 
(* outer syntax *) 

198 

17057  199 
local structure P = OuterParse and K = OuterKeyword in 
12204  200 

201 
val rep_datatype_decl = 

22101  202 
(P.$$$ "elimination"  P.!!! SpecParse.xthm)  
203 
(P.$$$ "induction"  P.!!! SpecParse.xthm)  

204 
(P.$$$ "case_eqns"  P.!!! SpecParse.xthms1)  

205 
Scan.optional (P.$$$ "recursor_eqns"  P.!!! SpecParse.xthms1) [] 

12204  206 
>> (fn (((x, y), z), w) => rep_datatype x y z w); 
207 

208 
val rep_datatypeP = 

209 
OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl 

210 
(rep_datatype_decl >> Toplevel.theory); 

211 

212 
val _ = OuterSyntax.add_keywords ["elimination", "induction", "case_eqns", "recursor_eqns"]; 

213 
val _ = OuterSyntax.add_parsers [rep_datatypeP]; 

214 

215 
end; 

216 

217 
end; 

218 

219 

220 
val exhaust_tac = DatatypeTactics.exhaust_tac; 

221 
val induct_tac = DatatypeTactics.induct_tac; 