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