src/HOL/Integ/Presburger.thy

 *}
 
 lemma eq_number_of [code func]:
   "((number_of k)\<Colon>int) = number_of l \<longleftrightarrow> k = l"
   unfolding number_of_is_id ..
+
 lemma eq_Pls_Pls:
-  "Numeral.Pls = Numeral.Pls" ..
+  "Numeral.Pls = Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma eq_Pls_Min:
-  "Numeral.Pls \<noteq> Numeral.Min"
+  "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Pls_Bit0:
   "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Pls_Bit1:
-  "Numeral.Pls \<noteq> Numeral.Bit k bit.B1"
+  "Numeral.Pls = Numeral.Bit k bit.B1 \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Min_Pls:
-  "Numeral.Min \<noteq> Numeral.Pls"
+  "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma eq_Min_Min:
-  "Numeral.Min = Numeral.Min" ..
+  "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma eq_Min_Bit0:
-  "Numeral.Min \<noteq> Numeral.Bit k bit.B0"
+  "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Min_Bit1:
   "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
   unfolding Min_def Bit_def bit.cases by auto

 lemma eq_Bit0_Pls:
   "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
   unfolding Pls_def Bit_def bit.cases by auto
 
 lemma eq_Bit1_Pls:
-  "Numeral.Bit k bit.B1 \<noteq>  Numeral.Pls"
+  "Numeral.Bit k bit.B1 = Numeral.Pls \<longleftrightarrow> False"
   unfolding Pls_def Bit_def bit.cases by arith
 
 lemma eq_Bit0_Min:
-  "Numeral.Bit k bit.B0 \<noteq> Numeral.Min"
+  "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
   unfolding Min_def Bit_def bit.cases by arith
 
 lemma eq_Bit1_Min:
   "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
   unfolding Min_def Bit_def bit.cases by auto

 lemma less_eq_number_of [code func]:
   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   unfolding number_of_is_id ..
 
 lemma less_eq_Pls_Pls:
-  "Numeral.Pls \<le> Numeral.Pls" ..
+  "Numeral.Pls \<le> Numeral.Pls \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Pls_Min:
-  "\<not> (Numeral.Pls \<le> Numeral.Min)"
+  "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Pls_Bit:
   "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
   unfolding Pls_def Bit_def by (cases v) auto
 
 lemma less_eq_Min_Pls:
-  "Numeral.Min \<le> Numeral.Pls"
+  "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_eq_Min_Min:
-  "Numeral.Min \<le> Numeral.Min" ..
+  "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
 
 lemma less_eq_Min_Bit0:
   "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
   unfolding Min_def Bit_def by auto
 

 lemma less_eq_number_of [code func]:
   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   unfolding number_of_is_id ..
 
 lemma less_Pls_Pls:
-  "\<not> (Numeral.Pls < Numeral.Pls)" by auto
+  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by auto
 
 lemma less_Pls_Min:
-  "\<not> (Numeral.Pls < Numeral.Min)"
+  "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def by auto
 
 lemma less_Pls_Bit0:
   "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
   unfolding Pls_def Bit_def by auto

 lemma less_Pls_Bit1:
   "Numeral.Pls < Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Pls \<le> k"
   unfolding Pls_def Bit_def by auto
 
 lemma less_Min_Pls:
-  "Numeral.Min < Numeral.Pls"
+  "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by auto
 
 lemma less_Min_Min:
-  "\<not> (Numeral.Min < Numeral.Min)" by auto
+  "Numeral.Min < Numeral.Min \<longleftrightarrow> False" by auto
 
 lemma less_Min_Bit:
   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   unfolding Min_def Bit_def by (auto split: bit.split)