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