src/HOL/Presburger.thy
 changeset 21046 fe1db2f991a7 parent 20595 db6bedfba498 child 21454 a1937c51ed88
1.1 --- a/src/HOL/Presburger.thy	Mon Oct 16 14:07:21 2006 +0200
1.2 +++ b/src/HOL/Presburger.thy	Mon Oct 16 14:07:31 2006 +0200
1.3 @@ -10,8 +10,9 @@
1.5  theory Presburger
1.6  imports NatSimprocs
1.7 -uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML")
1.8 -	("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
1.9 +uses
1.10 +  ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML")
1.11 +  ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
1.12  begin
1.14  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
1.15 @@ -1094,7 +1095,7 @@
1.16  *}
1.18  lemma eq_number_of [code func]:
1.19 -  "OperationalEquality.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> OperationalEquality.eq k l"
1.20 +  "Code_Generator.eq ((number_of k)\<Colon>int) (number_of l) \<longleftrightarrow> Code_Generator.eq k l"
1.21    unfolding number_of_is_id ..
1.23  lemma less_eq_number_of [code func]:
1.24 @@ -1102,56 +1103,56 @@
1.25    unfolding number_of_is_id ..
1.27  lemma eq_Pls_Pls:
1.28 -  "OperationalEquality.eq Numeral.Pls Numeral.Pls"
1.29 +  "Code_Generator.eq Numeral.Pls Numeral.Pls"
1.30    unfolding eq_def ..
1.32  lemma eq_Pls_Min:
1.33 -  "\<not> OperationalEquality.eq Numeral.Pls Numeral.Min"
1.34 +  "\<not> Code_Generator.eq Numeral.Pls Numeral.Min"
1.35    unfolding eq_def Pls_def Min_def by auto
1.37  lemma eq_Pls_Bit0:
1.38 -  "OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
1.39 +  "Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B0) \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
1.40    unfolding eq_def Pls_def Bit_def bit.cases by auto
1.42  lemma eq_Pls_Bit1:
1.43 -  "\<not> OperationalEquality.eq Numeral.Pls (Numeral.Bit k bit.B1)"
1.44 +  "\<not> Code_Generator.eq Numeral.Pls (Numeral.Bit k bit.B1)"
1.45    unfolding eq_def Pls_def Bit_def bit.cases by arith
1.47  lemma eq_Min_Pls:
1.48 -  "\<not> OperationalEquality.eq Numeral.Min Numeral.Pls"
1.49 +  "\<not> Code_Generator.eq Numeral.Min Numeral.Pls"
1.50    unfolding eq_def Pls_def Min_def by auto
1.52  lemma eq_Min_Min:
1.53 -  "OperationalEquality.eq Numeral.Min Numeral.Min"
1.54 +  "Code_Generator.eq Numeral.Min Numeral.Min"
1.55    unfolding eq_def ..
1.57  lemma eq_Min_Bit0:
1.58 -  "\<not> OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B0)"
1.59 +  "\<not> Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B0)"
1.60    unfolding eq_def Min_def Bit_def bit.cases by arith
1.62  lemma eq_Min_Bit1:
1.63 -  "OperationalEquality.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
1.64 +  "Code_Generator.eq Numeral.Min (Numeral.Bit k bit.B1) \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
1.65    unfolding eq_def Min_def Bit_def bit.cases by auto
1.67  lemma eq_Bit0_Pls:
1.68 -  "OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> OperationalEquality.eq Numeral.Pls k"
1.69 +  "Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Pls \<longleftrightarrow> Code_Generator.eq Numeral.Pls k"
1.70    unfolding eq_def Pls_def Bit_def bit.cases by auto
1.72  lemma eq_Bit1_Pls:
1.73 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.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.77  lemma eq_Bit0_Min:
1.78 -  "\<not> OperationalEquality.eq (Numeral.Bit k bit.B0) Numeral.Min"
1.79 +  "\<not> Code_Generator.eq (Numeral.Bit k bit.B0) Numeral.Min"
1.80    unfolding eq_def Min_def Bit_def bit.cases by arith
1.82  lemma eq_Bit1_Min:
1.83 -  "OperationalEquality.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> OperationalEquality.eq Numeral.Min k"
1.84 +  "Code_Generator.eq (Numeral.Bit k bit.B1) Numeral.Min \<longleftrightarrow> Code_Generator.eq Numeral.Min k"
1.85    unfolding eq_def Min_def Bit_def bit.cases by auto
1.87  lemma eq_Bit_Bit:
1.88 -  "OperationalEquality.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
1.89 -    OperationalEquality.eq v1 v2 \<and> OperationalEquality.eq k1 k2"
1.90 +  "Code_Generator.eq (Numeral.Bit k1 v1) (Numeral.Bit k2 v2) \<longleftrightarrow>
1.91 +    Code_Generator.eq v1 v2 \<and> Code_Generator.eq k1 k2"
1.92    unfolding eq_def Bit_def
1.93    apply (cases v1)
1.94    apply (cases v2)