--- a/HOL.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.ML Tue Apr 19 10:50:00 1994 +0200
@@ -125,7 +125,8 @@
(** True **)
-val TrueI = refl RS (True_def RS iffD2);
+val TrueI = prove_goalw HOL.thy [True_def] "True"
+ (fn _ => [rtac refl 1]);
val eqTrueI = prove_goal HOL.thy "P ==> P=True"
(fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
@@ -135,13 +136,11 @@
(** Universal quantifier **)
-val allI = prove_goal HOL.thy "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn [asm] => [rtac (All_def RS ssubst) 1, rtac (asm RS (eqTrueI RS ext)) 1]);
+val allI = prove_goalw HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
-val spec = prove_goal HOL.thy "! x::'a.P(x) ==> P(x)"
- (fn prems =>
- [ rtac eqTrueE 1,
- resolve_tac (prems RL [All_def RS subst] RL [fun_cong]) 1 ]);
+val spec = prove_goalw HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+ (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
val allE = prove_goal HOL.thy "[| !x.P(x); P(x) ==> R |] ==> R"
(fn major::prems=>
@@ -157,7 +156,7 @@
before quantifiers! **)
val FalseE = prove_goal HOL.thy "False ==> P"
- (fn prems => [rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1]);
+ (fn prems => [rtac spec 1, fold_tac [False_def], resolve_tac prems 1]);
val False_neq_True = prove_goal HOL.thy "False=True ==> P"
(fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
@@ -165,14 +164,11 @@
(** Negation **)
-val notI = prove_goal HOL.thy "(P ==> False) ==> ~P"
- (fn prems=> [rtac (not_def RS ssubst) 1, rtac impI 1, eresolve_tac prems 1]);
+val notI = prove_goalw HOL.thy [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
-val notE = prove_goal HOL.thy "[| ~P; P |] ==> R"
- (fn prems =>
- [rtac (mp RS FalseE) 1,
- resolve_tac prems 2, rtac (not_def RS subst) 1,
- resolve_tac prems 1]);
+val notE = prove_goalw HOL.thy [not_def] "[| ~P; P |] ==> R"
+ (fn prems => [rtac (mp RS FalseE) 1, REPEAT(resolve_tac prems 1)]);
(** Implication **)
@@ -194,33 +190,27 @@
(** Existential quantifier **)
-val exI = prove_goal HOL.thy "P(x) ==> ? x::'a.P(x)"
- (fn prems =>
- [rtac (selectI RS (Ex_def RS ssubst)) 1,
- resolve_tac prems 1]);
+val exI = prove_goalw HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+ (fn prems => [rtac selectI 1, resolve_tac prems 1]);
-val exE = prove_goal HOL.thy "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
- (fn prems =>
- [resolve_tac prems 1, res_inst_tac [("P","%C.C(P)")] subst 1,
- rtac Ex_def 1, resolve_tac prems 1]);
+val exE = prove_goalw HOL.thy [Ex_def]
+ "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+ (fn prems => [REPEAT(resolve_tac prems 1)]);
(** Conjunction **)
-val conjI = prove_goal HOL.thy "[| P; Q |] ==> P&Q"
+val conjI = prove_goalw HOL.thy [and_def] "[| P; Q |] ==> P&Q"
(fn prems =>
- [ (rtac (and_def RS ssubst) 1),
- (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
+ [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
-val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
+val conjunct1 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> P"
(fn prems =>
- [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
- (REPEAT(ares_tac [impI] 1)) ]);
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
-val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q"
+val conjunct2 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> Q"
(fn prems =>
- [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
- (REPEAT(ares_tac [impI] 1)) ]);
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
val conjE = prove_goal HOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"
(fn prems =>
@@ -229,19 +219,15 @@
(** Disjunction *)
-val disjI1 = prove_goal HOL.thy "P ==> P|Q"
- (fn [prem] =>
- [rtac (or_def RS ssubst) 1,
- REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI1 = prove_goalw HOL.thy [or_def] "P ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-val disjI2 = prove_goal HOL.thy "Q ==> P|Q"
- (fn [prem] =>
- [rtac (or_def RS ssubst) 1,
- REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI2 = prove_goalw HOL.thy [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-val disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+val disjE = prove_goalw HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
(fn [a1,a2,a3] =>
- [rtac (mp RS mp) 1, rtac spec 1, rtac (or_def RS subst) 1, rtac a1 1,
+ [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
(** CCONTR -- classical logic **)
@@ -249,14 +235,18 @@
val ccontr = prove_goal HOL.thy "(~P ==> False) ==> P"
(fn prems =>
[rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
- rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1,
- rtac ssubst 1, atac 1, rtac (not_def RS ssubst) 1,
+ rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+ rtac ssubst 1, atac 1, rewtac not_def,
REPEAT (ares_tac [impI] 1) ]);
-val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+val ccontr = prove_goalw HOL.thy [not_def] "(~P ==> False) ==> P"
(fn prems =>
- [rtac ccontr 1,
- REPEAT (ares_tac (prems@[notE]) 1)]);
+ [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
+ rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+ rtac ssubst 1, atac 1, REPEAT (ares_tac [impI] 1) ]);
+
+val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+ (fn prems => [rtac ccontr 1, REPEAT (ares_tac (prems@[notE]) 1)]);
(*Double negation law*)
@@ -267,17 +257,15 @@
(** Unique existence **)
-val ex1I = prove_goal HOL.thy
+val ex1I = prove_goalw HOL.thy [Ex1_def]
"[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
(fn prems =>
- [ (rtac (Ex1_def RS ssubst) 1),
- (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
+ [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
-val ex1E = prove_goal HOL.thy
+val ex1E = prove_goalw HOL.thy [Ex1_def]
"[| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
(fn major::prems =>
- [ (resolve_tac ([major] RL [Ex1_def RS subst] RL [exE]) 1),
- (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)) ]);
+ [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
(** Select: Hilbert's Epsilon-operator **)
--- a/HOL.thy Wed Apr 06 16:31:06 1994 +0200
+++ b/HOL.thy Tue Apr 19 10:50:00 1994 +0200
@@ -103,15 +103,15 @@
(* Definitions *)
- True_def "True = ((%x::bool.x)=(%x.x))"
- All_def "All = (%P. P = (%x.True))"
- Ex_def "Ex = (%P. P(@x.P(x)))"
- False_def "False = (!P.P)"
- not_def "not = (%P. P-->False)"
- and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)"
- or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
- Ex1_def "Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
- Let_def "Let(s, f) = f(s)"
+ True_def "True == ((%x::bool.x)=(%x.x))"
+ All_def "All == (%P. P = (%x.True))"
+ Ex_def "Ex == (%P. P(@x.P(x)))"
+ False_def "False == (!P.P)"
+ not_def "not == (%P. P-->False)"
+ and_def "op & == (%P Q. !R. (P-->Q-->R) --> R)"
+ or_def "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+ Ex1_def "Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+ Let_def "Let(s, f) == f(s)"
(* Axioms *)
@@ -120,10 +120,10 @@
(* Misc Definitions *)
- Inv_def "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
- o_def "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+ Inv_def "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
+ o_def "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
- if_def "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+ if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
end
--- a/LList.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/LList.ML Tue Apr 19 10:50:00 1994 +0200
@@ -483,10 +483,9 @@
(** Two easy results about Lmap **)
-val [prem] = goal LList.thy
+val [prem] = goalw LList.thy [o_def]
"M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (stac o_def 1);
by (safe_tac set_cs);
by (etac LListE 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
--- a/Univ.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/Univ.ML Tue Apr 19 10:50:00 1994 +0200
@@ -147,16 +147,14 @@
val inj_Atom = result();
val Atom_inject = inj_Atom RS injD;
-goalw Univ.thy [Leaf_def] "inj(Leaf)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
by (rtac injI 1);
by (etac (Atom_inject RS Inl_inject) 1);
val inj_Leaf = result();
val Leaf_inject = inj_Leaf RS injD;
-goalw Univ.thy [Numb_def] "inj(Numb)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
by (rtac injI 1);
by (etac (Atom_inject RS Inr_inject) 1);
val inj_Numb = result();
@@ -223,8 +221,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
@@ -234,8 +231,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
@@ -301,13 +297,11 @@
by (rtac zero_less_Suc 1);
val ntrunc_Atom = result();
-goalw Univ.thy [Leaf_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
by (rtac ntrunc_Atom 1);
val ntrunc_Leaf = result();
-goalw Univ.thy [Numb_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
by (rtac ntrunc_Atom 1);
val ntrunc_Numb = result();
@@ -432,10 +426,10 @@
by (rtac (major RS equalityD2) 1);
val ntrunc_equality = result();
-val [major] = goal Univ.thy
+val [major] = goalw Univ.thy [o_def]
"[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
-by (resolve_tac ([major RS fun_cong] RL [o_def RS subst]) 1);
+by (rtac (major RS fun_cong) 1);
val ntrunc_o_equality = result();
(*** Monotonicity ***)
--- a/ex/PL.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/ex/PL.ML Tue Apr 19 10:50:00 1994 +0200
@@ -174,8 +174,8 @@
val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
by (rtac (major RS conseq_induct) 1);
by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (asm_simp_tac(pl_ss addsimps
- [ball_eq,not_def RS fun_cong RS sym])));
+by (ALLGOALS (asm_simp_tac(pl_ss addsimps [ball_eq])));
+by(fast_tac HOL_cs 1);
val soundness = result();
(** Structural induction on pl
@@ -261,8 +261,7 @@
goal PL.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
by (PL0.induct_tac "p" 1);
by (simp_tac pl_ss 1);
-by (simp_tac (pl_ss addsimps [insert_subset]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
by (simp_tac pl_ss 1);
by (fast_tac set_cs 1);
val hyps_insert = result();
--- a/ex/pl.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/ex/pl.ML Tue Apr 19 10:50:00 1994 +0200
@@ -174,8 +174,8 @@
val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
by (rtac (major RS conseq_induct) 1);
by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS (asm_simp_tac(pl_ss addsimps
- [ball_eq,not_def RS fun_cong RS sym])));
+by (ALLGOALS (asm_simp_tac(pl_ss addsimps [ball_eq])));
+by(fast_tac HOL_cs 1);
val soundness = result();
(** Structural induction on pl
@@ -261,8 +261,7 @@
goal PL.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{(#v)->false})";
by (PL0.induct_tac "p" 1);
by (simp_tac pl_ss 1);
-by (simp_tac (pl_ss addsimps [insert_subset]
- setloop (split_tac [expand_if])) 1);
+by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
by (simp_tac pl_ss 1);
by (fast_tac set_cs 1);
val hyps_insert = result();
--- a/fun.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/fun.ML Tue Apr 19 10:50:00 1994 +0200
@@ -49,8 +49,7 @@
by (REPEAT (ares_tac prems 1));
val imageE = result();
-goal Set.thy "(f o g)``r = f``(g``r)";
-by (stac o_def 1);
+goalw Set.thy [o_def] "(f o g)``r = f``(g``r)";
by (rtac set_ext 1);
by (fast_tac (HOL_cs addIs [imageI] addSEs [imageE]) 1);
val image_compose = result();
@@ -94,8 +93,8 @@
val inj_select = result();
(*A one-to-one function has an inverse (given using select).*)
-val [major] = goal Set.thy "inj(f) ==> Inv(f,f(x)) = x";
-by (EVERY1 [stac Inv_def, rtac (major RS inj_select)]);
+val [major] = goalw Set.thy [Inv_def] "inj(f) ==> Inv(f,f(x)) = x";
+by (EVERY1 [rtac (major RS inj_select)]);
val Inv_f_f = result();
(* Useful??? *)
@@ -136,9 +135,8 @@
(*** Lemmas about inj ***)
-val prems = goal Set.thy
+val prems = goalw Set.thy [o_def]
"[| inj(f); inj_onto(g,range(f)) |] ==> inj(g o f)";
-by (stac o_def 1);
by (cut_facts_tac prems 1);
by (fast_tac (HOL_cs addIs [injI,rangeI]
addEs [injD,inj_ontoD]) 1);
@@ -148,8 +146,8 @@
by (fast_tac (HOL_cs addIs [prem RS injD, inj_ontoI]) 1);
val inj_imp = result();
-val [prem] = goal Set.thy "y : range(f) ==> f(Inv(f,y)) = y";
-by (EVERY1 [stac Inv_def, rtac (prem RS rangeE), rtac selectI, etac sym]);
+val [prem] = goalw Set.thy [Inv_def] "y : range(f) ==> f(Inv(f,y)) = y";
+by (EVERY1 [rtac (prem RS rangeE), rtac selectI, etac sym]);
val f_Inv_f = result();
val prems = goal Set.thy
--- a/hol.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/hol.ML Tue Apr 19 10:50:00 1994 +0200
@@ -125,7 +125,8 @@
(** True **)
-val TrueI = refl RS (True_def RS iffD2);
+val TrueI = prove_goalw HOL.thy [True_def] "True"
+ (fn _ => [rtac refl 1]);
val eqTrueI = prove_goal HOL.thy "P ==> P=True"
(fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
@@ -135,13 +136,11 @@
(** Universal quantifier **)
-val allI = prove_goal HOL.thy "(!!x::'a. P(x)) ==> !x. P(x)"
- (fn [asm] => [rtac (All_def RS ssubst) 1, rtac (asm RS (eqTrueI RS ext)) 1]);
+val allI = prove_goalw HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
-val spec = prove_goal HOL.thy "! x::'a.P(x) ==> P(x)"
- (fn prems =>
- [ rtac eqTrueE 1,
- resolve_tac (prems RL [All_def RS subst] RL [fun_cong]) 1 ]);
+val spec = prove_goalw HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+ (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
val allE = prove_goal HOL.thy "[| !x.P(x); P(x) ==> R |] ==> R"
(fn major::prems=>
@@ -157,7 +156,7 @@
before quantifiers! **)
val FalseE = prove_goal HOL.thy "False ==> P"
- (fn prems => [rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1]);
+ (fn prems => [rtac spec 1, fold_tac [False_def], resolve_tac prems 1]);
val False_neq_True = prove_goal HOL.thy "False=True ==> P"
(fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
@@ -165,14 +164,11 @@
(** Negation **)
-val notI = prove_goal HOL.thy "(P ==> False) ==> ~P"
- (fn prems=> [rtac (not_def RS ssubst) 1, rtac impI 1, eresolve_tac prems 1]);
+val notI = prove_goalw HOL.thy [not_def] "(P ==> False) ==> ~P"
+ (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
-val notE = prove_goal HOL.thy "[| ~P; P |] ==> R"
- (fn prems =>
- [rtac (mp RS FalseE) 1,
- resolve_tac prems 2, rtac (not_def RS subst) 1,
- resolve_tac prems 1]);
+val notE = prove_goalw HOL.thy [not_def] "[| ~P; P |] ==> R"
+ (fn prems => [rtac (mp RS FalseE) 1, REPEAT(resolve_tac prems 1)]);
(** Implication **)
@@ -194,33 +190,27 @@
(** Existential quantifier **)
-val exI = prove_goal HOL.thy "P(x) ==> ? x::'a.P(x)"
- (fn prems =>
- [rtac (selectI RS (Ex_def RS ssubst)) 1,
- resolve_tac prems 1]);
+val exI = prove_goalw HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+ (fn prems => [rtac selectI 1, resolve_tac prems 1]);
-val exE = prove_goal HOL.thy "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
- (fn prems =>
- [resolve_tac prems 1, res_inst_tac [("P","%C.C(P)")] subst 1,
- rtac Ex_def 1, resolve_tac prems 1]);
+val exE = prove_goalw HOL.thy [Ex_def]
+ "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+ (fn prems => [REPEAT(resolve_tac prems 1)]);
(** Conjunction **)
-val conjI = prove_goal HOL.thy "[| P; Q |] ==> P&Q"
+val conjI = prove_goalw HOL.thy [and_def] "[| P; Q |] ==> P&Q"
(fn prems =>
- [ (rtac (and_def RS ssubst) 1),
- (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
+ [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
-val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
+val conjunct1 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> P"
(fn prems =>
- [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
- (REPEAT(ares_tac [impI] 1)) ]);
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
-val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q"
+val conjunct2 = prove_goalw HOL.thy [and_def] "[| P & Q |] ==> Q"
(fn prems =>
- [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
- (REPEAT(ares_tac [impI] 1)) ]);
+ [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
val conjE = prove_goal HOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"
(fn prems =>
@@ -229,19 +219,15 @@
(** Disjunction *)
-val disjI1 = prove_goal HOL.thy "P ==> P|Q"
- (fn [prem] =>
- [rtac (or_def RS ssubst) 1,
- REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI1 = prove_goalw HOL.thy [or_def] "P ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-val disjI2 = prove_goal HOL.thy "Q ==> P|Q"
- (fn [prem] =>
- [rtac (or_def RS ssubst) 1,
- REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+val disjI2 = prove_goalw HOL.thy [or_def] "Q ==> P|Q"
+ (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
-val disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+val disjE = prove_goalw HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
(fn [a1,a2,a3] =>
- [rtac (mp RS mp) 1, rtac spec 1, rtac (or_def RS subst) 1, rtac a1 1,
+ [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
(** CCONTR -- classical logic **)
@@ -249,14 +235,18 @@
val ccontr = prove_goal HOL.thy "(~P ==> False) ==> P"
(fn prems =>
[rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
- rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1,
- rtac ssubst 1, atac 1, rtac (not_def RS ssubst) 1,
+ rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+ rtac ssubst 1, atac 1, rewtac not_def,
REPEAT (ares_tac [impI] 1) ]);
-val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+val ccontr = prove_goalw HOL.thy [not_def] "(~P ==> False) ==> P"
(fn prems =>
- [rtac ccontr 1,
- REPEAT (ares_tac (prems@[notE]) 1)]);
+ [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
+ rtac spec 1, fold_tac [False_def], resolve_tac prems 1,
+ rtac ssubst 1, atac 1, REPEAT (ares_tac [impI] 1) ]);
+
+val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+ (fn prems => [rtac ccontr 1, REPEAT (ares_tac (prems@[notE]) 1)]);
(*Double negation law*)
@@ -267,17 +257,15 @@
(** Unique existence **)
-val ex1I = prove_goal HOL.thy
+val ex1I = prove_goalw HOL.thy [Ex1_def]
"[| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
(fn prems =>
- [ (rtac (Ex1_def RS ssubst) 1),
- (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
+ [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
-val ex1E = prove_goal HOL.thy
+val ex1E = prove_goalw HOL.thy [Ex1_def]
"[| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R |] ==> R"
(fn major::prems =>
- [ (resolve_tac ([major] RL [Ex1_def RS subst] RL [exE]) 1),
- (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)) ]);
+ [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
(** Select: Hilbert's Epsilon-operator **)
--- a/hol.thy Wed Apr 06 16:31:06 1994 +0200
+++ b/hol.thy Tue Apr 19 10:50:00 1994 +0200
@@ -103,15 +103,15 @@
(* Definitions *)
- True_def "True = ((%x::bool.x)=(%x.x))"
- All_def "All = (%P. P = (%x.True))"
- Ex_def "Ex = (%P. P(@x.P(x)))"
- False_def "False = (!P.P)"
- not_def "not = (%P. P-->False)"
- and_def "op & = (%P Q. !R. (P-->Q-->R) --> R)"
- or_def "op | = (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
- Ex1_def "Ex1 = (%P. ? x. P(x) & (! y. P(y) --> y=x))"
- Let_def "Let(s, f) = f(s)"
+ True_def "True == ((%x::bool.x)=(%x.x))"
+ All_def "All == (%P. P = (%x.True))"
+ Ex_def "Ex == (%P. P(@x.P(x)))"
+ False_def "False == (!P.P)"
+ not_def "not == (%P. P-->False)"
+ and_def "op & == (%P Q. !R. (P-->Q-->R) --> R)"
+ or_def "op | == (%P Q. !R. (P-->R) --> (Q-->R) --> R)"
+ Ex1_def "Ex1 == (%P. ? x. P(x) & (! y. P(y) --> y=x))"
+ Let_def "Let(s, f) == f(s)"
(* Axioms *)
@@ -120,10 +120,10 @@
(* Misc Definitions *)
- Inv_def "Inv = (%(f::'a=>'b) y. @x. f(x)=y)"
- o_def "op o = (%(f::'b=>'c) g (x::'a). f(g(x)))"
+ Inv_def "Inv == (%(f::'a=>'b) y. @x. f(x)=y)"
+ o_def "op o == (%(f::'b=>'c) g (x::'a). f(g(x)))"
- if_def "if = (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
+ if_def "if == (%P x y.@z::'a. (P=True --> z=x) & (P=False --> z=y))"
end
--- a/llist.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/llist.ML Tue Apr 19 10:50:00 1994 +0200
@@ -483,10 +483,9 @@
(** Two easy results about Lmap **)
-val [prem] = goal LList.thy
+val [prem] = goalw LList.thy [o_def]
"M: LList(A) ==> Lmap(f o g, M) = Lmap(f, Lmap(g, M))";
by (rtac (prem RS imageI RS LList_equalityI) 1);
-by (stac o_def 1);
by (safe_tac set_cs);
by (etac LListE 1);
by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS])));
--- a/simpdata.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/simpdata.ML Tue Apr 19 10:50:00 1994 +0200
@@ -46,8 +46,8 @@
(2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
-val o_apply = prove_goal HOL.thy "(f o g)(x) = f(g(x))"
- (fn _ => [ (stac o_def 1), (rtac refl 1) ]);
+val o_apply = prove_goalw HOL.thy [o_def] "(f o g)(x) = f(g(x))"
+ (fn _ => [rtac refl 1]);
val simp_thms = map prover
[ "(x=x) = True",
@@ -73,11 +73,11 @@
val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
val conj_comms = [conj_commute, conj_left_commute];
-val if_True = prove_goal HOL.thy "if(True,x,y) = x"
- (fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_True = prove_goalw HOL.thy [if_def] "if(True,x,y) = x"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
-val if_False = prove_goal HOL.thy "if(False,x,y) = y"
- (fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);
+val if_False = prove_goalw HOL.thy [if_def] "if(False,x,y) = y"
+ (fn _=>[fast_tac (HOL_cs addIs [select_equality]) 1]);
val if_P = prove_goal HOL.thy "P ==> if(P,x,y) = x"
(fn [prem] => [ stac (prem RS eqTrueI) 1, rtac if_True 1 ]);
@@ -112,7 +112,7 @@
let val lemma1 = prove_goal HOL.thy
"(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
(fn prems => [resolve_tac prems 1, etac exI 1]);
- val lemma2 = prove_goalw HOL.thy [Ex_def RS eq_reflection]
+ val lemma2 = prove_goalw HOL.thy [Ex_def]
"(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
(fn prems => [REPEAT(resolve_tac prems 1)])
in equal_intr lemma1 lemma2 end;
--- a/univ.ML Wed Apr 06 16:31:06 1994 +0200
+++ b/univ.ML Tue Apr 19 10:50:00 1994 +0200
@@ -147,16 +147,14 @@
val inj_Atom = result();
val Atom_inject = inj_Atom RS injD;
-goalw Univ.thy [Leaf_def] "inj(Leaf)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
by (rtac injI 1);
by (etac (Atom_inject RS Inl_inject) 1);
val inj_Leaf = result();
val Leaf_inject = inj_Leaf RS injD;
-goalw Univ.thy [Numb_def] "inj(Numb)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "inj(Numb)";
by (rtac injI 1);
by (etac (Atom_inject RS Inr_inject) 1);
val inj_Numb = result();
@@ -223,8 +221,7 @@
(** Scons vs Leaf **)
-goalw Univ.thy [Leaf_def] "(M$N) ~= Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "(M$N) ~= Leaf(a)";
by (rtac Scons_not_Atom 1);
val Scons_not_Leaf = result();
val Leaf_not_Scons = standard (Scons_not_Leaf RS not_sym);
@@ -234,8 +231,7 @@
(** Scons vs Numb **)
-goalw Univ.thy [Numb_def] "(M$N) ~= Numb(k)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "(M$N) ~= Numb(k)";
by (rtac Scons_not_Atom 1);
val Scons_not_Numb = result();
val Numb_not_Scons = standard (Scons_not_Numb RS not_sym);
@@ -301,13 +297,11 @@
by (rtac zero_less_Suc 1);
val ntrunc_Atom = result();
-goalw Univ.thy [Leaf_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
-by (stac o_def 1);
+goalw Univ.thy [Leaf_def,o_def] "ntrunc(Suc(k), Leaf(a)) = Leaf(a)";
by (rtac ntrunc_Atom 1);
val ntrunc_Leaf = result();
-goalw Univ.thy [Numb_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
-by (stac o_def 1);
+goalw Univ.thy [Numb_def,o_def] "ntrunc(Suc(k), Numb(i)) = Numb(i)";
by (rtac ntrunc_Atom 1);
val ntrunc_Numb = result();
@@ -432,10 +426,10 @@
by (rtac (major RS equalityD2) 1);
val ntrunc_equality = result();
-val [major] = goal Univ.thy
+val [major] = goalw Univ.thy [o_def]
"[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
-by (resolve_tac ([major RS fun_cong] RL [o_def RS subst]) 1);
+by (rtac (major RS fun_cong) 1);
val ntrunc_o_equality = result();
(*** Monotonicity ***)