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