--- a/src/HOL/Code_Numeral.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Oct 29 11:41:36 2009 +0100
@@ -3,7 +3,7 @@
header {* Type of target language numerals *}
theory Code_Numeral
-imports Nat_Numeral Divides
+imports Nat_Numeral Nat_Transfer Divides
begin
text {*
--- a/src/HOL/Divides.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Divides.thy Thu Oct 29 11:41:36 2009 +0100
@@ -6,7 +6,7 @@
header {* The division operators div and mod *}
theory Divides
-imports Nat_Numeral
+imports Nat_Numeral Nat_Transfer
uses
"~~/src/Provers/Arith/assoc_fold.ML"
"~~/src/Provers/Arith/cancel_numerals.ML"
--- a/src/HOL/Fun.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Fun.thy Thu Oct 29 11:41:36 2009 +0100
@@ -7,7 +7,6 @@
theory Fun
imports Complete_Lattice
-uses ("Tools/transfer.ML")
begin
text{*As a simplification rule, it replaces all function equalities by
@@ -604,16 +603,6 @@
*}
-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/GCD.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/GCD.thy Thu Oct 29 11:41:36 2009 +0100
@@ -28,7 +28,7 @@
header {* GCD *}
theory GCD
-imports Fact
+imports Fact Parity
begin
declare One_nat_def [simp del]
--- a/src/HOL/IntDiv.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/IntDiv.thy Thu Oct 29 11:41:36 2009 +0100
@@ -1024,139 +1024,16 @@
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
-lemma zdvd_anti_sym:
- "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
- apply (simp add: dvd_def, auto)
- apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
- done
-
-lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
- shows "\<bar>a\<bar> = \<bar>b\<bar>"
-proof-
- from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
- from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
- from k k' have "a = a*k*k'" by simp
- with mult_cancel_left1[where c="a" and b="k*k'"]
- have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
- hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
- thus ?thesis using k k' by auto
-qed
-
-lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
- apply (subgoal_tac "m = n + (m - n)")
- apply (erule ssubst)
- apply (blast intro: dvd_add, simp)
- done
-
-lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
-apply (rule iffI)
- apply (erule_tac [2] dvd_add)
- apply (subgoal_tac "n = (n + k * m) - k * m")
- apply (erule ssubst)
- apply (erule dvd_diff)
- apply(simp_all)
-done
-
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
by (rule dvd_mod) (* TODO: remove *)
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
by (rule dvd_mod_imp_dvd) (* TODO: remove *)
-lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
-apply(auto simp:abs_if)
- apply(clarsimp simp:dvd_def mult_less_0_iff)
- using mult_le_cancel_left_neg[of _ "-1::int"]
- apply(clarsimp simp:dvd_def mult_less_0_iff)
- apply(clarsimp simp:dvd_def mult_less_0_iff
- minus_mult_right simp del: mult_minus_right)
-apply(clarsimp simp:dvd_def mult_less_0_iff)
-done
-
-lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
- apply (auto elim!: dvdE)
- apply (subgoal_tac "0 < n")
- prefer 2
- apply (blast intro: order_less_trans)
- apply (simp add: zero_less_mult_iff)
- done
-
lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
using zmod_zdiv_equality[where a="m" and b="n"]
by (simp add: algebra_simps)
-lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
-apply (subgoal_tac "m mod n = 0")
- apply (simp add: zmult_div_cancel)
-apply (simp only: dvd_eq_mod_eq_0)
-done
-
-lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
- shows "m dvd n"
-proof-
- from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
- {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
- with h have False by (simp add: mult_assoc)}
- hence "n = m * h" by blast
- thus ?thesis by simp
-qed
-
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
-proof -
- have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
- proof -
- fix k
- assume A: "int y = int x * k"
- then show "x dvd y" proof (cases k)
- case (1 n) with A have "y = x * n" by (simp add: zmult_int)
- then show ?thesis ..
- next
- case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
- also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
- also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
- finally have "- int (x * Suc n) = int y" ..
- then show ?thesis by (simp only: negative_eq_positive) auto
- qed
- qed
- then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
-qed
-
-lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
-proof
- assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
- hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
- hence "nat \<bar>x\<bar> = 1" by simp
- thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
-next
- assume "\<bar>x\<bar>=1" thus "x dvd 1"
- by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
-qed
-lemma zdvd_mult_cancel1:
- assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
-proof
- assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
- by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
-next
- assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
- from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
-qed
-
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding zdvd_int by (cases "z \<ge> 0") simp_all
-
-lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
- by (auto simp add: dvd_int_iff)
-
-lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
- apply (rule_tac z=n in int_cases)
- apply (auto simp add: dvd_int_iff)
- apply (rule_tac z=z in int_cases)
- apply (auto simp add: dvd_imp_le)
- done
-
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
apply (induct "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
@@ -1182,6 +1059,12 @@
lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
+lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
+apply (subgoal_tac "m mod n = 0")
+ apply (simp add: zmult_div_cancel)
+apply (simp only: dvd_eq_mod_eq_0)
+done
+
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
"\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
@@ -1349,6 +1232,43 @@
declare dvd_eq_mod_eq_0_number_of [simp]
+subsection {* Transfer setup *}
+
+lemma transfer_nat_int_functions:
+ "(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: nat_div_distrib nat_mod_distrib)
+
+lemma transfer_nat_int_function_closures:
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
+ "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
+ apply (cases "y = 0")
+ apply (auto simp add: pos_imp_zdiv_nonneg_iff)
+ apply (cases "y = 0")
+ apply auto
+done
+
+declare TransferMorphism_nat_int[transfer add return:
+ transfer_nat_int_functions
+ transfer_nat_int_function_closures
+]
+
+lemma transfer_int_nat_functions:
+ "(int x) div (int y) = int (x div y)"
+ "(int x) mod (int y) = int (x mod y)"
+ by (auto simp add: zdiv_int zmod_int)
+
+lemma transfer_int_nat_function_closures:
+ "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)"
+ by (simp_all only: is_nat_def transfer_nat_int_function_closures)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_functions
+ transfer_int_nat_function_closures
+]
+
+
subsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--- a/src/HOL/IsaMakefile Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/IsaMakefile Thu Oct 29 11:41:36 2009 +0100
@@ -223,7 +223,6 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
- Tools/transfer.ML \
Tools/typecopy.ML \
Tools/typedef_codegen.ML \
Tools/typedef.ML \
@@ -255,6 +254,7 @@
Main.thy \
Map.thy \
Nat_Numeral.thy \
+ Nat_Transfer.thy \
Presburger.thy \
Predicate_Compile.thy \
Quickcheck.thy \
@@ -276,6 +276,7 @@
Tools/Groebner_Basis/misc.ML \
Tools/Groebner_Basis/normalizer.ML \
Tools/Groebner_Basis/normalizer_data.ML \
+ Tools/choice_specification.ML \
Tools/int_arith.ML \
Tools/list_code.ML \
Tools/meson.ML \
@@ -299,7 +300,6 @@
Tools/Qelim/presburger.ML \
Tools/Qelim/qelim.ML \
Tools/recdef.ML \
- Tools/choice_specification.ML \
Tools/res_atp.ML \
Tools/res_axioms.ML \
Tools/res_clause.ML \
@@ -307,6 +307,7 @@
Tools/res_reconstruct.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
+ Tools/transfer.ML \
Tools/TFL/casesplit.ML \
Tools/TFL/dcterm.ML \
Tools/TFL/post.ML \
@@ -334,7 +335,6 @@
Log.thy \
Lubs.thy \
MacLaurin.thy \
- Nat_Transfer.thy \
NthRoot.thy \
PReal.thy \
Parity.thy \
--- a/src/HOL/List.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/List.thy Thu Oct 29 11:41:36 2009 +0100
@@ -3587,8 +3587,8 @@
by (blast intro: listrel.intros)
lemma listrel_Cons:
- "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
-by (auto simp add: set_Cons_def intro: listrel.intros)
+ "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
+by (auto simp add: set_Cons_def intro: listrel.intros)
subsection {* Size function *}
@@ -3615,6 +3615,45 @@
by (induct xs) force+
+subsection {* Transfer *}
+
+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 {* Code generator *}
subsubsection {* Setup *}
@@ -4017,5 +4056,4 @@
"list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
by(simp add: all_from_to_int_iff_ball list_ex_iff)
-
end
--- a/src/HOL/Nat_Transfer.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Nat_Transfer.thy Thu Oct 29 11:41:36 2009 +0100
@@ -1,15 +1,26 @@
(* Authors: Jeremy Avigad and Amine Chaieb *)
-header {* Sets up transfer from nats to ints and back. *}
+header {* Generic transfer machinery; specific transfer from nats to ints and back. *}
theory Nat_Transfer
-imports Main Parity
+imports Nat_Numeral
+uses ("Tools/transfer.ML")
begin
+subsection {* Generic transfer machinery *}
+
+definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
+ where "TransferMorphism a B \<longleftrightarrow> True"
+
+use "Tools/transfer.ML"
+
+setup Transfer.setup
+
+
subsection {* Set up transfer from nat to int *}
-(* set up transfer direction *)
+text {* set up transfer direction *}
lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
by (simp add: TransferMorphism_def)
@@ -20,7 +31,7 @@
labels: natint
]
-(* basic functions and relations *)
+text {* basic functions and relations *}
lemma transfer_nat_int_numerals:
"(0::nat) = nat 0"
@@ -43,31 +54,20 @@
"(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)
+ nat_power_eq 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:
@@ -89,7 +89,21 @@
]
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
+
+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. 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:
"(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
@@ -110,7 +124,7 @@
cong: all_cong ex_cong]
-(* if *)
+text {* if *}
lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
nat (if P then x else y)"
@@ -119,7 +133,7 @@
declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
-(* operations with sets *)
+text {* operations with sets *}
definition
nat_set :: "int set \<Rightarrow> bool"
@@ -132,8 +146,6 @@
"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)
@@ -144,17 +156,12 @@
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? *)
@@ -167,7 +174,6 @@
"(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)
@@ -194,7 +200,7 @@
]
-(* setsum and setprod *)
+text {* setsum and setprod *}
(* this handles the case where the *domain* of f is nat *)
lemma transfer_nat_int_sum_prod:
@@ -262,52 +268,10 @@
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 *)
+text {* set up transfer direction *}
lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
by (simp add: TransferMorphism_def)
@@ -319,7 +283,11 @@
]
-(* basic functions and relations *)
+text {* basic functions and relations *}
+
+lemma UNIV_apply:
+ "UNIV x = True"
+ by (simp add: top_fun_eq top_bool_eq)
definition
is_nat :: "int \<Rightarrow> bool"
@@ -338,17 +306,13 @@
"(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)
+ by (auto simp add: int_mult tsub_def int_power)
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"
@@ -361,12 +325,7 @@
"(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)
+ by (auto simp add: zdvd_int)
declare TransferMorphism_int_nat[transfer add return:
transfer_int_nat_numerals
@@ -377,7 +336,7 @@
]
-(* first-order quantifiers *)
+text {* first-order quantifiers *}
lemma transfer_int_nat_quantifiers:
"(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
@@ -392,7 +351,7 @@
return: transfer_int_nat_quantifiers]
-(* if *)
+text {* if *}
lemma int_if_cong: "(if P then (int x) else (int y)) =
int (if P then x else y)"
@@ -402,7 +361,7 @@
-(* operations with sets *)
+text {* operations with sets *}
lemma transfer_int_nat_set_functions:
"nat_set A \<Longrightarrow> card A = card (nat ` A)"
@@ -410,7 +369,6 @@
"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
@@ -421,7 +379,6 @@
"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"
@@ -454,7 +411,7 @@
]
-(* setsum and setprod *)
+text {* setsum and setprod *}
(* this handles the case where the *domain* of f is int *)
lemma transfer_int_nat_sum_prod:
--- a/src/HOL/Parity.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Parity.thy Thu Oct 29 11:41:36 2009 +0100
@@ -28,6 +28,13 @@
end
+lemma transfer_int_nat_relations:
+ "even (int x) \<longleftrightarrow> even x"
+ by (simp add: even_nat_def)
+
+declare TransferMorphism_int_nat[transfer add return:
+ transfer_int_nat_relations
+]
lemma even_zero_int[simp]: "even (0::int)" by presburger
@@ -310,6 +317,8 @@
subsection {* General Lemmas About Division *}
+(*FIXME move to Divides.thy*)
+
lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
apply (induct "m")
apply (simp_all add: mod_Suc)
--- a/src/HOL/Presburger.thy Thu Oct 29 08:14:39 2009 +0100
+++ b/src/HOL/Presburger.thy Thu Oct 29 11:41:36 2009 +0100
@@ -385,20 +385,6 @@
text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
-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. 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))"
by (case_tac "y \<le> x", simp_all add: zdiff_int)
--- 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