--- a/src/HOL/Tools/ComputeNumeral.thy Wed Apr 02 15:58:30 2008 +0200
+++ b/src/HOL/Tools/ComputeNumeral.thy Wed Apr 02 15:58:31 2008 +0200
@@ -1,5 +1,5 @@
theory ComputeNumeral
-imports ComputeHOL Float
+imports ComputeHOL "~~/src/HOL/Real/Float"
begin
(* normalization of bit strings *)
@@ -29,61 +29,61 @@
lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
(* equality for bit strings *)
-lemma biteq1: "(Int.Pls = Int.Pls) = True" by (rule eq_Pls_Pls)
-lemma biteq2: "(Int.Min = Int.Min) = True" by (rule eq_Min_Min)
-lemma biteq3: "(Int.Pls = Int.Min) = False" by (rule eq_Pls_Min)
-lemma biteq4: "(Int.Min = Int.Pls) = False" by (rule eq_Min_Pls)
-lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" by (rule eq_Bit0_Bit0)
-lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" by (rule eq_Bit1_Bit1)
-lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" by (rule eq_Bit0_Bit1)
-lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" by (rule eq_Bit1_Bit0)
-lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" by (rule eq_Pls_Bit0)
-lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" by (rule eq_Pls_Bit1)
-lemma biteq11: "(Int.Min = Int.Bit0 x) = False" by (rule eq_Min_Bit0)
-lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" by (rule eq_Min_Bit1)
-lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" by (subst eq_Bit0_Pls) auto
-lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" by (rule eq_Bit1_Pls)
-lemma biteq15: "(Int.Bit0 x = Int.Min) = False" by (rule eq_Bit0_Min)
-lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" by (subst eq_Bit1_Min) auto
+lemma biteq1: "(Int.Pls = Int.Pls) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq2: "(Int.Min = Int.Min) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq11: "(Int.Min = Int.Bit0 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq15: "(Int.Bit0 x = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
(* x < y for bit strings *)
-lemma bitless1: "(Int.Pls < Int.Min) = False" by (rule less_Pls_Min)
-lemma bitless2: "(Int.Pls < Int.Pls) = False" by (rule less_Pls_Pls)
-lemma bitless3: "(Int.Min < Int.Pls) = True" by (rule less_Min_Pls)
-lemma bitless4: "(Int.Min < Int.Min) = False" by (rule less_Min_Min)
-lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (rule less_Bit0_Bit0)
-lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (rule less_Bit1_Bit1)
-lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (rule less_Bit0_Bit1)
-lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (rule less_Bit1_Bit0)
-lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (rule less_Pls_Bit0)
-lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_Pls_Bit1)
-lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
-lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (rule less_Min_Bit1)
-lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit0_Pls)
-lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (rule less_Bit1_Pls)
-lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
-lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (rule less_Bit1_Min)
+lemma bitless1: "(Int.Pls < Int.Min) = False" by (simp add: less_int_code)
+lemma bitless2: "(Int.Pls < Int.Pls) = False" by (simp add: less_int_code)
+lemma bitless3: "(Int.Min < Int.Pls) = True" by (simp add: less_int_code)
+lemma bitless4: "(Int.Min < Int.Min) = False" by (simp add: less_int_code)
+lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code)
+lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (simp add: less_int_code)
+lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (simp add: less_int_code)
+lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code)
+lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (simp add: less_int_code)
+lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (simp add: less_int_code)
+lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (simp add: less_int_code)
+lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code)
+lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code)
+lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (simp add: less_int_code)
lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8
bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
(* x \<le> y for bit strings *)
-lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (rule less_eq_Pls_Min)
-lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (rule less_eq_Pls_Pls)
-lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (rule less_eq_Min_Pls)
-lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (rule less_eq_Min_Min)
-lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit0)
-lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit1_Bit1)
-lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (rule less_eq_Bit0_Bit1)
-lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (rule less_eq_Bit1_Bit0)
-lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit0)
-lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (rule less_eq_Pls_Bit1)
-lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Bit0_def Pls_def Min_def by auto
-lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (rule less_eq_Min_Bit1)
-lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (rule less_eq_Bit0_Pls)
-lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (rule less_eq_Bit1_Pls)
-lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Bit0_def Pls_def Min_def by auto
-lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (rule less_eq_Bit1_Min)
+lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (simp add: less_eq_int_code)
+lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
+lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
+lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (simp add: less_eq_int_code)
+lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (simp add: less_eq_int_code)
+lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
+lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
+lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (simp add: less_eq_int_code)
+lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
+lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
+lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (simp add: less_eq_int_code)
+lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (simp add: less_eq_int_code)
+lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (simp add: less_eq_int_code)
+lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
+lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (simp add: less_eq_int_code)
lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8
bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16