src/ZF/add_ind_def.ML
changeset 1735 96244c247b07
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
equal deleted inserted replaced
1734:604da1a11a99 1735:96244c247b07
    31   val bnd_mono  : term                  (*monotonicity predicate*)
    31   val bnd_mono  : term                  (*monotonicity predicate*)
    32   val bnd_monoI : thm                   (*intro rule for bnd_mono*)
    32   val bnd_monoI : thm                   (*intro rule for bnd_mono*)
    33   val subs      : thm                   (*subset theorem for fp*)
    33   val subs      : thm                   (*subset theorem for fp*)
    34   val Tarski    : thm                   (*Tarski's fixed point theorem*)
    34   val Tarski    : thm                   (*Tarski's fixed point theorem*)
    35   val induct    : thm                   (*induction/coinduction rule*)
    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; apparently never used*)
       
    49   end;
    36   end;
    50 
    37 
    51 signature SU =                  (** Description of a disjoint sum **)
    38 signature SU =                  (** Description of a disjoint sum **)
    52   sig
    39   sig
    53   val sum       : term                  (*disjoint sum operator*)
    40   val sum       : term                  (*disjoint sum operator*)
    74 
    61 
    75 
    62 
    76 
    63 
    77 (*Declares functions to add fixedpoint/constructor defs to a theory*)
    64 (*Declares functions to add fixedpoint/constructor defs to a theory*)
    78 functor Add_inductive_def_Fun 
    65 functor Add_inductive_def_Fun 
    79     (structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =
    66     (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU)
       
    67     : ADD_INDUCTIVE_DEF =
    80 struct
    68 struct
    81 open Logic Ind_Syntax;
    69 open Logic Ind_Syntax;
    82 
    70 
    83 (*internal version*)
    71 (*internal version*)
    84 fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
    72 fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
   203 
   191 
   204     (** Define the case operator **)
   192     (** Define the case operator **)
   205 
   193 
   206     (*Combine split terms using case; yields the case operator for one part*)
   194     (*Combine split terms using case; yields the case operator for one part*)
   207     fun call_case case_list = 
   195     fun call_case case_list = 
   208       let fun call_f (free,args) = 
   196       let fun call_f (free,[]) = Abs("null", iT, free)
   209               ap_split Pr.split_const free (map (#2 o dest_Free) args)
   197 	    | call_f (free,args) =
       
   198                   CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
       
   199 		              Ind_Syntax.iT 
       
   200 			      free 
   210       in  fold_bal (app Su.elim) (map call_f case_list)  end;
   201       in  fold_bal (app Su.elim) (map call_f case_list)  end;
   211 
   202 
   212     (** Generating function variables for the case definition
   203     (** Generating function variables for the case definition
   213         Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   204         Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   214 
   205