--- 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 ..
--- 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 *}
--- 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"
--- 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':
--- 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"
--- 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]"