author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47308  9caab698dbe4 
child 50696  85f944352d55 
permissions  rwrr 
43197  1 
(* Title: HOL/Metis_Examples/Clausification.thy 
42338  2 
Author: Jasmin Blanchette, TU Muenchen 
3 

43197  4 
Example that exercises Metis's Clausifier. 
42338  5 
*) 
6 

43197  7 
header {* Example that Exercises Metis's Clausifier *} 
8 

9 
theory Clausification 

42338  10 
imports Complex_Main 
11 
begin 

12 

13 
(* FIXME: shouldn't need this *) 

14 
declare [[unify_search_bound = 100]] 

15 
declare [[unify_trace_bound = 100]] 

16 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42350
diff
changeset

17 

42345  18 
text {* Definitional CNF for facts *} 
19 

20 
declare [[meson_max_clauses = 10]] 

21 

22 
axiomatization q :: "nat \<Rightarrow> nat \<Rightarrow> bool" where 

23 
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)" 

24 

25 
declare [[metis_new_skolemizer = false]] 

26 

27 
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" 

28 
by (metis qax) 

29 

30 
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

31 
by (metis (full_types) qax) 
42345  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 (metis qax) 

35 

36 
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)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

37 
by (metis (full_types) qax) 
42345  38 

39 
declare [[metis_new_skolemizer]] 

40 

41 
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" 

42 
by (metis qax) 

43 

44 
lemma "\<exists>b. \<forall>a. (q b a \<or> q a b)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

45 
by (metis (full_types) qax) 
42345  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 (metis qax) 

49 

50 
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)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

51 
by (metis (full_types) qax) 
42345  52 

53 
declare [[meson_max_clauses = 60]] 

54 

55 
axiomatization r :: "nat \<Rightarrow> nat \<Rightarrow> bool" where 

56 
rax: "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or> 

57 
(r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or> 

58 
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> 

59 
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" 

60 

61 
declare [[metis_new_skolemizer = false]] 

62 

63 
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" 

64 
by (metis rax) 

65 

66 
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

67 
by (metis (full_types) rax) 
42345  68 

69 
declare [[metis_new_skolemizer]] 

70 

71 
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" 

72 
by (metis rax) 

73 

74 
lemma "r 0 0 \<or> r 1 1 \<or> r 2 2 \<or> r 3 3" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

75 
by (metis (full_types) rax) 
42345  76 

42350  77 
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or> 
78 
(r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or> 

79 
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> 

80 
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" 

81 
by (metis rax) 

82 

83 
lemma "(r 0 0 \<and> r 0 1 \<and> r 0 2 \<and> r 0 3) \<or> 

84 
(r 1 0 \<and> r 1 1 \<and> r 1 2 \<and> r 1 3) \<or> 

85 
(r 2 0 \<and> r 2 1 \<and> r 2 2 \<and> r 2 3) \<or> 

86 
(r 3 0 \<and> r 3 1 \<and> r 3 2 \<and> r 3 3)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

87 
by (metis (full_types) rax) 
42350  88 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42350
diff
changeset

89 

42345  90 
text {* Definitional CNF for goal *} 
91 

42338  92 
axiomatization p :: "nat \<Rightarrow> nat \<Rightarrow> bool" where 
42345  93 
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  94 

95 
declare [[metis_new_skolemizer = false]] 

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 pax) 

100 

101 
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> 

102 
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

103 
by (metis (full_types) pax) 
42338  104 

105 
declare [[metis_new_skolemizer]] 

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 pax) 

110 

111 
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> 

112 
(p 0 1 \<or> \<not> x) \<and> (p 1 0 \<or> \<not> x) \<and> (p a b \<or> \<not> x)" 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

113 
by (metis (full_types) pax) 
42338  114 

42747
f132d13fcf75
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
blanchet
parents:
42350
diff
changeset

115 

42338  116 
text {* New Skolemizer *} 
117 

118 
declare [[metis_new_skolemizer]] 

119 

120 
lemma 

121 
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 typeinstances 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

122 
assumes fn_le: "!!n. f n \<le> x" and 1: "f > lim f" 
42338  123 
shows "lim f \<le> x" 
124 
by (metis 1 LIMSEQ_le_const2 fn_le) 

125 

126 
definition 

127 
bounded :: "'a::metric_space set \<Rightarrow> bool" where 

128 
"bounded S \<longleftrightarrow> (\<exists>x eee. \<forall>y\<in>S. dist x y \<le> eee)" 

129 

130 
lemma "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S" 

131 
by (metis bounded_def subset_eq) 

132 

133 
lemma 

47308  134 
assumes a: "Quotient R Abs Rep T" 
42338  135 
shows "symp R" 
136 
using a unfolding Quotient_def using sympI 

43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43197
diff
changeset

137 
by (metis (full_types)) 
42338  138 

139 
lemma 

140 
"(\<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 typeinstances 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

141 
(\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))" 
42338  142 
by (metis split_list_last_prop [where P = P] in_set_conv_decomp) 
143 

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 typeinstances 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

144 
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 typeinstances 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

145 
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 typeinstances 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

146 

6babd86a54a4
handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several typeinstances 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

147 
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 typeinstances 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

148 
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 typeinstances 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

149 

42338  150 
end 