more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
--- 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>
--- a/src/FOL/IFOL.thy Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/IFOL.thy Mon Oct 19 20:29:29 2015 +0200
@@ -30,81 +30,85 @@
typedecl o
judgment
- Trueprop :: "o => prop" ("(_)" 5)
+ Trueprop :: "o \<Rightarrow> prop" ("(_)" 5)
subsubsection \<open>Equality\<close>
axiomatization
- eq :: "['a, 'a] => o" (infixl "=" 50)
+ eq :: "['a, 'a] \<Rightarrow> o" (infixl "=" 50)
where
- refl: "a=a" and
- subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
+ refl: "a = a" and
+ subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
subsubsection \<open>Propositional logic\<close>
axiomatization
False :: o and
- conj :: "[o, o] => o" (infixr "&" 35) and
- disj :: "[o, o] => o" (infixr "|" 30) and
- imp :: "[o, o] => o" (infixr "-->" 25)
+ conj :: "[o, o] => o" (infixr "\<and>" 35) and
+ disj :: "[o, o] => o" (infixr "\<or>" 30) and
+ imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
where
- conjI: "[| P; Q |] ==> P&Q" and
- conjunct1: "P&Q ==> P" and
- conjunct2: "P&Q ==> Q" and
+ conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" and
+ conjunct1: "P \<and> Q \<Longrightarrow> P" and
+ conjunct2: "P \<and> Q \<Longrightarrow> Q" and
- disjI1: "P ==> P|Q" and
- disjI2: "Q ==> P|Q" and
- disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and
+ disjI1: "P \<Longrightarrow> P \<or> Q" and
+ disjI2: "Q \<Longrightarrow> P \<or> Q" and
+ disjE: "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" and
- impI: "(P ==> Q) ==> P-->Q" and
- mp: "[| P-->Q; P |] ==> Q" and
+ impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and
+ mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and
- FalseE: "False ==> P"
+ FalseE: "False \<Longrightarrow> P"
subsubsection \<open>Quantifiers\<close>
axiomatization
- All :: "('a => o) => o" (binder "ALL " 10) and
- Ex :: "('a => o) => o" (binder "EX " 10)
+ All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) and
+ Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
where
- allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
- spec: "(ALL x. P(x)) ==> P(x)" and
- exI: "P(x) ==> (EX x. P(x))" and
- exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
+ allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and
+ spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and
+ exI: "P(x) \<Longrightarrow> (\<exists>x. P(x))" and
+ exE: "\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
subsubsection \<open>Definitions\<close>
-definition "True == False-->False"
-definition Not ("~ _" [40] 40) where not_def: "~P == P-->False"
-definition iff (infixr "<->" 25) where "P<->Q == (P-->Q) & (Q-->P)"
+definition "True \<equiv> False \<longrightarrow> False"
+
+definition Not ("\<not> _" [40] 40)
+ where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
-definition Ex1 :: "('a => o) => o" (binder "EX! " 10)
- where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+definition iff (infixr "\<longleftrightarrow>" 25)
+ where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
+
+definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>!" 10)
+ where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)"
axiomatization where -- \<open>Reflection, admissible\<close>
- eq_reflection: "(x=y) ==> (x==y)" and
- iff_reflection: "(P<->Q) ==> (P==Q)"
+ eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and
+ iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)"
+
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> o" (infixl "\<noteq>" 50)
+ where "x \<noteq> y \<equiv> \<not> (x = y)"
-subsubsection \<open>Additional notation\<close>
-
-abbreviation not_equal :: "['a, 'a] => o" (infixl "~=" 50)
- where "x ~= y == ~ (x = y)"
+subsubsection \<open>Old-style ASCII syntax\<close>
-notation (xsymbols)
- not_equal (infixl "\<noteq>" 50) and
- Not ("\<not> _" [40] 40) and
- conj (infixr "\<and>" 35) and
- disj (infixr "\<or>" 30) and
- All (binder "\<forall>" 10) and
- Ex (binder "\<exists>" 10) and
- Ex1 (binder "\<exists>!" 10) and
- imp (infixr "\<longrightarrow>" 25) and
- iff (infixr "\<longleftrightarrow>" 25)
+notation (ASCII)
+ not_equal (infixl "~=" 50) and
+ Not ("~ _" [40] 40) and
+ conj (infixr "&" 35) and
+ disj (infixr "|" 30) and
+ All (binder "ALL " 10) and
+ Ex (binder "EX " 10) and
+ Ex1 (binder "EX! " 10) and
+ imp (infixr "-->" 25) and
+ iff (infixr "<->" 25)
subsection \<open>Lemmas and proof tools\<close>
@@ -115,11 +119,11 @@
unfolding True_def by (rule impI)
-(*** Sequent-style elimination rules for & --> and ALL ***)
+subsubsection \<open>Sequent-style elimination rules for @{text "\<and>"} @{text "\<longrightarrow>"} and @{text "\<forall>"}\<close>
lemma conjE:
- assumes major: "P & Q"
- and r: "[| P; Q |] ==> R"
+ assumes major: "P \<and> Q"
+ and r: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
shows R
apply (rule r)
apply (rule major [THEN conjunct1])
@@ -127,9 +131,9 @@
done
lemma impE:
- assumes major: "P --> Q"
+ assumes major: "P \<longrightarrow> Q"
and P
- and r: "Q ==> R"
+ and r: "Q \<Longrightarrow> R"
shows R
apply (rule r)
apply (rule major [THEN mp])
@@ -137,17 +141,17 @@
done
lemma allE:
- assumes major: "ALL x. P(x)"
- and r: "P(x) ==> R"
+ assumes major: "\<forall>x. P(x)"
+ and r: "P(x) \<Longrightarrow> R"
shows R
apply (rule r)
apply (rule major [THEN spec])
done
-(*Duplicates the quantifier; for use with eresolve_tac*)
+text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close>
lemma all_dupE:
- assumes major: "ALL x. P(x)"
- and r: "[| P(x); ALL x. P(x) |] ==> R"
+ assumes major: "\<forall>x. P(x)"
+ and r: "\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R"
shows R
apply (rule r)
apply (rule major [THEN spec])
@@ -155,64 +159,71 @@
done
-(*** Negation rules, which translate between ~P and P-->False ***)
+subsubsection \<open>Negation rules, which translate between @{text "\<not> P"} and @{text "P \<longrightarrow> False"}\<close>
-lemma notI: "(P ==> False) ==> ~P"
+lemma notI: "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P"
unfolding not_def by (erule impI)
-lemma notE: "[| ~P; P |] ==> R"
+lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R"
unfolding not_def by (erule mp [THEN FalseE])
-lemma rev_notE: "[| P; ~P |] ==> R"
+lemma rev_notE: "\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R"
by (erule notE)
-(*This is useful with the special implication rules for each kind of P. *)
+text \<open>This is useful with the special implication rules for each kind of @{text P}.\<close>
lemma not_to_imp:
- assumes "~P"
- and r: "P --> False ==> Q"
+ assumes "\<not> P"
+ and r: "P \<longrightarrow> False \<Longrightarrow> Q"
shows Q
apply (rule r)
apply (rule impI)
- apply (erule notE [OF \<open>~P\<close>])
+ apply (erule notE [OF \<open>\<not> P\<close>])
done
-(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
- this implication, then apply impI to move P back into the assumptions.*)
-lemma rev_mp: "[| P; P --> Q |] ==> Q"
+text \<open>
+ For substitution into an assumption @{text P}, reduce @{text Q} to @{text
+ "P \<longrightarrow> Q"}, substitute into this implication, then apply @{text impI} to
+ move @{text P} back into the assumptions.
+\<close>
+lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (erule mp)
-(*Contrapositive of an inference rule*)
+text \<open>Contrapositive of an inference rule.\<close>
lemma contrapos:
- assumes major: "~Q"
- and minor: "P ==> Q"
- shows "~P"
+ assumes major: "\<not> Q"
+ and minor: "P \<Longrightarrow> Q"
+ shows "\<not> P"
apply (rule major [THEN notE, THEN notI])
apply (erule minor)
done
-(*** Modus Ponens Tactics ***)
+subsubsection \<open>Modus Ponens Tactics\<close>
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+text \<open>
+ Finds @{text "P \<longrightarrow> Q"} and P in the assumptions, replaces implication by
+ @{text Q}.
+\<close>
ML \<open>
- fun mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i
- fun eq_mp_tac ctxt i = eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i
+ fun mp_tac ctxt i =
+ eresolve_tac ctxt @{thms notE impE} i THEN assume_tac ctxt i;
+ fun eq_mp_tac ctxt i =
+ eresolve_tac ctxt @{thms notE impE} i THEN eq_assume_tac i;
\<close>
-(*** If-and-only-if ***)
+subsection \<open>If-and-only-if\<close>
-lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q"
+lemma iffI: "\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q"
apply (unfold iff_def)
apply (rule conjI)
apply (erule impI)
apply (erule impI)
done
-
lemma iffE:
- assumes major: "P <-> Q"
- and r: "P-->Q ==> Q-->P ==> R"
+ assumes major: "P \<longleftrightarrow> Q"
+ and r: "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R"
shows R
apply (insert major, unfold iff_def)
apply (erule conjE)
@@ -220,236 +231,250 @@
apply assumption
done
-(* Destruct rules for <-> similar to Modus Ponens *)
-lemma iffD1: "[| P <-> Q; P |] ==> Q"
+subsubsection \<open>Destruct rules for @{text "\<longleftrightarrow>"} similar to Modus Ponens\<close>
+
+lemma iffD1: "\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q"
apply (unfold iff_def)
apply (erule conjunct1 [THEN mp])
apply assumption
done
-lemma iffD2: "[| P <-> Q; Q |] ==> P"
+lemma iffD2: "\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P"
apply (unfold iff_def)
apply (erule conjunct2 [THEN mp])
apply assumption
done
-lemma rev_iffD1: "[| P; P <-> Q |] ==> Q"
+lemma rev_iffD1: "\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
apply (erule iffD1)
apply assumption
done
-lemma rev_iffD2: "[| Q; P <-> Q |] ==> P"
+lemma rev_iffD2: "\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P"
apply (erule iffD2)
apply assumption
done
-lemma iff_refl: "P <-> P"
+lemma iff_refl: "P \<longleftrightarrow> P"
by (rule iffI)
-lemma iff_sym: "Q <-> P ==> P <-> Q"
+lemma iff_sym: "Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q"
apply (erule iffE)
apply (rule iffI)
apply (assumption | erule mp)+
done
-lemma iff_trans: "[| P <-> Q; Q<-> R |] ==> P <-> R"
+lemma iff_trans: "\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R"
apply (rule iffI)
apply (assumption | erule iffE | erule (1) notE impE)+
done
-(*** Unique existence. NOTE THAT the following 2 quantifications
- EX!x such that [EX!y such that P(x,y)] (sequential)
- EX!x,y such that P(x,y) (simultaneous)
- do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
-***)
+subsection \<open>Unique existence\<close>
+
+text \<open>
+ NOTE THAT the following 2 quantifications:
-lemma ex1I:
- "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
+ \<^item> EX!x such that [EX!y such that P(x,y)] (sequential)
+ \<^item> EX!x,y such that P(x,y) (simultaneous)
+
+ do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
+\<close>
+
+lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"
apply (unfold ex1_def)
apply (assumption | rule exI conjI allI impI)+
done
-(*Sometimes easier to use: the premises have no shared variables. Safe!*)
-lemma ex_ex1I:
- "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
+text \<open>Sometimes easier to use: the premises have no shared variables. Safe!\<close>
+lemma ex_ex1I: "\<exists>x. P(x) \<Longrightarrow> (\<And>x y. \<lbrakk>P(x); P(y)\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> \<exists>!x. P(x)"
apply (erule exE)
apply (rule ex1I)
apply assumption
apply assumption
done
-lemma ex1E:
- "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x); ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
+lemma ex1E: "\<exists>! x. P(x) \<Longrightarrow> (\<And>x. \<lbrakk>P(x); \<forall>y. P(y) \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
apply (unfold ex1_def)
apply (assumption | erule exE conjE)+
done
-(*** <-> congruence rules for simplification ***)
+subsubsection \<open>@{text "\<longleftrightarrow>"} congruence rules for simplification\<close>
-(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*)
+text \<open>Use @{text iffE} on a premise. For @{text conj_cong}, @{text
+ imp_cong}, @{text all_cong}, @{text ex_cong}.\<close>
ML \<open>
fun iff_tac ctxt prems i =
resolve_tac ctxt (prems RL @{thms iffE}) i THEN
- REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i)
+ REPEAT1 (eresolve_tac ctxt @{thms asm_rl mp} i);
\<close>
method_setup iff =
- \<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
+ \<open>Attrib.thms >>
+ (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close>
lemma conj_cong:
- assumes "P <-> P'"
- and "P' ==> Q <-> Q'"
- shows "(P&Q) <-> (P'&Q')"
+ assumes "P \<longleftrightarrow> P'"
+ and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+ shows "(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
apply (insert assms)
apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
done
-(*Reversed congruence rule! Used in ZF/Order*)
+text \<open>Reversed congruence rule! Used in ZF/Order.\<close>
lemma conj_cong2:
- assumes "P <-> P'"
- and "P' ==> Q <-> Q'"
- shows "(Q&P) <-> (Q'&P')"
+ assumes "P \<longleftrightarrow> P'"
+ and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+ shows "(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')"
apply (insert assms)
apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+
done
lemma disj_cong:
- assumes "P <-> P'" and "Q <-> Q'"
- shows "(P|Q) <-> (P'|Q')"
+ assumes "P \<longleftrightarrow> P'" and "Q \<longleftrightarrow> Q'"
+ shows "(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')"
apply (insert assms)
- apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+
+ apply (erule iffE disjE disjI1 disjI2 |
+ assumption | rule iffI | erule (1) notE impE)+
done
lemma imp_cong:
- assumes "P <-> P'"
- and "P' ==> Q <-> Q'"
- shows "(P-->Q) <-> (P'-->Q')"
+ assumes "P \<longleftrightarrow> P'"
+ and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'"
+ shows "(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
apply (insert assms)
apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+
done
-lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
+lemma iff_cong: "\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')"
apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
done
-lemma not_cong: "P <-> P' ==> ~P <-> ~P'"
+lemma not_cong: "P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'"
apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
done
lemma all_cong:
- assumes "!!x. P(x) <-> Q(x)"
- shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
+ assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+ shows "(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+
done
lemma ex_cong:
- assumes "!!x. P(x) <-> Q(x)"
- shows "(EX x. P(x)) <-> (EX x. Q(x))"
+ assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+ shows "(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+
done
lemma ex1_cong:
- assumes "!!x. P(x) <-> Q(x)"
- shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
+ assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)"
+ shows "(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))"
apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+
done
-(*** Equality rules ***)
-lemma sym: "a=b ==> b=a"
+subsection \<open>Equality rules\<close>
+
+lemma sym: "a = b \<Longrightarrow> b = a"
apply (erule subst)
apply (rule refl)
done
-lemma trans: "[| a=b; b=c |] ==> a=c"
+lemma trans: "\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c"
apply (erule subst, assumption)
done
-(** **)
-lemma not_sym: "b ~= a ==> a ~= b"
+lemma not_sym: "b \<noteq> a \<Longrightarrow> a \<noteq> b"
apply (erule contrapos)
apply (erule sym)
done
-
-(* Two theorms for rewriting only one instance of a definition:
- the first for definitions of formulae and the second for terms *)
-lemma def_imp_iff: "(A == B) ==> A <-> B"
+text \<open>
+ Two theorems for rewriting only one instance of a definition:
+ the first for definitions of formulae and the second for terms.
+\<close>
+
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B"
apply unfold
apply (rule iff_refl)
done
-lemma meta_eq_to_obj_eq: "(A == B) ==> A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> A = B"
apply unfold
apply (rule refl)
done
-lemma meta_eq_to_iff: "x==y ==> x<->y"
+lemma meta_eq_to_iff: "x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y"
by unfold (rule iff_refl)
-(*substitution*)
-lemma ssubst: "[| b = a; P(a) |] ==> P(b)"
+text \<open>Substitution.\<close>
+lemma ssubst: "\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)"
apply (drule sym)
apply (erule (1) subst)
done
-(*A special case of ex1E that would otherwise need quantifier expansion*)
-lemma ex1_equalsE:
- "[| EX! x. P(x); P(a); P(b) |] ==> a=b"
+text \<open>A special case of @{text ex1E} that would otherwise need quantifier
+ expansion.\<close>
+lemma ex1_equalsE: "\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b"
apply (erule ex1E)
apply (rule trans)
apply (rule_tac [2] sym)
apply (assumption | erule spec [THEN mp])+
done
-(** Polymorphic congruence rules **)
-lemma subst_context: "[| a=b |] ==> t(a)=t(b)"
+subsubsection \<open>Polymorphic congruence rules\<close>
+
+lemma subst_context: "a = b \<Longrightarrow> t(a) = t(b)"
apply (erule ssubst)
apply (rule refl)
done
-lemma subst_context2: "[| a=b; c=d |] ==> t(a,c)=t(b,d)"
+lemma subst_context2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)"
+ apply (erule ssubst)+
+ apply (rule refl)
+ done
+
+lemma subst_context3: "\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)"
apply (erule ssubst)+
apply (rule refl)
done
-lemma subst_context3: "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)"
- apply (erule ssubst)+
- apply (rule refl)
- done
+text \<open>
+ Useful with @{ML eresolve_tac} for proving equalties from known
+ equalities.
-(*Useful with eresolve_tac for proving equalties from known equalities.
a = b
| |
- c = d *)
-lemma box_equals: "[| a=b; a=c; b=d |] ==> c=d"
+ c = d
+\<close>
+lemma box_equals: "\<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> c = d"
apply (rule trans)
apply (rule trans)
apply (rule sym)
apply assumption+
done
-(*Dual of box_equals: for proving equalities backwards*)
-lemma simp_equals: "[| a=c; b=d; c=d |] ==> a=b"
+text \<open>Dual of box_equals: for proving equalities backwards.\<close>
+lemma simp_equals: "\<lbrakk>a = c; b = d; c = d\<rbrakk> \<Longrightarrow> a = b"
apply (rule trans)
apply (rule trans)
apply assumption+
apply (erule sym)
done
-(** Congruence rules for predicate letters **)
-lemma pred1_cong: "a=a' ==> P(a) <-> P(a')"
+subsubsection \<open>Congruence rules for predicate letters\<close>
+
+lemma pred1_cong: "a = a' \<Longrightarrow> P(a) \<longleftrightarrow> P(a')"
apply (rule iffI)
apply (erule (1) subst)
apply (erule (1) ssubst)
done
-lemma pred2_cong: "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')"
+lemma pred2_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> P(a,b) \<longleftrightarrow> P(a',b')"
apply (rule iffI)
apply (erule subst)+
apply assumption
@@ -457,7 +482,7 @@
apply assumption
done
-lemma pred3_cong: "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
+lemma pred3_cong: "\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> P(a,b,c) \<longleftrightarrow> P(a',b',c')"
apply (rule iffI)
apply (erule subst)+
apply assumption
@@ -465,81 +490,85 @@
apply assumption
done
-(*special case for the equality predicate!*)
-lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'"
+text \<open>Special case for the equality predicate!\<close>
+lemma eq_cong: "\<lbrakk>a = a'; b = b'\<rbrakk> \<Longrightarrow> a = b \<longleftrightarrow> a' = b'"
apply (erule (1) pred2_cong)
done
-(*** Simplifications of assumed implications.
- Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
- used with mp_tac (restricted to atomic formulae) is COMPLETE for
- intuitionistic propositional logic. See
- R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
- (preprint, University of St Andrews, 1991) ***)
+subsection \<open>Simplifications of assumed implications\<close>
+
+text \<open>
+ Roy Dyckhoff has proved that @{text conj_impE}, @{text disj_impE}, and
+ @{text imp_impE} used with @{ML mp_tac} (restricted to atomic formulae) is
+ COMPLETE for intuitionistic propositional logic.
+
+ See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
+ (preprint, University of St Andrews, 1991).
+\<close>
lemma conj_impE:
- assumes major: "(P&Q)-->S"
- and r: "P-->(Q-->S) ==> R"
+ assumes major: "(P \<and> Q) \<longrightarrow> S"
+ and r: "P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R"
shows R
by (assumption | rule conjI impI major [THEN mp] r)+
lemma disj_impE:
- assumes major: "(P|Q)-->S"
- and r: "[| P-->S; Q-->S |] ==> R"
+ assumes major: "(P \<or> Q) \<longrightarrow> S"
+ and r: "\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R"
shows R
by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+
-(*Simplifies the implication. Classical version is stronger.
- Still UNSAFE since Q must be provable -- backtracking needed. *)
+text \<open>Simplifies the implication. Classical version is stronger.
+ Still UNSAFE since Q must be provable -- backtracking needed.\<close>
lemma imp_impE:
- assumes major: "(P-->Q)-->S"
- and r1: "[| P; Q-->S |] ==> Q"
- and r2: "S ==> R"
+ assumes major: "(P \<longrightarrow> Q) \<longrightarrow> S"
+ and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q"
+ and r2: "S \<Longrightarrow> R"
shows R
by (assumption | rule impI major [THEN mp] r1 r2)+
-(*Simplifies the implication. Classical version is stronger.
- Still UNSAFE since ~P must be provable -- backtracking needed. *)
-lemma not_impE:
- "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
+text \<open>Simplifies the implication. Classical version is stronger.
+ Still UNSAFE since ~P must be provable -- backtracking needed.\<close>
+lemma not_impE: "\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R"
apply (drule mp)
apply (rule notI)
apply assumption
apply assumption
done
-(*Simplifies the implication. UNSAFE. *)
+text \<open>Simplifies the implication. UNSAFE.\<close>
lemma iff_impE:
- assumes major: "(P<->Q)-->S"
- and r1: "[| P; Q-->S |] ==> Q"
- and r2: "[| Q; P-->S |] ==> P"
- and r3: "S ==> R"
+ assumes major: "(P \<longleftrightarrow> Q) \<longrightarrow> S"
+ and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q"
+ and r2: "\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P"
+ and r3: "S \<Longrightarrow> R"
shows R
apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
done
-(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
+text \<open>What if @{text "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"} is an assumption?
+ UNSAFE.\<close>
lemma all_impE:
- assumes major: "(ALL x. P(x))-->S"
- and r1: "!!x. P(x)"
- and r2: "S ==> R"
+ assumes major: "(\<forall>x. P(x)) \<longrightarrow> S"
+ and r1: "\<And>x. P(x)"
+ and r2: "S \<Longrightarrow> R"
shows R
apply (rule allI impI major [THEN mp] r1 r2)+
done
-(*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *)
+text \<open>
+ Unsafe: @{text "\<exists>x. P(x)) \<longrightarrow> S"} is equivalent
+ to @{text "\<forall>x. P(x) \<longrightarrow> S"}.\<close>
lemma ex_impE:
- assumes major: "(EX x. P(x))-->S"
- and r: "P(x)-->S ==> R"
+ assumes major: "(\<exists>x. P(x)) \<longrightarrow> S"
+ and r: "P(x) \<longrightarrow> S \<Longrightarrow> R"
shows R
apply (assumption | rule exI impI major [THEN mp] r)+
done
-(*** Courtesy of Krzysztof Grabczewski ***)
-
-lemma disj_imp_disj:
- "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
+text \<open>Courtesy of Krzysztof Grabczewski.\<close>
+lemma disj_imp_disj: "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S"
apply (erule disjE)
apply (rule disjI1) apply assumption
apply (rule disjI2) apply assumption
@@ -556,7 +585,7 @@
ML_file "fologic.ML"
-lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
+lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
ML \<open>
structure Hypsubst = Hypsubst
@@ -583,9 +612,9 @@
setup \<open>Intuitionistic.method_setup @{binding iprover}\<close>
lemma impE':
- assumes 1: "P --> Q"
- and 2: "Q ==> R"
- and 3: "P --> Q ==> P"
+ assumes 1: "P \<longrightarrow> Q"
+ and 2: "Q \<Longrightarrow> R"
+ and 3: "P \<longrightarrow> Q \<Longrightarrow> P"
shows R
proof -
from 3 and 1 have P .
@@ -594,8 +623,8 @@
qed
lemma allE':
- assumes 1: "ALL x. P(x)"
- and 2: "P(x) ==> ALL x. P(x) ==> Q"
+ assumes 1: "\<forall>x. P(x)"
+ and 2: "P(x) \<Longrightarrow> \<forall>x. P(x) \<Longrightarrow> Q"
shows Q
proof -
from 1 have "P(x)" by (rule spec)
@@ -603,8 +632,8 @@
qed
lemma notE':
- assumes 1: "~ P"
- and 2: "~ P ==> P"
+ assumes 1: "\<not> P"
+ and 2: "\<not> P \<Longrightarrow> P"
shows R
proof -
from 2 and 1 have P .
@@ -616,70 +645,73 @@
and [Pure.elim 2] = allE notE' impE'
and [Pure.intro] = exI disjI2 disjI1
-setup \<open>Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)\<close>
+setup \<open>
+ Context_Rules.addSWrapper
+ (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac)
+\<close>
-lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
+lemma iff_not_sym: "\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)"
by iprover
lemmas [sym] = sym iff_sym not_sym iff_not_sym
and [Pure.elim?] = iffD1 iffD2 impE
-lemma eq_commute: "a=b <-> b=a"
-apply (rule iffI)
-apply (erule sym)+
-done
+lemma eq_commute: "a = b \<longleftrightarrow> b = a"
+ apply (rule iffI)
+ apply (erule sym)+
+ done
subsection \<open>Atomizing meta-level rules\<close>
-lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
+lemma atomize_all [atomize]: "(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))"
proof
- assume "!!x. P(x)"
- then show "ALL x. P(x)" ..
+ assume "\<And>x. P(x)"
+ then show "\<forall>x. P(x)" ..
next
- assume "ALL x. P(x)"
- then show "!!x. P(x)" ..
+ assume "\<forall>x. P(x)"
+ then show "\<And>x. P(x)" ..
qed
-lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
+lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)"
proof
- assume "A ==> B"
- then show "A --> B" ..
+ assume "A \<Longrightarrow> B"
+ then show "A \<longrightarrow> B" ..
next
- assume "A --> B" and A
+ assume "A \<longrightarrow> B" and A
then show B by (rule mp)
qed
-lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
+lemma atomize_eq [atomize]: "(x \<equiv> y) \<equiv> Trueprop (x = y)"
proof
- assume "x == y"
- show "x = y" unfolding \<open>x == y\<close> by (rule refl)
+ assume "x \<equiv> y"
+ show "x = y" unfolding \<open>x \<equiv> y\<close> by (rule refl)
next
assume "x = y"
- then show "x == y" by (rule eq_reflection)
+ then show "x \<equiv> y" by (rule eq_reflection)
qed
-lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
+lemma atomize_iff [atomize]: "(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)"
proof
- assume "A == B"
- show "A <-> B" unfolding \<open>A == B\<close> by (rule iff_refl)
+ assume "A \<equiv> B"
+ show "A \<longleftrightarrow> B" unfolding \<open>A \<equiv> B\<close> by (rule iff_refl)
next
- assume "A <-> B"
- then show "A == B" by (rule iff_reflection)
+ assume "A \<longleftrightarrow> B"
+ then show "A \<equiv> B" by (rule iff_reflection)
qed
-lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
+lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)"
proof
assume conj: "A &&& B"
- show "A & B"
+ show "A \<and> B"
proof (rule conjI)
from conj show A by (rule conjunctionD1)
from conj show B by (rule conjunctionD2)
qed
next
- assume conj: "A & B"
+ assume conj: "A \<and> B"
show "A &&& B"
proof -
from conj show A ..
@@ -693,24 +725,24 @@
subsection \<open>Atomizing elimination rules\<close>
-lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
+lemma atomize_exL[atomize_elim]: "(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)"
by rule iprover+
-lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
+lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)"
by rule iprover+
-lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
+lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)"
by rule iprover+
-lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
+lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop(A)" ..
subsection \<open>Calculational rules\<close>
-lemma forw_subst: "a = b ==> P(b) ==> P(a)"
+lemma forw_subst: "a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)"
by (rule ssubst)
-lemma back_subst: "P(a) ==> a = b ==> P(b)"
+lemma back_subst: "P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)"
by (rule subst)
text \<open>
@@ -724,12 +756,13 @@
mp
trans
+
subsection \<open>``Let'' declarations\<close>
nonterminal letbinds and letbind
-definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
- "Let(s, f) == f(s)"
+definition Let :: "['a::{}, 'a => 'b] \<Rightarrow> ('b::{})"
+ where "Let(s, f) \<equiv> f(s)"
syntax
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
@@ -739,12 +772,11 @@
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
- "let x = a in e" == "CONST Let(a, %x. e)"
-
+ "let x = a in e" == "CONST Let(a, \<lambda>x. e)"
-lemma LetI:
- assumes "!!x. x=t ==> P(u(x))"
- shows "P(let x=t in u(x))"
+lemma LetI:
+ assumes "\<And>x. x = t \<Longrightarrow> P(u(x))"
+ shows "P(let x = t in u(x))"
apply (unfold Let_def)
apply (rule refl [THEN assms])
done
@@ -753,108 +785,113 @@
subsection \<open>Intuitionistic simplification 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)"
+ "P \<and> True \<longleftrightarrow> P"
+ "True \<and> P \<longleftrightarrow> P"
+ "P \<and> False \<longleftrightarrow> False"
+ "False \<and> P \<longleftrightarrow> False"
+ "P \<and> P \<longleftrightarrow> P"
+ "P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+ "P \<and> \<not> P \<longleftrightarrow> False"
+ "\<not> P \<and> P \<longleftrightarrow> False"
+ "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
by iprover+
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)"
+ "P \<or> True \<longleftrightarrow> True"
+ "True \<or> P \<longleftrightarrow> True"
+ "P \<or> False \<longleftrightarrow> P"
+ "False \<or> P \<longleftrightarrow> P"
+ "P \<or> P \<longleftrightarrow> P"
+ "P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+ "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
by iprover+
lemma not_simps:
- "~(P|Q) <-> ~P & ~Q"
- "~ False <-> True"
- "~ True <-> False"
+ "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
+ "\<not> False \<longleftrightarrow> True"
+ "\<not> True \<longleftrightarrow> False"
by iprover+
lemma imp_simps:
- "(P --> False) <-> ~P"
- "(P --> True) <-> True"
- "(False --> P) <-> True"
- "(True --> P) <-> P"
- "(P --> P) <-> True"
- "(P --> ~P) <-> ~P"
+ "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+ "(P \<longrightarrow> True) \<longleftrightarrow> True"
+ "(False \<longrightarrow> P) \<longleftrightarrow> True"
+ "(True \<longrightarrow> P) \<longleftrightarrow> P"
+ "(P \<longrightarrow> P) \<longleftrightarrow> True"
+ "(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
by iprover+
lemma iff_simps:
- "(True <-> P) <-> P"
- "(P <-> True) <-> P"
- "(P <-> P) <-> True"
- "(False <-> P) <-> ~P"
- "(P <-> False) <-> ~P"
+ "(True \<longleftrightarrow> P) \<longleftrightarrow> P"
+ "(P \<longleftrightarrow> True) \<longleftrightarrow> P"
+ "(P \<longleftrightarrow> P) \<longleftrightarrow> True"
+ "(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+ "(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
by iprover+
-(*The x=t versions are needed for the simplification procedures*)
+text \<open>The @{text "x = t"} versions are needed for the simplification
+ procedures.\<close>
lemma quant_simps:
- "!!P. (ALL x. P) <-> P"
- "(ALL x. x=t --> P(x)) <-> P(t)"
- "(ALL x. t=x --> P(x)) <-> P(t)"
- "!!P. (EX x. P) <-> P"
- "EX x. x=t"
- "EX x. t=x"
- "(EX x. x=t & P(x)) <-> P(t)"
- "(EX x. t=x & P(x)) <-> P(t)"
+ "\<And>P. (\<forall>x. P) \<longleftrightarrow> P"
+ "(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+ "\<And>P. (\<exists>x. P) \<longleftrightarrow> P"
+ "\<exists>x. x = t"
+ "\<exists>x. t = x"
+ "(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+ "(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
by iprover+
-(*These are NOT supplied by default!*)
+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)"
+ "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+ "(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+ "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
by iprover+
-text \<open>Conversion into rewrite rules\<close>
+subsubsection \<open>Conversion into rewrite rules\<close>
-lemma P_iff_F: "~P ==> (P <-> False)" by iprover
-lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection])
+lemma P_iff_F: "\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)"
+ by iprover
+lemma iff_reflection_F: "\<not> P \<Longrightarrow> (P \<equiv> False)"
+ by (rule P_iff_F [THEN iff_reflection])
-lemma P_iff_T: "P ==> (P <-> True)" by iprover
-lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection])
+lemma P_iff_T: "P \<Longrightarrow> (P \<longleftrightarrow> True)"
+ by iprover
+lemma iff_reflection_T: "P \<Longrightarrow> (P \<equiv> True)"
+ by (rule P_iff_T [THEN iff_reflection])
-text \<open>More rewrite rules\<close>
+subsubsection \<open>More rewrite rules\<close>
-lemma conj_commute: "P&Q <-> Q&P" by iprover
-lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover
+lemma conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" by iprover
+lemma conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover
lemmas conj_comms = conj_commute conj_left_commute
-lemma disj_commute: "P|Q <-> Q|P" by iprover
-lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover
+lemma disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" by iprover
+lemma disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover
lemmas disj_comms = disj_commute disj_left_commute
-lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover
-lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover
+lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)" by iprover
+lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)" by iprover
-lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover
-lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover
+lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover
+lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover
-lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover
-lemma imp_conj: "((P&Q)-->R) <-> (P --> (Q --> R))" by iprover
-lemma imp_disj: "(P|Q --> R) <-> (P-->R) & (Q-->R)" by iprover
+lemma imp_conj_distrib: "(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" by iprover
+lemma imp_conj: "((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover
+lemma imp_disj: "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" by iprover
-lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover
+lemma de_Morgan_disj: "(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)" by iprover
-lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover
-lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover
+lemma not_ex: "(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))" by iprover
+lemma imp_ex: "((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)" by iprover
-lemma ex_disj_distrib:
- "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover
+lemma ex_disj_distrib: "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))"
+ by iprover
-lemma all_conj_distrib:
- "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
+lemma all_conj_distrib: "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))"
+ by iprover
end
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Oct 19 17:45:36 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Oct 19 20:29:29 2015 +0200
@@ -162,8 +162,8 @@
declare [[show_hyps]]
ML \<open>
- check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
- check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+ check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
+ check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
\<close>
end
@@ -175,8 +175,8 @@
(* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
ML \<open>
- check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
- check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+ check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \<longleftrightarrow> \<not> p2(p3(?x))";
+ check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
\<close>
end