--- a/src/HOL/Code_Numeral.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Code_Numeral.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/Divides.thy Thu Oct 29 13:37:55 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/Fact.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Fact.thy Thu Oct 29 13:37:55 2009 +0100
@@ -8,7 +8,7 @@
header{*Factorial Function*}
theory Fact
-imports Nat_Transfer
+imports Main
begin
class fact =
@@ -266,9 +266,6 @@
lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
by auto
-class ordered_semiring_1 = ordered_semiring + semiring_1
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
-
lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
--- a/src/HOL/Fun.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Fun.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/GCD.thy Thu Oct 29 13:37:55 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/Int.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Int.thy Thu Oct 29 13:37:55 2009 +0100
@@ -1984,6 +1984,135 @@
lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+subsection {* The divides relation *}
+
+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 dvd_imp_le_int:
+ fixes d i :: int
+ assumes "i \<noteq> 0" and "d dvd i"
+ shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
+proof -
+ from `d dvd i` obtain k where "i = d * k" ..
+ with `i \<noteq> 0` have "k \<noteq> 0" by auto
+ then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
+ then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
+ with `i = d * k` show ?thesis by (simp add: abs_mult)
+qed
+
+lemma zdvd_not_zless:
+ fixes m n :: int
+ assumes "0 < m" and "m < n"
+ shows "\<not> n dvd m"
+proof
+ from assms have "0 < n" by auto
+ assume "n dvd m" then obtain k where k: "m = n * k" ..
+ with `0 < m` have "0 < n * k" by auto
+ with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
+ with k `0 < n` `m < n` have "n * k < n * 1" by simp
+ with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
+qed
+
+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: of_nat_mult [symmetric])
+ 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: of_nat_mult [symmetric])
+ 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 of_nat_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"
+ then have "x = 1 \<or> x = -1" by auto
+ then show "x dvd 1" by (auto intro: dvdI)
+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
+
+
subsection {* Configuration of the code generator *}
code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
--- a/src/HOL/IntDiv.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/IntDiv.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/IsaMakefile Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/List.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/Nat_Transfer.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/Parity.thy Thu Oct 29 13:37:55 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 11:26:47 2009 +0100
+++ b/src/HOL/Presburger.thy Thu Oct 29 13:37:55 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/Ring_and_Field.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy Thu Oct 29 13:37:55 2009 +0100
@@ -767,6 +767,8 @@
end
+class ordered_semiring_1 = ordered_semiring + semiring_1
+
class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
@@ -884,6 +886,8 @@
end
+class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
+
class mult_mono1 = times + zero + ord +
assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
@@ -2025,15 +2029,15 @@
lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
==> x * y <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
==> y * x <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
- x / y <= z";
-by (subst pos_divide_le_eq, assumption+);
+ x / y <= z"
+by (subst pos_divide_le_eq, assumption+)
lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
z <= x / y"
@@ -2060,8 +2064,8 @@
lemma frac_less: "(0::'a::ordered_field) <= x ==>
x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
apply (rule mult_imp_div_pos_less)
- apply simp;
- apply (subst times_divide_eq_left);
+ apply simp
+ apply (subst times_divide_eq_left)
apply (rule mult_imp_less_div_pos, assumption)
apply (erule mult_less_le_imp_less)
apply simp_all
@@ -2071,7 +2075,7 @@
x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
apply (rule mult_imp_div_pos_less)
apply simp_all
- apply (subst times_divide_eq_left);
+ apply (subst times_divide_eq_left)
apply (rule mult_imp_less_div_pos, assumption)
apply (erule mult_le_less_imp_less)
apply simp_all
--- a/src/HOL/SetInterval.thy Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/SetInterval.thy Thu Oct 29 13:37:55 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
--- a/src/HOL/Tools/transfer.ML Thu Oct 29 11:26:47 2009 +0100
+++ b/src/HOL/Tools/transfer.ML Thu Oct 29 13:37:55 2009 +0100
@@ -14,8 +14,15 @@
structure Transfer : TRANSFER =
struct
-type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
- guess : bool, hints : string list};
+type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list,
+ guess : bool, hints : string list };
+
+fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry,
+ { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) =
+ { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2),
+ ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2),
+ guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) };
+
type data = simpset * (thm * entry) list;
structure Data = GenericDataFun
@@ -24,7 +31,7 @@
val empty = (HOL_ss, []);
val extend = I;
fun merge _ ((ss1, e1), (ss2, e2)) =
- (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2));
+ (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
);
val get = Data.get o Context.Proof;