src/Pure/logic.ML
changeset 546 36e40454e03e
parent 447 d1f827fa0a18
child 585 409c9ee7a9f3
     1.1 --- a/src/Pure/logic.ML	Thu Aug 18 17:53:28 1994 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Aug 18 17:56:07 1994 +0200
     1.3 @@ -10,41 +10,43 @@
     1.4  
     1.5  signature LOGIC = 
     1.6    sig
     1.7 -  val assum_pairs: term -> (term*term)list
     1.8 -  val auto_rename: bool ref   
     1.9 -  val close_form: term -> term   
    1.10 -  val count_prems: term * int -> int
    1.11 -  val dest_equals: term -> term * term
    1.12 -  val dest_flexpair: term -> term * term
    1.13 -  val dest_implies: term -> term * term
    1.14 -  val dest_inclass: term -> typ * class
    1.15 -  val dest_type: term -> typ
    1.16 -  val flatten_params: int -> term -> term
    1.17 -  val freeze_vars: term -> term
    1.18 -  val incr_indexes: typ list * int -> term -> term
    1.19 -  val lift_fns: term * int -> (term -> term) * (term -> term)
    1.20 -  val list_flexpairs: (term*term)list * term -> term
    1.21 -  val list_implies: term list * term -> term
    1.22 +  val assum_pairs	: term -> (term*term)list
    1.23 +  val auto_rename	: bool ref   
    1.24 +  val close_form	: term -> term   
    1.25 +  val count_prems	: term * int -> int
    1.26 +  val dest_equals	: term -> term * term
    1.27 +  val dest_flexpair	: term -> term * term
    1.28 +  val dest_implies	: term -> term * term
    1.29 +  val dest_inclass	: term -> typ * class
    1.30 +  val dest_type		: term -> typ
    1.31 +  val flatten_params	: int -> term -> term
    1.32 +  val freeze_vars	: term -> term
    1.33 +  val incr_indexes	: typ list * int -> term -> term
    1.34 +  val lift_fns		: term * int -> (term -> term) * (term -> term)
    1.35 +  val list_flexpairs	: (term*term)list * term -> term
    1.36 +  val list_implies	: term list * term -> term
    1.37    val list_rename_params: string list * term -> term
    1.38 -  val mk_equals: term * term -> term
    1.39 -  val mk_flexpair: term * term -> term
    1.40 -  val mk_implies: term * term -> term
    1.41 -  val mk_inclass: typ * class -> term
    1.42 -  val mk_type: typ -> term
    1.43 -  val occs: term * term -> bool
    1.44 -  val rule_of: (term*term)list * term list * term -> term
    1.45 -  val set_rename_prefix: string -> unit   
    1.46 -  val skip_flexpairs: term -> term
    1.47 +  val mk_equals		: term * term -> term
    1.48 +  val mk_flexpair	: term * term -> term
    1.49 +  val mk_implies	: term * term -> term
    1.50 +  val mk_inclass	: typ * class -> term
    1.51 +  val mk_type		: typ -> term
    1.52 +  val occs		: term * term -> bool
    1.53 +  val rule_of		: (term*term)list * term list * term -> term
    1.54 +  val set_rename_prefix	: string -> unit   
    1.55 +  val skip_flexpairs	: term -> term
    1.56    val strip_assums_concl: term -> term
    1.57 -  val strip_assums_hyp: term -> term list
    1.58 -  val strip_flexpairs: term -> (term*term)list * term
    1.59 -  val strip_horn: term -> (term*term)list * term list * term
    1.60 -  val strip_imp_concl: term -> term
    1.61 -  val strip_imp_prems: term -> term list
    1.62 -  val strip_params: term -> (string * typ) list
    1.63 -  val strip_prems: int * term list * term -> term list * term
    1.64 -  val thaw_vars: term -> term
    1.65 -  val varify: term -> term  
    1.66 +  val strip_assums_hyp	: term -> term list
    1.67 +  val strip_flexpairs	: term -> (term*term)list * term
    1.68 +  val strip_horn	: term -> (term*term)list * term list * term
    1.69 +  val strip_imp_concl	: term -> term
    1.70 +  val strip_imp_prems	: term -> term list
    1.71 +  val strip_params	: term -> (string * typ) list
    1.72 +  val strip_prems	: int * term list * term -> term list * term
    1.73 +  val thaw_vars		: term -> term
    1.74 +  val unvarifyT		: typ -> typ  
    1.75 +  val unvarify		: term -> term  
    1.76 +  val varify		: term -> term  
    1.77    end;
    1.78  
    1.79  functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
    1.80 @@ -318,4 +320,17 @@
    1.81    | varify (f$t) = varify f $ varify t
    1.82    | varify t = t;
    1.83  
    1.84 +(*Inverse of varifyT.  Move to Pure/type.ML?*)
    1.85 +fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
    1.86 +  | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
    1.87 +  | unvarifyT T = T;
    1.88 +
    1.89 +(*Inverse of varify.  Converts axioms back to their original form.*)
    1.90 +fun unvarify (Const(a,T))    = Const(a, unvarifyT T)
    1.91 +  | unvarify (Var((a,0), T)) = Free(a, unvarifyT T)
    1.92 +  | unvarify (Var(ixn,T))    = Var(ixn, unvarifyT T)	(*non-zero index!*)
    1.93 +  | unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body)
    1.94 +  | unvarify (f$t) = unvarify f $ unvarify t
    1.95 +  | unvarify t = t;
    1.96 +
    1.97  end;