42338
|
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 |
|
42340
|
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)
|
42338
|
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
|