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