|
1 (* Title: FOL/ex/if |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 For ex/if.thy. First-Order Logic: the 'if' example |
|
7 *) |
|
8 |
|
9 open If; |
|
10 open Cla; (*in case structure Int is open!*) |
|
11 |
|
12 val prems = goalw If.thy [if_def] |
|
13 "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"; |
|
14 by (fast_tac (FOL_cs addIs prems) 1); |
|
15 val ifI = result(); |
|
16 |
|
17 val major::prems = goalw If.thy [if_def] |
|
18 "[| if(P,Q,R); [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"; |
|
19 by (cut_facts_tac [major] 1); |
|
20 by (fast_tac (FOL_cs addIs prems) 1); |
|
21 val ifE = result(); |
|
22 |
|
23 |
|
24 goal If.thy |
|
25 "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; |
|
26 by (resolve_tac [iffI] 1); |
|
27 by (eresolve_tac [ifE] 1); |
|
28 by (eresolve_tac [ifE] 1); |
|
29 by (resolve_tac [ifI] 1); |
|
30 by (resolve_tac [ifI] 1); |
|
31 |
|
32 choplev 0; |
|
33 val if_cs = FOL_cs addSIs [ifI] addSEs[ifE]; |
|
34 by (fast_tac if_cs 1); |
|
35 val if_commute = result(); |
|
36 |
|
37 |
|
38 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; |
|
39 by (fast_tac if_cs 1); |
|
40 val nested_ifs = result(); |
|
41 |
|
42 choplev 0; |
|
43 by (rewrite_goals_tac [if_def]); |
|
44 by (fast_tac FOL_cs 1); |
|
45 result(); |
|
46 |
|
47 |
|
48 (*An invalid formula. High-level rules permit a simpler diagnosis*) |
|
49 goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"; |
|
50 by (fast_tac if_cs 1) handle ERROR => writeln"Failed, as expected"; |
|
51 (*Check that subgoals remain: proof failed.*) |
|
52 getgoal 1; |
|
53 by (REPEAT (step_tac if_cs 1)); |
|
54 |
|
55 choplev 0; |
|
56 by (rewrite_goals_tac [if_def]); |
|
57 by (fast_tac FOL_cs 1) handle ERROR => writeln"Failed, as expected"; |
|
58 (*Check that subgoals remain: proof failed.*) |
|
59 getgoal 1; |
|
60 by (REPEAT (step_tac FOL_cs 1)); |
|
61 |
|
62 |
|
63 |
|
64 writeln"Reached end of file."; |