1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/ZF/FOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +header{*Examples of Classical Reasoning*}
     1.5 +
     1.6 +theory FOL_examples = FOL:
     1.7 +
     1.8 +lemma "EX y. ALL x. P(y)-->P(x)"
     1.9 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.10 +apply (rule exCI)
    1.11 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.12 +apply (rule allI)
    1.13 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.14 +apply (rule impI)
    1.15 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.16 +apply (erule allE)
    1.17 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.18 +txt{*see below for @{text allI} combined with @{text swap}*}
    1.19 +apply (erule allI [THEN [2] swap])
    1.20 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.21 +apply (rule impI)
    1.22 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.23 +apply (erule notE)
    1.24 +  --{* @{subgoals[display,indent=0,margin=65]} *}
    1.25 +apply assumption
    1.26 +done
    1.27 +
    1.28 +text {*
    1.29 +@{thm[display] allI [THEN [2] swap]}
    1.30 +*}
    1.31 +
    1.32 +lemma "EX y. ALL x. P(y)-->P(x)"
    1.33 +by blast
    1.34 +
    1.35 +end
    1.36 +
    1.37 +