# HG changeset patch
# User haftmann
# Date 1252588988 -7200
# Node ID c2544c7b06117bae86df5b6f2c821a00d48548b2
# Parent  73151030615f9a5d77e01d13400c779f11f1de9b
split of test examples from NatTransfer

diff -r 73151030615f -r c2544c7b0611 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Sep 10 15:23:08 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Sep 10 15:23:08 2009 +0200
@@ -60,6 +60,7 @@
   "BinEx",
   "Sqrt",
   "Sqrt_Script",
+  "Transfer_ex",
   "Arithmetic_Series_Complex",
   "HarmonicSeries",
   "Refute_Examples",
diff -r 73151030615f -r c2544c7b0611 src/HOL/ex/Transfer_Ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Ex.thy	Thu Sep 10 15:23:08 2009 +0200
@@ -0,0 +1,42 @@
+
+header {* Various examples for transfer procedure *}
+
+theory Transfer_Ex
+imports Complex_Main
+begin
+
+(* nat to int *)
+
+lemma ex1: "(x::nat) + y = y + x"
+  by auto
+
+thm ex1 [transferred]
+
+lemma ex2: "(a::nat) div b * b + a mod b = a"
+  by (rule mod_div_equality)
+
+thm ex2 [transferred]
+
+lemma ex3: "ALL (x::nat). ALL y. EX z. z >= x + y"
+  by auto
+
+thm ex3 [transferred natint]
+
+lemma ex4: "(x::nat) >= y \<Longrightarrow> (x - y) + y = x"
+  by auto
+
+thm ex4 [transferred]
+
+lemma ex5: "(2::nat) * (SUM i <= n. i) = n * (n + 1)"
+  by (induct n rule: nat_induct, auto)
+
+thm ex5 [transferred]
+
+theorem ex6: "0 <= (n::int) \<Longrightarrow> 2 * \<Sum>{0..n} = n * (n + 1)"
+  by (rule ex5 [transferred])
+
+thm ex6 [transferred]
+
+thm ex5 [transferred, transferred]
+
+end
\ No newline at end of file