src/FOLP/ex/intro.ML
changeset 17480 fd19f77dcf60
parent 15661 9ef583b08647
     1.1 --- a/src/FOLP/ex/intro.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/intro.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  (**** Some simple backward proofs ****)
     1.6  
     1.7 -goal FOLP.thy "?p:P|P --> P";
     1.8 +goal (theory "FOLP") "?p:P|P --> P";
     1.9  by (rtac impI 1);
    1.10  by (rtac disjE 1);
    1.11  by (assume_tac 3);
    1.12 @@ -22,7 +22,7 @@
    1.13  by (assume_tac 1);
    1.14  val mythm = result();
    1.15  
    1.16 -goal FOLP.thy "?p:(P & Q) | R  --> (P | R)";
    1.17 +goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
    1.18  by (rtac impI 1);
    1.19  by (etac disjE 1);
    1.20  by (dtac conjunct1 1);
    1.21 @@ -32,7 +32,7 @@
    1.22  result();
    1.23  
    1.24  (*Correct version, delaying use of "spec" until last*)
    1.25 -goal FOLP.thy "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
    1.26 +goal (theory "FOLP") "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
    1.27  by (rtac impI 1);
    1.28  by (rtac allI 1);
    1.29  by (rtac allI 1);
    1.30 @@ -44,12 +44,12 @@
    1.31  
    1.32  (**** Demonstration of fast_tac ****)
    1.33  
    1.34 -goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
    1.35 +goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
    1.36  \       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
    1.37  by (fast_tac FOLP_cs 1);
    1.38  result();
    1.39  
    1.40 -goal FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
    1.41 +goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
    1.42  \       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
    1.43  by (fast_tac FOLP_cs 1);
    1.44  result();
    1.45 @@ -57,7 +57,7 @@
    1.46  
    1.47  (**** Derivation of conjunction elimination rule ****)
    1.48  
    1.49 -val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
    1.50 +val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
    1.51  by (rtac minor 1);
    1.52  by (resolve_tac [major RS conjunct1] 1);
    1.53  by (resolve_tac [major RS conjunct2] 1);
    1.54 @@ -69,14 +69,14 @@
    1.55  
    1.56  (** Derivation of negation introduction **)
    1.57  
    1.58 -val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
    1.59 +val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
    1.60  by (rewtac not_def);
    1.61  by (rtac impI 1);
    1.62  by (resolve_tac prems 1);
    1.63  by (assume_tac 1);
    1.64  result();
    1.65  
    1.66 -val [major,minor] = goal FOLP.thy "[| p:~P;  q:P |] ==> ?p:R";
    1.67 +val [major,minor] = goal (theory "FOLP") "[| p:~P;  q:P |] ==> ?p:R";
    1.68  by (rtac FalseE 1);
    1.69  by (rtac mp 1);
    1.70  by (resolve_tac [rewrite_rule [not_def] major] 1);
    1.71 @@ -84,9 +84,7 @@
    1.72  result();
    1.73  
    1.74  (*Alternative proof of above result*)
    1.75 -val [major,minor] = goalw FOLP.thy [not_def]
    1.76 +val [major,minor] = goalw (theory "FOLP") [not_def]
    1.77      "[| p:~P;  q:P |] ==> ?p:R";
    1.78  by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
    1.79  result();
    1.80 -
    1.81 -writeln"Reached end of file.";