src/HOL/Metis_Examples/Clausify.thy
changeset 42338 802f2fe7a0c9
child 42340 4e4f0665e5be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Metis_Examples/Clausify.thy	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -0,0 +1,70 @@
     1.4 +(*  Title:      HOL/Metis_Examples/Clausifier.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +
     1.7 +Testing Metis's clausifier.
     1.8 +*)
     1.9 +
    1.10 +theory Clausifier
    1.11 +imports Complex_Main
    1.12 +begin
    1.13 +
    1.14 +
    1.15 +text {* Definitional CNF for goal *}
    1.16 +
    1.17 +(* FIXME: shouldn't need this *)
    1.18 +declare [[unify_search_bound = 100]]
    1.19 +declare [[unify_trace_bound = 100]]
    1.20 +
    1.21 +axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    1.22 +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))"
    1.23 +
    1.24 +declare [[metis_new_skolemizer = false]]
    1.25 +
    1.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>
    1.27 +                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.28 +by (metis pax)
    1.29 +
    1.30 +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>
    1.31 +                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.32 +by (metisFT pax)
    1.33 +
    1.34 +declare [[metis_new_skolemizer]]
    1.35 +
    1.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>
    1.37 +                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.38 +by (metis pax)
    1.39 +
    1.40 +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>
    1.41 +                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    1.42 +by (metisFT pax)
    1.43 +
    1.44 +
    1.45 +text {* New Skolemizer *}
    1.46 +
    1.47 +declare [[metis_new_skolemizer]]
    1.48 +
    1.49 +lemma
    1.50 +  fixes x :: real
    1.51 +  assumes fn_le: "!!n. f n \<le> x" and 1: "f----> lim f"
    1.52 +  shows "lim f \<le> x"
    1.53 +by (metis 1 LIMSEQ_le_const2 fn_le)
    1.54 +
    1.55 +definition
    1.56 +  bounded :: "'a::metric_space set \<Rightarrow> bool" where
    1.57 +  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
    1.58 +
    1.59 +lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
    1.60 +by (metis bounded_def subset_eq)
    1.61 +
    1.62 +lemma
    1.63 +  assumes a: "Quotient R Abs Rep"
    1.64 +  shows "symp R"
    1.65 +using a unfolding Quotient_def using sympI
    1.66 +by metisFT
    1.67 +
    1.68 +lemma
    1.69 +  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    1.70 +   (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    1.71 +by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
    1.72 +
    1.73 +end