author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 18081  fe15796b257d 
child 25131  2c8caac48ade 
permissions  rwrr 
2640  1 
(* Title: HOLCF/Tr.thy 
2 
ID: $Id$ 

3 
Author: Franz Regensburger 

4 

16070
4a83dd540b88
removed LICENCE note  everything is subject to Isabelle licence as
wenzelm
parents:
15649
diff
changeset

5 
Introduce infix if_then_else_fi and boolean connectives andalso, orelse. 
2640  6 
*) 
7 

15649  8 
header {* The type of lifted booleans *} 
9 

10 
theory Tr 

16228  11 
imports Lift 
15649  12 
begin 
2640  13 

16631  14 
defaultsort pcpo 
15 

2782  16 
types 
17 
tr = "bool lift" 

18 

2766  19 
translations 
2782  20 
"tr" <= (type) "bool lift" 
2640  21 

22 
consts 

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

23 
TT :: "tr" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

24 
FF :: "tr" 
18081
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

25 
trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

26 
trand :: "tr \<rightarrow> tr \<rightarrow> tr" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

27 
tror :: "tr \<rightarrow> tr \<rightarrow> tr" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

28 
neg :: "tr \<rightarrow> tr" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

29 
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" 
2640  30 

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

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

32 
"@cifte" :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

33 
"@andalso" :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

34 
"@orelse" :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) 
2640  35 

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

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

37 
"x andalso y" == "trand\<cdot>x\<cdot>y" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

38 
"x orelse y" == "tror\<cdot>x\<cdot>y" 
18081
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

39 
"If b then e1 else e2 fi" == "trifte\<cdot>e1\<cdot>e2\<cdot>b" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

40 

fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

41 
translations 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

42 
"\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

43 
"\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t" 
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

44 

2640  45 
defs 
18081
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

46 
TT_def: "TT \<equiv> Def True" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

47 
FF_def: "FF \<equiv> Def False" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

48 
neg_def: "neg \<equiv> flift2 Not" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

49 
ifte_def: "trifte \<equiv> \<Lambda> t e. FLIFT b. if b then t else e" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

50 
andalso_def: "trand \<equiv> \<Lambda> x y. If x then y else FF fi" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

51 
orelse_def: "tror \<equiv> \<Lambda> x y. If x then TT else y fi" 
fe15796b257d
changed order of arguments for constant behind Ifthenelsefi syntax; added LAM patterns for TT, FF
huffman
parents:
18070
diff
changeset

52 
If2_def: "If2 Q x y \<equiv> If Q then x else y fi" 
15649  53 

54 
text {* Exhaustion and Elimination for type @{typ tr} *} 

55 

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

56 
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" 
15649  57 
apply (unfold FF_def TT_def) 
58 
apply (induct_tac "t") 

59 
apply fast 

60 
apply fast 

61 
done 

62 

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

63 
lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
15649  64 
apply (rule Exh_tr [THEN disjE]) 
65 
apply fast 

66 
apply (erule disjE) 

67 
apply fast 

68 
apply fast 

69 
done 

70 

71 
text {* tactic for trthms with case split *} 

72 

73 
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def 

74 
(* 

75 
fun prover t = prove_goal thy t 

76 
(fn prems => 

77 
[ 

78 
(res_inst_tac [("p","y")] trE 1), 

79 
(REPEAT(asm_simp_tac (simpset() addsimps 

80 
[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) 

81 
]) 

82 
*) 

83 
text {* distinctness for type @{typ tr} *} 

84 

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

85 
lemma dist_less_tr [simp]: 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

86 
"\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" 
15649  87 
by (simp_all add: tr_defs) 
88 

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

89 
lemma dist_eq_tr [simp]: 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

90 
"TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" 
15649  91 
by (simp_all add: tr_defs) 
92 

93 
text {* lemmas about andalso, orelse, neg and if *} 

94 

95 
lemma ifte_thms [simp]: 

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

96 
"If \<bottom> then e1 else e2 fi = \<bottom>" 
15649  97 
"If FF then e1 else e2 fi = e2" 
98 
"If TT then e1 else e2 fi = e1" 

16756  99 
by (simp_all add: ifte_def TT_def FF_def) 
15649  100 

101 
lemma andalso_thms [simp]: 

102 
"(TT andalso y) = y" 

103 
"(FF andalso y) = FF" 

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

104 
"(\<bottom> andalso y) = \<bottom>" 
15649  105 
"(y andalso TT) = y" 
106 
"(y andalso y) = y" 

107 
apply (unfold andalso_def, simp_all) 

108 
apply (rule_tac p=y in trE, simp_all) 

109 
apply (rule_tac p=y in trE, simp_all) 

110 
done 

111 

112 
lemma orelse_thms [simp]: 

113 
"(TT orelse y) = TT" 

114 
"(FF orelse y) = y" 

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

115 
"(\<bottom> orelse y) = \<bottom>" 
15649  116 
"(y orelse FF) = y" 
117 
"(y orelse y) = y" 

118 
apply (unfold orelse_def, simp_all) 

119 
apply (rule_tac p=y in trE, simp_all) 

120 
apply (rule_tac p=y in trE, simp_all) 

121 
done 

122 

123 
lemma neg_thms [simp]: 

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

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

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

126 
"neg\<cdot>\<bottom> = \<bottom>" 
15649  127 
by (simp_all add: neg_def TT_def FF_def) 
128 

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

130 

131 
lemma split_If2: 

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

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

135 
apply (simp_all) 

136 
done 

137 

16121  138 
ML {* 
15649  139 
val split_If_tac = 
140 
simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")]) 

141 
THEN' (split_tac [thm "split_If2"]) 

142 
*} 

143 

144 
subsection "Rewriting of HOLCF operations to HOL functions" 

145 

146 
lemma andalso_or: 

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

147 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" 
15649  148 
apply (rule_tac p = "t" in trE) 
149 
apply simp_all 

150 
done 

151 

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

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

153 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)" 
15649  154 
apply (rule_tac p = "t" in trE) 
155 
apply simp_all 

156 
done 

157 

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

158 
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x" 
15649  159 
by (simp add: FF_def) 
160 

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

161 
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)" 
15649  162 
by (simp add: FF_def) 
163 

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

165 
by (simp add: TT_def) 

166 

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

167 
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" 
15649  168 
by (simp add: TT_def) 
169 

170 
lemma If_and_if: 

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

171 
"(If Def P then A else B fi) = (if P then A else B)" 
15649  172 
apply (rule_tac p = "Def P" in trE) 
173 
apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) 

174 
done 

175 

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

176 
subsection {* Compactness *} 
15649  177 

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

178 
lemma compact_TT [simp]: "compact TT" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

179 
by (rule compact_chfin) 
15649  180 

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

181 
lemma compact_FF [simp]: "compact FF" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

182 
by (rule compact_chfin) 
2640  183 

184 
end 