replaced extend_theory by new add_* functions;
authorclasohm
Fri Jul 01 11:03:42 1994 +0200 (1994-07-01 ago)
changeset 4443ca9d49fd662
parent 443 10884e64c241
child 445 7b6d8b8d4580
replaced extend_theory by new add_* functions;
changed syntax of datatype declaration
src/ZF/Fin.ML
src/ZF/List.ML
src/ZF/constructor.ML
src/ZF/ind_syntax.ML
src/ZF/intr_elim.ML
     1.1 --- a/src/ZF/Fin.ML	Wed Jun 29 12:13:03 1994 +0200
     1.2 +++ b/src/ZF/Fin.ML	Fri Jul 01 11:03:42 1994 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  *)
     1.5  
     1.6  structure Fin = Inductive_Fun
     1.7 - (val thy        = Arith.thy addconsts [(["Fin"],"i=>i")]
     1.8 + (val thy        = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
     1.9    val rec_doms   = [("Fin","Pow(A)")]
    1.10    val sintrs     = ["0 : Fin(A)",
    1.11                      "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
     2.1 --- a/src/ZF/List.ML	Wed Jun 29 12:13:03 1994 +0200
     2.2 +++ b/src/ZF/List.ML	Fri Jul 01 11:03:42 1994 +0200
     2.3 @@ -9,10 +9,9 @@
     2.4  structure List = Datatype_Fun
     2.5   (val thy        = Univ.thy
     2.6    val rec_specs  = [("list", "univ(A)",
     2.7 -                      [(["Nil"],    "i"), 
     2.8 -                       (["Cons"],   "[i,i]=>i")])]
     2.9 +                      [(["Nil"],    "i", NoSyn), 
    2.10 +                       (["Cons"],   "[i,i]=>i", NoSyn)])]
    2.11    val rec_styp   = "i=>i"
    2.12 -  val ext        = None
    2.13    val sintrs     = ["Nil : list(A)",
    2.14                      "[| a: A;  l: list(A) |] ==> Cons(a,l) : list(A)"]
    2.15    val monos      = []
     3.1 --- a/src/ZF/constructor.ML	Wed Jun 29 12:13:03 1994 +0200
     3.2 +++ b/src/ZF/constructor.ML	Fri Jul 01 11:03:42 1994 +0200
     3.3 @@ -22,10 +22,9 @@
     3.4  signature CONSTRUCTOR =
     3.5    sig
     3.6    val thy        : theory		(*parent theory*)
     3.7 -  val rec_specs  : (string * string * (string list * string)list) list
     3.8 +  val rec_specs  : (string * string * (string list * string * mixfix)list) list
     3.9                        (*recursion ops, types, domains, constructors*)
    3.10    val rec_styp	 : string		(*common type of all recursion ops*)
    3.11 -  val ext        : Syntax.sext option	(*syntax extension for new theory*)
    3.12    val sintrs     : string list		(*desired introduction rules*)
    3.13    val monos      : thm list		(*monotonicity of each M operator*)
    3.14    val type_intrs : thm list		(*type-checking intro rules*)
    3.15 @@ -63,15 +62,21 @@
    3.16     (fn a => "Name of recursive set not an identifier: " ^ a);
    3.17  
    3.18  (*Expands multiple constant declarations*)
    3.19 -fun pairtypes (cs,st) = map (rpair st) cs;
    3.20 +fun flatten_consts ((names, typ, mfix) :: cs) =
    3.21 +      let fun mk_const name = (name, typ, mfix)
    3.22 +      in (map mk_const names) @ (flatten_consts cs) end
    3.23 +  | flatten_consts [] = [];
    3.24  
    3.25  (*Constructors with types and arguments*)
    3.26  fun mk_con_ty_list cons_pairs = 
    3.27 -  let fun mk_con_ty (a,st) =
    3.28 -	  let val T = rdty st
    3.29 -	      val args = mk_frees "xa" (binder_types T)
    3.30 -	  in  (a,T,args) end
    3.31 -  in  map mk_con_ty (flat (map pairtypes cons_pairs))  end;
    3.32 +  let fun mk_con_ty (a, st, syn) =
    3.33 +	  let val T = rdty st;
    3.34 +	      val args = mk_frees "xa" (binder_types T);
    3.35 +              val name = const_name a syn; (* adds "op" to infix constructors*)
    3.36 +	  in (name, T, args) end;
    3.37 +
    3.38 +      fun pairtypes c = flatten_consts [c];
    3.39 +  in map mk_con_ty (flat (map pairtypes cons_pairs))  end;
    3.40  
    3.41  val con_ty_lists = map (mk_con_ty_list o #3) rec_specs;
    3.42  
    3.43 @@ -87,8 +92,8 @@
    3.44  
    3.45  (*Make constructor definition*)
    3.46  fun mk_con_defs (kpart, con_ty_list) = 
    3.47 -  let val ncon = length con_ty_list	(*number of constructors*)
    3.48 -      fun mk_def ((a,T,args), kcon) =	(*kcon = index of this constructor*)
    3.49 +  let val ncon = length con_ty_list	   (*number of constructors*)
    3.50 +      fun mk_def ((a,T,args), kcon) = (*kcon = index of this constructor*)
    3.51  	  mk_defpair sign 
    3.52  	     (list_comb (Const(a,T), args),
    3.53  	      mk_inject npart kpart (mk_inject ncon kcon (mk_tuple args)))
    3.54 @@ -107,7 +112,7 @@
    3.55  
    3.56  (*Treatment of a single constructor*)
    3.57  fun add_case ((a,T,args), (opno,cases)) =
    3.58 -    if Syntax.is_identifier a 
    3.59 +    if Syntax.is_identifier a
    3.60      then (opno,   
    3.61  	  (Free(case_name ^ "_" ^ a, T), args) :: cases)
    3.62      else (opno+1, 
    3.63 @@ -142,13 +147,15 @@
    3.64  val axpairs =
    3.65      big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists));
    3.66  
    3.67 -val const_decs = remove_mixfixes ext
    3.68 -		   (([big_case_name], flatten_typ sign big_case_typ) :: 
    3.69 -		    (big_rec_name ins rec_names, rec_styp) :: 
    3.70 +val const_decs = flatten_consts
    3.71 +		   (([big_case_name], flatten_typ sign big_case_typ, NoSyn) ::
    3.72 +		    (big_rec_name ins rec_names, rec_styp, NoSyn) ::
    3.73  		    flat (map #3 rec_specs));
    3.74  
    3.75 -val con_thy = extend_theory thy (big_rec_name ^ "_Constructors")
    3.76 -    ([], [], [], [], [], const_decs, ext) axpairs;
    3.77 +val con_thy = thy
    3.78 +              |> add_consts const_decs
    3.79 +              |> add_axioms axpairs
    3.80 +              |> add_thyname (big_rec_name ^ "_Constructors");
    3.81  
    3.82  (*1st element is the case definition; others are the constructors*)
    3.83  val con_defs = map (get_axiom con_thy o #1) axpairs;
     4.1 --- a/src/ZF/ind_syntax.ML	Wed Jun 29 12:13:03 1994 +0200
     4.2 +++ b/src/ZF/ind_syntax.ML	Fri Jul 01 11:03:42 1994 +0200
     4.3 @@ -14,14 +14,6 @@
     4.4      end;
     4.5  fun flatten_term sign t = Pretty.str_of (Sign.pretty_term sign t);
     4.6  
     4.7 -(*Add constants to a theory*)
     4.8 -infix addconsts;
     4.9 -fun thy addconsts const_decs = 
    4.10 -    extend_theory thy (space_implode "_" (flat (map #1 const_decs)) 
    4.11 -		       ^ "_Theory")
    4.12 -		  ([], [], [], [], [], const_decs, None) [];
    4.13 -
    4.14 -
    4.15  (*Make a definition, lhs==rhs, checking that vars on lhs contain *)
    4.16  fun mk_defpair sign (lhs,rhs) = 
    4.17    let val Const(name,_) = head_of lhs
     5.1 --- a/src/ZF/intr_elim.ML	Wed Jun 29 12:13:03 1994 +0200
     5.2 +++ b/src/ZF/intr_elim.ML	Fri Jul 01 11:03:42 1994 +0200
     5.3 @@ -207,8 +207,10 @@
     5.4  	 | _ => rec_tms ~~		(*define the sets as Parts*)
     5.5  		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
     5.6  
     5.7 -val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
     5.8 -    ([], [], [], [], [], [], None) axpairs;
     5.9 +val thy = 
    5.10 +  Ind.thy
    5.11 +  |> add_axioms axpairs
    5.12 +  |> add_thyname (big_rec_name ^ "_Inductive");
    5.13  
    5.14  val defs = map (get_axiom thy o #1) axpairs;
    5.15