src/Pure/logic.ML
author obua
Sun May 29 12:39:12 2005 +0200 (2005-05-29)
changeset 16108 cf468b93a02e
parent 15596 8665d08085df
child 16130 38b111451155
permissions -rw-r--r--
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
     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 infix occs;
    10 
    11 signature LOGIC =
    12 sig
    13   val is_all            : term -> bool
    14   val mk_equals         : term * term -> term
    15   val dest_equals       : term -> term * term
    16   val is_equals         : term -> bool
    17   val mk_implies        : term * term -> term
    18   val dest_implies      : term -> term * term
    19   val is_implies        : term -> bool
    20   val list_implies      : term list * term -> term
    21   val strip_imp_prems   : term -> term list
    22   val strip_imp_concl   : term -> term
    23   val strip_prems       : int * term list * term -> term list * term
    24   val count_prems       : term * int -> int
    25   val mk_conjunction    : term * term -> term
    26   val mk_conjunction_list: term list -> term
    27   val strip_horn        : term -> term list * term
    28   val mk_cond_defpair   : term list -> term * term -> string * term
    29   val mk_defpair        : term * term -> string * term
    30   val mk_type           : typ -> term
    31   val dest_type         : term -> typ
    32   val mk_inclass        : typ * class -> term
    33   val dest_inclass      : term -> typ * class
    34   val goal_const        : term
    35   val mk_goal           : term -> term
    36   val dest_goal         : term -> term
    37   val occs              : term * term -> bool
    38   val close_form        : term -> term
    39   val incr_indexes      : typ list * int -> term -> term
    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 ostrip_prems) *)
   116 fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1)
   117   | count_prems (_,n) = n;
   118 
   119 (*strip a proof state (Horn clause):
   120   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   121 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   122 
   123 
   124 (** conjunction **)
   125 
   126 fun mk_conjunction (t, u) =
   127   Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0));
   128 
   129 fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
   130   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   131 
   132 
   133 (** definitions **)
   134 
   135 fun mk_cond_defpair As (lhs, rhs) =
   136   (case Term.head_of lhs of
   137     Const (name, _) =>
   138       (Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs)))
   139   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   140 
   141 fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs;
   142 
   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 
   152 (** class constraints **)
   153 
   154 fun mk_inclass (ty, c) =
   155   Const (Sign.const_of_class c, itselfT ty --> propT) $ mk_type ty;
   156 
   157 fun dest_inclass (t as Const (c_class, _) $ ty) =
   158       ((dest_type ty, Sign.class_of_const c_class)
   159         handle TERM _ => raise TERM ("dest_inclass", [t]))
   160   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   161 
   162 
   163 (** atomic goals **)
   164 
   165 val goal_const = Const ("Goal", propT --> propT);
   166 fun mk_goal t = goal_const $ t;
   167 
   168 fun dest_goal (Const ("Goal", _) $ t) = t
   169   | dest_goal t = raise TERM ("dest_goal", [t]);
   170 
   171 
   172 (*** Low-level term operations ***)
   173 
   174 (*Does t occur in u?  Or is alpha-convertible to u?
   175   The term t must contain no loose bound variables*)
   176 fun t occs u = exists_subterm (fn s => t aconv s) u;
   177 
   178 (*Close up a formula over all free variables by quantification*)
   179 fun close_form A =
   180   list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
   181 
   182 
   183 (*** Specialized operations for resolution... ***)
   184 
   185 (*For all variables in the term, increment indexnames and lift over the Us
   186     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   187 fun incr_indexes (Us: typ list, inc:int) t =
   188   let fun incr (Var ((a,i), T), lev) =
   189                 Unify.combound (Var((a, i+inc), Us---> incr_tvar inc T),
   190                                 lev, length Us)
   191         | incr (Abs (a,T,body), lev) =
   192                 Abs (a, incr_tvar inc T, incr(body,lev+1))
   193         | incr (Const(a,T),_) = Const(a, incr_tvar inc T)
   194         | incr (Free(a,T),_) = Free(a, incr_tvar inc T)
   195         | incr (f$t, lev) = incr(f,lev) $ incr(t,lev)
   196         | incr (t,lev) = t
   197   in  incr(t,0)  end;
   198 
   199 (*Make lifting functions from subgoal and increment.
   200     lift_abs operates on tpairs (unification constraints)
   201     lift_all operates on propositions     *)
   202 fun lift_fns (B,inc) =
   203   let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
   204         | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
   205               Abs(a, T, lift_abs (T::Us, t) u)
   206         | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
   207       fun lift_all (Us, Const("==>", _) $ A $ B) u =
   208               implies $ A $ lift_all (Us,B) u
   209         | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
   210               all T $ Abs(a, T, lift_all (T::Us,t) u)
   211         | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
   212   in  (lift_abs([],B), lift_all([],B))  end;
   213 
   214 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   215 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B
   216   | strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t
   217   | strip_assums_hyp B = [];
   218 
   219 (*Strips assumptions in goal, yielding conclusion.   *)
   220 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   221   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   222   | strip_assums_concl B = B;
   223 
   224 (*Make a list of all the parameters in a subgoal, even if nested*)
   225 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   226   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   227   | strip_params B = [];
   228 
   229 (*test for meta connectives in prems of a 'subgoal'*)
   230 fun has_meta_prems prop i =
   231   let
   232     fun is_meta (Const ("==>", _) $ _ $ _) = true
   233       | is_meta (Const ("==", _) $ _ $ _) = true
   234       | is_meta (Const ("all", _) $ _) = true
   235       | is_meta _ = false;
   236   in
   237     (case strip_prems (i, [], prop) of
   238       (B :: _, _) => exists is_meta (strip_assums_hyp B)
   239     | _ => false) handle TERM _ => false
   240   end;
   241 
   242 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   243     where j is the total number of parameters (precomputed)
   244   If n>0 then deletes assumption n. *)
   245 fun remove_params j n A =
   246     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   247     else case A of
   248         Const("==>", _) $ H $ B =>
   249           if n=1 then                           (remove_params j (n-1) B)
   250           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   251       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   252       | _ => if n>0 then raise TERM("remove_params", [A])
   253              else A;
   254 
   255 (** Auto-renaming of parameters in subgoals **)
   256 
   257 val auto_rename = ref false
   258 and rename_prefix = ref "ka";
   259 
   260 (*rename_prefix is not exported; it is set by this function.*)
   261 fun set_rename_prefix a =
   262     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   263     then  (rename_prefix := a;  auto_rename := true)
   264     else  error"rename prefix must be nonempty and consist of letters";
   265 
   266 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   267   A name clash could cause the printer to rename bound vars;
   268     then res_inst_tac would not work properly.*)
   269 fun rename_vars (a, []) = []
   270   | rename_vars (a, (_,T)::vars) =
   271         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   272 
   273 (*Move all parameters to the front of the subgoal, renaming them apart;
   274   if n>0 then deletes assumption n. *)
   275 fun flatten_params n A =
   276     let val params = strip_params A;
   277         val vars = if !auto_rename
   278                    then rename_vars (!rename_prefix, params)
   279                    else ListPair.zip (variantlist(map #1 params,[]),
   280                                       map #2 params)
   281     in  list_all (vars, remove_params (length vars) n A)
   282     end;
   283 
   284 (*Makes parameters in a goal have the names supplied by the list cs.*)
   285 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   286       implies $ A $ list_rename_params (cs, B)
   287   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   288       all T $ Abs(c, T, list_rename_params (cs, t))
   289   | list_rename_params (cs, B) = B;
   290 
   291 (*** Treatmsent of "assume", "erule", etc. ***)
   292 
   293 (*Strips assumptions in goal yielding  
   294    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   295   where x1...xm are the parameters. This version (21.1.2005) REQUIRES 
   296   the the parameters to be flattened, but it allows erule to work on 
   297   assumptions of the form !!x. phi. Any !! after the outermost string
   298   will be regarded as belonging to the conclusion, and left untouched.
   299   Used ONLY by assum_pairs.
   300       Unless nasms<0, it can terminate the recursion early; that allows
   301   erule to work on assumptions of the form P==>Q.*)
   302 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   303   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 
   304       strip_assums_imp (nasms-1, H::Hs, B)
   305   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   306 
   307 
   308 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   309 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   310       strip_assums_all ((a,T)::params, t)
   311   | strip_assums_all (params, B) = (params, B);
   312 
   313 (*Produces disagreement pairs, one for each assumption proof, in order.
   314   A is the first premise of the lifted rule, and thus has the form
   315     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   316   nasms is the number of assumptions in the original subgoal, needed when B
   317     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   318 fun assum_pairs(nasms,A) =
   319   let val (params, A') = strip_assums_all ([],A)
   320       val (Hs,B) = strip_assums_imp (nasms,[],A')
   321       fun abspar t = Unify.rlist_abs(params, t)
   322       val D = abspar B
   323       fun pairrev ([], pairs) = pairs
   324         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   325   in  pairrev (Hs,[])
   326   end;
   327 
   328 (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   329   without (?) everywhere*)
   330 fun varify (Const(a,T)) = Const(a, Type.varifyT T)
   331   | varify (Free(a,T)) = Var((a,0), Type.varifyT T)
   332   | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T)
   333   | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body)
   334   | varify (f$t) = varify f $ varify t
   335   | varify t = t;
   336 
   337 (*Inverse of varify.  Converts axioms back to their original form.*)
   338 fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
   339   | unvarify (Free(a,T))     = Free(a, Type.unvarifyT T)  (* CB: added *)
   340   | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
   341   | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
   342   | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)
   343   | unvarify (f$t) = unvarify f $ unvarify t
   344   | unvarify t = t;
   345 
   346 
   347 (*Get subgoal i*)
   348 fun get_goal st i = List.nth (strip_imp_prems st, i-1)
   349   handle Subscript => error "Goal number out of range";
   350 
   351 (*reverses parameters for substitution*)
   352 fun goal_params st i =
   353   let val gi = get_goal st i
   354       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   355   in (gi, rfrees) end;
   356 
   357 fun concl_of_goal st i =
   358   let val (gi, rfrees) = goal_params st i
   359       val B = strip_assums_concl gi
   360   in subst_bounds (rfrees, B) end;
   361 
   362 fun prems_of_goal st i =
   363   let val (gi, rfrees) = goal_params st i
   364       val As = strip_assums_hyp gi
   365   in map (fn A => subst_bounds (rfrees, A)) As end;
   366 
   367 end;