15 |
15 |
16 types |
16 types |
17 tr = "bool lift" |
17 tr = "bool lift" |
18 |
18 |
19 translations |
19 translations |
20 "tr" <= (type) "bool lift" |
20 "tr" <= (type) "bool lift" |
21 |
21 |
22 consts |
22 definition |
23 TT :: "tr" |
23 TT :: "tr" where |
24 FF :: "tr" |
24 "TT = Def True" |
25 trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" |
|
26 trand :: "tr \<rightarrow> tr \<rightarrow> tr" |
|
27 tror :: "tr \<rightarrow> tr \<rightarrow> tr" |
|
28 neg :: "tr \<rightarrow> tr" |
|
29 If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" |
|
30 |
25 |
|
26 definition |
|
27 FF :: "tr" where |
|
28 "FF = Def False" |
|
29 |
|
30 definition |
|
31 trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where |
|
32 ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)" |
31 abbreviation |
33 abbreviation |
32 cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where |
34 cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where |
33 "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b" |
35 "If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b" |
34 |
36 |
|
37 definition |
|
38 trand :: "tr \<rightarrow> tr \<rightarrow> tr" where |
|
39 andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)" |
35 abbreviation |
40 abbreviation |
36 andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where |
41 andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where |
37 "x andalso y == trand\<cdot>x\<cdot>y" |
42 "x andalso y == trand\<cdot>x\<cdot>y" |
38 |
43 |
|
44 definition |
|
45 tror :: "tr \<rightarrow> tr \<rightarrow> tr" where |
|
46 orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)" |
39 abbreviation |
47 abbreviation |
40 orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where |
48 orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where |
41 "x orelse y == tror\<cdot>x\<cdot>y" |
49 "x orelse y == tror\<cdot>x\<cdot>y" |
42 |
50 |
|
51 definition |
|
52 neg :: "tr \<rightarrow> tr" where |
|
53 "neg = flift2 Not" |
|
54 |
|
55 definition |
|
56 If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where |
|
57 "If2 Q x y = (If Q then x else y fi)" |
|
58 |
43 translations |
59 translations |
44 "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>" |
60 "\<Lambda> (CONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>" |
45 "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t" |
61 "\<Lambda> (CONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t" |
46 |
62 |
47 defs |
|
48 TT_def: "TT \<equiv> Def True" |
|
49 FF_def: "FF \<equiv> Def False" |
|
50 neg_def: "neg \<equiv> flift2 Not" |
|
51 ifte_def: "trifte \<equiv> \<Lambda> t e. FLIFT b. if b then t else e" |
|
52 andalso_def: "trand \<equiv> \<Lambda> x y. If x then y else FF fi" |
|
53 orelse_def: "tror \<equiv> \<Lambda> x y. If x then TT else y fi" |
|
54 If2_def: "If2 Q x y \<equiv> If Q then x else y fi" |
|
55 |
63 |
56 text {* Exhaustion and Elimination for type @{typ tr} *} |
64 text {* Exhaustion and Elimination for type @{typ tr} *} |
57 |
65 |
58 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" |
66 lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF" |
59 apply (unfold FF_def TT_def) |
67 apply (unfold FF_def TT_def) |
60 apply (induct_tac "t") |
68 apply (induct t) |
61 apply fast |
69 apply fast |
62 apply fast |
70 apply fast |
63 done |
71 done |
64 |
72 |
65 lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
73 lemma trE: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = TT \<Longrightarrow> Q; p = FF \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
76 (* |
84 (* |
77 fun prover t = prove_goal thy t |
85 fun prover t = prove_goal thy t |
78 (fn prems => |
86 (fn prems => |
79 [ |
87 [ |
80 (res_inst_tac [("p","y")] trE 1), |
88 (res_inst_tac [("p","y")] trE 1), |
81 (REPEAT(asm_simp_tac (simpset() addsimps |
89 (REPEAT(asm_simp_tac (simpset() addsimps |
82 [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) |
90 [o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1)) |
83 ]) |
91 ]) |
84 *) |
92 *) |
85 text {* distinctness for type @{typ tr} *} |
93 text {* distinctness for type @{typ tr} *} |
86 |
94 |
127 "neg\<cdot>FF = TT" |
135 "neg\<cdot>FF = TT" |
128 "neg\<cdot>\<bottom> = \<bottom>" |
136 "neg\<cdot>\<bottom> = \<bottom>" |
129 by (simp_all add: neg_def TT_def FF_def) |
137 by (simp_all add: neg_def TT_def FF_def) |
130 |
138 |
131 text {* split-tac for If via If2 because the constant has to be a constant *} |
139 text {* split-tac for If via If2 because the constant has to be a constant *} |
132 |
140 |
133 lemma split_If2: |
141 lemma split_If2: |
134 "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" |
142 "P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))" |
135 apply (unfold If2_def) |
143 apply (unfold If2_def) |
136 apply (rule_tac p = "Q" in trE) |
144 apply (rule_tac p = "Q" in trE) |
137 apply (simp_all) |
145 apply (simp_all) |
138 done |
146 done |
139 |
147 |
140 ML {* |
148 ML {* |
141 val split_If_tac = |
149 val split_If_tac = |
142 simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")]) |
150 simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym]) |
143 THEN' (split_tac [thm "split_If2"]) |
151 THEN' (split_tac [@{thm split_If2}]) |
144 *} |
152 *} |
145 |
153 |
146 subsection "Rewriting of HOLCF operations to HOL functions" |
154 subsection "Rewriting of HOLCF operations to HOL functions" |
147 |
155 |
148 lemma andalso_or: |
156 lemma andalso_or: |
149 "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" |
157 "t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)" |
150 apply (rule_tac p = "t" in trE) |
158 apply (rule_tac p = "t" in trE) |
151 apply simp_all |
159 apply simp_all |
152 done |
160 done |
153 |
161 |
167 by (simp add: TT_def) |
175 by (simp add: TT_def) |
168 |
176 |
169 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" |
177 lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)" |
170 by (simp add: TT_def) |
178 by (simp add: TT_def) |
171 |
179 |
172 lemma If_and_if: |
180 lemma If_and_if: |
173 "(If Def P then A else B fi) = (if P then A else B)" |
181 "(If Def P then A else B fi) = (if P then A else B)" |
174 apply (rule_tac p = "Def P" in trE) |
182 apply (rule_tac p = "Def P" in trE) |
175 apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) |
183 apply (auto simp add: TT_def[symmetric] FF_def[symmetric]) |
176 done |
184 done |
177 |
185 |