author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 48891  c0eafbd55de3 
child 54148  c8cc5ab4a863 
permissions  rwrr 
39941  1 
(* Title: HOL/Meson.thy 
39944  2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
3 
Author: Tobias Nipkow, TU Muenchen 

4 
Author: Jasmin Blanchette, TU Muenchen 

39941  5 
Copyright 2001 University of Cambridge 
6 
*) 

7 

39947  8 
header {* MESON Proof Method *} 
39941  9 

10 
theory Meson 

39946  11 
imports Datatype 
39941  12 
begin 
13 

40620  14 
subsection {* Negation Normal Form *} 
39941  15 

16 
text {* de Morgan laws *} 

17 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

18 
lemma not_conjD: "~(P&Q) ==> ~P  ~Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

19 
and not_disjD: "~(PQ) ==> ~P & ~Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

20 
and not_notD: "~~P ==> P" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

21 
and not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

22 
and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)" 
39941  23 
by fast+ 
24 

25 
text {* Removal of @{text ">"} and @{text "<>"} (positive and 

26 
negative occurrences) *} 

27 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

28 
lemma imp_to_disjD: "P>Q ==> ~P  Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

29 
and not_impD: "~(P>Q) ==> P & ~Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

30 
and iff_to_disjD: "P=Q ==> (~P  Q) & (~Q  P)" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

31 
and not_iffD: "~(P=Q) ==> (P  Q) & (~P  ~Q)" 
39941  32 
 {* Much more efficient than @{prop "(P & ~Q)  (Q & ~P)"} for computing CNF *} 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

33 
and not_refl_disj_D: "x ~= x  P ==> P" 
39941  34 
by fast+ 
35 

36 

40620  37 
subsection {* Pulling out the existential quantifiers *} 
39941  38 

39 
text {* Conjunction *} 

40 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

41 
lemma conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

42 
and conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)" 
39941  43 
by fast+ 
44 

45 

46 
text {* Disjunction *} 

47 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

48 
lemma disj_exD: "!!P Q. (\<exists>x. P(x))  (\<exists>x. Q(x)) ==> \<exists>x. P(x)  Q(x)" 
39941  49 
 {* DO NOT USE with forallSkolemization: makes fewer schematic variables!! *} 
50 
 {* With exSkolemization, makes fewer Skolem constants *} 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

51 
and disj_exD1: "!!P Q. (\<exists>x. P(x))  Q ==> \<exists>x. P(x)  Q" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

52 
and disj_exD2: "!!P Q. P  (\<exists>x. Q(x)) ==> \<exists>x. P  Q(x)" 
39941  53 
by fast+ 
54 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

55 
lemma disj_assoc: "(PQ)R ==> P(QR)" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

56 
and disj_comm: "PQ ==> QP" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

57 
and disj_FalseD1: "FalseP ==> P" 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

58 
and disj_FalseD2: "PFalse ==> P" 
39941  59 
by fast+ 
60 

61 

62 
text{* Generation of contrapositives *} 

63 

64 
text{*Inserts negated disjunct after removing the negation; P is a literal. 

65 
Model elimination requires assuming the negation of every attempted subgoal, 

66 
hence the negated disjuncts.*} 

67 
lemma make_neg_rule: "~PQ ==> ((~P==>P) ==> Q)" 

68 
by blast 

69 

