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