author  wenzelm 
Tue, 31 May 2005 11:53:12 +0200  
changeset 16121  a80aa66d2271 
parent 16070  4a83dd540b88 
child 16228  9b5b0c92230a 
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 

11 
imports Lift Fix 

12 
begin 

2640  13 

2782  14 
types 
15 
tr = "bool lift" 

16 

2766  17 
translations 
2782  18 
"tr" <= (type) "bool lift" 
2640  19 

20 
consts 

15649  21 
TT :: "tr" 
22 
FF :: "tr" 

2640  23 
Icifte :: "tr > 'c > 'c > 'c" 
24 
trand :: "tr > tr > tr" 

25 
tror :: "tr > tr > tr" 

26 
neg :: "tr > tr" 

3036  27 
If2 :: "tr=>'c=>'c=>'c" 
2640  28 

29 
syntax "@cifte" :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60) 

30 
"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35) 

31 
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30) 

32 

33 
translations 

10834  34 
"x andalso y" == "trand$x$y" 
35 
"x orelse y" == "tror$x$y" 

36 
"If b then e1 else e2 fi" == "Icifte$b$e1$e2" 

2640  37 
defs 
15649  38 
TT_def: "TT==Def True" 
39 
FF_def: "FF==Def False" 

40 
neg_def: "neg == flift2 Not" 

41 
ifte_def: "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)" 

42 
andalso_def: "trand == (LAM x y. If x then y else FF fi)" 

43 
orelse_def: "tror == (LAM x y. If x then TT else y fi)" 

44 
If2_def: "If2 Q x y == If Q then x else y fi" 

45 

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

47 

48 
lemma Exh_tr: "t=UU  t = TT  t = FF" 

49 
apply (unfold FF_def TT_def) 

50 
apply (induct_tac "t") 

51 
apply fast 

52 
apply fast 

53 
done 

54 

55 
lemma trE: "[ p=UU ==> Q; p = TT ==>Q; p = FF ==>Q] ==>Q" 

56 
apply (rule Exh_tr [THEN disjE]) 

57 
apply fast 

58 
apply (erule disjE) 

59 
apply fast 

60 
apply fast 

61 
done 

62 

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

64 

65 
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def 

66 
(* 

67 
fun prover t = prove_goal thy t 

68 
(fn prems => 

69 
[ 

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

71 
(REPEAT(asm_simp_tac (simpset() addsimps 

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

73 
]) 

74 
*) 

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

76 

77 
lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT" 

78 
by (simp_all add: tr_defs) 

79 

80 
lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT" 

81 
by (simp_all add: tr_defs) 

82 

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

84 

85 
lemma ifte_simp: 

86 
"If x then e1 else e2 fi = 

87 
flift1 (%b. if b then e1 else e2)$x" 

88 
apply (unfold ifte_def TT_def FF_def flift1_def) 

89 
apply (simp add: cont_flift1_arg cont_if) 

90 
done 

91 

92 
lemma ifte_thms [simp]: 

93 
"If UU then e1 else e2 fi = UU" 

94 
"If FF then e1 else e2 fi = e2" 

95 
"If TT then e1 else e2 fi = e1" 

96 
by (simp_all add: ifte_simp TT_def FF_def) 

97 

98 
lemma andalso_thms [simp]: 

99 
"(TT andalso y) = y" 

100 
"(FF andalso y) = FF" 

101 
"(UU andalso y) = UU" 

102 
"(y andalso TT) = y" 

103 
"(y andalso y) = y" 

104 
apply (unfold andalso_def, simp_all) 

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

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

107 
done 

108 

109 
lemma orelse_thms [simp]: 

110 
"(TT orelse y) = TT" 

111 
"(FF orelse y) = y" 

112 
"(UU orelse y) = UU" 

113 
"(y orelse FF) = y" 

114 
"(y orelse y) = y" 

115 
apply (unfold orelse_def, simp_all) 

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

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

118 
done 

119 

120 
lemma neg_thms [simp]: 

121 
"neg$TT = FF" 

122 
"neg$FF = TT" 

123 
"neg$UU = UU" 

124 
by (simp_all add: neg_def TT_def FF_def) 

125 

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

127 

128 
lemma split_If2: 

129 
"P (If2 Q x y ) = ((Q=UU > P UU) & (Q=TT > P x) & (Q=FF > P y))" 

130 
apply (unfold If2_def) 

131 
apply (rule_tac p = "Q" in trE) 

132 
apply (simp_all) 

133 
done 

134 

16121  135 
ML {* 
15649  136 
val split_If_tac = 
137 
simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")]) 

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

139 
*} 

140 

141 
subsection "Rewriting of HOLCF operations to HOL functions" 

142 

143 
lemma andalso_or: 

144 
"!!t.[t~=UU]==> ((t andalso s)=FF)=(t=FF  s=FF)" 

145 
apply (rule_tac p = "t" in trE) 

146 
apply simp_all 

147 
done 

148 

149 
lemma andalso_and: "[t~=UU]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)" 

150 
apply (rule_tac p = "t" in trE) 

151 
apply simp_all 

152 
done 

153 

154 
lemma Def_bool1 [simp]: "(Def x ~= FF) = x" 

155 
by (simp add: FF_def) 

156 

157 
lemma Def_bool2 [simp]: "(Def x = FF) = (~x)" 

158 
by (simp add: FF_def) 

159 

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

161 
by (simp add: TT_def) 

162 

163 
lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)" 

164 
by (simp add: TT_def) 

165 

166 
lemma If_and_if: 

167 
"(If Def P then A else B fi)= (if P then A else B)" 

168 
apply (rule_tac p = "Def P" in trE) 

169 
apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) 

170 
done 

171 

172 
subsection "admissibility" 

173 

174 
text {* 

175 
The following rewrite rules for admissibility should in the future be 

176 
replaced by a more general admissibility test that also checks 

177 
chainfiniteness, of which these lemmata are specific examples 

178 
*} 

179 

180 
lemma adm_trick_1: "(x~=FF) = (x=TTx=UU)" 

181 
apply (rule_tac p = "x" in trE) 

182 
apply (simp_all) 

183 
done 

184 

185 
lemma adm_trick_2: "(x~=TT) = (x=FFx=UU)" 

186 
apply (rule_tac p = "x" in trE) 

187 
apply (simp_all) 

188 
done 

189 

190 
lemmas adm_tricks = adm_trick_1 adm_trick_2 

191 

192 
lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)" 

193 
by (simp add: adm_tricks) 

194 

195 
lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)" 

196 
by (simp add: adm_tricks) 

2640  197 

198 
end 