src/HOL/Presburger.thy
changeset 22744 5cbe966d67a2
parent 22394 54ea68b5a92f
child 22801 caffcb450ef4
     1.1 --- a/src/HOL/Presburger.thy	Fri Apr 20 11:21:41 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Fri Apr 20 11:21:42 2007 +0200
     1.3 @@ -1069,11 +1069,12 @@
     1.4  lemma eq_number_of [code func]:
     1.5    "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
     1.6    unfolding number_of_is_id ..
     1.7 +
     1.8  lemma eq_Pls_Pls:
     1.9 -  "Numeral.Pls = Numeral.Pls" ..
    1.10 +  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
    1.11  
    1.12  lemma eq_Pls_Min:
    1.13 -  "Numeral.Pls \<noteq> Numeral.Min"
    1.14 +  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
    1.15    unfolding Pls_def Min_def by auto
    1.16  
    1.17  lemma eq_Pls_Bit0:
    1.18 @@ -1081,18 +1082,18 @@
    1.19    unfolding Pls_def Bit_def bit.cases by auto
    1.20  
    1.21  lemma eq_Pls_Bit1:
    1.22 -  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
    1.23 +  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
    1.24    unfolding Pls_def Bit_def bit.cases by arith
    1.25  
    1.26  lemma eq_Min_Pls:
    1.27 -  "Numeral.Min \<noteq> Numeral.Pls"
    1.28 +  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
    1.29    unfolding Pls_def Min_def by auto
    1.30  
    1.31  lemma eq_Min_Min:
    1.32 -  "Numeral.Min = Numeral.Min" ..
    1.33 +  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
    1.34  
    1.35  lemma eq_Min_Bit0:
    1.36 -  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
    1.37 +  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
    1.38    unfolding Min_def Bit_def bit.cases by arith
    1.39  
    1.40  lemma eq_Min_Bit1:
    1.41 @@ -1104,11 +1105,11 @@
    1.42    unfolding Pls_def Bit_def bit.cases by auto
    1.43  
    1.44  lemma eq_Bit1_Pls:
    1.45 -  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
    1.46 +  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
    1.47    unfolding Pls_def Bit_def bit.cases by arith
    1.48  
    1.49  lemma eq_Bit0_Min:
    1.50 -  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
    1.51 +  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
    1.52    unfolding Min_def Bit_def bit.cases by arith
    1.53  
    1.54  lemma eq_Bit1_Min:
    1.55 @@ -1140,10 +1141,10 @@
    1.56    unfolding number_of_is_id ..
    1.57  
    1.58  lemma less_eq_Pls_Pls:
    1.59 -  "Numeral.Pls \<le> Numeral.Pls" ..
    1.60 +  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
    1.61  
    1.62  lemma less_eq_Pls_Min:
    1.63 -  "\<not> (Numeral.Pls \<le> Numeral.Min)"
    1.64 +  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
    1.65    unfolding Pls_def Min_def by auto
    1.66  
    1.67  lemma less_eq_Pls_Bit:
    1.68 @@ -1151,11 +1152,11 @@
    1.69    unfolding Pls_def Bit_def by (cases v) auto
    1.70  
    1.71  lemma less_eq_Min_Pls:
    1.72 -  "Numeral.Min \<le> Numeral.Pls"
    1.73 +  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
    1.74    unfolding Pls_def Min_def by auto
    1.75  
    1.76  lemma less_eq_Min_Min:
    1.77 -  "Numeral.Min \<le> Numeral.Min" ..
    1.78 +  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
    1.79  
    1.80  lemma less_eq_Min_Bit0:
    1.81    "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
    1.82 @@ -1198,10 +1199,10 @@
    1.83    unfolding number_of_is_id ..
    1.84  
    1.85  lemma less_Pls_Pls:
    1.86 -  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
    1.87 +  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
    1.88  
    1.89  lemma less_Pls_Min:
    1.90 -  "\<not> (Numeral.Pls < Numeral.Min)"
    1.91 +  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
    1.92    unfolding Pls_def Min_def by auto
    1.93  
    1.94  lemma less_Pls_Bit0:
    1.95 @@ -1213,11 +1214,11 @@
    1.96    unfolding Pls_def Bit_def by auto
    1.97  
    1.98  lemma less_Min_Pls:
    1.99 -  "Numeral.Min < Numeral.Pls"
   1.100 +  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   1.101    unfolding Pls_def Min_def by auto
   1.102  
   1.103  lemma less_Min_Min:
   1.104 -  "\<not> (Numeral.Min < Numeral.Min)" by auto
   1.105 +  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
   1.106  
   1.107  lemma less_Min_Bit:
   1.108    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"