author  huffman 
Wed, 27 Oct 2010 14:15:54 0700  
changeset 40322  707eb30e8a53 
parent 36452  d37c6eed8117 
child 40324  b5e1ab22198a 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Tr.thy 
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 

2782  13 
types 
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]: 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

43 
"\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" 
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 

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

56 
lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> 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 

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

59 
lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> 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 

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

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

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

69 
ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)" 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
36452
diff
changeset

70 

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

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

72 
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

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

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

75 

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

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

77 
"\<Lambda> (XCONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>" 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

78 
"\<Lambda> (XCONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t" 
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

79 

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

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

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

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

83 
"If TT then e1 else e2 = e1" 
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset

84 
by (simp_all add: ifte_def TT_def FF_def) 
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 

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

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

88 

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

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

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

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

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

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

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

95 

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

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

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

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

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

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

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

102 

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

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

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

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

106 

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

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

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

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

110 

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

113 
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def 

27148  114 

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

117 
lemma andalso_thms [simp]: 

118 
"(TT andalso y) = y" 

119 
"(FF andalso y) = FF" 

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

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

123 
apply (unfold andalso_def, simp_all) 

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

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

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

128 
lemma orelse_thms [simp]: 

129 
"(TT orelse y) = TT" 

130 
"(FF orelse y) = y" 

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

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

134 
apply (unfold orelse_def, simp_all) 

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

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

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

139 
lemma neg_thms [simp]: 

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

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

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

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

145 
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

146 

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

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

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

151 
apply (simp_all) 

152 
done 

153 

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

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

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

160 
subsection "Rewriting of HOLCF operations to HOL functions" 

161 

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

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

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

166 
done 

167 

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

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

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

172 
done 

173 

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

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

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

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

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

181 
by (simp add: TT_def) 

182 

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

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

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

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

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

190 
done 

191 

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

192 
subsection {* Compactness *} 
15649  193 

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

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

195 
by (rule compact_chfin) 
15649  196 

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

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

198 
by (rule compact_chfin) 
2640  199 

200 
end 