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