src/HOL/Lattices.thy
changeset 61629 90f54d9e63f2
parent 61605 1bf7b186542e
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Lattices.thy	Wed Nov 11 09:06:30 2015 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Nov 11 09:21:56 2015 +0100
     1.3 @@ -707,8 +707,44 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
     1.8 +by(simp add: inf_sup_aci sup_compl_top)
     1.9 +
    1.10 +lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
    1.11 +by(simp add: inf_sup_aci sup_compl_top)
    1.12 +
    1.13 +lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
    1.14 +by(simp add: inf_sup_aci inf_compl_bot)
    1.15 +
    1.16 +lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
    1.17 +by(simp add: inf_sup_aci inf_compl_bot)
    1.18 +
    1.19 +declare inf_compl_bot [simp] sup_compl_top [simp]
    1.20 +
    1.21 +lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
    1.22 +by(simp add: sup_assoc[symmetric])
    1.23 +
    1.24 +lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
    1.25 +using sup_compl_top_left1[of "- x" y] by simp
    1.26 +
    1.27 +lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
    1.28 +by(simp add: inf_assoc[symmetric])
    1.29 +
    1.30 +lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
    1.31 +using inf_compl_bot_left1[of "- x" y] by simp
    1.32 +
    1.33 +lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
    1.34 +by(subst inf_left_commute) simp
    1.35 +
    1.36  end
    1.37  
    1.38 +ML_file "Tools/boolean_algebra_cancel.ML"
    1.39 +
    1.40 +simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
    1.41 +  {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv *}
    1.42 +
    1.43 +simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
    1.44 +  {* fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv *}
    1.45  
    1.46  subsection \<open>@{text "min/max"} as special case of lattice\<close>
    1.47