src/Doc/Logics_ZF/FOL_examples.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 66453 cc19f7ca2ed6
child 67406 23307fd33906
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 section{*Examples of Classical Reasoning*}
     2 
     3 theory FOL_examples imports FOL begin
     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