equal
deleted
inserted
replaced
35 by (induct x rule: one_induct) simp_all |
35 by (induct x rule: one_induct) simp_all |
36 |
36 |
37 lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE" |
37 lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE" |
38 by (induct x rule: one_induct) simp_all |
38 by (induct x rule: one_induct) simp_all |
39 |
39 |
40 lemma dist_eq_one [simp]: "ONE \<noteq> \<bottom>" "\<bottom> \<noteq> ONE" |
40 lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>" |
41 unfolding ONE_def by simp_all |
41 unfolding ONE_def by simp |
42 |
42 |
43 lemma one_neq_iffs [simp]: |
43 lemma one_neq_iffs [simp]: |
44 "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>" |
44 "x \<noteq> ONE \<longleftrightarrow> x = \<bottom>" |
45 "ONE \<noteq> x \<longleftrightarrow> x = \<bottom>" |
45 "ONE \<noteq> x \<longleftrightarrow> x = \<bottom>" |
46 "x \<noteq> \<bottom> \<longleftrightarrow> x = ONE" |
46 "x \<noteq> \<bottom> \<longleftrightarrow> x = ONE" |