# HG changeset patch
# User huffman
# Date 1291668786 28800
# Node ID 7a67a8832da81e514534572e9bfad7eb7e93f0a0
# Parent  75b4ff66781cc599ab9e040bbeb15c5307fb929c
simplify ideal completion proofs

diff -r 75b4ff66781c -r 7a67a8832da8 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Mon Dec 06 11:44:30 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy	Mon Dec 06 12:53:06 2010 -0800
@@ -52,17 +52,6 @@
 lemma ex_ideal: "\<exists>A. A \<in> {A. ideal A}"
 by (fast intro: ideal_principal)
 
-lemma lub_image_principal:
-  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-  shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
-apply (rule lub_eqI)
-apply (rule is_lub_maximal)
-apply (rule ub_imageI)
-apply (simp add: f)
-apply (rule imageI)
-apply (simp add: r_refl)
-done
-
 text {* The set of ideals is a cpo *}
 
 lemma ideal_UN:
@@ -156,7 +145,7 @@
   assumes ideal_rep: "\<And>x. ideal (rep x)"
   assumes rep_lub: "\<And>Y. chain Y \<Longrightarrow> rep (\<Squnion>i. Y i) = (\<Union>i. rep (Y i))"
   assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
-  assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
+  assumes belowI: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
   assumes countable: "\<exists>f::'a \<Rightarrow> nat. inj f"
 begin
 
@@ -168,20 +157,11 @@
 done
 
 lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
-by (rule iffI [OF rep_mono subset_repD])
-
-lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
-unfolding below_def rep_principal
-apply safe
-apply (erule (1) idealD3 [OF ideal_rep])
-apply (erule subsetD, simp add: r_refl)
-done
-
-lemma mem_rep_iff_principal_below: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
-by (simp add: rep_eq)
+by (rule iffI [OF rep_mono belowI])
 
 lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
-by (simp add: rep_eq)
+unfolding below_def rep_principal
+by (auto intro: r_refl elim: idealD3 [OF ideal_rep])
 
 lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
 by (simp add: principal_below_iff_mem_rep rep_principal)
@@ -192,9 +172,6 @@
 lemma eq_iff: "x = y \<longleftrightarrow> rep x = rep y"
 unfolding po_eq_conv below_def by auto
 
-lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
-by (simp add: rep_eq)
-
 lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
 by (simp only: principal_below_iff)
 
@@ -202,16 +179,6 @@
   "\<forall>i. Y i \<preceq> Y (Suc i) \<Longrightarrow> chain (\<lambda>i. principal (Y i))"
 by (simp add: chainI principal_mono)
 
-lemma lub_principal_rep: "principal ` rep x <<| x"
-apply (rule is_lubI)
-apply (rule ub_imageI)
-apply (erule repD)
-apply (subst below_def)
-apply (rule subsetI)
-apply (drule (1) ub_imageD)
-apply (simp add: rep_eq)
-done
-
 subsubsection {* Principal ideals approximate all elements *}
 
 lemma compact_principal [simp]: "compact (principal a)"
@@ -321,13 +288,6 @@
 apply (drule (2) admD2, fast, simp)
 done
 
-lemma obtain_compact_chain:
-  obtains Y :: "nat \<Rightarrow> 'b"
-  where "chain Y" and "\<forall>i. compact (Y i)" and "x = (\<Squnion>i. Y i)"
-apply (rule obtain_principal_chain [of x])
-apply (rule_tac Y="\<lambda>i. principal (Y i)" in that, simp_all)
-done
-
 subsection {* Defining functions in terms of basis elements *}
 
 definition
@@ -387,7 +347,12 @@
   shows "basis_fun f\<cdot>(principal a) = f a"
 apply (subst basis_fun_beta, erule f_mono)
 apply (subst rep_principal)
-apply (rule lub_image_principal, erule f_mono)
+apply (rule lub_eqI)
+apply (rule is_lub_maximal)
+apply (rule ub_imageI)
+apply (simp add: f_mono)
+apply (rule imageI)
+apply (simp add: r_refl)
 done
 
 lemma basis_fun_mono: