1 (* Title: FOL/ex/If.ML |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1991 University of Cambridge |
|
4 |
|
5 First-Order Logic: the 'if' example. |
|
6 *) |
|
7 |
|
8 theory If imports "~~/src/FOL/FOL" begin |
|
9 |
|
10 definition "if" :: "[o,o,o]=>o" where |
|
11 "if(P,Q,R) == P&Q | ~P&R" |
|
12 |
|
13 lemma ifI: |
|
14 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)" |
|
15 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
16 apply (simp add: if_def) |
|
17 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
18 apply blast |
|
19 done |
|
20 |
|
21 lemma ifE: |
|
22 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S" |
|
23 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
24 apply (simp add: if_def) |
|
25 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
26 apply blast |
|
27 done |
|
28 |
|
29 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
|
30 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
31 apply (rule iffI) |
|
32 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
33 apply (erule ifE) |
|
34 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
35 apply (erule ifE) |
|
36 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
37 apply (rule ifI) |
|
38 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
39 apply (rule ifI) |
|
40 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
41 oops |
|
42 |
|
43 text{*Trying again from the beginning in order to use @{text blast}*} |
|
44 declare ifI [intro!] |
|
45 declare ifE [elim!] |
|
46 |
|
47 lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))" |
|
48 by blast |
|
49 |
|
50 |
|
51 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
|
52 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
53 by blast |
|
54 |
|
55 text{*Trying again from the beginning in order to prove from the definitions*} |
|
56 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))" |
|
57 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
58 apply (simp add: if_def) |
|
59 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
60 apply blast |
|
61 done |
|
62 |
|
63 |
|
64 text{*An invalid formula. High-level rules permit a simpler diagnosis*} |
|
65 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
|
66 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
67 apply auto |
|
68 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
69 (*The next step will fail unless subgoals remain*) |
|
70 apply (tactic all_tac) |
|
71 oops |
|
72 |
|
73 text{*Trying again from the beginning in order to prove from the definitions*} |
|
74 lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))" |
|
75 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
76 apply (simp add: if_def) |
|
77 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
78 apply (auto) |
|
79 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
80 (*The next step will fail unless subgoals remain*) |
|
81 apply (tactic all_tac) |
|
82 oops |
|
83 |
|
84 |
|
85 end |
|