author | wenzelm |
Wed, 11 Jun 2008 15:41:08 +0200 | |
changeset 27148 | 5b78e50adc49 |
parent 25135 | 4f8176c940cf |
child 27294 | c11e716fafeb |
permissions | -rw-r--r-- |
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 |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
20 |
"tr" <= (type) "bool lift" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
21 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
22 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
23 |
TT :: "tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
24 |
"TT = Def True" |
2640 | 25 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
26 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
27 |
FF :: "tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
28 |
"FF = Def False" |
2640 | 29 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
30 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
31 |
trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
32 |
ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
33 |
abbreviation |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
34 |
cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
35 |
"If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b" |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
36 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
37 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
38 |
trand :: "tr \<rightarrow> tr \<rightarrow> tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
39 |
andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
40 |
abbreviation |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
41 |
andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
42 |
"x andalso y == trand\<cdot>x\<cdot>y" |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
43 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
44 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
45 |
tror :: "tr \<rightarrow> tr \<rightarrow> tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
46 |
orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
47 |
abbreviation |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
48 |
orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
49 |
"x orelse y == tror\<cdot>x\<cdot>y" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
50 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
51 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
52 |
neg :: "tr \<rightarrow> tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
53 |
"neg = flift2 Not" |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
54 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
55 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
56 |
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
57 |
"If2 Q x y = (If Q then x else y fi)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
58 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
59 |
translations |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
60 |
"\<Lambda> (CONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
61 |
"\<Lambda> (CONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
62 |
|
15649 | 63 |
|
64 |
text {* Exhaustion and Elimination for type @{typ tr} *} |
|
65 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
66 |
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" |
15649 | 67 |
apply (unfold FF_def TT_def) |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
68 |
apply (induct t) |
15649 | 69 |
apply fast |
70 |
apply fast |
|
71 |
done |
|
72 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
73 |
lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
15649 | 74 |
apply (rule Exh_tr [THEN disjE]) |
75 |
apply fast |
|
76 |
apply (erule disjE) |
|
77 |
apply fast |
|
78 |
apply fast |
|
79 |
done |
|
80 |
||
81 |
text {* tactic for tr-thms with case split *} |
|
82 |
||
83 |
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def |
|
27148 | 84 |
|
85 |
||
15649 | 86 |
text {* distinctness for type @{typ tr} *} |
87 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
88 |
lemma dist_less_tr [simp]: |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
89 |
"\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT" |
15649 | 90 |
by (simp_all add: tr_defs) |
91 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
92 |
lemma dist_eq_tr [simp]: |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
93 |
"TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" |
15649 | 94 |
by (simp_all add: tr_defs) |
95 |
||
96 |
text {* lemmas about andalso, orelse, neg and if *} |
|
97 |
||
98 |
lemma ifte_thms [simp]: |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
99 |
"If \<bottom> then e1 else e2 fi = \<bottom>" |
15649 | 100 |
"If FF then e1 else e2 fi = e2" |
101 |
"If TT then e1 else e2 fi = e1" |
|
16756 | 102 |
by (simp_all add: ifte_def TT_def FF_def) |
15649 | 103 |
|
104 |
lemma andalso_thms [simp]: |
|
105 |
"(TT andalso y) = y" |
|
106 |
"(FF andalso y) = FF" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
107 |
"(\<bottom> andalso y) = \<bottom>" |
15649 | 108 |
"(y andalso TT) = y" |
109 |
"(y andalso y) = y" |
|
110 |
apply (unfold andalso_def, simp_all) |
|
111 |
apply (rule_tac p=y in trE, simp_all) |
|
112 |
apply (rule_tac p=y in trE, simp_all) |
|
113 |
done |
|
114 |
||
115 |
lemma orelse_thms [simp]: |
|
116 |
"(TT orelse y) = TT" |
|
117 |
"(FF orelse y) = y" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
118 |
"(\<bottom> orelse y) = \<bottom>" |
15649 | 119 |
"(y orelse FF) = y" |
120 |
"(y orelse y) = y" |
|
121 |
apply (unfold orelse_def, simp_all) |
|
122 |
apply (rule_tac p=y in trE, simp_all) |
|
123 |
apply (rule_tac p=y in trE, simp_all) |
|
124 |
done |
|
125 |
||
126 |
lemma neg_thms [simp]: |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
127 |
"neg\<cdot>TT = FF" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
128 |
"neg\<cdot>FF = TT" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
129 |
"neg\<cdot>\<bottom> = \<bottom>" |
15649 | 130 |
by (simp_all add: neg_def TT_def FF_def) |
131 |
||
132 |
text {* split-tac for If via If2 because the constant has to be a constant *} |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
133 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
134 |
lemma split_If2: |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
135 |
"P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" |
15649 | 136 |
apply (unfold If2_def) |
137 |
apply (rule_tac p = "Q" in trE) |
|
138 |
apply (simp_all) |
|
139 |
done |
|
140 |
||
16121 | 141 |
ML {* |
15649 | 142 |
val split_If_tac = |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
143 |
simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym]) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
144 |
THEN' (split_tac [@{thm split_If2}]) |
15649 | 145 |
*} |
146 |
||
147 |
subsection "Rewriting of HOLCF operations to HOL functions" |
|
148 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
149 |
lemma andalso_or: |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
150 |
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" |
15649 | 151 |
apply (rule_tac p = "t" in trE) |
152 |
apply simp_all |
|
153 |
done |
|
154 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
155 |
lemma andalso_and: |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
156 |
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) = (t \<noteq> FF \<and> s \<noteq> FF)" |
15649 | 157 |
apply (rule_tac p = "t" in trE) |
158 |
apply simp_all |
|
159 |
done |
|
160 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
161 |
lemma Def_bool1 [simp]: "(Def x \<noteq> FF) = x" |
15649 | 162 |
by (simp add: FF_def) |
163 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
164 |
lemma Def_bool2 [simp]: "(Def x = FF) = (\<not> x)" |
15649 | 165 |
by (simp add: FF_def) |
166 |
||
167 |
lemma Def_bool3 [simp]: "(Def x = TT) = x" |
|
168 |
by (simp add: TT_def) |
|
169 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
170 |
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" |
15649 | 171 |
by (simp add: TT_def) |
172 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
173 |
lemma If_and_if: |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
174 |
"(If Def P then A else B fi) = (if P then A else B)" |
15649 | 175 |
apply (rule_tac p = "Def P" in trE) |
176 |
apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) |
|
177 |
done |
|
178 |
||
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
179 |
subsection {* Compactness *} |
15649 | 180 |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
181 |
lemma compact_TT [simp]: "compact TT" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
182 |
by (rule compact_chfin) |
15649 | 183 |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
184 |
lemma compact_FF [simp]: "compact FF" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
185 |
by (rule compact_chfin) |
2640 | 186 |
|
187 |
end |