equal
deleted
inserted
replaced
38 by (cases x rule: trE) simp_all |
38 by (cases x rule: trE) simp_all |
39 |
39 |
40 text {* distinctness for type @{typ tr} *} |
40 text {* distinctness for type @{typ tr} *} |
41 |
41 |
42 lemma dist_below_tr [simp]: |
42 lemma dist_below_tr [simp]: |
43 "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" |
43 "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT" |
44 unfolding TT_def FF_def by simp_all |
44 unfolding TT_def FF_def by simp_all |
45 |
45 |
46 lemma dist_eq_tr [simp]: |
46 lemma dist_eq_tr [simp]: |
47 "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" |
47 "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" |
48 unfolding TT_def FF_def by simp_all |
48 unfolding TT_def FF_def by simp_all |
51 by (induct x rule: tr_induct) simp_all |
51 by (induct x rule: tr_induct) simp_all |
52 |
52 |
53 lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF" |
53 lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF" |
54 by (induct x rule: tr_induct) simp_all |
54 by (induct x rule: tr_induct) simp_all |
55 |
55 |
56 lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF" |
56 lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF" |
57 by (induct x rule: tr_induct) simp_all |
57 by (induct x rule: tr_induct) simp_all |
58 |
58 |
59 lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT" |
59 lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT" |
60 by (induct x rule: tr_induct) simp_all |
60 by (induct x rule: tr_induct) simp_all |
61 |
61 |
62 |
62 |
63 subsection {* Case analysis *} |
63 subsection {* Case analysis *} |
64 |
64 |