author | huffman |
Thu, 26 May 2005 02:23:27 +0200 | |
changeset 16081 | 81a4b4a245b0 |
parent 16070 | 4a83dd540b88 |
child 16121 | a80aa66d2271 |
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 |
|
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 tr-thms 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 {* split-tac 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 |
||
135 |
ML_setup {* |
|
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 |
chain-finiteness, of which these lemmata are specific examples |
|
178 |
*} |
|
179 |
||
180 |
lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)" |
|
181 |
apply (rule_tac p = "x" in trE) |
|
182 |
apply (simp_all) |
|
183 |
done |
|
184 |
||
185 |
lemma adm_trick_2: "(x~=TT) = (x=FF|x=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 |