src/HOL/Metis_Examples/Clausify.thy
 changeset 42345 5ecd55993606 parent 42343 118cc349de35 child 42350 128dc0fa87fc
```     1.1 --- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
1.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:05 2011 +0200
1.3 @@ -8,14 +8,73 @@
1.4  imports Complex_Main
1.5  begin
1.6
1.7 -text {* Definitional CNF for goal *}
1.8 -
1.9  (* FIXME: shouldn't need this *)
1.10  declare [[unify_search_bound = 100]]
1.11  declare [[unify_trace_bound = 100]]
1.12
1.13 +text {* Definitional CNF for facts *}
1.14 +
1.15 +declare [[meson_max_clauses = 10]]
1.16 +
1.17 +axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.18 +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)"
1.19 +
1.20 +declare [[metis_new_skolemizer = false]]
1.21 +
1.22 +lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.23 +by (metis qax)
1.24 +
1.25 +lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.26 +by (metisFT qax)
1.27 +
1.28 +lemma "\<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)"
1.29 +by (metis qax)
1.30 +
1.31 +lemma "\<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)"
1.32 +by (metisFT qax)
1.33 +
1.34 +declare [[metis_new_skolemizer]]
1.35 +
1.36 +lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.37 +by (metis qax)
1.38 +
1.39 +lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
1.40 +by (metisFT qax)
1.41 +
1.42 +lemma "\<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)"
1.43 +by (metis qax)
1.44 +
1.45 +lemma "\<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)"
1.46 +by (metisFT qax)
1.47 +
1.48 +declare [[meson_max_clauses = 60]]
1.49 +
1.50 +axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.51 +rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
1.52 +      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
1.53 +      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
1.54 +      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
1.55 +
1.56 +declare [[metis_new_skolemizer = false]]
1.57 +
1.58 +lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.59 +by (metis rax)
1.60 +
1.61 +lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.62 +by (metisFT rax)
1.63 +
1.64 +declare [[metis_new_skolemizer]]
1.65 +
1.66 +lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.67 +by (metis rax)
1.68 +
1.69 +lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
1.70 +by (metisFT rax)
1.71 +
1.72 +text {* Definitional CNF for goal *}
1.73 +
1.74  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
1.75 -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))"
1.76 +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)"
1.77
1.78  declare [[metis_new_skolemizer = false]]
1.79
```