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.4  
     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.13  
    1.14  text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
    1.15 @@ -1094,7 +1095,7 @@
    1.16  *}
    1.17  
    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.22  
    1.23  lemma less_eq_number_of [code func]:
    1.24 @@ -1102,56 +1103,56 @@
    1.25    unfolding number_of_is_id ..
    1.26  
    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.31  
    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.36  
    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.41  
    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.46  
    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.51  
    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.56  
    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.61  
    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.66  
    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.71  
    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.76  
    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.81  
    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.86  
    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)