1.1 --- a/src/HOLCF/Tr.thy Fri Jun 20 18:00:55 2008 +0200
1.2 +++ b/src/HOLCF/Tr.thy Fri Jun 20 18:03:01 2008 +0200
1.3 @@ -11,7 +11,7 @@
1.4 imports Lift
1.5 begin
1.6
1.7 -defaultsort pcpo
1.8 +subsection {* Type definition and constructors *}
1.9
1.10 types
1.11 tr = "bool lift"
1.12 @@ -27,6 +27,44 @@
1.13 FF :: "tr" where
1.14 "FF = Def False"
1.15
1.16 +text {* Exhaustion and Elimination for type @{typ tr} *}
1.17 +
1.18 +lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
1.19 +unfolding FF_def TT_def by (induct t) auto
1.20 +
1.21 +lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
1.22 +unfolding FF_def TT_def by (induct p) auto
1.23 +
1.24 +lemma tr_induct: "\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x"
1.25 +by (cases x rule: trE) simp_all
1.26 +
1.27 +text {* distinctness for type @{typ tr} *}
1.28 +
1.29 +lemma dist_less_tr [simp]:
1.30 + "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
1.31 +unfolding TT_def FF_def by simp_all
1.32 +
1.33 +lemma dist_eq_tr [simp]:
1.34 + "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
1.35 +unfolding TT_def FF_def by simp_all
1.36 +
1.37 +lemma TT_less_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
1.38 +by (induct x rule: tr_induct) simp_all
1.39 +
1.40 +lemma FF_less_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
1.41 +by (induct x rule: tr_induct) simp_all
1.42 +
1.43 +lemma not_less_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
1.44 +by (induct x rule: tr_induct) simp_all
1.45 +
1.46 +lemma not_less_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
1.47 +by (induct x rule: tr_induct) simp_all
1.48 +
1.49 +
1.50 +subsection {* Case analysis *}
1.51 +
1.52 +defaultsort pcpo
1.53 +
1.54 definition
1.55 trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
1.56 ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
1.57 @@ -34,6 +72,19 @@
1.58 cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where
1.59 "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
1.60
1.61 +translations
1.62 + "\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
1.63 + "\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
1.64 +
1.65 +lemma ifte_thms [simp]:
1.66 + "If \<bottom> then e1 else e2 fi = \<bottom>"
1.67 + "If FF then e1 else e2 fi = e2"
1.68 + "If TT then e1 else e2 fi = e1"
1.69 +by (simp_all add: ifte_def TT_def FF_def)
1.70 +
1.71 +
1.72 +subsection {* Boolean connectives *}
1.73 +
1.74 definition
1.75 trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
1.76 andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
1.77 @@ -56,51 +107,12 @@
1.78 If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
1.79 "If2 Q x y = (If Q then x else y fi)"
1.80
1.81 -translations
1.82 - "\<Lambda> (CONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
1.83 - "\<Lambda> (CONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
1.84 -
1.85 -
1.86 -text {* Exhaustion and Elimination for type @{typ tr} *}
1.87 -
1.88 -lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
1.89 -apply (unfold FF_def TT_def)
1.90 -apply (induct t)
1.91 -apply fast
1.92 -apply fast
1.93 -done
1.94 -
1.95 -lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
1.96 -apply (rule Exh_tr [THEN disjE])
1.97 -apply fast
1.98 -apply (erule disjE)
1.99 -apply fast
1.100 -apply fast
1.101 -done
1.102 -
1.103 text {* tactic for tr-thms with case split *}
1.104
1.105 lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
1.106
1.107 -
1.108 -text {* distinctness for type @{typ tr} *}
1.109 -
1.110 -lemma dist_less_tr [simp]:
1.111 - "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
1.112 -by (simp_all add: tr_defs)
1.113 -
1.114 -lemma dist_eq_tr [simp]:
1.115 - "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
1.116 -by (simp_all add: tr_defs)
1.117 -
1.118 text {* lemmas about andalso, orelse, neg and if *}
1.119
1.120 -lemma ifte_thms [simp]:
1.121 - "If \<bottom> then e1 else e2 fi = \<bottom>"
1.122 - "If FF then e1 else e2 fi = e2"
1.123 - "If TT then e1 else e2 fi = e1"
1.124 -by (simp_all add: ifte_def TT_def FF_def)
1.125 -
1.126 lemma andalso_thms [simp]:
1.127 "(TT andalso y) = y"
1.128 "(FF andalso y) = FF"
1.129 @@ -108,8 +120,8 @@
1.130 "(y andalso TT) = y"
1.131 "(y andalso y) = y"
1.132 apply (unfold andalso_def, simp_all)
1.133 -apply (rule_tac p=y in trE, simp_all)
1.134 -apply (rule_tac p=y in trE, simp_all)
1.135 +apply (cases y rule: trE, simp_all)
1.136 +apply (cases y rule: trE, simp_all)
1.137 done
1.138
1.139 lemma orelse_thms [simp]:
1.140 @@ -119,8 +131,8 @@
1.141 "(y orelse FF) = y"
1.142 "(y orelse y) = y"
1.143 apply (unfold orelse_def, simp_all)
1.144 -apply (rule_tac p=y in trE, simp_all)
1.145 -apply (rule_tac p=y in trE, simp_all)
1.146 +apply (cases y rule: trE, simp_all)
1.147 +apply (cases y rule: trE, simp_all)
1.148 done
1.149
1.150 lemma neg_thms [simp]:
1.151 @@ -178,10 +190,10 @@
1.152
1.153 subsection {* Compactness *}
1.154
1.155 -lemma compact_TT [simp]: "compact TT"
1.156 +lemma compact_TT: "compact TT"
1.157 by (rule compact_chfin)
1.158
1.159 -lemma compact_FF [simp]: "compact FF"
1.160 +lemma compact_FF: "compact FF"
1.161 by (rule compact_chfin)
1.162
1.163 end