# HG changeset patch
# User haftmann
# Date 1207144711 -7200
# Node ID 682dfb674df35c68fd791f227afd89fdeaa57729
# Parent  dba7125d0fef1792ea640d5768f6e718e96551c7
proofs adjusted to new situation in Int.thy/Presburger.thy

diff -r dba7125d0fef -r 682dfb674df3 src/HOL/Tools/ComputeNumeral.thy
--- 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