author | wenzelm |
Sat, 27 Feb 2021 13:20:52 +0100 | |
changeset 73310 | 6e155bb1516d |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tr.thy |
2640 | 2 |
Author: Franz Regensburger |
3 |
*) |
|
4 |
||
62175 | 5 |
section \<open>The type of lifted booleans\<close> |
15649 | 6 |
|
7 |
theory Tr |
|
67312 | 8 |
imports Lift |
15649 | 9 |
begin |
2640 | 10 |
|
62175 | 11 |
subsection \<open>Type definition and constructors\<close> |
16631 | 12 |
|
67312 | 13 |
type_synonym tr = "bool lift" |
2782 | 14 |
|
2766 | 15 |
translations |
67312 | 16 |
(type) "tr" \<leftharpoondown> (type) "bool lift" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
17 |
|
67312 | 18 |
definition TT :: "tr" |
19 |
where "TT = Def True" |
|
2640 | 20 |
|
67312 | 21 |
definition FF :: "tr" |
22 |
where "FF = Def False" |
|
2640 | 23 |
|
69597 | 24 |
text \<open>Exhaustion and Elimination for type \<^typ>\<open>tr\<close>\<close> |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
25 |
|
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
26 |
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" |
67312 | 27 |
by (induct t) (auto simp: FF_def TT_def) |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
28 |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
29 |
lemma trE [case_names bottom TT FF, cases type: tr]: |
35783 | 30 |
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
67312 | 31 |
by (induct p) (auto simp: FF_def TT_def) |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
32 |
|
48659
40a87b4dac19
declare trE and tr_induct as default cases and induct rules for type tr
huffman
parents:
42151
diff
changeset
|
33 |
lemma tr_induct [case_names bottom TT FF, induct type: tr]: |
67312 | 34 |
"P \<bottom> \<Longrightarrow> P TT \<Longrightarrow> P FF \<Longrightarrow> P x" |
35 |
by (cases x) simp_all |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
36 |
|
69597 | 37 |
text \<open>distinctness for type \<^typ>\<open>tr\<close>\<close> |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
38 |
|
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
|
39 |
lemma dist_below_tr [simp]: |
41182 | 40 |
"TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT" |
67312 | 41 |
by (simp_all add: TT_def FF_def) |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
42 |
|
67312 | 43 |
lemma dist_eq_tr [simp]: "TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT" |
44 |
by (simp_all add: TT_def FF_def) |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
45 |
|
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
|
46 |
lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT" |
67312 | 47 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
48 |
|
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
|
49 |
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF" |
67312 | 50 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
51 |
|
41182 | 52 |
lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF" |
67312 | 53 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
54 |
|
41182 | 55 |
lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT" |
67312 | 56 |
by (induct x) simp_all |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
57 |
|
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
58 |
|
62175 | 59 |
subsection \<open>Case analysis\<close> |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
60 |
|
36452 | 61 |
default_sort pcpo |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
62 |
|
67312 | 63 |
definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a" |
64 |
where "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
|
65 |
|
67312 | 66 |
abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(If (_)/ then (_)/ else (_))" [0, 0, 60] 60) |
67 |
where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b" |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
68 |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
69 |
translations |
67312 | 70 |
"\<Lambda> (XCONST TT). t" \<rightleftharpoons> "CONST tr_case\<cdot>t\<cdot>\<bottom>" |
71 |
"\<Lambda> (XCONST FF). t" \<rightleftharpoons> "CONST tr_case\<cdot>\<bottom>\<cdot>t" |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
72 |
|
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
73 |
lemma ifte_thms [simp]: |
40322
707eb30e8a53
make syntax of continuous if-then-else consistent with HOL if-then-else
huffman
parents:
36452
diff
changeset
|
74 |
"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
|
75 |
"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
|
76 |
"If TT then e1 else e2 = e1" |
67312 | 77 |
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
|
78 |
|
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
79 |
|
62175 | 80 |
subsection \<open>Boolean connectives\<close> |
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
81 |
|
67312 | 82 |
definition trand :: "tr \<rightarrow> tr \<rightarrow> tr" |
83 |
where andalso_def: "trand = (\<Lambda> x y. If x then y else FF)" |
|
84 |
||
85 |
abbreviation andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) |
|
86 |
where "x andalso y \<equiv> trand\<cdot>x\<cdot>y" |
|
87 |
||
88 |
definition tror :: "tr \<rightarrow> tr \<rightarrow> tr" |
|
89 |
where orelse_def: "tror = (\<Lambda> x y. If x then TT else y)" |
|
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
18081
diff
changeset
|
90 |
|
67312 | 91 |
abbreviation orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) |
92 |
where "x orelse y \<equiv> tror\<cdot>x\<cdot>y" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
93 |
|
67312 | 94 |
definition neg :: "tr \<rightarrow> tr" |
95 |
where "neg = flift2 Not" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
96 |
|
67312 | 97 |
definition If2 :: "tr \<Rightarrow> 'c \<Rightarrow> 'c \<Rightarrow> 'c" |
98 |
where "If2 Q x y = (If Q then x else y)" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
99 |
|
62175 | 100 |
text \<open>tactic for tr-thms with case split\<close> |
15649 | 101 |
|
40324 | 102 |
lemmas tr_defs = andalso_def orelse_def neg_def tr_case_def TT_def FF_def |
27148 | 103 |
|
62175 | 104 |
text \<open>lemmas about andalso, orelse, neg and if\<close> |
15649 | 105 |
|
106 |
lemma andalso_thms [simp]: |
|
107 |
"(TT andalso y) = y" |
|
108 |
"(FF andalso y) = FF" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
109 |
"(\<bottom> andalso y) = \<bottom>" |
15649 | 110 |
"(y andalso TT) = y" |
111 |
"(y andalso y) = y" |
|
67312 | 112 |
apply (unfold andalso_def, simp_all) |
113 |
apply (cases y, simp_all) |
|
114 |
apply (cases y, simp_all) |
|
115 |
done |
|
15649 | 116 |
|
117 |
lemma orelse_thms [simp]: |
|
118 |
"(TT orelse y) = TT" |
|
119 |
"(FF orelse y) = y" |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
120 |
"(\<bottom> orelse y) = \<bottom>" |
15649 | 121 |
"(y orelse FF) = y" |
122 |
"(y orelse y) = y" |
|
67312 | 123 |
apply (unfold orelse_def, simp_all) |
124 |
apply (cases y, simp_all) |
|
125 |
apply (cases y, simp_all) |
|
126 |
done |
|
15649 | 127 |
|
128 |
lemma neg_thms [simp]: |
|
18070
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
129 |
"neg\<cdot>TT = FF" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
130 |
"neg\<cdot>FF = TT" |
b653e18f0a41
cleaned up; removed adm_tricks in favor of compactness theorems
huffman
parents:
16756
diff
changeset
|
131 |
"neg\<cdot>\<bottom> = \<bottom>" |
67312 | 132 |
by (simp_all add: neg_def TT_def FF_def) |
15649 | 133 |
|
62175 | 134 |
text \<open>split-tac for If via If2 because the constant has to be a constant\<close> |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
25131
diff
changeset
|
135 |
|
67312 | 136 |
lemma split_If2: "P (If2 Q x y) \<longleftrightarrow> ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" |
137 |
by (cases Q) (simp_all add: If2_def) |
|
15649 | 138 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
139 |
(* FIXME unused!? *) |
62175 | 140 |
ML \<open> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
141 |
fun split_If_tac ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48659
diff
changeset
|
142 |
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
|
143 |
THEN' (split_tac ctxt [@{thm split_If2}]) |
62175 | 144 |
\<close> |
15649 | 145 |
|
146 |
subsection "Rewriting of HOLCF operations to HOL functions" |
|
147 |
||
67312 | 148 |
lemma andalso_or: "t \<noteq> \<bottom> \<Longrightarrow> (t andalso s) = FF \<longleftrightarrow> t = FF \<or> s = FF" |
149 |
by (cases t) simp_all |
|
15649 | 150 |
|
67312 | 151 |
lemma andalso_and: "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) \<noteq> FF) \<longleftrightarrow> t \<noteq> FF \<and> s \<noteq> FF" |
152 |
by (cases t) simp_all |
|
15649 | 153 |
|
67312 | 154 |
lemma Def_bool1 [simp]: "Def x \<noteq> FF \<longleftrightarrow> x" |
155 |
by (simp add: FF_def) |
|
15649 | 156 |
|
67312 | 157 |
lemma Def_bool2 [simp]: "Def x = FF \<longleftrightarrow> \<not> x" |
158 |
by (simp add: FF_def) |
|
15649 | 159 |
|
67312 | 160 |
lemma Def_bool3 [simp]: "Def x = TT \<longleftrightarrow> x" |
161 |
by (simp add: TT_def) |
|
15649 | 162 |
|
67312 | 163 |
lemma Def_bool4 [simp]: "Def x \<noteq> TT \<longleftrightarrow> \<not> x" |
164 |
by (simp add: TT_def) |
|
15649 | 165 |
|
67312 | 166 |
lemma If_and_if: "(If Def P then A else B) = (if P then A else B)" |
167 |
by (cases "Def P") (auto simp add: TT_def[symmetric] FF_def[symmetric]) |
|
168 |
||
15649 | 169 |
|
62175 | 170 |
subsection \<open>Compactness\<close> |
15649 | 171 |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
172 |
lemma compact_TT: "compact TT" |
67312 | 173 |
by (rule compact_chfin) |
15649 | 174 |
|
27294
c11e716fafeb
added some lemmas; reorganized into sections; tuned proofs
huffman
parents:
27148
diff
changeset
|
175 |
lemma compact_FF: "compact FF" |
67312 | 176 |
by (rule compact_chfin) |
2640 | 177 |
|
178 |
end |