417 lemma cb_take_zero [simp]: "cb_take 0 a = compact_bot" |
421 lemma cb_take_zero [simp]: "cb_take 0 a = compact_bot" |
418 by (simp only: cb_take.simps) |
422 by (simp only: cb_take.simps) |
419 |
423 |
420 lemma Rep_cb_take: |
424 lemma Rep_cb_take: |
421 "Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)" |
425 "Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)" |
422 by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx) |
426 by (simp add: cb_take.simps(2)) |
423 |
427 |
424 lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric] |
428 lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric] |
425 |
429 |
426 lemma cb_take_covers: "\<exists>n. cb_take n x = x" |
430 lemma cb_take_covers: "\<exists>n. cb_take n x = x" |
427 apply (subgoal_tac "\<exists>n. cb_take (Suc n) x = x", fast) |
431 apply (subgoal_tac "\<exists>n. cb_take (Suc n) x = x", fast) |
428 apply (simp add: Rep_compact_basis_inject [symmetric]) |
432 apply (simp add: Rep_compact_basis_inject [symmetric]) |
429 apply (simp add: Rep_cb_take) |
433 apply (simp add: Rep_cb_take) |
430 apply (rule compact_eq_approx) |
434 apply (rule compact_eq_approx) |
431 apply (rule compact_Rep_compact_basis) |
435 apply (rule Rep_compact_basis') |
432 done |
436 done |
433 |
437 |
434 lemma cb_take_less: "cb_take n x \<sqsubseteq> x" |
438 lemma cb_take_less: "cb_take n x \<sqsubseteq> x" |
435 unfolding compact_le_def |
439 unfolding compact_le_def |
436 by (cases n, simp, simp add: Rep_cb_take approx_below) |
440 by (cases n, simp, simp add: Rep_cb_take approx_below) |
781 "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)" |
785 "ideal_completion below Rep_compact_basis (approximants :: 'a \<Rightarrow> _)" |
782 proof |
786 proof |
783 fix w :: "'a" |
787 fix w :: "'a" |
784 show "below.ideal (approximants w)" |
788 show "below.ideal (approximants w)" |
785 proof (rule below.idealI) |
789 proof (rule below.idealI) |
786 show "\<exists>x. x \<in> approximants w" |
790 have "Abs_compact_basis (approx 0\<cdot>w) \<in> approximants w" |
787 unfolding approximants_def |
791 by (simp add: approximants_def approx_below) |
788 apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI) |
792 thus "\<exists>x. x \<in> approximants w" .. |
789 apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) |
|
790 done |
|
791 next |
793 next |
792 fix x y :: "'a compact_basis" |
794 fix x y :: "'a compact_basis" |
793 assume "x \<in> approximants w" "y \<in> approximants w" |
795 assume x: "x \<in> approximants w" and y: "y \<in> approximants w" |
794 thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
796 obtain i where i: "approx i\<cdot>(Rep_compact_basis x) = Rep_compact_basis x" |
795 unfolding approximants_def |
797 using compact_eq_approx Rep_compact_basis' by fast |
796 apply simp |
798 obtain j where j: "approx j\<cdot>(Rep_compact_basis y) = Rep_compact_basis y" |
797 apply (cut_tac a=x in compact_Rep_compact_basis) |
799 using compact_eq_approx Rep_compact_basis' by fast |
798 apply (cut_tac a=y in compact_Rep_compact_basis) |
800 let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)" |
799 apply (drule compact_eq_approx) |
801 have "?z \<in> approximants w" |
800 apply (drule compact_eq_approx) |
802 by (simp add: approximants_def approx_below) |
801 apply (clarify, rename_tac i j) |
803 moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z" |
802 apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI) |
804 by (simp add: approximants_def compact_le_def) |
803 apply (simp add: compact_le_def) |
805 (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2) |
804 apply (simp add: Abs_compact_basis_inverse approx_below compact_approx) |
806 ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" .. |
805 apply (erule subst, erule subst) |
|
806 apply (simp add: monofun_cfun chain_mono [OF chain_approx]) |
|
807 done |
|
808 next |
807 next |
809 fix x y :: "'a compact_basis" |
808 fix x y :: "'a compact_basis" |
810 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" |
809 assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w" |
811 unfolding approximants_def |
810 unfolding approximants_def compact_le_def |
812 apply simp |
811 by (auto elim: below_trans) |
813 apply (simp add: compact_le_def) |
|
814 apply (erule (1) below_trans) |
|
815 done |
|
816 qed |
812 qed |
817 next |
813 next |
818 fix Y :: "nat \<Rightarrow> 'a" |
814 fix Y :: "nat \<Rightarrow> 'a" |
819 assume Y: "chain Y" |
815 assume "chain Y" |
820 show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" |
816 thus "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))" |
821 unfolding approximants_def |
817 unfolding approximants_def |
822 apply safe |
818 by (auto simp add: compact_below_lub_iff) |
823 apply (simp add: compactD2 [OF compact_Rep_compact_basis Y]) |
|
824 apply (erule below_lub [OF Y]) |
|
825 done |
|
826 next |
819 next |
827 fix a :: "'a compact_basis" |
820 fix a :: "'a compact_basis" |
828 show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
821 show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}" |
829 unfolding approximants_def compact_le_def .. |
822 unfolding approximants_def compact_le_def .. |
830 next |
823 next |
831 fix x y :: "'a" |
824 fix x y :: "'a" |
832 assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y" |
825 assume "approximants x \<subseteq> approximants y" |
833 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y") |
826 hence "\<forall>z. compact z \<longrightarrow> z \<sqsubseteq> x \<longrightarrow> z \<sqsubseteq> y" |
834 apply (simp add: lub_distribs) |
827 by (simp add: approximants_def subset_eq) |
835 apply (rule admD, simp, simp) |
828 (metis Abs_compact_basis_inverse') |
836 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD) |
829 hence "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y" |
837 apply (simp add: approximants_def Abs_compact_basis_inverse |
830 by (simp add: lub_below approx_below) |
838 approx_below compact_approx) |
831 thus "x \<sqsubseteq> y" |
839 apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx) |
832 by (simp add: lub_distribs) |
840 done |
|
841 next |
833 next |
842 show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f" |
834 show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f" |
843 by (rule exI, rule inj_place) |
835 by (rule exI, rule inj_place) |
844 qed |
836 qed |
845 |
837 |