--- a/src/FOL/FOL.thy Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/FOL.thy Mon Oct 19 20:29:29 2015 +0200
@@ -17,7 +17,7 @@
subsection \<open>The classical axiom\<close>
axiomatization where
- classical: "(~P ==> P) ==> P"
+ classical: "(\<not> P \<Longrightarrow> P) \<Longrightarrow> P"
subsection \<open>Lemmas and proof tools\<close>
@@ -25,40 +25,41 @@
lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
by (erule FalseE [THEN classical])
-(*** Classical introduction rules for | and EX ***)
-lemma disjCI: "(~Q ==> P) ==> P|Q"
+subsubsection \<open>Classical introduction rules for @{text "\<or>"} and @{text "\<exists>"}\<close>
+
+lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
apply (rule classical)
apply (assumption | erule meta_mp | rule disjI1 notI)+
apply (erule notE disjI2)+
done
-(*introduction rule involving only EX*)
+text \<open>Introduction rule involving only @{text "\<exists>"}\<close>
lemma ex_classical:
- assumes r: "~(EX x. P(x)) ==> P(a)"
- shows "EX x. P(x)"
+ assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
+ shows "\<exists>x. P(x)"
apply (rule classical)
apply (rule exI, erule r)
done
-(*version of above, simplifying ~EX to ALL~ *)
+text \<open>Version of above, simplifying @{text "\<not>\<exists>"} to @{text "\<forall>\<not>"}.\<close>
lemma exCI:
- assumes r: "ALL x. ~P(x) ==> P(a)"
- shows "EX x. P(x)"
+ assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
+ shows "\<exists>x. P(x)"
apply (rule ex_classical)
apply (rule notI [THEN allI, THEN r])
apply (erule notE)
apply (erule exI)
done
-lemma excluded_middle: "~P | P"
+lemma excluded_middle: "\<not> P \<or> P"
apply (rule disjCI)
apply assumption
done
lemma case_split [case_names True False]:
- assumes r1: "P ==> Q"
- and r2: "~P ==> Q"
+ assumes r1: "P \<Longrightarrow> Q"
+ and r2: "\<not> P \<Longrightarrow> Q"
shows Q
apply (rule excluded_middle [THEN disjE])
apply (erule r2)
@@ -67,7 +68,7 @@
ML \<open>
fun case_tac ctxt a fixes =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
\<close>
method_setup case_tac = \<open>
@@ -76,14 +77,13 @@
\<close> "case_tac emulation (dynamic instantiation!)"
-(*** Special elimination rules *)
-
+subsection \<open>Special elimination rules\<close>
-(*Classical implies (-->) elimination. *)
+text \<open>Classical implies (@{text "\<longrightarrow>"}) elimination.\<close>
lemma impCE:
- assumes major: "P-->Q"
- and r1: "~P ==> R"
- and r2: "Q ==> R"
+ assumes major: "P \<longrightarrow> Q"
+ and r1: "\<not> P \<Longrightarrow> R"
+ and r2: "Q \<Longrightarrow> R"
shows R
apply (rule excluded_middle [THEN disjE])
apply (erule r1)
@@ -91,13 +91,15 @@
apply (erule major [THEN mp])
done
-(*This version of --> elimination works on Q before P. It works best for
- those cases in which P holds "almost everywhere". Can't install as
- default: would break old proofs.*)
+text \<open>
+ This version of @{text "\<longrightarrow>"} elimination works on @{text Q} before @{text
+ P}. It works best for those cases in which P holds ``almost everywhere''.
+ Can't install as default: would break old proofs.
+\<close>
lemma impCE':
- assumes major: "P-->Q"
- and r1: "Q ==> R"
- and r2: "~P ==> R"
+ assumes major: "P \<longrightarrow> Q"
+ and r1: "Q \<Longrightarrow> R"
+ and r2: "\<not> P \<Longrightarrow> R"
shows R
apply (rule excluded_middle [THEN disjE])
apply (erule r2)
@@ -105,27 +107,30 @@
apply (erule major [THEN mp])
done
-(*Double negation law*)
-lemma notnotD: "~~P ==> P"
+text \<open>Double negation law.\<close>
+lemma notnotD: "\<not> \<not> P \<Longrightarrow> P"
apply (rule classical)
apply (erule notE)
apply assumption
done
-lemma contrapos2: "[| Q; ~ P ==> ~ Q |] ==> P"
+lemma contrapos2: "\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P"
apply (rule classical)
apply (drule (1) meta_mp)
apply (erule (1) notE)
done
-(*** Tactics for implication and contradiction ***)
+
+subsubsection \<open>Tactics for implication and contradiction\<close>
-(*Classical <-> elimination. Proof substitutes P=Q in
- ~P ==> ~Q and P ==> Q *)
+text \<open>
+ Classical @{text "\<longleftrightarrow>"} elimination. Proof substitutes @{text "P = Q"} in
+ @{text "\<not> P \<Longrightarrow> \<not> Q"} and @{text "P \<Longrightarrow> Q"}.
+\<close>
lemma iffCE:
- assumes major: "P<->Q"
- and r1: "[| P; Q |] ==> R"
- and r2: "[| ~P; ~Q |] ==> R"
+ assumes major: "P \<longleftrightarrow> Q"
+ and r1: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
+ and r2: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
shows R
apply (rule major [unfolded iff_def, THEN conjE])
apply (elim impCE)
@@ -137,8 +142,8 @@
(*Better for fast_tac: needs no quantifier duplication!*)
lemma alt_ex1E:
- assumes major: "EX! x. P(x)"
- and r: "!!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R"
+ assumes major: "\<exists>! x. P(x)"
+ and r: "\<And>x. \<lbrakk>P(x); \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
shows R
using major
proof (rule ex1E)
@@ -147,19 +152,22 @@
assume "P(x)"
then show R
proof (rule r)
- { fix y y'
+ {
+ fix y y'
assume "P(y)" and "P(y')"
- with * have "x = y" and "x = y'" by - (tactic "IntPr.fast_tac @{context} 1")+
+ with * have "x = y" and "x = y'"
+ by - (tactic "IntPr.fast_tac @{context} 1")+
then have "y = y'" by (rule subst)
} note r' = this
- show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'" by (intro strip, elim conjE) (rule r')
+ show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'"
+ by (intro strip, elim conjE) (rule r')
qed
qed
-lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
by (rule classical) iprover
-lemma swap: "~ P ==> (~ R ==> P) ==> R"
+lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
by (rule classical) iprover
@@ -207,11 +215,11 @@
\<close>
-lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
+lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
by blast
-(* Elimination of True from asumptions: *)
-lemma True_implies_equals: "(True ==> PROP P) == PROP P"
+text \<open>Elimination of @{text True} from assumptions:\<close>
+lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
proof
assume "True \<Longrightarrow> PROP P"
from this and TrueI show "PROP P" .
@@ -220,98 +228,108 @@
then show "PROP P" .
qed
-lemma uncurry: "P --> Q --> R ==> P & Q --> R"
+lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
by blast
-lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
+lemma iff_allI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
by blast
-lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
+lemma iff_exI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
by blast
-lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast
+lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
+ by blast
-lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
+lemma ex_comm: "(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
+ by blast
-(*** Classical simplification rules ***)
+subsection \<open>Classical simplification rules\<close>
-(*Avoids duplication of subgoals after expand_if, when the true and false
- cases boil down to the same thing.*)
-lemma cases_simp: "(P --> Q) & (~P --> Q) <-> Q" by blast
+text \<open>
+ Avoids duplication of subgoals after @{text expand_if}, when the true and
+ false cases boil down to the same thing.
+\<close>
+
+lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
+ by blast
-(*** Miniscoping: pushing quantifiers in
- We do NOT distribute of ALL over &, or dually that of EX over |
- Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
- show that this step can increase proof length!
-***)
+subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
+
+text \<open>
+ We do NOT distribute of @{text "\<forall>"} over @{text "\<and>"}, or dually that of
+ @{text "\<exists>"} over @{text "\<or>"}.
-(*existential miniscoping*)
+ Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
+ this step can increase proof length!
+\<close>
+
+text \<open>Existential miniscoping.\<close>
lemma int_ex_simps:
- "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
- "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
- "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
- "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+ "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+ "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+ "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+ "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
by iprover+
-(*classical rules*)
+text \<open>Classical rules.\<close>
lemma cla_ex_simps:
- "!!P Q. (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
- "!!P Q. (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
+ "\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
by blast+
lemmas ex_simps = int_ex_simps cla_ex_simps
-(*universal miniscoping*)
+text \<open>Universal miniscoping.\<close>
lemma int_all_simps:
- "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
- "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
- "!!P Q. (ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q"
- "!!P Q. (ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"
+ "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+ "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+ "\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q"
+ "\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
by iprover+
-(*classical rules*)
+text \<open>Classical rules.\<close>
lemma cla_all_simps:
- "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
- "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+ "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+ "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
by blast+
lemmas all_simps = int_all_simps cla_all_simps
-(*** Named rewrite rules proved for IFOL ***)
+subsubsection \<open>Named rewrite rules proved for IFOL\<close>
-lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
-lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
+lemma imp_disj1: "(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
+lemma imp_disj2: "Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
-lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
+lemma de_Morgan_conj: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)" by blast
-lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
-lemma not_iff: "~(P <-> Q) <-> (P <-> ~Q)" by blast
+lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)" by blast
+lemma not_iff: "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
-lemma not_all: "(~ (ALL x. P(x))) <-> (EX x.~P(x))" by blast
-lemma imp_all: "((ALL x. P(x)) --> Q) <-> (EX x. P(x) --> Q)" by blast
+lemma not_all: "(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))" by blast
+lemma imp_all: "((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)" by blast
lemmas meta_simps =
- triv_forall_equality (* prunes params *)
- True_implies_equals (* prune asms `True' *)
+ triv_forall_equality -- \<open>prunes params\<close>
+ True_implies_equals -- \<open>prune asms @{text True}\<close>
lemmas IFOL_simps =
refl [THEN P_iff_T] conj_simps disj_simps not_simps
imp_simps iff_simps quant_simps
-lemma notFalseI: "~False" by iprover
+lemma notFalseI: "\<not> False" by iprover
lemma cla_simps_misc:
- "~(P&Q) <-> ~P | ~Q"
- "P | ~P"
- "~P | P"
- "~ ~ P <-> P"
- "(~P --> P) <-> P"
- "(~P <-> ~Q) <-> (P<->Q)" by blast+
+ "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
+ "P \<or> \<not> P"
+ "\<not> P \<or> P"
+ "\<not> \<not> P \<longleftrightarrow> P"
+ "(\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+ "(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)" by blast+
lemmas cla_simps =
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
@@ -320,8 +338,8 @@
ML_file "simpdata.ML"
-simproc_setup defined_Ex ("EX x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
-simproc_setup defined_All ("ALL x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
+simproc_setup defined_Ex ("\<exists>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
+simproc_setup defined_All ("\<forall>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
ML \<open>
(*intuitionistic simprules only*)
@@ -349,35 +367,36 @@
subsection \<open>Other simple lemmas\<close>
-lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
-by blast
+lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)"
+ by blast
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
+lemma [simp]: "((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))"
+ by blast
-lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
-by blast
+lemma not_disj_iff_imp: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+ by blast
+
-(** Monotonicity of implications **)
+subsubsection \<open>Monotonicity of implications\<close>
-lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma conj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
+ by fast (*or (IntPr.fast_tac 1)*)
-lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma disj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
+ by fast (*or (IntPr.fast_tac 1)*)
-lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
+lemma imp_mono: "\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
+ by fast (*or (IntPr.fast_tac 1)*)
-lemma imp_refl: "P-->P"
-by (rule impI, assumption)
+lemma imp_refl: "P \<longrightarrow> P"
+ by (rule impI)
-(*The quantifier monotonicity rules are also intuitionistically valid*)
-lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))"
-by blast
+text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
+lemma ex_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
+ by blast
-lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
-by blast
+lemma all_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))"
+ by blast
subsection \<open>Proof by cases and induction\<close>