more int/nat transfer rules; examples of new untransferred attribute

--- a/src/HOL/ex/Transfer_Ex.thy	Mon Jun 10 06:08:14 2013 -0700
+++ b/src/HOL/ex/Transfer_Ex.thy	Mon Jun 10 06:08:17 2013 -0700
@@ -2,7 +2,7 @@
 header {* Various examples for transfer procedure *}
 
 theory Transfer_Ex
-imports Main
+imports Main Transfer_Int_Nat
 begin
 
 lemma ex1: "(x::nat) + y = y + x"
@@ -11,31 +11,55 @@
 lemma "0 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> x + y = y + x"
   by (fact ex1 [transferred])
 
+(* Using new transfer package *)
+lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> x + y = y + x"
+  by (fact ex1 [untransferred])
+
 lemma ex2: "(a::nat) div b * b + a mod b = a"
   by (rule mod_div_equality)
 
 lemma "0 \<le> (b\<Colon>int) \<Longrightarrow> 0 \<le> (a\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
   by (fact ex2 [transferred])
 
+(* Using new transfer package *)
+lemma "0 \<le> (a\<Colon>int) \<Longrightarrow> 0 \<le> (b\<Colon>int) \<Longrightarrow> a div b * b + a mod b = a"
+  by (fact ex2 [untransferred])
+
 lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
   by auto
 
 lemma "\<forall>x\<ge>0\<Colon>int. \<forall>y\<ge>0. \<exists>z\<ge>0. x + y \<le> z"
   by (fact ex3 [transferred nat_int])
 
+(* Using new transfer package *)
+lemma "\<forall>x\<Colon>int\<in>{0..}. \<forall>y\<in>{0..}. \<exists>z\<in>{0..}. x + y \<le> z"
+  by (fact ex3 [untransferred])
+
 lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
   by auto
 
 lemma "0 \<le> (x\<Colon>int) \<Longrightarrow> 0 \<le> (y\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
   by (fact ex4 [transferred])
 
+(* Using new transfer package *)
+lemma "0 \<le> (y\<Colon>int) \<Longrightarrow> 0 \<le> (x\<Colon>int) \<Longrightarrow> y \<le> x \<Longrightarrow> tsub x y + y = x"
+  by (fact ex4 [untransferred])
+
 lemma ex5: "(2::nat) * \<Sum>{..n} = n * (n + 1)"
   by (induct n rule: nat_induct, auto)
 
 lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
   by (fact ex5 [transferred])
 
+(* Using new transfer package *)
+lemma "0 \<le> (n\<Colon>int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+  by (fact ex5 [untransferred])
+
 lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
   by (fact ex5 [transferred, transferred])
 
-end
\ No newline at end of file
+(* Using new transfer package *)
+lemma "0 \<le> (n\<Colon>nat) \<Longrightarrow> 2 * \<Sum>{..n} = n * (n + 1)"
+  by (fact ex5 [untransferred, Transfer.transferred])
+
+end

--- a/src/HOL/ex/Transfer_Int_Nat.thy	Mon Jun 10 06:08:14 2013 -0700
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Mon Jun 10 06:08:17 2013 -0700
@@ -91,6 +91,24 @@
 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd"
   unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd)
 
+lemma ZN_atMost [transfer_rule]:
+  "(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost"
+  unfolding fun_rel_def ZN_def set_rel_def
+  by (clarsimp simp add: Bex_def, arith)
+
+lemma ZN_atLeastAtMost [transfer_rule]:
+  "(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost"
+  unfolding fun_rel_def ZN_def set_rel_def
+  by (clarsimp simp add: Bex_def, arith)
+
+lemma ZN_setsum [transfer_rule]:
+  "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum"
+  apply (intro fun_relI)
+  apply (erule (1) bi_unique_set_rel_lemma)
+  apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def)
+  apply (rule setsum_cong2, simp)
+  done
+
 text {* For derived operations, we can use the @{text "transfer_prover"}
   method to help generate transfer rules. *}