src/Doc/Logics_ZF/FOL_examples.thy

minor performance tuning: more direct Bytes with Symbol.encode;

section\<open>Examples of Classical Reasoning\<close>

theory FOL_examples imports FOL begin

lemma "EX y. ALL x. P(y)-->P(x)"
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule exCI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule allI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule allE)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
txt\<open>see below for \<open>allI\<close> combined with \<open>swap\<close>\<close>
apply (erule allI [THEN [2] swap])
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule notE)
  \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done

text \<open>
@{thm[display] allI [THEN [2] swap]}
\<close>

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

end