Theory FOL_examples

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