section‹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 ‹allI› combined with ‹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