src/HOL/Metis_Examples/Clausification.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43228 2ed2f092e990
child 47308 9caab698dbe4
permissions -rw-r--r--
remove lemma stupid_ext
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
blanchet@43197
     7
header {* Example that Exercises Metis's Clausifier *}
blanchet@43197
     8
blanchet@43197
     9
theory Clausification
blanchet@42338
    10
imports Complex_Main
blanchet@42338
    11
begin
blanchet@42338
    12
blanchet@42338
    13
(* FIXME: shouldn't need this *)
blanchet@42338
    14
declare [[unify_search_bound = 100]]
blanchet@42338
    15
declare [[unify_trace_bound = 100]]
blanchet@42338
    16
blanchet@42747
    17
blanchet@42345
    18
text {* Definitional CNF for facts *}
blanchet@42345
    19
blanchet@42345
    20
declare [[meson_max_clauses = 10]]
blanchet@42345
    21
blanchet@42345
    22
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    23
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
    24
blanchet@42345
    25
declare [[metis_new_skolemizer = false]]
blanchet@42345
    26
blanchet@42345
    27
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    28
by (metis qax)
blanchet@42345
    29
blanchet@42345
    30
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@43228
    31
by (metis (full_types) qax)
blanchet@42345
    32
blanchet@42345
    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)"
blanchet@42345
    34
by (metis qax)
blanchet@42345
    35
blanchet@42345
    36
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
    37
by (metis (full_types) qax)
blanchet@42345
    38
blanchet@42345
    39
declare [[metis_new_skolemizer]]
blanchet@42345
    40
blanchet@42345
    41
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    42
by (metis qax)
blanchet@42345
    43
blanchet@42345
    44
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@43228
    45
by (metis (full_types) qax)
blanchet@42345
    46
blanchet@42345
    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)"
blanchet@42345
    48
by (metis qax)
blanchet@42345
    49
blanchet@42345
    50
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
    51
by (metis (full_types) qax)
blanchet@42345
    52
blanchet@42345
    53
declare [[meson_max_clauses = 60]]
blanchet@42345
    54
blanchet@42345
    55
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    56
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42345
    57
      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42345
    58
      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42345
    59
      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42345
    60
blanchet@42345
    61
declare [[metis_new_skolemizer = false]]
blanchet@42345
    62
blanchet@42345
    63
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    64
by (metis rax)
blanchet@42345
    65
blanchet@42345
    66
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@43228
    67
by (metis (full_types) rax)
blanchet@42345
    68
blanchet@42345
    69
declare [[metis_new_skolemizer]]
blanchet@42345
    70
blanchet@42345
    71
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    72
by (metis rax)
blanchet@42345
    73
blanchet@42345
    74
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@43228
    75
by (metis (full_types) rax)
blanchet@42345
    76
blanchet@42350
    77
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
    78
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
    79
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
    80
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42350
    81
by (metis rax)
blanchet@42350
    82
blanchet@42350
    83
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42350
    84
       (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42350
    85
       (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42350
    86
       (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@43228
    87
by (metis (full_types) rax)
blanchet@42350
    88
blanchet@42747
    89
blanchet@42345
    90
text {* Definitional CNF for goal *}
blanchet@42345
    91
blanchet@42338
    92
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    93
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
    94
blanchet@42338
    95
declare [[metis_new_skolemizer = false]]
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@42338
    99
by (metis pax)
blanchet@42338
   100
blanchet@42338
   101
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
   102
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@43228
   103
by (metis (full_types) pax)
blanchet@42338
   104
blanchet@42338
   105
declare [[metis_new_skolemizer]]
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@42338
   109
by (metis pax)
blanchet@42338
   110
blanchet@42338
   111
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
   112
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@43228
   113
by (metis (full_types) pax)
blanchet@42338
   114
blanchet@42747
   115
blanchet@42338
   116
text {* New Skolemizer *}
blanchet@42338
   117
blanchet@42338
   118
declare [[metis_new_skolemizer]]
blanchet@42338
   119
blanchet@42338
   120
lemma
blanchet@42338
   121
  fixes x :: real
blanchet@42342
   122
  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
blanchet@42338
   123
  shows "lim f \<le> x"
blanchet@42338
   124
by (metis 1 LIMSEQ_le_const2 fn_le)
blanchet@42338
   125
blanchet@42338
   126
definition
blanchet@42338
   127
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
blanchet@42338
   128
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
blanchet@42338
   129
blanchet@42338
   130
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
blanchet@42338
   131
by (metis bounded_def subset_eq)
blanchet@42338
   132
blanchet@42338
   133
lemma
blanchet@42338
   134
  assumes a: "Quotient R Abs Rep"
blanchet@42338
   135
  shows "symp R"
blanchet@42338
   136
using a unfolding Quotient_def using sympI
blanchet@43228
   137
by (metis (full_types))
blanchet@42338
   138
blanchet@42338
   139
lemma
blanchet@42338
   140
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
blanchet@42342
   141
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
blanchet@42338
   142
by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
blanchet@42338
   143
blanchet@42342
   144
lemma ex_tl: "EX ys. tl ys = xs"
blanchet@42342
   145
using tl.simps(2) by fast
blanchet@42342
   146
blanchet@42342
   147
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
blanchet@42342
   148
by (metis ex_tl)
blanchet@42342
   149
blanchet@42338
   150
end