src/HOL/Nat_Transfer.thy

--- a/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
+++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:22 2017 +0200
@@ -3,7 +3,7 @@
 section \<open>Generic transfer machinery;  specific transfer from nats to ints and back.\<close>
 
 theory Nat_Transfer
-imports Int
+imports Int Divides
 begin
 
 subsection \<open>Generic transfer machinery\<close>
@@ -21,7 +21,8 @@
 
 text \<open>set up transfer direction\<close>
 
-lemma transfer_morphism_nat_int: "transfer_morphism nat (op <= (0::int))" ..
+lemma transfer_morphism_nat_int [no_atp]:
+  "transfer_morphism nat (op <= (0::int))" ..
 
 declare transfer_morphism_nat_int [transfer add
   mode: manual
@@ -31,7 +32,7 @@
 
 text \<open>basic functions and relations\<close>
 
-lemma transfer_nat_int_numerals [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_numerals [no_atp, transfer key: transfer_morphism_nat_int]:
     "(0::nat) = nat 0"
     "(1::nat) = nat 1"
     "(2::nat) = nat 2"
@@ -46,15 +47,17 @@
 lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
   by (simp add: tsub_def)
 
-lemma transfer_nat_int_functions [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_functions [no_atp, transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
     "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
   by (auto simp add: eq_nat_nat_iff nat_mult_distrib
-      nat_power_eq tsub_def)
+      nat_power_eq tsub_def nat_div_distrib nat_mod_distrib)
 
-lemma transfer_nat_int_function_closures [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_function_closures [no_atp, transfer key: transfer_morphism_nat_int]:
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
     "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
@@ -64,9 +67,16 @@
     "(2::int) >= 0"
     "(3::int) >= 0"
     "int z >= 0"
-  by (auto simp add: zero_le_mult_iff tsub_def)
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+            apply (auto simp add: zero_le_mult_iff tsub_def pos_imp_zdiv_nonneg_iff)
+   apply (cases "y = 0")
+    apply (auto simp add: pos_imp_zdiv_nonneg_iff)
+  apply (cases "y = 0")
+   apply auto
+  done
 
-lemma transfer_nat_int_relations [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_relations [no_atp, transfer key: transfer_morphism_nat_int]:
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
       (nat (x::int) = nat y) = (x = y)"
     "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
@@ -94,7 +104,7 @@
   then show "\<exists>x. P x" by auto
 qed
 
-lemma transfer_nat_int_quantifiers [transfer key: transfer_morphism_nat_int]:
+lemma transfer_nat_int_quantifiers [no_atp, transfer key: transfer_morphism_nat_int]:
     "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
     "(EX (x::nat). P x) = (EX (x::int). x >= 0 & P (nat x))"
   by (rule all_nat, rule ex_nat)
@@ -126,7 +136,7 @@
 where
   "nat_set S = (ALL x:S. x >= 0)"
 
-lemma transfer_nat_int_set_functions:
+lemma transfer_nat_int_set_functions [no_atp]:
     "card A = card (int ` A)"
     "{} = nat ` ({}::int set)"
     "A Un B = nat ` (int ` A Un int ` B)"
@@ -144,7 +154,7 @@
   apply auto
 done
 
-lemma transfer_nat_int_set_function_closures:
+lemma transfer_nat_int_set_function_closures [no_atp]:
     "nat_set {}"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
@@ -154,7 +164,7 @@
   unfolding nat_set_def apply auto
 done
 
-lemma transfer_nat_int_set_relations:
+lemma transfer_nat_int_set_relations [no_atp]:
     "(finite A) = (finite (int ` A))"
     "(x : A) = (int x : int ` A)"
     "(A = B) = (int ` A = int ` B)"
@@ -169,11 +179,11 @@
   apply (drule_tac x = "int x" in spec, auto)
 done
 
-lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
+lemma transfer_nat_int_set_return_embed [no_atp]: "nat_set A \<Longrightarrow>
     (int ` nat ` A = A)"
   by (auto simp add: nat_set_def image_def)
 
-lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
+lemma transfer_nat_int_set_cong [no_atp]: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
     {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
   by auto
 
@@ -189,7 +199,7 @@
 text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod:
+lemma transfer_nat_int_sum_prod [no_atp]:
     "sum f A = sum (%x. f (nat x)) (int ` A)"
     "prod f A = prod (%x. f (nat x)) (int ` A)"
   apply (subst sum.reindex)
@@ -199,14 +209,14 @@
 done
 
 (* this handles the case where the *range* of f is nat *)
-lemma transfer_nat_int_sum_prod2:
+lemma transfer_nat_int_sum_prod2 [no_atp]:
     "sum f A = nat(sum (%x. int (f x)) A)"
     "prod f A = nat(prod (%x. int (f x)) A)"
   apply (simp only: int_sum [symmetric] nat_int)
   apply (simp only: int_prod [symmetric] nat_int)
   done
 
-lemma transfer_nat_int_sum_prod_closure:
+lemma transfer_nat_int_sum_prod_closure [no_atp]:
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> sum f A >= 0"
     "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> prod f A >= 0"
   unfolding nat_set_def
@@ -236,7 +246,7 @@
    Also, why aren't sum.cong and prod.cong enough,
    with the previously mentioned rule turned on? *)
 
-lemma transfer_nat_int_sum_prod_cong:
+lemma transfer_nat_int_sum_prod_cong [no_atp]:
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
       sum f A = sum g B"
     "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
@@ -257,7 +267,7 @@
 
 text \<open>set up transfer direction\<close>
 
-lemma transfer_morphism_int_nat: "transfer_morphism int (\<lambda>n. True)" ..
+lemma transfer_morphism_int_nat [no_atp]: "transfer_morphism int (\<lambda>n. True)" ..
 
 declare transfer_morphism_int_nat [transfer add
   mode: manual
@@ -273,21 +283,23 @@
 where
   "is_nat x = (x >= 0)"
 
-lemma transfer_int_nat_numerals:
+lemma transfer_int_nat_numerals [no_atp]:
     "0 = int 0"
     "1 = int 1"
     "2 = int 2"
     "3 = int 3"
   by auto
 
-lemma transfer_int_nat_functions:
+lemma transfer_int_nat_functions [no_atp]:
     "(int x) + (int y) = int (x + y)"
     "(int x) * (int y) = int (x * y)"
     "tsub (int x) (int y) = int (x - y)"
     "(int x)^n = int (x^n)"
-  by (auto simp add: tsub_def)
+    "(int x) div (int y) = int (x div y)"
+    "(int x) mod (int y) = int (x mod y)"
+  by (auto simp add: zdiv_int zmod_int tsub_def)
 
-lemma transfer_int_nat_function_closures:
+lemma transfer_int_nat_function_closures [no_atp]:
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
@@ -297,9 +309,11 @@
     "is_nat 2"
     "is_nat 3"
     "is_nat (int z)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
 
-lemma transfer_int_nat_relations:
+lemma transfer_int_nat_relations [no_atp]:
     "(int x = int y) = (x = y)"
     "(int x < int y) = (x < y)"
     "(int x <= int y) = (x <= y)"
@@ -316,7 +330,7 @@
 
 text \<open>first-order quantifiers\<close>
 
-lemma transfer_int_nat_quantifiers:
+lemma transfer_int_nat_quantifiers [no_atp]:
     "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
     "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
   apply (subst all_nat)
@@ -341,7 +355,7 @@
 
 text \<open>operations with sets\<close>
 
-lemma transfer_int_nat_set_functions:
+lemma transfer_int_nat_set_functions [no_atp]:
     "nat_set A \<Longrightarrow> card A = card (nat ` A)"
     "{} = int ` ({}::nat set)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
@@ -353,7 +367,7 @@
           transfer_nat_int_set_return_embed nat_0_le
           cong: transfer_nat_int_set_cong)
 
-lemma transfer_int_nat_set_function_closures:
+lemma transfer_int_nat_set_function_closures [no_atp]:
     "nat_set {}"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
@@ -362,7 +376,7 @@
     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
 
-lemma transfer_int_nat_set_relations:
+lemma transfer_int_nat_set_relations [no_atp]:
     "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
     "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
@@ -371,12 +385,12 @@
   by (simp_all only: is_nat_def transfer_nat_int_set_relations
     transfer_nat_int_set_return_embed nat_0_le)
 
-lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
+lemma transfer_int_nat_set_return_embed [no_atp]: "nat ` int ` A = A"
   by (simp only: transfer_nat_int_set_relations
     transfer_nat_int_set_function_closures
     transfer_nat_int_set_return_embed nat_0_le)
 
-lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
+lemma transfer_int_nat_set_cong [no_atp]: "(!!x. P x = P' x) \<Longrightarrow>
     {(x::nat). P x} = {x. P' x}"
   by auto
 
@@ -392,7 +406,7 @@
 text \<open>sum and prod\<close>
 
 (* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod:
+lemma transfer_int_nat_sum_prod [no_atp]:
     "nat_set A \<Longrightarrow> sum f A = sum (%x. f (int x)) (nat ` A)"
     "nat_set A \<Longrightarrow> prod f A = prod (%x. f (int x)) (nat ` A)"
   apply (subst sum.reindex)
@@ -403,7 +417,7 @@
 done
 
 (* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2:
+lemma transfer_int_nat_sum_prod2 [no_atp]:
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> sum f A = int(sum (%x. nat (f x)) A)"
     "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
       prod f A = int(prod (%x. nat (f x)) A)"
@@ -414,4 +428,6 @@
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   cong: sum.cong prod.cong]
 
+declare transfer_morphism_int_nat [transfer add return: even_int_iff]
+
 end