src/HOL/Isar_Examples/Basic_Logic.thy

 text {* In order to get a first idea of how Isabelle/Isar proof
   documents may look like, we consider the propositions @{text I},
   @{text K}, and @{text S}.  The following (rather explicit) proofs
   should require little extra explanations. *}
 
-lemma I: "A --> A"
+lemma I: "A \<longrightarrow> A"
 proof
   assume A
   show A by fact
 qed
 
-lemma K: "A --> B --> A"
+lemma K: "A \<longrightarrow> B \<longrightarrow> A"
 proof
   assume A
-  show "B --> A"
+  show "B \<longrightarrow> A"
   proof
     show A by fact
   qed
 qed
 
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
-proof
-  assume "A --> B --> C"
-  show "(A --> B) --> A --> C"
-  proof
-    assume "A --> B"
-    show "A --> C"
+lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
+proof
+  assume "A \<longrightarrow> B \<longrightarrow> C"
+  show "(A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C"
+  proof
+    assume "A \<longrightarrow> B"
+    show "A \<longrightarrow> C"
     proof
       assume A
       show C
       proof (rule mp)
-        show "B --> C" by (rule mp) fact+
+        show "B \<longrightarrow> C" by (rule mp) fact+
         show B by (rule mp) fact+
       qed
     qed
   qed
 qed

   yet.
 
   First of all, proof by assumption may be abbreviated as a single
   dot. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
 proof
   assume A
   show A by fact+
 qed
 

   any remaining goals by assumption\footnote{This is not a completely
   trivial operation, as proof by assumption may involve full
   higher-order unification.}.  Thus we may skip the rather vacuous
   body of the above proof as well. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
 proof
 qed
 
 text {* Note that the \isacommand{proof} command refers to the @{text
   rule} method (without arguments) by default.  Thus it implicitly
   applies a single rule, as determined from the syntactic form of the
   statements involved.  The \isacommand{by} command abbreviates any
   proof with empty body, so the proof may be further pruned. *}
 
-lemma "A --> A"
+lemma "A \<longrightarrow> A"
   by rule
 
 text {* Proof by a single rule may be abbreviated as double-dot. *}
 
-lemma "A --> A" ..
+lemma "A \<longrightarrow> A" ..
 
 text {* Thus we have arrived at an adequate representation of the
   proof of a tautology that holds by a single standard
   rule.\footnote{Apparently, the rule here is implication
   introduction.} *}

 
   The @{text intro} proof method repeatedly decomposes a goal's
   conclusion.\footnote{The dual method is @{text elim}, acting on a
   goal's premises.} *}
 
-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
 proof (intro impI)
   assume A
   show A by fact
 qed
 
 text {* Again, the body may be collapsed. *}
 
-lemma "A --> B --> A"
+lemma "A \<longrightarrow> B \<longrightarrow> A"
   by (intro impI)
 
 text {* Just like @{text rule}, the @{text intro} and @{text elim}
   proof methods pick standard structural rules, in case no explicit
   arguments are given.  While implicit rules are usually just fine for

   reasoning as a first-class concept.  In order to demonstrate the
   difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
 
   The first version is purely backward. *}
 
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  show "B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  show "B \<and> A"
   proof
     show B by (rule conjunct2) fact
     show A by (rule conjunct1) fact
   qed
 qed

   \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
   current facts, enabling the use of double-dot proofs.  Note that
   \isacommand{from} already does forward-chaining, involving the
   @{text conjE} rule here. *}
 
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  show "B & A"
-  proof
-    from `A & B` show B ..
-    from `A & B` show A ..
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  show "B \<and> A"
+  proof
+    from `A \<and> B` show B ..
+    from `A \<and> B` show A ..
   qed
 qed
 
 text {* In the next version, we move the forward step one level
   upwards.  Forward-chaining from the most recent facts is indicated

   from @{text "A \<and> B"} actually becomes an elimination, rather than an
   introduction.  The resulting proof structure directly corresponds to
   that of the @{text conjE} rule, including the repeated goal
   proposition that is abbreviated as @{text ?thesis} below. *}
 
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  then show "B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
     assume B A
     then show ?thesis ..   -- {* rule @{text conjI} of @{text "B \<and> A"} *}
   qed
 qed
 
 text {* In the subsequent version we flatten the structure of the main
   body by doing forward reasoning all the time.  Only the outermost
   decomposition step is left as backward. *}
 
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  from `A & B` have A ..
-  from `A & B` have B ..
-  from `B` `A` show "B & A" ..
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  from `A \<and> B` have A ..
+  from `A \<and> B` have B ..
+  from `B` `A` show "B \<and> A" ..
 qed
 
 text {* We can still push forward-reasoning a bit further, even at the
   risk of getting ridiculous.  Note that we force the initial proof
   step to do nothing here, by referring to the ``-'' proof method. *}
 
