src/HOL/Library/Continuity.thy
changeset 19736 d8d0f8f51d69
parent 15140 322485b816ac
child 21312 1d39091a3208
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -11,9 +11,9 @@
     1.4  
     1.5  subsection "Chains"
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    up_chain :: "(nat => 'a set) => bool"
    1.10 -  "up_chain F == \<forall>i. F i \<subseteq> F (Suc i)"
    1.11 +  "up_chain F = (\<forall>i. F i \<subseteq> F (Suc i))"
    1.12  
    1.13  lemma up_chainI: "(!!i. F i \<subseteq> F (Suc i)) ==> up_chain F"
    1.14    by (simp add: up_chain_def)
    1.15 @@ -21,10 +21,10 @@
    1.16  lemma up_chainD: "up_chain F ==> F i \<subseteq> F (Suc i)"
    1.17    by (simp add: up_chain_def)
    1.18  
    1.19 -lemma up_chain_less_mono [rule_format]:
    1.20 -    "up_chain F ==> x < y --> F x \<subseteq> F y"
    1.21 -  apply (induct_tac y)
    1.22 -  apply (blast dest: up_chainD elim: less_SucE)+
    1.23 +lemma up_chain_less_mono:
    1.24 +    "up_chain F ==> x < y ==> F x \<subseteq> F y"
    1.25 +  apply (induct y)
    1.26 +   apply (blast dest: up_chainD elim: less_SucE)+
    1.27    done
    1.28  
    1.29  lemma up_chain_mono: "up_chain F ==> x \<le> y ==> F x \<subseteq> F y"
    1.30 @@ -33,9 +33,9 @@
    1.31    done
    1.32  
    1.33  
    1.34 -constdefs
    1.35 +definition
    1.36    down_chain :: "(nat => 'a set) => bool"
    1.37 -  "down_chain F == \<forall>i. F (Suc i) \<subseteq> F i"
    1.38 +  "down_chain F = (\<forall>i. F (Suc i) \<subseteq> F i)"
    1.39  
    1.40  lemma down_chainI: "(!!i. F (Suc i) \<subseteq> F i) ==> down_chain F"
    1.41    by (simp add: down_chain_def)
    1.42 @@ -43,10 +43,10 @@
    1.43  lemma down_chainD: "down_chain F ==> F (Suc i) \<subseteq> F i"
    1.44    by (simp add: down_chain_def)
    1.45  
    1.46 -lemma down_chain_less_mono [rule_format]:
    1.47 -    "down_chain F ==> x < y --> F y \<subseteq> F x"
    1.48 -  apply (induct_tac y)
    1.49 -  apply (blast dest: down_chainD elim: less_SucE)+
    1.50 +lemma down_chain_less_mono:
    1.51 +    "down_chain F ==> x < y ==> F y \<subseteq> F x"
    1.52 +  apply (induct y)
    1.53 +   apply (blast dest: down_chainD elim: less_SucE)+
    1.54    done
    1.55  
    1.56  lemma down_chain_mono: "down_chain F ==> x \<le> y ==> F y \<subseteq> F x"
    1.57 @@ -57,9 +57,9 @@
    1.58  
    1.59  subsection "Continuity"
    1.60  
    1.61 -constdefs
    1.62 +definition
    1.63    up_cont :: "('a set => 'a set) => bool"
    1.64 -  "up_cont f == \<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F)"
    1.65 +  "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
    1.66  
    1.67  lemma up_contI:
    1.68      "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
    1.69 @@ -84,10 +84,10 @@
    1.70    done
    1.71  
    1.72  
    1.73 -constdefs
    1.74 +definition
    1.75    down_cont :: "('a set => 'a set) => bool"
    1.76 -  "down_cont f ==
    1.77 -    \<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F)"
    1.78 +  "down_cont f =
    1.79 +    (\<forall>F. down_chain F --> f (Inter (range F)) = Inter (f ` range F))"
    1.80  
    1.81  lemma down_contI:
    1.82    "(!!F. down_chain F ==> f (Inter (range F)) = Inter (f ` range F)) ==>
    1.83 @@ -114,9 +114,9 @@
    1.84  
    1.85  subsection "Iteration"
    1.86  
    1.87 -constdefs
    1.88 +definition
    1.89    up_iterate :: "('a set => 'a set) => nat => 'a set"
    1.90 -  "up_iterate f n == (f^n) {}"
    1.91 +  "up_iterate f n = (f^n) {}"
    1.92  
    1.93  lemma up_iterate_0 [simp]: "up_iterate f 0 = {}"
    1.94    by (simp add: up_iterate_def)
    1.95 @@ -166,9 +166,9 @@
    1.96    done
    1.97  
    1.98  
    1.99 -constdefs
   1.100 +definition
   1.101    down_iterate :: "('a set => 'a set) => nat => 'a set"
   1.102 -  "down_iterate f n == (f^n) UNIV"
   1.103 +  "down_iterate f n = (f^n) UNIV"
   1.104  
   1.105  lemma down_iterate_0 [simp]: "down_iterate f 0 = UNIV"
   1.106    by (simp add: down_iterate_def)