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