src/HOL/Metis_Examples/Clausify.thy
 author blanchet Thu Apr 14 11:24:04 2011 +0200 (2011-04-14) changeset 42340 4e4f0665e5be parent 42338 802f2fe7a0c9 child 42342 6babd86a54a4 permissions -rw-r--r--
added outstanding issue to Metis example
```     1 (*  Title:      HOL/Metis_Examples/Clausifier.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3
```
```     4 Testing Metis's clausifier.
```
```     5 *)
```
```     6
```
```     7 theory Clausifier
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 text {* Outstanding issues *}
```
```    12
```
```    13 lemma ex_tl: "EX ys. tl ys = xs"
```
```    14 using tl.simps(2) by fast
```
```    15
```
```    16 lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)"
```
```    17 using [[metis_new_skolemizer = false]] (* FAILS with "= true" *)
```
```    18 by (metis ex_tl)
```
```    19
```
```    20 text {* Definitional CNF for goal *}
```
```    21
```
```    22 (* FIXME: shouldn't need this *)
```
```    23 declare [[unify_search_bound = 100]]
```
```    24 declare [[unify_trace_bound = 100]]
```
```    25
```
```    26 axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
```
```    27 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))"
```
```    28
```
```    29 declare [[metis_new_skolemizer = false]]
```
```    30
```
```    31 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>
```
```    32                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
```
```    33 by (metis pax)
```
```    34
```
```    35 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>
```
```    36                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
```
```    37 by (metisFT pax)
```
```    38
```
```    39 declare [[metis_new_skolemizer]]
```
```    40
```
```    41 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>
```
```    42                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
```
```    43 by (metis pax)
```
```    44
```
```    45 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>
```
```    46                    (p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)"
```
```    47 by (metisFT pax)
```
```    48
```
```    49 text {* New Skolemizer *}
```
```    50
```
```    51 declare [[metis_new_skolemizer]]
```
```    52
```
```    53 lemma
```
```    54   fixes x :: real
```
```    55   assumes fn_le: "!!n. f n \<le> x" and 1: "f----> lim f"
```
```    56   shows "lim f \<le> x"
```
```    57 by (metis 1 LIMSEQ_le_const2 fn_le)
```
```    58
```
```    59 definition
```
```    60   bounded :: "'a::metric_space set \<Rightarrow> bool" where
```
```    61   "bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)"
```
```    62
```
```    63 lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
```
```    64 by (metis bounded_def subset_eq)
```
```    65
```
```    66 lemma
```
```    67   assumes a: "Quotient R Abs Rep"
```
```    68   shows "symp R"
```
```    69 using a unfolding Quotient_def using sympI
```
```    70 by metisFT
```
```    71
```
```    72 lemma
```
```    73   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
```
```    74    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
```
```    75 by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
```
```    76
```
```    77 end
```