equal
deleted
inserted
replaced
24 apply (drule (1) bspec, erule bexE) |
24 apply (drule (1) bspec, erule bexE) |
25 apply (erule rev_bexI) |
25 apply (erule rev_bexI) |
26 apply (erule (1) trans_less) |
26 apply (erule (1) trans_less) |
27 done |
27 done |
28 |
28 |
29 interpretation lower_le!: preorder lower_le |
29 interpretation lower_le: preorder lower_le |
30 by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans) |
30 by (rule preorder.intro, rule lower_le_refl, rule lower_le_trans) |
31 |
31 |
32 lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t" |
32 lemma lower_le_minimal [simp]: "PDUnit compact_bot \<le>\<flat> t" |
33 unfolding lower_le_def Rep_PDUnit |
33 unfolding lower_le_def Rep_PDUnit |
34 by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv]) |
34 by (simp, rule Rep_pd_basis_nonempty [folded ex_in_conv]) |
131 lemma Rep_lower_principal: |
131 lemma Rep_lower_principal: |
132 "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}" |
132 "Rep_lower_pd (lower_principal t) = {u. u \<le>\<flat> t}" |
133 unfolding lower_principal_def |
133 unfolding lower_principal_def |
134 by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) |
134 by (simp add: Abs_lower_pd_inverse lower_le.ideal_principal) |
135 |
135 |
136 interpretation lower_pd!: |
136 interpretation lower_pd: |
137 ideal_completion lower_le pd_take lower_principal Rep_lower_pd |
137 ideal_completion lower_le pd_take lower_principal Rep_lower_pd |
138 apply unfold_locales |
138 apply unfold_locales |
139 apply (rule pd_take_lower_le) |
139 apply (rule pd_take_lower_le) |
140 apply (rule pd_take_idem) |
140 apply (rule pd_take_idem) |
141 apply (erule pd_take_lower_mono) |
141 apply (erule pd_take_lower_mono) |