# HG changeset patch
# User haftmann
# Date 1222327683 -7200
# Node ID b8390cd56b8fdab1f663c832a95ceafb1dfc48a9
# Parent  4562584d9d66a69e6835e2a9ecdbeec13a2991f7
discontinued special treatment of op = vs. eq_class.eq

diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -135,7 +135,7 @@
 subsubsection {* Code generator setup *}
 
 lemmas [code func del] = term.recs term.cases term.size
-lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
+lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
 
 lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -77,7 +77,10 @@
 text {* using built-in Haskell equality *}
 
 code_class eq
-  (Haskell "Eq" where "op =" \<equiv> "(==)")
+  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")
+
+code_const "eq_class.eq"
+  (Haskell infixl 4 "==")
 
 code_const "op ="
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Datatype.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -686,7 +686,7 @@
 code_instance option :: eq
   (Haskell -)
 
-code_const "op = \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved SML
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -1710,16 +1710,24 @@
 
 class eq = type +
   fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  assumes eq: "eq x y \<longleftrightarrow> x = y "
+  assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
 begin
 
+lemma eq: "eq = (op =)"
+  by (rule ext eq_equals)+
+
 lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
-  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
 declare equals_eq [symmetric, code post]
 
+lemma eq_refl: "eq x x \<longleftrightarrow> True"
+  unfolding eq by rule+
+
 end
 
+declare simp_thms(6) [code nbe]
+
 hide (open) const eq
 hide const eq
 
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -28,7 +28,7 @@
 code_reserved OCaml
   char
 
-code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -111,8 +111,8 @@
 qed
 
 lemma [code func]:
-  "k = l \<longleftrightarrow> nat_of_index k = nat_of_index l"
-  by (cases k, cases l) simp
+  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
+  by (cases k, cases l) (simp add: eq)
 
 
 subsection {* Indices as datatype of ints *}
@@ -319,7 +319,7 @@
   (OCaml "(fun n -> fun m ->/ (n '/ m, n mod m))")
   (Haskell "divMod")
 
-code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
   (OCaml "!((_ : int) = _)")
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -72,7 +72,7 @@
   (OCaml "Big'_int.mult'_big'_int")
   (Haskell infixl 7 "*")
 
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/Code_Message.thy
--- a/src/HOL/Library/Code_Message.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -50,7 +50,7 @@
 code_instance message_string :: eq
   (Haskell -)
 
-code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -400,7 +400,7 @@
   (OCaml "Big'_int.quomod'_big'_int")
   (Haskell "divMod")
 
-code_const "op = \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/RType.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -91,9 +91,9 @@
 *}
 
 lemma [code func]:
-  "Typerep tyco1 tys1 = Typerep tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2
-     \<and> list_all2 (op =) tys1 tys2"
-  by (auto simp add: list_all2_eq [symmetric])
+  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
+     \<and> list_all2 eq_class.eq tys1 tys2"
+  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
 
 code_type typerep
   (SML "Term.typ")
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/List.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -3625,7 +3625,7 @@
 code_instance list :: eq
   (Haskell -)
 
