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