src/HOL/Metis_Examples/Clausify.thy
author blanchet
Thu Apr 14 11:24:04 2011 +0200 (2011-04-14)
changeset 42338 802f2fe7a0c9
child 42340 4e4f0665e5be
permissions -rw-r--r--
started clausifier examples
     1 (*  Title:      HOL/Metis_Examples/Clausifier.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Testing Metis's clausifier.
     5 *)
     6 
     7 theory Clausifier
     8 imports Complex_Main
     9 begin
    10 
    11 
    12 text {* Definitional CNF for goal *}
    13 
    14 (* FIXME: shouldn't need this *)
    15 declare [[unify_search_bound = 100]]
    16 declare [[unify_trace_bound = 100]]
    17 
    18 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    19 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 
    21 declare [[metis_new_skolemizer = false]]
    22 
    23 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>
    24                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    25 by (metis pax)
    26 
    27 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>
    28                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    29 by (metisFT pax)
    30 
    31 declare [[metis_new_skolemizer]]
    32 
    33 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>
    34                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    35 by (metis pax)
    36 
    37 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>
    38                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    39 by (metisFT pax)
    40 
    41 
    42 text {* New Skolemizer *}
    43 
    44 declare [[metis_new_skolemizer]]
    45 
    46 lemma
    47   fixes x :: real
    48   assumes fn_le: "!!n. f n \<le> x" and 1: "f----> lim f"
    49   shows "lim f \<le> x"
    50 by (metis 1 LIMSEQ_le_const2 fn_le)
    51 
    52 definition
    53   bounded :: "'a::metric_space set \<Rightarrow> bool" where
    54   "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
    55 
    56 lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
    57 by (metis bounded_def subset_eq)
    58 
    59 lemma
    60   assumes a: "Quotient R Abs Rep"
    61   shows "symp R"
    62 using a unfolding Quotient_def using sympI
    63 by metisFT
    64 
    65 lemma
    66   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    67    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
    68 by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
    69 
    70 end