src/HOL/Lattices.thy
changeset 25482 4ed49eccb1eb
parent 25382 72cfe89f7b21
child 25510 38c15efe603b
equal deleted inserted replaced
25481:aa16cd919dcc 25482:4ed49eccb1eb
    37 
    37 
    38 lemma le_infI1[intro]:
    38 lemma le_infI1[intro]:
    39   assumes "a \<sqsubseteq> x"
    39   assumes "a \<sqsubseteq> x"
    40   shows "a \<sqinter> b \<sqsubseteq> x"
    40   shows "a \<sqinter> b \<sqsubseteq> x"
    41 proof (rule order_trans)
    41 proof (rule order_trans)
    42   show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
    42   from assms show "a \<sqsubseteq> x" .
       
    43   show "a \<sqinter> b \<sqsubseteq> a" by simp 
    43 qed
    44 qed
    44 lemmas (in -) [rule del] = le_infI1
    45 lemmas (in -) [rule del] = le_infI1
    45 
    46 
    46 lemma le_infI2[intro]:
    47 lemma le_infI2[intro]:
    47   assumes "b \<sqsubseteq> x"
    48   assumes "b \<sqsubseteq> x"
    48   shows "a \<sqinter> b \<sqsubseteq> x"
    49   shows "a \<sqinter> b \<sqsubseteq> x"
    49 proof (rule order_trans)
    50 proof (rule order_trans)
    50   show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
    51   from assms show "b \<sqsubseteq> x" .
       
    52   show "a \<sqinter> b \<sqsubseteq> b" by simp
    51 qed
    53 qed
    52 lemmas (in -) [rule del] = le_infI2
    54 lemmas (in -) [rule del] = le_infI2
    53 
    55 
    54 lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    56 lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    55 by(blast intro: inf_greatest)
    57 by(blast intro: inf_greatest)