author | blanchet |
Thu, 14 Apr 2011 11:24:05 +0200 | |
changeset 42345 | 5ecd55993606 |
parent 42343 | 118cc349de35 |
child 42350 | 128dc0fa87fc |
permissions | -rw-r--r-- |
42343 | 1 |
(* Title: HOL/Metis_Examples/Clausify.thy |
42338 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
||
4 |
Testing Metis's clausifier. |
|
5 |
*) |
|
6 |
||
42343 | 7 |
theory Clausify |
42338 | 8 |
imports Complex_Main |
9 |
begin |
|
10 |
||
11 |
(* FIXME: shouldn't need this *) |
|
12 |
declare [[unify_search_bound = 100]] |
|
13 |
declare [[unify_trace_bound = 100]] |
|
14 |
||
42345 | 15 |
text {* Definitional CNF for facts *} |
16 |
||
17 |
declare [[meson_max_clauses = 10]] |
|
18 |
||
19 |
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
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)" |
|
21 |
||
22 |
declare [[metis_new_skolemizer = false]] |
|
23 |
||
24 |
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
25 |
by (metis qax) |
|
26 |
||
27 |
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
28 |
by (metisFT qax) |
|
29 |
||
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)" |
|
31 |
by (metis qax) |
|
32 |
||
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)" |
|
34 |
by (metisFT qax) |
|
35 |
||
36 |
declare [[metis_new_skolemizer]] |
|
37 |
||
38 |
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
39 |
by (metis qax) |
|
40 |
||
41 |
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" |
|
42 |
by (metisFT qax) |
|
43 |
||
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)" |
|
45 |
by (metis qax) |
|
46 |
||
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)" |
|
48 |
by (metisFT qax) |
|
49 |
||
50 |
declare [[meson_max_clauses = 60]] |
|
51 |
||
52 |
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
53 |
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or> |
|
54 |
(r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or> |
|
55 |
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> |
|
56 |
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" |
|
57 |
||
58 |
declare [[metis_new_skolemizer = false]] |
|
59 |
||
60 |
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
61 |
by (metis rax) |
|
62 |
||
63 |
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
64 |
by (metisFT rax) |
|
65 |
||
66 |
declare [[metis_new_skolemizer]] |
|
67 |
||
68 |
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
69 |
by (metis rax) |
|
70 |
||
71 |
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" |
|
72 |
by (metisFT rax) |
|
73 |
||
74 |
text {* Definitional CNF for goal *} |
|
75 |
||
42338 | 76 |
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
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)" |
42338 | 78 |
|
79 |
declare [[metis_new_skolemizer = false]] |
|
80 |
||
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> |
|
82 |
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
|
83 |
by (metis pax) |
|
84 |
||
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> |
|
86 |
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
|
87 |
by (metisFT pax) |
|
88 |
||
89 |
declare [[metis_new_skolemizer]] |
|
90 |
||
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> |
|
92 |
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
|
93 |
by (metis pax) |
|
94 |
||
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> |
|
96 |
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" |
|
97 |
by (metisFT pax) |
|
98 |
||
99 |
text {* New Skolemizer *} |
|
100 |
||
101 |
declare [[metis_new_skolemizer]] |
|
102 |
||
103 |
lemma |
|
104 |
fixes x :: real |
|
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
105 |
assumes fn_le: "!!n. f n \<le> x" and 1: "f ----> lim f" |
42338 | 106 |
shows "lim f \<le> x" |
107 |
by (metis 1 LIMSEQ_le_const2 fn_le) |
|
108 |
||
109 |
definition |
|
110 |
bounded :: "'a::metric_space set \<Rightarrow> bool" where |
|
111 |
"bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)" |
|
112 |
||
113 |
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S" |
|
114 |
by (metis bounded_def subset_eq) |
|
115 |
||
116 |
lemma |
|
117 |
assumes a: "Quotient R Abs Rep" |
|
118 |
shows "symp R" |
|
119 |
using a unfolding Quotient_def using sympI |
|
120 |
by metisFT |
|
121 |
||
122 |
lemma |
|
123 |
"(\<exists>x \<in> set xs. P x) \<longleftrightarrow> |
|
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
124 |
(\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))" |
42338 | 125 |
by (metis split_list_last_prop [where P = P] in_set_conv_decomp) |
126 |
||
42342
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
127 |
lemma ex_tl: "EX ys. tl ys = xs" |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
128 |
using tl.simps(2) by fast |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
129 |
|
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
130 |
lemma "(\<exists>ys\<Colon>nat list. tl ys = xs) \<and> (\<exists>bs\<Colon>int list. tl bs = as)" |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
131 |
by (metis ex_tl) |
6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377
blanchet
parents:
42340
diff
changeset
|
132 |
|
42338 | 133 |
end |