equal
deleted
inserted
replaced
113 |
113 |
114 goal thy |
114 goal thy |
115 "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"; |
115 "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)"; |
116 by (rtac iffI 1); |
116 by (rtac iffI 1); |
117 by (res_inst_tac [("p","t")] trE 1); |
117 by (res_inst_tac [("p","t")] trE 1); |
118 auto(); |
118 by (Auto_tac()); |
119 by (res_inst_tac [("p","t")] trE 1); |
119 by (res_inst_tac [("p","t")] trE 1); |
120 auto(); |
120 by (Auto_tac()); |
121 qed"andalso_or"; |
121 qed"andalso_or"; |
122 |
122 |
123 goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)"; |
123 goal thy "!!t.[|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 auto(); |
126 by (Auto_tac()); |
127 by (res_inst_tac [("p","t")] trE 1); |
127 by (res_inst_tac [("p","t")] trE 1); |
128 auto(); |
128 by (Auto_tac()); |
129 qed"andalso_and"; |
129 qed"andalso_and"; |
130 |
130 |
131 goal thy "(Def x ~=FF)= x"; |
131 goal thy "(Def x ~=FF)= x"; |
132 by (simp_tac (simpset() addsimps [FF_def]) 1); |
132 by (simp_tac (simpset() addsimps [FF_def]) 1); |
133 qed"Def_bool1"; |
133 qed"Def_bool1"; |