src/Doc/Logics_ZF/FOL_examples.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 56451 856492b0f755
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@58889
     1
section{*Examples of Classical Reasoning*}
paulson@14152
     2
wenzelm@48517
     3
theory FOL_examples imports "~~/src/FOL/FOL" begin
paulson@14152
     4
paulson@14152
     5
lemma "EX y. ALL x. P(y)-->P(x)"
paulson@14152
     6
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
     7
apply (rule exCI)
paulson@14152
     8
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
     9
apply (rule allI)
paulson@14152
    10
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    11
apply (rule impI)
paulson@14152
    12
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    13
apply (erule allE)
paulson@14152
    14
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    15
txt{*see below for @{text allI} combined with @{text swap}*}
paulson@14152
    16
apply (erule allI [THEN [2] swap])
paulson@14152
    17
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    18
apply (rule impI)
paulson@14152
    19
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    20
apply (erule notE)
paulson@14152
    21
  --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@14152
    22
apply assumption
paulson@14152
    23
done
paulson@14152
    24
paulson@14152
    25
text {*
paulson@14152
    26
@{thm[display] allI [THEN [2] swap]}
paulson@14152
    27
*}
paulson@14152
    28
paulson@14152
    29
lemma "EX y. ALL x. P(y)-->P(x)"
paulson@14152
    30
by blast
paulson@14152
    31
paulson@14152
    32
end
paulson@14152
    33
paulson@14152
    34