--- a/src/HOL/SetInterval.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/SetInterval.thy Thu Oct 29 11:41:36 2009 +0100
@@ -9,7 +9,7 @@
header {* Set intervals *}
theory SetInterval
-imports Int
+imports Int Nat_Transfer
begin
context ord
@@ -1150,4 +1150,41 @@
"\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
"\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
+subsection {* Transfer setup *}
+
+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 TransferMorphism_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 TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_set_functions
+ transfer_int_nat_set_function_closures
+]
+
end