src/Pure/logic.ML
author wenzelm
Thu Oct 04 20:29:24 2007 +0200 (2007-10-04)
changeset 24848 5dbbd33c3236
parent 24258 2f399483535a
child 25939 ddea202704b4
permissions -rw-r--r--
replaced literal 'a by Name.aT;
     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 dest_all: term -> typ * term
    12   val mk_equals: term * term -> term
    13   val dest_equals: term -> term * term
    14   val mk_implies: term * term -> term
    15   val dest_implies: term -> term * term
    16   val list_implies: term list * term -> term
    17   val strip_imp_prems: term -> term list
    18   val strip_imp_concl: term -> term
    19   val strip_prems: int * term list * term -> term list * term
    20   val count_prems: term -> int
    21   val nth_prem: int * term -> term
    22   val true_prop: term
    23   val conjunction: term
    24   val mk_conjunction: term * term -> term
    25   val mk_conjunction_list: term list -> term
    26   val mk_conjunction_balanced: term list -> term
    27   val dest_conjunction: term -> term * term
    28   val dest_conjunction_list: term -> term list
    29   val dest_conjunction_balanced: int -> term -> term list
    30   val dest_conjunctions: term -> term list
    31   val strip_horn: term -> term list * term
    32   val mk_type: typ -> term
    33   val dest_type: term -> typ
    34   val type_map: (term -> term) -> typ -> typ
    35   val const_of_class: class -> string
    36   val class_of_const: string -> class
    37   val mk_inclass: typ * class -> term
    38   val dest_inclass: term -> typ * class
    39   val name_classrel: string * string -> string
    40   val mk_classrel: class * class -> term
    41   val dest_classrel: term -> class * class
    42   val name_arities: arity -> string list
    43   val name_arity: string * sort list * class -> string
    44   val mk_arities: arity -> term list
    45   val dest_arity: term -> string * sort list * class
    46   val protectC: term
    47   val protect: term -> term
    48   val unprotect: term -> term
    49   val mk_term: term -> term
    50   val dest_term: term -> term
    51   val occs: term * term -> bool
    52   val close_form: term -> term
    53   val combound: term * int * int -> term
    54   val rlist_abs: (string * typ) list * term -> term
    55   val incr_indexes: typ list * int -> term -> term
    56   val incr_tvar: int -> typ -> typ
    57   val lift_abs: int -> term -> term -> term
    58   val lift_all: int -> term -> term -> term
    59   val strip_assums_hyp: term -> term list
    60   val strip_assums_concl: term -> term
    61   val strip_params: term -> (string * typ) list
    62   val has_meta_prems: term -> bool
    63   val flatten_params: int -> term -> term
    64   val auto_rename: bool ref
    65   val set_rename_prefix: string -> unit
    66   val list_rename_params: string list * term -> term
    67   val assum_pairs: int * term -> (term*term)list
    68   val varifyT: typ -> typ
    69   val unvarifyT: typ -> typ
    70   val varify: term -> term
    71   val unvarify: term -> term
    72   val legacy_varifyT: typ -> typ
    73   val legacy_unvarifyT: typ -> typ
    74   val legacy_varify: term -> term
    75   val legacy_unvarify: term -> term
    76   val get_goal: term -> int -> term
    77   val goal_params: term -> int -> term * term list
    78   val prems_of_goal: term -> int -> term list
    79   val concl_of_goal: term -> int -> term
    80 end;
    81 
    82 structure Logic : LOGIC =
    83 struct
    84 
    85 
    86 (*** Abstract syntax operations on the meta-connectives ***)
    87 
    88 (** all **)
    89 
    90 fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    91   | dest_all t = raise TERM ("dest_all", [t]);
    92 
    93 
    94 (** equality **)
    95 
    96 fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
    97 
    98 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
    99   | dest_equals t = raise TERM ("dest_equals", [t]);
   100 
   101 
   102 (** implies **)
   103 
   104 fun mk_implies (A, B) = implies $ A $ B;
   105 
   106 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   107   | dest_implies A = raise TERM ("dest_implies", [A]);
   108 
   109 
   110 (** nested implications **)
   111 
   112 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   113 fun list_implies ([], B) = B
   114   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   115 
   116 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   117 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   118   | strip_imp_prems _ = [];
   119 
   120 (* A1==>...An==>B  goes to B, where B is not an implication *)
   121 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   122   | strip_imp_concl A = A : term;
   123 
   124 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   125     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   126   if  i<0 or else i too big then raises  TERM*)
   127 fun strip_prems (0, As, B) = (As, B)
   128   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   129         strip_prems (i-1, A::As, B)
   130   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   131 
   132 (*Count premises -- quicker than (length o strip_prems) *)
   133 fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
   134   | count_prems _ = 0;
   135 
   136 (*Select Ai from A1 ==>...Ai==>B*)
   137 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   138   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   139   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   140 
   141 (*strip a proof state (Horn clause):
   142   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   143 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   144 
   145 
   146 
   147 (** conjunction **)
   148 
   149 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
   150 val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
   151 
   152 
   153 (*A && B*)
   154 fun mk_conjunction (A, B) = conjunction $ A $ B;
   155 
   156 (*A && B && C -- improper*)
   157 fun mk_conjunction_list [] = true_prop
   158   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   159 
   160 (*(A && B) && (C && D) -- balanced*)
   161 fun mk_conjunction_balanced [] = true_prop
   162   | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
   163 
   164 
   165 (*A && B*)
   166 fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
   167   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   168 
   169 (*A && B && C -- improper*)
   170 fun dest_conjunction_list t =
   171   (case try dest_conjunction t of
   172     NONE => [t]
   173   | SOME (A, B) => A :: dest_conjunction_list B);
   174 
   175 (*(A && B) && (C && D) -- balanced*)
   176 fun dest_conjunction_balanced 0 _ = []
   177   | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
   178 
   179 (*((A && B) && C) && D && E -- flat*)
   180 fun dest_conjunctions t =
   181   (case try dest_conjunction t of
   182     NONE => [t]
   183   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   184 
   185 
   186 
   187 (** types as terms **)
   188 
   189 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   190 
   191 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   192   | dest_type t = raise TERM ("dest_type", [t]);
   193 
   194 fun type_map f = dest_type o f o mk_type;
   195 
   196 
   197 
   198 (** type classes **)
   199 
   200 (* const names *)
   201 
   202 val classN = "_class";
   203 
   204 val const_of_class = suffix classN;
   205 
   206 fun class_of_const c = unsuffix classN c
   207   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   208 
   209 
   210 (* class constraints *)
   211 
   212 fun mk_inclass (ty, c) =
   213   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   214 
   215 fun dest_inclass (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   216   | dest_inclass t = raise TERM ("dest_inclass", [t]);
   217 
   218 
   219 (* class relations *)
   220 
   221 fun name_classrel (c1, c2) =
   222   NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
   223 
   224 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
   225 
   226 fun dest_classrel tm =
   227   (case dest_inclass tm of
   228     (TVar (_, [c1]), c2) => (c1, c2)
   229   | _ => raise TERM ("dest_classrel", [tm]));
   230 
   231 
   232 (* type arities *)
   233 
   234 fun name_arities (t, _, S) =
   235   let val b = NameSpace.base t
   236   in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
   237 
   238 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   239 
   240 fun mk_arities (t, Ss, S) =
   241   let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
   242   in map (fn c => mk_inclass (T, c)) S end;
   243 
   244 fun dest_arity tm =
   245   let
   246     fun err () = raise TERM ("dest_arity", [tm]);
   247 
   248     val (ty, c) = dest_inclass tm;
   249     val (t, tvars) =
   250       (case ty of
   251         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   252       | _ => err ());
   253     val Ss =
   254       if has_duplicates (eq_fst (op =)) tvars then err ()
   255       else map snd tvars;
   256   in (t, Ss, c) end;
   257 
   258 
   259 
   260   (** protected propositions and embedded terms **)
   261 
   262 val protectC = Const ("prop", propT --> propT);
   263 fun protect t = protectC $ t;
   264 
   265 fun unprotect (Const ("prop", _) $ t) = t
   266   | unprotect t = raise TERM ("unprotect", [t]);
   267 
   268 
   269 fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t --> propT) $ t;
   270 
   271 fun dest_term (Const ("ProtoPure.term", _) $ t) = t
   272   | dest_term t = raise TERM ("dest_term", [t]);
   273 
   274 
   275 
   276 (*** Low-level term operations ***)
   277 
   278 (*Does t occur in u?  Or is alpha-convertible to u?
   279   The term t must contain no loose bound variables*)
   280 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   281 
   282 (*Close up a formula over all free variables by quantification*)
   283 fun close_form A =
   284   Term.list_all_free (rev (Term.add_frees A []), A);
   285 
   286 
   287 
   288 (*** Specialized operations for resolution... ***)
   289 
   290 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   291 fun combound (t, n, k) =
   292     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   293 
   294 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   295 fun rlist_abs ([], body) = body
   296   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   297 
   298 
   299 local exception SAME in
   300 
   301 fun incrT k =
   302   let
   303     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   304       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   305       | incr _ = raise SAME
   306     and incrs (T :: Ts) =
   307         (incr T :: (incrs Ts handle SAME => Ts)
   308           handle SAME => T :: incrs Ts)
   309       | incrs [] = raise SAME;
   310   in incr end;
   311 
   312 (*For all variables in the term, increment indexnames and lift over the Us
   313     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   314 fun incr_indexes ([], 0) t = t
   315   | incr_indexes (Ts, k) t =
   316   let
   317     val n = length Ts;
   318     val incrT = if k = 0 then I else incrT k;
   319 
   320     fun incr lev (Var ((x, i), T)) =
   321           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   322       | incr lev (Abs (x, T, body)) =
   323           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   324             handle SAME => Abs (x, T, incr (lev + 1) body))
   325       | incr lev (t $ u) =
   326           (incr lev t $ (incr lev u handle SAME => u)
   327             handle SAME => t $ incr lev u)
   328       | incr _ (Const (c, T)) = Const (c, incrT T)
   329       | incr _ (Free (x, T)) = Free (x, incrT T)
   330       | incr _ (t as Bound _) = t;
   331   in incr 0 t handle SAME => t end;
   332 
   333 fun incr_tvar 0 T = T
   334   | incr_tvar k T = incrT k T handle SAME => T;
   335 
   336 end;
   337 
   338 
   339 (* Lifting functions from subgoal and increment:
   340     lift_abs operates on terms
   341     lift_all operates on propositions *)
   342 
   343 fun lift_abs inc =
   344   let
   345     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   346       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   347       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   348   in lift [] end;
   349 
   350 fun lift_all inc =
   351   let
   352     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   353       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   354       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   355   in lift [] end;
   356 
   357 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   358 fun strip_assums_hyp B =
   359   let
   360     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   361       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   362           strip (map (incr_boundvars 1) Hs) t
   363       | strip Hs B = rev Hs
   364   in strip [] B end;
   365 
   366 (*Strips assumptions in goal, yielding conclusion.   *)
   367 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   368   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   369   | strip_assums_concl B = B;
   370 
   371 (*Make a list of all the parameters in a subgoal, even if nested*)
   372 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   373   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   374   | strip_params B = [];
   375 
   376 (*test for nested meta connectives in prems*)
   377 val has_meta_prems =
   378   let
   379     fun is_meta (Const ("==", _) $ _ $ _) = true
   380       | is_meta (Const ("==>", _) $ _ $ _) = true
   381       | is_meta (Const ("all", _) $ _) = true
   382       | is_meta _ = false;
   383     fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
   384       | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
   385       | ex_meta _ = false;
   386   in ex_meta end;
   387 
   388 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   389     where j is the total number of parameters (precomputed)
   390   If n>0 then deletes assumption n. *)
   391 fun remove_params j n A =
   392     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   393     else case A of
   394         Const("==>", _) $ H $ B =>
   395           if n=1 then                           (remove_params j (n-1) B)
   396           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   397       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   398       | _ => if n>0 then raise TERM("remove_params", [A])
   399              else A;
   400 
   401 (** Auto-renaming of parameters in subgoals **)
   402 
   403 val auto_rename = ref false
   404 and rename_prefix = ref "ka";
   405 
   406 (*rename_prefix is not exported; it is set by this function.*)
   407 fun set_rename_prefix a =
   408     if a<>"" andalso forall Symbol.is_letter (Symbol.explode a)
   409     then  (rename_prefix := a;  auto_rename := true)
   410     else  error"rename prefix must be nonempty and consist of letters";
   411 
   412 (*Makes parameters in a goal have distinctive names (not guaranteed unique!)
   413   A name clash could cause the printer to rename bound vars;
   414     then res_inst_tac would not work properly.*)
   415 fun rename_vars (a, []) = []
   416   | rename_vars (a, (_,T)::vars) =
   417         (a,T) :: rename_vars (Symbol.bump_string a, vars);
   418 
   419 (*Move all parameters to the front of the subgoal, renaming them apart;
   420   if n>0 then deletes assumption n. *)
   421 fun flatten_params n A =
   422     let val params = strip_params A;
   423         val vars = if !auto_rename
   424                    then rename_vars (!rename_prefix, params)
   425                    else ListPair.zip (Name.variant_list [] (map #1 params),
   426                                       map #2 params)
   427     in  list_all (vars, remove_params (length vars) n A)
   428     end;
   429 
   430 (*Makes parameters in a goal have the names supplied by the list cs.*)
   431 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   432       implies $ A $ list_rename_params (cs, B)
   433   | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
   434       all T $ Abs(c, T, list_rename_params (cs, t))
   435   | list_rename_params (cs, B) = B;
   436 
   437 (*** Treatment of "assume", "erule", etc. ***)
   438 
   439 (*Strips assumptions in goal yielding
   440    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   441   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   442   the the parameters to be flattened, but it allows erule to work on
   443   assumptions of the form !!x. phi. Any !! after the outermost string
   444   will be regarded as belonging to the conclusion, and left untouched.
   445   Used ONLY by assum_pairs.
   446       Unless nasms<0, it can terminate the recursion early; that allows
   447   erule to work on assumptions of the form P==>Q.*)
   448 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   449   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   450       strip_assums_imp (nasms-1, H::Hs, B)
   451   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   452 
   453 
   454 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   455 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   456       strip_assums_all ((a,T)::params, t)
   457   | strip_assums_all (params, B) = (params, B);
   458 
   459 (*Produces disagreement pairs, one for each assumption proof, in order.
   460   A is the first premise of the lifted rule, and thus has the form
   461     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   462   nasms is the number of assumptions in the original subgoal, needed when B
   463     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   464 fun assum_pairs(nasms,A) =
   465   let val (params, A') = strip_assums_all ([],A)
   466       val (Hs,B) = strip_assums_imp (nasms,[],A')
   467       fun abspar t = rlist_abs(params, t)
   468       val D = abspar B
   469       fun pairrev ([], pairs) = pairs
   470         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   471   in  pairrev (Hs,[])
   472   end;
   473 
   474 
   475 (* global schematic variables *)
   476 
   477 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   478 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   479 
   480 fun varifyT ty = ty |> Term.map_atyps
   481   (fn TFree (a, S) => TVar ((a, 0), S)
   482     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   483 
   484 fun unvarifyT ty = ty |> Term.map_atyps
   485   (fn TVar ((a, 0), S) => TFree (a, S)
   486     | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   487     | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   488 
   489 fun varify tm =
   490   tm |> Term.map_aterms
   491     (fn Free (x, T) => Var ((x, 0), T)
   492       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   493       | t => t)
   494   |> Term.map_types varifyT
   495   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   496 
   497 fun unvarify tm =
   498   tm |> Term.map_aterms
   499     (fn Var ((x, 0), T) => Free (x, T)
   500       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   501       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   502       | t => t)
   503   |> Term.map_types unvarifyT
   504   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   505 
   506 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   507 val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S) | T => T);
   508 
   509 val legacy_varify =
   510   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   511   Term.map_types legacy_varifyT;
   512 
   513 val legacy_unvarify =
   514   Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
   515   Term.map_types legacy_unvarifyT;
   516 
   517 
   518 (* goal states *)
   519 
   520 fun get_goal st i = nth_prem (i, st)
   521   handle TERM _ => error "Goal number out of range";
   522 
   523 (*reverses parameters for substitution*)
   524 fun goal_params st i =
   525   let val gi = get_goal st i
   526       val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   527   in (gi, rfrees) end;
   528 
   529 fun concl_of_goal st i =
   530   let val (gi, rfrees) = goal_params st i
   531       val B = strip_assums_concl gi
   532   in subst_bounds (rfrees, B) end;
   533 
   534 fun prems_of_goal st i =
   535   let val (gi, rfrees) = goal_params st i
   536       val As = strip_assums_hyp gi
   537   in map (fn A => subst_bounds (rfrees, A)) As end;
   538 
   539 end;