src/HOL/Numeral_Simprocs.thy
changeset 60758 d8d85a8172b5
parent 59867 58043346ca64
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Various *)
     1.5  
     1.6 -section {* Combination and Cancellation Simprocs for Numeral Expressions *}
     1.7 +section \<open>Combination and Cancellation Simprocs for Numeral Expressions\<close>
     1.8  
     1.9  theory Numeral_Simprocs
    1.10  imports Divides
    1.11 @@ -23,12 +23,12 @@
    1.12  declare split_div [of _ _ "numeral k", arith_split] for k
    1.13  declare split_mod [of _ _ "numeral k", arith_split] for k
    1.14  
    1.15 -text {* For @{text combine_numerals} *}
    1.16 +text \<open>For @{text combine_numerals}\<close>
    1.17  
    1.18  lemma left_add_mult_distrib: "i*u + (j*u + k) = (i+j)*u + (k::nat)"
    1.19  by (simp add: add_mult_distrib)
    1.20  
    1.21 -text {* For @{text cancel_numerals} *}
    1.22 +text \<open>For @{text cancel_numerals}\<close>
    1.23  
    1.24  lemma nat_diff_add_eq1:
    1.25       "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)"
    1.26 @@ -62,7 +62,7 @@
    1.27       "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)"
    1.28  by (auto split add: nat_diff_split simp add: add_mult_distrib)
    1.29  
    1.30 -text {* For @{text cancel_numeral_factors} *}
    1.31 +text \<open>For @{text cancel_numeral_factors}\<close>
    1.32  
    1.33  lemma nat_mult_le_cancel1: "(0::nat) < k ==> (k*m <= k*n) = (m<=n)"
    1.34  by auto
    1.35 @@ -83,7 +83,7 @@
    1.36  lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
    1.37  by(auto)
    1.38  
    1.39 -text {* For @{text cancel_factor} *}
    1.40 +text \<open>For @{text cancel_factor}\<close>
    1.41  
    1.42  lemmas nat_mult_le_cancel_disj = mult_le_cancel1
    1.43  
    1.44 @@ -107,17 +107,17 @@
    1.45  
    1.46  simproc_setup semiring_assoc_fold
    1.47    ("(a::'a::comm_semiring_1_cancel) * b") =
    1.48 -  {* fn phi => Numeral_Simprocs.assoc_fold *}
    1.49 +  \<open>fn phi => Numeral_Simprocs.assoc_fold\<close>
    1.50  
    1.51  (* TODO: see whether the type class can be generalized further *)
    1.52  simproc_setup int_combine_numerals
    1.53    ("(i::'a::comm_ring_1) + j" | "(i::'a::comm_ring_1) - j") =
    1.54 -  {* fn phi => Numeral_Simprocs.combine_numerals *}
    1.55 +  \<open>fn phi => Numeral_Simprocs.combine_numerals\<close>
    1.56  
    1.57  simproc_setup field_combine_numerals
    1.58    ("(i::'a::{field,ring_char_0}) + j"
    1.59    |"(i::'a::{field,ring_char_0}) - j") =
    1.60 -  {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.61 +  \<open>fn phi => Numeral_Simprocs.field_combine_numerals\<close>
    1.62  
    1.63  simproc_setup inteq_cancel_numerals
    1.64    ("(l::'a::comm_ring_1) + m = n"
    1.65 @@ -128,7 +128,7 @@
    1.66    |"(l::'a::comm_ring_1) = m * n"
    1.67    |"- (l::'a::comm_ring_1) = m"
    1.68    |"(l::'a::comm_ring_1) = - m") =
    1.69 -  {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
    1.70 +  \<open>fn phi => Numeral_Simprocs.eq_cancel_numerals\<close>
    1.71  
    1.72  simproc_setup intless_cancel_numerals
    1.73    ("(l::'a::linordered_idom) + m < n"
    1.74 @@ -139,7 +139,7 @@
    1.75    |"(l::'a::linordered_idom) < m * n"
    1.76    |"- (l::'a::linordered_idom) < m"
    1.77    |"(l::'a::linordered_idom) < - m") =
    1.78 -  {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
    1.79 +  \<open>fn phi => Numeral_Simprocs.less_cancel_numerals\<close>
    1.80  
    1.81  simproc_setup intle_cancel_numerals
    1.82    ("(l::'a::linordered_idom) + m \<le> n"
    1.83 @@ -150,140 +150,140 @@
    1.84    |"(l::'a::linordered_idom) \<le> m * n"
    1.85    |"- (l::'a::linordered_idom) \<le> m"
    1.86    |"(l::'a::linordered_idom) \<le> - m") =
    1.87 -  {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.88 +  \<open>fn phi => Numeral_Simprocs.le_cancel_numerals\<close>
    1.89  
    1.90  simproc_setup ring_eq_cancel_numeral_factor
    1.91    ("(l::'a::{idom,ring_char_0}) * m = n"
    1.92    |"(l::'a::{idom,ring_char_0}) = m * n") =
    1.93 -  {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.94 +  \<open>fn phi => Numeral_Simprocs.eq_cancel_numeral_factor\<close>
    1.95  
    1.96  simproc_setup ring_less_cancel_numeral_factor
    1.97    ("(l::'a::linordered_idom) * m < n"
    1.98    |"(l::'a::linordered_idom) < m * n") =
    1.99 -  {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
   1.100 +  \<open>fn phi => Numeral_Simprocs.less_cancel_numeral_factor\<close>
   1.101  
   1.102  simproc_setup ring_le_cancel_numeral_factor
   1.103    ("(l::'a::linordered_idom) * m <= n"
   1.104    |"(l::'a::linordered_idom) <= m * n") =
   1.105 -  {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
   1.106 +  \<open>fn phi => Numeral_Simprocs.le_cancel_numeral_factor\<close>
   1.107  
   1.108  (* TODO: remove comm_ring_1 constraint if possible *)
   1.109  simproc_setup int_div_cancel_numeral_factors
   1.110    ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
   1.111    |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
   1.112 -  {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
   1.113 +  \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
   1.114  
   1.115  simproc_setup divide_cancel_numeral_factor
   1.116    ("((l::'a::{field,ring_char_0}) * m) / n"
   1.117    |"(l::'a::{field,ring_char_0}) / (m * n)"
   1.118    |"((numeral v)::'a::{field,ring_char_0}) / (numeral w)") =
   1.119 -  {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
   1.120 +  \<open>fn phi => Numeral_Simprocs.divide_cancel_numeral_factor\<close>
   1.121  
   1.122  simproc_setup ring_eq_cancel_factor
   1.123    ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
   1.124 -  {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
   1.125 +  \<open>fn phi => Numeral_Simprocs.eq_cancel_factor\<close>
   1.126  
   1.127  simproc_setup linordered_ring_le_cancel_factor
   1.128    ("(l::'a::linordered_idom) * m <= n"
   1.129    |"(l::'a::linordered_idom) <= m * n") =
   1.130 -  {* fn phi => Numeral_Simprocs.le_cancel_factor *}
   1.131 +  \<open>fn phi => Numeral_Simprocs.le_cancel_factor\<close>
   1.132  
   1.133  simproc_setup linordered_ring_less_cancel_factor
   1.134    ("(l::'a::linordered_idom) * m < n"
   1.135    |"(l::'a::linordered_idom) < m * n") =
   1.136 -  {* fn phi => Numeral_Simprocs.less_cancel_factor *}
   1.137 +  \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
   1.138  
   1.139  simproc_setup int_div_cancel_factor
   1.140    ("((l::'a::semiring_div) * m) div n"
   1.141    |"(l::'a::semiring_div) div (m * n)") =
   1.142 -  {* fn phi => Numeral_Simprocs.div_cancel_factor *}
   1.143 +  \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
   1.144  
   1.145  simproc_setup int_mod_cancel_factor
   1.146    ("((l::'a::semiring_div) * m) mod n"
   1.147    |"(l::'a::semiring_div) mod (m * n)") =
   1.148 -  {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
   1.149 +  \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
   1.150  
   1.151  simproc_setup dvd_cancel_factor
   1.152    ("((l::'a::idom) * m) dvd n"
   1.153    |"(l::'a::idom) dvd (m * n)") =
   1.154 -  {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
   1.155 +  \<open>fn phi => Numeral_Simprocs.dvd_cancel_factor\<close>
   1.156  
   1.157  simproc_setup divide_cancel_factor
   1.158    ("((l::'a::field) * m) / n"
   1.159    |"(l::'a::field) / (m * n)") =
   1.160 -  {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
   1.161 +  \<open>fn phi => Numeral_Simprocs.divide_cancel_factor\<close>
   1.162  
   1.163  ML_file "Tools/nat_numeral_simprocs.ML"
   1.164  
   1.165  simproc_setup nat_combine_numerals
   1.166    ("(i::nat) + j" | "Suc (i + j)") =
   1.167 -  {* fn phi => Nat_Numeral_Simprocs.combine_numerals *}
   1.168 +  \<open>fn phi => Nat_Numeral_Simprocs.combine_numerals\<close>
   1.169  
   1.170  simproc_setup nateq_cancel_numerals
   1.171    ("(l::nat) + m = n" | "(l::nat) = m + n" |
   1.172     "(l::nat) * m = n" | "(l::nat) = m * n" |
   1.173     "Suc m = n" | "m = Suc n") =
   1.174 -  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals *}
   1.175 +  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numerals\<close>
   1.176  
   1.177  simproc_setup natless_cancel_numerals
   1.178    ("(l::nat) + m < n" | "(l::nat) < m + n" |
   1.179     "(l::nat) * m < n" | "(l::nat) < m * n" |
   1.180     "Suc m < n" | "m < Suc n") =
   1.181 -  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numerals *}
   1.182 +  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numerals\<close>
   1.183  
   1.184  simproc_setup natle_cancel_numerals
   1.185    ("(l::nat) + m \<le> n" | "(l::nat) \<le> m + n" |
   1.186     "(l::nat) * m \<le> n" | "(l::nat) \<le> m * n" |
   1.187     "Suc m \<le> n" | "m \<le> Suc n") =
   1.188 -  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numerals *}
   1.189 +  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numerals\<close>
   1.190  
   1.191  simproc_setup natdiff_cancel_numerals
   1.192    ("((l::nat) + m) - n" | "(l::nat) - (m + n)" |
   1.193     "(l::nat) * m - n" | "(l::nat) - m * n" |
   1.194     "Suc m - n" | "m - Suc n") =
   1.195 -  {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
   1.196 +  \<open>fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals\<close>
   1.197  
   1.198  simproc_setup nat_eq_cancel_numeral_factor
   1.199    ("(l::nat) * m = n" | "(l::nat) = m * n") =
   1.200 -  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
   1.201 +  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor\<close>
   1.202  
   1.203  simproc_setup nat_less_cancel_numeral_factor
   1.204    ("(l::nat) * m < n" | "(l::nat) < m * n") =
   1.205 -  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
   1.206 +  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor\<close>
   1.207  
   1.208  simproc_setup nat_le_cancel_numeral_factor
   1.209    ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
   1.210 -  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
   1.211 +  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor\<close>
   1.212  
   1.213  simproc_setup nat_div_cancel_numeral_factor
   1.214    ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
   1.215 -  {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
   1.216 +  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor\<close>
   1.217  
   1.218  simproc_setup nat_dvd_cancel_numeral_factor
   1.219    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   1.220 -  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
   1.221 +  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor\<close>
   1.222  
   1.223  simproc_setup nat_eq_cancel_factor
   1.224    ("(l::nat) * m = n" | "(l::nat) = m * n") =
   1.225 -  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
   1.226 +  \<open>fn phi => Nat_Numeral_Simprocs.eq_cancel_factor\<close>
   1.227  
   1.228  simproc_setup nat_less_cancel_factor
   1.229    ("(l::nat) * m < n" | "(l::nat) < m * n") =
   1.230 -  {* fn phi => Nat_Numeral_Simprocs.less_cancel_factor *}
   1.231 +  \<open>fn phi => Nat_Numeral_Simprocs.less_cancel_factor\<close>
   1.232  
   1.233  simproc_setup nat_le_cancel_factor
   1.234    ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
   1.235 -  {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
   1.236 +  \<open>fn phi => Nat_Numeral_Simprocs.le_cancel_factor\<close>
   1.237  
   1.238  simproc_setup nat_div_cancel_factor
   1.239    ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
   1.240 -  {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
   1.241 +  \<open>fn phi => Nat_Numeral_Simprocs.div_cancel_factor\<close>
   1.242  
   1.243  simproc_setup nat_dvd_cancel_factor
   1.244    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
   1.245 -  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor *}
   1.246 +  \<open>fn phi => Nat_Numeral_Simprocs.dvd_cancel_factor\<close>
   1.247  
   1.248 -declaration {* 
   1.249 +declaration \<open>
   1.250    K (Lin_Arith.add_simprocs
   1.251        [@{simproc semiring_assoc_fold},
   1.252         @{simproc int_combine_numerals},
   1.253 @@ -297,6 +297,6 @@
   1.254         @{simproc natless_cancel_numerals},
   1.255         @{simproc natle_cancel_numerals},
   1.256         @{simproc natdiff_cancel_numerals}])
   1.257 -*}
   1.258 +\<close>
   1.259  
   1.260  end