|
1 (* Title: FOLP/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 "[| !!x.x:P ==> f(x):Q; !!x.x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)"; |
|
14 by (fast_tac (FOLP_cs addIs prems) 1); |
|
15 val ifI = result(); |
|
16 |
|
17 val major::prems = goalw If.thy [if_def] |
|
18 "[| p:if(P,Q,R); !!x y.[| x:P; y:Q |] ==> f(x,y):S; \ |
|
19 \ !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S"; |
|
20 by (cut_facts_tac [major] 1); |
|
21 by (fast_tac (FOLP_cs addIs prems) 1); |
|
22 val ifE = result(); |
|
23 |
|
24 |
|
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))"; |
|
27 by (resolve_tac [iffI] 1); |
|
28 by (eresolve_tac [ifE] 1); |
|
29 by (eresolve_tac [ifE] 1); |
|
30 by (resolve_tac [ifI] 1); |
|
31 by (resolve_tac [ifI] 1); |
|
32 |
|
33 choplev 0; |
|
34 val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE]; |
|
35 by (fast_tac if_cs 1); |
|
36 val if_commute = result(); |
|
37 |
|
38 |
|
39 goal If.thy "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"; |
|
40 by (fast_tac if_cs 1); |
|
41 val nested_ifs = result(); |
|
42 |
|
43 writeln"Reached end of file."; |