--- a/src/HOL/Fact.thy Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Fact.thy Fri Sep 11 09:05:26 2009 +0200
@@ -8,7 +8,7 @@
header{*Factorial Function*}
theory Fact
-imports NatTransfer
+imports Nat_Transfer
begin
class fact =
--- a/src/HOL/Fun.thy Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Fun.thy Fri Sep 11 09:05:26 2009 +0200
@@ -7,6 +7,7 @@
theory Fun
imports Complete_Lattice
+uses ("Tools/transfer.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -568,6 +569,16 @@
*}
+subsection {* Generic transfer procedure *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
subsection {* Code generator setup *}
types_code
--- a/src/HOL/IntDiv.thy Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/IntDiv.thy Fri Sep 11 09:05:26 2009 +0200
@@ -1102,20 +1102,6 @@
thus ?thesis by simp
qed
-
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-apply (simp split add: split_nat)
-apply (rule iffI)
-apply (erule exE)
-apply (rule_tac x = "int x" in exI)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "nat x" in exI)
-apply (erule conjE)
-apply (erule_tac x = "nat x" in allE)
-apply simp
-done
-
theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
proof -
have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
--- a/src/HOL/IsaMakefile Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 11 09:05:26 2009 +0200
@@ -291,7 +291,7 @@
Log.thy \
Lubs.thy \
MacLaurin.thy \
- NatTransfer.thy \
+ Nat_Transfer.thy \
NthRoot.thy \
SEQ.thy \
Series.thy \
@@ -306,7 +306,7 @@
Real.thy \
RealVector.thy \
Tools/float_syntax.ML \
- Tools/transfer_data.ML \
+ Tools/transfer.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
Tools/Qelim/langford_data.ML \
@@ -901,7 +901,7 @@
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
ex/Sudoku.thy ex/Tarski.thy \
- ex/Termination.thy ex/Unification.thy ex/document/root.bib \
+ ex/Termination.thy ex/Transfer_Ex.thy ex/Unification.thy ex/document/root.bib \
ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/NatTransfer.thy Thu Sep 10 16:16:18 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,537 +0,0 @@
-(* Title: HOL/Library/NatTransfer.thy
- Authors: Jeremy Avigad and Amine Chaieb
-
- Sets up transfer from nats to ints and
- back.
-*)
-
-
-header {* NatTransfer *}
-
-theory NatTransfer
-imports Main Parity
-uses ("Tools/transfer_data.ML")
-begin
-
-subsection {* A transfer Method between isomorphic domains*}
-
-definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
- where "TransferMorphism a B = True"
-
-use "Tools/transfer_data.ML"
-
-setup TransferData.setup
-
-
-subsection {* Set up transfer from nat to int *}
-
-(* set up transfer direction *)
-
-lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
- by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_nat_int[transfer
- add mode: manual
- return: nat_0_le
- labels: natint
-]
-
-(* basic functions and relations *)
-
-lemma transfer_nat_int_numerals:
- "(0::nat) = nat 0"
- "(1::nat) = nat 1"
- "(2::nat) = nat 2"
- "(3::nat) = nat 3"
- by auto
-
-definition
- tsub :: "int \<Rightarrow> int \<Rightarrow> int"
-where
- "tsub x y = (if x >= y then x - y else 0)"
-
-lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
- by (simp add: tsub_def)
-
-
-lemma transfer_nat_int_functions:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
- "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
- by (auto simp add: eq_nat_nat_iff nat_mult_distrib
- nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
-
-lemma transfer_nat_int_function_closures:
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
- "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
- "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
- "(0::int) >= 0"
- "(1::int) >= 0"
- "(2::int) >= 0"
- "(3::int) >= 0"
- "int z >= 0"
- apply (auto simp add: zero_le_mult_iff tsub_def)
- apply (case_tac "y = 0")
- apply auto
- apply (subst pos_imp_zdiv_nonneg_iff, auto)
- apply (case_tac "y = 0")
- apply force
- apply (rule pos_mod_sign)
- apply arith
-done
-
-lemma transfer_nat_int_relations:
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) = nat y) = (x = y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) < nat y) = (x < y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) <= nat y) = (x <= y)"
- "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
- (nat (x::int) dvd nat y) = (x dvd y)"
- by (auto simp add: zdvd_int even_nat_def)
-
-declare TransferMorphism_nat_int[transfer add return:
- transfer_nat_int_numerals
- transfer_nat_int_functions
- transfer_nat_int_function_closures
- transfer_nat_int_relations
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_nat_int_quantifiers:
- "(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 TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_quantifiers
- cong: all_cong ex_cong]
-
-
-(* if *)
-
-lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
- nat (if P then x else y)"
- by auto
-
-declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
-
-
-(* operations with sets *)
-
-definition
- nat_set :: "int set \<Rightarrow> bool"
-where
- "nat_set S = (ALL x:S. x >= 0)"
-
-lemma transfer_nat_int_set_functions:
- "card A = card (int ` A)"
- "{} = nat ` ({}::int set)"
- "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)}"
- "{..n} = nat ` {0..int n}"
- "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
- 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
- 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:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "x >= 0 \<Longrightarrow> nat_set {x..y}"
- "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? *)
- unfolding nat_set_def apply auto
-done
-
-lemma transfer_nat_int_set_relations:
- "(finite A) = (finite (int ` A))"
- "(x : A) = (int x : int ` A)"
- "(A = B) = (int ` A = int ` B)"
- "(A < B) = (int ` A < int ` B)"
- "(A <= B) = (int ` A <= int ` B)"
-
- apply (rule iffI)
- apply (erule finite_imageI)
- apply (erule finite_imageD)
- apply (auto simp add: image_def expand_set_eq inj_on_def)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
- apply (drule_tac x = "int x" in spec, auto)
-done
-
-lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
- (int ` nat ` A = A)"
- by (auto simp add: nat_set_def image_def)
-
-lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
- {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
- by auto
-
-declare TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_set_functions
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed
- cong: transfer_nat_int_set_cong
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is nat *)
-lemma transfer_nat_int_sum_prod:
- "setsum f A = setsum (%x. f (nat x)) (int ` A)"
- "setprod f A = setprod (%x. f (nat x)) (int ` A)"
- apply (subst setsum_reindex)
- apply (unfold inj_on_def, auto)
- apply (subst setprod_reindex)
- apply (unfold inj_on_def o_def, auto)
-done
-
-(* this handles the case where the *range* of f is nat *)
-lemma transfer_nat_int_sum_prod2:
- "setsum f A = nat(setsum (%x. int (f x)) A)"
- "setprod f A = nat(setprod (%x. int (f x)) A)"
- apply (subst int_setsum [symmetric])
- apply auto
- apply (subst int_setprod [symmetric])
- apply auto
-done
-
-lemma transfer_nat_int_sum_prod_closure:
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
- "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
- unfolding nat_set_def
- apply (rule setsum_nonneg)
- apply auto
- apply (rule setprod_nonneg)
- apply auto
-done
-
-(* this version doesn't work, even with nat_set A \<Longrightarrow>
- x : A \<Longrightarrow> x >= 0 turned on. Why not?
-
- also: what does =simp=> do?
-
-lemma transfer_nat_int_sum_prod_closure:
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
- "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
- unfolding nat_set_def simp_implies_def
- apply (rule setsum_nonneg)
- apply auto
- apply (rule setprod_nonneg)
- apply auto
-done
-*)
-
-(* Making A = B in this lemma doesn't work. Why not?
- Also, why aren't setsum_cong and setprod_cong enough,
- with the previously mentioned rule turned on? *)
-
-lemma transfer_nat_int_sum_prod_cong:
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- setsum f A = setsum g B"
- "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
- setprod f A = setprod g B"
- unfolding nat_set_def
- apply (subst setsum_cong, assumption)
- apply auto [2]
- apply (subst setprod_cong, assumption, auto)
-done
-
-declare TransferMorphism_nat_int[transfer add
- return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
- transfer_nat_int_sum_prod_closure
- cong: transfer_nat_int_sum_prod_cong]
-
-(* lists *)
-
-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";
-
-thm nat_0_le;
-
-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 {* Set up transfer from int to nat *}
-
-(* set up transfer direction *)
-
-lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
- by (simp add: TransferMorphism_def)
-
-declare TransferMorphism_int_nat[transfer add
- mode: manual
-(* labels: int-nat *)
- return: nat_int
-]
-
-
-(* basic functions and relations *)
-
-definition
- is_nat :: "int \<Rightarrow> bool"
-where
- "is_nat x = (x >= 0)"
-
-lemma transfer_int_nat_numerals:
- "0 = int 0"
- "1 = int 1"
- "2 = int 2"
- "3 = int 3"
- by auto
-
-lemma transfer_int_nat_functions:
- "(int x) + (int y) = int (x + y)"
- "(int x) * (int y) = int (x * y)"
- "tsub (int x) (int y) = int (x - y)"
- "(int x)^n = int (x^n)"
- "(int x) div (int y) = int (x div y)"
- "(int x) mod (int y) = int (x mod y)"
- by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
-
-lemma transfer_int_nat_function_closures:
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
- "is_nat x \<Longrightarrow> is_nat (x^n)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
- "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
- "is_nat 0"
- "is_nat 1"
- "is_nat 2"
- "is_nat 3"
- "is_nat (int z)"
- by (simp_all only: is_nat_def transfer_nat_int_function_closures)
-
-lemma transfer_int_nat_relations:
- "(int x = int y) = (x = y)"
- "(int x < int y) = (x < y)"
- "(int x <= int y) = (x <= y)"
- "(int x dvd int y) = (x dvd y)"
- "(even (int x)) = (even x)"
- by (auto simp add: zdvd_int even_nat_def)
-
-lemma UNIV_apply:
- "UNIV x = True"
- by (simp add: top_fun_eq top_bool_eq)
-
-declare TransferMorphism_int_nat[transfer add return:
- transfer_int_nat_numerals
- transfer_int_nat_functions
- transfer_int_nat_function_closures
- transfer_int_nat_relations
- UNIV_apply
-]
-
-
-(* first-order quantifiers *)
-
-lemma transfer_int_nat_quantifiers:
- "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
- "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
- apply (subst all_nat)
- apply auto [1]
- apply (subst ex_nat)
- apply auto
-done
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_quantifiers]
-
-
-(* if *)
-
-lemma int_if_cong: "(if P then (int x) else (int y)) =
- int (if P then x else y)"
- by auto
-
-declare TransferMorphism_int_nat [transfer add return: int_if_cong]
-
-
-
-(* operations with sets *)
-
-lemma transfer_int_nat_set_functions:
- "nat_set A \<Longrightarrow> card A = card (nat ` A)"
- "{} = int ` ({}::nat set)"
- "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
- transfer_nat_int_set_return_embed nat_0_le
- cong: transfer_nat_int_set_cong)
-
-lemma transfer_int_nat_set_function_closures:
- "nat_set {}"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
- "is_nat x \<Longrightarrow> nat_set {x..y}"
- "nat_set {x. x >= 0 & P x}"
- "nat_set (int ` C)"
- "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
- by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
-
-lemma transfer_int_nat_set_relations:
- "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
- "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
- "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
- by (simp_all only: is_nat_def transfer_nat_int_set_relations
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
- by (simp only: transfer_nat_int_set_relations
- transfer_nat_int_set_function_closures
- transfer_nat_int_set_return_embed nat_0_le)
-
-lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
- {(x::nat). P x} = {x. P' x}"
- by auto
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_set_functions
- transfer_int_nat_set_function_closures
- transfer_int_nat_set_relations
- transfer_int_nat_set_return_embed
- cong: transfer_int_nat_set_cong
-]
-
-
-(* setsum and setprod *)
-
-(* this handles the case where the *domain* of f is int *)
-lemma transfer_int_nat_sum_prod:
- "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
- "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
- apply (subst setsum_reindex)
- apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
- apply (subst setprod_reindex)
- apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
- cong: setprod_cong)
-done
-
-(* this handles the case where the *range* of f is int *)
-lemma transfer_int_nat_sum_prod2:
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
- "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
- setprod f A = int(setprod (%x. nat (f x)) A)"
- unfolding is_nat_def
- apply (subst int_setsum, auto)
- apply (subst int_setprod, auto simp add: cong: setprod_cong)
-done
-
-declare TransferMorphism_int_nat[transfer add
- return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
- cong: setsum_cong setprod_cong]
-
-
-subsection {* Test it out *}
-
-(* 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nat_Transfer.thy Fri Sep 11 09:05:26 2009 +0200
@@ -0,0 +1,484 @@
+
+(* Authors: Jeremy Avigad and Amine Chaieb *)
+
+header {* Sets up transfer from nats to ints and back. *}
+
+theory Nat_Transfer
+imports Main Parity
+begin
+
+subsection {* Set up transfer from nat to int *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
+ by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_nat_int[transfer
+ add mode: manual
+ return: nat_0_le
+ labels: natint
+]
+
+(* basic functions and relations *)
+
+lemma transfer_nat_int_numerals:
+ "(0::nat) = nat 0"
+ "(1::nat) = nat 1"
+ "(2::nat) = nat 2"
+ "(3::nat) = nat 3"
+ by auto
+
+definition
+ tsub :: "int \<Rightarrow> int \<Rightarrow> int"
+where
+ "tsub x y = (if x >= y then x - y else 0)"
+
+lemma tsub_eq: "x >= y \<Longrightarrow> tsub x y = x - y"
+ by (simp add: tsub_def)
+
+
+lemma transfer_nat_int_functions:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) + (nat y) = nat (x + y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
+ "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
+ by (auto simp add: eq_nat_nat_iff nat_mult_distrib
+ nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
+
+lemma transfer_nat_int_function_closures:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+ "(0::int) >= 0"
+ "(1::int) >= 0"
+ "(2::int) >= 0"
+ "(3::int) >= 0"
+ "int z >= 0"
+ apply (auto simp add: zero_le_mult_iff tsub_def)
+ apply (case_tac "y = 0")
+ apply auto
+ apply (subst pos_imp_zdiv_nonneg_iff, auto)
+ apply (case_tac "y = 0")
+ apply force
+ apply (rule pos_mod_sign)
+ apply arith
+done
+
+lemma transfer_nat_int_relations:
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) = nat y) = (x = y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) < nat y) = (x < y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) <= nat y) = (x <= y)"
+ "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow>
+ (nat (x::int) dvd nat y) = (x dvd y)"
+ by (auto simp add: zdvd_int)
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_numerals
+ transfer_nat_int_functions
+ transfer_nat_int_function_closures
+ transfer_nat_int_relations
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_nat_int_quantifiers:
+ "(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 TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_quantifiers
+ cong: all_cong ex_cong]
+
+
+(* if *)
+
+lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
+ nat (if P then x else y)"
+ by auto
+
+declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
+
+
+(* operations with sets *)
+
+definition
+ nat_set :: "int set \<Rightarrow> bool"
+where
+ "nat_set S = (ALL x:S. x >= 0)"
+
+lemma transfer_nat_int_set_functions:
+ "card A = card (int ` A)"
+ "{} = nat ` ({}::int set)"
+ "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)}"
+ "{..n} = nat ` {0..int n}"
+ "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
+ 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
+ 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:
+ "nat_set {}"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+ "x >= 0 \<Longrightarrow> nat_set {x..y}"
+ "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? *)
+ unfolding nat_set_def apply auto
+done
+
+lemma transfer_nat_int_set_relations:
+ "(finite A) = (finite (int ` A))"
+ "(x : A) = (int x : int ` A)"
+ "(A = B) = (int ` A = int ` B)"
+ "(A < B) = (int ` A < int ` B)"
+ "(A <= B) = (int ` A <= int ` B)"
+
+ apply (rule iffI)
+ apply (erule finite_imageI)
+ apply (erule finite_imageD)
+ apply (auto simp add: image_def expand_set_eq inj_on_def)
+ apply (drule_tac x = "int x" in spec, auto)
+ apply (drule_tac x = "int x" in spec, auto)
+ apply (drule_tac x = "int x" in spec, auto)
+done
+
+lemma transfer_nat_int_set_return_embed: "nat_set A \<Longrightarrow>
+ (int ` nat ` A = A)"
+ by (auto simp add: nat_set_def image_def)
+
+lemma transfer_nat_int_set_cong: "(!!x. x >= 0 \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ {(x::int). x >= 0 & P x} = {x. x >= 0 & P' x}"
+ by auto
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_set_functions
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_relations
+ transfer_nat_int_set_return_embed
+ cong: transfer_nat_int_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is nat *)
+lemma transfer_nat_int_sum_prod:
+ "setsum f A = setsum (%x. f (nat x)) (int ` A)"
+ "setprod f A = setprod (%x. f (nat x)) (int ` A)"
+ apply (subst setsum_reindex)
+ apply (unfold inj_on_def, auto)
+ apply (subst setprod_reindex)
+ apply (unfold inj_on_def o_def, auto)
+done
+
+(* this handles the case where the *range* of f is nat *)
+lemma transfer_nat_int_sum_prod2:
+ "setsum f A = nat(setsum (%x. int (f x)) A)"
+ "setprod f A = nat(setprod (%x. int (f x)) A)"
+ apply (subst int_setsum [symmetric])
+ apply auto
+ apply (subst int_setprod [symmetric])
+ apply auto
+done
+
+lemma transfer_nat_int_sum_prod_closure:
+ "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+ "nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ unfolding nat_set_def
+ apply (rule setsum_nonneg)
+ apply auto
+ apply (rule setprod_nonneg)
+ apply auto
+done
+
+(* this version doesn't work, even with nat_set A \<Longrightarrow>
+ x : A \<Longrightarrow> x >= 0 turned on. Why not?
+
+ also: what does =simp=> do?
+
+lemma transfer_nat_int_sum_prod_closure:
+ "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
+ "(!!x. x : A ==> f x >= (0::int)) \<Longrightarrow> setprod f A >= 0"
+ unfolding nat_set_def simp_implies_def
+ apply (rule setsum_nonneg)
+ apply auto
+ apply (rule setprod_nonneg)
+ apply auto
+done
+*)
+
+(* Making A = B in this lemma doesn't work. Why not?
+ Also, why aren't setsum_cong and setprod_cong enough,
+ with the previously mentioned rule turned on? *)
+
+lemma transfer_nat_int_sum_prod_cong:
+ "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setsum f A = setsum g B"
+ "A = B \<Longrightarrow> nat_set B \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setprod f A = setprod g B"
+ unfolding nat_set_def
+ apply (subst setsum_cong, assumption)
+ apply auto [2]
+ apply (subst setprod_cong, assumption, auto)
+done
+
+declare TransferMorphism_nat_int[transfer add
+ return: transfer_nat_int_sum_prod transfer_nat_int_sum_prod2
+ transfer_nat_int_sum_prod_closure
+ cong: transfer_nat_int_sum_prod_cong]
+
+(* lists *)
+
+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";
+
+thm nat_0_le;
+
+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 {* Set up transfer from int to nat *}
+
+(* set up transfer direction *)
+
+lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
+ by (simp add: TransferMorphism_def)
+
+declare TransferMorphism_int_nat[transfer add
+ mode: manual
+(* labels: int-nat *)
+ return: nat_int
+]
+
+
+(* basic functions and relations *)
+
+definition
+ is_nat :: "int \<Rightarrow> bool"
+where
+ "is_nat x = (x >= 0)"
+
+lemma transfer_int_nat_numerals:
+ "0 = int 0"
+ "1 = int 1"
+ "2 = int 2"
+ "3 = int 3"
+ by auto
+
+lemma transfer_int_nat_functions:
+ "(int x) + (int y) = int (x + y)"
+ "(int x) * (int y) = int (x * y)"
+ "tsub (int x) (int y) = int (x - y)"
+ "(int x)^n = int (x^n)"
+ "(int x) div (int y) = int (x div y)"
+ "(int x) mod (int y) = int (x mod y)"
+ by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
+
+lemma transfer_int_nat_function_closures:
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
+ "is_nat x \<Longrightarrow> is_nat (x^n)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
+ "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
+ "is_nat 0"
+ "is_nat 1"
+ "is_nat 2"
+ "is_nat 3"
+ "is_nat (int z)"
+ by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+lemma transfer_int_nat_relations:
+ "(int x = int y) = (x = y)"
+ "(int x < int y) = (x < y)"
+ "(int x <= int y) = (x <= y)"
+ "(int x dvd int y) = (x dvd y)"
+ "(even (int x)) = (even x)"
+ by (auto simp add: zdvd_int even_nat_def)
+
+lemma UNIV_apply:
+ "UNIV x = True"
+ by (simp add: top_fun_eq top_bool_eq)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_numerals
+ transfer_int_nat_functions
+ transfer_int_nat_function_closures
+ transfer_int_nat_relations
+ UNIV_apply
+]
+
+
+(* first-order quantifiers *)
+
+lemma transfer_int_nat_quantifiers:
+ "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
+ "(EX (x::int) >= 0. P x) = (EX (x::nat). P (int x))"
+ apply (subst all_nat)
+ apply auto [1]
+ apply (subst ex_nat)
+ apply auto
+done
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_quantifiers]
+
+
+(* if *)
+
+lemma int_if_cong: "(if P then (int x) else (int y)) =
+ int (if P then x else y)"
+ by auto
+
+declare TransferMorphism_int_nat [transfer add return: int_if_cong]
+
+
+
+(* operations with sets *)
+
+lemma transfer_int_nat_set_functions:
+ "nat_set A \<Longrightarrow> card A = card (nat ` A)"
+ "{} = int ` ({}::nat set)"
+ "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
+ transfer_nat_int_set_return_embed nat_0_le
+ cong: transfer_nat_int_set_cong)
+
+lemma transfer_int_nat_set_function_closures:
+ "nat_set {}"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
+ "is_nat x \<Longrightarrow> nat_set {x..y}"
+ "nat_set {x. x >= 0 & P x}"
+ "nat_set (int ` C)"
+ "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
+ by (simp_all only: transfer_nat_int_set_function_closures is_nat_def)
+
+lemma transfer_int_nat_set_relations:
+ "nat_set A \<Longrightarrow> finite A = finite (nat ` A)"
+ "is_nat x \<Longrightarrow> nat_set A \<Longrightarrow> (x : A) = (nat x : nat ` A)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A = B) = (nat ` A = nat ` B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A < B) = (nat ` A < nat ` B)"
+ "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> (A <= B) = (nat ` A <= nat ` B)"
+ by (simp_all only: is_nat_def transfer_nat_int_set_relations
+ transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_return_embed: "nat ` int ` A = A"
+ by (simp only: transfer_nat_int_set_relations
+ transfer_nat_int_set_function_closures
+ transfer_nat_int_set_return_embed nat_0_le)
+
+lemma transfer_int_nat_set_cong: "(!!x. P x = P' x) \<Longrightarrow>
+ {(x::nat). P x} = {x. P' x}"
+ by auto
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_set_functions
+ transfer_int_nat_set_function_closures
+ transfer_int_nat_set_relations
+ transfer_int_nat_set_return_embed
+ cong: transfer_int_nat_set_cong
+]
+
+
+(* setsum and setprod *)
+
+(* this handles the case where the *domain* of f is int *)
+lemma transfer_int_nat_sum_prod:
+ "nat_set A \<Longrightarrow> setsum f A = setsum (%x. f (int x)) (nat ` A)"
+ "nat_set A \<Longrightarrow> setprod f A = setprod (%x. f (int x)) (nat ` A)"
+ apply (subst setsum_reindex)
+ apply (unfold inj_on_def nat_set_def, auto simp add: eq_nat_nat_iff)
+ apply (subst setprod_reindex)
+ apply (unfold inj_on_def nat_set_def o_def, auto simp add: eq_nat_nat_iff
+ cong: setprod_cong)
+done
+
+(* this handles the case where the *range* of f is int *)
+lemma transfer_int_nat_sum_prod2:
+ "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow> setsum f A = int(setsum (%x. nat (f x)) A)"
+ "(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
+ setprod f A = int(setprod (%x. nat (f x)) A)"
+ unfolding is_nat_def
+ apply (subst int_setsum, auto)
+ apply (subst int_setprod, auto simp add: cong: setprod_cong)
+done
+
+declare TransferMorphism_int_nat[transfer add
+ return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
+ cong: setsum_cong setprod_cong]
+
+end
--- a/src/HOL/Presburger.thy Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/Presburger.thy Fri Sep 11 09:05:26 2009 +0200
@@ -382,15 +382,22 @@
lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
by simp_all
+
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
-lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
by (simp split add: split_nat)
-lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
- apply (auto split add: split_nat)
- apply (rule_tac x="int x" in exI, simp)
- apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
- done
+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 zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/transfer.ML Fri Sep 11 09:05:26 2009 +0200
@@ -0,0 +1,241 @@
+(* Author: Amine Chaieb, University of Cambridge, 2009
+ Jeremy Avigad, Carnegie Mellon University
+*)
+
+signature TRANSFER =
+sig
+ type data
+ type entry
+ val get: Proof.context -> data
+ val del: attribute
+ val setup: theory -> theory
+end;
+
+structure Transfer : TRANSFER =
+struct
+
+val eq_thm = Thm.eq_thm;
+
+type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
+ guess : bool, hints : string list};
+type data = simpset * (thm * entry) list;
+
+structure Data = GenericDataFun
+(
+ type T = data;
+ val empty = (HOL_ss, []);
+ val extend = I;
+ fun merge _ ((ss1, e1), (ss2, e2)) =
+ (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
+);
+
+val get = Data.get o Context.Proof;
+
+fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
+
+val del = Thm.declaration_attribute (Data.map o del_data);
+val add_ss = Thm.declaration_attribute
+ (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
+
+val del_ss = Thm.declaration_attribute
+ (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
+
+val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
+
+fun merge_update eq m (k,v) [] = [(k,v)]
+ | merge_update eq m (k,v) ((k',v')::al) =
+ if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
+
+fun C f x y = f y x
+
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
+ HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
+
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
+ let
+ val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
+ val (aT,bT) =
+ let val T = typ_of (ctyp_of_term a)
+ in (Term.range_type T, Term.domain_type T)
+ end
+ val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
+ val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
+ val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
+ val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
+ val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
+ val cis = map (Thm.capply a) cfis
+ val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
+ val th1 = Drule.cterm_instantiate (cns~~ cis) th
+ val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
+ val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
+ (fold_rev implies_intr (map cprop_of hs) th2)
+in hd (Variable.export ctxt''' ctxt0 [th3]) end;
+
+local
+fun transfer_ruleh a D leave ctxt th =
+ let val (ss,al) = get ctxt
+ val a0 = cterm_of (ProofContext.theory_of ctxt) a
+ val D0 = cterm_of (ProofContext.theory_of ctxt) D
+ fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
+ in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
+ end
+ in case get_first h al of
+ SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
+ | NONE => error "Transfer: corresponding instance not found in context-data"
+ end
+in fun transfer_rule (a,D) leave (gctxt,th) =
+ (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
+end;
+
+fun splits P [] = []
+ | splits P (xxs as (x::xs)) =
+ let val pss = filter (P x) xxs
+ val qss = filter_out (P x) xxs
+ in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
+ end
+
+fun all_transfers leave (gctxt,th) =
+ let
+ val ctxt = Context.proof_of gctxt
+ val tys = map snd (Term.add_vars (prop_of th) [])
+ val _ = if null tys then error "transfer: Unable to guess instance" else ()
+ val tyss = splits (curry Type.could_unify) tys
+ val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
+ val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+ val insts =
+ map_filter (fn tys =>
+ get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k))
+ then SOME (get_aD k, ss)
+ else NONE) (snd (get ctxt))) tyss
+ val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+ val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+ val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+fun transfer_rule_by_hint ls leave (gctxt,th) =
+ let
+ val ctxt = Context.proof_of gctxt
+ val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
+ val insts =
+ map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls
+ then SOME (get_aD k, e) else NONE)
+ (snd (get ctxt))
+ val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
+ val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
+ val cth = Conjunction.intr_balanced ths
+ in (gctxt, cth)
+ end;
+
+
+fun transferred_attribute ls NONE leave =
+ if null ls then all_transfers leave else transfer_rule_by_hint ls leave
+ | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
+
+ (* Add data to the context *)
+fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
+ ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
+ =
+ let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
+ ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
+ hints = subtract (op = : string*string -> bool) hints0
+ (hints1 union_string hints2)}
+ end;
+
+local
+ val h = curry (merge Thm.eq_thm)
+in
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
+ {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
+end;
+
+fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
+ Thm.declaration_attribute (fn key => fn context => context |> Data.map
+ (fn (ss, al) =>
+ let
+ val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key)
+ in 0 end)
+ handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+ val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
+ val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
+ val entry =
+ if g then
+ let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
+ val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
+ val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
+ else inja
+ val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
+ in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
+ else e0
+ in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
+ end));
+
+
+
+(* concrete syntax *)
+
+local
+
+fun keyword k = Scan.lift (Args.$$$ k) >> K ()
+fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+
+val congN = "cong"
+val injN = "inj"
+val embedN = "embed"
+val returnN = "return"
+val addN = "add"
+val delN = "del"
+val modeN = "mode"
+val automaticN = "automatic"
+val manualN = "manual"
+val directionN = "direction"
+val labelsN = "labels"
+val leavingN = "leaving"
+
+val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
+
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
+val terms = thms >> map Drule.dest_term
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
+val name = Scan.lift Args.name
+val names = Scan.repeat (Scan.unless any_keyword name)
+fun optional scan = Scan.optional scan []
+fun optional2 scan = Scan.optional scan ([],[])
+
+val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
+val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
+val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
+val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
+val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
+val addscan = Scan.unless any_keyword (keyword addN)
+val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
+val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
+
+val transf_add = addscan |-- entry
+in
+
+val install_att_syntax =
+ (Scan.lift (Args.$$$ delN >> K del) ||
+ transf_add
+ >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
+
+val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
+ -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
+
+end;
+
+
+(* theory setup *)
+
+val setup =
+ Attrib.setup @{binding transfer} install_att_syntax
+ "Installs transfer data" #>
+ Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
+ "simp rules for transfer" #>
+ Attrib.setup @{binding transferred} transferred_att_syntax
+ "Transfers theorems";
+
+end;
--- a/src/HOL/Tools/transfer_data.ML Thu Sep 10 16:16:18 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,243 +0,0 @@
-(* Title: Tools/transfer.ML
- Author: Amine Chaieb, University of Cambridge, 2009
- Jeremy Avigad, Carnegie Mellon University
-*)
-
-signature TRANSFER_DATA =
-sig
- type data
- type entry
- val get: Proof.context -> data
- val del: attribute
- val add: attribute
- val setup: theory -> theory
-end;
-
-structure TransferData (* : TRANSFER_DATA*) =
-struct
-type entry = {inj : thm list , emb : thm list , ret : thm list , cong : thm list, guess : bool, hints : string list};
-type data = simpset * (thm * entry) list;
-
-val eq_key = Thm.eq_thm;
-fun eq_data arg = eq_fst eq_key arg;
-
-structure Data = GenericDataFun
-(
- type T = data;
- val empty = (HOL_ss, []);
- val extend = I;
- fun merge _ ((ss, e), (ss', e')) =
- (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
-);
-
-val get = Data.get o Context.Proof;
-
-fun del_data key = apsnd (remove eq_data (key, []));
-
-val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-
-val del_ss = Thm.declaration_attribute
- (fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
-
-val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
-
-fun merge_update eq m (k,v) [] = [(k,v)]
- | merge_update eq m (k,v) ((k',v')::al) =
- if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
-
-fun C f x y = f y x
-
-fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
- HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
-
-fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
- let
- val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
- val (aT,bT) =
- let val T = typ_of (ctyp_of_term a)
- in (Term.range_type T, Term.domain_type T)
- end
- val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
- val ns = filter (fn i => Type.could_unify (snd i, aT) andalso not (fst (fst i) mem_string leave)) (Term.add_vars (prop_of th) [])
- val (ins, ctxt'') = Variable.variant_fixes (map (fst o fst) ns) ctxt'
- val cns = map ((cterm_of o ProofContext.theory_of) ctxt'' o Var) ns
- val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
- val cis = map (Thm.capply a) cfis
- val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
- val th1 = Drule.cterm_instantiate (cns~~ cis) th
- val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
- val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
- (fold_rev implies_intr (map cprop_of hs) th2)
-in hd (Variable.export ctxt''' ctxt0 [th3]) end;
-
-local
-fun transfer_ruleh a D leave ctxt th =
- let val (ss,al) = get ctxt
- val a0 = cterm_of (ProofContext.theory_of ctxt) a
- val D0 = cterm_of (ProofContext.theory_of ctxt) D
- fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
- in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
- end
- in case get_first h al of
- SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
- | NONE => error "Transfer: corresponding instance not found in context-data"
- end
-in fun transfer_rule (a,D) leave (gctxt,th) =
- (gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
-end;
-
-fun splits P [] = []
- | splits P (xxs as (x::xs)) =
- let val pss = filter (P x) xxs
- val qss = filter_out (P x) xxs
- in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
- end
-
-fun all_transfers leave (gctxt,th) =
- let
- val ctxt = Context.proof_of gctxt
- val tys = map snd (Term.add_vars (prop_of th) [])
- val _ = if null tys then error "transfer: Unable to guess instance" else ()
- val tyss = splits (curry Type.could_unify) tys
- val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
- val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn tys =>
- get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k))
- then SOME (get_aD k, ss)
- else NONE) (snd (get ctxt))) tyss
- val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
- val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
- val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-fun transfer_rule_by_hint ls leave (gctxt,th) =
- let
- val ctxt = Context.proof_of gctxt
- val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls
- then SOME (get_aD k, e) else NONE)
- (snd (get ctxt))
- val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
- val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
- val cth = Conjunction.intr_balanced ths
- in (gctxt, cth)
- end;
-
-
-fun transferred_attribute ls NONE leave =
- if null ls then all_transfers leave else transfer_rule_by_hint ls leave
- | transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
-
- (* Add data to the context *)
-fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
- ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
- =
- let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
- ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
- hints = subtract (op = : string*string -> bool) hints0
- (hints1 union_string hints2)}
- end;
-
-local
- val h = curry (merge Thm.eq_thm)
-in
-fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
- {inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
-end;
-
-fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
- Thm.declaration_attribute (fn key => fn context => context |> Data.map
- (fn (ss, al) =>
- let
- val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key)
- in 0 end)
- handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
- val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
- val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
- val entry =
- if g then
- let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
- val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
- val inj' = if null inja then #inj (case AList.lookup eq_key al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
- else inja
- val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
- in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
- else e0
- in (ss, merge_update eq_key (gen_merge_entries ed) (key, entry) al)
- end));
-
-
-
-(* concrete syntax *)
-
-local
-
-fun keyword k = Scan.lift (Args.$$$ k) >> K ()
-fun keywordC k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-
-val congN = "cong"
-val injN = "inj"
-val embedN = "embed"
-val returnN = "return"
-val addN = "add"
-val delN = "del"
-val modeN = "mode"
-val automaticN = "automatic"
-val manualN = "manual"
-val directionN = "direction"
-val labelsN = "labels"
-val leavingN = "leaving"
-
-val any_keyword = keywordC congN || keywordC injN || keywordC embedN || keywordC returnN || keywordC directionN || keywordC modeN || keywordC delN || keywordC labelsN || keywordC leavingN
-
-val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
-val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
-val name = Scan.lift Args.name
-val names = Scan.repeat (Scan.unless any_keyword name)
-fun optional scan = Scan.optional scan []
-fun optional2 scan = Scan.optional scan ([],[])
-
-val mode = keywordC modeN |-- ((Scan.lift (Args.$$$ manualN) >> K false) || (Scan.lift (Args.$$$ automaticN) >> K true))
-val inj = (keywordC injN |-- thms) -- optional (keywordC delN |-- thms)
-val embed = (keywordC embedN |-- thms) -- optional (keywordC delN |-- thms)
-val return = (keywordC returnN |-- thms) -- optional (keywordC delN |-- thms)
-val cong = (keywordC congN |-- thms) -- optional (keywordC delN |-- thms)
-val addscan = Scan.unless any_keyword (keyword addN)
-val labels = (keywordC labelsN |-- names) -- optional (keywordC delN |-- names)
-val entry = Scan.optional mode true -- optional2 inj -- optional2 embed -- optional2 return -- optional2 cong -- optional2 labels
-
-val transf_add = addscan |-- entry
-in
-
-val install_att_syntax =
- (Scan.lift (Args.$$$ delN >> K del) ||
- transf_add
- >> (fn (((((g, inj), embed), ret), cg), hints) => add (inj, embed, ret, cg, g, hints)))
-
-val transferred_att_syntax = (optional names -- Scan.option (keywordC directionN |-- (Args.term -- Args.term))
- -- optional (keywordC leavingN |-- names) >> (fn ((hints, aD),leave) => transferred_attribute hints aD leave));
-
-end;
-
-
-(* theory setup *)
-
-
-val setup =
- Attrib.setup @{binding transfer} install_att_syntax
- "Installs transfer data" #>
- Attrib.setup @{binding transfer_simps} (Attrib.add_del add_ss del_ss)
- "simp rules for transfer" #>
- Attrib.setup @{binding transferred} transferred_att_syntax
- "Transfers theorems";
-
-end;
--- a/src/HOL/ex/ROOT.ML Thu Sep 10 16:16:18 2009 +0200
+++ b/src/HOL/ex/ROOT.ML Fri Sep 11 09:05:26 2009 +0200
@@ -60,6 +60,7 @@
"BinEx",
"Sqrt",
"Sqrt_Script",
+ "Transfer_Ex",
"Arithmetic_Series_Complex",
"HarmonicSeries",
"Refute_Examples",
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Transfer_Ex.thy Fri Sep 11 09:05:26 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