author  huffman 
Thu, 03 Nov 2005 00:12:29 +0100  
changeset 18070  b653e18f0a41 
parent 16756  e05c8039873a 
child 18081  fe15796b257d 
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" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

25 
Icifte :: "tr \<rightarrow> 'c \<rightarrow> 'c \<rightarrow> 'c" 
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" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

39 
"If b then e1 else e2 fi" == "Icifte\<cdot>b\<cdot>e1\<cdot>e2" 
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset

40 

2640  41 
defs 
15649  42 
TT_def: "TT==Def True" 
43 
FF_def: "FF==Def False" 

44 
neg_def: "neg == flift2 Not" 

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

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

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

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

49 

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

51 

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

52 
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" 
15649  53 
apply (unfold FF_def TT_def) 
54 
apply (induct_tac "t") 

55 
apply fast 

56 
apply fast 

57 
done 

58 

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

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

62 
apply (erule disjE) 

63 
apply fast 

64 
apply fast 

65 
done 

66 

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

68 

69 
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def 

70 
(* 

71 
fun prover t = prove_goal thy t 

72 
(fn prems => 

73 
[ 

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

75 
(REPEAT(asm_simp_tac (simpset() addsimps 

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

77 
]) 

78 
*) 

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

80 

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

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

82 
"\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" 
15649  83 
by (simp_all add: tr_defs) 
84 

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

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

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

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

90 

91 
lemma ifte_thms [simp]: 

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

92 
"If \<bottom> then e1 else e2 fi = \<bottom>" 
15649  93 
"If FF then e1 else e2 fi = e2" 
94 
"If TT then e1 else e2 fi = e1" 

16756  95 
by (simp_all add: ifte_def TT_def FF_def) 
15649  96 

97 
lemma andalso_thms [simp]: 

98 
"(TT andalso y) = y" 

99 
"(FF andalso y) = FF" 

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

100 
"(\<bottom> andalso y) = \<bottom>" 
15649  101 
"(y andalso TT) = y" 
102 
"(y andalso y) = y" 

103 
apply (unfold andalso_def, simp_all) 

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

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

106 
done 

107 

108 
lemma orelse_thms [simp]: 

109 
"(TT orelse y) = TT" 

110 
"(FF orelse y) = y" 

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

111 
"(\<bottom> orelse y) = \<bottom>" 
15649  112 
"(y orelse FF) = y" 
113 
"(y orelse y) = y" 

114 
apply (unfold orelse_def, simp_all) 

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

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

117 
done 

118 

119 
lemma neg_thms [simp]: 

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

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

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

122 
"neg\<cdot>\<bottom> = \<bottom>" 
15649  123 
by (simp_all add: neg_def TT_def FF_def) 
124 

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

126 

127 
lemma split_If2: 

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

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

131 
apply (simp_all) 

132 
done 

133 

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

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

138 
*} 

139 

140 
subsection "Rewriting of HOLCF operations to HOL functions" 

141 

142 
lemma andalso_or: 

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

143 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" 
15649  144 
apply (rule_tac p = "t" in trE) 
145 
apply simp_all 

146 
done 

147 

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

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

149 
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)" 
15649  150 
apply (rule_tac p = "t" in trE) 
151 
apply simp_all 

152 
done 

153 

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

154 
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x" 
15649  155 
by (simp add: FF_def) 
156 

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

157 
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)" 
15649  158 
by (simp add: FF_def) 
159 

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

161 
by (simp add: TT_def) 

162 

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

163 
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" 
15649  164 
by (simp add: TT_def) 
165 

166 
lemma If_and_if: 

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

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

170 
done 

171 

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

172 
subsection {* Compactness *} 
15649  173 

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

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

175 
by (rule compact_chfin) 
15649  176 

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

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

178 
by (rule compact_chfin) 
2640  179 

180 
end 