src/HOL/Metis_Examples/Clausify.thy
author blanchet
Thu Apr 14 11:24:05 2011 +0200 (2011-04-14)
changeset 42345 5ecd55993606
parent 42343 118cc349de35
child 42350 128dc0fa87fc
permissions -rw-r--r--
added examples of definitional CNF facts
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@42345
    15
text {* Definitional CNF for facts *}
blanchet@42345
    16
blanchet@42345
    17
declare [[meson_max_clauses = 10]]
blanchet@42345
    18
blanchet@42345
    19
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    20
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
    21
blanchet@42345
    22
declare [[metis_new_skolemizer = false]]
blanchet@42345
    23
blanchet@42345
    24
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    25
by (metis qax)
blanchet@42345
    26
blanchet@42345
    27
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    28
by (metisFT qax)
blanchet@42345
    29
blanchet@42345
    30
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
    31
by (metis 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 (metisFT qax)
blanchet@42345
    35
blanchet@42345
    36
declare [[metis_new_skolemizer]]
blanchet@42345
    37
blanchet@42345
    38
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    39
by (metis qax)
blanchet@42345
    40
blanchet@42345
    41
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)"
blanchet@42345
    42
by (metisFT qax)
blanchet@42345
    43
blanchet@42345
    44
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
    45
by (metis 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 (metisFT qax)
blanchet@42345
    49
blanchet@42345
    50
declare [[meson_max_clauses = 60]]
blanchet@42345
    51
blanchet@42345
    52
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    53
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or>
blanchet@42345
    54
      (r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or>
blanchet@42345
    55
      (r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or>
blanchet@42345
    56
      (r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)"
blanchet@42345
    57
blanchet@42345
    58
declare [[metis_new_skolemizer = false]]
blanchet@42345
    59
blanchet@42345
    60
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    61
by (metis rax)
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 (metisFT rax)
blanchet@42345
    65
blanchet@42345
    66
declare [[metis_new_skolemizer]]
blanchet@42345
    67
blanchet@42345
    68
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3"
blanchet@42345
    69
by (metis rax)
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 (metisFT rax)
blanchet@42345
    73
blanchet@42345
    74
text {* Definitional CNF for goal *}
blanchet@42345
    75
blanchet@42338
    76
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
blanchet@42345
    77
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
    78
blanchet@42338
    79
declare [[metis_new_skolemizer = false]]
blanchet@42338
    80
blanchet@42338
    81
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
    82
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    83
by (metis pax)
blanchet@42338
    84
blanchet@42338
    85
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
    86
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    87
by (metisFT pax)
blanchet@42338
    88
blanchet@42338
    89
declare [[metis_new_skolemizer]]
blanchet@42338
    90
blanchet@42338
    91
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
    92
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    93
by (metis pax)
blanchet@42338
    94
blanchet@42338
    95
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
    96
                   (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
blanchet@42338
    97
by (metisFT pax)
blanchet@42338
    98
blanchet@42338
    99
text {* New Skolemizer *}
blanchet@42338
   100
blanchet@42338
   101
declare [[metis_new_skolemizer]]
blanchet@42338
   102
blanchet@42338
   103
lemma
blanchet@42338
   104
  fixes x :: real
blanchet@42342
   105
  assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f"
blanchet@42338
   106
  shows "lim f \<le> x"
blanchet@42338
   107
by (metis 1 LIMSEQ_le_const2 fn_le)
blanchet@42338
   108
blanchet@42338
   109
definition
blanchet@42338
   110
  bounded :: "'a::metric_space set \<Rightarrow> bool" where
blanchet@42338
   111
  "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
blanchet@42338
   112
blanchet@42338
   113
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
blanchet@42338
   114
by (metis bounded_def subset_eq)
blanchet@42338
   115
blanchet@42338
   116
lemma
blanchet@42338
   117
  assumes a: "Quotient R Abs Rep"
blanchet@42338
   118
  shows "symp R"
blanchet@42338
   119
using a unfolding Quotient_def using sympI
blanchet@42338
   120
by metisFT
blanchet@42338
   121
blanchet@42338
   122
lemma
blanchet@42338
   123
  "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
blanchet@42342
   124
   (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
blanchet@42338
   125
by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
blanchet@42338
   126
blanchet@42342
   127
lemma ex_tl: "EX ys. tl ys = xs"
blanchet@42342
   128
using tl.simps(2) by fast
blanchet@42342
   129
blanchet@42342
   130
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
blanchet@42342
   131
by (metis ex_tl)
blanchet@42342
   132
blanchet@42338
   133
end