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 


6 
Induction and exhaustion tactics for Isabelle/ZF

6070

7 


8 
The theory information needed to support them (and to support primrec)


9 


10 
Also, a function to install other sets as if they were datatypes

6065

11 
*)


12 


13 


14 
signature DATATYPE_TACTICS =


15 
sig


16 
val induct_tac : string > int > tactic


17 
val exhaust_tac : string > int > tactic

6070

18 
val rep_datatype_i : thm > thm > thm list > thm list > theory > theory

6065

19 
end;


20 


21 

6070

22 


23 
(** Datatype information, e.g. associated theorems **)


24 


25 
type datatype_info =


26 
{inductive: bool, (*true if inductive, not coinductive*)


27 
constructors : term list, (*the constructors, as Consts*)


28 
rec_rewrites : thm list, (*recursor equations*)


29 
case_rewrites : thm list, (*case equations*)


30 
induct : thm,


31 
mutual_induct : thm,


32 
exhaustion : thm};


33 


34 
structure DatatypesArgs =


35 
struct


36 
val name = "ZF/datatypes";


37 
type T = datatype_info Symtab.table;


38 


39 
val empty = Symtab.empty;

6556

40 
val copy = I;

6070

41 
val prep_ext = I;


42 
val merge: T * T > T = Symtab.merge (K true);


43 


44 
fun print sg tab =


45 
Pretty.writeln (Pretty.strs ("datatypes:" ::


46 
map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));


47 
end;


48 


49 
structure DatatypesData = TheoryDataFun(DatatypesArgs);


50 


51 


52 
(** Constructor information: needed to map constructors to datatypes **)


53 


54 
type constructor_info =


55 
{big_rec_name : string, (*name of the mutually recursive set*)


56 
constructors : term list, (*the constructors, as Consts*)

6141

57 
free_iffs : thm list, (*freeness simprules*)

6070

58 
rec_rewrites : thm list}; (*recursor equations*)


59 


60 


61 
structure ConstructorsArgs =


62 
struct


63 
val name = "ZF/constructors"


64 
type T = constructor_info Symtab.table


65 


66 
val empty = Symtab.empty

6556

67 
val copy = I;

6070

68 
val prep_ext = I


69 
val merge: T * T > T = Symtab.merge (K true)


70 


71 
fun print sg tab = () (*nothing extra to print*)


72 
end;


73 


74 
structure ConstructorsData = TheoryDataFun(ConstructorsArgs);


75 


76 
val setup_datatypes = [DatatypesData.init, ConstructorsData.init];


77 


78 


79 

6065

80 
structure DatatypeTactics : DATATYPE_TACTICS =


81 
struct


82 


83 
fun datatype_info_sg sign name =


84 
(case Symtab.lookup (DatatypesData.get_sg sign, name) of


85 
Some info => info


86 
 None => error ("Unknown datatype " ^ quote name));


87 


88 


89 
(*Given a variable, find the inductive set associated it in the assumptions*)


90 
fun find_tname var Bi =


91 
let fun mk_pair (Const("op :",_) $ Free (v,_) $ A) =


92 
(v, #1 (dest_Const (head_of A)))


93 
 mk_pair _ = raise Match


94 
val pairs = mapfilter (try (mk_pair o FOLogic.dest_Trueprop))


95 
(#2 (strip_context Bi))


96 
in case assoc (pairs, var) of


97 
None => error ("Cannot determine datatype of " ^ quote var)


98 
 Some t => t


99 
end;


100 


101 
(** generic exhaustion and induction tactic for datatypes


102 
Differences from HOL:


103 
(1) no checking if the induction var occurs in premises, since it always


104 
appears in one of them, and it's hard to check for other occurrences


105 
(2) exhaustion works for VARIABLES in the premises, not general terms


106 
**)


107 


108 
fun exhaust_induct_tac exh var i state =


109 
let


110 
val (_, _, Bi, _) = dest_state (state, i)


111 
val {sign, ...} = rep_thm state


112 
val tn = find_tname var Bi


113 
val rule =


114 
if exh then #exhaustion (datatype_info_sg sign tn)


115 
else #induct (datatype_info_sg sign tn)


116 
val (Const("op :",_) $ Var(ixn,_) $ _) =

6112

117 
(case prems_of rule of


118 
[] => error "induction is not available for this datatype"


119 
 major::_ => FOLogic.dest_Trueprop major)

6065

120 
val ind_vname = Syntax.string_of_vname ixn


121 
val vname' = (*delete leading question mark*)


122 
String.substring (ind_vname, 1, size ind_vname1)


123 
in


124 
eres_inst_tac [(vname',var)] rule i state


125 
end;


126 


127 
val exhaust_tac = exhaust_induct_tac true;


128 
val induct_tac = exhaust_induct_tac false;


129 

6070

130 


131 


132 
(**** declare nondatatype as datatype ****)


133 


134 
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =


135 
let


136 
val sign = sign_of thy;


137 


138 
(*analyze the LHS of a case equation to get a constructor*)


139 
fun const_of (Const("op =", _) $ (_ $ c) $ _) = c


140 
 const_of eqn = error ("Illformed case equation: " ^


141 
Sign.string_of_term sign eqn);


142 


143 
val constructors =


144 
map (head_of o const_of o FOLogic.dest_Trueprop o


145 
#prop o rep_thm) case_eqns;


146 

6112

147 
val Const ("op :", _) $ _ $ data =

6070

148 
FOLogic.dest_Trueprop (hd (prems_of elim));


149 

6112

150 
val Const(big_rec_name, _) = head_of data;


151 

6070

152 
val simps = case_eqns @ recursor_eqns;


153 


154 
val dt_info =


155 
{inductive = true,


156 
constructors = constructors,


157 
rec_rewrites = recursor_eqns,


158 
case_rewrites = case_eqns,


159 
induct = induct,


160 
mutual_induct = TrueI, (*No need for mutual induction*)


161 
exhaustion = elim};


162 


163 
val con_info =


164 
{big_rec_name = big_rec_name,


165 
constructors = constructors,


166 
(*let primrec handle definition by cases*)

6141

167 
free_iffs = [], (*thus we expect the necessary freeness rewrites


168 
to be in the simpset already, as is the case for


169 
Nat and disjoint sum*)

6070

170 
rec_rewrites = (case recursor_eqns of


171 
[] => case_eqns  _ => recursor_eqns)};


172 


173 
(*associate with each constructor the datatype name and rewrites*)


174 
val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors


175 


176 
in


177 
thy > Theory.add_path (Sign.base_name big_rec_name)

6092

178 
> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]

6070

179 
> DatatypesData.put


180 
(Symtab.update


181 
((big_rec_name, dt_info), DatatypesData.get thy))


182 
> ConstructorsData.put


183 
(foldr Symtab.update (con_pairs, ConstructorsData.get thy))


184 
> Theory.parent_path


185 
end


186 
handle _ => error "Failure in rep_datatype";


187 

6065

188 
end;


189 


190 

6070

191 
val exhaust_tac = DatatypeTactics.exhaust_tac;


192 
val induct_tac = DatatypeTactics.induct_tac;
