--- a/NEWS Sun Jul 10 20:59:04 2011 +0200
+++ b/NEWS Sun Jul 10 21:46:41 2011 +0200
@@ -60,6 +60,9 @@
*** HOL ***
+* Archimedian_Field.thy:
+ floor now is defined as parameter of a separate type class floor_ceiling.
+
* Finite_Set.thy: more coherent development of fold_set locales:
locale fun_left_comm ~> locale comp_fun_commute
--- a/src/HOL/Archimedean_Field.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy Sun Jul 10 21:46:41 2011 +0200
@@ -141,9 +141,9 @@
subsection {* Floor function *}
-definition
- floor :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+class floor_ceiling = archimedean_field +
+ fixes floor :: "'a \<Rightarrow> int"
+ assumes floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
notation (xsymbols)
floor ("\<lfloor>_\<rfloor>")
@@ -151,9 +151,6 @@
notation (HTML output)
floor ("\<lfloor>_\<rfloor>")
-lemma floor_correct: "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
- unfolding floor_def using floor_exists1 by (rule theI')
-
lemma floor_unique: "\<lbrakk>of_int z \<le> x; x < of_int z + 1\<rbrakk> \<Longrightarrow> floor x = z"
using floor_correct [of x] floor_exists1 [of x] by auto
@@ -273,8 +270,8 @@
subsection {* Ceiling function *}
definition
- ceiling :: "'a::archimedean_field \<Rightarrow> int" where
- [code del]: "ceiling x = - floor (- x)"
+ ceiling :: "'a::floor_ceiling \<Rightarrow> int" where
+ "ceiling x = - floor (- x)"
notation (xsymbols)
ceiling ("\<lceil>_\<rceil>")
--- a/src/HOL/Complete_Lattice.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Sun Jul 10 21:46:41 2011 +0200
@@ -85,47 +85,47 @@
lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
-lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
by (auto intro: Sup_least dest: Sup_upper)
lemma Inf_mono:
assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
- shows "Inf A \<sqsubseteq> Inf B"
+ shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
proof (rule Inf_greatest)
fix b assume "b \<in> B"
with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
- from `a \<in> A` have "Inf A \<sqsubseteq> a" by (rule Inf_lower)
- with `a \<sqsubseteq> b` show "Inf A \<sqsubseteq> b" by auto
+ from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
+ with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
qed
lemma Sup_mono:
assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
- shows "Sup A \<sqsubseteq> Sup B"
+ shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
proof (rule Sup_least)
fix a assume "a \<in> A"
with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
- from `b \<in> B` have "b \<sqsubseteq> Sup B" by (rule Sup_upper)
- with `a \<sqsubseteq> b` show "a \<sqsubseteq> Sup B" by auto
+ from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
+ with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
qed
lemma top_le:
- "top \<sqsubseteq> x \<Longrightarrow> x = top"
+ "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
by (rule antisym) auto
lemma le_bot:
- "x \<sqsubseteq> bot \<Longrightarrow> x = bot"
+ "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
by (rule antisym) auto
-lemma not_less_bot[simp]: "\<not> (x \<sqsubset> bot)"
+lemma not_less_bot[simp]: "\<not> (x \<sqsubset> \<bottom>)"
using bot_least[of x] by (auto simp: le_less)
-lemma not_top_less[simp]: "\<not> (top \<sqsubset> x)"
+lemma not_top_less[simp]: "\<not> (\<top> \<sqsubset> x)"
using top_greatest[of x] by (auto simp: le_less)
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> Sup A"
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
using Sup_upper[of u A] by auto
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> Inf A \<sqsubseteq> v"
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
using Inf_lower[of u A] by auto
definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -172,22 +172,22 @@
lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
by (simp add: INFI_def cong: image_cong)
-lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
+lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
by (auto simp add: SUPR_def intro: Sup_upper)
-lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (SUP i:A. M i)"
+lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
using le_SUPI[of i A M] by auto
-lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
+lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
by (auto simp add: SUPR_def intro: Sup_least)
-lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
+lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
by (auto simp add: INFI_def intro: Inf_lower)
-lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> u"
+lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
using INF_leI[of i A M] by auto
-lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
+lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
by (auto simp add: INFI_def intro: Inf_greatest)
lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
@@ -328,60 +328,75 @@
by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
qed
-lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
+lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
by (unfold Inter_eq) blast
-lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
+lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
by (simp add: Inter_eq)
text {*
\medskip A ``destruct'' rule -- every @{term X} in @{term C}
- contains @{term A} as an element, but @{prop "A:X"} can hold when
- @{prop "X:C"} does not! This rule is analogous to @{text spec}.
+ contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
+ @{prop "X \<in> C"} does not! This rule is analogous to @{text spec}.
*}
-lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
+lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
by auto
-lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
+lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
-- {* ``Classical'' elimination rule -- does not require proving
- @{prop "X:C"}. *}
+ @{prop "X \<in> C"}. *}
by (unfold Inter_eq) blast
-lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
- by blast
+lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
+ by (fact Inf_lower)
+
+lemma (in complete_lattice) Inf_less_eq:
+ assumes "\<And>v. v \<in> A \<Longrightarrow> v \<sqsubseteq> u"
+ and "A \<noteq> {}"
+ shows "\<Sqinter>A \<le> u"
+proof -
+ from `A \<noteq> {}` obtain v where "v \<in> A" by blast
+ moreover with assms have "v \<sqsubseteq> u" by blast
+ ultimately show ?thesis by (rule Inf_lower2)
+qed
lemma Inter_subset:
"[| !!X. X \<in> A ==> X \<subseteq> B; A ~= {} |] ==> \<Inter>A \<subseteq> B"
- by blast
+ by (fact Inf_less_eq)
lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
- by (iprover intro: InterI subsetI dest: subsetD)
+ by (fact Inf_greatest)
lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by blast
+ by (fact Inf_binary [symmetric])
lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
by (fact Inf_empty)
lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
- by blast
+ by (fact Inf_UNIV)
lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
- by blast
+ by (fact Inf_insert)
+
+lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+ by (auto intro: Inf_greatest Inf_lower)
lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
- by blast
+ by (fact Inf_inter_less)
+
+(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
by blast
lemma Inter_UNIV_conv [simp,no_atp]:
- "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
- "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
+ "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
+ "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
by blast+
-lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
+lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
by blast
--- a/src/HOL/IMP/C_like.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/IMP/C_like.thy Sun Jul 10 21:46:41 2011 +0200
@@ -49,6 +49,7 @@
code_pred big_step .
+declare [[values_timeout = 3600]]
text{* Examples: *}
--- a/src/HOL/Rat.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/Rat.thy Sun Jul 10 21:46:41 2011 +0200
@@ -739,6 +739,20 @@
qed
qed
+instantiation rat :: floor_ceiling
+begin
+
+definition [code del]:
+ "floor (x::rat) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+ fix x :: rat
+ show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+ unfolding floor_rat_def using floor_exists1 by (rule theI')
+qed
+
+end
+
lemma floor_Fract: "floor (Fract a b) = a div b"
using rat_floor_lemma [of a b]
by (simp add: floor_unique)
@@ -1083,6 +1097,10 @@
by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract)
qed
+lemma rat_floor_code [code]:
+ "floor p = (let (a, b) = quotient_of p in a div b)"
+by (cases p) (simp add: quotient_of_Fract floor_Fract)
+
instantiation rat :: equal
begin
--- a/src/HOL/RealDef.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/RealDef.thy Sun Jul 10 21:46:41 2011 +0200
@@ -793,6 +793,20 @@
done
qed
+instantiation real :: floor_ceiling
+begin
+
+definition [code del]:
+ "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+
+instance proof
+ fix x :: real
+ show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
+ unfolding floor_real_def using floor_exists1 by (rule theI')
+qed
+
+end
+
subsection {* Completeness *}
lemma not_positive_Real:
@@ -1748,6 +1762,9 @@
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
+lemma real_floor_code [code]: "floor (Ratreal x) = floor x"
+ by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)
+
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Evaluation.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
[code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\<cdot>} k"
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Jul 10 21:46:41 2011 +0200
@@ -814,7 +814,7 @@
fun dest_Char (Symbol.Char s) = s
-val string_of = concat o map (dest_Char o Symbol.decode)
+val string_of = implode o map (dest_Char o Symbol.decode)
val is_atom_ident = forall Symbol.is_ascii_lower
--- a/src/HOL/ex/Quickcheck_Examples.thy Sun Jul 10 20:59:04 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy Sun Jul 10 21:46:41 2011 +0200
@@ -294,6 +294,29 @@
quickcheck[random, size = 10]
oops
+subsubsection {* floor and ceiling functions *}
+
+lemma
+ "floor x + floor y = floor (x + y :: rat)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "floor x + floor y = floor (x + y :: real)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "ceiling x + ceiling y = ceiling (x + y :: rat)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "ceiling x + ceiling y = ceiling (x + y :: real)"
+quickcheck[expect = counterexample]
+oops
+
+
subsection {* Examples with Records *}
record point =