author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 58956 | a816aa3ff391 |
child 62175 | 8ffc4d0e652d |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tr.thy |
2640 | 2 |
Author: Franz Regensburger |
3 |
*) |
|
4 |
||
58880 | 5 |
section {* The type of lifted booleans *} |
15649 | 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 |
|
41295 | 13 |
type_synonym |
2782 | 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 |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
32 |
lemma trE [case_names bottom TT FF, cases type: tr]: |
35783 | 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 |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
36 |
lemma tr_induct [case_names bottom TT FF, induct type: tr]: |
35783 | 37 |
"\<lbrakk>P \<bottom>; P TT; P FF\<rbrakk> \<Longrightarrow> P x" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
38 |
by (cases x) simp_all |
27294
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]: |
41182 | 43 |
"TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT" |
27294
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" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
51 |
by (induct x) simp_all |
27294
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" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
54 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
55 |
|
41182 | 56 |
lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
57 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
58 |
|
41182 | 59 |
lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
60 |
by (induct x) simp_all |
27294
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 |
|
40324 | 67 |
definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" where |
68 |
"tr_case = (\<Lambda> t e (Def b). if b then t else e)" |
|
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
69 |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
70 |
abbreviation |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
71 |
cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) |
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
72 |
where |
40324 | 73 |
"If b then e1 else e2 == tr_case\<cdot>e1\<cdot>e2\<cdot>b" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
74 |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
75 |
translations |
40324 | 76 |
"\<Lambda> (XCONST TT). t" == "CONST tr_case\<cdot>t\<cdot>\<bottom>" |
77 |
"\<Lambda> (XCONST FF). t" == "CONST tr_case\<cdot>\<bottom>\<cdot>t" |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
78 |
|
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
79 |
lemma ifte_thms [simp]: |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
80 |
"If \<bottom> then e1 else e2 = \<bottom>" |
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
81 |
"If FF then e1 else e2 = e2" |
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
82 |
"If TT then e1 else e2 = e1" |
40324 | 83 |
by (simp_all add: tr_case_def TT_def FF_def) |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
84 |
|
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 |
subsection {* Boolean connectives *} |
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
87 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
88 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
89 |
trand :: "tr \<rightarrow> tr \<rightarrow> tr" where |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
90 |
andalso_def: "trand = (\<Lambda> x y. If x then y else FF)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
91 |
abbreviation |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
92 |
andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
93 |
"x andalso y == trand\<cdot>x\<cdot>y" |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
94 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
95 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
96 |
tror :: "tr \<rightarrow> tr \<rightarrow> tr" where |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
97 |
orelse_def: "tror = (\<Lambda> x y. If x then TT else y)" |
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
98 |
abbreviation |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
99 |
orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
100 |
"x orelse y == tror\<cdot>x\<cdot>y" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
101 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
102 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
103 |
neg :: "tr \<rightarrow> tr" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
104 |
"neg = flift2 Not" |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
105 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
106 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
107 |
If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
108 |
"If2 Q x y = (If Q then x else y)" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
109 |
|
15649 | 110 |
text {* tactic for tr-thms with case split *} |
111 |
||
40324 | 112 |
lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def |
27148 | 113 |
|
15649 | 114 |
text {* lemmas about andalso, orelse, neg and if *} |
115 |
||
116 |
lemma andalso_thms [simp]: |
|
117 |
"(TT andalso y) = y" |
|
118 |
"(FF andalso y) = FF" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
119 |
"(\<bottom> andalso y) = \<bottom>" |
15649 | 120 |
"(y andalso TT) = y" |
121 |
"(y andalso y) = y" |
|
122 |
apply (unfold andalso_def, simp_all) |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
123 |
apply (cases y, simp_all) |
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
124 |
apply (cases y, simp_all) |
15649 | 125 |
done |
126 |
||
127 |
lemma orelse_thms [simp]: |
|
128 |
"(TT orelse y) = TT" |
|
129 |
"(FF orelse y) = y" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
130 |
"(\<bottom> orelse y) = \<bottom>" |
15649 | 131 |
"(y orelse FF) = y" |
132 |
"(y orelse y) = y" |
|
133 |
apply (unfold orelse_def, simp_all) |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
134 |
apply (cases y, simp_all) |
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
135 |
apply (cases y, simp_all) |
15649 | 136 |
done |
137 |
||
138 |
lemma neg_thms [simp]: |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
139 |
"neg\<cdot>TT = FF" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
140 |
"neg\<cdot>FF = TT" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
141 |
"neg\<cdot>\<bottom> = \<bottom>" |
15649 | 142 |
by (simp_all add: neg_def TT_def FF_def) |
143 |
||
144 |
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
|
145 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
146 |
lemma split_If2: |
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
147 |
"P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" |
15649 | 148 |
apply (unfold If2_def) |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
149 |
apply (cases Q) |
15649 | 150 |
apply (simp_all) |
151 |
done |
|
152 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
153 |
(* FIXME unused!? *) |
16121 | 154 |
ML {* |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
155 |
fun split_If_tac ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
156 |
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym]) |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58880
diff
changeset
|
157 |
THEN' (split_tac ctxt [@{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)" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
164 |
apply (cases t) |
15649 | 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)" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
170 |
apply (cases t) |
15649 | 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 if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
187 |
"(If Def P then A else B) = (if P then A else B)" |
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
188 |
apply (cases "Def P") |
15649 | 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 |