# HG changeset patch
# User huffman
# Date 1213977781 -7200
# Node ID c11e716fafeb99caa12a077014ef8766af19efda
# Parent  de9a2fd0eab448144a5478bfb957194f91021dc9
added some lemmas; reorganized into sections; tuned proofs

diff -r de9a2fd0eab4 -r c11e716fafeb src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Fri Jun 20 18:00:55 2008 +0200
+++ b/src/HOLCF/Tr.thy	Fri Jun 20 18:03:01 2008 +0200
@@ -11,7 +11,7 @@
 imports Lift
 begin
 
-defaultsort pcpo
+subsection {* Type definition and constructors *}
 
 types
   tr = "bool lift"
@@ -27,6 +27,44 @@
   FF :: "tr" where
   "FF = Def False"
 
+text {* Exhaustion and Elimination for type @{typ tr} *}
+
+lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
+unfolding FF_def TT_def by (induct t) auto
+
+lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
+unfolding FF_def TT_def by (induct p) auto
+
+lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
+by (cases x rule: trE) simp_all
+
+text {* distinctness for type @{typ tr} *}
+
+lemma dist_less_tr [simp]:
+  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
+unfolding TT_def FF_def by simp_all
+
+lemma dist_eq_tr [simp]:
+  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
+unfolding TT_def FF_def by simp_all
+
+lemma TT_less_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
+by (induct x rule: tr_induct) simp_all
+
+lemma FF_less_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
+by (induct x rule: tr_induct) simp_all
+
+lemma not_less_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
+by (induct x rule: tr_induct) simp_all
+
+lemma not_less_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
+by (induct x rule: tr_induct) simp_all
+
+
+subsection {* Case analysis *}
+
+defaultsort pcpo
+
 definition
   trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
   ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
@@ -34,6 +72,19 @@
   cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c"  ("(3If _/ (then _/ else _) fi)" 60)  where
   "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
 
+translations
+  "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
+  "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
+
+lemma ifte_thms [simp]:
+  "If \<bottom> then e1 else e2 fi = \<bottom>"
+  "If FF then e1 else e2 fi = e2"
+  "If TT then e1 else e2 fi = e1"
+by (simp_all add: ifte_def TT_def FF_def)
+
+
+subsection {* Boolean connectives *}
+
 definition
   trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
   andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
@@ -56,51 +107,12 @@
   If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
   "If2 Q x y = (If Q then x else y fi)"
 
-translations
-  "\<Lambda> (CONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
-  "\<Lambda> (CONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
-
-
-text {* Exhaustion and Elimination for type @{typ tr} *}
-
-lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
-apply (unfold FF_def TT_def)
-apply (induct t)
-apply fast
-apply fast
-done
-
-lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
-apply (rule Exh_tr [THEN disjE])
-apply fast
-apply (erule disjE)
-apply fast
-apply fast
-done
-
 text {* tactic for tr-thms with case split *}
 
 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
 
-
-text {* distinctness for type @{typ tr} *}
-
-lemma dist_less_tr [simp]:
-  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
-by (simp_all add: tr_defs)
-
-lemma dist_eq_tr [simp]:
-  "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
-by (simp_all add: tr_defs)
-
 text {* lemmas about andalso, orelse, neg and if *}
 
-lemma ifte_thms [simp]:
-  "If \<bottom> then e1 else e2 fi = \<bottom>"
-  "If FF then e1 else e2 fi = e2"
-  "If TT then e1 else e2 fi = e1"
-by (simp_all add: ifte_def TT_def FF_def)
-
 lemma andalso_thms [simp]:
   "(TT andalso y) = y"
   "(FF andalso y) = FF"
@@ -108,8 +120,8 @@
   "(y andalso TT) = y"
   "(y andalso y) = y"
 apply (unfold andalso_def, simp_all)
-apply (rule_tac p=y in trE, simp_all)
-apply (rule_tac p=y in trE, simp_all)
+apply (cases y rule: trE, simp_all)
+apply (cases y rule: trE, simp_all)
 done
 
 lemma orelse_thms [simp]:
@@ -119,8 +131,8 @@
   "(y orelse FF) = y"
   "(y orelse y) = y"
 apply (unfold orelse_def, simp_all)
-apply (rule_tac p=y in trE, simp_all)
-apply (rule_tac p=y in trE, simp_all)
+apply (cases y rule: trE, simp_all)
+apply (cases y rule: trE, simp_all)
 done
 
 lemma neg_thms [simp]:
@@ -178,10 +190,10 @@
 
 subsection {* Compactness *}
 
-lemma compact_TT [simp]: "compact TT"
+lemma compact_TT: "compact TT"
 by (rule compact_chfin)
 
-lemma compact_FF [simp]: "compact FF"
+lemma compact_FF: "compact FF"
 by (rule compact_chfin)
 
 end