70 
text{*Version for Plaisted's "Postive refinement" of the Meson procedure*} 

71 
lemma make_refined_neg_rule: "~PQ ==> (P ==> Q)" 

72 
by blast 

73 

74 
text{*@{term P} should be a literal*} 

75 
lemma make_pos_rule: "PQ ==> ((P==>~P) ==> Q)" 

76 
by blast 

77 

78 
text{*Versions of @{text make_neg_rule} and @{text make_pos_rule} that don't 

79 
insert new assumptions, for ordinary resolution.*} 

80 

81 
lemmas make_neg_rule' = make_refined_neg_rule 

82 

83 
lemma make_pos_rule': "[PQ; ~P] ==> Q" 

84 
by blast 

85 

86 
text{* Generation of a goal clause  put away the final literal *} 

87 

88 
lemma make_neg_goal: "~P ==> ((~P==>P) ==> False)" 

89 
by blast 

90 

91 
lemma make_pos_goal: "P ==> ((P==>~P) ==> False)" 

92 
by blast 

93 

94 

40620  95 
subsection {* Lemmas for Forward Proof *} 
39941  96 

97 
text{*There is a similarity to congruence rules*} 

98 

99 
(*NOTE: could handle conjunctions (faster?) by 

100 
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) 

101 
lemma conj_forward: "[ P'&Q'; P' ==> P; Q' ==> Q ] ==> P&Q" 

102 
by blast 

103 

104 
lemma disj_forward: "[ P'Q'; P' ==> P; Q' ==> Q ] ==> PQ" 

105 
by blast 

106 

107 
(*Version of @{text disj_forward} for removal of duplicate literals*) 

108 
lemma disj_forward2: 

109 
"[ P'Q'; P' ==> P; [ Q'; P==>False ] ==> Q ] ==> PQ" 

110 
apply blast 

111 
done 

112 

113 
lemma all_forward: "[ \<forall>x. P'(x); !!x. P'(x) ==> P(x) ] ==> \<forall>x. P(x)" 

114 
by blast 

115 

116 
lemma ex_forward: "[ \<exists>x. P'(x); !!x. P'(x) ==> P(x) ] ==> \<exists>x. P(x)" 

117 
by blast 

118 

119 

40620  120 
subsection {* Clausification helper *} 
39941  121 

122 
lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" 

123 
by simp 

124 

47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

125 
lemma ext_cong_neq: "F g \<noteq> F h \<Longrightarrow> F g \<noteq> F h \<and> (\<exists>x. g x \<noteq> h x)" 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

126 
apply (erule contrapos_np) 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

127 
apply clarsimp 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

128 
apply (rule cong[where f = F]) 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

129 
by auto 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

130 

39941  131 

132 
text{* Combinator translation helpers *} 

133 

134 
definition COMBI :: "'a \<Rightarrow> 'a" where 

135 
[no_atp]: "COMBI P = P" 

136 

137 
definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where 

138 
[no_atp]: "COMBK P Q = P" 

139 

140 
definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]: 

141 
"COMBB P Q R = P (Q R)" 

142 

143 
definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where 

144 
[no_atp]: "COMBC P Q R = P R Q" 

145 

146 
definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where 

147 
[no_atp]: "COMBS P Q R = P R (Q R)" 

148 

149 
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" 

150 
apply (rule eq_reflection) 

151 
apply (rule ext) 

152 
apply (simp add: COMBS_def) 

153 
done 

154 

155 
lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI" 

156 
apply (rule eq_reflection) 

157 
apply (rule ext) 

158 
apply (simp add: COMBI_def) 

159 
done 

160 

161 
lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y" 

162 
apply (rule eq_reflection) 

163 
apply (rule ext) 

164 
apply (simp add: COMBK_def) 

165 
done 

166 

167 
lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g" 

168 
apply (rule eq_reflection) 

169 
apply (rule ext) 

170 
apply (simp add: COMBB_def) 

171 
done 

172 

173 
lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b" 

174 
apply (rule eq_reflection) 

175 
apply (rule ext) 

176 
apply (simp add: COMBC_def) 

177 
done 

178 

179 

40620  180 
subsection {* Skolemization helpers *} 
39941  181 

182 
definition skolem :: "'a \<Rightarrow> 'a" where 

183 
[no_atp]: "skolem = (\<lambda>x. x)" 

184 

185 
lemma skolem_COMBK_iff: "P \<longleftrightarrow> skolem (COMBK P (i\<Colon>nat))" 

186 
unfolding skolem_def COMBK_def by (rule refl) 

187 

188 
lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff] 

189 
lemmas skolem_COMBK_D = iffD2 [OF skolem_COMBK_iff] 

190 

191 

40620  192 
subsection {* Meson package *} 
39941  193 

48891  194 
ML_file "Tools/Meson/meson.ML" 
195 
ML_file "Tools/Meson/meson_clausify.ML" 

196 
ML_file "Tools/Meson/meson_tactic.ML" 

39941  197 

42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
40620
diff
changeset

198 
setup {* Meson_Tactic.setup *} 
39941  199 

39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

200 
hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

201 
hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

202 
not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

203 
disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI 
47953
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

204 
ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K 
a2c3706c4cb1
added "ext_cong_neq" lemma (not used yet); tuning
blanchet
parents:
42616
diff
changeset

205 
abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39950
diff
changeset

206 

39941  207 
end 