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
```