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