src/HOL/Metis_Examples/Clausify.thy
changeset 42350 128dc0fa87fc
parent 42345 5ecd55993606
child 42747 f132d13fcf75
     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 @@ -71,6 +71,18 @@
     1.4  lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
     1.5  by (metisFT rax)
     1.6  
     1.7 +lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
     1.8 +       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
     1.9 +       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    1.10 +       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    1.11 +by (metis rax)
    1.12 +
    1.13 +lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
    1.14 +       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    1.15 +       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    1.16 +       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    1.17 +by (metisFT rax)
    1.18 +
    1.19  text {* Definitional CNF for goal *}
    1.20  
    1.21  axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where