-code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 setup {*
diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Product_Type.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -22,13 +22,15 @@
 declare case_split [cases type: bool]
   -- "prefer plain propositional version"
 
-lemma [code func]:
-  shows "False = P \<longleftrightarrow> \<not> P"
-    and "True = P \<longleftrightarrow> P" 
-    and "P = False \<longleftrightarrow> \<not> P" 
-    and "P = True \<longleftrightarrow> P" by simp_all
+lemma
+  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
+    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
+    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
+    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
+    and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
+  by (simp_all add: eq)
 
-code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_instance bool :: eq
@@ -88,7 +90,7 @@
 instance unit :: eq ..
 
 lemma [code func]:
-  "(u\<Colon>unit) = v \<longleftrightarrow> True" unfolding unit_eq [of u] unit_eq [of v] by rule+
+  "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
 
 code_type unit
   (SML "unit")
@@ -98,7 +100,7 @@
 code_instance unit :: eq
   (Haskell -)
 
-code_const "op = \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_const Unity
@@ -916,7 +918,7 @@
 instance * :: (eq, eq) eq ..
 
 lemma [code func]:
-  "(x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) = (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by auto
+  "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
 
 lemma split_case_cert:
   assumes "CASE \<equiv> split f"
@@ -935,7 +937,7 @@
 code_instance * :: eq
   (Haskell -)
 
-code_const "op = \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_const Pair
diff -r 4562584d9d66 -r b8390cd56b8f src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Thu Sep 25 09:28:03 2008 +0200
@@ -20,9 +20,8 @@
 
   (*constant aliasses*)
   val add_const_alias: thm -> theory -> theory
-  val subst_alias: theory -> string -> string
+  val triv_classes: theory -> class list
   val resubst_alias: theory -> string -> string
-  val triv_classes: theory -> class list
 
   (*constants*)
   val string_of_typ: theory -> typ -> string
@@ -39,7 +38,7 @@
   (*defining equations*)
   val assert_rew: thm -> thm
   val mk_rew: thm -> thm
-  val mk_func: thm -> thm
+  val mk_func: bool -> thm -> thm
   val head_func: thm -> string * ((string * sort) list * typ)
   val expand_eta: int -> thm -> thm
   val rewrite_func: simpset -> thm -> thm
@@ -223,6 +222,7 @@
     |> map Drule.zero_var_indexes
   end;
 
+
 (* const aliasses *)
 
 structure ConstAlias = TheoryDataFun
@@ -252,16 +252,6 @@
       ((c_c', thm) :: alias, fold (insert (op =)) some_class classes))
   end;
 
-fun rew_alias thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-  in rewrite_head ((map snd o fst o ConstAlias.get) thy) thm end;
-
-fun subst_alias thy c = ConstAlias.get thy
-  |> fst
-  |> get_first (fn ((c', c''), _) => if c = c' then SOME c'' else NONE)
-  |> the_default c;
-
 fun resubst_alias thy =
   let
     val alias = fst (ConstAlias.get thy);
@@ -275,19 +265,18 @@
 
 val triv_classes = snd o ConstAlias.get;
 
+
 (* reading constants as terms *)
 
 fun check_bare_const thy t = case try dest_Const t
  of SOME c_ty => c_ty
   | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
 
-fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
-  o check_bare_const thy;
+fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
 
 fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
 
-fun read_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
-  o read_bare_const thy;
+fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
 
 
 (* constructor sets *)
@@ -372,7 +361,7 @@
 
 (* defining equations *)
 
-fun assert_func thm =
+fun assert_func linear thm =
   let
     val thy = Thm.theory_of_thm thm;
     val (head, args) = (strip_comb o fst o Logic.dest_equals
@@ -380,7 +369,7 @@
     val _ = case head of Const _ => () | _ =>
       bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
     val _ =
-      if has_duplicates (op =)
+      if linear andalso has_duplicates (op =)
         ((fold o fold_aterms) (fn Var (v, _) => cons v
           | _ => I
         ) args [])
@@ -403,7 +392,7 @@
     val _ = map (check 0) args;
   in thm end;
 
-val mk_func = rew_alias o assert_func o mk_rew;
+fun mk_func linear = assert_func linear o mk_rew;
 
 fun head_func thm =
   let
@@ -454,6 +443,6 @@
 
 fun case_cert thm = case_certificate thm
   handle Bind => error "bad case certificate"
-      | TERM _ => error "bad case certificate";
+       | TERM _ => error "bad case certificate";
 
 end;
diff -r 4562584d9d66 -r b8390cd56b8f src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/Tools/code/code_name.ML	Thu Sep 25 09:28:03 2008 +0200
@@ -45,9 +45,8 @@
         val thy' = case some_thyname
          of SOME thyname => ThyInfo.the_theory thyname thy
           | NONE => thy;
-        val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
+        val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
           ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
-        val cs = map (Code_Unit.subst_alias thy') raw_cs;
         fun belongs_here c =
           not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
       in case some_thyname