-lemma "A & B --> B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof -
   {
-    assume "A & B"
-    from `A & B` have A ..
-    from `A & B` have B ..
-    from `B` `A` have "B & A" ..
+    assume "A \<and> B"
+    from `A \<and> B` have A ..
+    from `A \<and> B` have B ..
+    from `B` `A` have "B \<and> A" ..
   }
   then show ?thesis ..         -- {* rule @{text impI} *}
 qed
 
 text {* \medskip With these examples we have shifted through a whole

 
 text {* For our example the most appropriate way of reasoning is
   probably the middle one, with conjunction introduction done after
   elimination. *}
 
-lemma "A & B --> B & A"
-proof
-  assume "A & B"
-  then show "B & A"
+lemma "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof
     assume B A
     then show ?thesis ..
   qed
 qed

 
 text {* We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof
   below involves forward-chaining from @{text "P \<or> P"}, followed by an
   explicit case-analysis on the two \emph{identical} cases. *}
 
-lemma "P | P --> P"
-proof
-  assume "P | P"
+lemma "P \<or> P \<longrightarrow> P"
+proof
+  assume "P \<or> P"
   then show P
   proof                    -- {*
     rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   *}
     assume P show P by fact

 
   \medskip In our example the situation is even simpler, since the two
   cases actually coincide.  Consequently the proof may be rephrased as
   follows. *}
 
-lemma "P | P --> P"
-proof
-  assume "P | P"
+lemma "P \<or> P --> P"
+proof
+  assume "P \<or> P"
   then show P
   proof
     assume P
     show P by fact
     show P by fact

 text {* Again, the rather vacuous body of the proof may be collapsed.
   Thus the case analysis degenerates into two assumption steps, which
   are implicitly performed when concluding the single rule step of the
   double-dot proof as follows. *}
 
-lemma "P | P --> P"
-proof
-  assume "P | P"
+lemma "P \<or> P --> P"
+proof
+  assume "P \<or> P"
   then show P ..
 qed
 
 
 subsubsection {* A quantifier proof *}

   instantiation.  Furthermore, we encounter two new language elements:
   the \isacommand{fix} command augments the context by some new
   ``arbitrary, but fixed'' element; the \isacommand{is} annotation
   binds term abbreviations by higher-order pattern matching. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
+proof
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
   proof (rule exE)             -- {*
     rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   *}
     fix a
     assume "P (f a)" (is "P ?witness")

   redundant.  Above, the basic proof outline gives already enough
   structural clues for the system to infer both the rules and their
   instances (by higher-order unification).  Thus we may as well prune
   the text as follows. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
-  then show "EX y. P y"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
+proof
+  assume "\<exists>x. P (f x)"
+  then show "\<exists>y. P y"
   proof
     fix a
     assume "P (f a)"
     then show ?thesis ..
   qed

 text {* Explicit @{text \<exists>}-elimination as seen above can become quite
   cumbersome in practice.  The derived Isar language element
   ``\isakeyword{obtain}'' provides a more handsome way to do
   generalized existence reasoning. *}
 
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
-  assume "EX x. P (f x)"
+lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
+proof
+  assume "\<exists>x. P (f x)"
   then obtain a where "P (f a)" ..
-  then show "EX y. P y" ..
+  then show "\<exists>y. P y" ..
 qed
 
 text {* Technically, \isakeyword{obtain} is similar to
   \isakeyword{fix} and \isakeyword{assume} together with a soundness
   proof of the elimination involved.  Thus it behaves similar to any

 text {* We derive the conjunction elimination rule from the
   corresponding projections.  The proof is quite straight-forward,
   since Isabelle/Isar supports non-atomic goals and assumptions fully
   transparently. *}
 
-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
+theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
 proof -
-  assume "A & B"
-  assume r: "A ==> B ==> C"
+  assume "A \<and> B"
+  assume r: "A \<Longrightarrow> B \<Longrightarrow> C"
   show C
   proof (rule r)
     show A by (rule conjunct1) fact
     show B by (rule conjunct2) fact
   qed