src/HOL/Presburger.thy
changeset 21454 a1937c51ed88
parent 21046 fe1db2f991a7
child 22026 cc60e54aa7cb
     1.1 --- a/src/HOL/Presburger.thy	Wed Nov 22 10:20:11 2006 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Wed Nov 22 10:20:12 2006 +0100
     1.3 @@ -1090,12 +1090,12 @@
     1.4  text {* Code generator setup *}
     1.5  
     1.6  text {*
     1.7 -  Presburger arithmetic is neccesary to prove some
     1.8 +  Presburger arithmetic is necessary (at least convenient) to prove some
     1.9    of the following code lemmas on integer numerals.
    1.10  *}
    1.11  
    1.12  lemma eq_number_of [code func]:
    1.13 -  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
    1.14 +  "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
    1.15    unfolding number_of_is_id ..
    1.16  
    1.17  lemma less_eq_number_of [code func]:
    1.18 @@ -1103,57 +1103,55 @@
    1.19    unfolding number_of_is_id ..
    1.20  
    1.21  lemma eq_Pls_Pls:
    1.22 -  "Code_Generator.eq Numeral.Pls Numeral.Pls"
    1.23 -  unfolding eq_def ..
    1.24 +  "Numeral.Pls = Numeral.Pls" ..
    1.25  
    1.26  lemma eq_Pls_Min:
    1.27 -  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
    1.28 -  unfolding eq_def Pls_def Min_def by auto
    1.29 +  "Numeral.Pls \<noteq> Numeral.Min"
    1.30 +  unfolding Pls_def Min_def by auto
    1.31  
    1.32  lemma eq_Pls_Bit0:
    1.33 -  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    1.34 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    1.35 +  "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
    1.36 +  unfolding Pls_def Bit_def bit.cases by auto
    1.37  
    1.38  lemma eq_Pls_Bit1:
    1.39 -  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
    1.40 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    1.41 +  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
    1.42 +  unfolding Pls_def Bit_def bit.cases by arith
    1.43  
    1.44  lemma eq_Min_Pls:
    1.45 -  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
    1.46 -  unfolding eq_def Pls_def Min_def by auto
    1.47 +  "Numeral.Min \<noteq> Numeral.Pls"
    1.48 +  unfolding Pls_def Min_def by auto
    1.49  
    1.50  lemma eq_Min_Min:
    1.51 -  "Code_Generator.eq Numeral.Min Numeral.Min"
    1.52 -  unfolding eq_def ..
    1.53 +  "Numeral.Min = Numeral.Min" ..
    1.54  
    1.55  lemma eq_Min_Bit0:
    1.56 -  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
    1.57 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    1.58 +  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
    1.59 +  unfolding Min_def Bit_def bit.cases by arith
    1.60  
    1.61  lemma eq_Min_Bit1:
    1.62 -  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    1.63 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    1.64 +  "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
    1.65 +  unfolding Min_def Bit_def bit.cases by auto
    1.66  
    1.67  lemma eq_Bit0_Pls:
    1.68 -  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
    1.69 -  unfolding eq_def Pls_def Bit_def bit.cases by auto
    1.70 +  "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
    1.71 +  unfolding Pls_def Bit_def bit.cases by auto
    1.72  
    1.73  lemma eq_Bit1_Pls:
    1.74 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Pls"
    1.75 -  unfolding eq_def Pls_def Bit_def bit.cases by arith
    1.76 +  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
    1.77 +  unfolding Pls_def Bit_def bit.cases by arith
    1.78  
    1.79  lemma eq_Bit0_Min:
    1.80 -  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
    1.81 -  unfolding eq_def Min_def Bit_def bit.cases by arith
    1.82 +  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
    1.83 +  unfolding Min_def Bit_def bit.cases by arith
    1.84  
    1.85  lemma eq_Bit1_Min:
    1.86 -  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
    1.87 -  unfolding eq_def Min_def Bit_def bit.cases by auto
    1.88 +  "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
    1.89 +  unfolding Min_def Bit_def bit.cases by auto
    1.90  
    1.91  lemma eq_Bit_Bit:
    1.92 -  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
    1.93 -    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
    1.94 -  unfolding eq_def Bit_def
    1.95 +  "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
    1.96 +    v1 = v2 \<and> k1 = k2"
    1.97 +  unfolding Bit_def
    1.98    apply (cases v1)
    1.99    apply (cases v2)
   1.100    apply auto