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
wenzelm@58889
     1
section{*Examples of Classical Reasoning*}
paulson@14152
     2
wenzelm@66453
     3
theory FOL_examples imports 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