src/HOL/Library/Continuity.thy
changeset 24331 76f7a8c6e842
parent 23752 15839159f8b6
child 25076 a50b36401c61
     1.1 --- a/src/HOL/Library/Continuity.thy	Sun Aug 19 12:43:05 2007 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sun Aug 19 21:21:37 2007 +0200
     1.3 @@ -139,26 +139,26 @@
     1.4    "up_cont f = (\<forall>F. up_chain F --> f (\<Union>(range F)) = \<Union>(f ` range F))"
     1.5  
     1.6  lemma up_contI:
     1.7 -    "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
     1.8 -  apply (unfold up_cont_def)
     1.9 -  apply blast
    1.10 -  done
    1.11 +  "(!!F. up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)) ==> up_cont f"
    1.12 +apply (unfold up_cont_def)
    1.13 +apply blast
    1.14 +done
    1.15  
    1.16  lemma up_contD:
    1.17 -    "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
    1.18 -  apply (unfold up_cont_def)
    1.19 -  apply auto
    1.20 -  done
    1.21 +  "up_cont f ==> up_chain F ==> f (\<Union>(range F)) = \<Union>(f ` range F)"
    1.22 +apply (unfold up_cont_def)
    1.23 +apply auto
    1.24 +done
    1.25  
    1.26  
    1.27  lemma up_cont_mono: "up_cont f ==> mono f"
    1.28 -  apply (rule monoI)
    1.29 -  apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
    1.30 -   apply (rule up_chainI)
    1.31 -   apply  simp+
    1.32 -  apply (drule Un_absorb1)
    1.33 -  apply (auto simp add: nat_not_singleton)
    1.34 -  done
    1.35 +apply (rule monoI)
    1.36 +apply (drule_tac F = "\<lambda>i. if i = 0 then A else B" in up_contD)
    1.37 + apply (rule up_chainI)
    1.38 + apply simp
    1.39 +apply (drule Un_absorb1)
    1.40 +apply (auto simp add: nat_not_singleton)
    1.41 +done
    1.42  
    1.43  
    1.44  definition
    1.45 @@ -180,13 +180,13 @@
    1.46    done
    1.47  
    1.48  lemma down_cont_mono: "down_cont f ==> mono f"
    1.49 -  apply (rule monoI)
    1.50 -  apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
    1.51 -   apply (rule down_chainI)
    1.52 -   apply simp+
    1.53 -  apply (drule Int_absorb1)
    1.54 -  apply (auto simp add: nat_not_singleton)
    1.55 -  done
    1.56 +apply (rule monoI)
    1.57 +apply (drule_tac F = "\<lambda>i. if i = 0 then B else A" in down_contD)
    1.58 + apply (rule down_chainI)
    1.59 + apply simp
    1.60 +apply (drule Int_absorb1)
    1.61 +apply (auto simp add: nat_not_singleton)
    1.62 +done
    1.63  
    1.64  
    1.65  subsection "Iteration"