src/HOL/Metis_Examples/Clausify.thy
author blanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42345 5ecd55993606
parent 42343 118cc349de35
child 42350 128dc0fa87fc
permissions -rw-r--r--
added examples of definitional CNF facts
     1 (*  Title:      HOL/Metis_Examples/Clausify.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3 
     4 Testing Metis's clausifier.
     5 *)
     6 
     7 theory Clausify
     8 imports Complex_Main
     9 begin
    10 
    11 (* FIXME: shouldn't need this *)
    12 declare [[unify_search_bound = 100]]
    13 declare [[unify_trace_bound = 100]]
    14 
    15 text {* Definitional CNF for facts *}
    16 
    17 declare [[meson_max_clauses = 10]]
    18 
    19 axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    20 qax: "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    21 
    22 declare [[metis_new_skolemizer = false]]
    23 
    24 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    25 by (metis qax)
    26 
    27 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    28 by (metisFT qax)
    29 
    30 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    31 by (metis qax)
    32 
    33 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    34 by (metisFT qax)
    35 
    36 declare [[metis_new_skolemizer]]
    37 
    38 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    39 by (metis qax)
    40 
    41 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    42 by (metisFT qax)
    43 
    44 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    45 by (metis qax)
    46 
    47 lemma "\<exists>b. \<forall>a. (q b a \<and> q 0 0 \<and> q 1 a \<and> q a 1) \<or> (q 0 1 \<and> q 1 0 \<and> q a b \<and> q 1 1)"
    48 by (metisFT qax)
    49 
    50 declare [[meson_max_clauses = 60]]
    51 
    52 axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    53 rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
    54       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    55       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    56       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    57 
    58 declare [[metis_new_skolemizer = false]]
    59 
    60 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    61 by (metis rax)
    62 
    63 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    64 by (metisFT rax)
    65 
    66 declare [[metis_new_skolemizer]]
    67 
    68 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    69 by (metis rax)
    70 
    71 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    72 by (metisFT rax)
    73 
    74 text {* Definitional CNF for goal *}
    75 
    76 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    77 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)"
    78 
    79 declare [[metis_new_skolemizer = false]]
    80 
    81 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>
    82                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    83 by (metis pax)
    84 
    85 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>
    86                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    87 by (metisFT pax)
    88 
    89 declare [[metis_new_skolemizer]]
    90 
    91 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>
    92                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    93 by (metis pax)
    94 
    95 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>
    96                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
    97 by (metisFT pax)
    98 
    99 text {* New Skolemizer *}
   100 
   101 declare [[metis_new_skolemizer]]
   102 
   103 lemma
   104   fixes x :: real
   105   assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
   106   shows "lim f \<le> x"
   107 by (metis 1 LIMSEQ_le_const2 fn_le)
   108 
   109 definition
   110   bounded :: "'a::metric_space set \<Rightarrow> bool" where
   111   "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
   112 
   113 lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
   114 by (metis bounded_def subset_eq)
   115 
   116 lemma
   117   assumes a: "Quotient R Abs Rep"
   118   shows "symp R"
   119 using a unfolding Quotient_def using sympI
   120 by metisFT
   121 
   122 lemma
   123   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   124    (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
   125 by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
   126 
   127 lemma ex_tl: "EX ys. tl ys = xs"
   128 using tl.simps(2) by fast
   129 
   130 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
   131 by (metis ex_tl)
   132 
   133 end