equal
deleted
inserted
replaced
488 |
488 |
489 lemma meet_defl_eq2: "b \<sqsubseteq> a \<Longrightarrow> meet_defl\<cdot>a\<cdot>b = b" |
489 lemma meet_defl_eq2: "b \<sqsubseteq> a \<Longrightarrow> meet_defl\<cdot>a\<cdot>b = b" |
490 by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest) |
490 by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest) |
491 |
491 |
492 interpretation meet_defl: semilattice "\<lambda>a b. meet_defl\<cdot>a\<cdot>b" |
492 interpretation meet_defl: semilattice "\<lambda>a b. meet_defl\<cdot>a\<cdot>b" |
493 by default |
493 by standard |
494 (fast intro: below_antisym meet_defl_greatest |
494 (fast intro: below_antisym meet_defl_greatest |
495 meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+ |
495 meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+ |
496 |
496 |
497 lemma deflation_meet_defl: "deflation (meet_defl\<cdot>a)" |
497 lemma deflation_meet_defl: "deflation (meet_defl\<cdot>a)" |
498 apply (rule deflation.intro) |
498 apply (rule deflation.intro) |