21 |
21 |
22 lemma "(a | b) & ~a \<Longrightarrow> b" |
22 lemma "(a | b) & ~a \<Longrightarrow> b" |
23 by sat |
23 by sat |
24 |
24 |
25 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)" |
25 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)" |
|
26 (* |
26 apply (tactic {* cnf.cnf_rewrite_tac 1 *}) |
27 apply (tactic {* cnf.cnf_rewrite_tac 1 *}) |
|
28 *) |
27 by sat |
29 by sat |
28 |
30 |
29 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)" |
31 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)" |
|
32 (* |
30 apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) |
33 apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) |
31 apply (erule exE | erule conjE)+ |
34 apply (erule exE | erule conjE)+ |
|
35 *) |
32 by satx |
36 by satx |
33 |
37 |
34 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow> |
38 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow> |
35 (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" |
39 (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" |
|
40 (* |
36 apply (tactic {* cnf.cnf_rewrite_tac 1 *}) |
41 apply (tactic {* cnf.cnf_rewrite_tac 1 *}) |
|
42 *) |
37 by sat |
43 by sat |
38 |
44 |
39 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow> |
45 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \<Longrightarrow> |
40 (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" |
46 (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" |
|
47 (* |
41 apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) |
48 apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) |
42 apply (erule exE | erule conjE)+ |
49 apply (erule exE | erule conjE)+ |
|
50 *) |
43 by satx |
51 by satx |
44 |
52 |
45 lemma "P=P=P=P=P=P=P=P=P=P" |
53 lemma "P=P=P=P=P=P=P=P=P=P" |
46 by sat |
54 by sat |
47 |
55 |