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