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