clasohm@1461 ` 1` ```(* Title: ZF/add_ind_def.ML ``` lcp@516 ` 2` ``` ID: \$Id\$ ``` clasohm@1461 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` lcp@516 ` 4` ``` Copyright 1994 University of Cambridge ``` lcp@516 ` 5` lcp@516 ` 6` ```Fixedpoint definition module -- for Inductive/Coinductive Definitions ``` lcp@516 ` 7` lcp@516 ` 8` ```Features: ``` lcp@516 ` 9` ```* least or greatest fixedpoints ``` lcp@516 ` 10` ```* user-specified product and sum constructions ``` lcp@516 ` 11` ```* mutually recursive definitions ``` lcp@516 ` 12` ```* definitions involving arbitrary monotone operators ``` lcp@516 ` 13` ```* automatically proves introduction and elimination rules ``` lcp@516 ` 14` lcp@516 ` 15` ```The recursive sets must *already* be declared as constants in parent theory! ``` lcp@516 ` 16` lcp@516 ` 17` ``` Introduction rules have the form ``` lcp@516 ` 18` ``` [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |] ``` lcp@516 ` 19` ``` where M is some monotone operator (usually the identity) ``` lcp@516 ` 20` ``` P(x) is any (non-conjunctive) side condition on the free variables ``` lcp@516 ` 21` ``` ti, t are any terms ``` lcp@516 ` 22` ``` Sj, Sk are two of the sets being defined in mutual recursion ``` lcp@516 ` 23` lcp@516 ` 24` ```Sums are used only for mutual recursion; ``` lcp@516 ` 25` ```Products are used only to derive "streamlined" induction rules for relations ``` lcp@516 ` 26` ```*) ``` lcp@516 ` 27` clasohm@1461 ` 28` ```signature FP = (** Description of a fixed point operator **) ``` lcp@516 ` 29` ``` sig ``` clasohm@1461 ` 30` ``` val oper : term (*fixed point operator*) ``` clasohm@1461 ` 31` ``` val bnd_mono : term (*monotonicity predicate*) ``` clasohm@1461 ` 32` ``` val bnd_monoI : thm (*intro rule for bnd_mono*) ``` clasohm@1461 ` 33` ``` val subs : thm (*subset theorem for fp*) ``` clasohm@1461 ` 34` ``` val Tarski : thm (*Tarski's fixed point theorem*) ``` clasohm@1461 ` 35` ``` val induct : thm (*induction/coinduction rule*) ``` lcp@516 ` 36` ``` end; ``` lcp@516 ` 37` clasohm@1461 ` 38` ```signature SU = (** Description of a disjoint sum **) ``` lcp@516 ` 39` ``` sig ``` clasohm@1461 ` 40` ``` val sum : term (*disjoint sum operator*) ``` clasohm@1461 ` 41` ``` val inl : term (*left injection*) ``` clasohm@1461 ` 42` ``` val inr : term (*right injection*) ``` clasohm@1461 ` 43` ``` val elim : term (*case operator*) ``` clasohm@1461 ` 44` ``` val case_inl : thm (*inl equality rule for case*) ``` clasohm@1461 ` 45` ``` val case_inr : thm (*inr equality rule for case*) ``` clasohm@1461 ` 46` ``` val inl_iff : thm (*injectivity of inl, using <->*) ``` clasohm@1461 ` 47` ``` val inr_iff : thm (*injectivity of inr, using <->*) ``` clasohm@1461 ` 48` ``` val distinct : thm (*distinctness of inl, inr using <->*) ``` clasohm@1461 ` 49` ``` val distinct' : thm (*distinctness of inr, inl using <->*) ``` clasohm@1461 ` 50` ``` val free_SEs : thm list (*elim rules for SU, and pair_iff!*) ``` lcp@516 ` 51` ``` end; ``` lcp@516 ` 52` lcp@516 ` 53` ```signature ADD_INDUCTIVE_DEF = ``` lcp@516 ` 54` ``` sig ``` lcp@727 ` 55` ``` val add_fp_def_i : term list * term * term list -> theory -> theory ``` lcp@516 ` 56` ``` val add_constructs_def : ``` lcp@516 ` 57` ``` string list * ((string*typ*mixfix) * ``` lcp@516 ` 58` ``` string * term list * term list) list list -> ``` lcp@516 ` 59` ``` theory -> theory ``` lcp@516 ` 60` ``` end; ``` lcp@516 ` 61` lcp@516 ` 62` lcp@516 ` 63` lcp@516 ` 64` ```(*Declares functions to add fixedpoint/constructor defs to a theory*) ``` lcp@516 ` 65` ```functor Add_inductive_def_Fun ``` paulson@1735 ` 66` ``` (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU) ``` paulson@1735 ` 67` ``` : ADD_INDUCTIVE_DEF = ``` lcp@516 ` 68` ```struct ``` lcp@516 ` 69` ```open Logic Ind_Syntax; ``` lcp@516 ` 70` lcp@516 ` 71` ```(*internal version*) ``` lcp@727 ` 72` ```fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = ``` lcp@516 ` 73` ``` let ``` paulson@2871 ` 74` ``` val dummy = (*has essential ancestors?*) ``` paulson@2871 ` 75` ``` require_thy thy "Inductive" "(co)inductive definitions" ``` paulson@2871 ` 76` lcp@516 ` 77` ``` val sign = sign_of thy; ``` lcp@516 ` 78` lcp@516 ` 79` ``` (*recT and rec_params should agree for all mutually recursive components*) ``` lcp@750 ` 80` ``` val rec_hds = map head_of rec_tms; ``` lcp@516 ` 81` paulson@2871 ` 82` ``` val dummy = assert_all is_Const rec_hds ``` clasohm@1461 ` 83` ``` (fn t => "Recursive set not previously declared as constant: " ^ ``` clasohm@1461 ` 84` ``` Sign.string_of_term sign t); ``` lcp@750 ` 85` lcp@750 ` 86` ``` (*Now we know they are all Consts, so get their names, type and params*) ``` lcp@750 ` 87` ``` val rec_names = map (#1 o dest_Const) rec_hds ``` lcp@750 ` 88` ``` and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); ``` lcp@516 ` 89` wenzelm@3939 ` 90` ``` val rec_base_names = map Sign.base_name rec_names; ``` wenzelm@3925 ` 91` ``` val dummy = assert_all Syntax.is_identifier rec_base_names ``` wenzelm@3925 ` 92` ``` (fn a => "Base name of recursive set not an identifier: " ^ a); ``` lcp@516 ` 93` lcp@516 ` 94` ``` local (*Checking the introduction rules*) ``` lcp@516 ` 95` ``` val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; ``` lcp@516 ` 96` ``` fun intr_ok set = ``` clasohm@1461 ` 97` ``` case head_of set of Const(a,recT) => a mem rec_names | _ => false; ``` lcp@516 ` 98` ``` in ``` paulson@2871 ` 99` ``` val dummy = assert_all intr_ok intr_sets ``` clasohm@1461 ` 100` ``` (fn t => "Conclusion of rule does not name a recursive set: " ^ ``` clasohm@1461 ` 101` ``` Sign.string_of_term sign t); ``` lcp@516 ` 102` ``` end; ``` lcp@516 ` 103` paulson@2871 ` 104` ``` val dummy = assert_all is_Free rec_params ``` clasohm@1461 ` 105` ``` (fn t => "Param in recursion term not a free variable: " ^ ``` clasohm@1461 ` 106` ``` Sign.string_of_term sign t); ``` lcp@516 ` 107` lcp@516 ` 108` ``` (*** Construct the lfp definition ***) ``` lcp@516 ` 109` ``` val mk_variant = variant (foldr add_term_names (intr_tms,[])); ``` lcp@516 ` 110` lcp@516 ` 111` ``` val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; ``` lcp@516 ` 112` lcp@516 ` 113` ``` fun dest_tprop (Const("Trueprop",_) \$ P) = P ``` lcp@516 ` 114` ``` | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ ``` clasohm@1461 ` 115` ``` Sign.string_of_term sign Q); ``` lcp@516 ` 116` lcp@516 ` 117` ``` (*Makes a disjunct from an introduction rule*) ``` lcp@516 ` 118` ``` fun lfp_part intr = (*quantify over rule's free vars except parameters*) ``` lcp@516 ` 119` ``` let val prems = map dest_tprop (strip_imp_prems intr) ``` paulson@2871 ` 120` ``` val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds ``` clasohm@1461 ` 121` ``` val exfrees = term_frees intr \\ rec_params ``` paulson@4352 ` 122` ``` val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr)) ``` paulson@4352 ` 123` ``` in foldr FOLogic.mk_exists ``` paulson@4352 ` 124` ``` (exfrees, fold_bal (app FOLogic.conj) (zeq::prems)) ``` paulson@4352 ` 125` ``` end; ``` lcp@516 ` 126` lcp@516 ` 127` ``` (*The Part(A,h) terms -- compose injections to make h*) ``` clasohm@1461 ` 128` ``` fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) ``` lcp@516 ` 129` ``` | mk_Part h = Part_const \$ Free(X',iT) \$ Abs(w',iT,h); ``` lcp@516 ` 130` lcp@516 ` 131` ``` (*Access to balanced disjoint sums via injections*) ``` lcp@516 ` 132` ``` val parts = ``` clasohm@1461 ` 133` ``` map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) ``` clasohm@1461 ` 134` ``` (length rec_tms)); ``` lcp@516 ` 135` lcp@516 ` 136` ``` (*replace each set by the corresponding Part(A,h)*) ``` lcp@516 ` 137` ``` val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms; ``` lcp@516 ` 138` lcp@516 ` 139` ``` val lfp_abs = absfree(X', iT, ``` paulson@4352 ` 140` ``` mk_Collect(z', dom_sum, ``` paulson@4352 ` 141` ``` fold_bal (app FOLogic.disj) part_intrs)); ``` lcp@516 ` 142` lcp@516 ` 143` ``` val lfp_rhs = Fp.oper \$ dom_sum \$ lfp_abs ``` lcp@516 ` 144` paulson@2871 ` 145` ``` val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) ``` clasohm@1461 ` 146` ``` "Illegal occurrence of recursion operator") ``` clasohm@1461 ` 147` ``` rec_hds; ``` lcp@516 ` 148` lcp@516 ` 149` ``` (*** Make the new theory ***) ``` lcp@516 ` 150` lcp@516 ` 151` ``` (*A key definition: ``` lcp@516 ` 152` ``` If no mutual recursion then it equals the one recursive set. ``` lcp@516 ` 153` ``` If mutual recursion then it differs from all the recursive sets. *) ``` wenzelm@3925 ` 154` ``` val big_rec_base_name = space_implode "_" rec_base_names; ``` wenzelm@4235 ` 155` ``` val big_rec_name = Sign.intern_const sign big_rec_base_name; ``` lcp@516 ` 156` lcp@516 ` 157` ``` (*Big_rec... is the union of the mutually recursive sets*) ``` lcp@516 ` 158` ``` val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); ``` lcp@516 ` 159` lcp@516 ` 160` ``` (*The individual sets must already be declared*) ``` lcp@516 ` 161` ``` val axpairs = map mk_defpair ``` clasohm@1461 ` 162` ``` ((big_rec_tm, lfp_rhs) :: ``` clasohm@1461 ` 163` ``` (case parts of ``` clasohm@1461 ` 164` ``` [_] => [] (*no mutual recursion*) ``` clasohm@1461 ` 165` ``` | _ => rec_tms ~~ (*define the sets as Parts*) ``` clasohm@1461 ` 166` ``` map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); ``` lcp@516 ` 167` paulson@4804 ` 168` ``` (*tracing: print the fixedpoint definition*) ``` paulson@4804 ` 169` ``` val _ = if !Ind_Syntax.trace then ``` paulson@4804 ` 170` ``` seq (writeln o Sign.string_of_term sign o #2) axpairs ``` paulson@4804 ` 171` ``` else () ``` paulson@4804 ` 172` wenzelm@4027 ` 173` ``` in thy |> PureThy.add_store_defs_i axpairs end ``` lcp@516 ` 174` lcp@516 ` 175` lcp@516 ` 176` ```(*Expects the recursive sets to have been defined already. ``` lcp@516 ` 177` ``` con_ty_lists specifies the constructors in the form (name,prems,mixfix) *) ``` wenzelm@3925 ` 178` ```fun add_constructs_def (rec_base_names, con_ty_lists) thy = ``` lcp@516 ` 179` ``` let ``` paulson@2871 ` 180` ``` val dummy = (*has essential ancestors?*) ``` wenzelm@3925 ` 181` ``` require_thy thy "Datatype" "(co)datatype definitions"; ``` wenzelm@3925 ` 182` wenzelm@3925 ` 183` ``` val sign = sign_of thy; ``` wenzelm@3925 ` 184` ``` val full_name = Sign.full_name sign; ``` paulson@2871 ` 185` paulson@2871 ` 186` ``` val dummy = writeln" Defining the constructor functions..."; ``` clasohm@1461 ` 187` ``` val case_name = "f"; (*name for case variables*) ``` lcp@516 ` 188` wenzelm@3925 ` 189` lcp@516 ` 190` ``` (** Define the constructors **) ``` lcp@516 ` 191` lcp@516 ` 192` ``` (*The empty tuple is 0*) ``` lcp@516 ` 193` ``` fun mk_tuple [] = Const("0",iT) ``` lcp@516 ` 194` ``` | mk_tuple args = foldr1 (app Pr.pair) args; ``` lcp@516 ` 195` wenzelm@3925 ` 196` ``` fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k; ``` lcp@516 ` 197` wenzelm@3925 ` 198` ``` val npart = length rec_base_names; (*total # of mutually recursive parts*) ``` lcp@516 ` 199` lcp@516 ` 200` ``` (*Make constructor definition; kpart is # of this mutually recursive part*) ``` lcp@516 ` 201` ``` fun mk_con_defs (kpart, con_ty_list) = ``` clasohm@1461 ` 202` ``` let val ncon = length con_ty_list (*number of constructors*) ``` clasohm@1461 ` 203` ``` fun mk_def (((id,T,syn), name, args, prems), kcon) = ``` clasohm@1461 ` 204` ``` (*kcon is index of constructor*) ``` wenzelm@3925 ` 205` ``` mk_defpair (list_comb (Const (full_name name, T), args), ``` clasohm@1461 ` 206` ``` mk_inject npart kpart ``` clasohm@1461 ` 207` ``` (mk_inject ncon kcon (mk_tuple args))) ``` paulson@2266 ` 208` ``` in ListPair.map mk_def (con_ty_list, 1 upto ncon) end; ``` lcp@516 ` 209` lcp@516 ` 210` ``` (** Define the case operator **) ``` lcp@516 ` 211` lcp@516 ` 212` ``` (*Combine split terms using case; yields the case operator for one part*) ``` lcp@516 ` 213` ``` fun call_case case_list = ``` paulson@1735 ` 214` ``` let fun call_f (free,[]) = Abs("null", iT, free) ``` paulson@2033 ` 215` ``` | call_f (free,args) = ``` paulson@1735 ` 216` ``` CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args)) ``` paulson@2033 ` 217` ``` Ind_Syntax.iT ``` paulson@2033 ` 218` ``` free ``` lcp@516 ` 219` ``` in fold_bal (app Su.elim) (map call_f case_list) end; ``` lcp@516 ` 220` lcp@516 ` 221` ``` (** Generating function variables for the case definition ``` clasohm@1461 ` 222` ``` Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **) ``` lcp@516 ` 223` lcp@516 ` 224` ``` (*Treatment of a single constructor*) ``` wenzelm@3925 ` 225` ``` fun add_case (((_, T, _), name, args, prems), (opno, cases)) = ``` wenzelm@3925 ` 226` ``` if Syntax.is_identifier name then ``` wenzelm@3925 ` 227` ``` (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases) ``` wenzelm@3925 ` 228` ``` else ``` wenzelm@3925 ` 229` ``` (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: cases); ``` lcp@516 ` 230` lcp@516 ` 231` ``` (*Treatment of a list of constructors, for one part*) ``` wenzelm@3925 ` 232` ``` fun add_case_list (con_ty_list, (opno, case_lists)) = ``` wenzelm@3925 ` 233` ``` let val (opno', case_list) = foldr add_case (con_ty_list, (opno, [])) ``` wenzelm@3925 ` 234` ``` in (opno', case_list :: case_lists) end; ``` lcp@516 ` 235` lcp@516 ` 236` ``` (*Treatment of all parts*) ``` lcp@516 ` 237` ``` val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[])); ``` lcp@516 ` 238` lcp@516 ` 239` ``` val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT); ``` lcp@516 ` 240` wenzelm@3925 ` 241` ``` val big_rec_base_name = space_implode "_" rec_base_names; ``` wenzelm@3925 ` 242` ``` val big_case_base_name = big_rec_base_name ^ "_case"; ``` wenzelm@3925 ` 243` ``` val big_case_name = full_name big_case_base_name; ``` lcp@516 ` 244` lcp@516 ` 245` ``` (*The list of all the function variables*) ``` lcp@516 ` 246` ``` val big_case_args = flat (map (map #1) case_lists); ``` lcp@516 ` 247` wenzelm@3925 ` 248` ``` val big_case_tm = ``` wenzelm@3925 ` 249` ``` list_comb (Const (big_case_name, big_case_typ), big_case_args); ``` lcp@516 ` 250` wenzelm@3925 ` 251` ``` val big_case_def = mk_defpair ``` wenzelm@3925 ` 252` ``` (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); ``` lcp@516 ` 253` wenzelm@3925 ` 254` wenzelm@3925 ` 255` ``` (* Build the new theory *) ``` lcp@516 ` 256` lcp@516 ` 257` ``` val const_decs = ``` wenzelm@3925 ` 258` ``` (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists); ``` lcp@516 ` 259` lcp@516 ` 260` ``` val axpairs = ``` wenzelm@3925 ` 261` ``` big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)); ``` lcp@516 ` 262` wenzelm@3925 ` 263` ``` in ``` wenzelm@3925 ` 264` ``` thy ``` wenzelm@3925 ` 265` ``` |> Theory.add_consts_i const_decs ``` wenzelm@4027 ` 266` ``` |> PureThy.add_store_defs_i axpairs ``` wenzelm@3925 ` 267` ``` end; ``` wenzelm@3925 ` 268` wenzelm@3925 ` 269` lcp@516 ` 270` ```end; ```