header{*Examples of Classical Reasoning*}

 theory FOL_examples imports FOL begin

 lemma "EX y. ALL x. P(y)-->P(x)"

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule exCI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule allI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule impI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule allE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 txt{*see below for @{text allI} combined with @{text swap}*}

 apply (erule allI [THEN [2] swap])

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (rule impI)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply (erule notE)

   --{* @{subgoals[display,indent=0,margin=65]} *}

 apply assumption

 done

 text {*

 @{thm[display] allI [THEN [2] swap]}

 *}

 lemma "EX y. ALL x. P(y)-->P(x)"

 by blast

 end