equal
deleted
inserted
replaced
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 |