equal
deleted
inserted
replaced
118 by Auto_tac; |
118 by Auto_tac; |
119 by (res_inst_tac [("p","t")] trE 1); |
119 by (res_inst_tac [("p","t")] trE 1); |
120 by Auto_tac; |
120 by Auto_tac; |
121 qed"andalso_or"; |
121 qed"andalso_or"; |
122 |
122 |
123 Goal "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"; |
123 Goal "[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"; |
124 by (rtac iffI 1); |
124 by (rtac iffI 1); |
125 by (res_inst_tac [("p","t")] trE 1); |
125 by (res_inst_tac [("p","t")] trE 1); |
126 by Auto_tac; |
126 by Auto_tac; |
127 by (res_inst_tac [("p","t")] trE 1); |
127 by (res_inst_tac [("p","t")] trE 1); |
128 by Auto_tac; |
128 by Auto_tac; |
174 qed"adm_trick_2"; |
174 qed"adm_trick_2"; |
175 |
175 |
176 val adm_tricks = [adm_trick_1,adm_trick_2]; |
176 val adm_tricks = [adm_trick_1,adm_trick_2]; |
177 |
177 |
178 |
178 |
179 Goal "!!f. cont(f) ==> adm (%x. (f x)~=TT)"; |
179 Goal "cont(f) ==> adm (%x. (f x)~=TT)"; |
180 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1); |
180 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1); |
181 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1)); |
181 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1)); |
182 qed"adm_nTT"; |
182 qed"adm_nTT"; |
183 |
183 |
184 Goal "!!f. cont(f) ==> adm (%x. (f x)~=FF)"; |
184 Goal "cont(f) ==> adm (%x. (f x)~=FF)"; |
185 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1); |
185 by (simp_tac (HOL_basic_ss addsimps adm_tricks) 1); |
186 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1)); |
186 by (REPEAT ((resolve_tac (adm_lemmas@cont_lemmas1) 1) ORELSE atac 1)); |
187 qed"adm_nFF"; |
187 qed"adm_nFF"; |
188 |
188 |
189 Addsimps [adm_nTT,adm_nFF]; |
189 Addsimps [adm_nTT,adm_nFF]; |