src/FOL/FOL.thy

 
 
 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>
 
 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)
   apply (erule r1)
   done
 
 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>
   Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
     (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
 \<close> "case_tac emulation (dynamic instantiation!)"
 
 
-(*** Special elimination rules *)
-
-
-(*Classical implies (-->) elimination. *)
+subsection \<open>Special elimination rules\<close>
+
+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)
   apply (rule r2)
   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)
   apply (rule r1)
   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 ***)
-
-(*Classical <-> elimination.  Proof substitutes P=Q in
-    ~P ==> ~Q    and    P ==> Q  *)
+
+subsubsection \<open>Tactics for implication and contradiction\<close>
+
+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)
      apply (erule (1) r2)
     apply (erule (1) notE)+

   done
 
 
 (*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)
   fix x
   assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
   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
 
 
 section \<open>Classical Reasoner\<close>
 

   );
   val blast_tac = Blast.blast_tac;
 \<close>
 
 
-lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
-  by blast
-
-(* Elimination of True from asumptions: *)
-lemma True_implies_equals: "(True ==> PROP P) == PROP P"
+lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
+  by blast
+
+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" .
 next
   assume "PROP P"
   then show "PROP P" .
 qed
 
-lemma uncurry: "P --> Q --> R ==> P & Q --> R"
-  by blast
-
-lemma iff_allI: "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
-  by blast
-
-lemma iff_exI: "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
-  by blast
-
-lemma all_comm: "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))" by blast
-
-lemma ex_comm: "(EX x y. P(x,y)) <-> (EX y x. P(x,y))" by blast
-
-
-
-(*** Classical simplification rules ***)
-
-(*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
-
-
-(*** 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!
-***)
-
-(*existential miniscoping*)
+lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
+  by blast
+
+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: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
+  by blast
+
+lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>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
+
+
+
+subsection \<open>Classical simplification rules\<close>
+
+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
+
+
+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>"}.
+
+  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 ***)
-
-lemma imp_disj1: "(P-->Q) | R <-> (P-->Q | R)" by blast
-lemma imp_disj2: "Q | (P-->R) <-> (P-->Q | R)" by blast
-
-lemma de_Morgan_conj: "(~(P & Q)) <-> (~P | ~Q)" by blast
-
-lemma not_imp: "~(P --> Q) <-> (P & ~Q)" by blast
-lemma not_iff: "~(P <-> Q) <-> (P <-> ~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
+subsubsection \<open>Named rewrite rules proved for IFOL\<close>
+
+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: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> 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: "(\<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
   not_imp not_all not_ex cases_simp cla_simps_misc
 
 
 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*)
 val IFOL_ss =
   put_simpset FOL_basic_ss @{context}

 ML_file "~~/src/Tools/eqsubst.ML"
 
 
 subsection \<open>Other simple lemmas\<close>
 
-lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
-by blast
-
-lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
-by blast
-
-lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
-by blast
-
-(** Monotonicity of implications **)
-
-lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&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 imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
-by fast (*or (IntPr.fast_tac 1)*)
-
-lemma imp_refl: "P-->P"
-by (rule impI, assumption)
-
-(*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
-
-lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
-by blast
+lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> 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: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
+  by blast
+
+
+subsubsection \<open>Monotonicity of implications\<close>
+
+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: "\<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: "\<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 \<longrightarrow> P"
+  by (rule impI)
+
+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: "(\<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>
 
 text \<open>Proper handling of non-atomic rule statements.\<close>