516

1 
(* Title: ZF/add_ind_def.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1994 University of Cambridge


5 


6 
Fixedpoint definition module  for Inductive/Coinductive Definitions


7 


8 
Features:


9 
* least or greatest fixedpoints


10 
* userspecified product and sum constructions


11 
* mutually recursive definitions


12 
* definitions involving arbitrary monotone operators


13 
* automatically proves introduction and elimination rules


14 


15 
The recursive sets must *already* be declared as constants in parent theory!


16 


17 
Introduction rules have the form


18 
[ ti:M(Sj), ..., P(x), ... ] ==> t: Sk ]


19 
where M is some monotone operator (usually the identity)


20 
P(x) is any (nonconjunctive) side condition on the free variables


21 
ti, t are any terms


22 
Sj, Sk are two of the sets being defined in mutual recursion


23 


24 
Sums are used only for mutual recursion;


25 
Products are used only to derive "streamlined" induction rules for relations


26 
*)


27 


28 
signature FP = (** Description of a fixed point operator **)


29 
sig


30 
val oper : term (*fixed point operator*)


31 
val bnd_mono : term (*monotonicity predicate*)


32 
val bnd_monoI : thm (*intro rule for bnd_mono*)


33 
val subs : thm (*subset theorem for fp*)


34 
val Tarski : thm (*Tarski's fixed point theorem*)


35 
val induct : thm (*induction/coinduction rule*)


36 
end;


37 


38 
signature PR = (** Description of a Cartesian product **)


39 
sig


40 
val sigma : term (*Cartesian product operator*)


41 
val pair : term (*pairing operator*)


42 
val split_const : term (*splitting operator*)


43 
val fsplit_const : term (*splitting operator for formulae*)


44 
val pair_iff : thm (*injectivity of pairing, using <>*)


45 
val split_eq : thm (*equality rule for split*)


46 
val fsplitI : thm (*intro rule for fsplit*)


47 
val fsplitD : thm (*destruct rule for fsplit*)


48 
val fsplitE : thm (*elim rule for fsplit*)


49 
end;


50 


51 
signature SU = (** Description of a disjoint sum **)


52 
sig


53 
val sum : term (*disjoint sum operator*)


54 
val inl : term (*left injection*)


55 
val inr : term (*right injection*)


56 
val elim : term (*case operator*)


57 
val case_inl : thm (*inl equality rule for case*)


58 
val case_inr : thm (*inr equality rule for case*)


59 
val inl_iff : thm (*injectivity of inl, using <>*)


60 
val inr_iff : thm (*injectivity of inr, using <>*)


61 
val distinct : thm (*distinctness of inl, inr using <>*)


62 
val distinct' : thm (*distinctness of inr, inl using <>*)


63 
end;


64 


65 
signature ADD_INDUCTIVE_DEF =


66 
sig


67 
val add_fp_def_i : term list * term list * term list > theory > theory


68 
val add_fp_def : (string*string) list * string list > theory > theory


69 
val add_constructs_def :


70 
string list * ((string*typ*mixfix) *


71 
string * term list * term list) list list >


72 
theory > theory


73 
end;


74 


75 


76 


77 
(*Declares functions to add fixedpoint/constructor defs to a theory*)


78 
functor Add_inductive_def_Fun


79 
(structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =


80 
struct


81 
open Logic Ind_Syntax;


82 


83 
(*internal version*)


84 
fun add_fp_def_i (rec_tms, domts, intr_tms) thy =


85 
let


86 
val sign = sign_of thy;


87 


88 
(*recT and rec_params should agree for all mutually recursive components*)


89 
val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)


90 
and rec_hds = map head_of rec_tms;


91 


92 
val rec_names = map (#1 o dest_Const) rec_hds;


93 


94 
val _ = assert_all Syntax.is_identifier rec_names


95 
(fn a => "Name of recursive set not an identifier: " ^ a);


96 


97 
val _ = assert_all (is_some o lookup_const sign) rec_names


98 
(fn a => "Recursive set not previously declared as constant: " ^ a);


99 


100 
local (*Checking the introduction rules*)


101 
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;


102 
fun intr_ok set =


103 
case head_of set of Const(a,recT) => a mem rec_names  _ => false;


104 
in


105 
val _ = assert_all intr_ok intr_sets


106 
(fn t => "Conclusion of rule does not name a recursive set: " ^


107 
Sign.string_of_term sign t);


108 
end;


109 


110 
val _ = assert_all is_Free rec_params


111 
(fn t => "Param in recursion term not a free variable: " ^


112 
Sign.string_of_term sign t);


113 


114 
(*** Construct the lfp definition ***)


115 
val mk_variant = variant (foldr add_term_names (intr_tms,[]));


116 


117 
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";


118 


119 
fun dest_tprop (Const("Trueprop",_) $ P) = P


120 
 dest_tprop Q = error ("Illformed premise of introduction rule: " ^


121 
Sign.string_of_term sign Q);


122 


123 
(*Makes a disjunct from an introduction rule*)


124 
fun lfp_part intr = (*quantify over rule's free vars except parameters*)


125 
let val prems = map dest_tprop (strip_imp_prems intr)


126 
val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds


127 
val exfrees = term_frees intr \\ rec_params


128 
val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))


129 
in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;


130 


131 
val dom_sum = fold_bal (app Su.sum) domts;


132 


133 
(*The Part(A,h) terms  compose injections to make h*)


134 
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)


