Adapted to changes in definition of SUP.
authorberghofe
Sat Mar 10 16:24:52 2007 +0100 (2007-03-10)
changeset 2243128344ccffc35
parent 22430 6a56bf1b3a64
child 22432 1d00d26fee0d
Adapted to changes in definition of SUP.
src/HOL/Library/Continuity.thy
src/HOL/Library/Graphs.thy
src/HOL/Library/Kleene_Algebras.thy
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat Mar 10 16:23:28 2007 +0100
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sat Mar 10 16:24:52 2007 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    "chain M \<longleftrightarrow> (\<forall>i. M i \<le> M (Suc i))"
     1.5  
     1.6  definition
     1.7 -  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool" where
     1.8 +  continuous :: "('a::comp_lat \<Rightarrow> 'a::comp_lat) \<Rightarrow> bool" where
     1.9    "continuous F \<longleftrightarrow> (\<forall>M. chain M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.10  
    1.11  abbreviation
    1.12 @@ -24,12 +24,12 @@
    1.13    "bot \<equiv> Sup {}"
    1.14  
    1.15  lemma SUP_nat_conv:
    1.16 -  "(SUP n::nat. M n::'a::comp_lat) = sup (M 0) (SUP n. M(Suc n))"
    1.17 +  "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
    1.18  apply(rule order_antisym)
    1.19   apply(rule SUP_leI)
    1.20   apply(case_tac n)
    1.21    apply simp
    1.22 - apply (blast intro:le_SUPI le_supI2)
    1.23 + apply (fast intro:le_SUPI le_supI2)
    1.24  apply(simp)
    1.25  apply (blast intro:SUP_leI le_SUPI)
    1.26  done
    1.27 @@ -43,10 +43,10 @@
    1.28    have "F B = sup (F A) (F B)"
    1.29    proof -
    1.30      have "sup A B = B" using `A <= B` by (simp add:sup_absorb2)
    1.31 -    hence "F B = F(SUP i. ?C i)" by(simp add: SUP_nat_conv)
    1.32 +    hence "F B = F(SUP i. ?C i)" by (subst SUP_nat_conv) simp
    1.33      also have "\<dots> = (SUP i. F(?C i))"
    1.34        using `chain ?C` `continuous F` by(simp add:continuous_def)
    1.35 -    also have "\<dots> = sup (F A) (F B)" by(simp add: SUP_nat_conv)
    1.36 +    also have "\<dots> = sup (F A) (F B)" by (subst SUP_nat_conv) simp
    1.37      finally show ?thesis .
    1.38    qed
    1.39    thus "F A \<le> F B" by(subst le_iff_sup, simp)
    1.40 @@ -80,7 +80,7 @@
    1.41        thus ?thesis by(auto simp add:chain_def)
    1.42      qed
    1.43      hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.44 -    also have "\<dots> \<le> ?U" by(blast intro:SUP_leI le_SUPI)
    1.45 +    also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    1.46      finally show "F ?U \<le> ?U" .
    1.47    qed
    1.48    ultimately show ?thesis by (blast intro:order_antisym)
     2.1 --- a/src/HOL/Library/Graphs.thy	Sat Mar 10 16:23:28 2007 +0100
     2.2 +++ b/src/HOL/Library/Graphs.thy	Sat Mar 10 16:24:52 2007 +0100
     2.3 @@ -245,7 +245,7 @@
     2.4  
     2.5  lemma Sup_graph_eq:
     2.6    "(SUP n. Graph (G n)) = Graph (\<Union>n. G n)"
     2.7 -  unfolding SUP_def 
     2.8 +  unfolding SUPR_def
     2.9    apply (rule order_antisym)
    2.10    apply (rule Sup_least)
    2.11    apply auto
     3.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Sat Mar 10 16:23:28 2007 +0100
     3.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Sat Mar 10 16:24:52 2007 +0100
     3.3 @@ -104,7 +104,7 @@
     3.4    assumes "l \<le> M i"
     3.5    shows "l \<le> (SUP i. M i)"
     3.6    using prems
     3.7 -  by (rule order_trans) (rule le_SUPI, rule refl)
     3.8 +  by (rule order_trans) (rule le_SUPI [OF UNIV_I])
     3.9  
    3.10  
    3.11  lemma zero_minimum[simp]: "(0::'a::pre_kleene) \<le> x"
    3.12 @@ -117,21 +117,20 @@
    3.13    
    3.14    have [simp]: "1 \<le> star a"
    3.15      unfolding star_cont[of 1 a 1, simplified] 
    3.16 -    by (rule le_SUPI) (rule power_0[symmetric])
    3.17 +    by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
    3.18    
    3.19    show "1 + a * star a \<le> star a" 
    3.20      apply (rule plus_leI, simp)
    3.21      apply (simp add:star_cont[of a a 1, simplified])
    3.22      apply (simp add:star_cont[of 1 a 1, simplified])
    3.23 -    apply (intro SUP_leI le_SUPI)
    3.24 -    by (rule power_Suc[symmetric])
    3.25 +    apply (subst power_Suc[symmetric])
    3.26 +    by (intro SUP_leI le_SUPI UNIV_I)
    3.27  
    3.28    show "1 + star a * a \<le> star a" 
    3.29      apply (rule plus_leI, simp)
    3.30      apply (simp add:star_cont[of 1 a a, simplified])
    3.31      apply (simp add:star_cont[of 1 a 1, simplified])
    3.32 -    apply (intro SUP_leI le_SUPI)
    3.33 -    by (simp add:power_Suc[symmetric] power_commutes)
    3.34 +    by (auto intro: SUP_leI le_SUPI UNIV_I simp add: power_Suc[symmetric] power_commutes)
    3.35  
    3.36    show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
    3.37    proof -