# HG changeset patch
# User haftmann
# Date 1222330642 -7200
# Node ID abfc66969d1f0f6738f859ecb3c3a797c4ee2e66
# Parent  715163ec93c0340a619d9995f139203a8fbb354d
non left-linear equations for nbe

diff -r 715163ec93c0 -r abfc66969d1f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Int.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -1855,6 +1855,10 @@
     simp_all only: Min_def succ_def pred_def number_of_is_id)
     (auto simp add: iszero_def)
 
+lemma eq_int_refl [code nbe]:
+  "eq_class.eq (k::int) k \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
 lemma less_eq_number_of_int_code [code func]:
   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   unfolding number_of_is_id ..
diff -r 715163ec93c0 -r abfc66969d1f src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -114,6 +114,10 @@
   "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)
 
+lemma [code nbe]:
+  "eq_class.eq (k::index) k \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
 
 subsection {* Indices as datatype of ints *}
 
diff -r 715163ec93c0 -r abfc66969d1f src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -70,8 +70,12 @@
   unfolding divmod_aux_def divmod_div_mod zdiv_int [symmetric] zmod_int [symmetric] by simp
 
 lemma eq_nat_code [code]:
-  "n = m \<longleftrightarrow> (of_nat n \<Colon> int) = of_nat m"
-  by simp
+  "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
+  by (simp add: eq)
+
+lemma eq_nat_refl [code nbe]:
+  "eq_class.eq (n::nat) n \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
 
 lemma less_eq_nat_code [code]:
   "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
diff -r 715163ec93c0 -r abfc66969d1f src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -875,6 +875,10 @@
      else a * d =  b * c)"
   by (auto simp add: eq eq_rat)
 
+lemma rat_eq_refl [code nbe]:
+  "eq_class.eq (r::rat) r \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
 end
 
 lemma le_rat':
diff -r 715163ec93c0 -r abfc66969d1f src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -1088,6 +1088,10 @@
 lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \<longleftrightarrow> eq_class.eq x y"
   by (simp add: eq_real_def eq)
 
+lemma real_eq_refl [code nbe]:
+  "eq_class.eq (x::real) x \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
 end
 
 lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> x \<le> y"
diff -r 715163ec93c0 -r abfc66969d1f src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Thu Sep 25 09:28:08 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy	Thu Sep 25 10:17:22 2008 +0200
@@ -8,15 +8,6 @@
 imports Main "~~/src/HOL/Real/Rational"
 begin
 
-lemma [code nbe]:
-  "x = x \<longleftrightarrow> True" by rule+
-
-lemma [code nbe]:
-  "eq_class.eq (x::bool) x \<longleftrightarrow> True" unfolding eq by rule+
-
-lemma [code nbe]:
-  "eq_class.eq (x::nat) x \<longleftrightarrow> True" unfolding eq by rule+
-
 lemma "True" by normalization
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
@@ -29,9 +20,6 @@
 
 datatype n = Z | S n
 
-lemma [code nbe]:
-  "eq_class.eq (x::n) x \<longleftrightarrow> True" unfolding eq by rule+
-
 consts
   add :: "n \<Rightarrow> n \<Rightarrow> n"
   add2 :: "n \<Rightarrow> n \<Rightarrow> n"
@@ -83,9 +71,6 @@
 lemma "[] @ xs = xs" by normalization
 lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
 
-lemma [code nbe]:
-  "eq_class.eq (x :: 'a\<Colon>eq list) x \<longleftrightarrow> True" unfolding eq by rule+
-
 lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+
 lemma "rev [a, b, c] = [c, b, a]" by normalization
 normal_form "rev (a#b#cs) = rev cs @ [b, a]"