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