src/HOL/Lattices.thy
 changeset 25482 4ed49eccb1eb parent 25382 72cfe89f7b21 child 25510 38c15efe603b
equal 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)`