added all, is_all;
authorwenzelm
Mon Jun 23 23:45:47 2008 +0200 (2008-06-23)
changeset 273343f17273766f2
parent 27333 7095f775131a
child 27335 e8eef124d0fd
added all, is_all;
improved dest_all;
added implies (from term.ML);
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Mon Jun 23 23:45:46 2008 +0200
     1.2 +++ b/src/Pure/logic.ML	Mon Jun 23 23:45:47 2008 +0200
     1.3 @@ -8,9 +8,12 @@
     1.4  
     1.5  signature LOGIC =
     1.6  sig
     1.7 -  val dest_all: term -> typ * term
     1.8 +  val all: term -> term -> term
     1.9 +  val is_all: term -> bool
    1.10 +  val dest_all: term -> (string * typ) * term
    1.11    val mk_equals: term * term -> term
    1.12    val dest_equals: term -> term * term
    1.13 +  val implies: term
    1.14    val mk_implies: term * term -> term
    1.15    val dest_implies: term -> term * term
    1.16    val list_implies: term list * term -> term
    1.17 @@ -85,13 +88,22 @@
    1.18  
    1.19  (** all **)
    1.20  
    1.21 -fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A)
    1.22 +fun all v t = Const ("all", (Term.fastype_of v --> propT) --> propT) $ lambda v t;
    1.23 +
    1.24 +fun is_all (Const ("all", _) $ Abs _) = true
    1.25 +  | is_all _ = false;
    1.26 +
    1.27 +fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) =
    1.28 +      let val (x, b) = Term.dest_abs abs  (*potentially slow*)
    1.29 +      in ((x, T), b) end
    1.30    | dest_all t = raise TERM ("dest_all", [t]);
    1.31  
    1.32  
    1.33  (** equality **)
    1.34  
    1.35 -fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u;
    1.36 +fun mk_equals (t, u) =
    1.37 +  let val T = Term.fastype_of t
    1.38 +  in Const ("==", T --> T --> propT) $ t $ u end;
    1.39  
    1.40  fun dest_equals (Const ("==", _) $ t $ u) = (t, u)
    1.41    | dest_equals t = raise TERM ("dest_equals", [t]);
    1.42 @@ -99,6 +111,8 @@
    1.43  
    1.44  (** implies **)
    1.45  
    1.46 +val implies = Const ("==>", propT --> propT --> propT);
    1.47 +
    1.48  fun mk_implies (A, B) = implies $ A $ B;
    1.49  
    1.50  fun dest_implies (Const ("==>", _) $ A $ B) = (A, B)
    1.51 @@ -408,8 +422,8 @@
    1.52  (*Makes parameters in a goal have the names supplied by the list cs.*)
    1.53  fun list_rename_params (cs, Const("==>", _) $ A $ B) =
    1.54        implies $ A $ list_rename_params (cs, B)
    1.55 -  | list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) =
    1.56 -      all T $ Abs(c, T, list_rename_params (cs, t))
    1.57 +  | list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) =
    1.58 +      a $ Abs(c, T, list_rename_params (cs, t))
    1.59    | list_rename_params (cs, B) = B;
    1.60  
    1.61  (*** Treatment of "assume", "erule", etc. ***)