(* Title: Sequents/LK.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Axiom to express monotonicity (a variant of the deduction theorem). Makes the
link between \<turnstile> and \<Longrightarrow>, needed for instance to prove imp_cong.
Axiom left_cong allows the simplifier to use left-side formulas. Ideally it
should be derived from lower-level axioms.
CANNOT be added to LK0.thy because modal logic is built upon it, and
various modal rules would become inconsistent.
*)
theory LK
imports LK0
begin
axiomatization where
monotonic: "($H \ P \ $H \ Q) \ $H, P \ Q" and
left_cong: "\P == P'; \ P' \ ($H \ $F) \ ($H' \ $F')\
\<Longrightarrow> (P, $H \<turnstile> $F) \<equiv> (P', $H' \<turnstile> $F')"
subsection \<open>Rewrite rules\<close>
lemma conj_simps:
"\ P \ True \ P"
"\ True \ P \ P"
"\ P \ False \ False"
"\ False \ P \ False"
"\ P \ P \ P"
"\ P \ P \ Q \ P \ Q"
"\ P \ \ P \ False"
"\ \ P \ P \ False"
"\ (P \ Q) \ R \ P \ (Q \ R)"
by (fast add!: subst)+
lemma disj_simps:
"\ P \ True \ True"
"\ True \ P \ True"
"\ P \ False \ P"
"\ False \ P \ P"
"\ P \ P \ P"
"\ P \ P \ Q \ P \ Q"
"\ (P \ Q) \ R \ P \ (Q \ R)"
by (fast add!: subst)+
lemma not_simps:
"\ \ False \ True"
"\ \ True \ False"
by (fast add!: subst)+
lemma imp_simps:
"\ (P \ False) \ \ P"
"\ (P \ True) \ True"
"\ (False \ P) \ True"
"\ (True \ P) \ P"
"\ (P \ P) \ True"
"\ (P \ \ P) \ \ P"
by (fast add!: subst)+
lemma iff_simps:
"\ (True \ P) \ P"
"\ (P \ True) \ P"
"\ (P \ P) \ True"
"\ (False \ P) \ \ P"
"\ (P \ False) \ \ P"
by (fast add!: subst)+
lemma quant_simps:
"\P. \ (\x. P) \ P"
"\P. \ (\x. x = t \ P(x)) \ P(t)"
"\P. \ (\x. t = x \ P(x)) \ P(t)"
"\P. \ (\x. P) \ P"
"\P. \ (\x. x = t \ P(x)) \ P(t)"
"\P. \ (\x. t = x \ P(x)) \ P(t)"
by (fast add!: subst)+
subsection \<open>Miniscoping: pushing quantifiers in\<close>
text \<open>
We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or>
Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
show that this step can increase proof length!
\<close>
text \<open>existential miniscoping\<close>
lemma ex_simps:
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
by (fast add!: subst)+
text \<open>universal miniscoping\<close>
lemma all_simps:
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
"\P Q. \ (\x. P(x) \ Q) \ (\x. P(x)) \ Q"
"\P Q. \ (\x. P \ Q(x)) \ P \ (\x. Q(x))"
by (fast add!: subst)+
text \<open>These are NOT supplied by default!\<close>
lemma distrib_simps:
"\ P \ (Q \ R) \ P \ Q \ P \ R"
"\ (Q \ R) \ P \ Q \ P \ R \ P"
"\ (P \ Q \ R) \ (P \ R) \ (Q \ R)"
by (fast add!: subst)+
lemma P_iff_F: "\ \ P \ \ (P \ False)"
apply (erule thinR [THEN cut])
apply fast
done
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
lemma P_iff_T: "\ P \ \ (P \ True)"
apply (erule thinR [THEN cut])
apply fast
done
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
lemma LK_extra_simps:
"\ P \ \ P"
"\ \ P \ P"
"\ \ \ P \ P"
"\ (\ P \ P) \ P"
"\ (\ P \ \ Q) \ (P \ Q)"
by (fast add!: subst)+
subsection \<open>Named rewrite rules\<close>
lemma conj_commute: "\ P \ Q \ Q \ P"
and conj_left_commute: "\ P \ (Q \ R) \ Q \ (P \ R)"
by (fast add!: subst)+
lemmas conj_comms = conj_commute conj_left_commute
lemma disj_commute: "\ P \ Q \ Q \ P"
and disj_left_commute: "\ P \ (Q \ R) \ Q \ (P \ R)"
by (fast add!: subst)+
lemmas disj_comms = disj_commute disj_left_commute
lemma conj_disj_distribL: "\ P \ (Q \ R) \ (P \ Q \ P \ R)"
and conj_disj_distribR: "\ (P \ Q) \ R \ (P \ R \ Q \ R)"
and disj_conj_distribL: "\ P \ (Q \ R) \ (P \ Q) \ (P \ R)"
and disj_conj_distribR: "\ (P \ Q) \ R \ (P \ R) \ (Q \ R)"
and imp_conj_distrib: "\ (P \ (Q \ R)) \ (P \ Q) \ (P \ R)"
and imp_conj: "\ ((P \ Q) \ R) \ (P \ (Q \ R))"
and imp_disj: "\ (P \ Q \ R) \ (P \ R) \ (Q \ R)"
and imp_disj1: "\ (P \ Q) \ R \ (P \ Q \ R)"
and imp_disj2: "\ Q \ (P \ R) \ (P \ Q \ R)"
and de_Morgan_disj: "\ (\ (P \ Q)) \ (\ P \ \ Q)"
and de_Morgan_conj: "\ (\ (P \ Q)) \ (\ P \ \ Q)"
and not_iff: "\ \ (P \ Q) \ (P \ \ Q)"
by (fast add!: subst)+
lemma imp_cong:
assumes p1: "\ P \ P'"
and p2: "\ P' \ \ Q \ Q'"
shows "\ (P \ Q) \ (P' \ Q')"
apply (lem p1)
apply safe
apply (tactic \<open>
REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
DEPTH_SOLVE_1
(resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
Cla.safe_tac \<^context> 1)\<close>)
done
lemma conj_cong:
assumes p1: "\ P \ P'"
and p2: "\ P' \ \ Q \ Q'"
shows "\ (P \ Q) \ (P' \ Q')"
apply (lem p1)
apply safe
apply (tactic \<open>
REPEAT (resolve_tac \<^context> @{thms cut} 1 THEN
DEPTH_SOLVE_1
(resolve_tac \<^context> [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN
Cla.safe_tac \<^context> 1)\<close>)
done
lemma eq_sym_conv: "\ x = y \ y = x"
by (fast add!: subst)
ML_file \<open>simpdata.ML\<close>
setup \<open>map_theory_simpset (put_simpset LK_ss)\<close>
setup \<open>Simplifier.method_setup []\<close>
text \<open>To create substitution rules\<close>
lemma eq_imp_subst: "\ a = b \ $H, A(a), $G \ $E, A(b), $F"
by simp
lemma split_if: "\ P(if Q then x else y) \ ((Q \ P(x)) \ (\ Q \ P(y)))"
apply (rule_tac P = Q in cut)
prefer 2
apply (simp add: if_P)
apply (rule_tac P = "\ Q" in cut)
prefer 2
apply (simp add: if_not_P)
apply fast
done
lemma if_cancel: "\ (if P then x else x) = x"
apply (lem split_if)
apply fast
done
lemma if_eq_cancel: "\ (if x = y then y else x) = x"
apply (lem split_if)
apply safe
apply (rule symL)
apply (rule basic)
done
end
¤ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
