src/FOLP/ex/foundn.ML
changeset 17480 fd19f77dcf60
parent 3836 f1a1817659e6
child 18678 dd0c569fa43d
     1.1 --- a/src/FOLP/ex/foundn.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/foundn.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -6,9 +6,7 @@
     1.4  Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
     1.5  *)
     1.6  
     1.7 -writeln"File FOLP/ex/foundn.ML";
     1.8 -
     1.9 -goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
    1.10 +goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
    1.11  by (rtac impI 1);
    1.12  by (rtac impI 1);
    1.13  by (rtac conjI 1);
    1.14 @@ -19,7 +17,7 @@
    1.15  
    1.16  (*A form of conj-elimination*)
    1.17  val prems = 
    1.18 -goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
    1.19 +goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
    1.20  by (resolve_tac prems 1);
    1.21  by (rtac conjunct1 1);
    1.22  by (resolve_tac prems 1);
    1.23 @@ -29,7 +27,7 @@
    1.24  
    1.25  
    1.26  val prems = 
    1.27 -goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    1.28 +goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    1.29  by (resolve_tac prems 1);
    1.30  by (rtac notI 1);
    1.31  by (res_inst_tac [ ("P", "~B") ]  notE  1);
    1.32 @@ -47,7 +45,7 @@
    1.33  
    1.34  
    1.35  val prems = 
    1.36 -goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    1.37 +goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    1.38  by (resolve_tac prems 1);
    1.39  by (rtac notI 1);
    1.40  by (rtac notE 1);
    1.41 @@ -61,7 +59,7 @@
    1.42  
    1.43  
    1.44  val prems = 
    1.45 -goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
    1.46 +goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
    1.47  by (rtac disjE 1);
    1.48  by (resolve_tac prems 1);
    1.49  by (assume_tac 1);
    1.50 @@ -75,7 +73,7 @@
    1.51  writeln"Examples with quantifiers";
    1.52  
    1.53  val prems =
    1.54 -goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
    1.55 +goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
    1.56  by (rtac allI 1);
    1.57  by (rtac disjI1 1);
    1.58  by (resolve_tac (prems RL [spec]) 1); 
    1.59 @@ -84,14 +82,14 @@
    1.60  result();
    1.61  
    1.62  
    1.63 -goal IFOLP.thy "?p : ALL x. EX y. x=y";
    1.64 +goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
    1.65  by (rtac allI 1);
    1.66  by (rtac exI 1);
    1.67  by (rtac refl 1);
    1.68  result();
    1.69  
    1.70  
    1.71 -goal IFOLP.thy "?p : EX y. ALL x. x=y";
    1.72 +goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
    1.73  by (rtac exI 1);
    1.74  by (rtac allI 1);
    1.75  by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
    1.76 @@ -99,7 +97,7 @@
    1.77  
    1.78  
    1.79  (*Parallel lifting example. *)
    1.80 -goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
    1.81 +goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
    1.82  by (resolve_tac [exI, allI] 1);
    1.83  by (resolve_tac [exI, allI] 1);
    1.84  by (resolve_tac [exI, allI] 1);
    1.85 @@ -108,7 +106,7 @@
    1.86  
    1.87  
    1.88  val prems =
    1.89 -goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
    1.90 +goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
    1.91  by (rtac conjE 1);
    1.92  by (resolve_tac prems 1);
    1.93  by (rtac exE 1);
    1.94 @@ -121,7 +119,7 @@
    1.95  
    1.96  
    1.97  (*A bigger demonstration of quantifiers -- not in the paper*)
    1.98 -goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    1.99 +goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   1.100  by (rtac impI 1);
   1.101  by (rtac allI 1);
   1.102  by (rtac exE 1 THEN assume_tac 1);
   1.103 @@ -129,6 +127,3 @@
   1.104  by (rtac allE 1 THEN assume_tac 1);
   1.105  by (assume_tac 1);
   1.106  result();  
   1.107 -
   1.108 -
   1.109 -writeln"Reached end of file.";