src/Pure/logic.ML
changeset 1458 fd510875fb71
parent 637 b344bf624143
child 1460 5a6f2aabd538
     1.1 --- a/src/Pure/logic.ML	Mon Jan 29 13:50:10 1996 +0100
     1.2 +++ b/src/Pure/logic.ML	Mon Jan 29 13:56:41 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Pure/logic.ML
     1.5 +(*  Title:      Pure/logic.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   Cambridge University 1992
    1.10  
    1.11  Supporting code for defining the abstract type "thm"
    1.12 @@ -10,43 +10,43 @@
    1.13  
    1.14  signature LOGIC = 
    1.15    sig
    1.16 -  val assum_pairs	: term -> (term*term)list
    1.17 -  val auto_rename	: bool ref   
    1.18 -  val close_form	: term -> term   
    1.19 -  val count_prems	: term * int -> int
    1.20 -  val dest_equals	: term -> term * term
    1.21 -  val dest_flexpair	: term -> term * term
    1.22 -  val dest_implies	: term -> term * term
    1.23 -  val dest_inclass	: term -> typ * class
    1.24 -  val dest_type		: term -> typ
    1.25 -  val flatten_params	: int -> term -> term
    1.26 -  val freeze_vars	: term -> term
    1.27 -  val incr_indexes	: typ list * int -> term -> term
    1.28 -  val lift_fns		: term * int -> (term -> term) * (term -> term)
    1.29 -  val list_flexpairs	: (term*term)list * term -> term
    1.30 -  val list_implies	: term list * term -> term
    1.31 +  val assum_pairs       : term -> (term*term)list
    1.32 +  val auto_rename       : bool ref   
    1.33 +  val close_form        : term -> term   
    1.34 +  val count_prems       : term * int -> int
    1.35 +  val dest_equals       : term -> term * term
    1.36 +  val dest_flexpair     : term -> term * term
    1.37 +  val dest_implies      : term -> term * term
    1.38 +  val dest_inclass      : term -> typ * class
    1.39 +  val dest_type         : term -> typ
    1.40 +  val flatten_params    : int -> term -> term
    1.41 +  val freeze_vars       : term -> term
    1.42 +  val incr_indexes      : typ list * int -> term -> term
    1.43 +  val lift_fns          : term * int -> (term -> term) * (term -> term)
    1.44 +  val list_flexpairs    : (term*term)list * term -> term
    1.45 +  val list_implies      : term list * term -> term
    1.46    val list_rename_params: string list * term -> term
    1.47    val is_equals         : term -> bool
    1.48 -  val mk_equals		: term * term -> term
    1.49 -  val mk_flexpair	: term * term -> term
    1.50 -  val mk_implies	: term * term -> term
    1.51 -  val mk_inclass	: typ * class -> term
    1.52 -  val mk_type		: typ -> term
    1.53 -  val occs		: term * term -> bool
    1.54 -  val rule_of		: (term*term)list * term list * term -> term
    1.55 -  val set_rename_prefix	: string -> unit   
    1.56 -  val skip_flexpairs	: term -> term
    1.57 +  val mk_equals         : term * term -> term
    1.58 +  val mk_flexpair       : term * term -> term
    1.59 +  val mk_implies        : term * term -> term
    1.60 +  val mk_inclass        : typ * class -> term
    1.61 +  val mk_type           : typ -> term
    1.62 +  val occs              : term * term -> bool
    1.63 +  val rule_of           : (term*term)list * term list * term -> term
    1.64 +  val set_rename_prefix : string -> unit   
    1.65 +  val skip_flexpairs    : term -> term
    1.66    val strip_assums_concl: term -> term
    1.67 -  val strip_assums_hyp	: term -> term list
    1.68 -  val strip_flexpairs	: term -> (term*term)list * term
    1.69 -  val strip_horn	: term -> (term*term)list * term list * term
    1.70 -  val strip_imp_concl	: term -> term
    1.71 -  val strip_imp_prems	: term -> term list
    1.72 -  val strip_params	: term -> (string * typ) list
    1.73 -  val strip_prems	: int * term list * term -> term list * term
    1.74 -  val thaw_vars		: term -> term
    1.75 -  val unvarify		: term -> term  
    1.76 -  val varify		: term -> term  
    1.77 +  val strip_assums_hyp  : term -> term list
    1.78 +  val strip_flexpairs   : term -> (term*term)list * term
    1.79 +  val strip_horn        : term -> (term*term)list * term list * term
    1.80 +  val strip_imp_concl   : term -> term
    1.81 +  val strip_imp_prems   : term -> term list
    1.82 +  val strip_params      : term -> (string * typ) list
    1.83 +  val strip_prems       : int * term list * term -> term list * term
    1.84 +  val thaw_vars         : term -> term
    1.85 +  val unvarify          : term -> term  
    1.86 +  val varify            : term -> term  
    1.87    end;
    1.88  
    1.89  functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC =
    1.90 @@ -91,11 +91,11 @@
    1.91    | strip_imp_concl A = A : term;
    1.92  
    1.93  (*Strip and return premises: (i, [], A1==>...Ai==>B)
    1.94 -    goes to   ([Ai, A(i-1),...,A1] , B) 	(REVERSED) 
    1.95 +    goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED) 
    1.96    if  i<0 or else i too big then raises  TERM*)
    1.97  fun strip_prems (0, As, B) = (As, B) 
    1.98    | strip_prems (i, As, Const("==>", _) $ A $ B) = 
    1.99 -	strip_prems (i-1, A::As, B)
   1.100 +        strip_prems (i-1, A::As, B)
   1.101    | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   1.102  
   1.103  (*Count premises -- quicker than (length ostrip_prems) *)
   1.104 @@ -114,13 +114,13 @@
   1.105      goes to (a1=?=b1) ==>...(an=?=bn)==>C *)
   1.106  fun list_flexpairs ([], A) = A
   1.107    | list_flexpairs ((t,u)::pairs, A) =
   1.108 -	implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
   1.109 +        implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
   1.110  
   1.111  (*Make the object-rule tpairs==>As==>B   *)
   1.112  fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B));
   1.113  
   1.114  (*Remove and return flexflex pairs: 
   1.115 -    (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )	
   1.116 +    (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )     
   1.117    [Tail recursive in order to return a pair of results] *)
   1.118  fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) =
   1.119          strip_flex_aux ((t,u)::pairs, C)
   1.120 @@ -130,7 +130,7 @@
   1.121  
   1.122  (*Discard flexflex pairs*)
   1.123  fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) =
   1.124 -	skip_flexpairs C
   1.125 +        skip_flexpairs C
   1.126    | skip_flexpairs C = C;
   1.127  
   1.128  (*strip a proof state (Horn clause): 
   1.129 @@ -165,13 +165,13 @@
   1.130  fun t occs u = (t aconv u) orelse 
   1.131        (case u of
   1.132            Abs(_,_,body) => t occs body
   1.133 -	| f$t' => t occs f  orelse  t occs t'
   1.134 -	| _ => false);
   1.135 +        | f$t' => t occs f  orelse  t occs t'
   1.136 +        | _ => false);
   1.137  
   1.138  (*Close up a formula over all free variables by quantification*)
   1.139  fun close_form A =
   1.140      list_all_free (map dest_Free (sort atless (term_frees A)),   
   1.141 -		   A);
   1.142 +                   A);
   1.143  
   1.144  
   1.145  (*Freeze all (T)Vars by turning them into (T)Frees*)
   1.146 @@ -188,9 +188,9 @@
   1.147    | thaw_vars(Free(a,T))  =
   1.148        let val T' = Type.thaw_vars T
   1.149        in case explode a of
   1.150 -	   "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
   1.151 +           "?"::vn => let val (ixn,_) = Syntax.scan_varname vn
   1.152                        in Var(ixn,T') end
   1.153 -	 | _       => Free(a,T')
   1.154 +         | _       => Free(a,T')
   1.155        end
   1.156    | thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t)
   1.157    | thaw_vars(s$t)        = thaw_vars s $ thaw_vars t
   1.158 @@ -203,14 +203,14 @@
   1.159      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   1.160  fun incr_indexes (Us: typ list, inc:int) t = 
   1.161    let fun incr (Var ((a,i), T), lev) = 
   1.162 -		Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   1.163 -				lev, length Us)
   1.164 -	| incr (Abs (a,T,body), lev) =
   1.165 -		Abs (a, incr_tvar inc T, incr(body,lev+1))
   1.166 -	| incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   1.167 -	| incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   1.168 -	| incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   1.169 -	| incr (t,lev) = t
   1.170 +                Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   1.171 +                                lev, length Us)
   1.172 +        | incr (Abs (a,T,body), lev) =
   1.173 +                Abs (a, incr_tvar inc T, incr(body,lev+1))
   1.174 +        | incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   1.175 +        | incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   1.176 +        | incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   1.177 +        | incr (t,lev) = t
   1.178    in  incr(t,0)  end;
   1.179  
   1.180  (*Make lifting functions from subgoal and increment.
   1.181 @@ -218,14 +218,14 @@
   1.182      lift_all operates on propositions     *)
   1.183  fun lift_fns (B,inc) =
   1.184    let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   1.185 -	| lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   1.186 -	      Abs(a, T, lift_abs (T::Us, t) u)
   1.187 -	| lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   1.188 +        | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   1.189 +              Abs(a, T, lift_abs (T::Us, t) u)
   1.190 +        | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   1.191        fun lift_all (Us, Const("==>", _) $ A $ B) u =
   1.192 -	      implies $ A $ lift_all (Us,B) u
   1.193 -	| lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   1.194 -	      all T $ Abs(a, T, lift_all (T::Us,t) u)
   1.195 -	| lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   1.196 +              implies $ A $ lift_all (Us,B) u
   1.197 +        | lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   1.198 +              all T $ Abs(a, T, lift_all (T::Us,t) u)
   1.199 +        | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   1.200    in  (lift_abs([],B), lift_all([],B))  end;
   1.201  
   1.202  (*Strips assumptions in goal, yielding list of hypotheses.   *)
   1.203 @@ -250,8 +250,8 @@
   1.204      if j=0 andalso n<=0 then A  (*nothing left to do...*)
   1.205      else case A of
   1.206          Const("==>", _) $ H $ B => 
   1.207 -	  if n=1 then                           (remove_params j (n-1) B)
   1.208 -	  else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   1.209 +          if n=1 then                           (remove_params j (n-1) B)
   1.210 +          else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   1.211        | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   1.212        | _ => if n>0 then raise TERM("remove_params", [A])
   1.213               else A;
   1.214 @@ -278,9 +278,9 @@
   1.215    if n>0 then deletes assumption n. *)
   1.216  fun flatten_params n A =
   1.217      let val params = strip_params A;
   1.218 -	val vars = if !auto_rename 
   1.219 -		   then rename_vars (!rename_prefix, params)
   1.220 -		   else variantlist(map #1 params,[]) ~~ map #2 params
   1.221 +        val vars = if !auto_rename 
   1.222 +                   then rename_vars (!rename_prefix, params)
   1.223 +                   else variantlist(map #1 params,[]) ~~ map #2 params
   1.224      in  list_all (vars, remove_params (length vars) n A)
   1.225      end;
   1.226  
   1.227 @@ -294,9 +294,9 @@
   1.228  (*Strips assumptions in goal yielding  ( [Hn,...,H1], [xm,...,x1], B )
   1.229    where H1,...,Hn are the hypotheses and x1...xm are the parameters.   *)
   1.230  fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 
   1.231 -	strip_assums_aux (H::Hs, params, B)
   1.232 +        strip_assums_aux (H::Hs, params, B)
   1.233    | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
   1.234 -	strip_assums_aux (Hs, (a,T)::params, t)
   1.235 +        strip_assums_aux (Hs, (a,T)::params, t)
   1.236    | strip_assums_aux (Hs, params, B) = (Hs, params, B);
   1.237  
   1.238  fun strip_assums A = strip_assums_aux ([],[],A);
   1.239 @@ -310,7 +310,7 @@
   1.240        val D = Unify.rlist_abs(params, B)
   1.241        fun pairrev ([],pairs) = pairs  
   1.242          | pairrev (H::Hs,pairs) = 
   1.243 -	    pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   1.244 +            pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   1.245    in  pairrev (Hs,[])   (*WAS:  map pair (rev Hs)  *)
   1.246    end;
   1.247