src/HOL/Presburger.thy
 changeset 23460 f9ae34d5f8da parent 23438 dd824e86fa8a
```     1.1 --- a/src/HOL/Presburger.thy	Thu Jun 21 15:42:13 2007 +0200
1.2 +++ b/src/HOL/Presburger.thy	Thu Jun 21 15:42:14 2007 +0200
1.3 @@ -7,12 +7,15 @@
1.4
1.5  theory Presburger
1.6  imports NatSimprocs SetInterval
1.7 -  uses "Tools/Presburger/cooper_data" "Tools/Presburger/qelim"
1.8 -       "Tools/Presburger/generated_cooper.ML"
1.9 -       ("Tools/Presburger/cooper.ML") ("Tools/Presburger/presburger.ML")
1.10 -
1.11 +uses
1.12 +  "Tools/Presburger/cooper_data.ML"
1.13 +  "Tools/Presburger/generated_cooper.ML"
1.14 +  ("Tools/Presburger/cooper.ML")
1.15 +  ("Tools/Presburger/presburger.ML")
1.16  begin
1.17 -setup {* Cooper_Data.setup*}
1.18 +
1.19 +setup CooperData.setup
1.20 +
1.21
1.22  subsection{* The @{text "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
1.23
1.24 @@ -462,7 +465,7 @@
1.25    #> (fn (((elim, add_ths), del_ths),ctxt) =>
1.26           Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
1.27  end
1.28 -*} ""
1.29 +*} "Cooper's algorithm for Presburger arithmetic"
1.30
1.31  lemma [presburger]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.32  lemma [presburger]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.33 @@ -470,7 +473,9 @@
1.34  lemma [presburger]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.35  lemma [presburger]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
1.36
1.37 +
1.38  subsection {* Code generator setup *}
1.39 +
1.40  text {*
1.41    Presburger arithmetic is convenient to prove some
1.42    of the following code lemmas on integer numerals:
1.43 @@ -481,7 +486,7 @@
1.44
1.45  lemma eq_Pls_Min:
1.46    "Numeral.Pls = Numeral.Min \<longleftrightarrow> False"
1.47 -  unfolding Pls_def Min_def by presburger
1.48 +  unfolding Pls_def Numeral.Min_def by presburger
1.49
1.50  lemma eq_Pls_Bit0:
1.51    "Numeral.Pls = Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls = k"
1.52 @@ -493,18 +498,18 @@
1.53
1.54  lemma eq_Min_Pls:
1.55    "Numeral.Min = Numeral.Pls \<longleftrightarrow> False"
1.56 -  unfolding Pls_def Min_def by presburger
1.57 +  unfolding Pls_def Numeral.Min_def by presburger
1.58
1.59  lemma eq_Min_Min:
1.60    "Numeral.Min = Numeral.Min \<longleftrightarrow> True" by presburger
1.61
1.62  lemma eq_Min_Bit0:
1.63    "Numeral.Min = Numeral.Bit k bit.B0 \<longleftrightarrow> False"
1.64 -  unfolding Min_def Bit_def bit.cases by presburger
1.65 +  unfolding Numeral.Min_def Bit_def bit.cases by presburger
1.66
1.67  lemma eq_Min_Bit1:
1.68    "Numeral.Min = Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min = k"
1.69 -  unfolding Min_def Bit_def bit.cases by presburger
1.70 +  unfolding Numeral.Min_def Bit_def bit.cases by presburger
1.71
1.72  lemma eq_Bit0_Pls:
1.73    "Numeral.Bit k bit.B0 = Numeral.Pls \<longleftrightarrow> Numeral.Pls = k"
1.74 @@ -516,11 +521,11 @@
1.75
1.76  lemma eq_Bit0_Min:
1.77    "Numeral.Bit k bit.B0 = Numeral.Min \<longleftrightarrow> False"
1.78 -  unfolding Min_def Bit_def bit.cases  by presburger
1.79 +  unfolding Numeral.Min_def Bit_def bit.cases  by presburger
1.80
1.81  lemma eq_Bit1_Min:
1.82    "(Numeral.Bit k bit.B1) = Numeral.Min \<longleftrightarrow> Numeral.Min = k"
1.83 -  unfolding Min_def Bit_def bit.cases  by presburger
1.84 +  unfolding Numeral.Min_def Bit_def bit.cases  by presburger
1.85
1.86  lemma eq_Bit_Bit:
1.87    "Numeral.Bit k1 v1 = Numeral.Bit k2 v2 \<longleftrightarrow>
1.88 @@ -535,7 +540,7 @@
1.89    apply presburger
1.90    apply (cases v2)
1.91    apply auto
1.92 -done
1.93 +  done
1.94
1.95  lemma eq_number_of:
1.96    "(number_of k \<Colon> int) = number_of l \<longleftrightarrow> k = l"
1.97 @@ -547,7 +552,7 @@
1.98
1.99  lemma less_eq_Pls_Min:
1.100    "Numeral.Pls \<le> Numeral.Min \<longleftrightarrow> False"
1.101 -  unfolding Pls_def Min_def by presburger
1.102 +  unfolding Pls_def Numeral.Min_def by presburger
1.103
1.104  lemma less_eq_Pls_Bit:
1.105    "Numeral.Pls \<le> Numeral.Bit k v \<longleftrightarrow> Numeral.Pls \<le> k"
1.106 @@ -555,18 +560,18 @@
1.107
1.108  lemma less_eq_Min_Pls:
1.109    "Numeral.Min \<le> Numeral.Pls \<longleftrightarrow> True"
1.110 -  unfolding Pls_def Min_def by presburger
1.111 +  unfolding Pls_def Numeral.Min_def by presburger
1.112
1.113  lemma less_eq_Min_Min:
1.114    "Numeral.Min \<le> Numeral.Min \<longleftrightarrow> True" by rule+
1.115
1.116  lemma less_eq_Min_Bit0:
1.117    "Numeral.Min \<le> Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Min < k"
1.118 -  unfolding Min_def Bit_def by auto
1.119 +  unfolding Numeral.Min_def Bit_def by auto
1.120
1.121  lemma less_eq_Min_Bit1:
1.122    "Numeral.Min \<le> Numeral.Bit k bit.B1 \<longleftrightarrow> Numeral.Min \<le> k"
1.123 -  unfolding Min_def Bit_def by auto
1.124 +  unfolding Numeral.Min_def Bit_def by auto
1.125
1.126  lemma less_eq_Bit0_Pls:
1.127    "Numeral.Bit k bit.B0 \<le> Numeral.Pls \<longleftrightarrow> k \<le> Numeral.Pls"
1.128 @@ -578,7 +583,7 @@
1.129
1.130  lemma less_eq_Bit_Min:
1.131    "Numeral.Bit k v \<le> Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1.132 -  unfolding Min_def Bit_def by (cases v) auto
1.133 +  unfolding Numeral.Min_def Bit_def by (cases v) auto
1.134
1.135  lemma less_eq_Bit0_Bit:
1.136    "Numeral.Bit k1 bit.B0 \<le> Numeral.Bit k2 v \<longleftrightarrow> k1 \<le> k2"
1.137 @@ -602,7 +607,7 @@
1.138
1.139  lemma less_Pls_Min:
1.140    "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
1.141 -  unfolding Pls_def Min_def  by presburger
1.142 +  unfolding Pls_def Numeral.Min_def  by presburger
1.143
1.144  lemma less_Pls_Bit0:
1.145    "Numeral.Pls < Numeral.Bit k bit.B0 \<longleftrightarrow> Numeral.Pls < k"
1.146 @@ -614,14 +619,14 @@
1.147
1.148  lemma less_Min_Pls:
1.149    "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
1.150 -  unfolding Pls_def Min_def by presburger
1.151 +  unfolding Pls_def Numeral.Min_def by presburger
1.152
1.153  lemma less_Min_Min:
1.154    "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
1.155
1.156  lemma less_Min_Bit:
1.157    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
1.158 -  unfolding Min_def Bit_def by (auto split: bit.split)
1.159 +  unfolding Numeral.Min_def Bit_def by (auto split: bit.split)
1.160
1.161  lemma less_Bit_Pls:
1.162    "Numeral.Bit k v < Numeral.Pls \<longleftrightarrow> k < Numeral.Pls"
1.163 @@ -629,11 +634,11 @@
1.164
1.165  lemma less_Bit0_Min:
1.166    "Numeral.Bit k bit.B0 < Numeral.Min \<longleftrightarrow> k \<le> Numeral.Min"
1.167 -  unfolding Min_def Bit_def by auto
1.168 +  unfolding Numeral.Min_def Bit_def by auto
1.169
1.170  lemma less_Bit1_Min:
1.171    "Numeral.Bit k bit.B1 < Numeral.Min \<longleftrightarrow> k < Numeral.Min"
1.172 -  unfolding Min_def Bit_def by auto
1.173 +  unfolding Numeral.Min_def Bit_def by auto
1.174
1.175  lemma less_Bit_Bit0:
1.176    "Numeral.Bit k1 v < Numeral.Bit k2 bit.B0 \<longleftrightarrow> k1 < k2"
```