src/ZF/ind_syntax.ML
changeset 6053 8a1059aa01f0
parent 4972 7fe1d30c1374
child 6093 87bf8c03b169
     1.1 --- a/src/ZF/ind_syntax.ML	Mon Dec 28 16:58:11 1998 +0100
     1.2 +++ b/src/ZF/ind_syntax.ML	Mon Dec 28 16:59:28 1998 +0100
     1.3 @@ -15,6 +15,10 @@
     1.4  (*Print tracing messages during processing of "inductive" theory sections*)
     1.5  val trace = ref false;
     1.6  
     1.7 +fun traceIt msg ct = 
     1.8 +    if !trace then (writeln (msg ^ string_of_cterm ct); ct)
     1.9 +    else ct;
    1.10 +
    1.11  (** Abstract syntax definitions for ZF **)
    1.12  
    1.13  val iT = Type("i",[]);
    1.14 @@ -29,6 +33,10 @@
    1.15  
    1.16  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    1.17  
    1.18 +val apply_const = Const("op `", [iT,iT]--->iT);
    1.19 +
    1.20 +val Vrecursor_const = Const("Vrecursor", [[iT,iT]--->iT, iT]--->iT);
    1.21 +
    1.22  val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
    1.23  fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    1.24  
    1.25 @@ -60,6 +68,11 @@
    1.26  
    1.27  (** For datatype definitions **)
    1.28  
    1.29 +(*Constructor name, type, mixfix info;
    1.30 +  internal name from mixfix, datatype sets, full premises*)
    1.31 +type constructor_spec = 
    1.32 +    ((string * typ * mixfix) * string * term list * term list);
    1.33 +
    1.34  fun dest_mem (Const("op :",_) $ x $ A) = (x,A)
    1.35    | dest_mem _ = error "Constructor specifications must have the form x:A";
    1.36  
    1.37 @@ -103,8 +116,8 @@
    1.38  
    1.39  (*Previously these both did    replicate (length rec_tms);  however now
    1.40    [q]univ itself constitutes the sum domain for mutual recursion!*)
    1.41 -fun data_domain rec_tms = univ $ union_params (hd rec_tms);
    1.42 -fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
    1.43 +fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
    1.44 +  | data_domain true  rec_tms = quniv $ union_params (hd rec_tms);
    1.45  
    1.46  (*Could go to FOL, but it's hardly general*)
    1.47  val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
    1.48 @@ -128,5 +141,3 @@
    1.49  
    1.50  end;
    1.51  
    1.52 -
    1.53 -val trace_induct = Ind_Syntax.trace;