--- a/src/HOL/Library/Continuity.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Continuity.thy Mon Apr 20 09:32:07 2009 +0200
@@ -5,7 +5,7 @@
header {* Continuity and iterations (of set transformers) *}
theory Continuity
-imports Relation_Power Main
+imports Transitive_Closure Main
begin
subsection {* Continuity for complete lattices *}
@@ -48,25 +48,25 @@
qed
lemma continuous_lfp:
- assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
+ assumes "continuous F" shows "lfp F = (SUP i. (F o^ i) bot)"
proof -
note mono = continuous_mono[OF `continuous F`]
- { fix i have "(F^^i) bot \<le> lfp F"
+ { fix i have "(F o^ i) bot \<le> lfp F"
proof (induct i)
- show "(F^^0) bot \<le> lfp F" by simp
+ show "(F o^ 0) bot \<le> lfp F" by simp
next
case (Suc i)
- have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
+ have "(F o^ Suc i) bot = F((F o^ i) bot)" by simp
also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
finally show ?case .
qed }
- hence "(SUP i. (F^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
- moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
+ hence "(SUP i. (F o^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+ moreover have "lfp F \<le> (SUP i. (F o^ i) bot)" (is "_ \<le> ?U")
proof (rule lfp_lowerbound)
- have "chain(%i. (F^^i) bot)"
+ have "chain(%i. (F o^ i) bot)"
proof -
- { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
+ { fix i have "(F o^ i) bot \<le> (F o^ (Suc i)) bot"
proof (induct i)
case 0 show ?case by simp
next
@@ -74,7 +74,7 @@
qed }
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)
+ hence "F ?U = (SUP i. (F o^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
finally show "F ?U \<le> ?U" .
qed
@@ -193,7 +193,7 @@
definition
up_iterate :: "('a set => 'a set) => nat => 'a set" where
- "up_iterate f n = (f^^n) {}"
+ "up_iterate f n = (f o^ n) {}"
lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
by (simp add: up_iterate_def)
@@ -245,7 +245,7 @@
definition
down_iterate :: "('a set => 'a set) => nat => 'a set" where
- "down_iterate f n = (f^^n) UNIV"
+ "down_iterate f n = (f o^ n) UNIV"
lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
by (simp add: down_iterate_def)