1.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Fri Nov 26 23:12:01 2010 +0100
     1.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Fri Nov 26 23:14:14 2010 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
     1.5  
     1.6  lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
     1.7 -  by normalization rule+
     1.8 +  by normalization
     1.9  lemma "rev [a, b, c] = [c, b, a]" by normalization
    1.10  value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
    1.11  value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
    1.12 @@ -108,10 +108,13 @@
    1.13  lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
    1.14  value [nbe] "Suc 0 \<in> set ms"
    1.15  
    1.16 +(* non-left-linear patterns, equality by extensionality *)
    1.17 +
    1.18  lemma "f = f" by normalization
    1.19  lemma "f x = f x" by normalization
    1.20  lemma "(f o g) x = f (g x)" by normalization
    1.21  lemma "(f o id) x = f x" by normalization
    1.22 +lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
    1.23  value [nbe] "(\<lambda>x. x)"
    1.24  
    1.25  (* Church numerals: *)

     2.1 --- a/src/Pure/library.ML	Fri Nov 26 23:12:01 2010 +0100
     2.2 +++ b/src/Pure/library.ML	Fri Nov 26 23:14:14 2010 +0100
     2.3 @@ -546,7 +546,7 @@
     2.4  
     2.5  fun forall2 P [] [] = true
     2.6    | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
     2.7 -  | forall2 P _ _ = false;
     2.8 +  | forall2 P _ _ = raise UnequalLengths;
     2.9  
    2.10  fun map_split f [] = ([], [])
    2.11    | map_split f (x :: xs) =

     3.1 --- a/src/Tools/nbe.ML	Fri Nov 26 23:12:01 2010 +0100
     3.2 +++ b/src/Tools/nbe.ML	Fri Nov 26 23:14:14 2010 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4    val apps: Univ -> Univ list -> Univ        (*explicit applications*)
     3.5    val abss: int -> (Univ list -> Univ) -> Univ
     3.6                                               (*abstractions as closures*)
     3.7 -  val same: Univ -> Univ -> bool
     3.8 +  val eq_Univ: Univ * Univ -> bool
     3.9  
    3.10    val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
    3.11    val trace: bool Unsynchronized.ref
    3.12 @@ -170,11 +170,6 @@
    3.13    | Abs of (int * (Univ list -> Univ)) * Univ list
    3.14                                         (*abstractions as closures*);
    3.15  
    3.16 -fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso forall2 same xs ys
    3.17 -  | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
    3.18 -  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso forall2 same xs ys
    3.19 -  | same _ _ = false;
    3.20 -
    3.21  
    3.22  (* constructor functions *)
    3.23  
    3.24 @@ -188,6 +183,28 @@
    3.25    | apps (Const (name, xs)) ys = Const (name, ys @ xs)
    3.26    | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
    3.27  
    3.28 +fun satisfy_abs (abs as ((n, f), xs)) some_k =
    3.29 +  let
    3.30 +    val ys = case some_k
    3.31 +     of NONE => replicate n (BVar (0, []))
    3.32 +      | SOME k => map_range (fn l => BVar (k + l, [])) n;
    3.33 +  in (apps (Abs abs) ys, ys) end;
    3.34 +
    3.35 +fun maxidx (Const (_, xs)) = fold maxidx xs
    3.36 +  | maxidx (DFree _) = I
    3.37 +  | maxidx (BVar (l, xs)) = fold maxidx xs #> Integer.max (l + 1)
    3.38 +  | maxidx (Abs abs) = maxidx (fst (satisfy_abs abs NONE));
    3.39 +
    3.40 +fun eq_Univ (Const (k, xs), Const (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
    3.41 +  | eq_Univ (DFree (s, k), DFree (t, l)) = s = t andalso k = l
    3.42 +  | eq_Univ (BVar (k, xs), BVar (l, ys)) = k = l andalso eq_list eq_Univ (xs, ys)
    3.43 +  | eq_Univ (x as Abs abs, y) =
    3.44 +      let
    3.45 +        val (x, ys) = satisfy_abs abs ((SOME o maxidx x o maxidx y) 0)
    3.46 +      in eq_Univ (x, apps y ys) end
    3.47 +  | eq_Univ (x, y as Abs _) = eq_Univ (y, x)
    3.48 +  | eq_Univ _ = false;
    3.49 +
    3.50  
    3.51  (** assembling and compiling ML code from terms **)
    3.52  
    3.53 @@ -241,7 +258,7 @@
    3.54    val name_const =  prefix ^ "Const";
    3.55    val name_abss =   prefix ^ "abss";
    3.56    val name_apps =   prefix ^ "apps";
    3.57 -  val name_same =   prefix ^ "same";
    3.58 +  val name_eq =     prefix ^ "eq_Univ";
    3.59  in
    3.60  
    3.61  val univs_cookie = (Univs.get, put_result, name_put);
    3.62 @@ -267,7 +284,7 @@
    3.63  fun nbe_abss 0 f = f `$` ml_list []
    3.64    | nbe_abss n f = name_abss `$$` [string_of_int n, f];
    3.65  
    3.66 -fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
    3.67 +fun nbe_eq (v1, v2) = "(" ^ name_eq ^ " (" ^ nbe_bound v1 ^ ", " ^ nbe_bound v2 ^ "))";
    3.68  
    3.69  end;
    3.70  
    3.71 @@ -353,7 +370,7 @@
    3.72          val (samepairs, args') = subst_nonlin_vars args;
    3.73          val s_args = map assemble_arg args';
    3.74          val s_rhs = if null samepairs then assemble_rhs rhs
    3.75 -          else ml_if (ml_and (map (uncurry nbe_same) samepairs))
    3.76 +          else ml_if (ml_and (map nbe_eq samepairs))
    3.77              (assemble_rhs rhs) default_rhs;
    3.78          val eqns = if is_eval then
    3.79              [([ml_list (rev (dicts @ s_args))], s_rhs)]