src/ZF/ind_syntax.ML
changeset 543 e961b2092869
parent 516 1957113f0d7d
child 568 756b0e2a6cac
     1.1 --- a/src/ZF/ind_syntax.ML	Thu Aug 18 12:56:57 1994 +0200
     1.2 +++ b/src/ZF/ind_syntax.ML	Thu Aug 18 17:41:40 1994 +0200
     1.3 @@ -14,28 +14,12 @@
     1.4  (*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*)
     1.5  fun mk_defpair (lhs, rhs) = 
     1.6    let val Const(name, _) = head_of lhs
     1.7 -      val dummy = assert (term_vars rhs subset term_vars lhs
     1.8 -		          andalso
     1.9 -		          term_frees rhs subset term_frees lhs
    1.10 -		          andalso
    1.11 -		          term_tvars rhs subset term_tvars lhs
    1.12 -		          andalso
    1.13 -		          term_tfrees rhs subset term_tfrees lhs)
    1.14 -	          ("Extra variables on RHS in definition of " ^ name)
    1.15    in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end;
    1.16  
    1.17  fun get_def thy s = get_axiom thy (s^"_def");
    1.18  
    1.19  fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a);
    1.20  
    1.21 -(*export to Pure/library?  *)
    1.22 -fun assert_all pred l msg_fn = 
    1.23 -  let fun asl [] = ()
    1.24 -	| asl (x::xs) = if pred x then asl xs
    1.25 -	                else error (msg_fn x)
    1.26 -  in  asl l  end;
    1.27 -
    1.28 -
    1.29  (** Abstract syntax definitions for FOL and ZF **)
    1.30  
    1.31  val iT = Type("i",[])
    1.32 @@ -78,15 +62,6 @@
    1.33  val Trueprop = Const("Trueprop",oT-->propT);
    1.34  fun mk_tprop P = Trueprop $ P;
    1.35  
    1.36 -(*Prove a goal stated as a term, with exception handling*)
    1.37 -fun prove_term sign defs (P,tacsf) = 
    1.38 -    let val ct = cterm_of sign P
    1.39 -    in  prove_goalw_cterm defs ct tacsf
    1.40 -	handle e => (writeln ("Exception in proof of\n" ^
    1.41 -			       string_of_cterm ct); 
    1.42 -		     raise e)
    1.43 -    end;
    1.44 -
    1.45  (*Read an assumption in the given theory*)
    1.46  fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT));
    1.47  
    1.48 @@ -127,21 +102,6 @@
    1.49    | chk_prem rec_hd t = 
    1.50  	deny (Logic.occs(rec_hd,t)) "Recursion term in side formula";
    1.51  
    1.52 -
    1.53 -(*Inverse of varifyT.  Move to Pure/type.ML?*)
    1.54 -fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    1.55 -  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    1.56 -  | unvarifyT T = T;
    1.57 -
    1.58 -(*Inverse of varify.  Move to Pure/logic.ML?*)
    1.59 -fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
    1.60 -  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
    1.61 -  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
    1.62 -  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
    1.63 -  | unvarify (f$t) = unvarify f $ unvarify t
    1.64 -  | unvarify t = t;
    1.65 -
    1.66 -
    1.67  (*Make distinct individual variables a1, a2, a3, ..., an. *)
    1.68  fun mk_frees a [] = []
    1.69    | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts;