src/HOL/Metis_Examples/Clausify.thy
changeset 42342 6babd86a54a4
parent 42340 4e4f0665e5be
child 42343 118cc349de35
     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:05 2011 +0200
     1.3 @@ -8,15 +8,6 @@
     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  (* FIXME: shouldn't need this *)
    1.19 @@ -52,7 +43,7 @@
    1.20  
    1.21  lemma
    1.22    fixes x :: real
    1.23 -  assumes fn_le: "!!n. f n \<le> x" and 1: "f----> lim f"
    1.24 +  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
    1.25    shows "lim f \<le> x"
    1.26  by (metis 1 LIMSEQ_le_const2 fn_le)
    1.27  
    1.28 @@ -71,7 +62,13 @@
    1.29  
    1.30  lemma
    1.31    "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    1.32 -   (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.33 +   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.34  by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
    1.35  
    1.36 +lemma ex_tl: "EX ys. tl ys = xs"
    1.37 +using tl.simps(2) by fast
    1.38 +
    1.39 +lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
    1.40 +by (metis ex_tl)
    1.41 +
    1.42  end