doc-src/ZF/FOL_examples.thy
author kleing
Mon, 29 Dec 2003 06:49:26 +0100
changeset 14333 14f29eb097a3
parent 14152 12f6f18e7afc
child 16417 9bc16273c2d4
permissions -rw-r--r--
\<^bsub> .. \<^esub>
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14152
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     1
header{*Examples of Classical Reasoning*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     2
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     3
theory FOL_examples = FOL:
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     4
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     5
lemma "EX y. ALL x. P(y)-->P(x)"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     6
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     7
apply (rule exCI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     8
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
     9
apply (rule allI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    10
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    11
apply (rule impI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    12
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    13
apply (erule allE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    14
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    15
txt{*see below for @{text allI} combined with @{text swap}*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    16
apply (erule allI [THEN [2] swap])
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    17
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    18
apply (rule impI)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    19
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    20
apply (erule notE)
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    21
  --{* @{subgoals[display,indent=0,margin=65]} *}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    22
apply assumption
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    23
done
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    24
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    25
text {*
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    26
@{thm[display] allI [THEN [2] swap]}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    27
*}
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    28
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    29
lemma "EX y. ALL x. P(y)-->P(x)"
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    30
by blast
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    31
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    32
end
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    33
12f6f18e7afc For the Isar version of the ZF logics manual
paulson
parents:
diff changeset
    34