2640
|
1 |
(* Title: HOLCF/Tr.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Franz Regensburger
|
15649
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
2640
|
5 |
|
|
6 |
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
|
|
7 |
*)
|
|
8 |
|
15649
|
9 |
header {* The type of lifted booleans *}
|
|
10 |
|
|
11 |
theory Tr
|
|
12 |
imports Lift Fix
|
|
13 |
begin
|
2640
|
14 |
|
2782
|
15 |
types
|
|
16 |
tr = "bool lift"
|
|
17 |
|
2766
|
18 |
translations
|
2782
|
19 |
"tr" <= (type) "bool lift"
|
2640
|
20 |
|
|
21 |
consts
|
15649
|
22 |
TT :: "tr"
|
|
23 |
FF :: "tr"
|
2640
|
24 |
Icifte :: "tr -> 'c -> 'c -> 'c"
|
|
25 |
trand :: "tr -> tr -> tr"
|
|
26 |
tror :: "tr -> tr -> tr"
|
|
27 |
neg :: "tr -> tr"
|
3036
|
28 |
If2 :: "tr=>'c=>'c=>'c"
|
2640
|
29 |
|
|
30 |
syntax "@cifte" :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
|
|
31 |
"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
|
|
32 |
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
|
|
33 |
|
|
34 |
translations
|
10834
|
35 |
"x andalso y" == "trand$x$y"
|
|
36 |
"x orelse y" == "tror$x$y"
|
|
37 |
"If b then e1 else e2 fi" == "Icifte$b$e1$e2"
|
2640
|
38 |
defs
|
15649
|
39 |
TT_def: "TT==Def True"
|
|
40 |
FF_def: "FF==Def False"
|
|
41 |
neg_def: "neg == flift2 Not"
|
|
42 |
ifte_def: "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
|
|
43 |
andalso_def: "trand == (LAM x y. If x then y else FF fi)"
|
|
44 |
orelse_def: "tror == (LAM x y. If x then TT else y fi)"
|
|
45 |
If2_def: "If2 Q x y == If Q then x else y fi"
|
|
46 |
|
|
47 |
text {* Exhaustion and Elimination for type @{typ tr} *}
|
|
48 |
|
|
49 |
lemma Exh_tr: "t=UU | t = TT | t = FF"
|
|
50 |
apply (unfold FF_def TT_def)
|
|
51 |
apply (induct_tac "t")
|
|
52 |
apply fast
|
|
53 |
apply fast
|
|
54 |
done
|
|
55 |
|
|
56 |
lemma trE: "[| p=UU ==> Q; p = TT ==>Q; p = FF ==>Q|] ==>Q"
|
|
57 |
apply (rule Exh_tr [THEN disjE])
|
|
58 |
apply fast
|
|
59 |
apply (erule disjE)
|
|
60 |
apply fast
|
|
61 |
apply fast
|
|
62 |
done
|
|
63 |
|
|
64 |
text {* tactic for tr-thms with case split *}
|
|
65 |
|
|
66 |
lemmas tr_defs = andalso_def orelse_def neg_def ifte_def TT_def FF_def
|
|
67 |
(*
|
|
68 |
fun prover t = prove_goal thy t
|
|
69 |
(fn prems =>
|
|
70 |
[
|
|
71 |
(res_inst_tac [("p","y")] trE 1),
|
|
72 |
(REPEAT(asm_simp_tac (simpset() addsimps
|
|
73 |
[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
|
|
74 |
])
|
|
75 |
*)
|
|
76 |
text {* distinctness for type @{typ tr} *}
|
|
77 |
|
|
78 |
lemma dist_less_tr [simp]: "~TT << UU" "~FF << UU" "~TT << FF" "~FF << TT"
|
|
79 |
by (simp_all add: tr_defs)
|
|
80 |
|
|
81 |
lemma dist_eq_tr [simp]: "TT~=UU" "FF~=UU" "TT~=FF" "UU~=TT" "UU~=FF" "FF~=TT"
|
|
82 |
by (simp_all add: tr_defs)
|
|
83 |
|
|
84 |
text {* lemmas about andalso, orelse, neg and if *}
|
|
85 |
|
|
86 |
lemma ifte_simp:
|
|
87 |
"If x then e1 else e2 fi =
|
|
88 |
flift1 (%b. if b then e1 else e2)$x"
|
|
89 |
apply (unfold ifte_def TT_def FF_def flift1_def)
|
|
90 |
apply (simp add: cont_flift1_arg cont_if)
|
|
91 |
done
|
|
92 |
|
|
93 |
lemma ifte_thms [simp]:
|
|
94 |
"If UU then e1 else e2 fi = UU"
|
|
95 |
"If FF then e1 else e2 fi = e2"
|
|
96 |
"If TT then e1 else e2 fi = e1"
|
|
97 |
by (simp_all add: ifte_simp TT_def FF_def)
|
|
98 |
|
|
99 |
lemma andalso_thms [simp]:
|
|
100 |
"(TT andalso y) = y"
|
|
101 |
"(FF andalso y) = FF"
|
|
102 |
"(UU andalso y) = UU"
|
|
103 |
"(y andalso TT) = y"
|
|
104 |
"(y andalso y) = y"
|
|
105 |
apply (unfold andalso_def, simp_all)
|
|
106 |
apply (rule_tac p=y in trE, simp_all)
|
|
107 |
apply (rule_tac p=y in trE, simp_all)
|
|
108 |
done
|
|
109 |
|
|
110 |
lemma orelse_thms [simp]:
|
|
111 |
"(TT orelse y) = TT"
|
|
112 |
"(FF orelse y) = y"
|
|
113 |
"(UU orelse y) = UU"
|
|
114 |
"(y orelse FF) = y"
|
|
115 |
"(y orelse y) = y"
|
|
116 |
apply (unfold orelse_def, simp_all)
|
|
117 |
apply (rule_tac p=y in trE, simp_all)
|
|
118 |
apply (rule_tac p=y in trE, simp_all)
|
|
119 |
done
|
|
120 |
|
|
121 |
lemma neg_thms [simp]:
|
|
122 |
"neg$TT = FF"
|
|
123 |
"neg$FF = TT"
|
|
124 |
"neg$UU = UU"
|
|
125 |
by (simp_all add: neg_def TT_def FF_def)
|
|
126 |
|
|
127 |
text {* split-tac for If via If2 because the constant has to be a constant *}
|
|
128 |
|
|
129 |
lemma split_If2:
|
|
130 |
"P (If2 Q x y ) = ((Q=UU --> P UU) & (Q=TT --> P x) & (Q=FF --> P y))"
|
|
131 |
apply (unfold If2_def)
|
|
132 |
apply (rule_tac p = "Q" in trE)
|
|
133 |
apply (simp_all)
|
|
134 |
done
|
|
135 |
|
|
136 |
ML_setup {*
|
|
137 |
val split_If_tac =
|
|
138 |
simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
|
|
139 |
THEN' (split_tac [thm "split_If2"])
|
|
140 |
*}
|
|
141 |
|
|
142 |
subsection "Rewriting of HOLCF operations to HOL functions"
|
|
143 |
|
|
144 |
lemma andalso_or:
|
|
145 |
"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"
|
|
146 |
apply (rule_tac p = "t" in trE)
|
|
147 |
apply simp_all
|
|
148 |
done
|
|
149 |
|
|
150 |
lemma andalso_and: "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"
|
|
151 |
apply (rule_tac p = "t" in trE)
|
|
152 |
apply simp_all
|
|
153 |
done
|
|
154 |
|
|
155 |
lemma Def_bool1 [simp]: "(Def x ~= FF) = x"
|
|
156 |
by (simp add: FF_def)
|
|
157 |
|
|
158 |
lemma Def_bool2 [simp]: "(Def x = FF) = (~x)"
|
|
159 |
by (simp add: FF_def)
|
|
160 |
|
|
161 |
lemma Def_bool3 [simp]: "(Def x = TT) = x"
|
|
162 |
by (simp add: TT_def)
|
|
163 |
|
|
164 |
lemma Def_bool4 [simp]: "(Def x ~= TT) = (~x)"
|
|
165 |
by (simp add: TT_def)
|
|
166 |
|
|
167 |
lemma If_and_if:
|
|
168 |
"(If Def P then A else B fi)= (if P then A else B)"
|
|
169 |
apply (rule_tac p = "Def P" in trE)
|
|
170 |
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
|
|
171 |
done
|
|
172 |
|
|
173 |
subsection "admissibility"
|
|
174 |
|
|
175 |
text {*
|
|
176 |
The following rewrite rules for admissibility should in the future be
|
|
177 |
replaced by a more general admissibility test that also checks
|
|
178 |
chain-finiteness, of which these lemmata are specific examples
|
|
179 |
*}
|
|
180 |
|
|
181 |
lemma adm_trick_1: "(x~=FF) = (x=TT|x=UU)"
|
|
182 |
apply (rule_tac p = "x" in trE)
|
|
183 |
apply (simp_all)
|
|
184 |
done
|
|
185 |
|
|
186 |
lemma adm_trick_2: "(x~=TT) = (x=FF|x=UU)"
|
|
187 |
apply (rule_tac p = "x" in trE)
|
|
188 |
apply (simp_all)
|
|
189 |
done
|
|
190 |
|
|
191 |
lemmas adm_tricks = adm_trick_1 adm_trick_2
|
|
192 |
|
|
193 |
lemma adm_nTT [simp]: "cont(f) ==> adm (%x. (f x)~=TT)"
|
|
194 |
by (simp add: adm_tricks)
|
|
195 |
|
|
196 |
lemma adm_nFF [simp]: "cont(f) ==> adm (%x. (f x)~=FF)"
|
|
197 |
by (simp add: adm_tricks)
|
2640
|
198 |
|
|
199 |
end
|