src/HOL/Metis_Examples/Clausify.thy
author blanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42747 f132d13fcf75
parent 42350 128dc0fa87fc
child 42756 6b7ef9b724fd
permissions -rw-r--r--
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
     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 sledgehammer_params [prover = e, blocking, timeout = 10]
    16 
    17 
    18 text {* Extensionality *}
    19 
    20 lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
    21 by simp
    22 
    23 definition inc :: "nat \<Rightarrow> nat" where
    24 "inc x = x + 1"
    25 
    26 lemma "inc \<noteq> (\<lambda>y. 0)"
    27 sledgehammer [expect = some] (inc_def plus_1_not_0)
    28 by (metis inc_def plus_1_not_0)
    29 
    30 lemma "inc = (\<lambda>y. y + 1)"
    31 sledgehammer [expect = some] (inc_def)
    32 by (metis inc_def)
    33 
    34 lemma "(\<lambda>y. y + 1) = inc"
    35 sledgehammer [expect = some] (inc_def)
    36 by (metis inc_def)
    37 
    38 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    39 "add_swap = (\<lambda>x y. y + x)"
    40 
    41 lemma "add_swap m n = n + m"
    42 sledgehammer [expect = some] (add_swap_def)
    43 by (metis add_swap_def)
    44 
    45 
    46 text {* Definitional CNF for facts *}
    47 
    48 declare [[meson_max_clauses = 10]]
    49 
    50 axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    51 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)"
    52 
    53 declare [[metis_new_skolemizer = false]]
    54 
    55 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    56 by (metis qax)
    57 
    58 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    59 by (metisFT qax)
    60 
    61 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)"
    62 by (metis qax)
    63 
    64 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)"
    65 by (metisFT qax)
    66 
    67 declare [[metis_new_skolemizer]]
    68 
    69 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    70 by (metis qax)
    71 
    72 lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
    73 by (metisFT qax)
    74 
    75 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)"
    76 by (metis qax)
    77 
    78 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)"
    79 by (metisFT qax)
    80 
    81 declare [[meson_max_clauses = 60]]
    82 
    83 axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
    84 rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
    85       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
    86       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
    87       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
    88 
    89 declare [[metis_new_skolemizer = false]]
    90 
    91 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    92 by (metis rax)
    93 
    94 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
    95 by (metisFT rax)
    96 
    97 declare [[metis_new_skolemizer]]
    98 
    99 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
   100 by (metis rax)
   101 
   102 lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
   103 by (metisFT rax)
   104 
   105 lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
   106        (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
   107        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
   108        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
   109 by (metis rax)
   110 
   111 lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
   112        (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
   113        (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
   114        (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
   115 by (metisFT rax)
   116 
   117 
   118 text {* Definitional CNF for goal *}
   119 
   120 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   121 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)"
   122 
   123 declare [[metis_new_skolemizer = false]]
   124 
   125 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>
   126                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
   127 by (metis pax)
   128 
   129 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>
   130                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
   131 by (metisFT pax)
   132 
   133 declare [[metis_new_skolemizer]]
   134 
   135 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>
   136                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
   137 by (metis pax)
   138 
   139 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>
   140                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
   141 by (metisFT pax)
   142 
   143 
   144 text {* New Skolemizer *}
   145 
   146 declare [[metis_new_skolemizer]]
   147 
   148 lemma
   149   fixes x :: real
   150   assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
   151   shows "lim f \<le> x"
   152 by (metis 1 LIMSEQ_le_const2 fn_le)
   153 
   154 definition
   155   bounded :: "'a::metric_space set \<Rightarrow> bool" where
   156   "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
   157 
   158 lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
   159 by (metis bounded_def subset_eq)
   160 
   161 lemma
   162   assumes a: "Quotient R Abs Rep"
   163   shows "symp R"
   164 using a unfolding Quotient_def using sympI
   165 by metisFT
   166 
   167 lemma
   168   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   169    (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
   170 by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
   171 
   172 lemma ex_tl: "EX ys. tl ys = xs"
   173 using tl.simps(2) by fast
   174 
   175 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
   176 by (metis ex_tl)
   177 
   178 end