src/ZF/add_ind_def.ML
changeset 727 711e4eb8c213
parent 612 1ebe4d36dedc
child 750 019aadf0e315
equal deleted inserted replaced
726:d703d1a1a2af 727:711e4eb8c213
    62   val distinct'	: thm			(*distinctness of inr, inl using <->*)
    62   val distinct'	: thm			(*distinctness of inr, inl using <->*)
    63   end;
    63   end;
    64 
    64 
    65 signature ADD_INDUCTIVE_DEF =
    65 signature ADD_INDUCTIVE_DEF =
    66   sig 
    66   sig 
    67   val add_fp_def_i : term list * term list * term list -> theory -> theory
    67   val add_fp_def_i : term list * term * term list -> theory -> theory
    68   val add_fp_def   : (string*string) list * string list -> theory -> theory
       
    69   val add_constructs_def :
    68   val add_constructs_def :
    70         string list * ((string*typ*mixfix) * 
    69         string list * ((string*typ*mixfix) * 
    71                        string * term list * term list) list list ->
    70                        string * term list * term list) list list ->
    72         theory -> theory
    71         theory -> theory
    73   end;
    72   end;
    79     (structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =
    78     (structure Fp: FP and Pr : PR and Su : SU) : ADD_INDUCTIVE_DEF =
    80 struct
    79 struct
    81 open Logic Ind_Syntax;
    80 open Logic Ind_Syntax;
    82 
    81 
    83 (*internal version*)
    82 (*internal version*)
    84 fun add_fp_def_i (rec_tms, domts, intr_tms) thy = 
    83 fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
    85   let
    84   let
    86     val sign = sign_of thy;
    85     val sign = sign_of thy;
    87 
    86 
    88     (*recT and rec_params should agree for all mutually recursive components*)
    87     (*recT and rec_params should agree for all mutually recursive components*)
    89     val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
    88     val (Const(_,recT),rec_params) = strip_comb (hd rec_tms)
   126 	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
   125 	  val _ = seq (fn rec_hd => seq (chk_prem rec_hd) prems) rec_hds
   127 	  val exfrees = term_frees intr \\ rec_params
   126 	  val exfrees = term_frees intr \\ rec_params
   128 	  val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
   127 	  val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
   129       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
   128       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
   130 
   129 
   131     val dom_sum = fold_bal (app Su.sum) domts;
       
   132 
       
   133     (*The Part(A,h) terms -- compose injections to make h*)
   130     (*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*)
   131     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);
   132       | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
   136 
   133 
   137     (*Access to balanced disjoint sums via injections*)
   134     (*Access to balanced disjoint sums via injections*)
   170 		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   167 		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
   171 
   168 
   172     val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
   169     val _ = seq (writeln o Sign.string_of_term sign o #2) axpairs
   173   
   170   
   174   in  thy |> add_defs_i axpairs  end
   171   in  thy |> add_defs_i axpairs  end
   175 
       
   176 
       
   177 (*external, string-based version; needed?*)
       
   178 fun add_fp_def (rec_doms, sintrs) thy = 
       
   179   let val sign = sign_of thy;
       
   180       val rec_tms = map (readtm sign iT o fst) rec_doms
       
   181       and domts   = map (readtm sign iT o snd) rec_doms
       
   182       val intr_tms = map (readtm sign propT) sintrs
       
   183   in  add_fp_def_i (rec_tms, domts, intr_tms) thy  end
       
   184 
   172 
   185 
   173 
   186 (*Expects the recursive sets to have been defined already.
   174 (*Expects the recursive sets to have been defined already.
   187   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
   175   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
   188 fun add_constructs_def (rec_names, con_ty_lists) thy = 
   176 fun add_constructs_def (rec_names, con_ty_lists) thy =