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