equal
deleted
inserted
replaced
6 |
6 |
7 theory Clausifier |
7 theory Clausifier |
8 imports Complex_Main |
8 imports Complex_Main |
9 begin |
9 begin |
10 |
10 |
|
11 text {* Outstanding issues *} |
|
12 |
|
13 lemma ex_tl: "EX ys. tl ys = xs" |
|
14 using tl.simps(2) by fast |
|
15 |
|
16 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)" |
|
17 using [[metis_new_skolemizer = false]] (* FAILS with "= true" *) |
|
18 by (metis ex_tl) |
11 |
19 |
12 text {* Definitional CNF for goal *} |
20 text {* Definitional CNF for goal *} |
13 |
21 |
14 (* FIXME: shouldn't need this *) |
22 (* FIXME: shouldn't need this *) |
15 declare [[unify_search_bound = 100]] |
23 declare [[unify_search_bound = 100]] |
36 |
44 |
37 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and> |
45 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and> |
38 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
46 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
39 by (metisFT pax) |
47 by (metisFT pax) |
40 |
48 |
41 |
|
42 text {* New Skolemizer *} |
49 text {* New Skolemizer *} |
43 |
50 |
44 declare [[metis_new_skolemizer]] |
51 declare [[metis_new_skolemizer]] |
45 |
52 |
46 lemma |
53 lemma |