doc-src/ZF/FOL_examples.thy
author nipkow
Wed Aug 04 11:25:08 2004 +0200 (2004-08-04)
changeset 15106 e8cef6993701
parent 14152 12f6f18e7afc
child 16417 9bc16273c2d4
permissions -rw-r--r--
aded comment
     1 header{*Examples of Classical Reasoning*}
     2 
     3 theory FOL_examples = FOL:
     4 
     5 lemma "EX y. ALL x. P(y)-->P(x)"
     6   --{* @{subgoals[display,indent=0,margin=65]} *}
     7 apply (rule exCI)
     8   --{* @{subgoals[display,indent=0,margin=65]} *}
     9 apply (rule allI)
    10   --{* @{subgoals[display,indent=0,margin=65]} *}
    11 apply (rule impI)
    12   --{* @{subgoals[display,indent=0,margin=65]} *}
    13 apply (erule allE)
    14   --{* @{subgoals[display,indent=0,margin=65]} *}
    15 txt{*see below for @{text allI} combined with @{text swap}*}
    16 apply (erule allI [THEN [2] swap])
    17   --{* @{subgoals[display,indent=0,margin=65]} *}
    18 apply (rule impI)
    19   --{* @{subgoals[display,indent=0,margin=65]} *}
    20 apply (erule notE)
    21   --{* @{subgoals[display,indent=0,margin=65]} *}
    22 apply assumption
    23 done
    24 
    25 text {*
    26 @{thm[display] allI [THEN [2] swap]}
    27 *}
    28 
    29 lemma "EX y. ALL x. P(y)-->P(x)"
    30 by blast
    31 
    32 end
    33 
    34