src/HOL/Metis_Examples/Clausification.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 58889 5b7a9633cfa8 child 61076 bdc1e2f0a86a permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
```     1 (*  Title:      HOL/Metis_Examples/Clausification.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3
```
```     4 Example that exercises Metis's Clausifier.
```
```     5 *)
```
```     6
```
```     7 section {* 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
```