src/FOLP/ex/if.ML
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOLP/ex/if.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,43 @@
     1.4 +(*  Title: 	FOLP/ex/if
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +For ex/if.thy.  First-Order Logic: the 'if' example
    1.10 +*)
    1.11 +
    1.12 +open If;
    1.13 +open Cla;    (*in case structure Int is open!*)
    1.14 +
    1.15 +val prems = goalw If.thy [if_def]
    1.16 +    "[| !!x.x:P ==> f(x):Q; !!x.x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
    1.17 +by (fast_tac (FOLP_cs addIs prems) 1);
    1.18 +val ifI = result();
    1.19 +
    1.20 +val major::prems = goalw If.thy [if_def]
    1.21 +   "[| p:if(P,Q,R);  !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
    1.22 +\                    !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
    1.23 +by (cut_facts_tac [major] 1);
    1.24 +by (fast_tac (FOLP_cs addIs prems) 1);
    1.25 +val ifE = result();
    1.26 +
    1.27 +
    1.28 +goal If.thy
    1.29 +    "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
    1.30 +by (resolve_tac [iffI] 1);
    1.31 +by (eresolve_tac [ifE] 1);
    1.32 +by (eresolve_tac [ifE] 1);
    1.33 +by (resolve_tac [ifI] 1);
    1.34 +by (resolve_tac [ifI] 1);
    1.35 +
    1.36 +choplev 0;
    1.37 +val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
    1.38 +by (fast_tac if_cs 1);
    1.39 +val if_commute = result();
    1.40 +
    1.41 +
    1.42 +goal If.thy "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    1.43 +by (fast_tac if_cs 1);
    1.44 +val nested_ifs = result();
    1.45 +
    1.46 +writeln"Reached end of file.";