changeset 1459 | d12da312eff4 |
parent 0 | a5a9c433f639 |
child 3836 | f1a1817659e6 |
1458:fd510875fb71 | 1459:d12da312eff4 |
---|---|
1 (* Title: FOLP/ex/if |
1 (* Title: FOLP/ex/if |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 For ex/if.thy. First-Order Logic: the 'if' example |
6 For ex/if.thy. First-Order Logic: the 'if' example |
7 *) |
7 *) |
8 |
8 |
22 val ifE = result(); |
22 val ifE = result(); |
23 |
23 |
24 |
24 |
25 goal If.thy |
25 goal If.thy |
26 "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; |
26 "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"; |
27 by (resolve_tac [iffI] 1); |
27 by (rtac iffI 1); |
28 by (eresolve_tac [ifE] 1); |
28 by (etac ifE 1); |
29 by (eresolve_tac [ifE] 1); |
29 by (etac ifE 1); |
30 by (resolve_tac [ifI] 1); |
30 by (rtac ifI 1); |
31 by (resolve_tac [ifI] 1); |
31 by (rtac ifI 1); |
32 |
32 |
33 choplev 0; |
33 choplev 0; |
34 val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE]; |
34 val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE]; |
35 by (fast_tac if_cs 1); |
35 by (fast_tac if_cs 1); |
36 val if_commute = result(); |
36 val if_commute = result(); |