doc-src/ZF/FOL_examples.thy
author paulson
Tue Aug 19 13:53:58 2003 +0200 (2003-08-19)
changeset 14152 12f6f18e7afc
child 16417 9bc16273c2d4
permissions -rw-r--r--
For the Isar version of the ZF logics manual
paulson@14152
     1
header{*Examples of Classical Reasoning*}
paulson@14152
     2
paulson@14152
     3
theory FOL_examples = FOL:
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