# HG changeset patch
# User berghofe
# Date 1173540292 -3600
# Node ID 28344ccffc35a121bf7270271c98a9e6752d7705
# Parent  6a56bf1b3a64997fa8d2f2eca9a854a294789ab5
Adapted to changes in definition of SUP.

diff -r 6a56bf1b3a64 -r 28344ccffc35 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Sat Mar 10 16:23:28 2007 +0100
+++ b/src/HOL/Library/Continuity.thy	Sat Mar 10 16:24:52 2007 +0100
@@ -16,7 +16,7 @@
   "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
 
 definition
-  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
+  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
   "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
 
 abbreviation
@@ -24,12 +24,12 @@
   "bot \<equiv> Sup {}"
 
 lemma SUP_nat_conv:
-  "(SUP n::nat. M n::'a::comp_lat) = sup (M 0) (SUP n. M(Suc n))"
+  "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
 apply(rule order_antisym)
  apply(rule SUP_leI)
  apply(case_tac n)
   apply simp
- apply (blast intro:le_SUPI le_supI2)
+ apply (fast intro:le_SUPI le_supI2)
 apply(simp)
 apply (blast intro:SUP_leI le_SUPI)
 done
@@ -43,10 +43,10 @@
   have "F B = sup (F A) (F B)"
   proof -
     have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
-    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
+    hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
     also have "\<dots> = (SUP i. F(?C i))"
       using `chain ?C` `continuous F` by(simp add:continuous_def)
-    also have "\<dots> = sup (F A) (F B)" by(simp add: SUP_nat_conv)
+    also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
     finally show ?thesis .
   qed
   thus "F A \<le> F B" by(subst le_iff_sup, simp)
@@ -80,7 +80,7 @@
       thus ?thesis by(auto simp add:chain_def)
     qed
     hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
-    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
+    also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
     finally show "F ?U \<le> ?U" .
   qed
   ultimately show ?thesis by (blast intro:order_antisym)
diff -r 6a56bf1b3a64 -r 28344ccffc35 src/HOL/Library/Graphs.thy
--- a/src/HOL/Library/Graphs.thy	Sat Mar 10 16:23:28 2007 +0100
+++ b/src/HOL/Library/Graphs.thy	Sat Mar 10 16:24:52 2007 +0100
@@ -245,7 +245,7 @@
 
 lemma Sup_graph_eq:
   "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
-  unfolding SUP_def 
+  unfolding SUPR_def
   apply (rule order_antisym)
   apply (rule Sup_least)
   apply auto
diff -r 6a56bf1b3a64 -r 28344ccffc35 src/HOL/Library/Kleene_Algebras.thy
--- a/src/HOL/Library/Kleene_Algebras.thy	Sat Mar 10 16:23:28 2007 +0100
+++ b/src/HOL/Library/Kleene_Algebras.thy	Sat Mar 10 16:24:52 2007 +0100
@@ -104,7 +104,7 @@
   assumes "l \<le> M i"
   shows "l \<le> (SUP i. M i)"
   using prems
-  by (rule order_trans) (rule le_SUPI, rule refl)
+  by (rule order_trans) (rule le_SUPI [OF UNIV_I])
 
 
 lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
@@ -117,21 +117,20 @@
   
   have [simp]: "1 \<le> star a"
     unfolding star_cont[of 1 a 1, simplified] 
-    by (rule le_SUPI) (rule power_0[symmetric])
+    by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
   
   show "1 + a * star a \<le> star a" 
     apply (rule plus_leI, simp)
     apply (simp add:star_cont[of a a 1, simplified])
     apply (simp add:star_cont[of 1 a 1, simplified])
-    apply (intro SUP_leI le_SUPI)
-    by (rule power_Suc[symmetric])
+    apply (subst power_Suc[symmetric])
+    by (intro SUP_leI le_SUPI UNIV_I)
 
   show "1 + star a * a \<le> star a" 
     apply (rule plus_leI, simp)
     apply (simp add:star_cont[of 1 a a, simplified])
     apply (simp add:star_cont[of 1 a 1, simplified])
-    apply (intro SUP_leI le_SUPI)
-    by (simp add:power_Suc[symmetric] power_commutes)
+    by (auto intro: SUP_leI le_SUPI UNIV_I simp add: power_Suc[symmetric] power_commutes)
 
   show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
   proof -