author paulson Fri Apr 10 13:15:28 1998 +0200 (1998-04-10 ago) changeset 4804 02b7c759159b parent 4352 7ac9f3e8a97d child 4860 3692eb8a6cdb permissions -rw-r--r--
Fixed bug in inductive sections to allow disjunctive premises;
```     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 * 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
```
```    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 SU =                  (** Description of a disjoint sum **)
```
```    39   sig
```
```    40   val sum       : term                  (*disjoint sum operator*)
```
```    41   val inl       : term                  (*left injection*)
```
```    42   val inr       : term                  (*right injection*)
```
```    43   val elim      : term                  (*case operator*)
```
```    44   val case_inl  : thm                   (*inl equality rule for case*)
```
```    45   val case_inr  : thm                   (*inr equality rule for case*)
```
```    46   val inl_iff   : thm                   (*injectivity of inl, using <->*)
```
```    47   val inr_iff   : thm                   (*injectivity of inr, using <->*)
```
```    48   val distinct  : thm                   (*distinctness of inl, inr using <->*)
```
```    49   val distinct' : thm                   (*distinctness of inr, inl using <->*)
```
```    50   val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
```
```    51   end;
```
```    52
```
```    53 signature ADD_INDUCTIVE_DEF =
```
```    54   sig
```
```    55   val add_fp_def_i : term list * term * term list -> theory -> theory
```
```    56   val add_constructs_def :
```
```    57         string list * ((string*typ*mixfix) *
```
```    58                        string * term list * term list) list list ->
```
```    59         theory -> theory
```
```    60   end;
```
```    61
```
```    62
```
```    63
```
```    64 (*Declares functions to add fixedpoint/constructor defs to a theory*)
```
```    65 functor Add_inductive_def_Fun
```
```    66     (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
```
```    67     : ADD_INDUCTIVE_DEF =
```
```    68 struct
```
```    69 open Logic Ind_Syntax;
```
```    70
```
```    71 (*internal version*)
```
```    72 fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy =
```
```    73   let
```
```    74     val dummy = (*has essential ancestors?*)
```
```    75 	require_thy thy "Inductive" "(co)inductive definitions"
```
```    76
```
```    77     val sign = sign_of thy;
```
```    78
```
```    79     (*recT and rec_params should agree for all mutually recursive components*)
```
```    80     val rec_hds = map head_of rec_tms;
```
```    81
```
```    82     val dummy = assert_all is_Const rec_hds
```
```    83             (fn t => "Recursive set not previously declared as constant: " ^
```
```    84                      Sign.string_of_term sign t);
```
```    85
```
```    86     (*Now we know they are all Consts, so get their names, type and params*)
```
```    87     val rec_names = map (#1 o dest_Const) rec_hds
```
```    88     and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
```
```    89
```
```    90     val rec_base_names = map Sign.base_name rec_names;
```
```    91     val dummy = assert_all Syntax.is_identifier rec_base_names
```
```    92       (fn a => "Base name of recursive set not an identifier: " ^ a);
```
```    93
```
```    94     local (*Checking the introduction rules*)
```
```    95       val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
```
```    96       fun intr_ok set =
```
```    97           case head_of set of Const(a,recT) => a mem rec_names | _ => false;
```
```    98     in
```
```    99       val dummy =  assert_all intr_ok intr_sets
```
```   100          (fn t => "Conclusion of rule does not name a recursive set: " ^
```
```   101                   Sign.string_of_term sign t);
```
```   102     end;
```
```   103
```
```   104     val dummy = assert_all is_Free rec_params
```
```   105         (fn t => "Param in recursion term not a free variable: " ^
```
```   106                  Sign.string_of_term sign t);
```
```   107
```
```   108     (*** Construct the lfp definition ***)
```
```   109     val mk_variant = variant (foldr add_term_names (intr_tms,[]));
```
```   110
```
```   111     val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
```
```   112
```
```   113     fun dest_tprop (Const("Trueprop",_) \$ P) = P
```
```   114       | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
```
```   115                               Sign.string_of_term sign Q);
```
```   116
```
```   117     (*Makes a disjunct from an introduction rule*)
```
```   118     fun lfp_part intr = (*quantify over rule's free vars except parameters*)
```
```   119       let val prems = map dest_tprop (strip_imp_prems intr)
```
```   120           val dummy = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
```
```   121           val exfrees = term_frees intr \\ rec_params
```
```   122           val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
```
```   123       in foldr FOLogic.mk_exists
```
```   124 	       (exfrees, fold_bal (app FOLogic.conj) (zeq::prems))
```
```   125       end;
```
```   126
```
```   127     (*The Part(A,h) terms -- compose injections to make h*)
```
```   128     fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
```
```   129       | mk_Part h         = Part_const \$ Free(X',iT) \$ Abs(w',iT,h);
```
```   130
```
```   131     (*Access to balanced disjoint sums via injections*)
```
```   132     val parts =
```
```   133         map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0)
```
```   134                                   (length rec_tms));
```
```   135
```
```   136     (*replace each set by the corresponding Part(A,h)*)
```
```   137     val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
```
```   138
```
```   139     val lfp_abs = absfree(X', iT,
```
```   140                      mk_Collect(z', dom_sum,
```
```   141 				fold_bal (app FOLogic.disj) part_intrs));
```
```   142
```
```   143     val lfp_rhs = Fp.oper \$ dom_sum \$ lfp_abs
```
```   144
```
```   145     val dummy = seq (fn rec_hd => deny (rec_hd occs lfp_rhs)
```
```   146                                "Illegal occurrence of recursion operator")
```
```   147              rec_hds;
```
```   148
```
```   149     (*** Make the new theory ***)
```
```   150
```
```   151     (*A key definition:
```
```   152       If no mutual recursion then it equals the one recursive set.
```
```   153       If mutual recursion then it differs from all the recursive sets. *)
```
```   154     val big_rec_base_name = space_implode "_" rec_base_names;
```
```   155     val big_rec_name = Sign.intern_const sign big_rec_base_name;
```
```   156
```
```   157     (*Big_rec... is the union of the mutually recursive sets*)
```
```   158     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
```
```   159
```
```   160     (*The individual sets must already be declared*)
```
```   161     val axpairs = map mk_defpair
```
```   162           ((big_rec_tm, lfp_rhs) ::
```
```   163            (case parts of
```
```   164                [_] => []                        (*no mutual recursion*)
```
```   165              | _ => rec_tms ~~          (*define the sets as Parts*)
```
```   166                     map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
```
```   167
```
```   168     (*tracing: print the fixedpoint definition*)
```
```   169     val _ = if !Ind_Syntax.trace then
```
```   170 		seq (writeln o Sign.string_of_term sign o #2) axpairs
```
```   171             else ()
```
```   172
```
```   173   in  thy |> PureThy.add_store_defs_i axpairs  end
```
```   174
```
```   175
```
```   176 (*Expects the recursive sets to have been defined already.
```
```   177   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
```
```   178 fun add_constructs_def (rec_base_names, con_ty_lists) thy =
```
```   179   let
```
```   180     val dummy = (*has essential ancestors?*)
```
```   181       require_thy thy "Datatype" "(co)datatype definitions";
```
```   182
```
```   183     val sign = sign_of thy;
```
```   184     val full_name = Sign.full_name sign;
```
```   185
```
```   186     val dummy = writeln"  Defining the constructor functions...";
```
```   187     val case_name = "f";                (*name for case variables*)
```
```   188
```
```   189
```
```   190     (** Define the constructors **)
```
```   191
```
```   192     (*The empty tuple is 0*)
```
```   193     fun mk_tuple [] = Const("0",iT)
```
```   194       | mk_tuple args = foldr1 (app Pr.pair) args;
```
```   195
```
```   196     fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
```
```   197
```
```   198     val npart = length rec_base_names;       (*total # of mutually recursive parts*)
```
```   199
```
```   200     (*Make constructor definition; kpart is # of this mutually recursive part*)
```
```   201     fun mk_con_defs (kpart, con_ty_list) =
```
```   202       let val ncon = length con_ty_list    (*number of constructors*)
```
```   203           fun mk_def (((id,T,syn), name, args, prems), kcon) =
```
```   204                 (*kcon is index of constructor*)
```
```   205               mk_defpair (list_comb (Const (full_name name, T), args),
```
```   206                           mk_inject npart kpart
```
```   207                           (mk_inject ncon kcon (mk_tuple args)))
```
```   208       in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
```
```   209
```
```   210     (** Define the case operator **)
```
```   211
```
```   212     (*Combine split terms using case; yields the case operator for one part*)
```
```   213     fun call_case case_list =
```
```   214       let fun call_f (free,[]) = Abs("null", iT, free)
```
```   215             | call_f (free,args) =
```
```   216                   CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
```
```   217                               Ind_Syntax.iT
```
```   218                               free
```
```   219       in  fold_bal (app Su.elim) (map call_f case_list)  end;
```
```   220
```
```   221     (** Generating function variables for the case definition
```
```   222         Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
```
```   223
```
```   224     (*Treatment of a single constructor*)
```
```   225     fun add_case (((_, T, _), name, args, prems), (opno, cases)) =
```
```   226       if Syntax.is_identifier name then
```
```   227         (opno, (Free (case_name ^ "_" ^ name, T), args) :: cases)
```
```   228       else
```
```   229         (opno + 1, (Free (case_name ^ "_op_" ^ string_of_int opno, T), args) :: 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_base_name = space_implode "_" rec_base_names;
```
```   242     val big_case_base_name = big_rec_base_name ^ "_case";
```
```   243     val big_case_name = full_name big_case_base_name;
```
```   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
```
```   255     (* Build the new theory *)
```
```   256
```
```   257     val const_decs =
```
```   258       (big_case_base_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
```
```   259
```
```   260     val axpairs =
```
```   261       big_case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists));
```
```   262
```
```   263   in
```
```   264     thy
```
```   265     |> Theory.add_consts_i const_decs
```
```   266     |> PureThy.add_store_defs_i axpairs
```
```   267   end;
```
```   268
```
```   269
```
```   270 end;
```