--- a/src/CTT/ex/elim.ML Fri Jan 19 16:00:22 1996 +0100
+++ b/src/CTT/ex/elim.ML Sat Jan 20 02:00:11 1996 +0100
@@ -1,10 +1,10 @@
-(* Title: CTT/ex/elim
+(* Title: CTT/ex/elim
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
Some examples taken from P. Martin-L\"of, Intuitionistic type theory
- (Bibliopolis, 1984).
+ (Bibliopolis, 1984).
by (safe_tac prems 1);
by (step_tac prems 1);
@@ -65,9 +65,9 @@
(*more general goal with same proof*)
val prems = goal CTT.thy
- "[| A type; !!x. x:A ==> B(x) type; \
-\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \
-\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \
+ "[| A type; !!x. x:A ==> B(x) type; \
+\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \
+\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \
\ (PROD x:A . PROD y:B(x) . C(<x,y>))";
by (pc_tac prems 1);
result();
@@ -131,9 +131,9 @@
(*Martin-Lof (1984) page 50*)
writeln"AXIOM OF CHOICE!!! Delicate use of elimination rules";
val prems = goal CTT.thy
- "[| A type; !!x. x:A ==> B(x) type; \
-\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
-\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
+ "[| A type; !!x. x:A ==> B(x) type; \
+\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
+\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
by (intr_tac prems);
by (add_mp_tac 2);
@@ -148,9 +148,9 @@
writeln"Axiom of choice. Proof without fst, snd. Harder still!";
val prems = goal CTT.thy
- "[| A type; !!x.x:A ==> B(x) type; \
-\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
-\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
+ "[| A type; !!x.x:A ==> B(x) type; \
+\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
+\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
by (intr_tac prems);
(*Must not use add_mp_tac as subst_prodE hides the construction.*)
--- a/src/FOLP/ex/intro.ML Fri Jan 19 16:00:22 1996 +0100
+++ b/src/FOLP/ex/intro.ML Sat Jan 20 02:00:11 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: FOL/ex/intro
+(* Title: FOL/ex/intro
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Examples for the manual "Introduction to Isabelle"
@@ -15,29 +15,29 @@
(**** Some simple backward proofs ****)
goal FOLP.thy "?p:P|P --> P";
-by (resolve_tac [impI] 1);
-by (resolve_tac [disjE] 1);
+by (rtac impI 1);
+by (rtac disjE 1);
by (assume_tac 3);
by (assume_tac 2);
by (assume_tac 1);
val mythm = result();
goal FOLP.thy "?p:(P & Q) | R --> (P | R)";
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disjE] 1);
-by (dresolve_tac [conjunct1] 1);
-by (resolve_tac [disjI1] 1);
-by (resolve_tac [disjI2] 2);
+by (rtac impI 1);
+by (etac disjE 1);
+by (dtac conjunct1 1);
+by (rtac disjI1 1);
+by (rtac disjI2 2);
by (REPEAT (assume_tac 1));
result();
(*Correct version, delaying use of "spec" until last*)
goal FOLP.thy "?p:(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [allI] 1);
-by (dresolve_tac [spec] 1);
-by (dresolve_tac [spec] 1);
+by (rtac impI 1);
+by (rtac allI 1);
+by (rtac allI 1);
+by (dtac spec 1);
+by (dtac spec 1);
by (assume_tac 1);
result();
@@ -58,7 +58,7 @@
(**** Derivation of conjunction elimination rule ****)
val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
by (resolve_tac [major RS conjunct1] 1);
by (resolve_tac [major RS conjunct2] 1);
prth (topthm());
@@ -70,17 +70,17 @@
(** Derivation of negation introduction **)
val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
-by (rewrite_goals_tac [not_def]);
-by (resolve_tac [impI] 1);
+by (rewtac not_def);
+by (rtac impI 1);
by (resolve_tac prems 1);
by (assume_tac 1);
result();
val [major,minor] = goal FOLP.thy "[| p:~P; q:P |] ==> ?p:R";
-by (resolve_tac [FalseE] 1);
-by (resolve_tac [mp] 1);
+by (rtac FalseE 1);
+by (rtac mp 1);
by (resolve_tac [rewrite_rule [not_def] major] 1);
-by (resolve_tac [minor] 1);
+by (rtac minor 1);
result();
(*Alternative proof of above result*)