src/HOL/Library/Lattice_Constructions.thy
changeset 60509 0928cf63920f
parent 60508 2127bee2069a
child 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 20:05:21 2015 +0200
     1.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Wed Jun 17 22:12:08 2015 +0200
     1.3 @@ -255,13 +255,13 @@
     1.4    unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
     1.5  
     1.6  lemma greater_than_two_values:
     1.7 -  assumes "a \<noteq> aa" "Value a \<le> z" "Value aa \<le> z"
     1.8 +  assumes "a \<noteq> b" "Value a \<le> z" "Value b \<le> z"
     1.9    shows "z = Top"
    1.10    using assms
    1.11    by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
    1.12  
    1.13  lemma lesser_than_two_values:
    1.14 -  assumes "a \<noteq> aa" "z \<le> Value a" "z \<le> Value aa"
    1.15 +  assumes "a \<noteq> b" "z \<le> Value a" "z \<le> Value b"
    1.16    shows "z = Bot"
    1.17    using assms
    1.18    by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
    1.19 @@ -358,41 +358,55 @@
    1.20  next
    1.21    fix z :: "'a flat_complete_lattice"
    1.22    fix A
    1.23 -  assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
    1.24 -  {
    1.25 -    fix v
    1.26 -    assume *: "A - {Top} = {Value v}"
    1.27 -    then have "(THE v. A - {Top} = {Value v}) = v"
    1.28 -      by (auto intro!: the1_equality)
    1.29 -    with * have "z \<le> Value (THE v::'a. A - {Top} = {Value v})"
    1.30 -      using z by auto
    1.31 -  }
    1.32 -  moreover
    1.33 -  {
    1.34 -    assume not_one_value: "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v::'a. A - {Top} = {Value v})"
    1.35 -    have "z \<le> Bot"
    1.36 -    proof (cases "A - {Top} = {Bot}")
    1.37 -      case True
    1.38 -      with z show ?thesis
    1.39 +  show "z \<le> Inf A" if z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
    1.40 +  proof -
    1.41 +    consider "A = {} \<or> A = {Top}"
    1.42 +      | "A \<noteq> {}" "A \<noteq> {Top}" "\<exists>v. A - {Top} = {Value v}"
    1.43 +      | "A \<noteq> {}" "A \<noteq> {Top}" "\<not> (\<exists>v. A - {Top} = {Value v})"
    1.44 +      by blast
    1.45 +    then show ?thesis
    1.46 +    proof cases
    1.47 +      case 1
    1.48 +      then have "Inf A = Top"
    1.49 +        unfolding Inf_flat_complete_lattice_def by auto
    1.50 +      then show ?thesis by simp
    1.51 +    next
    1.52 +      case 2
    1.53 +      then obtain v where v1: "A - {Top} = {Value v}"
    1.54          by auto
    1.55 +      then have v2: "(THE v. A - {Top} = {Value v}) = v"
    1.56 +        by (auto intro!: the1_equality)
    1.57 +      from 2 v2 have Inf: "Inf A = Value v"
    1.58 +        unfolding Inf_flat_complete_lattice_def by simp
    1.59 +      from v1 have "Value v \<in> A" by blast
    1.60 +      then have "z \<le> Value v" by (rule z)
    1.61 +      with Inf show ?thesis by simp
    1.62      next
    1.63 -      case False
    1.64 -      from not_one_value
    1.65 -      obtain a1 where a1: "a1 \<in> A - {Top}" by auto
    1.66 -      from not_one_value False a1
    1.67 -      obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
    1.68 -        by (cases a1) auto
    1.69 -      with a1 z[of "a1"] z[of "a2"] show ?thesis
    1.70 -        apply (cases a1)
    1.71 -        apply auto
    1.72 -        apply (cases a2)
    1.73 -        apply auto
    1.74 -        apply (auto dest!: lesser_than_two_values)
    1.75 -        done
    1.76 +      case 3
    1.77 +      then have Inf: "Inf A = Bot"
    1.78 +        unfolding Inf_flat_complete_lattice_def by auto
    1.79 +      have "z \<le> Bot"
    1.80 +      proof (cases "A - {Top} = {Bot}")
    1.81 +        case True
    1.82 +        then have "Bot \<in> A" by blast
    1.83 +        then show ?thesis by (rule z)
    1.84 +      next
    1.85 +        case False
    1.86 +        from 3 obtain a1 where a1: "a1 \<in> A - {Top}"
    1.87 +          by auto
    1.88 +        from 3 False a1 obtain a2 where "a2 \<in> A - {Top} \<and> a1 \<noteq> a2"
    1.89 +          by (cases a1) auto
    1.90 +        with a1 z[of "a1"] z[of "a2"] show ?thesis
    1.91 +          apply (cases a1)
    1.92 +          apply auto
    1.93 +          apply (cases a2)
    1.94 +          apply auto
    1.95 +          apply (auto dest!: lesser_than_two_values)
    1.96 +          done
    1.97 +      qed
    1.98 +      with Inf show ?thesis by simp
    1.99      qed
   1.100 -  }
   1.101 -  ultimately show "z \<le> Inf A"
   1.102 -    using z unfolding Inf_flat_complete_lattice_def by auto  -- slow
   1.103 +  qed
   1.104  next
   1.105    fix x :: "'a flat_complete_lattice"
   1.106    fix A
   1.107 @@ -414,40 +428,54 @@
   1.108  next
   1.109    fix z :: "'a flat_complete_lattice"
   1.110    fix A
   1.111 -  assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.112 -  {
   1.113 -    fix v
   1.114 -    assume "A - {Bot} = {Value v}"
   1.115 -    moreover
   1.116 -    then have "(THE v. A - {Bot} = {Value v}) = v"
   1.117 -      by (auto intro!: the1_equality)
   1.118 -    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) \<le> z"
   1.119 -      using z by auto
   1.120 -  }
   1.121 -  moreover
   1.122 -  {
   1.123 -    assume not_one_value: "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v::'a. A - {Bot} = {Value v})"
   1.124 -    have "Top \<le> z"
   1.125 -    proof (cases "A - {Bot} = {Top}")
   1.126 -      case True
   1.127 -      with z show ?thesis
   1.128 +  show "Sup A \<le> z" if z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
   1.129 +  proof -
   1.130 +    consider "A = {} \<or> A = {Bot}"
   1.131 +      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<exists>v. A - {Bot} = {Value v}"
   1.132 +      | "A \<noteq> {}" "A \<noteq> {Bot}" "\<not> (\<exists>v. A - {Bot} = {Value v})"
   1.133 +      by blast
   1.134 +    then show ?thesis
   1.135 +    proof cases
   1.136 +      case 1
   1.137 +      then have "Sup A = Bot"
   1.138 +        unfolding Sup_flat_complete_lattice_def by auto
   1.139 +      then show ?thesis by simp
   1.140 +    next
   1.141 +      case 2
   1.142 +      then obtain v where v1: "A - {Bot} = {Value v}"
   1.143          by auto
   1.144 +      then have v2: "(THE v. A - {Bot} = {Value v}) = v"
   1.145 +        by (auto intro!: the1_equality)
   1.146 +      from 2 v2 have Sup: "Sup A = Value v"
   1.147 +        unfolding Sup_flat_complete_lattice_def by simp
   1.148 +      from v1 have "Value v \<in> A" by blast
   1.149 +      then have "Value v \<le> z" by (rule z)
   1.150 +      with Sup show ?thesis by simp
   1.151      next
   1.152 -      case False
   1.153 -      from not_one_value obtain a1 where a1: "a1 \<in> A - {Bot}"
   1.154 -        by auto
   1.155 -      from not_one_value False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
   1.156 -        by (cases a1) auto
   1.157 -      with a1 z[of "a1"] z[of "a2"] show ?thesis
   1.158 -        apply (cases a1)
   1.159 -        apply auto
   1.160 -        apply (cases a2)
   1.161 -        apply (auto dest!: greater_than_two_values)
   1.162 -        done
   1.163 +      case 3
   1.164 +      then have Sup: "Sup A = Top"
   1.165 +        unfolding Sup_flat_complete_lattice_def by auto
   1.166 +      have "Top \<le> z"
   1.167 +      proof (cases "A - {Bot} = {Top}")
   1.168 +        case True
   1.169 +        then have "Top \<in> A" by blast
   1.170 +        then show ?thesis by (rule z)
   1.171 +      next
   1.172 +        case False
   1.173 +        from 3 obtain a1 where a1: "a1 \<in> A - {Bot}"
   1.174 +          by auto
   1.175 +        from 3 False a1 obtain a2 where "a2 \<in> A - {Bot} \<and> a1 \<noteq> a2"
   1.176 +          by (cases a1) auto
   1.177 +        with a1 z[of "a1"] z[of "a2"] show ?thesis
   1.178 +          apply (cases a1)
   1.179 +          apply auto
   1.180 +          apply (cases a2)
   1.181 +          apply (auto dest!: greater_than_two_values)
   1.182 +          done
   1.183 +      qed
   1.184 +      with Sup show ?thesis by simp
   1.185      qed
   1.186 -  }
   1.187 -  ultimately show "Sup A \<le> z"
   1.188 -    using z unfolding Sup_flat_complete_lattice_def by auto  -- slow
   1.189 +  qed
   1.190  next
   1.191    show "Inf {} = (top :: 'a flat_complete_lattice)"
   1.192      by (simp add: Inf_flat_complete_lattice_def top_flat_complete_lattice_def)