src/Pure/logic.ML
author wenzelm
Sun Mar 21 22:13:31 2010 +0100 (2010-03-21)
changeset 35854 d452abc96459
parent 35845 e5980f0ad025
child 36767 d0095729e1f1
permissions -rw-r--r--
Logic.mk_of_sort convenience;
     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 mk_of_sort: typ * sort -> term list
    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_tvar_same: int -> typ Same.operation
    59   val incr_tvar: int -> typ -> typ
    60   val incr_indexes_same: typ list * int -> term Same.operation
    61   val incr_indexes: typ list * int -> term -> term
    62   val lift_abs: int -> term -> term -> term
    63   val lift_all: int -> term -> term -> term
    64   val strip_assums_hyp: term -> term list
    65   val strip_assums_concl: term -> term
    66   val strip_params: term -> (string * typ) list
    67   val has_meta_prems: term -> bool
    68   val flatten_params: int -> term -> term
    69   val list_rename_params: string list * term -> term
    70   val assum_pairs: int * term -> (term*term)list
    71   val assum_problems: int * term -> (term -> term) * term list * term
    72   val varifyT_global: typ -> typ
    73   val unvarifyT_global: typ -> typ
    74   val varify_global: term -> term
    75   val unvarify_global: 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 = Balanced_Tree.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 = Balanced_Tree.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/sort membership *)
   222 
   223 fun mk_of_class (ty, c) =
   224   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
   225 
   226 fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   227   | dest_of_class t = raise TERM ("dest_of_class", [t]);
   228 
   229 fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
   230 
   231 
   232 (* class relations *)
   233 
   234 fun name_classrel (c1, c2) =
   235   Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
   236 
   237 fun mk_classrel (c1, c2) = mk_of_class (Term.aT [c1], c2);
   238 
   239 fun dest_classrel tm =
   240   (case dest_of_class tm of
   241     (TVar (_, [c1]), c2) => (c1, c2)
   242   | _ => raise TERM ("dest_classrel", [tm]));
   243 
   244 
   245 (* type arities *)
   246 
   247 fun name_arities (t, _, S) =
   248   let val b = Long_Name.base_name t
   249   in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
   250 
   251 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   252 
   253 fun mk_arities (t, Ss, S) =
   254   let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss))
   255   in map (fn c => mk_of_class (T, c)) S end;
   256 
   257 fun dest_arity tm =
   258   let
   259     fun err () = raise TERM ("dest_arity", [tm]);
   260 
   261     val (ty, c) = dest_of_class tm;
   262     val (t, tvars) =
   263       (case ty of
   264         Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ())
   265       | _ => err ());
   266     val Ss =
   267       if has_duplicates (eq_fst (op =)) tvars then err ()
   268       else map snd tvars;
   269   in (t, Ss, c) end;
   270 
   271 
   272 
   273 (** protected propositions and embedded terms **)
   274 
   275 val protectC = Const ("prop", propT --> propT);
   276 fun protect t = protectC $ t;
   277 
   278 fun unprotect (Const ("prop", _) $ t) = t
   279   | unprotect t = raise TERM ("unprotect", [t]);
   280 
   281 
   282 fun mk_term t = Const ("Pure.term", Term.fastype_of t --> propT) $ t;
   283 
   284 fun dest_term (Const ("Pure.term", _) $ t) = t
   285   | dest_term t = raise TERM ("dest_term", [t]);
   286 
   287 
   288 
   289 (*** Low-level term operations ***)
   290 
   291 (*Does t occur in u?  Or is alpha-convertible to u?
   292   The term t must contain no loose bound variables*)
   293 fun occs (t, u) = exists_subterm (fn s => t aconv s) u;
   294 
   295 (*Close up a formula over all free variables by quantification*)
   296 fun close_form A =
   297   Term.list_all_free (rev (Term.add_frees A []), A);
   298 
   299 
   300 
   301 (*** Specialized operations for resolution... ***)
   302 
   303 (*computes t(Bound(n+k-1),...,Bound(n))  *)
   304 fun combound (t, n, k) =
   305     if  k>0  then  combound (t,n+1,k-1) $ (Bound n)  else  t;
   306 
   307 (* ([xn,...,x1], t)   ======>   (x1,...,xn)t *)
   308 fun rlist_abs ([], body) = body
   309   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
   310 
   311 fun incr_tvar_same 0 = Same.same
   312   | incr_tvar_same k = Term_Subst.map_atypsT_same
   313       (fn TVar ((a, i), S) => TVar ((a, i + k), S)
   314         | _ => raise Same.SAME);
   315 
   316 fun incr_tvar k T = incr_tvar_same k T handle Same.SAME => T;
   317 
   318 (*For all variables in the term, increment indexnames and lift over the Us
   319     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   320 fun incr_indexes_same ([], 0) = Same.same
   321   | incr_indexes_same (Ts, k) =
   322       let
   323         val n = length Ts;
   324         val incrT = incr_tvar_same k;
   325 
   326         fun incr lev (Var ((x, i), T)) =
   327               combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
   328           | incr lev (Abs (x, T, body)) =
   329               (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
   330                 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
   331           | incr lev (t $ u) =
   332               (incr lev t $ (incr lev u handle Same.SAME => u)
   333                 handle Same.SAME => t $ incr lev u)
   334           | incr _ (Const (c, T)) = Const (c, incrT T)
   335           | incr _ (Free (x, T)) = Free (x, incrT T)
   336           | incr _ (Bound _) = raise Same.SAME;
   337       in incr 0 end;
   338 
   339 fun incr_indexes arg t = incr_indexes_same arg t handle Same.SAME => t;
   340 
   341 
   342 (* Lifting functions from subgoal and increment:
   343     lift_abs operates on terms
   344     lift_all operates on propositions *)
   345 
   346 fun lift_abs inc =
   347   let
   348     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   349       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   350       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   351   in lift [] end;
   352 
   353 fun lift_all inc =
   354   let
   355     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   356       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   357       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   358   in lift [] end;
   359 
   360 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   361 fun strip_assums_hyp B =
   362   let
   363     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   364       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   365           strip (map (incr_boundvars 1) Hs) t
   366       | strip Hs B = rev Hs
   367   in strip [] B end;
   368 
   369 (*Strips assumptions in goal, yielding conclusion.   *)
   370 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   371   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   372   | strip_assums_concl B = B;
   373 
   374 (*Make a list of all the parameters in a subgoal, even if nested*)
   375 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   376   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   377   | strip_params B = [];
   378 
   379 (*test for nested meta connectives in prems*)
   380 val has_meta_prems =
   381   let
   382     fun is_meta (Const ("==", _) $ _ $ _) = true
   383       | is_meta (Const ("==>", _) $ _ $ _) = true
   384       | is_meta (Const ("all", _) $ _) = true
   385       | is_meta _ = false;
   386     fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
   387       | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
   388       | ex_meta _ = false;
   389   in ex_meta end;
   390 
   391 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   392     where j is the total number of parameters (precomputed)
   393   If n>0 then deletes assumption n. *)
   394 fun remove_params j n A =
   395     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   396     else case A of
   397         Const("==>", _) $ H $ B =>
   398           if n=1 then                           (remove_params j (n-1) B)
   399           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   400       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   401       | _ => if n>0 then raise TERM("remove_params", [A])
   402              else A;
   403 
   404 (*Move all parameters to the front of the subgoal, renaming them apart;
   405   if n>0 then deletes assumption n. *)
   406 fun flatten_params n A =
   407     let val params = strip_params A;
   408         val vars = ListPair.zip (Name.variant_list [] (map #1 params),
   409                                  map #2 params)
   410     in  list_all (vars, remove_params (length vars) n A)
   411     end;
   412 
   413 (*Makes parameters in a goal have the names supplied by the list cs.*)
   414 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   415       implies $ A $ list_rename_params (cs, B)
   416   | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
   417       a $ Abs(c, T, list_rename_params (cs, t))
   418   | list_rename_params (cs, B) = B;
   419 
   420 
   421 
   422 (*** Treatment of "assume", "erule", etc. ***)
   423 
   424 (*Strips assumptions in goal yielding
   425    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   426   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   427   the the parameters to be flattened, but it allows erule to work on
   428   assumptions of the form !!x. phi. Any !! after the outermost string
   429   will be regarded as belonging to the conclusion, and left untouched.
   430   Used ONLY by assum_pairs.
   431       Unless nasms<0, it can terminate the recursion early; that allows
   432   erule to work on assumptions of the form P==>Q.*)
   433 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   434   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   435       strip_assums_imp (nasms-1, H::Hs, B)
   436   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   437 
   438 (*Strips OUTER parameters only.*)
   439 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   440       strip_assums_all ((a,T)::params, t)
   441   | strip_assums_all (params, B) = (params, B);
   442 
   443 (*Produces disagreement pairs, one for each assumption proof, in order.
   444   A is the first premise of the lifted rule, and thus has the form
   445     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   446   nasms is the number of assumptions in the original subgoal, needed when B
   447     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   448 fun assum_pairs(nasms,A) =
   449   let val (params, A') = strip_assums_all ([],A)
   450       val (Hs,B) = strip_assums_imp (nasms,[],A')
   451       fun abspar t = rlist_abs(params, t)
   452       val D = abspar B
   453       fun pairrev ([], pairs) = pairs
   454         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   455   in  pairrev (Hs,[])
   456   end;
   457 
   458 fun assum_problems (nasms, A) =
   459   let
   460     val (params, A') = strip_assums_all ([], A)
   461     val (Hs, B) = strip_assums_imp (nasms, [], A')
   462     fun abspar t = rlist_abs (params, t)
   463   in (abspar, rev Hs, B) 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_global_same ty = ty
   472   |> Term_Subst.map_atypsT_same
   473     (fn TFree (a, S) => TVar ((a, 0), S)
   474       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   475 
   476 fun unvarifyT_global_same ty = ty
   477   |> Term_Subst.map_atypsT_same
   478     (fn TVar ((a, 0), S) => TFree (a, S)
   479       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   480       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   481 
   482 val varifyT_global = Same.commit varifyT_global_same;
   483 val unvarifyT_global = Same.commit unvarifyT_global_same;
   484 
   485 fun varify_global tm = tm
   486   |> Same.commit (Term_Subst.map_aterms_same
   487     (fn Free (x, T) => Var ((x, 0), T)
   488       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   489       | _ => raise Same.SAME))
   490   |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
   491   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   492 
   493 fun unvarify_global tm = tm
   494   |> Same.commit (Term_Subst.map_aterms_same
   495     (fn Var ((x, 0), T) => Free (x, T)
   496       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   497       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   498       | _ => raise Same.SAME))
   499   |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
   500   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   501 
   502 
   503 (* goal states *)
   504 
   505 fun get_goal st i = nth_prem (i, st)
   506   handle TERM _ => error "Goal number out of range";
   507 
   508 (*reverses parameters for substitution*)
   509 fun goal_params st i =
   510   let val gi = get_goal st i
   511       val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
   512   in (gi, rfrees) end;
   513 
   514 fun concl_of_goal st i =
   515   let val (gi, rfrees) = goal_params st i
   516       val B = strip_assums_concl gi
   517   in subst_bounds (rfrees, B) end;
   518 
   519 fun prems_of_goal st i =
   520   let val (gi, rfrees) = goal_params st i
   521       val As = strip_assums_hyp gi
   522   in map (fn A => subst_bounds (rfrees, A)) As end;
   523 
   524 end;