src/Pure/logic.ML
author wenzelm
Fri Dec 19 10:15:51 1997 +0100 (1997-12-19)
changeset 4443 d55e85d7f0c2
parent 4345 7e9436ffb813
child 4631 c7fa4ae34495
permissions -rw-r--r--
term order stuff moved to term.ML;
     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 = (t aconv u) orelse 
   165       (case u of
   166           Abs(_,_,body) => t occs body
   167 	| f$t' => t occs f  orelse  t occs t'
   168 	| _ => false);
   169 
   170 (*Close up a formula over all free variables by quantification*)
   171 fun close_form A =
   172   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   173 
   174 
   175 (*** Specialized operations for resolution... ***)
   176 
   177 (*For all variables in the term, increment indexnames and lift over the Us
   178     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   179 fun incr_indexes (Us: typ list, inc:int) t = 
   180   let fun incr (Var ((a,i), T), lev) = 
   181 		Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   182 				lev, length Us)
   183 	| incr (Abs (a,T,body), lev) =
   184 		Abs (a, incr_tvar inc T, incr(body,lev+1))
   185 	| incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   186 	| incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   187 	| incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   188 	| incr (t,lev) = t
   189   in  incr(t,0)  end;
   190 
   191 (*Make lifting functions from subgoal and increment.
   192     lift_abs operates on tpairs (unification constraints)
   193     lift_all operates on propositions     *)
   194 fun lift_fns (B,inc) =
   195   let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   196 	| lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   197 	      Abs(a, T, lift_abs (T::Us, t) u)
   198 	| lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   199       fun lift_all (Us, Const("==>", _) $ A $ B) u =
   200 	      implies $ A $ lift_all (Us,B) u
   201 	| lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 
   202 	      all T $ Abs(a, T, lift_all (T::Us,t) u)
   203 	| lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   204   in  (lift_abs([],B), lift_all([],B))  end;
   205 
   206 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   207 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   208   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   209   | strip_assums_hyp B = [];
   210 
   211 (*Strips assumptions in goal, yielding conclusion.   *)
   212 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   213   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   214   | strip_assums_concl B = B;
   215 
   216 (*Make a list of all the parameters in a subgoal, even if nested*)
   217 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   218   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   219   | strip_params B = [];
   220 
   221 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   222     where j is the total number of parameters (precomputed) 
   223   If n>0 then deletes assumption n. *)
   224 fun remove_params j n A = 
   225     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   226     else case A of
   227         Const("==>", _) $ H $ B => 
   228 	  if n=1 then                           (remove_params j (n-1) B)
   229 	  else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   230       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   231       | _ => if n>0 then raise TERM("remove_params", [A])
   232              else A;
   233 
   234 (** Auto-renaming of parameters in subgoals **)
   235 
   236 val auto_rename = ref false
   237 and rename_prefix = ref "ka";
   238 
   239 (*rename_prefix is not exported; it is set by this function.*)
   240 fun set_rename_prefix a =
   241     if a<>"" andalso forall is_letter (explode a)
   242     then  (rename_prefix := a;  auto_rename := true)
   243     else  error"rename prefix must be nonempty and consist of letters";
   244 
   245 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   246   A name clash could cause the printer to rename bound vars;
   247     then res_inst_tac would not work properly.*)
   248 fun rename_vars (a, []) = []
   249   | rename_vars (a, (_,T)::vars) =
   250         (a,T) :: rename_vars (bump_string a, vars);
   251 
   252 (*Move all parameters to the front of the subgoal, renaming them apart;
   253   if n>0 then deletes assumption n. *)
   254 fun flatten_params n A =
   255     let val params = strip_params A;
   256 	val vars = if !auto_rename 
   257 		   then rename_vars (!rename_prefix, params)
   258 		   else ListPair.zip (variantlist(map #1 params,[]),
   259 				      map #2 params)
   260     in  list_all (vars, remove_params (length vars) n A)
   261     end;
   262 
   263 (*Makes parameters in a goal have the names supplied by the list cs.*)
   264 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   265       implies $ A $ list_rename_params (cs, B)
   266   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
   267       all T $ Abs(c, T, list_rename_params (cs, t))
   268   | list_rename_params (cs, B) = B;
   269 
   270 (*Strips assumptions in goal yielding  ( [Hn,...,H1], [xm,...,x1], B )
   271   where H1,...,Hn are the hypotheses and x1...xm are the parameters.   *)
   272 fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 
   273 	strip_assums_aux (H::Hs, params, B)
   274   | strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) =
   275 	strip_assums_aux (Hs, (a,T)::params, t)
   276   | strip_assums_aux (Hs, params, B) = (Hs, params, B);
   277 
   278 fun strip_assums A = strip_assums_aux ([],[],A);
   279 
   280 
   281 (*Produces disagreement pairs, one for each assumption proof, in order.
   282   A is the first premise of the lifted rule, and thus has the form
   283     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B) *)
   284 fun assum_pairs A =
   285   let val (Hs, params, B) = strip_assums A
   286       val D = Unify.rlist_abs(params, B)
   287       fun pairrev ([],pairs) = pairs  
   288         | pairrev (H::Hs,pairs) = 
   289 	    pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs)
   290   in  pairrev (Hs,[])   (*WAS:  map pair (rev Hs)  *)
   291   end;
   292 
   293 
   294 (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   295   without (?) everywhere*)
   296 fun varify (Const(a,T)) = Const(a, Type.varifyT T)
   297   | varify (Free(a,T)) = Var((a,0), Type.varifyT T)
   298   | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T)
   299   | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body)
   300   | varify (f$t) = varify f $ varify t
   301   | varify t = t;
   302 
   303 (*Inverse of varify.  Converts axioms back to their original form.*)
   304 fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
   305   | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
   306   | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
   307   | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)
   308   | unvarify (f$t) = unvarify f $ unvarify t
   309   | unvarify t = t;
   310 
   311 
   312 
   313 (** Test wellformedness of rewrite rules **)
   314 
   315 fun vperm (Var _, Var _) = true
   316   | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
   317   | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
   318   | vperm (t, u) = (t = u);
   319 
   320 fun var_perm (t, u) =
   321   vperm (t, u) andalso eq_set_term (term_vars t, term_vars u);
   322 
   323 (*simple test for looping rewrite*)
   324 fun looptest sign prems lhs rhs =
   325    is_Var (head_of lhs)
   326   orelse
   327    (exists (apl (lhs, op occs)) (rhs :: prems))
   328   orelse
   329    (null prems andalso
   330     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs));
   331 (*the condition "null prems" in the last case is necessary because
   332   conditional rewrites with extra variables in the conditions may terminate
   333   although the rhs is an instance of the lhs. Example:
   334   ?m < ?n ==> f(?n) == f(?m)*)
   335 
   336 fun rewrite_rule_extra_vars prems elhs erhs =
   337   if not ((term_vars erhs) subset
   338           (union_term (term_vars elhs, List.concat(map term_vars prems))))
   339   then Some("extra Var(s) on rhs") else
   340   if not ((term_tvars erhs) subset
   341           (term_tvars elhs  union  List.concat(map term_tvars prems)))
   342   then Some("extra TVar(s) on rhs")
   343   else None;
   344 
   345 fun rewrite_rule_ok sign prems lhs rhs =
   346   let
   347     val elhs = Pattern.eta_contract lhs;
   348     val erhs = Pattern.eta_contract rhs;
   349     val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs)
   350                andalso not (is_Var elhs)
   351   in (case rewrite_rule_extra_vars prems elhs erhs of
   352         None => if not perm andalso looptest sign prems elhs erhs
   353                 then Some("loops")
   354                 else None
   355       | some => some
   356       ,perm)
   357   end;
   358 
   359 end;