# HG changeset patch
# User haftmann
# Date 1507569047 -7200
# Node ID 4eb431c3f9745d61a385e630284b484aa353fcf0
# Parent  ecc99a5a1ab8095604f2a2c1f5fe58b23ca7343a
tuned imports

diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Numeric types for code generation onto target language numerals only\<close>
 
 theory Code_Numeral
-imports Nat_Transfer Divides Lifting
+imports Divides Lifting
 begin
 
 subsection \<open>Type of target language integers\<close>
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/GCD.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -1708,36 +1708,6 @@
 
 end
 
-text \<open>Transfer setup\<close>
-
-lemma transfer_nat_int_gcd:
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
-  for x y :: int
-  unfolding gcd_int_def lcm_int_def by auto
-
-lemma transfer_nat_int_gcd_closures:
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
-  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
-  for x y :: int
-  by (auto simp add: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_nat_int
-  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
-
-lemma transfer_int_nat_gcd:
-  "gcd (int x) (int y) = int (gcd x y)"
-  "lcm (int x) (int y) = int (lcm x y)"
-  by (auto simp: gcd_int_def lcm_int_def)
-
-lemma transfer_int_nat_gcd_closures:
-  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
-  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
-  by (auto simp: gcd_int_def lcm_int_def)
-
-declare transfer_morphism_int_nat
-  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
-
 lemma gcd_nat_induct:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/HOL.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -1574,6 +1574,14 @@
 
 subsection \<open>Other simple lemmas and lemma duplicates\<close>
 
+lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
+  by auto
+
+lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
+  by auto
+
 lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
   by blast+
 
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/Int.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -556,6 +556,43 @@
   "nat (of_bool P) = of_bool P"
   by auto
 
+lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
+  (is "?P = (?L \<and> ?R)")
+  for i :: int
+proof (cases "i < 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  have "?P = ?L"
+  proof
+    assume ?P
+    then show ?L using False by auto
+  next
+    assume ?L
+    moreover from False have "int (nat i) = i"
+      by (simp add: not_less)
+    ultimately show ?P
+      by simp
+  qed
+  with False show ?thesis by simp
+qed
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
+  by (auto split: split_nat)
+
+lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
+proof
+  assume "\<exists>x. P x"
+  then obtain x where "P x" ..
+  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
+  then show "\<exists>x\<ge>0. P (nat x)" ..
+next
+  assume "\<exists>x\<ge>0. P (nat x)"
+  then show "\<exists>x. P x" by auto
+qed
+
 
 text \<open>For termination proofs:\<close>
 lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
@@ -1043,25 +1080,6 @@
 \<close>
 lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
 
-lemma split_nat [arith_split]: "P (nat i) = ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
-  (is "?P = (?L \<and> ?R)")
-  for i :: int
-proof (cases "i < 0")
-  case True
-  then show ?thesis by auto
-next
-  case False
-  have "?P = ?L"
-  proof
-    assume ?P
-    then show ?L using False by auto
-  next
-    assume ?L
-    then show ?P using False by simp
-  qed
-  with False show ?thesis by simp
-qed
-
 lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
   by auto
 
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/List.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -6600,39 +6600,6 @@
   by (induction xs) simp_all
 
 
-subsection \<open>Transfer\<close>
-
-definition embed_list :: "nat list \<Rightarrow> int list" where
-"embed_list l = map int l"
-
-definition nat_list :: "int list \<Rightarrow> bool" where
-"nat_list l = nat_set (set l)"
-
-definition return_list :: "int list \<Rightarrow> nat list" where
-"return_list l = map nat l"
-
-lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
-    embed_list (return_list l) = l"
-  unfolding embed_list_def return_list_def nat_list_def nat_set_def
-  apply (induct l)
-  apply auto
-done
-
-lemma transfer_nat_int_list_functions:
-  "l @ m = return_list (embed_list l @ embed_list m)"
-  "[] = return_list []"
-  unfolding return_list_def embed_list_def
-  apply auto
-  apply (induct l, auto)
-  apply (induct m, auto)
-done
-
-(*
-lemma transfer_nat_int_fold1: "fold f l x =
-    fold (%x. f (nat x)) (embed_list l) x";
-*)
-
-
 subsection \<open>Code generation\<close>
 
 text\<open>Optional tail recursive version of @{const map}. Can avoid
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/Nat_Transfer.thy	Mon Oct 09 19:10:47 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 Divides
+imports List GCD
 begin
 
 subsection \<open>Generic transfer machinery\<close>
@@ -90,34 +90,11 @@
 
 text \<open>first-order quantifiers\<close>
 
-lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
-  by (simp split: split_nat)
-
-lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
-proof
-  assume "\<exists>x. P x"
-  then obtain x where "P x" ..
-  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
-  then show "\<exists>x\<ge>0. P (nat x)" ..
-next
-  assume "\<exists>x\<ge>0. P (nat x)"
-  then show "\<exists>x. P x" by auto
-qed
-
 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)
 
-(* should we restrict these? *)
-lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
-    (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
-  by auto
-
-lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
-    (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
-  by auto
-
 declare transfer_morphism_nat_int [transfer add
   cong: all_cong ex_cong]
 
@@ -142,17 +119,10 @@
     "A Un B = nat ` (int ` A Un int ` B)"
     "A Int B = nat ` (int ` A Int int ` B)"
     "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
-  apply (rule card_image [symmetric])
-  apply (auto simp add: inj_on_def image_def)
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in exI)
-  apply auto
-done
+    "{..n} = nat ` {0..int n}"
+    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
+  by (rule card_image [symmetric])
+    (auto simp add: inj_on_def image_def intro: bexI [of _ "int x" for x] exI [of _ "int x" for x])
 
 lemma transfer_nat_int_set_function_closures [no_atp]:
     "nat_set {}"
@@ -161,6 +131,7 @@
     "nat_set {x. x >= 0 & P x}"
     "nat_set (int ` C)"
     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
+    "x >= 0 \<Longrightarrow> nat_set {x..y}"
   unfolding nat_set_def apply auto
 done
 
@@ -361,6 +332,7 @@
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
     "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
     "{x. x >= 0 & P x} = int ` {x. P(int x)}"
+    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
        (* need all variants of these! *)
   by (simp_all only: is_nat_def transfer_nat_int_set_functions
           transfer_nat_int_set_function_closures
@@ -374,6 +346,7 @@
     "nat_set {x. x >= 0 & P x}"
     "nat_set (int ` C)"
     "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
+    "is_nat x \<Longrightarrow> nat_set {x..y}"
   by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
 
 lemma transfer_int_nat_set_relations [no_atp]:
@@ -430,4 +403,62 @@
 
 declare transfer_morphism_int_nat [transfer add return: even_int_iff]
 
+lemma transfer_nat_int_gcd [no_atp]:
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
+  for x y :: int
+  unfolding gcd_int_def lcm_int_def by auto
+
+lemma transfer_nat_int_gcd_closures [no_atp]:
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> gcd x y \<ge> 0"
+  "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> lcm x y \<ge> 0"
+  for x y :: int
+  by (auto simp add: gcd_int_def lcm_int_def)
+
+declare transfer_morphism_nat_int
+  [transfer add return: transfer_nat_int_gcd transfer_nat_int_gcd_closures]
+
+lemma transfer_int_nat_gcd [no_atp]:
+  "gcd (int x) (int y) = int (gcd x y)"
+  "lcm (int x) (int y) = int (lcm x y)"
+  by (auto simp: gcd_int_def lcm_int_def)
+
+lemma transfer_int_nat_gcd_closures [no_atp]:
+  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
+  "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
+  by (auto simp: gcd_int_def lcm_int_def)
+
+declare transfer_morphism_int_nat
+  [transfer add return: transfer_int_nat_gcd transfer_int_nat_gcd_closures]
+
+definition embed_list :: "nat list \<Rightarrow> int list" where
+"embed_list l = map int l"
+
+definition nat_list :: "int list \<Rightarrow> bool" where
+"nat_list l = nat_set (set l)"
+
+definition return_list :: "int list \<Rightarrow> nat list" where
+"return_list l = map nat l"
+
+lemma transfer_nat_int_list_return_embed [no_atp]:
+  "nat_list l \<longrightarrow> embed_list (return_list l) = l"
+  unfolding embed_list_def return_list_def nat_list_def nat_set_def
+  apply (induct l)
+  apply auto
+done
+
+lemma transfer_nat_int_list_functions [no_atp]:
+  "l @ m = return_list (embed_list l @ embed_list m)"
+  "[] = return_list []"
+  unfolding return_list_def embed_list_def
+  apply auto
+  apply (induct l, auto)
+  apply (induct m, auto)
+done
+
+(*
+lemma transfer_nat_int_fold1: "fold f l x =
+    fold (%x. f (nat x)) (embed_list l) x";
+*)
+
 end
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Semiring normalization\<close>
 
 theory Semiring_Normalization
-imports Numeral_Simprocs Nat_Transfer
+imports Numeral_Simprocs
 begin
 
 text \<open>Prelude\<close>
diff -r ecc99a5a1ab8 -r 4eb431c3f974 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Oct 09 19:10:47 2017 +0200
@@ -14,7 +14,7 @@
 section \<open>Set intervals\<close>
 
 theory Set_Interval
-imports Lattices_Big Divides Nat_Transfer
+imports Divides
 begin
 
 context ord
@@ -2231,42 +2231,4 @@
 
 (* TODO: Add support for more kinds of intervals here *)
 
-
-subsection \<open>Transfer setup\<close>
-
-lemma transfer_nat_int_set_functions:
-    "{..n} = nat ` {0..int n}"
-    "{m..n} = nat ` {int m..int n}"  (* need all variants of these! *)
-  apply (auto simp add: image_def)
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  apply (rule_tac x = "int x" in bexI)
-  apply auto
-  done
-
-lemma transfer_nat_int_set_function_closures:
-    "x >= 0 \<Longrightarrow> nat_set {x..y}"
-  by (simp add: nat_set_def)
-
-declare transfer_morphism_nat_int[transfer add
-  return: transfer_nat_int_set_functions
-    transfer_nat_int_set_function_closures
-]
-
-lemma transfer_int_nat_set_functions:
-    "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
-  by (simp only: is_nat_def transfer_nat_int_set_functions
-    transfer_nat_int_set_function_closures
-    transfer_nat_int_set_return_embed nat_0_le
-    cong: transfer_nat_int_set_cong)
-
-lemma transfer_int_nat_set_function_closures:
-    "is_nat x \<Longrightarrow> nat_set {x..y}"
-  by (simp only: transfer_nat_int_set_function_closures is_nat_def)
-
-declare transfer_morphism_int_nat[transfer add
-  return: transfer_int_nat_set_functions
-    transfer_int_nat_set_function_closures
-]
-
 end