opentheory/compat/HOL4boolScript.sml

7 fun export (tm,tac) =
11 val res0 = export(``!t. F ==> t``,
16 val res = export(``~~p ==> p``,
20 val res2 = export(``~(p ==> q) ==> p``,
25 val res3 = export(``!x. x = (x = T)``,
29 val res = export(``~(p ==> q) ==> ~q``,
34 val res = export(``~(p \/ q) ==> ~p``,
39 val res = export(``~(p \/ q) ==> ~q``,
44 val res7 = export(``!A. A ==> ~A ==> F``,
50 val res8 = export(``!t1 t2. (t1 ==> t2) ==> (t2 ==> t1) ==> (t1 <=> t2)``,
58 val res9 = export(``!t. t ==> F <=> (t = F)``,
71 val res = export(``!x. (x = x) <=> T``,
80 val res = export(``!f x. literal_case f x = f x``,
89 val res = export(``!f x. LET f x = f x``,
98 val res13 = export(``!P rep. TYPE_DEFINITION P rep <=> ^(rhs(concl(SPEC_ALL boolTheory.TYPE_DEFINITION_THM)))``,
103 val res = export(``(~A ==> F) ==> (A ==> F) ==> F``,
110 val res = export(``!f g. (f = g) <=> !x. (f x = g x)``,
114 val res = export(``!t1 t2. ((if T then t1 else t2) = t1) /\ ((if F then t1 else t2) = t2)``,
118 val res = export(``(!t. ~~t <=> t) /\ (~T <=> F) /\ (~F <=> T)``,
124 val res = export(``!t.
133 val res = export(``!t.
143 val res = export(``!t.
153 val res = export(``!t.
164 val res = export(``~(t /\ ~t)``,
170 val res = export(``!t. ~t ==> t ==> F``,
177 val res = export(``!t. (t ==> F) ==> ~t``,
182 val res = export(``!f b x y. f (if b then x else y) = if b then f x else f y``,
187 val res = export(``(!(t1:'a) t2. (if T then t1 else t2) = t1) /\
192 val res = export(``!A B. A ==> B <=> ~A \/ B``,
206 val res = export(``(x ==> y) /\ (z ==> w) ==> x /\ z ==> y /\ w``,
209 val res = export(``(x ==> y) /\ (z ==> w) ==> x \/ z ==> y \/ w``,
212 val res = export(``!t1 t2 t3. t1 /\ t2 /\ t3 <=> (t1 /\ t2) /\ t3``,
216 val res = export(``!A B C. A \/ B \/ C <=> (A \/ B) \/ C``,
220 val res = export(``!Q P. (!e. P e \/ Q) <=> (!x. P x) \/ Q``,
224 val res = export(``!t1 t2. (t1 <=> t2) <=> t1 /\ t2 \/ ~t1 /\ ~t2``,
238 val res = export(``!A B C. B /\ C \/ A <=> (B \/ A) /\ (C \/ A)``,
242 val res = export(``(?!x. P x) <=> ((?x. P x) /\ !x y. P x /\ P y ==> (x = y))``,
246 val res = export(``(!x. P x ==> Q x) ==> (?x. P x) ==> ?x. Q x``,
249 val res = export(``
262 val res = export(
276 val res = export(``!A B. (~(A /\ B) <=> ~A \/ ~B) /\ (~(A \/ B) <=> ~A /\ ~B)``,
285 val res = export(``!t1 t2. (t1 <=> t2) <=> (t1 ==> t2) /\ (t2 ==> t1)``,
294 val res = export(``
327 val res = export(``