17480
|
1 |
(* Title: FOLP/ex/If.ML
|
0
|
2 |
ID: $Id$
|
1459
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
4 |
Copyright 1991 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
17480
|
7 |
val prems = goalw (the_context ()) [if_def]
|
3836
|
8 |
"[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
|
0
|
9 |
by (fast_tac (FOLP_cs addIs prems) 1);
|
|
10 |
val ifI = result();
|
|
11 |
|
17480
|
12 |
val major::prems = goalw (the_context ()) [if_def]
|
0
|
13 |
"[| p:if(P,Q,R); !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
|
|
14 |
\ !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
|
|
15 |
by (cut_facts_tac [major] 1);
|
|
16 |
by (fast_tac (FOLP_cs addIs prems) 1);
|
|
17 |
val ifE = result();
|
|
18 |
|
|
19 |
|
5061
|
20 |
Goal
|
0
|
21 |
"?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
|
1459
|
22 |
by (rtac iffI 1);
|
|
23 |
by (etac ifE 1);
|
|
24 |
by (etac ifE 1);
|
|
25 |
by (rtac ifI 1);
|
|
26 |
by (rtac ifI 1);
|
0
|
27 |
|
|
28 |
choplev 0;
|
|
29 |
val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
|
|
30 |
by (fast_tac if_cs 1);
|
|
31 |
val if_commute = result();
|
|
32 |
|
|
33 |
|
5061
|
34 |
Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
|
0
|
35 |
by (fast_tac if_cs 1);
|
|
36 |
val nested_ifs = result();
|