src/ZF/add_ind_def.ML
changeset 1461 6bcb44e4d6e5
parent 1418 f5f97ee67cbb
child 1735 96244c247b07
equal deleted inserted replaced
1460:5a6f2aabd538 1461:6bcb44e4d6e5
     1 (*  Title: 	ZF/add_ind_def.ML
     1 (*  Title:      ZF/add_ind_def.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 Fixedpoint definition module -- for Inductive/Coinductive Definitions
     6 Fixedpoint definition module -- for Inductive/Coinductive Definitions
     7 
     7 
     8 Features:
     8 Features:
    23 
    23 
    24 Sums are used only for mutual recursion;
    24 Sums are used only for mutual recursion;
    25 Products are used only to derive "streamlined" induction rules for relations
    25 Products are used only to derive "streamlined" induction rules for relations
    26 *)
    26 *)
    27 
    27 
    28 signature FP =		(** Description of a fixed point operator **)
    28 signature FP =          (** Description of a fixed point operator **)
    29   sig
    29   sig
    30   val oper	: term			(*fixed point operator*)
    30   val oper      : term                  (*fixed point operator*)
    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;
    36   end;
    37 
    37 
    38 signature PR =			(** Description of a Cartesian product **)
    38 signature PR =                  (** Description of a Cartesian product **)
    39   sig
    39   sig
    40   val sigma	: term			(*Cartesian product operator*)
    40   val sigma     : term                  (*Cartesian product operator*)
    41   val pair	: term			(*pairing operator*)
    41   val pair      : term                  (*pairing operator*)
    42   val split_const  : term		(*splitting operator*)
    42   val split_const  : term               (*splitting operator*)
    43   val fsplit_const : term		(*splitting operator for formulae*)
    43   val fsplit_const : term               (*splitting operator for formulae*)
    44   val pair_iff	: thm			(*injectivity of pairing, using <->*)
    44   val pair_iff  : thm                   (*injectivity of pairing, using <->*)
    45   val split_eq	: thm			(*equality rule for split*)
    45   val split_eq  : thm                   (*equality rule for split*)
    46   val fsplitI	: thm			(*intro rule for fsplit*)
    46   val fsplitI   : thm                   (*intro rule for fsplit*)
    47   val fsplitD	: thm			(*destruct rule for fsplit*)
    47   val fsplitD   : thm                   (*destruct rule for fsplit*)
    48   val fsplitE	: thm			(*elim rule; apparently never used*)
    48   val fsplitE   : thm                   (*elim rule; apparently never used*)
    49   end;
    49   end;
    50 
    50 
    51 signature SU =			(** Description of a disjoint sum **)
    51 signature SU =                  (** Description of a disjoint sum **)
    52   sig
    52   sig
    53   val sum	: term			(*disjoint sum operator*)
    53   val sum       : term                  (*disjoint sum operator*)
    54   val inl	: term			(*left injection*)
    54   val inl       : term                  (*left injection*)
    55   val inr	: term			(*right injection*)
    55   val inr       : term                  (*right injection*)
    56   val elim	: term			(*case operator*)
    56   val elim      : term                  (*case operator*)
    57   val case_inl	: thm			(*inl equality rule for case*)
    57   val case_inl  : thm                   (*inl equality rule for case*)
    58   val case_inr	: thm			(*inr equality rule for case*)
    58   val case_inr  : thm                   (*inr equality rule for case*)
    59   val inl_iff	: thm			(*injectivity of inl, using <->*)
    59   val inl_iff   : thm                   (*injectivity of inl, using <->*)
    60   val inr_iff	: thm			(*injectivity of inr, using <->*)
    60   val inr_iff   : thm                   (*injectivity of inr, using <->*)
    61   val distinct	: thm			(*distinctness of inl, inr using <->*)
    61   val distinct  : thm                   (*distinctness of inl, inr using <->*)
    62   val distinct'	: thm			(*distinctness of inr, inl using <->*)
    62   val distinct' : thm                   (*distinctness of inr, inl using <->*)
    63   val free_SEs  : thm list		(*elim rules for SU, and pair_iff!*)
    63   val free_SEs  : thm list              (*elim rules for SU, and pair_iff!*)
    64   end;
    64   end;
    65 
    65 
    66 signature ADD_INDUCTIVE_DEF =
    66 signature ADD_INDUCTIVE_DEF =
    67   sig 
    67   sig 
    68   val add_fp_def_i : term list * term * term list -> theory -> theory
    68   val add_fp_def_i : term list * term * term list -> theory -> theory
    87 
    87 
    88     (*recT and rec_params should agree for all mutually recursive components*)
    88     (*recT and rec_params should agree for all mutually recursive components*)
    89     val rec_hds = map head_of rec_tms;
    89     val rec_hds = map head_of rec_tms;
    90 
    90 
    91     val _ = assert_all is_Const rec_hds
    91     val _ = assert_all is_Const rec_hds
    92 	    (fn t => "Recursive set not previously declared as constant: " ^ 
    92             (fn t => "Recursive set not previously declared as constant: " ^ 
    93 	             Sign.string_of_term sign t);
    93                      Sign.string_of_term sign t);
    94 
    94 
    95     (*Now we know they are all Consts, so get their names, type and params*)
    95     (*Now we know they are all Consts, so get their names, type and params*)
    96     val rec_names = map (#1 o dest_Const) rec_hds
    96     val rec_names = map (#1 o dest_Const) rec_hds
    97     and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    97     and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    98 
    98 
   100        (fn a => "Name of recursive set not an identifier: " ^ a);
   100        (fn a => "Name of recursive set not an identifier: " ^ a);
   101 
   101 
   102     local (*Checking the introduction rules*)
   102     local (*Checking the introduction rules*)
   103       val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
   103       val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
   104       fun intr_ok set =
   104       fun intr_ok set =
   105 	  case head_of set of Const(a,recT) => a mem rec_names | _ => false;
   105           case head_of set of Const(a,recT) => a mem rec_names | _ => false;
   106     in
   106     in
   107       val _ =  assert_all intr_ok intr_sets
   107       val _ =  assert_all intr_ok intr_sets
   108 	 (fn t => "Conclusion of rule does not name a recursive set: " ^ 
   108          (fn t => "Conclusion of rule does not name a recursive set: " ^ 
   109 		  Sign.string_of_term sign t);
   109                   Sign.string_of_term sign t);
   110     end;
   110     end;
   111 
   111 
   112     val _ = assert_all is_Free rec_params
   112     val _ = assert_all is_Free rec_params
   113 	(fn t => "Param in recursion term not a free variable: " ^
   113         (fn t => "Param in recursion term not a free variable: " ^
   114 		 Sign.string_of_term sign t);
   114                  Sign.string_of_term sign t);
   115 
   115 
   116     (*** Construct the lfp definition ***)
   116     (*** Construct the lfp definition ***)
   117     val mk_variant = variant (foldr add_term_names (intr_tms,[]));
   117     val mk_variant = variant (foldr add_term_names (intr_tms,[]));
   118 
   118 
   119     val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   119     val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   120 
   120 
   121     fun dest_tprop (Const("Trueprop",_) $ P) = P
   121     fun dest_tprop (Const("Trueprop",_) $ P) = P
   122       | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
   122       | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ 
   123 			      Sign.string_of_term sign Q);
   123                               Sign.string_of_term sign Q);
   124 
   124 
   125     (*Makes a disjunct from an introduction rule*)
   125     (*Makes a disjunct from an introduction rule*)
   126     fun lfp_part intr = (*quantify over rule's free vars except parameters*)
   126     fun lfp_part intr = (*quantify over rule's free vars except parameters*)
   127       let val prems = map dest_tprop (strip_imp_prems intr)
   127       let val prems = map dest_tprop (strip_imp_prems intr)
   128 	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
   128           val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
   129 	  val exfrees = term_frees intr \\ rec_params
   129           val exfrees = term_frees intr \\ rec_params
   130 	  val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
   130           val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
   131       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
   131       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
   132 
   132 
   133     (*The Part(A,h) terms -- compose injections to make h*)
   133     (*The Part(A,h) terms -- compose injections to make h*)
   134     fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
   134     fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
   135       | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
   135       | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
   136 
   136 
   137     (*Access to balanced disjoint sums via injections*)
   137     (*Access to balanced disjoint sums via injections*)
   138     val parts = 
   138     val parts = 
   139 	map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
   139         map mk_Part (accesses_bal (ap Su.inl, ap Su.inr, Bound 0) 
   140 				  (length rec_tms));
   140                                   (length rec_tms));
   141 
   141 
   142     (*replace each set by the corresponding Part(A,h)*)
   142     (*replace each set by the corresponding Part(A,h)*)
   143     val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
   143     val part_intrs = map (subst_free (rec_tms ~~ parts) o lfp_part) intr_tms;
   144 
   144 
   145     val lfp_abs = absfree(X', iT, 
   145     val lfp_abs = absfree(X', iT, 
   146 		     mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
   146                      mk_Collect(z', dom_sum, fold_bal (app disj) part_intrs));
   147 
   147 
   148     val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
   148     val lfp_rhs = Fp.oper $ dom_sum $ lfp_abs
   149 
   149 
   150     val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
   150     val _ = seq (fn rec_hd => deny (rec_hd occs lfp_rhs) 
   151 			       "Illegal occurrence of recursion operator")
   151                                "Illegal occurrence of recursion operator")
   152 	     rec_hds;
   152              rec_hds;
   153 
   153 
   154     (*** Make the new theory ***)
   154     (*** Make the new theory ***)
   155 
   155 
   156     (*A key definition:
   156     (*A key definition:
   157       If no mutual recursion then it equals the one recursive set.
   157       If no mutual recursion then it equals the one recursive set.
   161     (*Big_rec... is the union of the mutually recursive sets*)
   161     (*Big_rec... is the union of the mutually recursive sets*)
   162     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   162     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   163 
   163 
   164     (*The individual sets must already be declared*)
   164     (*The individual sets must already be declared*)
   165     val axpairs = map mk_defpair 
   165     val axpairs = map mk_defpair 
   166 	  ((big_rec_tm, lfp_rhs) ::
   166           ((big_rec_tm, lfp_rhs) ::
   167 	   (case parts of 
   167            (case parts of 
   168 	       [_] => [] 			(*no mutual recursion*)
   168                [_] => []                        (*no mutual recursion*)
   169 	     | _ => rec_tms ~~		(*define the sets as Parts*)
   169              | _ => rec_tms ~~          (*define the sets as Parts*)
   170 		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   170                     map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   171 
   171 
   172     val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
   172     val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
   173   
   173   
   174   in  thy |> add_defs_i axpairs  end
   174   in  thy |> add_defs_i axpairs  end
   175 
   175 
   177 (*Expects the recursive sets to have been defined already.
   177 (*Expects the recursive sets to have been defined already.
   178   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
   178   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
   179 fun add_constructs_def (rec_names, con_ty_lists) thy = 
   179 fun add_constructs_def (rec_names, con_ty_lists) thy = 
   180   let
   180   let
   181     val _ = writeln"  Defining the constructor functions...";
   181     val _ = writeln"  Defining the constructor functions...";
   182     val case_name = "f";		(*name for case variables*)
   182     val case_name = "f";                (*name for case variables*)
   183 
   183 
   184     (** Define the constructors **)
   184     (** Define the constructors **)
   185 
   185 
   186     (*The empty tuple is 0*)
   186     (*The empty tuple is 0*)
   187     fun mk_tuple [] = Const("0",iT)
   187     fun mk_tuple [] = Const("0",iT)
   188       | mk_tuple args = foldr1 (app Pr.pair) args;
   188       | mk_tuple args = foldr1 (app Pr.pair) args;
   189 
   189 
   190     fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
   190     fun mk_inject n k u = access_bal(ap Su.inl, ap Su.inr, u) n k;
   191 
   191 
   192     val npart = length rec_names;	(*total # of mutually recursive parts*)
   192     val npart = length rec_names;       (*total # of mutually recursive parts*)
   193 
   193 
   194     (*Make constructor definition; kpart is # of this mutually recursive part*)
   194     (*Make constructor definition; kpart is # of this mutually recursive part*)
   195     fun mk_con_defs (kpart, con_ty_list) = 
   195     fun mk_con_defs (kpart, con_ty_list) = 
   196       let val ncon = length con_ty_list	   (*number of constructors*)
   196       let val ncon = length con_ty_list    (*number of constructors*)
   197 	  fun mk_def (((id,T,syn), name, args, prems), kcon) =
   197           fun mk_def (((id,T,syn), name, args, prems), kcon) =
   198 		(*kcon is index of constructor*)
   198                 (*kcon is index of constructor*)
   199 	      mk_defpair (list_comb (Const(name,T), args),
   199               mk_defpair (list_comb (Const(name,T), args),
   200 			  mk_inject npart kpart
   200                           mk_inject npart kpart
   201 			  (mk_inject ncon kcon (mk_tuple args)))
   201                           (mk_inject ncon kcon (mk_tuple args)))
   202       in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
   202       in  map mk_def (con_ty_list ~~ (1 upto ncon))  end;
   203 
   203 
   204     (** Define the case operator **)
   204     (** Define the case operator **)
   205 
   205 
   206     (*Combine split terms using case; yields the case operator for one part*)
   206     (*Combine split terms using case; yields the case operator for one part*)
   207     fun call_case case_list = 
   207     fun call_case case_list = 
   208       let fun call_f (free,args) = 
   208       let fun call_f (free,args) = 
   209 	      ap_split Pr.split_const free (map (#2 o dest_Free) args)
   209               ap_split Pr.split_const free (map (#2 o dest_Free) args)
   210       in  fold_bal (app Su.elim) (map call_f case_list)  end;
   210       in  fold_bal (app Su.elim) (map call_f case_list)  end;
   211 
   211 
   212     (** Generating function variables for the case definition
   212     (** Generating function variables for the case definition
   213 	Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   213         Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
   214 
   214 
   215     (*Treatment of a single constructor*)
   215     (*Treatment of a single constructor*)
   216     fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
   216     fun add_case (((id,T,syn), name, args, prems), (opno,cases)) =
   217 	if Syntax.is_identifier id
   217         if Syntax.is_identifier id
   218 	then (opno,   
   218         then (opno,   
   219 	      (Free(case_name ^ "_" ^ id, T), args) :: cases)
   219               (Free(case_name ^ "_" ^ id, T), args) :: cases)
   220 	else (opno+1, 
   220         else (opno+1, 
   221 	      (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
   221               (Free(case_name ^ "_op_" ^ string_of_int opno, T), args) :: 
   222 	      cases)
   222               cases)
   223 
   223 
   224     (*Treatment of a list of constructors, for one part*)
   224     (*Treatment of a list of constructors, for one part*)
   225     fun add_case_list (con_ty_list, (opno,case_lists)) =
   225     fun add_case_list (con_ty_list, (opno,case_lists)) =
   226 	let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
   226         let val (opno',case_list) = foldr add_case (con_ty_list, (opno,[]))
   227 	in (opno', case_list :: case_lists) end;
   227         in (opno', case_list :: case_lists) end;
   228 
   228 
   229     (*Treatment of all parts*)
   229     (*Treatment of all parts*)
   230     val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
   230     val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
   231 
   231 
   232     val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
   232     val big_case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
   237 
   237 
   238     (*The list of all the function variables*)
   238     (*The list of all the function variables*)
   239     val big_case_args = flat (map (map #1) case_lists);
   239     val big_case_args = flat (map (map #1) case_lists);
   240 
   240 
   241     val big_case_tm = 
   241     val big_case_tm = 
   242 	list_comb (Const(big_case_name, big_case_typ), big_case_args); 
   242         list_comb (Const(big_case_name, big_case_typ), big_case_args); 
   243 
   243 
   244     val big_case_def = mk_defpair  
   244     val big_case_def = mk_defpair  
   245 	(big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
   245         (big_case_tm, fold_bal (app Su.elim) (map call_case case_lists)); 
   246 
   246 
   247     (** Build the new theory **)
   247     (** Build the new theory **)
   248 
   248 
   249     val const_decs =
   249     val const_decs =
   250 	(big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
   250         (big_case_name, big_case_typ, NoSyn) :: map #1 (flat con_ty_lists);
   251 
   251 
   252     val axpairs =
   252     val axpairs =
   253 	big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
   253         big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
   254 
   254 
   255     in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
   255     in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
   256 end;
   256 end;