src/FOLP/ex/foundn.ML
 author paulson Fri, 05 Oct 2007 09:59:03 +0200 changeset 24854 0ebcd575d3c6 parent 18678 dd0c569fa43d permissions -rw-r--r--
filtering out some package theorems
```
(*  Title:      FOLP/ex/foundn.ML
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1991  University of Cambridge

Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
*)

goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
by (rtac impI 1);
by (rtac impI 1);
by (rtac conjI 1);
by (assume_tac 2);
by (rtac conjunct1 1);
by (assume_tac 1);
result();

(*A form of conj-elimination*)
val prems =
goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
by (resolve_tac prems 1);
by (rtac conjunct1 1);
by (resolve_tac prems 1);
by (rtac conjunct2 1);
by (resolve_tac prems 1);
result();

val prems =
goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (res_inst_tac [ ("P", "~B") ]  notE  1);
by (rtac notI 2);
by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
by (assume_tac 2);
by (rtac disjI1 2);
by (assume_tac 2);
by (rtac notI 1);
by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
by (assume_tac 1);
by (rtac disjI2 1);
by (assume_tac 1);
result();

val prems =
goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (rtac notE 1);
by (rtac notI 2);
by (etac notE 2);
by (etac disjI1 2);
by (rtac notI 1);
by (etac notE 1);
by (etac disjI2 1);
result();

val prems =
goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
by (rtac disjE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
by (rtac FalseE 1);
by (res_inst_tac [ ("P", "~A") ]  notE  1);
by (resolve_tac prems 1);
by (assume_tac 1);
result();

writeln"Examples with quantifiers";

val prems =
goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
by (rtac allI 1);
by (rtac disjI1 1);
by (resolve_tac (prems RL [spec]) 1);
(*can use instead
by (rtac spec 1);  by (resolve_tac prems 1); *)
result();

goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
by (rtac allI 1);
by (rtac exI 1);
by (rtac refl 1);
result();

goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
by (rtac exI 1);
by (rtac allI 1);
by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";
getgoal 1;

(*Parallel lifting example. *)
goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);

val prems =
goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);
by (assume_tac 1);
by (rtac exI 1);
by (rtac conjI 1);
by (assume_tac 1);
by (assume_tac 1);
result();

(*A bigger demonstration of quantifiers -- not in the paper*)
goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac exE 1 THEN assume_tac 1);
by (rtac exI 1);
by (rtac allE 1 THEN assume_tac 1);
by (assume_tac 1);
result();
```