src/HOL/Library/Continuity.thy

 "chain M == !i. M i \<le> M(Suc i)"
  continuous :: "('a::order \<Rightarrow> 'a::order) \<Rightarrow> bool"
 "continuous F == !M. chain M \<longrightarrow> F(SUP i. M i) = (SUP i. F(M i))"
 
 abbreviation
- bot :: "'a::order"
-"bot == Sup {}"
+  bot :: "'a::order" where
+  "bot == Sup {}"
 
 lemma SUP_nat_conv:
  "(SUP n::nat. M n::'a::comp_lat) = join (M 0) (SUP n. M(Suc n))"
 apply(rule order_antisym)
  apply(rule SUP_leI)

 
 
 subsection "Chains"
 
 definition
-  up_chain :: "(nat => 'a set) => bool"
+  up_chain :: "(nat => 'a set) => bool" where
   "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
 
 lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
   by (simp add: up_chain_def)
 

   apply (blast dest: up_chain_less_mono)
   done
 
 
 definition
-  down_chain :: "(nat => 'a set) => bool"
+  down_chain :: "(nat => 'a set) => bool" where
   "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
 
 lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
   by (simp add: down_chain_def)
 

 
 
 subsection "Continuity"
 
 definition
-  up_cont :: "('a set => 'a set) => bool"
+  up_cont :: "('a set => 'a set) => bool" where
   "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
 
 lemma up_contI:
     "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
   apply (unfold up_cont_def)

   apply (auto simp add: nat_not_singleton)
   done
 
 
 definition
-  down_cont :: "('a set => 'a set) => bool"
+  down_cont :: "('a set => 'a set) => bool" where
   "down_cont f =
     (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
 
 lemma down_contI:
   "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>

 
 
 subsection "Iteration"
 
 definition
-  up_iterate :: "('a set => 'a set) => nat => 'a set"
+  up_iterate :: "('a set => 'a set) => nat => 'a set" where
   "up_iterate f n = (f^n) {}"
 
 lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
   by (simp add: up_iterate_def)
 

   apply (erule UNION_up_iterate_is_fp [symmetric])
   done
 
 
 definition
-  down_iterate :: "('a set => 'a set) => nat => 'a set"
+  down_iterate :: "('a set => 'a set) => nat => 'a set" where
   "down_iterate f n = (f^n) UNIV"
 
 lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   by (simp add: down_iterate_def)