equal
deleted
inserted
replaced
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 |
3 |
4 Example that exercises Metis's Clausifier. |
4 Example that exercises Metis's Clausifier. |
5 *) |
5 *) |
6 |
6 |
7 section {* Example that Exercises Metis's Clausifier *} |
7 section \<open>Example that Exercises Metis's Clausifier\<close> |
8 |
8 |
9 theory Clausification |
9 theory Clausification |
10 imports Complex_Main |
10 imports Complex_Main |
11 begin |
11 begin |
12 |
12 |
13 |
13 |
14 text {* Definitional CNF for facts *} |
14 text \<open>Definitional CNF for facts\<close> |
15 |
15 |
16 declare [[meson_max_clauses = 10]] |
16 declare [[meson_max_clauses = 10]] |
17 |
17 |
18 axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
18 axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
19 qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
19 qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)" |
81 (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> |
81 (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> |
82 (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" |
82 (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" |
83 by (metis (full_types) rax) |
83 by (metis (full_types) rax) |
84 |
84 |
85 |
85 |
86 text {* Definitional CNF for goal *} |
86 text \<open>Definitional CNF for goal\<close> |
87 |
87 |
88 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
88 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
89 pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)" |
89 pax: "\<exists>b. \<forall>a. (p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b)" |
90 |
90 |
91 declare [[metis_new_skolem = false]] |
91 declare [[metis_new_skolem = false]] |
107 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> |
107 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> |
108 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
108 (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
109 by (metis (full_types) pax) |
109 by (metis (full_types) pax) |
110 |
110 |
111 |
111 |
112 text {* New Skolemizer *} |
112 text \<open>New Skolemizer\<close> |
113 |
113 |
114 declare [[metis_new_skolem]] |
114 declare [[metis_new_skolem]] |
115 |
115 |
116 lemma |
116 lemma |
117 fixes x :: real |
117 fixes x :: real |