0
|
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.";
|