135 
 mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);


136 


137 
(*Access to balanced disjoint sums via injections*)


138 
val parts =


139 
map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)


140 
(length rec_tms));


141 


142 
(*replace each set by the corresponding Part(A,h)*)


143 
val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;


144 


145 
val lfp_abs = absfree(X', iT,


146 
mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));


147 


148 
val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs


149 


150 
val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)


151 
"Illegal occurrence of recursion operator")


152 
rec_hds;


153 


154 
(*** Make the new theory ***)


155 


156 
(*A key definition:


157 
If no mutual recursion then it equals the one recursive set.


158 
If mutual recursion then it differs from all the recursive sets. *)


159 
val big_rec_name = space_implode "_" rec_names;


160 


161 
(*Big_rec... is the union of the mutually recursive sets*)


162 
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);


163 


164 
(*The individual sets must already be declared*)


165 
val axpairs = map mk_defpair


166 
((big_rec_tm, lfp_rhs) ::


167 
(case parts of


168 
[_] => [] (*no mutual recursion*)


169 
 _ => rec_tms ~~ (*define the sets as Parts*)


170 
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));


171 

567

172 
in thy > add_defs_i axpairs end

516

173 


174 


175 
(*external, stringbased version; needed?*)


176 
fun add_fp_def (rec_doms, sintrs) thy =


177 
let val sign = sign_of thy;


178 
val rec_tms = map (readtm sign iT o fst) rec_doms


179 
and domts = map (readtm sign iT o snd) rec_doms


180 
val intr_tms = map (readtm sign propT) sintrs


181 
in add_fp_def_i (rec_tms, domts, intr_tms) thy end


182 


183 


184 
(*Expects the recursive sets to have been defined already.


185 
con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)


186 
fun add_constructs_def (rec_names, con_ty_lists) thy =


187 
let


188 
val _ = writeln" Defining the constructor functions...";


189 
val case_name = "f"; (*name for case variables*)


190 


191 
(** Define the constructors **)


192 


193 
(*The empty tuple is 0*)


194 
fun mk_tuple [] = Const("0",iT)


195 
 mk_tuple args = foldr1 (app Pr.pair) args;


196 


197 
fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;


198 


199 
val npart = length rec_names; (*total # of mutually recursive parts*)


200 


201 
(*Make constructor definition; kpart is # of this mutually recursive part*)


202 
fun mk_con_defs (kpart, con_ty_list) =


203 
let val ncon = length con_ty_list (*number of constructors*)


204 
fun mk_def (((id,T,syn), name, args, prems), kcon) =


205 
(*kcon is index of constructor*)


206 
mk_defpair (list_comb (Const(name,T), args),


207 
mk_inject npart kpart


208 
(mk_inject ncon kcon (mk_tuple args)))


209 
in map mk_def (con_ty_list ~~ (1 upto ncon)) end;


210 


211 
(** Define the case operator **)


212 


213 
(*Combine split terms using case; yields the case operator for one part*)


214 
fun call_case case_list =


215 
let fun call_f (free,args) =


216 
ap_split Pr.split_const free (map (#2 o dest_Free) args)


217 
in fold_bal (app Su.elim) (map call_f case_list) end;


218 


219 
(** Generating function variables for the case definition


220 
Nonidentifiers (e.g. infixes) get a name of the form f_op_nnn. **)


221 


222 
(*Treatment of a single constructor*)


223 
fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =


224 
if Syntax.is_identifier id


225 
then (opno,


226 
(Free(case_name ^ "_" ^ id, T), args) :: cases)


227 
else (opno+1,


228 
(Free(case_name ^ "_op_" ^ string_of_int opno, T), args) ::


229 
cases)


230 


231 
(*Treatment of a list of constructors, for one part*)


232 
fun add_case_list (con_ty_list, (opno,case_lists)) =


233 
let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))


234 
in (opno', case_list :: case_lists) end;


235 


236 
(*Treatment of all parts*)


237 
val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));


238 


239 
val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) > (iT>iT);


240 


241 
val big_rec_name = space_implode "_" rec_names;


242 


243 
val big_case_name = big_rec_name ^ "_case";


244 


245 
(*The list of all the function variables*)


246 
val big_case_args = flat (map (map #1) case_lists);


247 


248 
val big_case_tm =


249 
list_comb (Const(big_case_name, big_case_typ), big_case_args);


250 


251 
val big_case_def = mk_defpair


252 
(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists));


253 


254 
(** Build the new theory **)


255 


256 
val const_decs =


257 
(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);


258 


259 
val axpairs =


260 
big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))


261 

567

262 
in thy > add_consts_i const_decs > add_defs_i axpairs end;

516

263 
end;
