src/HOL/Nat_Transfer.thy
changeset 66817 0b12755ccbb2
parent 66795 420d0080545f
child 66836 4eb431c3f974
     1.1 --- a/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
     1.5  
     1.6  theory Nat_Transfer
     1.7 -imports Int
     1.8 +imports Int Divides
     1.9  begin
    1.10  
    1.11  subsection \<open>Generic transfer machinery\<close>
    1.12 @@ -21,7 +21,8 @@
    1.13  
    1.14  text \<open>set up transfer direction\<close>
    1.15  
    1.16 -lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
    1.17 +lemma transfer_morphism_nat_int [no_atp]:
    1.18 +  "transfer_morphism nat (op <= (0::int))" ..
    1.19  
    1.20  declare transfer_morphism_nat_int [transfer add
    1.21    mode: manual
    1.22 @@ -31,7 +32,7 @@
    1.23  
    1.24  text \<open>basic functions and relations\<close>
    1.25  
    1.26 -lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
    1.27 +lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
    1.28      "(0::nat) = nat 0"
    1.29      "(1::nat) = nat 1"
    1.30      "(2::nat) = nat 2"
    1.31 @@ -46,15 +47,17 @@
    1.32  lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
    1.33    by (simp add: tsub_def)
    1.34  
    1.35 -lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
    1.36 +lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
    1.37      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
    1.38      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
    1.39      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
    1.40      "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
    1.41 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
    1.42 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
    1.43    by (auto simp add: eq_nat_nat_iff nat_mult_distrib
    1.44 -      nat_power_eq tsub_def)
    1.45 +      nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
    1.46  
    1.47 -lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
    1.48 +lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
    1.49      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
    1.50      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
    1.51      "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
    1.52 @@ -64,9 +67,16 @@
    1.53      "(2::int) >= 0"
    1.54      "(3::int) >= 0"
    1.55      "int z >= 0"
    1.56 -  by (auto simp add: zero_le_mult_iff tsub_def)
    1.57 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
    1.58 +    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
    1.59 +            apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
    1.60 +   apply (cases "y = 0")
    1.61 +    apply (auto simp add: pos_imp_zdiv_nonneg_iff)
    1.62 +  apply (cases "y = 0")
    1.63 +   apply auto
    1.64 +  done
    1.65  
    1.66 -lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
    1.67 +lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
    1.68      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    1.69        (nat (x::int) = nat y) = (x = y)"
    1.70      "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
    1.71 @@ -94,7 +104,7 @@
    1.72    then show "\<exists>x. P x" by auto
    1.73  qed
    1.74  
    1.75 -lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
    1.76 +lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
    1.77      "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
    1.78      "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
    1.79    by (rule all_nat, rule ex_nat)
    1.80 @@ -126,7 +136,7 @@
    1.81  where
    1.82    "nat_set S = (ALL x:S. x >= 0)"
    1.83  
    1.84 -lemma transfer_nat_int_set_functions:
    1.85 +lemma transfer_nat_int_set_functions [no_atp]:
    1.86      "card A = card (int ` A)"
    1.87      "{} = nat ` ({}::int set)"
    1.88      "A Un B = nat ` (int ` A Un int ` B)"
    1.89 @@ -144,7 +154,7 @@
    1.90    apply auto
    1.91  done
    1.92  
    1.93 -lemma transfer_nat_int_set_function_closures:
    1.94 +lemma transfer_nat_int_set_function_closures [no_atp]:
    1.95      "nat_set {}"
    1.96      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
    1.97      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
    1.98 @@ -154,7 +164,7 @@
    1.99    unfolding nat_set_def apply auto
   1.100  done
   1.101  
   1.102 -lemma transfer_nat_int_set_relations:
   1.103 +lemma transfer_nat_int_set_relations [no_atp]:
   1.104      "(finite A) = (finite (int ` A))"
   1.105      "(x : A) = (int x : int ` A)"
   1.106      "(A = B) = (int ` A = int ` B)"
   1.107 @@ -169,11 +179,11 @@
   1.108    apply (drule_tac x = "int x" in spec, auto)
   1.109  done
   1.110  
   1.111 -lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
   1.112 +lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
   1.113      (int ` nat ` A = A)"
   1.114    by (auto simp add: nat_set_def image_def)
   1.115  
   1.116 -lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   1.117 +lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
   1.118      {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   1.119    by auto
   1.120  
   1.121 @@ -189,7 +199,7 @@
   1.122  text \<open>sum and prod\<close>
   1.123  
   1.124  (* this handles the case where the *domain* of f is nat *)
   1.125 -lemma transfer_nat_int_sum_prod:
   1.126 +lemma transfer_nat_int_sum_prod [no_atp]:
   1.127      "sum f A = sum (%x. f (nat x)) (int ` A)"
   1.128      "prod f A = prod (%x. f (nat x)) (int ` A)"
   1.129    apply (subst sum.reindex)
   1.130 @@ -199,14 +209,14 @@
   1.131  done
   1.132  
   1.133  (* this handles the case where the *range* of f is nat *)
   1.134 -lemma transfer_nat_int_sum_prod2:
   1.135 +lemma transfer_nat_int_sum_prod2 [no_atp]:
   1.136      "sum f A = nat(sum (%x. int (f x)) A)"
   1.137      "prod f A = nat(prod (%x. int (f x)) A)"
   1.138    apply (simp only: int_sum [symmetric] nat_int)
   1.139    apply (simp only: int_prod [symmetric] nat_int)
   1.140    done
   1.141  
   1.142 -lemma transfer_nat_int_sum_prod_closure:
   1.143 +lemma transfer_nat_int_sum_prod_closure [no_atp]:
   1.144      "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
   1.145      "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   1.146    unfolding nat_set_def
   1.147 @@ -236,7 +246,7 @@
   1.148     Also, why aren't sum.cong and prod.cong enough,
   1.149     with the previously mentioned rule turned on? *)
   1.150  
   1.151 -lemma transfer_nat_int_sum_prod_cong:
   1.152 +lemma transfer_nat_int_sum_prod_cong [no_atp]:
   1.153      "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   1.154        sum f A = sum g B"
   1.155      "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
   1.156 @@ -257,7 +267,7 @@
   1.157  
   1.158  text \<open>set up transfer direction\<close>
   1.159  
   1.160 -lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
   1.161 +lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
   1.162  
   1.163  declare transfer_morphism_int_nat [transfer add
   1.164    mode: manual
   1.165 @@ -273,21 +283,23 @@
   1.166  where
   1.167    "is_nat x = (x >= 0)"
   1.168  
   1.169 -lemma transfer_int_nat_numerals:
   1.170 +lemma transfer_int_nat_numerals [no_atp]:
   1.171      "0 = int 0"
   1.172      "1 = int 1"
   1.173      "2 = int 2"
   1.174      "3 = int 3"
   1.175    by auto
   1.176  
   1.177 -lemma transfer_int_nat_functions:
   1.178 +lemma transfer_int_nat_functions [no_atp]:
   1.179      "(int x) + (int y) = int (x + y)"
   1.180      "(int x) * (int y) = int (x * y)"
   1.181      "tsub (int x) (int y) = int (x - y)"
   1.182      "(int x)^n = int (x^n)"
   1.183 -  by (auto simp add: tsub_def)
   1.184 +    "(int x) div (int y) = int (x div y)"
   1.185 +    "(int x) mod (int y) = int (x mod y)"
   1.186 +  by (auto simp add: zdiv_int zmod_int tsub_def)
   1.187  
   1.188 -lemma transfer_int_nat_function_closures:
   1.189 +lemma transfer_int_nat_function_closures [no_atp]:
   1.190      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
   1.191      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
   1.192      "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
   1.193 @@ -297,9 +309,11 @@
   1.194      "is_nat 2"
   1.195      "is_nat 3"
   1.196      "is_nat (int z)"
   1.197 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
   1.198 +    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   1.199    by (simp_all only: is_nat_def transfer_nat_int_function_closures)
   1.200  
   1.201 -lemma transfer_int_nat_relations:
   1.202 +lemma transfer_int_nat_relations [no_atp]:
   1.203      "(int x = int y) = (x = y)"
   1.204      "(int x < int y) = (x < y)"
   1.205      "(int x <= int y) = (x <= y)"
   1.206 @@ -316,7 +330,7 @@
   1.207  
   1.208  text \<open>first-order quantifiers\<close>
   1.209  
   1.210 -lemma transfer_int_nat_quantifiers:
   1.211 +lemma transfer_int_nat_quantifiers [no_atp]:
   1.212      "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
   1.213      "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   1.214    apply (subst all_nat)
   1.215 @@ -341,7 +355,7 @@
   1.216  
   1.217  text \<open>operations with sets\<close>
   1.218  
   1.219 -lemma transfer_int_nat_set_functions:
   1.220 +lemma transfer_int_nat_set_functions [no_atp]:
   1.221      "nat_set A \<Longrightarrow> card A = card (nat ` A)"
   1.222      "{} = int ` ({}::nat set)"
   1.223      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
   1.224 @@ -353,7 +367,7 @@
   1.225            transfer_nat_int_set_return_embed nat_0_le
   1.226            cong: transfer_nat_int_set_cong)
   1.227  
   1.228 -lemma transfer_int_nat_set_function_closures:
   1.229 +lemma transfer_int_nat_set_function_closures [no_atp]:
   1.230      "nat_set {}"
   1.231      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
   1.232      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
   1.233 @@ -362,7 +376,7 @@
   1.234      "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   1.235    by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
   1.236  
   1.237 -lemma transfer_int_nat_set_relations:
   1.238 +lemma transfer_int_nat_set_relations [no_atp]:
   1.239      "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
   1.240      "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
   1.241      "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
   1.242 @@ -371,12 +385,12 @@
   1.243    by (simp_all only: is_nat_def transfer_nat_int_set_relations
   1.244      transfer_nat_int_set_return_embed nat_0_le)
   1.245  
   1.246 -lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
   1.247 +lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
   1.248    by (simp only: transfer_nat_int_set_relations
   1.249      transfer_nat_int_set_function_closures
   1.250      transfer_nat_int_set_return_embed nat_0_le)
   1.251  
   1.252 -lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
   1.253 +lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
   1.254      {(x::nat). P x} = {x. P' x}"
   1.255    by auto
   1.256  
   1.257 @@ -392,7 +406,7 @@
   1.258  text \<open>sum and prod\<close>
   1.259  
   1.260  (* this handles the case where the *domain* of f is int *)
   1.261 -lemma transfer_int_nat_sum_prod:
   1.262 +lemma transfer_int_nat_sum_prod [no_atp]:
   1.263      "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
   1.264      "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
   1.265    apply (subst sum.reindex)
   1.266 @@ -403,7 +417,7 @@
   1.267  done
   1.268  
   1.269  (* this handles the case where the *range* of f is int *)
   1.270 -lemma transfer_int_nat_sum_prod2:
   1.271 +lemma transfer_int_nat_sum_prod2 [no_atp]:
   1.272      "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
   1.273      "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
   1.274        prod f A = int(prod (%x. nat (f x)) A)"
   1.275 @@ -414,4 +428,6 @@
   1.276    return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   1.277    cong: sum.cong prod.cong]
   1.278  
   1.279 +declare transfer_morphism_int_nat [transfer add return: even_int_iff]
   1.280 +
   1.281  end