|
paulson@14152
|
1 |
header{*Examples of Classical Reasoning*}
|
|
paulson@14152
|
2 |
|
|
haftmann@16417
|
3 |
theory FOL_examples imports FOL begin
|
|
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 |
|