doc-src/ZF/FOL_examples.thy
author boehmes
Tue, 07 Dec 2010 15:44:38 +0100
changeset 41064 0c447a17770a
parent 16417 9bc16273c2d4
child 48517 0f8c8ac6cc0e
permissions -rw-r--r--
updated SMT certificates
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
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14152
diff changeset
     3
theory FOL_examples imports FOL begin
14152
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