src/HOL/Library/Continuity.thy
changeset 30952 7ab2716dd93b
parent 30950 1435a8f01a41
child 30971 7fbebf75b3ef
     1.1 --- a/src/HOL/Library/Continuity.thy	Fri Apr 17 16:41:31 2009 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Mon Apr 20 09:32:07 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Continuity and iterations (of set transformers) *}
     1.5  
     1.6  theory Continuity
     1.7 -imports Relation_Power Main
     1.8 +imports Transitive_Closure Main
     1.9  begin
    1.10  
    1.11  subsection {* Continuity for complete lattices *}
    1.12 @@ -48,25 +48,25 @@
    1.13  qed
    1.14  
    1.15  lemma continuous_lfp:
    1.16 - assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
    1.17 + assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
    1.18  proof -
    1.19    note mono = continuous_mono[OF `continuous F`]
    1.20 -  { fix i have "(F^^i) bot \<le> lfp F"
    1.21 +  { fix i have "(F o^ i) bot \<le> lfp F"
    1.22      proof (induct i)
    1.23 -      show "(F^^0) bot \<le> lfp F" by simp
    1.24 +      show "(F o^ 0) bot \<le> lfp F" by simp
    1.25      next
    1.26        case (Suc i)
    1.27 -      have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
    1.28 +      have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
    1.29        also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
    1.30        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    1.31        finally show ?case .
    1.32      qed }
    1.33 -  hence "(SUP i. (F^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    1.34 -  moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
    1.35 +  hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    1.36 +  moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
    1.37    proof (rule lfp_lowerbound)
    1.38 -    have "chain(%i. (F^^i) bot)"
    1.39 +    have "chain(%i. (F o^ i) bot)"
    1.40      proof -
    1.41 -      { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
    1.42 +      { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
    1.43  	proof (induct i)
    1.44  	  case 0 show ?case by simp
    1.45  	next
    1.46 @@ -74,7 +74,7 @@
    1.47  	qed }
    1.48        thus ?thesis by(auto simp add:chain_def)
    1.49      qed
    1.50 -    hence "F ?U = (SUP i. (F^^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.51 +    hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    1.52      also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    1.53      finally show "F ?U \<le> ?U" .
    1.54    qed
    1.55 @@ -193,7 +193,7 @@
    1.56  
    1.57  definition
    1.58    up_iterate :: "('a set => 'a set) => nat => 'a set" where
    1.59 -  "up_iterate f n = (f^^n) {}"
    1.60 +  "up_iterate f n = (f o^ n) {}"
    1.61  
    1.62  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
    1.63    by (simp add: up_iterate_def)
    1.64 @@ -245,7 +245,7 @@
    1.65  
    1.66  definition
    1.67    down_iterate :: "('a set => 'a set) => nat => 'a set" where
    1.68 -  "down_iterate f n = (f^^n) UNIV"
    1.69 +  "down_iterate f n = (f o^ n) UNIV"
    1.70  
    1.71  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
    1.72    by (simp add: down_iterate_def)