added outstanding issue to Metis example
authorblanchet
Thu Apr 14 11:24:04 2011 +0200 (2011-04-14)
changeset 423404e4f0665e5be
parent 42339 0e5d1e5e1177
child 42341 5a00af7f4978
added outstanding issue to Metis example
src/HOL/Metis_Examples/Clausify.thy
     1.1 --- a/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -8,6 +8,14 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 +text {* Outstanding issues *}
     1.8 +
     1.9 +lemma ex_tl: "EX ys. tl ys = xs"
    1.10 +using tl.simps(2) by fast
    1.11 +
    1.12 +lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
    1.13 +using [[metis_new_skolemizer = false]] (* FAILS with "= true" *)
    1.14 +by (metis ex_tl)
    1.15  
    1.16  text {* Definitional CNF for goal *}
    1.17  
    1.18 @@ -38,7 +46,6 @@
    1.19                     (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.20  by (metisFT pax)
    1.21  
    1.22 -
    1.23  text {* New Skolemizer *}
    1.24  
    1.25  declare [[metis_new_skolemizer]]