src/HOL/Conditionally_Complete_Lattices.thy
changeset 57275 0ddb5b755cdc
parent 56218 1c3f1f2431f9
child 57447 87429bdecad5
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 15:23:40 2014 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Wed Jun 18 07:31:12 2014 +0200
     1.3 @@ -559,4 +559,62 @@
     1.4  qed
     1.5  end
     1.6  
     1.7 +lemma interval_cases:
     1.8 +  fixes S :: "'a :: conditionally_complete_linorder set"
     1.9 +  assumes ivl: "\<And>a b x. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> x \<in> S"
    1.10 +  shows "\<exists>a b. S = {} \<or>
    1.11 +    S = UNIV \<or>
    1.12 +    S = {..<b} \<or>
    1.13 +    S = {..b} \<or>
    1.14 +    S = {a<..} \<or>
    1.15 +    S = {a..} \<or>
    1.16 +    S = {a<..<b} \<or>
    1.17 +    S = {a<..b} \<or>
    1.18 +    S = {a..<b} \<or>
    1.19 +    S = {a..b}"
    1.20 +proof -
    1.21 +  def lower \<equiv> "{x. \<exists>s\<in>S. s \<le> x}" and upper \<equiv> "{x. \<exists>s\<in>S. x \<le> s}"
    1.22 +  with ivl have "S = lower \<inter> upper"
    1.23 +    by auto
    1.24 +  moreover 
    1.25 +  have "\<exists>a. upper = UNIV \<or> upper = {} \<or> upper = {.. a} \<or> upper = {..< a}"
    1.26 +  proof cases
    1.27 +    assume *: "bdd_above S \<and> S \<noteq> {}"
    1.28 +    from * have "upper \<subseteq> {.. Sup S}"
    1.29 +      by (auto simp: upper_def intro: cSup_upper2)
    1.30 +    moreover from * have "{..< Sup S} \<subseteq> upper"
    1.31 +      by (force simp add: less_cSup_iff upper_def subset_eq Ball_def)
    1.32 +    ultimately have "upper = {.. Sup S} \<or> upper = {..< Sup S}"
    1.33 +      unfolding ivl_disj_un(2)[symmetric] by auto
    1.34 +    then show ?thesis by auto
    1.35 +  next
    1.36 +    assume "\<not> (bdd_above S \<and> S \<noteq> {})"
    1.37 +    then have "upper = UNIV \<or> upper = {}"
    1.38 +      by (auto simp: upper_def bdd_above_def not_le dest: less_imp_le)
    1.39 +    then show ?thesis
    1.40 +      by auto
    1.41 +  qed
    1.42 +  moreover
    1.43 +  have "\<exists>b. lower = UNIV \<or> lower = {} \<or> lower = {b ..} \<or> lower = {b <..}"
    1.44 +  proof cases
    1.45 +    assume *: "bdd_below S \<and> S \<noteq> {}"
    1.46 +    from * have "lower \<subseteq> {Inf S ..}"
    1.47 +      by (auto simp: lower_def intro: cInf_lower2)
    1.48 +    moreover from * have "{Inf S <..} \<subseteq> lower"
    1.49 +      by (force simp add: cInf_less_iff lower_def subset_eq Ball_def)
    1.50 +    ultimately have "lower = {Inf S ..} \<or> lower = {Inf S <..}"
    1.51 +      unfolding ivl_disj_un(1)[symmetric] by auto
    1.52 +    then show ?thesis by auto
    1.53 +  next
    1.54 +    assume "\<not> (bdd_below S \<and> S \<noteq> {})"
    1.55 +    then have "lower = UNIV \<or> lower = {}"
    1.56 +      by (auto simp: lower_def bdd_below_def not_le dest: less_imp_le)
    1.57 +    then show ?thesis
    1.58 +      by auto
    1.59 +  qed
    1.60 +  ultimately show ?thesis
    1.61 +    unfolding greaterThanAtMost_def greaterThanLessThan_def atLeastAtMost_def atLeastLessThan_def
    1.62 +    by (elim exE disjE) auto
    1.63 +qed
    1.64 +
    1.65  end