src/Pure/logic.ML
author nipkow
Thu Oct 16 13:45:16 1997 +0200 (1997-10-16)
changeset 3893 5a1f22e7b359
parent 3408 98a2d517cabe
child 3915 0eb9b9dd4de6
permissions -rw-r--r--
The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.
     1 (*  Title: 	Pure/logic.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Supporting code for defining the abstract type "thm"
     7 *)
     8 
     9 infix occs;
    10 
    11 signature LOGIC = 
    12   sig
    13   val assum_pairs	: term -> (term*term)list
    14   val auto_rename	: bool ref   
    15   val close_form	: term -> term   
    16   val count_prems	: term * int -> int
    17   val dest_equals	: term -> term * term
    18   val dest_flexpair	: term -> term * term
    19   val dest_implies	: term -> term * term
    20   val dest_inclass	: term -> typ * class
    21   val dest_type		: term -> typ
    22   val flatten_params	: int -> term -> term
    23   val incr_indexes	: typ list * int -> term -> term
    24   val lift_fns		: term * int -> (term -> term) * (term -> term)
    25   val list_flexpairs	: (term*term)list * term -> term
    26   val list_implies	: term list * term -> term
    27   val list_rename_params: string list * term -> term
    28   val is_equals         : term -> bool
    29   val loops		: Sign.sg -> term list -> term -> term
    30                           -> string option * bool
    31   val mk_equals		: term * term -> term
    32   val mk_flexpair	: term * term -> term
    33   val mk_implies	: term * term -> term
    34   val mk_inclass	: typ * class -> term
    35   val mk_type		: typ -> term
    36   val occs		: term * term -> bool
    37   val rule_of		: (term*term)list * term list * term -> term
    38   val set_rename_prefix	: string -> unit   
    39   val skip_flexpairs	: term -> term
    40   val strip_assums_concl: term -> term
    41   val strip_assums_hyp	: term -> term list
    42   val strip_flexpairs	: term -> (term*term)list * term
    43   val strip_horn	: term -> (term*term)list * term list * term
    44   val strip_imp_concl	: term -> term
    45   val strip_imp_prems	: term -> term list
    46   val strip_params	: term -> (string * typ) list
    47   val strip_prems	: int * term list * term -> term list * term
    48   val unvarify		: term -> term
    49   val varify		: term -> term
    50   val termord		: term * term -> order
    51   val lextermord	: term list * term list -> order
    52   val termless		: term * term -> bool
    53   end;
    54 
    55 structure Logic : LOGIC =
    56 struct
    57 
    58 (*** Abstract syntax operations on the meta-connectives ***)
    59 
    60 (** equality **)
    61 
    62 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
    63 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    64 
    65 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    66   | dest_equals t = raise TERM("dest_equals", [t]);
    67 
    68 fun is_equals (Const ("==", _) $ _ $ _) = true
    69   | is_equals _ = false;
    70 
    71 
    72 (** implies **)
    73 
    74 fun mk_implies(A,B) = implies $ A $ B;
    75 
    76 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
    77   | dest_implies A = raise TERM("dest_implies", [A]);
    78 
    79 (** nested implications **)
    80 
    81 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
    82 fun list_implies ([], B) = B : term
    83   | list_implies (A::AS, B) = implies $ A $ list_implies(AS,B);
    84 
    85 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
    86 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
    87   | strip_imp_prems _ = [];
    88 
    89 (* A1==>...An==>B  goes to B, where B is not an implication *)
    90 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
    91   | strip_imp_concl A = A : term;
    92 
    93 (*Strip and return premises: (i, [], A1==>...Ai==>B)
    94     goes to   ([Ai, A(i-1),...,A1] , B) 	(REVERSED) 
    95   if  i<0 or else i too big then raises  TERM*)
    96 fun strip_prems (0, As, B) = (As, B) 
    97   | strip_prems (i, As, Const("==>", _) $ A $ B) = 
    98 	strip_prems (i-1, A::As, B)
    99   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   100 
   101 (*Count premises -- quicker than (length ostrip_prems) *)
   102 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   103   | count_prems (_,n) = n;
   104 
   105 (** flex-flex constraints **)
   106 
   107 (*Make a constraint.*)
   108 fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u;
   109 
   110 fun dest_flexpair (Const("=?=",_) $ t $ u)  =  (t,u)
   111   | dest_flexpair t = raise TERM("dest_flexpair", [t]);
   112 
   113 (*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C )
   114     goes to (a1=?=b1) ==>...(an=?=bn)==>C *)
   115 fun list_flexpairs ([], A) = A
   116   | list_flexpairs ((t,u)::pairs, A) =
   117 	implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A);
   118 
   119 (*Make the object-rule tpairs==>As==>B   *)
   120 fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B));
   121 
   122 (*Remove and return flexflex pairs: 
   123     (a1=?=b1)==>...(an=?=bn)==>C  to  ( [(a1,b1),...,(an,bn)] , C )	
   124   [Tail recursive in order to return a pair of results] *)
   125 fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) =
   126         strip_flex_aux ((t,u)::pairs, C)
   127   | strip_flex_aux (pairs,C) = (rev pairs, C);
   128 
   129 fun strip_flexpairs A = strip_flex_aux([], A);
   130 
   131 (*Discard flexflex pairs*)
   132 fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) =
   133 	skip_flexpairs C
   134   | skip_flexpairs C = C;
   135 
   136 (*strip a proof state (Horn clause): 
   137    (a1==b1)==>...(am==bm)==>B1==>...Bn==>C
   138     goes to   ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C)    *)
   139 fun strip_horn A =
   140   let val (tpairs,horn) = strip_flexpairs A 
   141   in  (tpairs, strip_imp_prems horn, strip_imp_concl horn)   end;
   142 
   143 (** types as terms **)
   144 
   145 fun mk_type ty = Const ("TYPE", itselfT ty);
   146 
   147 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   148   | dest_type t = raise TERM ("dest_type", [t]);
   149 
   150 (** class constraints **)
   151 
   152 fun mk_inclass (ty, c) =
   153   Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
   154 
   155 fun dest_inclass (t as Const (c_class, _) $ ty) =
   156       ((dest_type ty, Sign.class_of_const c_class)
   157         handle TERM _ => raise TERM ("dest_inclass", [t]))
   158   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   159 
   160 
   161 (*** Low-level term operations ***)
   162 
   163 (*Does t occur in u?  Or is alpha-convertible to u?
   164   The term t must contain no loose bound variables*)
   165 fun t occs u = (t aconv u) orelse 
   166       (case u of
   167           Abs(_,_,body) => t occs body
   168 	| f$t' => t occs f  orelse  t occs t'
   169 	| _ => false);
   170 
   171 (*Close up a formula over all free variables by quantification*)
   172 fun close_form A =
   173     list_all_free (map dest_Free (sort atless (term_frees A)),   
   174 		   A);
   175 
   176 
   177 (*** Specialized operations for resolution... ***)
   178 
   179 (*For all variables in the term, increment indexnames and lift over the Us
   180     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   181 fun incr_indexes (Us: typ list, inc:int) t = 
   182   let fun incr (Var ((a,i), T), lev) = 
   183 		Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   184 				lev, length Us)
   185 	| incr (Abs (a,T,body), lev) =
   186 		Abs (a, incr_tvar inc T, incr(body,lev+1))
   187 	| incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   188 	| incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   189 	| incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   190 	| incr (t,lev) = t
   191   in  incr(t,0)  end;
   192 
   193 (*Make lifting functions from subgoal and increment.
   194     lift_abs operates on tpairs (unification constraints)
   195     lift_all operates on propositions     *)
   196 fun lift_fns (B,inc) =
   197   let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   198 	| lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   199 	      Abs(a, T, lift_abs (T::Us, t) u)
   200 	| lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   201       fun lift_all (Us, Const("==>", _) $ A $ B) u =
   202 	      implies $ A $ lift_all (Us,B) u
   203 	| lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   204 	      all T $ Abs(a, T, lift_all (T::Us,t) u)
   205 	| lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   206   in  (lift_abs([],B), lift_all([],B))  end;
   207 
   208 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   209 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   210   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   211   | strip_assums_hyp B = [];
   212 
   213 (*Strips assumptions in goal, yielding conclusion.   *)
   214 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   215   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   216   | strip_assums_concl B = B;
   217 
   218 (*Make a list of all the parameters in a subgoal, even if nested*)
   219 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   220   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   221   | strip_params B = [];
   222 
   223 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   224     where j is the total number of parameters (precomputed) 
   225   If n>0 then deletes assumption n. *)
   226 fun remove_params j n A = 
   227     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   228     else case A of
   229         Const("==>", _) $ H $ B => 
   230 	  if n=1 then                           (remove_params j (n-1) B)
   231 	  else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   232       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   233       | _ => if n>0 then raise TERM("remove_params", [A])
   234              else A;
   235 
   236 (** Auto-renaming of parameters in subgoals **)
   237 
   238 val auto_rename = ref false
   239 and rename_prefix = ref "ka";
   240 
   241 (*rename_prefix is not exported; it is set by this function.*)
   242 fun set_rename_prefix a =
   243     if a<>"" andalso forall is_letter (explode a)
   244     then  (rename_prefix := a;  auto_rename := true)
   245     else  error"rename prefix must be nonempty and consist of letters";
   246 
   247 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   248   A name clash could cause the printer to rename bound vars;
   249     then res_inst_tac would not work properly.*)
   250 fun rename_vars (a, []) = []
   251   | rename_vars (a, (_,T)::vars) =
   252         (a,T) :: rename_vars (bump_string a, vars);
   253 
   254 (*Move all parameters to the front of the subgoal, renaming them apart;
   255   if n>0 then deletes assumption n. *)
   256 fun flatten_params n A =
   257     let val params = strip_params A;
   258 	val vars = if !auto_rename 
   259 		   then rename_vars (!rename_prefix, params)
   260 		   else ListPair.zip (variantlist(map #1 params,[]),
   261 				      map #2 params)
   262     in  list_all (vars, remove_params (length vars) n A)
   263     end;
   264 
   265 (*Makes parameters in a goal have the names supplied by the list cs.*)
   266 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   267       implies $ A $ list_rename_params (cs, B)
   268   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
   269       all T $ Abs(c, T, list_rename_params (cs, t))
   270   | list_rename_params (cs, B) = B;
   271 
   272 (*Strips assumptions in goal yielding  ( [Hn,...,H1], [xm,...,x1], B )
   273   where H1,...,Hn are the hypotheses and x1...xm are the parameters.   *)
   274 fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 
   275 	strip_assums_aux (H::Hs, params, B)
   276   | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
   277 	strip_assums_aux (Hs, (a,T)::params, t)
   278   | strip_assums_aux (Hs, params, B) = (Hs, params, B);
   279 
   280 fun strip_assums A = strip_assums_aux ([],[],A);
   281 
   282 
   283 (*Produces disagreement pairs, one for each assumption proof, in order.
   284   A is the first premise of the lifted rule, and thus has the form
   285     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B) *)
   286 fun assum_pairs A =
   287   let val (Hs, params, B) = strip_assums A
   288       val D = Unify.rlist_abs(params, B)
   289       fun pairrev ([],pairs) = pairs  
   290         | pairrev (H::Hs,pairs) = 
   291 	    pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   292   in  pairrev (Hs,[])   (*WAS:  map pair (rev Hs)  *)
   293   end;
   294 
   295 
   296 (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   297   without (?) everywhere*)
   298 fun varify (Const(a,T)) = Const(a, Type.varifyT T)
   299   | varify (Free(a,T)) = Var((a,0), Type.varifyT T)
   300   | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T)
   301   | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body)
   302   | varify (f$t) = varify f $ varify t
   303   | varify t = t;
   304 
   305 (*Inverse of varify.  Converts axioms back to their original form.*)
   306 fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
   307   | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
   308   | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
   309   | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)
   310   | unvarify (f$t) = unvarify f $ unvarify t
   311   | unvarify t = t;
   312 
   313 
   314 (*** term order ***)
   315 
   316 (* NB: non-linearity of the ordering is not a soundness problem *)
   317 
   318 (* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
   319 fun string_of_hd(Const(a,_)) = a
   320   | string_of_hd(Free(a,_))  = a
   321   | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
   322   | string_of_hd(Bound i)    = string_of_int i
   323   | string_of_hd(Abs _)      = "***ABSTRACTION***";
   324 
   325 (* a strict (not reflexive) linear well-founded AC-compatible ordering
   326  * for terms:
   327  * s < t <=> 1. size(s) < size(t) or
   328              2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
   329              3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   330                 (s1..sn) < (t1..tn) (lexicographically)
   331  *)
   332 
   333 (* FIXME: should really take types into account as well.
   334  * Otherwise non-linear *)
   335 fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
   336   | termord(t,u) =
   337       (case intord(size_of_term t,size_of_term u) of
   338          EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
   339                   in case stringord(string_of_hd f, string_of_hd g) of
   340                        EQUAL => lextermord(ts,us)
   341                      | ord   => ord
   342                   end
   343        | ord => ord)
   344 and lextermord(t::ts,u::us) =
   345       (case termord(t,u) of
   346          EQUAL => lextermord(ts,us)
   347        | ord   => ord)
   348   | lextermord([],[]) = EQUAL
   349   | lextermord _ = error("lextermord");
   350 
   351 fun termless tu = (termord tu = LESS);
   352 
   353 (** Check for looping rewrite rules **)
   354 
   355 fun vperm (Var _, Var _) = true
   356   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   357   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   358   | vperm (t, u) = (t = u);
   359 
   360 fun var_perm (t, u) =
   361   vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
   362 
   363 (*simple test for looping rewrite*)
   364 fun looptest sign prems lhs rhs =
   365    is_Var (head_of lhs)
   366   orelse
   367    (exists (apl (lhs,occs)) (rhs :: prems))
   368   orelse
   369    (null prems andalso
   370     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
   371 (*the condition "null prems" in the last case is necessary because
   372   conditional rewrites with extra variables in the conditions may terminate
   373   although the rhs is an instance of the lhs. Example:
   374   ?m < ?n ==> f(?n) == f(?m)*)
   375 
   376 fun loops sign prems lhs rhs =
   377   let
   378     val elhs = Pattern.eta_contract lhs;
   379     val erhs = Pattern.eta_contract rhs;
   380     val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
   381                andalso not (is_Var elhs)
   382   in (if not ((term_vars erhs) subset
   383               (union_term (term_vars elhs, List.concat(map term_vars prems))))
   384       then Some("extra Var(s) on rhs") else
   385       if not perm andalso looptest sign prems elhs erhs
   386       then Some("loops")
   387       else None
   388       ,perm)
   389   end;
   390 
   391 end;