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