src/ZF/ind_syntax.ML
changeset 4352 7ac9f3e8a97d
parent 3925 90f499226ab9
child 4804 02b7c759159b
     1.1 --- a/src/ZF/ind_syntax.ML	Wed Dec 03 10:50:02 1997 +0100
     1.2 +++ b/src/ZF/ind_syntax.ML	Wed Dec 03 10:52:17 1997 +0100
     1.3 @@ -12,40 +12,22 @@
     1.4  structure Ind_Syntax =
     1.5  struct
     1.6  
     1.7 -(** Abstract syntax definitions for FOL and ZF **)
     1.8 -
     1.9 -val iT = Type("i",[])
    1.10 -and oT = Type("o",[]);
    1.11 -
    1.12 -
    1.13 -(** Logical constants **)
    1.14 +(** Abstract syntax definitions for ZF **)
    1.15  
    1.16 -val conj = Const("op &", [oT,oT]--->oT)
    1.17 -and disj = Const("op |", [oT,oT]--->oT)
    1.18 -and imp = Const("op -->", [oT,oT]--->oT);
    1.19 -
    1.20 -val eq_const = Const("op =", [iT,iT]--->oT);
    1.21 +val iT = Type("i",[]);
    1.22  
    1.23 -val mem_const = Const("op :", [iT,iT]--->oT);
    1.24 -
    1.25 -val exists_const = Const("Ex", [iT-->oT]--->oT);
    1.26 -fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P));
    1.27 -
    1.28 -val all_const = Const("All", [iT-->oT]--->oT);
    1.29 -fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P));
    1.30 +val mem_const = Const("op :", [iT,iT]--->FOLogic.oT);
    1.31  
    1.32  (*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
    1.33  fun mk_all_imp (A,P) = 
    1.34 -    all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
    1.35 +    FOLogic.all_const iT $ 
    1.36 +      Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0));
    1.37  
    1.38  val Part_const = Const("Part", [iT,iT-->iT]--->iT);
    1.39  
    1.40 -val Collect_const = Const("Collect", [iT,iT-->oT]--->iT);
    1.41 +val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
    1.42  fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
    1.43  
    1.44 -val Trueprop = Const("Trueprop",oT-->propT);
    1.45 -fun mk_tprop P = Trueprop $ P;
    1.46 -
    1.47  (*simple error-checking in the premises of an inductive definition*)
    1.48  fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
    1.49          error"Premises may not be conjuctive"
    1.50 @@ -79,7 +61,7 @@
    1.51  
    1.52  (*read a constructor specification*)
    1.53  fun read_construct sign (id, sprems, syn) =
    1.54 -    let val prems = map (readtm sign oT) sprems
    1.55 +    let val prems = map (readtm sign FOLogic.oT) sprems
    1.56          val args = map (#1 o dest_mem) prems
    1.57          val T = (map (#2 o dest_Free) args) ---> iT
    1.58                  handle TERM _ => error 
    1.59 @@ -94,8 +76,10 @@
    1.60    let
    1.61      fun mk_intr ((id,T,syn), name, args, prems) =
    1.62        Logic.list_implies
    1.63 -        (map mk_tprop prems,
    1.64 -          mk_tprop (mem_const $ list_comb (Const (Sign.full_name sg name, T), args) $ rec_tm))
    1.65 +        (map FOLogic.mk_Trueprop prems,
    1.66 +	 FOLogic.mk_Trueprop
    1.67 +	    (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
    1.68 +	               $ rec_tm))
    1.69    in  map mk_intr constructs  end;
    1.70  
    1.71  fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);