equal
deleted
inserted
replaced
|
1 header{*Examples of Classical Reasoning*} |
|
2 |
|
3 theory FOL_examples imports "~~/src/FOL/FOL" begin |
|
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 |