equal
deleted
inserted
replaced
154 |
154 |
155 syntax UU :: logic |
155 syntax UU :: logic |
156 translations "UU" \<rightharpoonup> "CONST bottom" |
156 translations "UU" \<rightharpoonup> "CONST bottom" |
157 |
157 |
158 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close> |
158 text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close> |
159 setup \<open>Reorient_Proc.add (fn Const(\<^const_name>\<open>bottom\<close>, _) => true | _ => false)\<close> |
159 setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close> |
160 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
160 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc |
161 |
161 |
162 text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close> |
162 text \<open>useful lemmas about \<^term>\<open>\<bottom>\<close>\<close> |
163 |
163 |
164 lemma below_bottom_iff [simp]: "x \<sqsubseteq> \<bottom> \<longleftrightarrow> x = \<bottom>" |
164 lemma below_bottom_iff [simp]: "x \<sqsubseteq> \<bottom> \<longleftrightarrow> x = \<bottom>" |