src/Pure/logic.ML
author wenzelm
Tue Jul 14 12:18:52 2009 +0200 (2009-07-14)
changeset 32004 6ef7056e5215
parent 31981 9c59cbb9c5a2
child 32008 fa0cc3c8f73d
permissions -rw-r--r--
removed obsolete/unused legacy_unvarify;
     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 legacy_varifyT: typ -> typ
    74   val legacy_varify: 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 
   309 local exception SAME in
   310 
   311 fun incrT k =
   312   let
   313     fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
   314       | incr (Type (a, Ts)) = Type (a, incrs Ts)
   315       | incr _ = raise SAME
   316     and incrs (T :: Ts) =
   317         (incr T :: (incrs Ts handle SAME => Ts)
   318           handle SAME => T :: incrs Ts)
   319       | incrs [] = raise SAME;
   320   in incr end;
   321 
   322 (*For all variables in the term, increment indexnames and lift over the Us
   323     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
   324 fun incr_indexes ([], 0) t = t
   325   | incr_indexes (Ts, k) t =
   326   let
   327     val n = length Ts;
   328     val incrT = if k = 0 then I else incrT k;
   329 
   330     fun incr lev (Var ((x, i), T)) =
   331           combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
   332       | incr lev (Abs (x, T, body)) =
   333           (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
   334             handle SAME => Abs (x, T, incr (lev + 1) body))
   335       | incr lev (t $ u) =
   336           (incr lev t $ (incr lev u handle SAME => u)
   337             handle SAME => t $ incr lev u)
   338       | incr _ (Const (c, T)) = Const (c, incrT T)
   339       | incr _ (Free (x, T)) = Free (x, incrT T)
   340       | incr _ (t as Bound _) = t;
   341   in incr 0 t handle SAME => t end;
   342 
   343 fun incr_tvar 0 T = T
   344   | incr_tvar k T = incrT k T handle SAME => T;
   345 
   346 end;
   347 
   348 
   349 (* Lifting functions from subgoal and increment:
   350     lift_abs operates on terms
   351     lift_all operates on propositions *)
   352 
   353 fun lift_abs inc =
   354   let
   355     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
   356       | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
   357       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   358   in lift [] end;
   359 
   360 fun lift_all inc =
   361   let
   362     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
   363       | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
   364       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   365   in lift [] end;
   366 
   367 (*Strips assumptions in goal, yielding list of hypotheses.   *)
   368 fun strip_assums_hyp B =
   369   let
   370     fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B
   371       | strip Hs (Const ("all", _) $ Abs (a, T, t)) =
   372           strip (map (incr_boundvars 1) Hs) t
   373       | strip Hs B = rev Hs
   374   in strip [] B end;
   375 
   376 (*Strips assumptions in goal, yielding conclusion.   *)
   377 fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B
   378   | strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t
   379   | strip_assums_concl B = B;
   380 
   381 (*Make a list of all the parameters in a subgoal, even if nested*)
   382 fun strip_params (Const("==>", _) $ H $ B) = strip_params B
   383   | strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t
   384   | strip_params B = [];
   385 
   386 (*test for nested meta connectives in prems*)
   387 val has_meta_prems =
   388   let
   389     fun is_meta (Const ("==", _) $ _ $ _) = true
   390       | is_meta (Const ("==>", _) $ _ $ _) = true
   391       | is_meta (Const ("all", _) $ _) = true
   392       | is_meta _ = false;
   393     fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B
   394       | ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B
   395       | ex_meta _ = false;
   396   in ex_meta end;
   397 
   398 (*Removes the parameters from a subgoal and renumber bvars in hypotheses,
   399     where j is the total number of parameters (precomputed)
   400   If n>0 then deletes assumption n. *)
   401 fun remove_params j n A =
   402     if j=0 andalso n<=0 then A  (*nothing left to do...*)
   403     else case A of
   404         Const("==>", _) $ H $ B =>
   405           if n=1 then                           (remove_params j (n-1) B)
   406           else implies $ (incr_boundvars j H) $ (remove_params j (n-1) B)
   407       | Const("all",_)$Abs(a,T,t) => remove_params (j-1) n t
   408       | _ => if n>0 then raise TERM("remove_params", [A])
   409              else A;
   410 
   411 (*Move all parameters to the front of the subgoal, renaming them apart;
   412   if n>0 then deletes assumption n. *)
   413 fun flatten_params n A =
   414     let val params = strip_params A;
   415         val vars = ListPair.zip (Name.variant_list [] (map #1 params),
   416                                  map #2 params)
   417     in  list_all (vars, remove_params (length vars) n A)
   418     end;
   419 
   420 (*Makes parameters in a goal have the names supplied by the list cs.*)
   421 fun list_rename_params (cs, Const("==>", _) $ A $ B) =
   422       implies $ A $ list_rename_params (cs, B)
   423   | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
   424       a $ Abs(c, T, list_rename_params (cs, t))
   425   | list_rename_params (cs, B) = B;
   426 
   427 (*** Treatment of "assume", "erule", etc. ***)
   428 
   429 (*Strips assumptions in goal yielding
   430    HS = [Hn,...,H1],   params = [xm,...,x1], and B,
   431   where x1...xm are the parameters. This version (21.1.2005) REQUIRES
   432   the the parameters to be flattened, but it allows erule to work on
   433   assumptions of the form !!x. phi. Any !! after the outermost string
   434   will be regarded as belonging to the conclusion, and left untouched.
   435   Used ONLY by assum_pairs.
   436       Unless nasms<0, it can terminate the recursion early; that allows
   437   erule to work on assumptions of the form P==>Q.*)
   438 fun strip_assums_imp (0, Hs, B) = (Hs, B)  (*recursion terminated by nasms*)
   439   | strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) =
   440       strip_assums_imp (nasms-1, H::Hs, B)
   441   | strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*)
   442 
   443 
   444 (*Strips OUTER parameters only, unlike similar legacy versions.*)
   445 fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) =
   446       strip_assums_all ((a,T)::params, t)
   447   | strip_assums_all (params, B) = (params, B);
   448 
   449 (*Produces disagreement pairs, one for each assumption proof, in order.
   450   A is the first premise of the lifted rule, and thus has the form
   451     H1 ==> ... Hk ==> B   and the pairs are (H1,B),...,(Hk,B).
   452   nasms is the number of assumptions in the original subgoal, needed when B
   453     has the form B1 ==> B2: it stops B1 from being taken as an assumption. *)
   454 fun assum_pairs(nasms,A) =
   455   let val (params, A') = strip_assums_all ([],A)
   456       val (Hs,B) = strip_assums_imp (nasms,[],A')
   457       fun abspar t = rlist_abs(params, t)
   458       val D = abspar B
   459       fun pairrev ([], pairs) = pairs
   460         | pairrev (H::Hs, pairs) = pairrev(Hs,  (abspar H, D) :: pairs)
   461   in  pairrev (Hs,[])
   462   end;
   463 
   464 fun assum_problems (nasms, A) =
   465   let
   466     val (params, A') = strip_assums_all ([], A)
   467     val (Hs, B) = strip_assums_imp (nasms, [], A')
   468     fun abspar t = rlist_abs (params, t)
   469   in (abspar, rev Hs, B) end;
   470 
   471 
   472 (* global schematic variables *)
   473 
   474 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
   475 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
   476 
   477 fun varifyT_option ty = ty
   478   |> Term_Subst.map_atypsT_option
   479     (fn TFree (a, S) => SOME (TVar ((a, 0), S))
   480       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
   481 
   482 fun unvarifyT_option ty = ty
   483   |> Term_Subst.map_atypsT_option
   484     (fn TVar ((a, 0), S) => SOME (TFree (a, S))
   485       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
   486       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
   487 
   488 val varifyT = perhaps varifyT_option;
   489 val unvarifyT = perhaps unvarifyT_option;
   490 
   491 fun varify tm = tm
   492   |> perhaps (Term_Subst.map_aterms_option
   493     (fn Free (x, T) => SOME (Var ((x, 0), T))
   494       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   495       | _ => NONE))
   496   |> perhaps (Term_Subst.map_types_option varifyT_option)
   497   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   498 
   499 fun unvarify tm = tm
   500   |> perhaps (Term_Subst.map_aterms_option
   501     (fn Var ((x, 0), T) => SOME (Free (x, T))
   502       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   503       | Free (x, _) => raise TERM (bad_fixed x, [tm])
   504       | _ => NONE))
   505   |> perhaps (Term_Subst.map_types_option unvarifyT_option)
   506   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   507 
   508 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
   509 
   510 val legacy_varify =
   511   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
   512   Term.map_types legacy_varifyT;
   513 
   514 
   515 (* goal states *)
   516 
   517 fun get_goal st i = nth_prem (i, st)
   518   handle TERM _ => error "Goal number out of range";
   519 
   520 (*reverses parameters for substitution*)
   521 fun goal_params st i =
   522   let val gi = get_goal st i
   523       val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
   524   in (gi, rfrees) end;
   525 
   526 fun concl_of_goal st i =
   527   let val (gi, rfrees) = goal_params st i
   528       val B = strip_assums_concl gi
   529   in subst_bounds (rfrees, B) end;
   530 
   531 fun prems_of_goal st i =
   532   let val (gi, rfrees) = goal_params st i
   533       val As = strip_assums_hyp gi
   534   in map (fn A => subst_bounds (rfrees, A)) As end;
   535 
   536 end;