src/Pure/logic.ML
author nipkow
Tue Nov 04 12:58:10 1997 +0100 (1997-11-04)
changeset 4116 42606637f87f
parent 3963 29c5ec9ecbaa
child 4318 9b672ea2dfe7
permissions -rw-r--r--
logic: loops -> rewrite_rule_ok
added rewrite_rule_extra_vars

thm: Rewrite rules must not introduce new type vars on rhs.
This lead to an incompleteness, is now banned, and the code
has been simplified.
     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 (* NB: non-linearity of the ordering is not a soundness problem *)
   318 
   319 (* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
   320 fun string_of_hd(Const(a,_)) = a
   321   | string_of_hd(Free(a,_))  = a
   322   | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
   323   | string_of_hd(Bound i)    = string_of_int i
   324   | string_of_hd(Abs _)      = "***ABSTRACTION***";
   325 
   326 (* a strict (not reflexive) linear well-founded AC-compatible ordering
   327  * for terms:
   328  * s < t <=> 1. size(s) < size(t) or
   329              2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
   330              3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   331                 (s1..sn) < (t1..tn) (lexicographically)
   332  *)
   333 
   334 (* FIXME: should really take types into account as well.
   335  * Otherwise non-linear *)
   336 fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
   337   | termord(t,u) =
   338       (case intord(size_of_term t,size_of_term u) of
   339          EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
   340                   in case stringord(string_of_hd f, string_of_hd g) of
   341                        EQUAL => lextermord(ts,us)
   342                      | ord   => ord
   343                   end
   344        | ord => ord)
   345 and lextermord(t::ts,u::us) =
   346       (case termord(t,u) of
   347          EQUAL => lextermord(ts,us)
   348        | ord   => ord)
   349   | lextermord([],[]) = EQUAL
   350   | lextermord _ = error("lextermord");
   351 
   352 fun termless tu = (termord tu = LESS);
   353 
   354 (** Test wellformedness of rewrite rules **)
   355 
   356 fun vperm (Var _, Var _) = true
   357   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   358   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   359   | vperm (t, u) = (t = u);
   360 
   361 fun var_perm (t, u) =
   362   vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
   363 
   364 (*simple test for looping rewrite*)
   365 fun looptest sign prems lhs rhs =
   366    is_Var (head_of lhs)
   367   orelse
   368    (exists (apl (lhs, op occs)) (rhs :: prems))
   369   orelse
   370    (null prems andalso
   371     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
   372 (*the condition "null prems" in the last case is necessary because
   373   conditional rewrites with extra variables in the conditions may terminate
   374   although the rhs is an instance of the lhs. Example:
   375   ?m < ?n ==> f(?n) == f(?m)*)
   376 
   377 fun rewrite_rule_extra_vars prems elhs erhs =
   378   if not ((term_vars erhs) subset
   379           (union_term (term_vars elhs, List.concat(map term_vars prems))))
   380   then Some("extra Var(s) on rhs") else
   381   if not ((term_tvars erhs) subset
   382           (term_tvars elhs  union  List.concat(map term_tvars prems)))
   383   then Some("extra TVar(s) on rhs")
   384   else None;
   385 
   386 fun rewrite_rule_ok sign prems lhs rhs =
   387   let
   388     val elhs = Pattern.eta_contract lhs;
   389     val erhs = Pattern.eta_contract rhs;
   390     val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
   391                andalso not (is_Var elhs)
   392   in (case rewrite_rule_extra_vars prems elhs erhs of
   393         None => if not perm andalso looptest sign prems elhs erhs
   394                 then Some("loops")
   395                 else None
   396       | some => some
   397       ,perm)
   398   end;
   399 
   400 end;