src/Doc/Logics-ZF/FOL_examples.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Logics-ZF/FOL_examples.thy	Sat Apr 05 11:37:00 2014 +0200
@@ -0,0 +1,34 @@
+header{*Examples of Classical Reasoning*}
+
+theory FOL_examples imports "~~/src/FOL/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
+
+