src/HOL/IMP/Abs_Int2.thy
 changeset 51848 ed847ce0b70c parent 51834 8deb369ee70b child 51849 19ee0cebe76d
equal inserted replaced
51847:b7a0af870bfc 51848:ed847ce0b70c
`    36 begin`
`    36 begin`
`    37 `
`    37 `
`    38 lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"`
`    38 lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"`
`    39 by (metis IntI inter_gamma_subset_gamma_inf set_mp)`
`    39 by (metis IntI inter_gamma_subset_gamma_inf set_mp)`
`    40 `
`    40 `
`    41 lemma gamma_inf[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"`
`    41 lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"`
`    42 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])`
`    42 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])`
`    43   (metis inf_le1 inf_le2 le_inf_iff mono_gamma)`
`    43   (metis inf_le1 inf_le2 le_inf_iff mono_gamma)`
`    44 `
`    44 `
`    45 end`
`    45 end`
`    46 `
`    46 `