|
1 header{*Examples of Intuitionistic Reasoning*} |
|
2 |
|
3 theory IFOL_examples imports "~~/src/FOL/IFOL" begin |
|
4 |
|
5 text{*Quantifier example from the book Logic and Computation*} |
|
6 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
|
7 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
8 apply (rule impI) |
|
9 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
10 apply (rule allI) |
|
11 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
12 apply (rule exI) |
|
13 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
14 apply (erule exE) |
|
15 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
16 apply (erule allE) |
|
17 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
18 txt{*Now @{text "apply assumption"} fails*} |
|
19 oops |
|
20 |
|
21 text{*Trying again, with the same first two steps*} |
|
22 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
|
23 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
24 apply (rule impI) |
|
25 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
26 apply (rule allI) |
|
27 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
28 apply (erule exE) |
|
29 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
30 apply (rule exI) |
|
31 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
32 apply (erule allE) |
|
33 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
34 apply assumption |
|
35 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
36 done |
|
37 |
|
38 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
|
39 by (tactic {*IntPr.fast_tac @{context} 1*}) |
|
40 |
|
41 text{*Example of Dyckhoff's method*} |
|
42 lemma "~ ~ ((P-->Q) | (Q-->P))" |
|
43 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
44 apply (unfold not_def) |
|
45 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
46 apply (rule impI) |
|
47 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
48 apply (erule disj_impE) |
|
49 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
50 apply (erule imp_impE) |
|
51 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
52 apply (erule imp_impE) |
|
53 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
54 apply assumption |
|
55 apply (erule FalseE)+ |
|
56 done |
|
57 |
|
58 end |