(* Title: HOL/Meson.thy
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Tobias Nipkow, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Copyright 2001 University of Cambridge
*)
section ‹MESON
Proof Method
›
theory Meson
imports Nat
begin
subsection ‹Negation Normal Form
›
text ‹de Morgan laws
›
lemma not_conjD:
"\(P\Q) \ \P \ \Q"
and not_disjD:
"\(P\Q) \ \P \ \Q"
and not_notD:
"\\P \ P"
and not_allD:
"\P. \(\x. P(x)) \ \x. \P(x)"
and not_exD:
"\P. \(\x. P(x)) \ \x. \P(x)"
by fast+
text ‹Removal of
‹⟶› and ‹⟷› (positive
and negative occurrences)
›
lemma imp_to_disjD:
"P\Q \ \P \ Q"
and not_impD:
"\(P\Q) \ P \ \Q"
and iff_to_disjD:
"P=Q \ (\P \ Q) \ (\Q \ P)"
and not_iffD:
"\(P=Q) \ (P \ Q) \ (\P \ \Q)"
🍋 ‹Much more efficient than
🍋‹(P
∧ ¬Q)
∨ (Q
∧ ¬P)
› for computing CNF
›
and not_refl_disj_D:
"x \ x \ P \ P"
by fast+
subsection ‹Pulling out the existential quantifiers
›
text ‹Conjunction
›
lemma conj_exD1:
"\P Q. (\x. P(x)) \ Q \ \x. P(x) \ Q"
and conj_exD2:
"\P Q. P \ (\x. Q(x)) \ \x. P \ Q(x)"
by fast+
text ‹Disjunction
›
lemma disj_exD:
"\P Q. (\x. P(x)) \ (\x. Q(x)) \ \x. P(x) \ Q(x)"
🍋 ‹DO NOT
USE with forall-Skolemization: makes fewer schematic variables!!
›
🍋 ‹With ex-Skolemization, makes fewer Skolem constants
›
and disj_exD1:
"\P Q. (\x. P(x)) \ Q \ \x. P(x) \ Q"
and disj_exD2:
"\P Q. P \ (\x. Q(x)) \ \x. P \ Q(x)"
by fast+
lemma disj_assoc:
"(P\Q)\R \ P\(Q\R)"
and disj_comm:
"P\Q \ Q\P"
and disj_FalseD1:
"False\P \ P"
and disj_FalseD2:
"P\False \ P"
by fast+
text‹Generation of contrapositives
›
text‹Inserts negated disjunct after removing the negation; P
is a literal.
Model elimination requires assuming the negation of every attempted subgoal,
hence the negated disjuncts.
›
lemma make_neg_rule:
"\P\Q \ ((\P\P) \ Q)"
by blast
text‹Version
for Plaisted
's "Postive refinement" of the Meson procedure\
lemma make_refined_neg_rule:
"\P\Q \ (P \ Q)"
by blast
text‹🍋‹P
› should be a literal
›
lemma make_pos_rule:
"P\Q \ ((P\\P) \ Q)"
by blast
text‹Versions of
‹make_neg_rule
› and ‹make_pos_rule
› that don
't
insert new assumptions,
for ordinary resolution.
›
lemmas make_neg_rule
' = make_refined_neg_rule
lemma make_pos_rule
': "\P\Q; \P\ \ Q"
by blast
text‹Generation of a goal clause -- put away the final literal
›
lemma make_neg_goal:
"\P \ ((\P\P) \ False)"
by blast
lemma make_pos_goal:
"P \ ((P\\P) \ False)"
by blast
subsection ‹Lemmas for Forward
Proof›
text‹There
is a similarity
to congruence rules. They are
also useful
in ordinary proofs.
›
(*NOTE: could handle conjunctions (faster?) by
nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)
lemma conj_forward:
"\P'\Q'; P' \ P; Q' \ Q \ \ P\Q"
by blast
lemma disj_forward:
"\P'\Q'; P' \ P; Q' \ Q \ \ P\Q"
by blast
lemma imp_forward:
"\P' \ Q'; P \ P'; Q' \ Q \ \ P \ Q"
by blast
lemma imp_forward2:
"\P' \ Q'; P \ P'; P' \ Q' \ Q \ \ P \ Q"
by blast
(*Version of @{text disj_forward} for removal of duplicate literals*)
lemma disj_forward2:
"\ P'\Q'; P' \ P; \Q'; P\False\ \ Q\ \ P\Q"
apply blast
done
lemma all_forward:
"[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)"
by blast
lemma ex_forward:
"[| \x. P'(x); !!x. P'(x) ==> P(x) |] ==> \x. P(x)"
by blast
subsection ‹Clausification helper
›
lemma TruepropI:
"P \ Q \ Trueprop P \ Trueprop Q"
by simp
lemma ext_cong_neq:
"F g \ F h \ F g \ F h \ (\x. g x \ h x)"
apply (erule contrapos_np)
apply clarsimp
apply (rule cong[
where f = F])
by auto
text‹Combinator translation helpers
›
definition COMBI ::
"'a \ 'a" where
"COMBI P = P"
definition COMBK ::
"'a \ 'b \ 'a" where
"COMBK P Q = P"
definition COMBB ::
"('b => 'c) \ ('a => 'b) \ 'a \ 'c" where
"COMBB P Q R = P (Q R)"
definition COMBC ::
"('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where
"COMBC P Q R = P R Q"
definition COMBS ::
"('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where
"COMBS P Q R = P R (Q R)"
lemma abs_S:
"\x. (f x) (g x) \ COMBS f g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBS_def)
done
lemma abs_I:
"\x. x \ COMBI"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBI_def)
done
lemma abs_K:
"\x. y \ COMBK y"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBK_def)
done
lemma abs_B:
"\x. a (g x) \ COMBB a g"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBB_def)
done
lemma abs_C:
"\x. (f x) b \ COMBC f b"
apply (rule eq_reflection)
apply (rule ext)
apply (simp add: COMBC_def)
done
subsection ‹Skolemization helpers
›
definition skolem ::
"'a \ 'a" where
"skolem = (\x. x)"
lemma skolem_COMBK_iff:
"P \ skolem (COMBK P (i::nat))"
unfolding skolem_def COMBK_def
by (rule refl)
lemmas skolem_COMBK_I = iffD1 [OF skolem_COMBK_iff]
subsection ‹Meson package
›
ML_file
‹Tools/Meson/meson.ML
›
ML_file
‹Tools/Meson/meson_clausify.ML
›
ML_file
‹Tools/Meson/meson_tactic.ML
›
hide_const (
open) COMBI COMBK COMBB COMBC COMBS skolem
hide_fact (
open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
ext_cong_neq COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K
abs_B abs_C abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I
end
