--- a/src/HOL/Archimedean_Field.thy Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Jun 17 09:44:16 2016 +0200
@@ -8,6 +8,63 @@
imports Main
begin
+lemma cInf_abs_ge:
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+ assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
+ shows "\<bar>Inf S\<bar> \<le> a"
+proof -
+ have "Sup (uminus ` S) = - (Inf S)"
+ proof (rule antisym)
+ show "- (Inf S) \<le> Sup(uminus ` S)"
+ apply (subst minus_le_iff)
+ apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
+ apply (subst minus_le_iff)
+ apply (rule cSup_upper, force)
+ using bdd apply (force simp add: abs_le_iff bdd_above_def)
+ done
+ next
+ show "Sup (uminus ` S) \<le> - Inf S"
+ apply (rule cSup_least)
+ using \<open>S \<noteq> {}\<close> apply (force simp add: )
+ apply clarsimp
+ apply (rule cInf_lower)
+ apply assumption
+ using bdd apply (simp add: bdd_below_def)
+ apply (rule_tac x="-a" in exI)
+ apply force
+ done
+ qed
+ with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
+qed
+
+lemma cSup_asclose:
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+ assumes S: "S \<noteq> {}"
+ and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+ shows "\<bar>Sup S - l\<bar> \<le> e"
+proof -
+ have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+ by arith
+ have "bdd_above S"
+ using b by (auto intro!: bdd_aboveI[of _ "l + e"])
+ with S b show ?thesis
+ unfolding th by (auto intro!: cSup_upper2 cSup_least)
+qed
+
+lemma cInf_asclose:
+ fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
+ assumes S: "S \<noteq> {}"
+ and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
+ shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+ have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
+ by arith
+ have "bdd_below S"
+ using b by (auto intro!: bdd_belowI[of _ "l - e"])
+ with S b show ?thesis
+ unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
+qed
+
subsection \<open>Class of Archimedean fields\<close>
text \<open>Archimedean fields have no infinite elements.\<close>
@@ -329,10 +386,10 @@
also have "\<dots> = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
using False by (simp only: of_int_add) (simp add: field_simps)
finally have "(of_int k / of_int l :: 'a) = \<dots> / of_int l"
- by simp
+ by simp
then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
using False by (simp only:) (simp add: field_simps)
- then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>"
+ then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k div l) + of_int (k mod l) / of_int l :: 'a\<rfloor>"
by simp
then have "\<lfloor>of_int k / of_int l :: 'a\<rfloor> = \<lfloor>of_int (k mod l) / of_int l + of_int (k div l) :: 'a\<rfloor>"
by (simp add: ac_simps)
@@ -355,10 +412,10 @@
also have "\<dots> = (of_nat (m div n) + of_nat (m mod n) / of_nat n) * of_nat n"
using False by (simp only: of_nat_add) (simp add: field_simps of_nat_mult)
finally have "(of_nat m / of_nat n :: 'a) = \<dots> / of_nat n"
- by simp
+ by simp
then have "(of_nat m / of_nat n :: 'a) = of_nat (m div n) + of_nat (m mod n) / of_nat n"
using False by (simp only:) simp
- then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
+ then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m div n) + of_nat (m mod n) / of_nat n :: 'a\<rfloor>"
by simp
then have "\<lfloor>of_nat m / of_nat n :: 'a\<rfloor> = \<lfloor>of_nat (m mod n) / of_nat n + of_nat (m div n) :: 'a\<rfloor>"
by (simp add: ac_simps)
@@ -376,7 +433,7 @@
where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
- unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff)
+ unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff)
lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> \<lceil>x\<rceil> = z"
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
@@ -512,7 +569,7 @@
lemma ceiling_diff_floor_le_1: "\<lceil>x\<rceil> - \<lfloor>x\<rfloor> \<le> 1"
proof -
- have "of_int \<lceil>x\<rceil> - 1 < x"
+ have "of_int \<lceil>x\<rceil> - 1 < x"
using ceiling_correct[of x] by simp
also have "x < of_int \<lfloor>x\<rfloor> + 1"
using floor_correct[of x] by simp_all
@@ -552,7 +609,7 @@
lemma frac_of_int [simp]: "frac (of_int z) = 0"
by (simp add: frac_def)
-lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
+lemma floor_add: "\<lfloor>x + y\<rfloor> = (if frac x + frac y < 1 then \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor> else (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>) + 1)"
proof -
{assume "x + y < 1 + (of_int \<lfloor>x\<rfloor> + of_int \<lfloor>y\<rfloor>)"
then have "\<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
@@ -563,14 +620,14 @@
then have "\<lfloor>x + y\<rfloor> = 1 + (\<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>)"
apply (simp add: floor_unique_iff)
apply (auto simp add: algebra_simps)
- by linarith
+ by linarith
}
ultimately show ?thesis
by (auto simp add: frac_def algebra_simps)
qed
lemma frac_add: "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y
- else (frac x + frac y) - 1)"
+ else (frac x + frac y) - 1)"
by (simp add: frac_def floor_add)
lemma frac_unique_iff:
@@ -582,7 +639,7 @@
lemma frac_eq: "(frac x) = x \<longleftrightarrow> 0 \<le> x \<and> x < 1"
by (simp add: frac_unique_iff)
-
+
lemma frac_neg:
fixes x :: "'a::floor_ceiling"
shows "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
@@ -643,8 +700,8 @@
unfolding round_def by (intro floor_mono) simp
lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
-
-lemma round_diff_minimal:
+
+lemma round_diff_minimal:
fixes z :: "'a :: floor_ceiling"
shows "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
proof (cases "of_int m \<ge> z")
--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jun 17 09:44:16 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Conditionally-complete Lattices\<close>
theory Conditionally_Complete_Lattices
-imports Main
+imports Finite_Set Lattices_Big Set_Interval
begin
lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
@@ -107,7 +107,7 @@
lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
by (auto simp: bdd_below_def mono_def)
-
+
lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
by (auto simp: bdd_above_def bdd_below_def antimono_def)
@@ -394,7 +394,7 @@
class conditionally_complete_linorder = conditionally_complete_lattice + linorder
begin
-lemma less_cSup_iff : (*REAL_SUP_LE in HOL4*)
+lemma less_cSup_iff:
"X \<noteq> {} \<Longrightarrow> bdd_above X \<Longrightarrow> y < Sup X \<longleftrightarrow> (\<exists>x\<in>X. y < x)"
by (rule iffI) (metis cSup_least not_less, metis cSup_upper less_le_trans)
@@ -429,7 +429,7 @@
(metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le)
next
show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
- apply (rule cSup_least)
+ apply (rule cSup_least)
apply auto
apply (metis less_le_not_le)
apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le)
@@ -440,7 +440,7 @@
show "P x"
apply (rule less_cSupE [OF lt], auto)
apply (metis less_le_not_le)
- apply (metis x)
+ apply (metis x)
done
next
fix d
@@ -512,7 +512,7 @@
unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
{ assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
by (simp add: Sup_nat_def bdd_above_nat) }
- { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
+ { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
moreover then have "bdd_above X"
by (auto simp: bdd_above_def)
ultimately show "Sup X \<le> x"
@@ -593,7 +593,7 @@
define lower upper where "lower = {x. \<exists>s\<in>S. s \<le> x}" and "upper = {x. \<exists>s\<in>S. x \<le> s}"
with ivl have "S = lower \<inter> upper"
by auto
- moreover
+ moreover
have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}"
proof cases
assume *: "bdd_above S \<and> S \<noteq> {}"
@@ -644,7 +644,7 @@
using a bdd
apply (auto simp: cINF_lower)
apply (metis eq cSUP_upper)
-done
+done
lemma cSUP_UNION:
fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
@@ -686,67 +686,10 @@
by (rule order_antisym)
qed
-lemma cSup_abs_le:
+lemma cSup_abs_le:
fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
apply (auto simp add: abs_le_iff intro: cSup_least)
by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
-lemma cInf_abs_ge:
- fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
- assumes "S \<noteq> {}" and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
- shows "\<bar>Inf S\<bar> \<le> a"
-proof -
- have "Sup (uminus ` S) = - (Inf S)"
- proof (rule antisym)
- show "- (Inf S) \<le> Sup(uminus ` S)"
- apply (subst minus_le_iff)
- apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
- apply (subst minus_le_iff)
- apply (rule cSup_upper, force)
- using bdd apply (force simp add: abs_le_iff bdd_above_def)
- done
- next
- show "Sup (uminus ` S) \<le> - Inf S"
- apply (rule cSup_least)
- using \<open>S \<noteq> {}\<close> apply (force simp add: )
- apply clarsimp
- apply (rule cInf_lower)
- apply assumption
- using bdd apply (simp add: bdd_below_def)
- apply (rule_tac x="-a" in exI)
- apply force
- done
- qed
- with cSup_abs_le [of "uminus ` S"] assms show ?thesis by fastforce
-qed
-
-lemma cSup_asclose:
- fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
- assumes S: "S \<noteq> {}"
- and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
- shows "\<bar>Sup S - l\<bar> \<le> e"
-proof -
- have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
- by arith
- have "bdd_above S"
- using b by (auto intro!: bdd_aboveI[of _ "l + e"])
- with S b show ?thesis
- unfolding th by (auto intro!: cSup_upper2 cSup_least)
-qed
-
-lemma cInf_asclose:
- fixes S :: "('a::{linordered_idom,conditionally_complete_linorder}) set"
- assumes S: "S \<noteq> {}"
- and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
- shows "\<bar>Inf S - l\<bar> \<le> e"
-proof -
- have th: "\<And>(x::'a) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
- by arith
- have "bdd_below S"
- using b by (auto intro!: bdd_belowI[of _ "l - e"])
- with S b show ?thesis
- unfolding th by (auto intro!: cInf_lower2 cInf_greatest)
-qed
-
end
--- a/src/HOL/Library/FSet.thy Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Library/FSet.thy Fri Jun 17 09:44:16 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Type of finite sets defined as a subtype of sets\<close>
theory FSet
-imports Conditionally_Complete_Lattices
+imports Main
begin
subsection \<open>Definition of the type\<close>
@@ -31,18 +31,18 @@
interpretation lifting_syntax .
-lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
+lift_definition bot_fset :: "'a fset" is "{}" parametric empty_transfer by simp
-lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
+lift_definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" is subset_eq parametric subset_transfer
.
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"
lemma less_fset_transfer[transfer_rule]:
- assumes [transfer_rule]: "bi_unique A"
+ assumes [transfer_rule]: "bi_unique A"
shows "((pcr_fset A) ===> (pcr_fset A) ===> op =) op \<subset> op <"
unfolding less_fset_def[abs_def] psubset_eq[abs_def] by transfer_prover
-
+
lift_definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is union parametric union_transfer
by simp
@@ -69,7 +69,7 @@
begin
definition "HOL.equal A B \<longleftrightarrow> A |\<subseteq>| B \<and> B |\<subseteq>| A"
instance by intro_classes (auto simp add: equal_fset_def)
-end
+end
instantiation fset :: (type) conditionally_complete_lattice
begin
@@ -78,18 +78,18 @@
lemma right_total_Inf_fset_transfer:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
- shows "(rel_set (rel_set A) ===> rel_set A)
- (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {})
+ shows "(rel_set (rel_set A) ===> rel_set A)
+ (\<lambda>S. if finite (\<Inter>S \<inter> Collect (Domainp A)) then \<Inter>S \<inter> Collect (Domainp A) else {})
(\<lambda>S. if finite (Inf S) then Inf S else {})"
by transfer_prover
lemma Inf_fset_transfer:
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
- shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {})
+ shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>A. if finite (Inf A) then Inf A else {})
(\<lambda>A. if finite (Inf A) then Inf A else {})"
by transfer_prover
-lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}"
+lift_definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" is "\<lambda>A. if finite (Inf A) then Inf A else {}"
parametric right_total_Inf_fset_transfer Inf_fset_transfer by simp
lemma Sup_fset_transfer:
@@ -107,11 +107,11 @@
by auto
instance
-proof
+proof
fix x z :: "'a fset"
fix X :: "'a fset set"
{
- assume "x \<in> X" "bdd_below X"
+ assume "x \<in> X" "bdd_below X"
then show "Inf X |\<subseteq>| x" by transfer auto
next
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)"
@@ -129,7 +129,7 @@
qed
end
-instantiation fset :: (finite) complete_lattice
+instantiation fset :: (finite) complete_lattice
begin
lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
@@ -143,7 +143,7 @@
instantiation fset :: (finite) complete_boolean_algebra
begin
-lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus
+lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus
parametric right_total_Compl_transfer Compl_transfer by simp
instance
@@ -169,7 +169,7 @@
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
-lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
+lift_definition fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is Set.member
parametric member_transfer .
abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
@@ -179,20 +179,20 @@
interpretation lifting_syntax .
-lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
+lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter
parametric Lifting_Set.filter_transfer unfolding Set.filter_def by simp
-lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
+lift_definition fPow :: "'a fset \<Rightarrow> 'a fset fset" is Pow parametric Pow_transfer
by (simp add: finite_subset)
lift_definition fcard :: "'a fset \<Rightarrow> nat" is card parametric card_transfer .
-lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image
+lift_definition fimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" (infixr "|`|" 90) is image
parametric image_transfer by simp
lift_definition fthe_elem :: "'a fset \<Rightarrow> 'a" is the_elem .
-lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
+lift_definition fbind :: "'a fset \<Rightarrow> ('a \<Rightarrow> 'b fset) \<Rightarrow> 'b fset" is Set.bind parametric bind_transfer
by (simp add: Set.bind_def)
lift_definition ffUnion :: "'a fset fset \<Rightarrow> 'a fset" is Union parametric Union_transfer by simp
@@ -464,7 +464,7 @@
lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
-lemma finite_fset [simp]:
+lemma finite_fset [simp]:
shows "finite (fset S)"
by transfer simp
@@ -485,16 +485,16 @@
subsubsection \<open>\<open>filter_fset\<close>\<close>
-lemma subset_ffilter:
+lemma subset_ffilter:
"ffilter P A |\<subseteq>| ffilter Q A = (\<forall> x. x |\<in>| A \<longrightarrow> P x \<longrightarrow> Q x)"
by transfer auto
-lemma eq_ffilter:
+lemma eq_ffilter:
"(ffilter P A = ffilter Q A) = (\<forall>x. x |\<in>| A \<longrightarrow> P x = Q x)"
by transfer auto
lemma pfsubset_ffilter:
- "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow>
+ "(\<And>x. x |\<in>| A \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| A & \<not> P x & Q x) \<Longrightarrow>
ffilter P A |\<subset>| ffilter Q A"
unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
@@ -520,9 +520,9 @@
subsubsection \<open>bounded quantification\<close>
lemma bex_simps [simp, no_atp]:
- "\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)"
+ "\<And>A P Q. fBex A (\<lambda>x. P x \<and> Q) = (fBex A P \<and> Q)"
"\<And>A P Q. fBex A (\<lambda>x. P \<and> Q x) = (P \<and> fBex A Q)"
- "\<And>P. fBex {||} P = False"
+ "\<And>P. fBex {||} P = False"
"\<And>a B P. fBex (finsert a B) P = (P a \<or> fBex B P)"
"\<And>A P f. fBex (f |`| A) P = fBex A (\<lambda>x. P (f x))"
"\<And>A P. (\<not> fBex A P) = fBall A (\<lambda>x. \<not> P x)"
@@ -601,7 +601,7 @@
lemma pfsubset_fcard_mono: "A |\<subset>| B \<Longrightarrow> fcard A < fcard B"
by transfer (rule psubset_card_mono)
-lemma fcard_funion_finter:
+lemma fcard_funion_finter:
"fcard A + fcard B = fcard (A |\<union>| B) + fcard (A |\<inter>| B)"
by transfer (rule card_Un_Int)
@@ -656,7 +656,7 @@
assumes "x |\<in>| A"
shows "ffold f z A = f x (ffold f z (A |-| {|x|}))"
using assms by (transfer fixing: f) (rule fold_rec)
-
+
lemma ffold_finsert_fremove:
"ffold f z (finsert x A) = f x (ffold f z (A |-| {|x|}))"
by (transfer fixing: f) (rule fold_insert_remove)
@@ -680,9 +680,9 @@
lemma ffold_finsert_idem:
"ffold f z (finsert x A) = f x (ffold f z A)"
by (transfer fixing: f) (rule fold_insert_idem)
-
+
declare ffold_finsert [simp del] ffold_finsert_idem [simp]
-
+
lemma ffold_finsert_idem2:
"ffold f z (finsert x A) = ffold f (f x z) A"
by (transfer fixing: f) (rule fold_insert_idem2)
@@ -692,7 +692,7 @@
subsection \<open>Choice in fsets\<close>
-lemma fset_choice:
+lemma fset_choice:
assumes "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
using assms by transfer metis
@@ -701,7 +701,7 @@
subsection \<open>Induction and Cases rules for fsets\<close>
lemma fset_exhaust [case_names empty insert, cases type: fset]:
- assumes fempty_case: "S = {||} \<Longrightarrow> P"
+ assumes fempty_case: "S = {||} \<Longrightarrow> P"
and finsert_case: "\<And>x S'. S = finsert x S' \<Longrightarrow> P"
shows "P"
using assms by transfer blast
@@ -739,9 +739,9 @@
case (insert x S)
have h: "P S" by fact
have "x |\<notin>| S" by fact
- then have "Suc (fcard S) = fcard (finsert x S)"
+ then have "Suc (fcard S) = fcard (finsert x S)"
by transfer auto
- then show "P (finsert x S)"
+ then show "P (finsert x S)"
using h card_fset_Suc_case by simp
qed
@@ -771,11 +771,11 @@
lift_definition rel_fset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" is rel_set
parametric rel_set_transfer .
-lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
+lemma rel_fset_alt_def: "rel_fset R = (\<lambda>A B. (\<forall>x.\<exists>y. x|\<in>|A \<longrightarrow> y|\<in>|B \<and> R x y)
\<and> (\<forall>y. \<exists>x. y|\<in>|B \<longrightarrow> x|\<in>|A \<and> R x y))"
apply (rule ext)+
apply transfer'
-apply (subst rel_set_def[unfolded fun_eq_iff])
+apply (subst rel_set_def[unfolded fun_eq_iff])
by blast
lemma finite_rel_set:
@@ -787,12 +787,12 @@
apply atomize_elim
apply (subst bchoice_iff[symmetric])
using R_S[unfolded rel_set_def OO_def] by blast
-
+
obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
apply atomize_elim
apply (subst bchoice_iff[symmetric])
using R_S[unfolded rel_set_def OO_def] by blast
-
+
let ?Y = "f ` X \<union> g ` Z"
have "finite ?Y" by (simp add: fin)
moreover have "rel_set R X ?Y"
@@ -960,7 +960,7 @@
bnf "'a fset"
map: fimage
- sets: fset
+ sets: fset
bd: natLeq
wits: "{||}"
rel: rel_fset
@@ -974,7 +974,7 @@
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
apply (fastforce simp: rel_fset_alt)
apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff rel_fset_alt
- rel_fset_aux[unfolded OO_Grp_alt])
+ rel_fset_aux[unfolded OO_Grp_alt])
apply transfer apply simp
done
@@ -1009,7 +1009,7 @@
lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
apply (subst fun_eq_iff)
including fset.lifting by transfer (auto intro: setsum.reindex_cong subset_inj_on)
-
+
setup \<open>
BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
@{thm size_fset_overloaded_def} @{thms size_fset_simps size_fset_overloaded_simps}
@@ -1023,8 +1023,8 @@
(* Set vs. sum relators: *)
-lemma rel_set_rel_sum[simp]:
-"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
+lemma rel_set_rel_sum[simp]:
+"rel_set (rel_sum \<chi> \<phi>) A1 A2 \<longleftrightarrow>
rel_set \<chi> (Inl -` A1) (Inl -` A2) \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)"
(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
proof safe
--- a/src/HOL/Main.thy Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Main.thy Fri Jun 17 09:44:16 2016 +0200
@@ -1,7 +1,7 @@
section \<open>Main HOL\<close>
theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter
+imports Predicate_Compile Quickcheck_Narrowing Extraction Coinduction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
begin
text \<open>
--- a/src/HOL/Real.thy Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Real.thy Fri Jun 17 09:44:16 2016 +0200
@@ -10,7 +10,7 @@
section \<open>Development of the Reals using Cauchy Sequences\<close>
theory Real
-imports Rat Conditionally_Complete_Lattices
+imports Rat
begin
text \<open>
@@ -961,7 +961,6 @@
qed
end
-
subsection \<open>Hiding implementation details\<close>
hide_const (open) vanishes cauchy positive Real