src/HOL/Library/Continuity.thy
 changeset 30950 1435a8f01a41 parent 30663 0b6aff7451b2 child 30952 7ab2716dd93b
```     1.1 --- a/src/HOL/Library/Continuity.thy	Fri Apr 17 15:57:26 2009 +0200
1.2 +++ b/src/HOL/Library/Continuity.thy	Fri Apr 17 16:41:30 2009 +0200
1.3 @@ -48,25 +48,25 @@
1.4  qed
1.5
1.6  lemma continuous_lfp:
1.7 - assumes "continuous F" shows "lfp F = (SUP i. (F^i) bot)"
1.8 + assumes "continuous F" shows "lfp F = (SUP i. (F^^i) bot)"
1.9  proof -
1.10    note mono = continuous_mono[OF `continuous F`]
1.11 -  { fix i have "(F^i) bot \<le> lfp F"
1.12 +  { fix i have "(F^^i) bot \<le> lfp F"
1.13      proof (induct i)
1.14 -      show "(F^0) bot \<le> lfp F" by simp
1.15 +      show "(F^^0) bot \<le> lfp F" by simp
1.16      next
1.17        case (Suc i)
1.18 -      have "(F^(Suc i)) bot = F((F^i) bot)" by simp
1.19 +      have "(F^^(Suc i)) bot = F((F^^i) bot)" by simp
1.20        also have "\<dots> \<le> F(lfp F)" by(rule monoD[OF mono Suc])
1.21        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
1.22        finally show ?case .
1.23      qed }
1.24 -  hence "(SUP i. (F^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
1.25 -  moreover have "lfp F \<le> (SUP i. (F^i) bot)" (is "_ \<le> ?U")
1.26 +  hence "(SUP i. (F^^i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
1.27 +  moreover have "lfp F \<le> (SUP i. (F^^i) bot)" (is "_ \<le> ?U")
1.28    proof (rule lfp_lowerbound)
1.29 -    have "chain(%i. (F^i) bot)"
1.30 +    have "chain(%i. (F^^i) bot)"
1.31      proof -
1.32 -      { fix i have "(F^i) bot \<le> (F^(Suc i)) bot"
1.33 +      { fix i have "(F^^i) bot \<le> (F^^(Suc i)) bot"
1.34  	proof (induct i)
1.35  	  case 0 show ?case by simp
1.36  	next
1.37 @@ -74,7 +74,7 @@
1.38  	qed }
1.39        thus ?thesis by(auto simp add:chain_def)
1.40      qed
1.41 -    hence "F ?U = (SUP i. (F^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
1.42 +    hence "F ?U = (SUP i. (F^^(i+1)) bot)" using `continuous F` by (simp add:continuous_def)
1.43      also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
1.44      finally show "F ?U \<le> ?U" .
1.45    qed
1.46 @@ -193,7 +193,7 @@
1.47
1.48  definition
1.49    up_iterate :: "('a set => 'a set) => nat => 'a set" where
1.50 -  "up_iterate f n = (f^n) {}"
1.51 +  "up_iterate f n = (f^^n) {}"
1.52
1.53  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"