declare more simp rules, rewrite proofs in Isar-style

--- a/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 16:41:31 2010 +0100
+++ b/src/HOL/HOLCF/Bifinite.thy	Tue Dec 21 08:43:39 2010 -0800
@@ -33,7 +33,7 @@
 apply (rule finite_deflation_approx)
 done
 
-lemma compact_approx: "compact (approx n\<cdot>x)"
+lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
 apply (rule finite_deflation.compact)
 apply (rule finite_deflation_approx)
 done

--- a/src/HOL/HOLCF/Universal.thy	Tue Dec 21 16:41:31 2010 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Tue Dec 21 08:43:39 2010 -0800
@@ -250,9 +250,13 @@
 typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}"
 by auto
 
-lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
+lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)"
 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
 
+lemma Abs_compact_basis_inverse' [simp]:
+   "compact x \<Longrightarrow> Rep_compact_basis (Abs_compact_basis x) = x"
+by (rule Abs_compact_basis_inverse [unfolded mem_Collect_eq])
+
 instantiation compact_basis :: (pcpo) below
 begin
 
@@ -276,7 +280,7 @@
   "compact_bot = Abs_compact_basis \<bottom>"
 
 lemma Rep_compact_bot [simp]: "Rep_compact_basis compact_bot = \<bottom>"
-unfolding compact_bot_def by (simp add: Abs_compact_basis_inverse)
+unfolding compact_bot_def by simp
 
 lemma compact_bot_minimal [simp]: "compact_bot \<sqsubseteq> a"
 unfolding compact_le_def Rep_compact_bot by simp
@@ -419,7 +423,7 @@
 
 lemma Rep_cb_take:
   "Rep_compact_basis (cb_take (Suc n) a) = approx n\<cdot>(Rep_compact_basis a)"
-by (simp add: Abs_compact_basis_inverse cb_take.simps(2) compact_approx)
+by (simp add: cb_take.simps(2))
 
 lemmas approx_Rep_compact_basis = Rep_cb_take [symmetric]
 
@@ -428,7 +432,7 @@
 apply (simp add: Rep_compact_basis_inject [symmetric])
 apply (simp add: Rep_cb_take)
 apply (rule compact_eq_approx)
-apply (rule compact_Rep_compact_basis)
+apply (rule Rep_compact_basis')
 done
 
 lemma cb_take_less: "cb_take n x \<sqsubseteq> x"
@@ -783,61 +787,49 @@
   fix w :: "'a"
   show "below.ideal (approximants w)"
   proof (rule below.idealI)
-    show "\<exists>x. x \<in> approximants w"
-      unfolding approximants_def
-      apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
-      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
-      done
+    have "Abs_compact_basis (approx 0\<cdot>w) \<in> approximants w"
+      by (simp add: approximants_def approx_below)
+    thus "\<exists>x. x \<in> approximants w" ..
   next
     fix x y :: "'a compact_basis"
-    assume "x \<in> approximants w" "y \<in> approximants w"
-    thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-      unfolding approximants_def
-      apply simp
-      apply (cut_tac a=x in compact_Rep_compact_basis)
-      apply (cut_tac a=y in compact_Rep_compact_basis)
-      apply (drule compact_eq_approx)
-      apply (drule compact_eq_approx)
-      apply (clarify, rename_tac i j)
-      apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
-      apply (simp add: compact_le_def)
-      apply (simp add: Abs_compact_basis_inverse approx_below compact_approx)
-      apply (erule subst, erule subst)
-      apply (simp add: monofun_cfun chain_mono [OF chain_approx])
-      done
+    assume x: "x \<in> approximants w" and y: "y \<in> approximants w"
+    obtain i where i: "approx i\<cdot>(Rep_compact_basis x) = Rep_compact_basis x"
+      using compact_eq_approx Rep_compact_basis' by fast
+    obtain j where j: "approx j\<cdot>(Rep_compact_basis y) = Rep_compact_basis y"
+      using compact_eq_approx Rep_compact_basis' by fast
+    let ?z = "Abs_compact_basis (approx (max i j)\<cdot>w)"
+    have "?z \<in> approximants w"
+      by (simp add: approximants_def approx_below)
+    moreover from x y have "x \<sqsubseteq> ?z \<and> y \<sqsubseteq> ?z"
+      by (simp add: approximants_def compact_le_def)
+         (metis i j monofun_cfun chain_mono chain_approx le_maxI1 le_maxI2)
+    ultimately show "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
   next
     fix x y :: "'a compact_basis"
     assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
-      unfolding approximants_def
-      apply simp
-      apply (simp add: compact_le_def)
-      apply (erule (1) below_trans)
-      done
+      unfolding approximants_def compact_le_def
+      by (auto elim: below_trans)
   qed
 next
   fix Y :: "nat \<Rightarrow> 'a"
-  assume Y: "chain Y"
-  show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
+  assume "chain Y"
+  thus "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
     unfolding approximants_def
-    apply safe
-    apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
-    apply (erule below_lub [OF Y])
-    done
+    by (auto simp add: compact_below_lub_iff)
 next
   fix a :: "'a compact_basis"
   show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
     unfolding approximants_def compact_le_def ..
 next
   fix x y :: "'a"
-  assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
-    apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y")
-    apply (simp add: lub_distribs)
-    apply (rule admD, simp, simp)
-    apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
-    apply (simp add: approximants_def Abs_compact_basis_inverse
-                     approx_below compact_approx)
-    apply (simp add: approximants_def Abs_compact_basis_inverse compact_approx)
-    done
+  assume "approximants x \<subseteq> approximants y"
+  hence "\<forall>z. compact z \<longrightarrow> z \<sqsubseteq> x \<longrightarrow> z \<sqsubseteq> y"
+    by (simp add: approximants_def subset_eq)
+       (metis Abs_compact_basis_inverse')
+  hence "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y"
+    by (simp add: lub_below approx_below)
+  thus "x \<sqsubseteq> y"
+    by (simp add: lub_distribs)
 next
   show "\<exists>f::'a compact_basis \<Rightarrow> nat. inj f"
     by (rule exI, rule inj_place)