91 class complete_linorder. |
91 class complete_linorder. |
92 |
92 |
93 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
93 Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, |
94 Sup_fun_def, Inf_apply, Sup_apply. |
94 Sup_fun_def, Inf_apply, Sup_apply. |
95 |
95 |
96 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary, |
96 Removed redundant lemmas (the right hand side gives hints how to replace them |
97 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter, |
97 for (metis ...), or (simp only: ...) proofs): |
98 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset, |
98 |
99 UNION_eq_Union_image, Union_def, UN_eq have been discarded. |
99 Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right] |
|
100 Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right] |
|
101 Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right |
|
102 Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right |
|
103 Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right |
|
104 Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right |
|
105 Inter_def ~> INF_def, image_def |
|
106 Union_def ~> SUP_def, image_def |
|
107 INT_eq ~> INF_def, and image_def |
|
108 UN_eq ~> SUP_def, and image_def |
|
109 INF_subset ~> INF_superset_mono [OF _ order_refl] |
100 |
110 |
101 More consistent and comprehensive names: |
111 More consistent and comprehensive names: |
102 |
112 |
|
113 INTER_eq_Inter_image ~> INF_def |
|
114 UNION_eq_Union_image ~> SUP_def |
103 INFI_def ~> INF_def |
115 INFI_def ~> INF_def |
104 SUPR_def ~> SUP_def |
116 SUPR_def ~> SUP_def |
105 INF_leI ~> INF_lower |
117 INF_leI ~> INF_lower |
106 INF_leI2 ~> INF_lower2 |
118 INF_leI2 ~> INF_lower2 |
107 le_INFI ~> INF_greatest |
119 le_INFI ~> INF_greatest |