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