src/HOL/Metis_Examples/Clausification.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63167 0909deb8059b
child 67613 ce654b0e6d69
permissions -rw-r--r--
executable domain membership checks
blanchet@43197
     1
(*  Title:      HOL/Metis_Examples/Clausification.thy
blanchet@42338
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42338
     3
blanchet@43197
     4
Example that exercises Metis's Clausifier.
blanchet@42338
     5
*)
blanchet@42338
     6
wenzelm@63167
     7
section \<open>Example that Exercises Metis's Clausifier\<close>
blanchet@43197
     8
blanchet@43197
     9
theory Clausification
blanchet@42338
    10
imports Complex_Main
blanchet@42338
    11
begin
blanchet@42338
    12
blanchet@42747
    13
wenzelm@63167
    14
text \<open>Definitional CNF for facts\<close>
blanchet@42345
    15
blanchet@42345
    16
declare [[meson_max_clauses = 10]]
blanchet@42345
    17
blanchet@42345
    18
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    19
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
    20
blanchet@50705
    21
declare [[metis_new_skolem = false]]
blanchet@42345
    22
blanchet@42345
    23
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    24
by (metis qax)
blanchet@42345
    25
blanchet@42345
    26
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@43228
    27
by (metis (full_types) qax)
blanchet@42345
    28
blanchet@42345
    29
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
    30
by (metis qax)
blanchet@42345
    31
blanchet@42345
    32
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@43228
    33
by (metis (full_types) qax)
blanchet@42345
    34
blanchet@50705
    35
declare [[metis_new_skolem]]
blanchet@42345
    36
blanchet@42345
    37
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    38
by (metis qax)
blanchet@42345
    39
blanchet@42345
    40
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@43228
    41
by (metis (full_types) qax)
blanchet@42345
    42
blanchet@42345
    43
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
    44
by (metis qax)
blanchet@42345
    45
blanchet@42345
    46
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@43228
    47
by (metis (full_types) qax)
blanchet@42345
    48
blanchet@42345
    49
declare [[meson_max_clauses = 60]]
blanchet@42345
    50
blanchet@42345
    51
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    52
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42345
    53
      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42345
    54
      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42345
    55
      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42345
    56
blanchet@50705
    57
declare [[metis_new_skolem = false]]
blanchet@42345
    58
blanchet@42345
    59
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    60
by (metis rax)
blanchet@42345
    61
blanchet@42345
    62
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@43228
    63
by (metis (full_types) rax)
blanchet@42345
    64
blanchet@50705
    65
declare [[metis_new_skolem]]
blanchet@42345
    66
blanchet@42345
    67
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    68
by (metis rax)
blanchet@42345
    69
blanchet@42345
    70
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@43228
    71
by (metis (full_types) rax)
blanchet@42345
    72
blanchet@42350
    73
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
    74
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
    75
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
    76
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42350
    77
by (metis rax)
blanchet@42350
    78
blanchet@42350
    79
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
    80
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
    81
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
    82
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@43228
    83
by (metis (full_types) rax)
blanchet@42350
    84
blanchet@42747
    85
wenzelm@63167
    86
text \<open>Definitional CNF for goal\<close>
blanchet@42345
    87
blanchet@42338
    88
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    89
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
    90
blanchet@50705
    91
declare [[metis_new_skolem = false]]
blanchet@42338
    92
blanchet@42338
    93
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
    94
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    95
by (metis pax)
blanchet@42338
    96
blanchet@42338
    97
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
    98
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@43228
    99
by (metis (full_types) pax)
blanchet@42338
   100
blanchet@50705
   101
declare [[metis_new_skolem]]
blanchet@42338
   102
blanchet@42338
   103
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
   104
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
   105
by (metis pax)
blanchet@42338
   106
blanchet@42338
   107
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
   108
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@43228
   109
by (metis (full_types) pax)
blanchet@42338
   110
blanchet@42747
   111
wenzelm@63167
   112
text \<open>New Skolemizer\<close>
blanchet@42338
   113
blanchet@50705
   114
declare [[metis_new_skolem]]
blanchet@42338
   115
blanchet@42338
   116
lemma
blanchet@42338
   117
  fixes x :: real
wenzelm@61969
   118
  assumes fn_le: "!!n. f n \<le> x" and 1: "f \<longlonglongrightarrow> lim f"
blanchet@42338
   119
  shows "lim f \<le> x"
blanchet@42338
   120
by (metis 1 LIMSEQ_le_const2 fn_le)
blanchet@42338
   121
blanchet@42338
   122
definition
blanchet@42338
   123
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
blanchet@42338
   124
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
blanchet@42338
   125
blanchet@42338
   126
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
blanchet@42338
   127
by (metis bounded_def subset_eq)
blanchet@42338
   128
blanchet@42338
   129
lemma
kuncar@47308
   130
  assumes a: "Quotient R Abs Rep T"
blanchet@42338
   131
  shows "symp R"
blanchet@42338
   132
using a unfolding Quotient_def using sympI
blanchet@43228
   133
by (metis (full_types))
blanchet@42338
   134
blanchet@42338
   135
lemma
blanchet@42338
   136
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
blanchet@42342
   137
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
blanchet@50696
   138
by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
blanchet@42338
   139
blanchet@42342
   140
lemma ex_tl: "EX ys. tl ys = xs"
blanchet@55417
   141
using list.sel(3) by fast
blanchet@42342
   142
wenzelm@61076
   143
lemma "(\<exists>ys::nat list. tl ys = xs) \<and> (\<exists>bs::int list. tl bs = as)"
blanchet@42342
   144
by (metis ex_tl)
blanchet@42342
   145
blanchet@42338
   146
end