added forall2 predicate lifter
authorhaftmann
Tue Nov 16 10:33:36 2010 +0100 (2010-11-16)
changeset 405646827505e96e1
parent 40563 1e218365a20e
child 40565 40cefa372680
added forall2 predicate lifter
src/Pure/Isar/code.ML
src/Pure/library.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/code.ML	Mon Nov 15 22:31:18 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Nov 16 10:33:36 2010 +0100
     1.3 @@ -565,7 +565,7 @@
     1.4        else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     1.5      val _ = check_eqn thy { allow_nonlinear = false,
     1.6        allow_consts = false, allow_pats = false } thm (lhs, rhs);
     1.7 -    val _ = if forall (Sign.of_sort thy) (Ts ~~ map snd vs') then ()
     1.8 +    val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
     1.9        else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
    1.10    in (thm, tyco) end;
    1.11  
     2.1 --- a/src/Pure/library.ML	Mon Nov 15 22:31:18 2010 +0100
     2.2 +++ b/src/Pure/library.ML	Tue Nov 16 10:33:36 2010 +0100
     2.3 @@ -97,6 +97,7 @@
     2.4    val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     2.5    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     2.6    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     2.7 +  val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
     2.8    val zip_options: 'a list -> 'b option list -> ('a * 'b) list
     2.9    val ~~ : 'a list * 'b list -> ('a * 'b) list
    2.10    val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
    2.11 @@ -543,6 +544,10 @@
    2.12    | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
    2.13    | fold2 f _ _ _ = raise UnequalLengths;
    2.14  
    2.15 +fun forall2 P [] [] = true
    2.16 +  | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
    2.17 +  | forall2 P _ _ = false;
    2.18 +
    2.19  fun map_split f [] = ([], [])
    2.20    | map_split f (x :: xs) =
    2.21        let
     3.1 --- a/src/Tools/nbe.ML	Mon Nov 15 22:31:18 2010 +0100
     3.2 +++ b/src/Tools/nbe.ML	Tue Nov 16 10:33:36 2010 +0100
     3.3 @@ -170,11 +170,10 @@
     3.4    | Abs of (int * (Univ list -> Univ)) * Univ list
     3.5                                         (*abstractions as closures*);
     3.6  
     3.7 -fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
     3.8 +fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
     3.9    | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
    3.10 -  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
    3.11 -  | same _ _ = false
    3.12 -and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
    3.13 +  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
    3.14 +  | same _ _ = false;
    3.15  
    3.16  
    3.17  (* constructor functions *)