1.1 --- a/src/HOL/Code_Numeral.thy Thu Oct 29 15:24:52 2009 +0100
1.2 +++ b/src/HOL/Code_Numeral.thy Thu Oct 29 15:26:00 2009 +0100
1.3 @@ -3,7 +3,7 @@
1.4 header {* Type of target language numerals *}
1.5
1.6 theory Code_Numeral
1.7 -imports Nat_Numeral Divides
1.8 +imports Nat_Numeral Nat_Transfer Divides
1.9 begin
1.10
1.11 text {*
2.1 --- a/src/HOL/Divides.thy Thu Oct 29 15:24:52 2009 +0100
2.2 +++ b/src/HOL/Divides.thy Thu Oct 29 15:26:00 2009 +0100
2.3 @@ -6,7 +6,7 @@
2.4 header {* The division operators div and mod *}
2.5
2.6 theory Divides
2.7 -imports Nat_Numeral
2.8 +imports Nat_Numeral Nat_Transfer
2.9 uses
2.10 "~~/src/Provers/Arith/assoc_fold.ML"
2.11 "~~/src/Provers/Arith/cancel_numerals.ML"
3.1 --- a/src/HOL/Fact.thy Thu Oct 29 15:24:52 2009 +0100
3.2 +++ b/src/HOL/Fact.thy Thu Oct 29 15:26:00 2009 +0100
3.3 @@ -8,7 +8,7 @@
3.4 header{*Factorial Function*}
3.5
3.6 theory Fact
3.7 -imports Nat_Transfer
3.8 +imports Main
3.9 begin
3.10
3.11 class fact =
3.12 @@ -266,9 +266,6 @@
3.13 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
3.14 by auto
3.15
3.16 -class ordered_semiring_1 = ordered_semiring + semiring_1
3.17 -class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
3.18 -
3.19 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
3.20
3.21 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
4.1 --- a/src/HOL/Fun.thy Thu Oct 29 15:24:52 2009 +0100
4.2 +++ b/src/HOL/Fun.thy Thu Oct 29 15:26:00 2009 +0100
4.3 @@ -7,7 +7,6 @@
4.4
4.5 theory Fun
4.6 imports Complete_Lattice
4.7 -uses ("Tools/transfer.ML")
4.8 begin
4.9
4.10 text{*As a simplification rule, it replaces all function equalities by
4.11 @@ -604,16 +603,6 @@
4.12 *}
4.13
4.14
4.15 -subsection {* Generic transfer procedure *}
4.16 -
4.17 -definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
4.18 - where "TransferMorphism a B \<longleftrightarrow> True"
4.19 -
4.20 -use "Tools/transfer.ML"
4.21 -
4.22 -setup Transfer.setup
4.23 -
4.24 -
4.25 subsection {* Code generator setup *}
4.26
4.27 types_code
5.1 --- a/src/HOL/GCD.thy Thu Oct 29 15:24:52 2009 +0100
5.2 +++ b/src/HOL/GCD.thy Thu Oct 29 15:26:00 2009 +0100
5.3 @@ -28,7 +28,7 @@
5.4 header {* GCD *}
5.5
5.6 theory GCD
5.7 -imports Fact
5.8 +imports Fact Parity
5.9 begin
5.10
5.11 declare One_nat_def [simp del]
6.1 --- a/src/HOL/Int.thy Thu Oct 29 15:24:52 2009 +0100
6.2 +++ b/src/HOL/Int.thy Thu Oct 29 15:26:00 2009 +0100
6.3 @@ -1984,6 +1984,135 @@
6.4 lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
6.5
6.6
6.7 +subsection {* The divides relation *}
6.8 +
6.9 +lemma zdvd_anti_sym:
6.10 + "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
6.11 + apply (simp add: dvd_def, auto)
6.12 + apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
6.13 + done
6.14 +
6.15 +lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
6.16 + shows "\<bar>a\<bar> = \<bar>b\<bar>"
6.17 +proof-
6.18 + from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
6.19 + from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
6.20 + from k k' have "a = a*k*k'" by simp
6.21 + with mult_cancel_left1[where c="a" and b="k*k'"]
6.22 + have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
6.23 + hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
6.24 + thus ?thesis using k k' by auto
6.25 +qed
6.26 +
6.27 +lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
6.28 + apply (subgoal_tac "m = n + (m - n)")
6.29 + apply (erule ssubst)
6.30 + apply (blast intro: dvd_add, simp)
6.31 + done
6.32 +
6.33 +lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
6.34 +apply (rule iffI)
6.35 + apply (erule_tac [2] dvd_add)
6.36 + apply (subgoal_tac "n = (n + k * m) - k * m")
6.37 + apply (erule ssubst)
6.38 + apply (erule dvd_diff)
6.39 + apply(simp_all)
6.40 +done
6.41 +
6.42 +lemma dvd_imp_le_int:
6.43 + fixes d i :: int
6.44 + assumes "i \<noteq> 0" and "d dvd i"
6.45 + shows "\<bar>d\<bar> \<le> \<bar>i\<bar>"
6.46 +proof -
6.47 + from `d dvd i` obtain k where "i = d * k" ..
6.48 + with `i \<noteq> 0` have "k \<noteq> 0" by auto
6.49 + then have "1 \<le> \<bar>k\<bar>" and "0 \<le> \<bar>d\<bar>" by auto
6.50 + then have "\<bar>d\<bar> * 1 \<le> \<bar>d\<bar> * \<bar>k\<bar>" by (rule mult_left_mono)
6.51 + with `i = d * k` show ?thesis by (simp add: abs_mult)
6.52 +qed
6.53 +
6.54 +lemma zdvd_not_zless:
6.55 + fixes m n :: int
6.56 + assumes "0 < m" and "m < n"
6.57 + shows "\<not> n dvd m"
6.58 +proof
6.59 + from assms have "0 < n" by auto
6.60 + assume "n dvd m" then obtain k where k: "m = n * k" ..
6.61 + with `0 < m` have "0 < n * k" by auto
6.62 + with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff)
6.63 + with k `0 < n` `m < n` have "n * k < n * 1" by simp
6.64 + with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto
6.65 +qed
6.66 +
6.67 +lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
6.68 + shows "m dvd n"
6.69 +proof-
6.70 + from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
6.71 + {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
6.72 + with h have False by (simp add: mult_assoc)}
6.73 + hence "n = m * h" by blast
6.74 + thus ?thesis by simp
6.75 +qed
6.76 +
6.77 +theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
6.78 +proof -
6.79 + have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
6.80 + proof -
6.81 + fix k
6.82 + assume A: "int y = int x * k"
6.83 + then show "x dvd y" proof (cases k)
6.84 + case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
6.85 + then show ?thesis ..
6.86 + next
6.87 + case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
6.88 + also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
6.89 + also have "\<dots> = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric])
6.90 + finally have "- int (x * Suc n) = int y" ..
6.91 + then show ?thesis by (simp only: negative_eq_positive) auto
6.92 + qed
6.93 + qed
6.94 + then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult)
6.95 +qed
6.96 +
6.97 +lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
6.98 +proof
6.99 + assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
6.100 + hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
6.101 + hence "nat \<bar>x\<bar> = 1" by simp
6.102 + thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
6.103 +next
6.104 + assume "\<bar>x\<bar>=1"
6.105 + then have "x = 1 \<or> x = -1" by auto
6.106 + then show "x dvd 1" by (auto intro: dvdI)
6.107 +qed
6.108 +
6.109 +lemma zdvd_mult_cancel1:
6.110 + assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
6.111 +proof
6.112 + assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
6.113 + by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
6.114 +next
6.115 + assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
6.116 + from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
6.117 +qed
6.118 +
6.119 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
6.120 + unfolding zdvd_int by (cases "z \<ge> 0") simp_all
6.121 +
6.122 +lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
6.123 + unfolding zdvd_int by (cases "z \<ge> 0") simp_all
6.124 +
6.125 +lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
6.126 + by (auto simp add: dvd_int_iff)
6.127 +
6.128 +lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
6.129 + apply (rule_tac z=n in int_cases)
6.130 + apply (auto simp add: dvd_int_iff)
6.131 + apply (rule_tac z=z in int_cases)
6.132 + apply (auto simp add: dvd_imp_le)
6.133 + done
6.134 +
6.135 +
6.136 subsection {* Configuration of the code generator *}
6.137
6.138 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
7.1 --- a/src/HOL/IntDiv.thy Thu Oct 29 15:24:52 2009 +0100
7.2 +++ b/src/HOL/IntDiv.thy Thu Oct 29 15:26:00 2009 +0100
7.3 @@ -1024,139 +1024,16 @@
7.4 lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
7.5 dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
7.6
7.7 -lemma zdvd_anti_sym:
7.8 - "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
7.9 - apply (simp add: dvd_def, auto)
7.10 - apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
7.11 - done
7.12 -
7.13 -lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a"
7.14 - shows "\<bar>a\<bar> = \<bar>b\<bar>"
7.15 -proof-
7.16 - from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast
7.17 - from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast
7.18 - from k k' have "a = a*k*k'" by simp
7.19 - with mult_cancel_left1[where c="a" and b="k*k'"]
7.20 - have kk':"k*k' = 1" using `a\<noteq>0` by (simp add: mult_assoc)
7.21 - hence "k = 1 \<and> k' = 1 \<or> k = -1 \<and> k' = -1" by (simp add: zmult_eq_1_iff)
7.22 - thus ?thesis using k k' by auto
7.23 -qed
7.24 -
7.25 -lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"
7.26 - apply (subgoal_tac "m = n + (m - n)")
7.27 - apply (erule ssubst)
7.28 - apply (blast intro: dvd_add, simp)
7.29 - done
7.30 -
7.31 -lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"
7.32 -apply (rule iffI)
7.33 - apply (erule_tac [2] dvd_add)
7.34 - apply (subgoal_tac "n = (n + k * m) - k * m")
7.35 - apply (erule ssubst)
7.36 - apply (erule dvd_diff)
7.37 - apply(simp_all)
7.38 -done
7.39 -
7.40 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
7.41 by (rule dvd_mod) (* TODO: remove *)
7.42
7.43 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
7.44 by (rule dvd_mod_imp_dvd) (* TODO: remove *)
7.45
7.46 -lemma dvd_imp_le_int: "(i::int) ~= 0 ==> d dvd i ==> abs d <= abs i"
7.47 -apply(auto simp:abs_if)
7.48 - apply(clarsimp simp:dvd_def mult_less_0_iff)
7.49 - using mult_le_cancel_left_neg[of _ "-1::int"]
7.50 - apply(clarsimp simp:dvd_def mult_less_0_iff)
7.51 - apply(clarsimp simp:dvd_def mult_less_0_iff
7.52 - minus_mult_right simp del: mult_minus_right)
7.53 -apply(clarsimp simp:dvd_def mult_less_0_iff)
7.54 -done
7.55 -
7.56 -lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
7.57 - apply (auto elim!: dvdE)
7.58 - apply (subgoal_tac "0 < n")
7.59 - prefer 2
7.60 - apply (blast intro: order_less_trans)
7.61 - apply (simp add: zero_less_mult_iff)
7.62 - done
7.63 -
7.64 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
7.65 using zmod_zdiv_equality[where a="m" and b="n"]
7.66 by (simp add: algebra_simps)
7.67
7.68 -lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
7.69 -apply (subgoal_tac "m mod n = 0")
7.70 - apply (simp add: zmult_div_cancel)
7.71 -apply (simp only: dvd_eq_mod_eq_0)
7.72 -done
7.73 -
7.74 -lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \<noteq> (0::int)"
7.75 - shows "m dvd n"
7.76 -proof-
7.77 - from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast
7.78 - {assume "n \<noteq> m*h" hence "k* n \<noteq> k* (m*h)" using kz by simp
7.79 - with h have False by (simp add: mult_assoc)}
7.80 - hence "n = m * h" by blast
7.81 - thus ?thesis by simp
7.82 -qed
7.83 -
7.84 -theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
7.85 -proof -
7.86 - have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
7.87 - proof -
7.88 - fix k
7.89 - assume A: "int y = int x * k"
7.90 - then show "x dvd y" proof (cases k)
7.91 - case (1 n) with A have "y = x * n" by (simp add: zmult_int)
7.92 - then show ?thesis ..
7.93 - next
7.94 - case (2 n) with A have "int y = int x * (- int (Suc n))" by simp
7.95 - also have "\<dots> = - (int x * int (Suc n))" by (simp only: mult_minus_right)
7.96 - also have "\<dots> = - int (x * Suc n)" by (simp only: zmult_int)
7.97 - finally have "- int (x * Suc n) = int y" ..
7.98 - then show ?thesis by (simp only: negative_eq_positive) auto
7.99 - qed
7.100 - qed
7.101 - then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left int_mult)
7.102 -qed
7.103 -
7.104 -lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
7.105 -proof
7.106 - assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by simp
7.107 - hence "nat \<bar>x\<bar> dvd 1" by (simp add: zdvd_int)
7.108 - hence "nat \<bar>x\<bar> = 1" by simp
7.109 - thus "\<bar>x\<bar> = 1" by (cases "x < 0", auto)
7.110 -next
7.111 - assume "\<bar>x\<bar>=1" thus "x dvd 1"
7.112 - by(cases "x < 0",simp_all add: minus_equation_iff dvd_eq_mod_eq_0)
7.113 -qed
7.114 -lemma zdvd_mult_cancel1:
7.115 - assumes mp:"m \<noteq>(0::int)" shows "(m * n dvd m) = (\<bar>n\<bar> = 1)"
7.116 -proof
7.117 - assume n1: "\<bar>n\<bar> = 1" thus "m * n dvd m"
7.118 - by (cases "n >0", auto simp add: minus_dvd_iff minus_equation_iff)
7.119 -next
7.120 - assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp
7.121 - from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
7.122 -qed
7.123 -
7.124 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
7.125 - unfolding zdvd_int by (cases "z \<ge> 0") simp_all
7.126 -
7.127 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
7.128 - unfolding zdvd_int by (cases "z \<ge> 0") simp_all
7.129 -
7.130 -lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
7.131 - by (auto simp add: dvd_int_iff)
7.132 -
7.133 -lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
7.134 - apply (rule_tac z=n in int_cases)
7.135 - apply (auto simp add: dvd_int_iff)
7.136 - apply (rule_tac z=z in int_cases)
7.137 - apply (auto simp add: dvd_imp_le)
7.138 - done
7.139 -
7.140 lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
7.141 apply (induct "y", auto)
7.142 apply (rule zmod_zmult1_eq [THEN trans])
7.143 @@ -1182,6 +1059,12 @@
7.144 lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
7.145 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
7.146
7.147 +lemma zdvd_mult_div_cancel:"(n::int) dvd m \<Longrightarrow> n * (m div n) = m"
7.148 +apply (subgoal_tac "m mod n = 0")
7.149 + apply (simp add: zmult_div_cancel)
7.150 +apply (simp only: dvd_eq_mod_eq_0)
7.151 +done
7.152 +
7.153 text{*Suggested by Matthias Daum*}
7.154 lemma int_power_div_base:
7.155 "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
7.156 @@ -1349,6 +1232,43 @@
7.157 declare dvd_eq_mod_eq_0_number_of [simp]
7.158
7.159
7.160 +subsection {* Transfer setup *}
7.161 +
7.162 +lemma transfer_nat_int_functions:
7.163 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
7.164 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
7.165 + by (auto simp add: nat_div_distrib nat_mod_distrib)
7.166 +
7.167 +lemma transfer_nat_int_function_closures:
7.168 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
7.169 + "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
7.170 + apply (cases "y = 0")
7.171 + apply (auto simp add: pos_imp_zdiv_nonneg_iff)
7.172 + apply (cases "y = 0")
7.173 + apply auto
7.174 +done
7.175 +
7.176 +declare TransferMorphism_nat_int[transfer add return:
7.177 + transfer_nat_int_functions
7.178 + transfer_nat_int_function_closures
7.179 +]
7.180 +
7.181 +lemma transfer_int_nat_functions:
7.182 + "(int x) div (int y) = int (x div y)"
7.183 + "(int x) mod (int y) = int (x mod y)"
7.184 + by (auto simp add: zdiv_int zmod_int)
7.185 +
7.186 +lemma transfer_int_nat_function_closures:
7.187 + "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
7.188 + "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
7.189 + by (simp_all only: is_nat_def transfer_nat_int_function_closures)
7.190 +
7.191 +declare TransferMorphism_int_nat[transfer add return:
7.192 + transfer_int_nat_functions
7.193 + transfer_int_nat_function_closures
7.194 +]
7.195 +
7.196 +
7.197 subsection {* Code generation *}
7.198
7.199 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
8.1 --- a/src/HOL/IsaMakefile Thu Oct 29 15:24:52 2009 +0100
8.2 +++ b/src/HOL/IsaMakefile Thu Oct 29 15:26:00 2009 +0100
8.3 @@ -225,7 +225,6 @@
8.4 Tools/sat_funcs.ML \
8.5 Tools/sat_solver.ML \
8.6 Tools/split_rule.ML \
8.7 - Tools/transfer.ML \
8.8 Tools/typecopy.ML \
8.9 Tools/typedef_codegen.ML \
8.10 Tools/typedef.ML \
8.11 @@ -257,6 +256,7 @@
8.12 Main.thy \
8.13 Map.thy \
8.14 Nat_Numeral.thy \
8.15 + Nat_Transfer.thy \
8.16 Presburger.thy \
8.17 Predicate_Compile.thy \
8.18 Quickcheck.thy \
8.19 @@ -278,6 +278,7 @@
8.20 Tools/Groebner_Basis/misc.ML \
8.21 Tools/Groebner_Basis/normalizer.ML \
8.22 Tools/Groebner_Basis/normalizer_data.ML \
8.23 + Tools/choice_specification.ML \
8.24 Tools/int_arith.ML \
8.25 Tools/list_code.ML \
8.26 Tools/meson.ML \
8.27 @@ -301,7 +302,6 @@
8.28 Tools/Qelim/presburger.ML \
8.29 Tools/Qelim/qelim.ML \
8.30 Tools/recdef.ML \
8.31 - Tools/choice_specification.ML \
8.32 Tools/res_atp.ML \
8.33 Tools/res_axioms.ML \
8.34 Tools/res_clause.ML \
8.35 @@ -309,6 +309,7 @@
8.36 Tools/res_reconstruct.ML \
8.37 Tools/string_code.ML \
8.38 Tools/string_syntax.ML \
8.39 + Tools/transfer.ML \
8.40 Tools/TFL/casesplit.ML \
8.41 Tools/TFL/dcterm.ML \
8.42 Tools/TFL/post.ML \
8.43 @@ -336,7 +337,6 @@
8.44 Log.thy \
8.45 Lubs.thy \
8.46 MacLaurin.thy \
8.47 - Nat_Transfer.thy \
8.48 NthRoot.thy \
8.49 PReal.thy \
8.50 Parity.thy \
9.1 --- a/src/HOL/List.thy Thu Oct 29 15:24:52 2009 +0100
9.2 +++ b/src/HOL/List.thy Thu Oct 29 15:26:00 2009 +0100
9.3 @@ -3587,8 +3587,8 @@
9.4 by (blast intro: listrel.intros)
9.5
9.6 lemma listrel_Cons:
9.7 - "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
9.8 -by (auto simp add: set_Cons_def intro: listrel.intros)
9.9 + "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
9.10 +by (auto simp add: set_Cons_def intro: listrel.intros)
9.11
9.12
9.13 subsection {* Size function *}
9.14 @@ -3615,6 +3615,45 @@
9.15 by (induct xs) force+
9.16
9.17
9.18 +subsection {* Transfer *}
9.19 +
9.20 +definition
9.21 + embed_list :: "nat list \<Rightarrow> int list"
9.22 +where
9.23 + "embed_list l = map int l"
9.24 +
9.25 +definition
9.26 + nat_list :: "int list \<Rightarrow> bool"
9.27 +where
9.28 + "nat_list l = nat_set (set l)"
9.29 +
9.30 +definition
9.31 + return_list :: "int list \<Rightarrow> nat list"
9.32 +where
9.33 + "return_list l = map nat l"
9.34 +
9.35 +lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
9.36 + embed_list (return_list l) = l"
9.37 + unfolding embed_list_def return_list_def nat_list_def nat_set_def
9.38 + apply (induct l)
9.39 + apply auto
9.40 +done
9.41 +
9.42 +lemma transfer_nat_int_list_functions:
9.43 + "l @ m = return_list (embed_list l @ embed_list m)"
9.44 + "[] = return_list []"
9.45 + unfolding return_list_def embed_list_def
9.46 + apply auto
9.47 + apply (induct l, auto)
9.48 + apply (induct m, auto)
9.49 +done
9.50 +
9.51 +(*
9.52 +lemma transfer_nat_int_fold1: "fold f l x =
9.53 + fold (%x. f (nat x)) (embed_list l) x";
9.54 +*)
9.55 +
9.56 +
9.57 subsection {* Code generator *}
9.58
9.59 subsubsection {* Setup *}
9.60 @@ -4017,5 +4056,4 @@
9.61 "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
9.62 by(simp add: all_from_to_int_iff_ball list_ex_iff)
9.63
9.64 -
9.65 end
10.1 --- a/src/HOL/Nat_Transfer.thy Thu Oct 29 15:24:52 2009 +0100
10.2 +++ b/src/HOL/Nat_Transfer.thy Thu Oct 29 15:26:00 2009 +0100
10.3 @@ -1,15 +1,26 @@
10.4
10.5 (* Authors: Jeremy Avigad and Amine Chaieb *)
10.6
10.7 -header {* Sets up transfer from nats to ints and back. *}
10.8 +header {* Generic transfer machinery; specific transfer from nats to ints and back. *}
10.9
10.10 theory Nat_Transfer
10.11 -imports Main Parity
10.12 +imports Nat_Numeral
10.13 +uses ("Tools/transfer.ML")
10.14 begin
10.15
10.16 +subsection {* Generic transfer machinery *}
10.17 +
10.18 +definition TransferMorphism:: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> bool"
10.19 + where "TransferMorphism a B \<longleftrightarrow> True"
10.20 +
10.21 +use "Tools/transfer.ML"
10.22 +
10.23 +setup Transfer.setup
10.24 +
10.25 +
10.26 subsection {* Set up transfer from nat to int *}
10.27
10.28 -(* set up transfer direction *)
10.29 +text {* set up transfer direction *}
10.30
10.31 lemma TransferMorphism_nat_int: "TransferMorphism nat (op <= (0::int))"
10.32 by (simp add: TransferMorphism_def)
10.33 @@ -20,7 +31,7 @@
10.34 labels: natint
10.35 ]
10.36
10.37 -(* basic functions and relations *)
10.38 +text {* basic functions and relations *}
10.39
10.40 lemma transfer_nat_int_numerals:
10.41 "(0::nat) = nat 0"
10.42 @@ -43,31 +54,20 @@
10.43 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) * (nat y) = nat (x * y)"
10.44 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) - (nat y) = nat (tsub x y)"
10.45 "(x::int) >= 0 \<Longrightarrow> (nat x)^n = nat (x^n)"
10.46 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) div (nat y) = nat (x div y)"
10.47 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> (nat x) mod (nat y) = nat (x mod y)"
10.48 by (auto simp add: eq_nat_nat_iff nat_mult_distrib
10.49 - nat_power_eq nat_div_distrib nat_mod_distrib tsub_def)
10.50 + nat_power_eq tsub_def)
10.51
10.52 lemma transfer_nat_int_function_closures:
10.53 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x + y >= 0"
10.54 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x * y >= 0"
10.55 "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> tsub x y >= 0"
10.56 "(x::int) >= 0 \<Longrightarrow> x^n >= 0"
10.57 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x div y >= 0"
10.58 - "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> x mod y >= 0"
10.59 "(0::int) >= 0"
10.60 "(1::int) >= 0"
10.61 "(2::int) >= 0"
10.62 "(3::int) >= 0"
10.63 "int z >= 0"
10.64 apply (auto simp add: zero_le_mult_iff tsub_def)
10.65 - apply (case_tac "y = 0")
10.66 - apply auto
10.67 - apply (subst pos_imp_zdiv_nonneg_iff, auto)
10.68 - apply (case_tac "y = 0")
10.69 - apply force
10.70 - apply (rule pos_mod_sign)
10.71 - apply arith
10.72 done
10.73
10.74 lemma transfer_nat_int_relations:
10.75 @@ -89,7 +89,21 @@
10.76 ]
10.77
10.78
10.79 -(* first-order quantifiers *)
10.80 +text {* first-order quantifiers *}
10.81 +
10.82 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
10.83 + by (simp split add: split_nat)
10.84 +
10.85 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
10.86 +proof
10.87 + assume "\<exists>x. P x"
10.88 + then obtain x where "P x" ..
10.89 + then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
10.90 + then show "\<exists>x\<ge>0. P (nat x)" ..
10.91 +next
10.92 + assume "\<exists>x\<ge>0. P (nat x)"
10.93 + then show "\<exists>x. P x" by auto
10.94 +qed
10.95
10.96 lemma transfer_nat_int_quantifiers:
10.97 "(ALL (x::nat). P x) = (ALL (x::int). x >= 0 \<longrightarrow> P (nat x))"
10.98 @@ -110,7 +124,7 @@
10.99 cong: all_cong ex_cong]
10.100
10.101
10.102 -(* if *)
10.103 +text {* if *}
10.104
10.105 lemma nat_if_cong: "(if P then (nat x) else (nat y)) =
10.106 nat (if P then x else y)"
10.107 @@ -119,7 +133,7 @@
10.108 declare TransferMorphism_nat_int [transfer add return: nat_if_cong]
10.109
10.110
10.111 -(* operations with sets *)
10.112 +text {* operations with sets *}
10.113
10.114 definition
10.115 nat_set :: "int set \<Rightarrow> bool"
10.116 @@ -132,8 +146,6 @@
10.117 "A Un B = nat ` (int ` A Un int ` B)"
10.118 "A Int B = nat ` (int ` A Int int ` B)"
10.119 "{x. P x} = nat ` {x. x >= 0 & P(nat x)}"
10.120 - "{..n} = nat ` {0..int n}"
10.121 - "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
10.122 apply (rule card_image [symmetric])
10.123 apply (auto simp add: inj_on_def image_def)
10.124 apply (rule_tac x = "int x" in bexI)
10.125 @@ -144,17 +156,12 @@
10.126 apply auto
10.127 apply (rule_tac x = "int x" in exI)
10.128 apply auto
10.129 - apply (rule_tac x = "int x" in bexI)
10.130 - apply auto
10.131 - apply (rule_tac x = "int x" in bexI)
10.132 - apply auto
10.133 done
10.134
10.135 lemma transfer_nat_int_set_function_closures:
10.136 "nat_set {}"
10.137 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
10.138 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
10.139 - "x >= 0 \<Longrightarrow> nat_set {x..y}"
10.140 "nat_set {x. x >= 0 & P x}"
10.141 "nat_set (int ` C)"
10.142 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> x >= 0" (* does it hurt to turn this on? *)
10.143 @@ -167,7 +174,6 @@
10.144 "(A = B) = (int ` A = int ` B)"
10.145 "(A < B) = (int ` A < int ` B)"
10.146 "(A <= B) = (int ` A <= int ` B)"
10.147 -
10.148 apply (rule iffI)
10.149 apply (erule finite_imageI)
10.150 apply (erule finite_imageD)
10.151 @@ -194,7 +200,7 @@
10.152 ]
10.153
10.154
10.155 -(* setsum and setprod *)
10.156 +text {* setsum and setprod *}
10.157
10.158 (* this handles the case where the *domain* of f is nat *)
10.159 lemma transfer_nat_int_sum_prod:
10.160 @@ -262,52 +268,10 @@
10.161 transfer_nat_int_sum_prod_closure
10.162 cong: transfer_nat_int_sum_prod_cong]
10.163
10.164 -(* lists *)
10.165 -
10.166 -definition
10.167 - embed_list :: "nat list \<Rightarrow> int list"
10.168 -where
10.169 - "embed_list l = map int l";
10.170 -
10.171 -definition
10.172 - nat_list :: "int list \<Rightarrow> bool"
10.173 -where
10.174 - "nat_list l = nat_set (set l)";
10.175 -
10.176 -definition
10.177 - return_list :: "int list \<Rightarrow> nat list"
10.178 -where
10.179 - "return_list l = map nat l";
10.180 -
10.181 -thm nat_0_le;
10.182 -
10.183 -lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
10.184 - embed_list (return_list l) = l";
10.185 - unfolding embed_list_def return_list_def nat_list_def nat_set_def
10.186 - apply (induct l);
10.187 - apply auto;
10.188 -done;
10.189 -
10.190 -lemma transfer_nat_int_list_functions:
10.191 - "l @ m = return_list (embed_list l @ embed_list m)"
10.192 - "[] = return_list []";
10.193 - unfolding return_list_def embed_list_def;
10.194 - apply auto;
10.195 - apply (induct l, auto);
10.196 - apply (induct m, auto);
10.197 -done;
10.198 -
10.199 -(*
10.200 -lemma transfer_nat_int_fold1: "fold f l x =
10.201 - fold (%x. f (nat x)) (embed_list l) x";
10.202 -*)
10.203 -
10.204 -
10.205 -
10.206
10.207 subsection {* Set up transfer from int to nat *}
10.208
10.209 -(* set up transfer direction *)
10.210 +text {* set up transfer direction *}
10.211
10.212 lemma TransferMorphism_int_nat: "TransferMorphism int (UNIV :: nat set)"
10.213 by (simp add: TransferMorphism_def)
10.214 @@ -319,7 +283,11 @@
10.215 ]
10.216
10.217
10.218 -(* basic functions and relations *)
10.219 +text {* basic functions and relations *}
10.220 +
10.221 +lemma UNIV_apply:
10.222 + "UNIV x = True"
10.223 + by (simp add: top_fun_eq top_bool_eq)
10.224
10.225 definition
10.226 is_nat :: "int \<Rightarrow> bool"
10.227 @@ -338,17 +306,13 @@
10.228 "(int x) * (int y) = int (x * y)"
10.229 "tsub (int x) (int y) = int (x - y)"
10.230 "(int x)^n = int (x^n)"
10.231 - "(int x) div (int y) = int (x div y)"
10.232 - "(int x) mod (int y) = int (x mod y)"
10.233 - by (auto simp add: int_mult tsub_def int_power zdiv_int zmod_int)
10.234 + by (auto simp add: int_mult tsub_def int_power)
10.235
10.236 lemma transfer_int_nat_function_closures:
10.237 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
10.238 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x * y)"
10.239 "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (tsub x y)"
10.240 "is_nat x \<Longrightarrow> is_nat (x^n)"
10.241 - "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
10.242 - "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
10.243 "is_nat 0"
10.244 "is_nat 1"
10.245 "is_nat 2"
10.246 @@ -361,12 +325,7 @@
10.247 "(int x < int y) = (x < y)"
10.248 "(int x <= int y) = (x <= y)"
10.249 "(int x dvd int y) = (x dvd y)"
10.250 - "(even (int x)) = (even x)"
10.251 - by (auto simp add: zdvd_int even_nat_def)
10.252 -
10.253 -lemma UNIV_apply:
10.254 - "UNIV x = True"
10.255 - by (simp add: top_fun_eq top_bool_eq)
10.256 + by (auto simp add: zdvd_int)
10.257
10.258 declare TransferMorphism_int_nat[transfer add return:
10.259 transfer_int_nat_numerals
10.260 @@ -377,7 +336,7 @@
10.261 ]
10.262
10.263
10.264 -(* first-order quantifiers *)
10.265 +text {* first-order quantifiers *}
10.266
10.267 lemma transfer_int_nat_quantifiers:
10.268 "(ALL (x::int) >= 0. P x) = (ALL (x::nat). P (int x))"
10.269 @@ -392,7 +351,7 @@
10.270 return: transfer_int_nat_quantifiers]
10.271
10.272
10.273 -(* if *)
10.274 +text {* if *}
10.275
10.276 lemma int_if_cong: "(if P then (int x) else (int y)) =
10.277 int (if P then x else y)"
10.278 @@ -402,7 +361,7 @@
10.279
10.280
10.281
10.282 -(* operations with sets *)
10.283 +text {* operations with sets *}
10.284
10.285 lemma transfer_int_nat_set_functions:
10.286 "nat_set A \<Longrightarrow> card A = card (nat ` A)"
10.287 @@ -410,7 +369,6 @@
10.288 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Un B = int ` (nat ` A Un nat ` B)"
10.289 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> A Int B = int ` (nat ` A Int nat ` B)"
10.290 "{x. x >= 0 & P x} = int ` {x. P(int x)}"
10.291 - "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
10.292 (* need all variants of these! *)
10.293 by (simp_all only: is_nat_def transfer_nat_int_set_functions
10.294 transfer_nat_int_set_function_closures
10.295 @@ -421,7 +379,6 @@
10.296 "nat_set {}"
10.297 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Un B)"
10.298 "nat_set A \<Longrightarrow> nat_set B \<Longrightarrow> nat_set (A Int B)"
10.299 - "is_nat x \<Longrightarrow> nat_set {x..y}"
10.300 "nat_set {x. x >= 0 & P x}"
10.301 "nat_set (int ` C)"
10.302 "nat_set A \<Longrightarrow> x : A \<Longrightarrow> is_nat x"
10.303 @@ -454,7 +411,7 @@
10.304 ]
10.305
10.306
10.307 -(* setsum and setprod *)
10.308 +text {* setsum and setprod *}
10.309
10.310 (* this handles the case where the *domain* of f is int *)
10.311 lemma transfer_int_nat_sum_prod:
11.1 --- a/src/HOL/Parity.thy Thu Oct 29 15:24:52 2009 +0100
11.2 +++ b/src/HOL/Parity.thy Thu Oct 29 15:26:00 2009 +0100
11.3 @@ -28,6 +28,13 @@
11.4
11.5 end
11.6
11.7 +lemma transfer_int_nat_relations:
11.8 + "even (int x) \<longleftrightarrow> even x"
11.9 + by (simp add: even_nat_def)
11.10 +
11.11 +declare TransferMorphism_int_nat[transfer add return:
11.12 + transfer_int_nat_relations
11.13 +]
11.14
11.15 lemma even_zero_int[simp]: "even (0::int)" by presburger
11.16
11.17 @@ -310,6 +317,8 @@
11.18
11.19 subsection {* General Lemmas About Division *}
11.20
11.21 +(*FIXME move to Divides.thy*)
11.22 +
11.23 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
11.24 apply (induct "m")
11.25 apply (simp_all add: mod_Suc)
12.1 --- a/src/HOL/Presburger.thy Thu Oct 29 15:24:52 2009 +0100
12.2 +++ b/src/HOL/Presburger.thy Thu Oct 29 15:26:00 2009 +0100
12.3 @@ -385,20 +385,6 @@
12.4
12.5 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
12.6
12.7 -lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
12.8 - by (simp split add: split_nat)
12.9 -
12.10 -lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
12.11 -proof
12.12 - assume "\<exists>x. P x"
12.13 - then obtain x where "P x" ..
12.14 - then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
12.15 - then show "\<exists>x\<ge>0. P (nat x)" ..
12.16 -next
12.17 - assume "\<exists>x\<ge>0. P (nat x)"
12.18 - then show "\<exists>x. P x" by auto
12.19 -qed
12.20 -
12.21 lemma zdiff_int_split: "P (int (x - y)) =
12.22 ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
12.23 by (case_tac "y \<le> x", simp_all add: zdiff_int)
13.1 --- a/src/HOL/Ring_and_Field.thy Thu Oct 29 15:24:52 2009 +0100
13.2 +++ b/src/HOL/Ring_and_Field.thy Thu Oct 29 15:26:00 2009 +0100
13.3 @@ -767,6 +767,8 @@
13.4
13.5 end
13.6
13.7 +class ordered_semiring_1 = ordered_semiring + semiring_1
13.8 +
13.9 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
13.10 assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
13.11 assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
13.12 @@ -884,6 +886,8 @@
13.13
13.14 end
13.15
13.16 +class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
13.17 +
13.18 class mult_mono1 = times + zero + ord +
13.19 assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
13.20
13.21 @@ -2025,15 +2029,15 @@
13.22
13.23 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
13.24 ==> x * y <= x"
13.25 -by (auto simp add: mult_compare_simps);
13.26 +by (auto simp add: mult_compare_simps)
13.27
13.28 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
13.29 ==> y * x <= x"
13.30 -by (auto simp add: mult_compare_simps);
13.31 +by (auto simp add: mult_compare_simps)
13.32
13.33 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
13.34 - x / y <= z";
13.35 -by (subst pos_divide_le_eq, assumption+);
13.36 + x / y <= z"
13.37 +by (subst pos_divide_le_eq, assumption+)
13.38
13.39 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
13.40 z <= x / y"
13.41 @@ -2060,8 +2064,8 @@
13.42 lemma frac_less: "(0::'a::ordered_field) <= x ==>
13.43 x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
13.44 apply (rule mult_imp_div_pos_less)
13.45 - apply simp;
13.46 - apply (subst times_divide_eq_left);
13.47 + apply simp
13.48 + apply (subst times_divide_eq_left)
13.49 apply (rule mult_imp_less_div_pos, assumption)
13.50 apply (erule mult_less_le_imp_less)
13.51 apply simp_all
13.52 @@ -2071,7 +2075,7 @@
13.53 x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
13.54 apply (rule mult_imp_div_pos_less)
13.55 apply simp_all
13.56 - apply (subst times_divide_eq_left);
13.57 + apply (subst times_divide_eq_left)
13.58 apply (rule mult_imp_less_div_pos, assumption)
13.59 apply (erule mult_le_less_imp_less)
13.60 apply simp_all
14.1 --- a/src/HOL/SetInterval.thy Thu Oct 29 15:24:52 2009 +0100
14.2 +++ b/src/HOL/SetInterval.thy Thu Oct 29 15:26:00 2009 +0100
14.3 @@ -9,7 +9,7 @@
14.4 header {* Set intervals *}
14.5
14.6 theory SetInterval
14.7 -imports Int
14.8 +imports Int Nat_Transfer
14.9 begin
14.10
14.11 context ord
14.12 @@ -1150,4 +1150,41 @@
14.13 "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
14.14 "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
14.15
14.16 +subsection {* Transfer setup *}
14.17 +
14.18 +lemma transfer_nat_int_set_functions:
14.19 + "{..n} = nat ` {0..int n}"
14.20 + "{m..n} = nat ` {int m..int n}" (* need all variants of these! *)
14.21 + apply (auto simp add: image_def)
14.22 + apply (rule_tac x = "int x" in bexI)
14.23 + apply auto
14.24 + apply (rule_tac x = "int x" in bexI)
14.25 + apply auto
14.26 + done
14.27 +
14.28 +lemma transfer_nat_int_set_function_closures:
14.29 + "x >= 0 \<Longrightarrow> nat_set {x..y}"
14.30 + by (simp add: nat_set_def)
14.31 +
14.32 +declare TransferMorphism_nat_int[transfer add
14.33 + return: transfer_nat_int_set_functions
14.34 + transfer_nat_int_set_function_closures
14.35 +]
14.36 +
14.37 +lemma transfer_int_nat_set_functions:
14.38 + "is_nat m \<Longrightarrow> is_nat n \<Longrightarrow> {m..n} = int ` {nat m..nat n}"
14.39 + by (simp only: is_nat_def transfer_nat_int_set_functions
14.40 + transfer_nat_int_set_function_closures
14.41 + transfer_nat_int_set_return_embed nat_0_le
14.42 + cong: transfer_nat_int_set_cong)
14.43 +
14.44 +lemma transfer_int_nat_set_function_closures:
14.45 + "is_nat x \<Longrightarrow> nat_set {x..y}"
14.46 + by (simp only: transfer_nat_int_set_function_closures is_nat_def)
14.47 +
14.48 +declare TransferMorphism_int_nat[transfer add
14.49 + return: transfer_int_nat_set_functions
14.50 + transfer_int_nat_set_function_closures
14.51 +]
14.52 +
14.53 end
15.1 --- a/src/HOL/Tools/transfer.ML Thu Oct 29 15:24:52 2009 +0100
15.2 +++ b/src/HOL/Tools/transfer.ML Thu Oct 29 15:26:00 2009 +0100
15.3 @@ -14,8 +14,15 @@
15.4 structure Transfer : TRANSFER =
15.5 struct
15.6
15.7 -type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
15.8 - guess : bool, hints : string list};
15.9 +type entry = { inj : thm list, emb : thm list, ret : thm list, cong : thm list,
15.10 + guess : bool, hints : string list };
15.11 +
15.12 +fun merge_entry ({ inj = inj1, emb = emb1, ret = ret1, cong = cong1, guess = guess1, hints = hints1 } : entry,
15.13 + { inj = inj2, emb = emb2, ret = ret2, cong = cong2, guess = guess2, hints = hints2 } : entry) =
15.14 + { inj = merge Thm.eq_thm (inj1, inj2), emb = merge Thm.eq_thm (emb1, emb2),
15.15 + ret = merge Thm.eq_thm (ret1, ret2), cong = merge Thm.eq_thm (cong1, cong2),
15.16 + guess = guess1 andalso guess2, hints = merge (op =) (hints1, hints2) };
15.17 +
15.18 type data = simpset * (thm * entry) list;
15.19
15.20 structure Data = GenericDataFun
15.21 @@ -24,7 +31,7 @@
15.22 val empty = (HOL_ss, []);
15.23 val extend = I;
15.24 fun merge _ ((ss1, e1), (ss2, e2)) =
15.25 - (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2));
15.26 + (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
15.27 );
15.28
15.29 val get = Data.get o Context.Proof;