# HG changeset patch
# User haftmann
# Date 1156919409 -7200
# Node ID d2a30fed7596d637b191ba79c855f8d5f07125f1
# Parent  110a223ba63c1f4d284fb12d15fefe71de03f363
fixes

diff -r 110a223ba63c -r d2a30fed7596 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:29:30 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 08:30:09 2006 +0200
@@ -370,6 +370,7 @@
   in map mk_dist (sym_product cos) end;
 
 local
+  val not_sym = thm "HOL.not_sym";
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
 in fun get_eq thy dtco =
   let
@@ -396,6 +397,7 @@
     val distinct =
       mk_distinct cos
       |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+      |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
   in inject1 @ inject2 @ distinct end;
 end (*local*);
 
diff -r 110a223ba63c -r d2a30fed7596 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 08:29:30 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 08:30:09 2006 +0200
@@ -298,7 +298,7 @@
 code_constapp
   wfrec
     ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
-    haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)")
+    haskell (target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
 
 subsection{*Variants for TFL: the Recdef Package*}
 
diff -r 110a223ba63c -r d2a30fed7596 src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Wed Aug 30 08:29:30 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy	Wed Aug 30 08:30:09 2006 +0200
@@ -154,7 +154,6 @@
 
 val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
 
-
 fun conv ct =
   let
     val {thy, t, ...} = rep_cterm ct;
@@ -206,6 +205,6 @@
   "rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
 
 lemma
-  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc 0" by eval
+  "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
 
 end
diff -r 110a223ba63c -r d2a30fed7596 src/HOL/ex/CodeOperationalEquality.thy
--- a/src/HOL/ex/CodeOperationalEquality.thy	Wed Aug 30 08:29:30 2006 +0200
+++ b/src/HOL/ex/CodeOperationalEquality.thy	Wed Aug 30 08:30:09 2006 +0200
@@ -35,14 +35,12 @@
 ML {*
 fun constrain_op_eq thy thms =
   let
-    fun dest_eq (Const ("op =", ty)) =
-          (SOME o hd o fst o strip_type) ty
-      | dest_eq _ = NONE
-    fun eqs_of t =
-      fold_aterms (fn t => case dest_eq t
-       of SOME (TVar v_sort) => cons v_sort
-        | _ => I) t [];
-    val eqs = maps (eqs_of o Thm.prop_of) thms;
+    fun add_eq (Const ("op =", ty)) =
+          fold (insert (eq_fst (op = : indexname * indexname -> bool)))
+            (Term.add_tvarsT ty [])
+      | add_eq _ =
+          I
+    val eqs = fold (fold_aterms add_eq o Thm.prop_of) thms [];
     val instT = map (fn (v_i, sort) =>
       (Thm.ctyp_of thy (TVar (v_i, sort)),
          Thm.ctyp_of thy (TVar (v_i, Sorts.inter_sort (Sign.classes_of thy) (sort, [class_eq]))))) eqs;
@@ -82,14 +80,24 @@
 
 setup {*
 let
+  val lift_not_thm = thm "HOL.Eq_FalseI";
+  val lift_thm = thm "HOL.eq_reflection";
+  val eq_def_thm = Thm.symmetric (thm "eq_def");
   fun get_eq_thms thy tyco = case DatatypePackage.get_datatype thy tyco
    of SOME _ => DatatypeCodegen.get_eq thy tyco
     | NONE => case TypedefCodegen.get_triv_typedef thy tyco
        of SOME (_ ,(_, thm)) => [thm]
         | NONE => [];
-  fun get_eq_thms_eq thy ("OperationalEquality.eq", ty) = (case strip_type ty
+  fun get_eq_thms_eq thy ("CodeOperationalEquality.eq", ty) = (case strip_type ty
        of (Type (tyco, _) :: _, _) =>
              get_eq_thms thy tyco
+             |> map (perhaps (try (fn thm => lift_not_thm OF [thm])))
+             |> map (perhaps (try (fn thm => lift_thm OF [thm])))
+             (*|> tap (writeln o cat_lines o map string_of_thm)*)
+             |> constrain_op_eq thy
+             (*|> tap (writeln o cat_lines o map string_of_thm)*)
+             |> map (Tactic.rewrite_rule [eq_def_thm])
+             (*|> tap (writeln o cat_lines o map string_of_thm)*)
         | _ => [])
     | get_eq_thms_eq _ _ = [];
 in
@@ -138,8 +146,6 @@
   (eq :: int) haskell
 
 code_constapp
-  "eq"
-    haskell (infixl 4 "==")
   "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
     haskell (infixl 4 "==")
   "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
@@ -154,5 +160,7 @@
     haskell (infixl 4 "==")
   "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     haskell (infixl 4 "==")
+  "eq"
+    haskell (infixl 4 "==")
 
 end
\ No newline at end of file