src/HOL/Metis_Examples/Clausify.thy
 author blanchet Thu Apr 14 11:24:05 2011 +0200 (2011-04-14) changeset 42343 118cc349de35 parent 42342 6babd86a54a4 child 42345 5ecd55993606 permissions -rw-r--r--
compile
1 (*  Title:      HOL/Metis_Examples/Clausify.thy
2     Author:     Jasmin Blanchette, TU Muenchen
4 Testing Metis's clausifier.
5 *)
7 theory Clausify
8 imports Complex_Main
9 begin
11 text {* Definitional CNF for goal *}
13 (* FIXME: shouldn't need this *)
14 declare [[unify_search_bound = 100]]
15 declare [[unify_trace_bound = 100]]
17 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
18 pax: "\<exists>b. \<forall>a. ((p b a \<and> p 0 0 \<and> p 1 a) \<or> (p 0 1 \<and> p 1 0 \<and> p a b))"
20 declare [[metis_new_skolemizer = false]]
22 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
23                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
24 by (metis pax)
26 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
27                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
28 by (metisFT pax)
30 declare [[metis_new_skolemizer]]
32 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
33                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
34 by (metis pax)
36 lemma "\<exists>b. \<forall>a. \<exists>x. (p b a \<or> x) \<and> (p 0 0 \<or> x) \<and> (p 1 a \<or> x) \<and>
37                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
38 by (metisFT pax)
40 text {* New Skolemizer *}
42 declare [[metis_new_skolemizer]]
44 lemma
45   fixes x :: real
46   assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
47   shows "lim f \<le> x"
48 by (metis 1 LIMSEQ_le_const2 fn_le)
50 definition
51   bounded :: "'a::metric_space set \<Rightarrow> bool" where
52   "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
54 lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
55 by (metis bounded_def subset_eq)
57 lemma
58   assumes a: "Quotient R Abs Rep"
59   shows "symp R"
60 using a unfolding Quotient_def using sympI
61 by metisFT
63 lemma
64   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
65    (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
66 by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
68 lemma ex_tl: "EX ys. tl ys = xs"
69 using tl.simps(2) by fast
71 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
72 by (metis ex_tl)
74 end