| author | wenzelm |
| Wed, 04 Oct 2017 12:00:53 +0200 | |
| changeset 66787 | 64b47495676d |
| parent 66453 | cc19f7ca2ed6 |
| child 67406 | 23307fd33906 |
| permissions | -rw-r--r-- |
| 58889 | 1 |
section{*Examples of Classical Reasoning*}
|
| 14152 | 2 |
|
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
58889
diff
changeset
|
3 |
theory FOL_examples imports FOL begin |
| 14152 | 4 |
|
5 |
lemma "EX y. ALL x. P(y)-->P(x)" |
|
6 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
7 |
apply (rule exCI) |
|
8 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
9 |
apply (rule allI) |
|
10 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
11 |
apply (rule impI) |
|
12 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
13 |
apply (erule allE) |
|
14 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
15 |
txt{*see below for @{text allI} combined with @{text swap}*}
|
|
16 |
apply (erule allI [THEN [2] swap]) |
|
17 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
18 |
apply (rule impI) |
|
19 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
20 |
apply (erule notE) |
|
21 |
--{* @{subgoals[display,indent=0,margin=65]} *}
|
|
22 |
apply assumption |
|
23 |
done |
|
24 |
||
25 |
text {*
|
|
26 |
@{thm[display] allI [THEN [2] swap]}
|
|
27 |
*} |
|
28 |
||
29 |
lemma "EX y. ALL x. P(y)-->P(x)" |
|
30 |
by blast |
|
31 |
||
32 |
end |
|
33 |
||
34 |