author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 48659  40a87b4dac19 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Tr.thy 
2640  2 
Author: Franz Regensburger 
3 
*) 

4 

15649  5 
header {* The type of lifted booleans *} 
6 

7 
theory Tr 

16228  8 
imports Lift 
15649  9 
begin 
2640  10 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

11 
subsection {* Type definition and constructors *} 
16631  12 

41295  13 
type_synonym 
2782  14 
tr = "bool lift" 
15 

2766  16 
translations 
35431  17 
(type) "tr" <= (type) "bool lift" 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

18 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

19 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

20 
TT :: "tr" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

21 
"TT = Def True" 
2640  22 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

23 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

24 
FF :: "tr" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

25 
"FF = Def False" 
2640  26 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

27 
text {* Exhaustion and Elimination for type @{typ tr} *} 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

28 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

29 
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

30 
unfolding FF_def TT_def by (induct t) auto 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

31 

35783  32 
lemma trE [case_names bottom TT FF]: 
33 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

34 
unfolding FF_def TT_def by (induct p) auto 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

35 

35783  36 
lemma tr_induct [case_names bottom TT FF]: 
37 
"\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x" 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

38 
by (cases x rule: trE) simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

39 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

40 
text {* distinctness for type @{typ tr} *} 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

41 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

42 
lemma dist_below_tr [simp]: 
41182  43 
"TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

44 
unfolding TT_def FF_def by simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

45 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

46 
lemma dist_eq_tr [simp]: 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

47 
"TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

48 
unfolding TT_def FF_def by simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

49 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

50 
lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

51 
by (induct x rule: tr_induct) simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

52 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
29138
diff
changeset

53 
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

54 
by (induct x rule: tr_induct) simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

55 

41182  56 
lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

57 
by (induct x rule: tr_induct) simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

58 

41182  59 
lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

60 
by (induct x rule: tr_induct) simp_all 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

61 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

62 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

63 
subsection {* Case analysis *} 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

64 

36452  65 
default_sort pcpo 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

66 

40324  67 
definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where 
68 
"tr_case = (\<Lambda> t e (Def b). if b then t else e)" 

40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

69 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

70 
abbreviation 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

71 
cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) 
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

72 
where 
40324  73 
"If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

74 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

75 
translations 
40324  76 
"\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>" 
77 
"\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t" 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

78 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

79 
lemma ifte_thms [simp]: 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

80 
"If \<bottom> then e1 else e2 = \<bottom>" 
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

81 
"If FF then e1 else e2 = e2" 
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

82 
"If TT then e1 else e2 = e1" 
40324  83 
by (simp_all add: tr_case_def TT_def FF_def) 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

84 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

85 

c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

86 
subsection {* Boolean connectives *} 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

87 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

88 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

89 
trand :: "tr \<rightarrow> tr \<rightarrow> tr" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

90 
andalso_def: "trand = (\<Lambda> x y. If x then y else FF)" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

91 
abbreviation 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

92 
andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

93 
"x andalso y == trand\<cdot>x\<cdot>y" 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

94 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

95 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

96 
tror :: "tr \<rightarrow> tr \<rightarrow> tr" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

97 
orelse_def: "tror = (\<Lambda> x y. If x then TT else y)" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

98 
abbreviation 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

99 
orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where 
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset

100 
"x orelse y == tror\<cdot>x\<cdot>y" 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

101 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

102 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

103 
neg :: "tr \<rightarrow> tr" where 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

104 
"neg = flift2 Not" 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

105 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

106 
definition 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

107 
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

108 
"If2 Q x y = (If Q then x else y)" 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

109 

15649  110 
text {* tactic for trthms with case split *} 
111 

40324  112 
lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def 
27148  113 

15649  114 
text {* lemmas about andalso, orelse, neg and if *} 
115 

116 
lemma andalso_thms [simp]: 

117 
"(TT andalso y) = y" 

118 
"(FF andalso y) = FF" 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

119 
"(\<bottom> andalso y) = \<bottom>" 
15649  120 
"(y andalso TT) = y" 
121 
"(y andalso y) = y" 

122 
apply (unfold andalso_def, simp_all) 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

123 
apply (cases y rule: trE, simp_all) 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

124 
apply (cases y rule: trE, simp_all) 
15649  125 
done 
126 

127 
lemma orelse_thms [simp]: 

128 
"(TT orelse y) = TT" 

129 
"(FF orelse y) = y" 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

130 
"(\<bottom> orelse y) = \<bottom>" 
15649  131 
"(y orelse FF) = y" 
132 
"(y orelse y) = y" 

133 
apply (unfold orelse_def, simp_all) 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

134 
apply (cases y rule: trE, simp_all) 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

135 
apply (cases y rule: trE, simp_all) 
15649  136 
done 
137 

138 
lemma neg_thms [simp]: 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

139 
"neg\<cdot>TT = FF" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

140 
"neg\<cdot>FF = TT" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

141 
"neg\<cdot>\<bottom> = \<bottom>" 
15649  142 
by (simp_all add: neg_def TT_def FF_def) 
143 

144 
text {* splittac for If via If2 because the constant has to be a constant *} 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

145 

4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

146 
lemma split_If2: 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

147 
"P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" 
15649  148 
apply (unfold If2_def) 
149 
apply (rule_tac p = "Q" in trE) 

150 
apply (simp_all) 

151 
done 

152 

16121  153 
ML {* 
15649  154 
val split_If_tac = 
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

155 
simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym]) 
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

156 
THEN' (split_tac [@{thm split_If2}]) 
15649  157 
*} 
158 

159 
subsection "Rewriting of HOLCF operations to HOL functions" 

160 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

161 
lemma andalso_or: 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

162 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" 
15649  163 
apply (rule_tac p = "t" in trE) 
164 
apply simp_all 

165 
done 

166 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

167 
lemma andalso_and: 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

168 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)" 
15649  169 
apply (rule_tac p = "t" in trE) 
170 
apply simp_all 

171 
done 

172 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

173 
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x" 
15649  174 
by (simp add: FF_def) 
175 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

176 
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)" 
15649  177 
by (simp add: FF_def) 
178 

179 
lemma Def_bool3 [simp]: "(Def x = TT) = x" 

180 
by (simp add: TT_def) 

181 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

182 
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" 
15649  183 
by (simp add: TT_def) 
184 

25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset

185 
lemma If_and_if: 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

186 
"(If Def P then A else B) = (if P then A else B)" 
15649  187 
apply (rule_tac p = "Def P" in trE) 
188 
apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) 

189 
done 

190 

18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

191 
subsection {* Compactness *} 
15649  192 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

193 
lemma compact_TT: "compact TT" 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

194 
by (rule compact_chfin) 
15649  195 

27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

196 
lemma compact_FF: "compact FF" 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

197 
by (rule compact_chfin) 
2640  198 

199 
end 