1.1 --- a/src/Pure/logic.ML Fri Oct 28 22:27:56 2005 +0200
1.2 +++ b/src/Pure/logic.ML Fri Oct 28 22:27:57 2005 +0200
1.3 @@ -30,14 +30,15 @@
1.4 val dest_type : term -> typ
1.5 val mk_inclass : typ * class -> term
1.6 val dest_inclass : term -> typ * class
1.7 - val goal_const : term
1.8 - val mk_goal : term -> term
1.9 - val dest_goal : term -> term
1.10 + val protectC : term
1.11 + val protect : term -> term
1.12 + val unprotect : term -> term
1.13 val occs : term * term -> bool
1.14 val close_form : term -> term
1.15 val incr_indexes : typ list * int -> term -> term
1.16 val incr_tvar : int -> typ -> typ
1.17 - val lift_fns : term * int -> (term -> term) * (term -> term)
1.18 + val lift_abs : int -> term -> term -> term
1.19 + val lift_all : int -> term -> term -> term
1.20 val strip_assums_hyp : term -> term list
1.21 val strip_assums_concl: term -> term
1.22 val strip_params : term -> (string * typ) list
1.23 @@ -165,13 +166,14 @@
1.24 | dest_inclass t = raise TERM ("dest_inclass", [t]);
1.25
1.26
1.27 -(** atomic goals **)
1.28
1.29 -val goal_const = Const ("Goal", propT --> propT);
1.30 -fun mk_goal t = goal_const $ t;
1.31 +(** protected propositions **)
1.32
1.33 -fun dest_goal (Const ("Goal", _) $ t) = t
1.34 - | dest_goal t = raise TERM ("dest_goal", [t]);
1.35 +val protectC = Const ("prop", propT --> propT);
1.36 +fun protect t = protectC $ t;
1.37 +
1.38 +fun unprotect (Const ("prop", _) $ t) = t
1.39 + | unprotect t = raise TERM ("unprotect", [t]);
1.40
1.41
1.42 (*** Low-level term operations ***)
1.43 @@ -203,13 +205,13 @@
1.44 (*For all variables in the term, increment indexnames and lift over the Us
1.45 result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
1.46 fun incr_indexes ([], 0) t = t
1.47 - | incr_indexes (Us, k) t =
1.48 + | incr_indexes (Ts, k) t =
1.49 let
1.50 - val n = length Us;
1.51 + val n = length Ts;
1.52 val incrT = if k = 0 then I else incrT k;
1.53
1.54 fun incr lev (Var ((x, i), T)) =
1.55 - Unify.combound (Var ((x, i + k), Us ---> (incrT T handle SAME => T)), lev, n)
1.56 + Unify.combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
1.57 | incr lev (Abs (x, T, body)) =
1.58 (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
1.59 handle SAME => Abs (x, T, incr (lev + 1) body))
1.60 @@ -228,19 +230,22 @@
1.61
1.62
1.63 (*Make lifting functions from subgoal and increment.
1.64 - lift_abs operates on tpairs (unification constraints)
1.65 - lift_all operates on propositions *)
1.66 -fun lift_fns (B,inc) =
1.67 - let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u
1.68 - | lift_abs (Us, Const("all",_)$Abs(a,T,t)) u =
1.69 - Abs(a, T, lift_abs (T::Us, t) u)
1.70 - | lift_abs (Us, _) u = incr_indexes(rev Us, inc) u
1.71 - fun lift_all (Us, Const("==>", _) $ A $ B) u =
1.72 - implies $ A $ lift_all (Us,B) u
1.73 - | lift_all (Us, Const("all",_)$Abs(a,T,t)) u =
1.74 - all T $ Abs(a, T, lift_all (T::Us,t) u)
1.75 - | lift_all (Us, _) u = incr_indexes(rev Us, inc) u;
1.76 - in (lift_abs([],B), lift_all([],B)) end;
1.77 + lift_abs operates on terms
1.78 + lift_all operates on propositions *)
1.79 +
1.80 +fun lift_abs inc =
1.81 + let
1.82 + fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
1.83 + | lift Ts (Const ("all", _) $ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t)
1.84 + | lift Ts _ t = incr_indexes (rev Ts, inc) t;
1.85 + in lift [] end;
1.86 +
1.87 +fun lift_all inc =
1.88 + let
1.89 + fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
1.90 + | lift Ts ((c as Const ("all", _)) $ Abs (a, T, b)) t = c $ Abs (a, T, lift (T :: Ts) b t)
1.91 + | lift Ts _ t = incr_indexes (rev Ts, inc) t;
1.92 + in lift [] end;
1.93
1.94 (*Strips assumptions in goal, yielding list of hypotheses. *)
1.95 fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B