adapted tool setup;
authorwenzelm
Thu Jun 21 15:42:14 2007 +0200 (2007-06-21)
changeset 23460f9ae34d5f8da
parent 23459 74e0cc2018d9
child 23461 9a586e80ce15
adapted tool setup;
src/HOL/Presburger.thy
     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"