src/Pure/logic.ML
author wenzelm
Thu Jul 16 21:00:09 2009 +0200 (2009-07-16)
changeset 32020 9abf5d66606e
parent 32014 857367925493
child 32023 2d071ac5032f
permissions -rw-r--r--
use structure 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_indexes: typ list * int -> term -> term
    58   val incr_tvar: int -> typ -> typ
    59   val lift_abs: int -> term -> term -> term
    60   val lift_all: int -> term -> term -> term
    61   val strip_assums_hyp: term -> term list
    62   val strip_assums_concl: term -> term
    63   val strip_params: term -> (string * typ) list
    64   val has_meta_prems: term -> bool
    65   val flatten_params: int -> term -> term
    66   val list_rename_params: string list * term -> term
    67   val assum_pairs: int * term -> (term*term)list
    68   val assum_problems: int * term -> (term -> term) * term list * term
    69   val varifyT: typ -> typ
    70   val unvarifyT: typ -> typ
    71   val varify: term -> term
    72   val unvarify: term -> term
    73   val get_goal: term -> int -> term
    74   val goal_params: term -> int -> term * term list
    75   val prems_of_goal: term -> int -> term list
    76   val concl_of_goal: term -> int -> term
    77 end;
    78 
    79 structure Logic : LOGIC =
    80 struct
    81 
    82 
    83 (*** Abstract syntax operations on the meta-connectives ***)
    84 
    85 (** all **)
    86 
    87 fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
    88 
    89 fun is_all (Const ("all", _) $ Abs _) = true
    90   | is_all _ = false;
    91 
    92 fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
    93       let val (x, b) = Term.dest_abs abs  (*potentially slow*)
    94       in ((x, T), b) end
    95   | dest_all t = raise TERM ("dest_all", [t]);
    96 
    97 
    98 (** equality **)
    99 
   100 fun mk_equals (t, u) =
   101   let val T = Term.fastype_of t
   102   in Const ("==", T --> T --> propT) $ t $ u end;
   103 
   104 fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
   105   | dest_equals t = raise TERM ("dest_equals", [t]);
   106 
   107 
   108 (** implies **)
   109 
   110 val implies = Const ("==>", propT --> propT --> propT);
   111 
   112 fun mk_implies (A, B) = implies $ A $ B;
   113 
   114 fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
   115   | dest_implies A = raise TERM ("dest_implies", [A]);
   116 
   117 
   118 (** nested implications **)
   119 
   120 (* [A1,...,An], B  goes to  A1==>...An==>B  *)
   121 fun list_implies ([], B) = B
   122   | list_implies (A::As, B) = implies $ A $ list_implies(As,B);
   123 
   124 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   125 fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B
   126   | strip_imp_prems _ = [];
   127 
   128 (* A1==>...An==>B  goes to B, where B is not an implication *)
   129 fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B
   130   | strip_imp_concl A = A : term;
   131 
   132 (*Strip and return premises: (i, [], A1==>...Ai==>B)
   133     goes to   ([Ai, A(i-1),...,A1] , B)         (REVERSED)
   134   if  i<0 or else i too big then raises  TERM*)
   135 fun strip_prems (0, As, B) = (As, B)
   136   | strip_prems (i, As, Const("==>", _) $ A $ B) =
   137         strip_prems (i-1, A::As, B)
   138   | strip_prems (_, As, A) = raise TERM("strip_prems", A::As);
   139 
   140 (*Count premises -- quicker than (length o strip_prems) *)
   141 fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B
   142   | count_prems _ = 0;
   143 
   144 (*Select Ai from A1 ==>...Ai==>B*)
   145 fun nth_prem (1, Const ("==>", _) $ A $ _) = A
   146   | nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i - 1, B)
   147   | nth_prem (_, A) = raise TERM ("nth_prem", [A]);
   148 
   149 (*strip a proof state (Horn clause):
   150   B1 ==> ... Bn ==> C   goes to   ([B1, ..., Bn], C)    *)
   151 fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
   152 
   153 
   154 
   155 (** conjunction **)
   156 
   157 val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
   158 val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
   159 
   160 
   161 (*A &&& B*)
   162 fun mk_conjunction (A, B) = conjunction $ A $ B;
   163 
   164 (*A &&& B &&& C -- improper*)
   165 fun mk_conjunction_list [] = true_prop
   166   | mk_conjunction_list ts = foldr1 mk_conjunction ts;
   167 
   168 (*(A &&& B) &&& (C &&& D) -- balanced*)
   169 fun mk_conjunction_balanced [] = true_prop
   170   | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
   171 
   172 
   173 (*A &&& B*)
   174 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
   175   | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
   176 
   177 (*A &&& B &&& C -- improper*)
   178 fun dest_conjunction_list t =
   179   (case try dest_conjunction t of
   180     NONE => [t]
   181   | SOME (A, B) => A :: dest_conjunction_list B);
   182 
   183 (*(A &&& B) &&& (C &&& D) -- balanced*)
   184 fun dest_conjunction_balanced 0 _ = []
   185   | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
   186 
   187 (*((A &&& B) &&& C) &&& D &&& E -- flat*)
   188 fun dest_conjunctions t =
   189   (case try dest_conjunction t of
   190     NONE => [t]
   191   | SOME (A, B) => dest_conjunctions A @ dest_conjunctions B);
   192 
   193 
   194 
   195 (** types as terms **)
   196 
   197 fun mk_type ty = Const ("TYPE", Term.itselfT ty);
   198 
   199 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   200   | dest_type t = raise TERM ("dest_type", [t]);
   201 
   202 fun type_map f = dest_type o f o mk_type;
   203 
   204 
   205 
   206 (** type classes **)
   207 
   208 (* const names *)
   209 
   210 val classN = "_class";
   211 
   212 val const_of_class = suffix classN;
   213 
   214 fun class_of_const c = unsuffix classN c
   215   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   216 
   217 
   218 (* class membership *)
   219 
   220 fun mk_of_class (ty, c) =
   221   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   222 
   223 fun dest_of_class (t as Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   224   | dest_of_class t = raise TERM ("dest_of_class", [t]);
   225 
   226 
   227 (* class relations *)
   228 
   229 fun name_classrel (c1, c2) =
   230   Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
   231 
   232 fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
   233 
   234 fun dest_classrel tm =
   235   (case dest_of_class tm of
   236     (TVar (_, [c1]), c2) => (c1, c2)
   237   | _ => raise TERM ("dest_classrel", [tm]));
   238 
   239 
   240 (* type arities *)
   241 
   242 fun name_arities (t, _, S) =
   243   let val b = Long_Name.base_name t
   244   in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
   245 
   246 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   247 
   248 fun mk_arities (t, Ss, S) =
   249   let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
   250   in map (fn c => mk_of_class (T, c)) S end;
   251 
   252 fun dest_arity tm =
   253   let
   254     fun err () = raise TERM ("dest_arity", [tm]);
   255 
   256     val (ty, c) = dest_of_class tm;
   257     val (t, tvars) =
   258       (case ty of
   259         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   260       | _ => err ());
   261     val Ss =
   262       if has_duplicates (eq_fst (op =)) tvars then err ()
   263       else map snd tvars;
   264   in (t, Ss, c) end;
   265 
   266 
   267 
   268 (** protected propositions and embedded terms **)
   269 
   270 val protectC = Const ("prop", propT --> propT);
   271 fun protect t = protectC $ t;
   272 
   273 fun unprotect (Const ("prop", _) $ t) = t
   274   | unprotect t = raise TERM ("unprotect", [t]);
   275 
   276 
   277 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
   278 
   279 fun dest_term (Const ("Pure.term", _) $ t) = t
   280   | dest_term t = raise TERM ("dest_term", [t]);
   281 
   282 
   283 
   284 (*** Low-level term operations ***)
   285 
   286 (*Does t occur in u?  Or is alpha-convertible to u?
   287   The term t must contain no loose bound variables*)
   288 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   289 
   290 (*Close up a formula over all free variables by quantification*)
   291 fun close_form A =
   292   Term.list_all_free (rev (Term.add_frees A []), A);
   293 
   294 
   295 
   296 (*** Specialized operations for resolution... ***)
   297 
   298 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   299 fun combound (t, n, k) =
   300     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   301 
   302 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   303 fun rlist_abs ([], body) = body
   304   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   305 
   306 
   307 fun incrT k = Term_Subst.map_atypsT_same
   308   (fn TVar ((a, i), S) => TVar ((a, i + k), S)
   309     | _ => raise Same.SAME);
   310 
   311 (*For all variables in the term, increment indexnames and lift over the Us
   312     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   313 fun incr_indexes ([], 0) t = t
   314   | incr_indexes (Ts, k) t =
   315       let
   316         val n = length Ts;
   317         val incrT = if k = 0 then I else incrT k;
   318 
   319         fun incr lev (Var ((x, i), T)) =
   320               combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
   321           | incr lev (Abs (x, T, body)) =
   322               (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
   323                 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
   324           | incr lev (t $ u) =
   325               (incr lev t $ (incr lev u handle Same.SAME => u)
   326                 handle Same.SAME => t $ incr lev u)
   327           | incr _ (Const (c, T)) = Const (c, incrT T)
   328           | incr _ (Free (x, T)) = Free (x, incrT T)
   329           | incr _ (t as Bound _) = t;
   330       in incr 0 t handle Same.SAME => t end;
   331 
   332 fun incr_tvar 0 T = T
   333   | incr_tvar k T = incrT k T handle Same.SAME => T;
   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;