src/Pure/logic.ML
author haftmann
Tue Sep 06 08:30:43 2005 +0200 (2005-09-06)
changeset 17271 2756a73f63a5
parent 17120 4ddeef83bd66
child 18029 19f1ad18bece
permissions -rw-r--r--
introduced some new-style AList operations
     1 (*  Title:      Pure/logic.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   Cambridge University 1992
     5 
     6 Abstract syntax operations of the Pure meta-logic.
     7 *)
     8 
     9 signature LOGIC =
    10 sig
    11   val is_all            : term -> bool
    12   val mk_equals         : term * term -> term
    13   val dest_equals       : term -> term * term
    14   val is_equals         : term -> bool
    15   val mk_implies        : term * term -> term
    16   val dest_implies      : term -> term * term
    17   val is_implies        : term -> bool
    18   val list_implies      : term list * term -> term
    19   val strip_imp_prems   : term -> term list
    20   val strip_imp_concl   : term -> term
    21   val strip_prems       : int * term list * term -> term list * term
    22   val count_prems       : term * int -> int
    23   val nth_prem          : int * term -> term
    24   val mk_conjunction    : term * term -> term
    25   val mk_conjunction_list: term list -> term
    26   val strip_horn        : term -> term list * term
    27   val mk_cond_defpair   : term list -> term * term -> string * term
    28   val mk_defpair        : term * term -> string * term
    29   val mk_type           : typ -> term
    30   val dest_type         : term -> typ
    31   val mk_inclass        : typ * class -> term
    32   val dest_inclass      : term -> typ * class
    33   val goal_const        : term
    34   val mk_goal           : term -> term
    35   val dest_goal         : term -> term
    36   val occs              : term * term -> bool
    37   val close_form        : term -> term
    38   val incr_indexes      : typ list * int -> term -> term
    39   val incr_tvar         : int -> typ -> typ
    40   val lift_fns          : term * int -> (term -> term) * (term -> term)
    41   val strip_assums_hyp  : term -> term list
    42   val strip_assums_concl: term -> term
    43   val strip_params      : term -> (string * typ) list
    44   val has_meta_prems    : term -> int -> bool
    45   val flatten_params    : int -> term -> term
    46   val auto_rename       : bool ref
    47   val set_rename_prefix : string -> unit
    48   val list_rename_params: string list * term -> term
    49   val assum_pairs       : int * term -> (term*term)list
    50   val varify            : term -> term
    51   val unvarify          : term -> term
    52   val get_goal          : term -> int -> term
    53   val goal_params       : term -> int -> term * term list
    54   val prems_of_goal     : term -> int -> term list
    55   val concl_of_goal     : term -> int -> term
    56 end;
    57 
    58 structure Logic : LOGIC =
    59 struct
    60 
    61 
    62 (*** Abstract syntax operations on the meta-connectives ***)
    63 
    64 (** all **)
    65 
    66 fun is_all (Const ("all", _) $ _) = true
    67   | is_all _ = false;
    68 
    69 
    70 (** equality **)
    71 
    72 (*Make an equality.  DOES NOT CHECK TYPE OF u*)
    73 fun mk_equals(t,u) = equals(fastype_of t) $ t $ u;
    74 
    75 fun dest_equals (Const("==",_) $ t $ u)  =  (t,u)
    76   | dest_equals t = raise TERM("dest_equals", [t]);
    77 
    78 fun is_equals (Const ("==", _) $ _ $ _) = true
    79   | is_equals _ = false;
    80 
    81 
    82 (** implies **)
    83 
    84 fun mk_implies(A,B) = implies $ A $ B;
    85 
    86 fun dest_implies (Const("==>",_) $ A $ B)  =  (A,B)
    87   | dest_implies A = raise TERM("dest_implies", [A]);
    88 
    89 fun is_implies (Const ("==>", _) $ _ $ _) = true
    90   | is_implies _ = false;
    91 
    92 
    93 (** nested implications **)
    94 
    95 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
    96 fun list_implies ([], B) = B : term
    97   | list_implies (A::AS, B) = implies $ A $ list_implies(AS,B);
    98 
    99 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   100 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   101   | strip_imp_prems _ = [];
   102 
   103 (* A1==>...An==>B  goes to B, where B is not an implication *)
   104 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   105   | strip_imp_concl A = A : term;
   106 
   107 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   108     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   109   if  i<0 or else i too big then raises  TERM*)
   110 fun strip_prems (0, As, B) = (As, B)
   111   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   112         strip_prems (i-1, A::As, B)
   113   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   114 
   115 (*Count premises -- quicker than (length o strip_prems) *)
   116 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   117   | count_prems (_,n) = n;
   118 
   119 (*Select Ai from A1 ==>...Ai==>B*)
   120 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   121   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   122   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   123 
   124 (*strip a proof state (Horn clause):
   125   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   126 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   127 
   128 
   129 (** conjunction **)
   130 
   131 fun mk_conjunction (t, u) =
   132   Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0));
   133 
   134 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   135   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   136 
   137 
   138 (** definitions **)
   139 
   140 fun mk_cond_defpair As (lhs, rhs) =
   141   (case Term.head_of lhs of
   142     Const (name, _) =>
   143       (Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   144   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   145 
   146 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   147 
   148 
   149 (** types as terms **)
   150 
   151 fun mk_type ty = Const ("TYPE", itselfT ty);
   152 
   153 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   154   | dest_type t = raise TERM ("dest_type", [t]);
   155 
   156 
   157 (** class constraints **)
   158 
   159 fun mk_inclass (ty, c) =
   160   Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
   161 
   162 fun dest_inclass (t as Const (c_class, _) $ ty) =
   163       ((dest_type ty, Sign.class_of_const c_class)
   164         handle TERM _ => raise TERM ("dest_inclass", [t]))
   165   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   166 
   167 
   168 (** atomic goals **)
   169 
   170 val goal_const = Const ("Goal", propT --> propT);
   171 fun mk_goal t = goal_const $ t;
   172 
   173 fun dest_goal (Const ("Goal", _) $ t) = t
   174   | dest_goal t = raise TERM ("dest_goal", [t]);
   175 
   176 
   177 (*** Low-level term operations ***)
   178 
   179 (*Does t occur in u?  Or is alpha-convertible to u?
   180   The term t must contain no loose bound variables*)
   181 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   182 
   183 (*Close up a formula over all free variables by quantification*)
   184 fun close_form A =
   185   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   186 
   187 
   188 (*** Specialized operations for resolution... ***)
   189 
   190 local exception SAME in
   191 
   192 fun incrT k =
   193   let
   194     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   195       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   196       | incr _ = raise SAME
   197     and incrs (T :: Ts) =
   198         (incr T :: (incrs Ts handle SAME => Ts)
   199           handle SAME => T :: incrs Ts)
   200       | incrs [] = raise SAME;
   201   in incr end;
   202 
   203 (*For all variables in the term, increment indexnames and lift over the Us
   204     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   205 fun incr_indexes ([], 0) t = t
   206   | incr_indexes (Us, k) t =
   207   let
   208     val n = length Us;
   209     val incrT = if k = 0 then I else incrT k;
   210 
   211     fun incr lev (Var ((x, i), T)) =
   212           Unify.combound (Var ((x, i + k), Us ---> (incrT T handle SAME => T)), lev, n)
   213       | incr lev (Abs (x, T, body)) =
   214           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   215             handle SAME => Abs (x, T, incr (lev + 1) body))
   216       | incr lev (t $ u) =
   217           (incr lev t $ (incr lev u handle SAME => u)
   218             handle SAME => t $ incr lev u)
   219       | incr _ (Const (c, T)) = Const (c, incrT T)
   220       | incr _ (Free (x, T)) = Free (x, incrT T)
   221       | incr _ (t as Bound _) = t;
   222   in incr 0 t handle SAME => t end;
   223 
   224 fun incr_tvar 0 T = T
   225   | incr_tvar k T = incrT k T handle SAME => T;
   226 
   227 end;
   228 
   229 
   230 (*Make lifting functions from subgoal and increment.
   231     lift_abs operates on tpairs (unification constraints)
   232     lift_all operates on propositions     *)
   233 fun lift_fns (B,inc) =
   234   let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   235         | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   236               Abs(a, T, lift_abs (T::Us, t) u)
   237         | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   238       fun lift_all (Us, Const("==>", _) $ A $ B) u =
   239               implies $ A $ lift_all (Us,B) u
   240         | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
   241               all T $ Abs(a, T, lift_all (T::Us,t) u)
   242         | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   243   in  (lift_abs([],B), lift_all([],B))  end;
   244 
   245 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   246 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   247   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   248   | strip_assums_hyp B = [];
   249 
   250 (*Strips assumptions in goal, yielding conclusion.   *)
   251 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   252   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   253   | strip_assums_concl B = B;
   254 
   255 (*Make a list of all the parameters in a subgoal, even if nested*)
   256 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   257   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   258   | strip_params B = [];
   259 
   260 (*test for meta connectives in prems of a 'subgoal'*)
   261 fun has_meta_prems prop i =
   262   let
   263     fun is_meta (Const ("==>", _) $ _ $ _) = true
   264       | is_meta (Const ("==", _) $ _ $ _) = true
   265       | is_meta (Const ("all", _) $ _) = true
   266       | is_meta _ = false;
   267   in
   268     (case strip_prems (i, [], prop) of
   269       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   270     | _ => false) handle TERM _ => false
   271   end;
   272 
   273 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   274     where j is the total number of parameters (precomputed)
   275   If n>0 then deletes assumption n. *)
   276 fun remove_params j n A =
   277     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   278     else case A of
   279         Const("==>", _) $ H $ B =>
   280           if n=1 then                           (remove_params j (n-1) B)
   281           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   282       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   283       | _ => if n>0 then raise TERM("remove_params", [A])
   284              else A;
   285 
   286 (** Auto-renaming of parameters in subgoals **)
   287 
   288 val auto_rename = ref false
   289 and rename_prefix = ref "ka";
   290 
   291 (*rename_prefix is not exported; it is set by this function.*)
   292 fun set_rename_prefix a =
   293     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   294     then  (rename_prefix := a;  auto_rename := true)
   295     else  error"rename prefix must be nonempty and consist of letters";
   296 
   297 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   298   A name clash could cause the printer to rename bound vars;
   299     then res_inst_tac would not work properly.*)
   300 fun rename_vars (a, []) = []
   301   | rename_vars (a, (_,T)::vars) =
   302         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   303 
   304 (*Move all parameters to the front of the subgoal, renaming them apart;
   305   if n>0 then deletes assumption n. *)
   306 fun flatten_params n A =
   307     let val params = strip_params A;
   308         val vars = if !auto_rename
   309                    then rename_vars (!rename_prefix, params)
   310                    else ListPair.zip (variantlist(map #1 params,[]),
   311                                       map #2 params)
   312     in  list_all (vars, remove_params (length vars) n A)
   313     end;
   314 
   315 (*Makes parameters in a goal have the names supplied by the list cs.*)
   316 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   317       implies $ A $ list_rename_params (cs, B)
   318   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   319       all T $ Abs(c, T, list_rename_params (cs, t))
   320   | list_rename_params (cs, B) = B;
   321 
   322 (*** Treatmsent of "assume", "erule", etc. ***)
   323 
   324 (*Strips assumptions in goal yielding
   325    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   326   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   327   the the parameters to be flattened, but it allows erule to work on
   328   assumptions of the form !!x. phi. Any !! after the outermost string
   329   will be regarded as belonging to the conclusion, and left untouched.
   330   Used ONLY by assum_pairs.
   331       Unless nasms<0, it can terminate the recursion early; that allows
   332   erule to work on assumptions of the form P==>Q.*)
   333 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   334   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   335       strip_assums_imp (nasms-1, H::Hs, B)
   336   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   337 
   338 
   339 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   340 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   341       strip_assums_all ((a,T)::params, t)
   342   | strip_assums_all (params, B) = (params, B);
   343 
   344 (*Produces disagreement pairs, one for each assumption proof, in order.
   345   A is the first premise of the lifted rule, and thus has the form
   346     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   347   nasms is the number of assumptions in the original subgoal, needed when B
   348     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   349 fun assum_pairs(nasms,A) =
   350   let val (params, A') = strip_assums_all ([],A)
   351       val (Hs,B) = strip_assums_imp (nasms,[],A')
   352       fun abspar t = Unify.rlist_abs(params, t)
   353       val D = abspar B
   354       fun pairrev ([], pairs) = pairs
   355         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   356   in  pairrev (Hs,[])
   357   end;
   358 
   359 (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   360   without (?) everywhere*)
   361 fun varify (Const(a, T)) = Const (a, Type.varifyT T)
   362   | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
   363   | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
   364   | varify (t as Bound _) = t
   365   | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
   366   | varify (f $ t) = varify f $ varify t;
   367 
   368 (*Inverse of varify.  Converts axioms back to their original form.*)
   369 fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
   370   | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
   371   | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
   372   | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
   373   | unvarify (t as Bound _) = t
   374   | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
   375   | unvarify (f $ t) = unvarify f $ unvarify t;
   376 
   377 
   378 (* goal states *)
   379 
   380 fun get_goal st i = nth_prem (i, st)
   381   handle TERM _ => error "Goal number out of range";
   382 
   383 (*reverses parameters for substitution*)
   384 fun goal_params st i =
   385   let val gi = get_goal st i
   386       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   387   in (gi, rfrees) end;
   388 
   389 fun concl_of_goal st i =
   390   let val (gi, rfrees) = goal_params st i
   391       val B = strip_assums_concl gi
   392   in subst_bounds (rfrees, B) end;
   393 
   394 fun prems_of_goal st i =
   395   let val (gi, rfrees) = goal_params st i
   396       val As = strip_assums_hyp gi
   397   in map (fn A => subst_bounds (rfrees, A)) As end;
   398 
   399 end;