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.
blanchet@42343
     1
(*  Title:      HOL/Metis_Examples/Clausify.thy
blanchet@42338
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42338
     3
blanchet@42338
     4
Testing Metis's clausifier.
blanchet@42338
     5
*)
blanchet@42338
     6
blanchet@42343
     7
theory Clausify
blanchet@42338
     8
imports Complex_Main
blanchet@42338
     9
begin
blanchet@42338
    10
blanchet@42338
    11
(* FIXME: shouldn't need this *)
blanchet@42338
    12
declare [[unify_search_bound = 100]]
blanchet@42338
    13
declare [[unify_trace_bound = 100]]
blanchet@42338
    14
blanchet@42747
    15
sledgehammer_params [prover = e, blocking, timeout = 10]
blanchet@42747
    16
blanchet@42747
    17
blanchet@42747
    18
text {* Extensionality *}
blanchet@42747
    19
blanchet@42747
    20
lemma plus_1_not_0: "n + (1\<Colon>nat) \<noteq> 0"
blanchet@42747
    21
by simp
blanchet@42747
    22
blanchet@42747
    23
definition inc :: "nat \<Rightarrow> nat" where
blanchet@42747
    24
"inc x = x + 1"
blanchet@42747
    25
blanchet@42747
    26
lemma "inc \<noteq> (\<lambda>y. 0)"
blanchet@42747
    27
sledgehammer [expect = some] (inc_def plus_1_not_0)
blanchet@42747
    28
by (metis inc_def plus_1_not_0)
blanchet@42747
    29
blanchet@42747
    30
lemma "inc = (\<lambda>y. y + 1)"
blanchet@42747
    31
sledgehammer [expect = some] (inc_def)
blanchet@42747
    32
by (metis inc_def)
blanchet@42747
    33
blanchet@42747
    34
lemma "(\<lambda>y. y + 1) = inc"
blanchet@42747
    35
sledgehammer [expect = some] (inc_def)
blanchet@42747
    36
by (metis inc_def)
blanchet@42747
    37
blanchet@42747
    38
definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
blanchet@42747
    39
"add_swap = (\<lambda>x y. y + x)"
blanchet@42747
    40
blanchet@42747
    41
lemma "add_swap m n = n + m"
blanchet@42747
    42
sledgehammer [expect = some] (add_swap_def)
blanchet@42747
    43
by (metis add_swap_def)
blanchet@42747
    44
blanchet@42747
    45
blanchet@42345
    46
text {* Definitional CNF for facts *}
blanchet@42345
    47
blanchet@42345
    48
declare [[meson_max_clauses = 10]]
blanchet@42345
    49
blanchet@42345
    50
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    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)"
blanchet@42345
    52
blanchet@42345
    53
declare [[metis_new_skolemizer = false]]
blanchet@42345
    54
blanchet@42345
    55
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    56
by (metis qax)
blanchet@42345
    57
blanchet@42345
    58
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    59
by (metisFT qax)
blanchet@42345
    60
blanchet@42345
    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)"
blanchet@42345
    62
by (metis qax)
blanchet@42345
    63
blanchet@42345
    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)"
blanchet@42345
    65
by (metisFT qax)
blanchet@42345
    66
blanchet@42345
    67
declare [[metis_new_skolemizer]]
blanchet@42345
    68
blanchet@42345
    69
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    70
by (metis qax)
blanchet@42345
    71
blanchet@42345
    72
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    73
by (metisFT qax)
blanchet@42345
    74
blanchet@42345
    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)"
blanchet@42345
    76
by (metis qax)
blanchet@42345
    77
blanchet@42345
    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)"
blanchet@42345
    79
by (metisFT qax)
blanchet@42345
    80
blanchet@42345
    81
declare [[meson_max_clauses = 60]]
blanchet@42345
    82
blanchet@42345
    83
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    84
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42345
    85
      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42345
    86
      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42345
    87
      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42345
    88
blanchet@42345
    89
declare [[metis_new_skolemizer = false]]
blanchet@42345
    90
blanchet@42345
    91
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    92
by (metis rax)
blanchet@42345
    93
blanchet@42345
    94
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    95
by (metisFT rax)
blanchet@42345
    96
blanchet@42345
    97
declare [[metis_new_skolemizer]]
blanchet@42345
    98
blanchet@42345
    99
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
   100
by (metis rax)
blanchet@42345
   101
blanchet@42345
   102
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
   103
by (metisFT rax)
blanchet@42345
   104
blanchet@42350
   105
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
   106
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
   107
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
   108
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42350
   109
by (metis rax)
blanchet@42350
   110
blanchet@42350
   111
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
   112
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
   113
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
   114
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42350
   115
by (metisFT rax)
blanchet@42350
   116
blanchet@42747
   117
blanchet@42345
   118
text {* Definitional CNF for goal *}
blanchet@42345
   119
blanchet@42338
   120
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
   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)"
blanchet@42338
   122
blanchet@42338
   123
declare [[metis_new_skolemizer = false]]
blanchet@42338
   124
blanchet@42338
   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>
blanchet@42338
   126
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
   127
by (metis pax)
blanchet@42338
   128
blanchet@42338
   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>
blanchet@42338
   130
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
   131
by (metisFT pax)
blanchet@42338
   132
blanchet@42338
   133
declare [[metis_new_skolemizer]]
blanchet@42338
   134
blanchet@42338
   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>
blanchet@42338
   136
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
   137
by (metis pax)
blanchet@42338
   138
blanchet@42338
   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>
blanchet@42338
   140
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
   141
by (metisFT pax)
blanchet@42338
   142
blanchet@42747
   143
blanchet@42338
   144
text {* New Skolemizer *}
blanchet@42338
   145
blanchet@42338
   146
declare [[metis_new_skolemizer]]
blanchet@42338
   147
blanchet@42338
   148
lemma
blanchet@42338
   149
  fixes x :: real
blanchet@42342
   150
  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
blanchet@42338
   151
  shows "lim f \<le> x"
blanchet@42338
   152
by (metis 1 LIMSEQ_le_const2 fn_le)
blanchet@42338
   153
blanchet@42338
   154
definition
blanchet@42338
   155
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
blanchet@42338
   156
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
blanchet@42338
   157
blanchet@42338
   158
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
blanchet@42338
   159
by (metis bounded_def subset_eq)
blanchet@42338
   160
blanchet@42338
   161
lemma
blanchet@42338
   162
  assumes a: "Quotient R Abs Rep"
blanchet@42338
   163
  shows "symp R"
blanchet@42338
   164
using a unfolding Quotient_def using sympI
blanchet@42338
   165
by metisFT
blanchet@42338
   166
blanchet@42338
   167
lemma
blanchet@42338
   168
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
blanchet@42342
   169
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
blanchet@42338
   170
by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
blanchet@42338
   171
blanchet@42342
   172
lemma ex_tl: "EX ys. tl ys = xs"
blanchet@42342
   173
using tl.simps(2) by fast
blanchet@42342
   174
blanchet@42342
   175
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
blanchet@42342
   176
by (metis ex_tl)
blanchet@42342
   177
blanchet@42338
   178
end