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
```