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