--- 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>
--- 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"
--- 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+
--- 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
--- 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
--- 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
--- 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>
--- 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