--- a/src/HOL/Arith.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Arith.ML Thu Jul 15 10:27:54 1999 +0200
@@ -12,16 +12,18 @@
(** Difference **)
-qed_goal "diff_0_eq_0" thy
- "0 - n = 0"
- (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
+Goal "0 - n = 0";
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_0_eq_0";
(*Must simplify BEFORE the induction! (Else we get a critical pair)
Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *)
-qed_goal "diff_Suc_Suc" thy
- "Suc(m) - Suc(n) = m - n"
- (fn _ =>
- [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
+Goal "Suc(m) - Suc(n) = m - n";
+by (Simp_tac 1);
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_Suc_Suc";
Addsimps [diff_0_eq_0, diff_Suc_Suc];
@@ -40,25 +42,36 @@
(*** Addition ***)
-qed_goal "add_0_right" thy "m + 0 = m"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "m + 0 = m";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_0_right";
-qed_goal "add_Suc_right" thy "m + Suc(n) = Suc(m+n)"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "m + Suc(n) = Suc(m+n)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_Suc_right";
Addsimps [add_0_right,add_Suc_right];
+
(*Associative law for addition*)
-qed_goal "add_assoc" thy "(m + n) + k = m + ((n + k)::nat)"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "(m + n) + k = m + ((n + k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_assoc";
(*Commutative law for addition*)
-qed_goal "add_commute" thy "m + n = n + (m::nat)"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "m + n = n + (m::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_commute";
-qed_goal "add_left_commute" thy "x+(y+z)=y+((x+z)::nat)"
- (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
- rtac (add_commute RS arg_cong) 1]);
+Goal "x+(y+z)=y+((x+z)::nat)";
+by (rtac (add_commute RS trans) 1);
+by (rtac (add_assoc RS trans) 1);
+by (rtac (add_commute RS arg_cong) 1);
+qed "add_left_commute";
(*Addition is an AC-operator*)
val add_ac = [add_assoc, add_commute, add_left_commute];
@@ -264,13 +277,16 @@
(*** Multiplication ***)
(*right annihilation in product*)
-qed_goal "mult_0_right" thy "m * 0 = 0"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "m * 0 = 0";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_0_right";
(*right successor law for multiplication*)
-qed_goal "mult_Suc_right" thy "m * Suc(n) = m + (m * n)"
- (fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
+Goal "m * Suc(n) = m + (m * n)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "mult_Suc_right";
Addsimps [mult_0_right, mult_Suc_right];
@@ -283,26 +299,35 @@
qed "mult_1_right";
(*Commutative law for multiplication*)
-qed_goal "mult_commute" thy "m * n = n * (m::nat)"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
+Goal "m * n = n * (m::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "mult_commute";
(*addition distributes over multiplication*)
-qed_goal "add_mult_distrib" thy "(m + n)*k = (m*k) + ((n*k)::nat)"
- (fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
+Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib";
-qed_goal "add_mult_distrib2" thy "k*(m + n) = (k*m) + ((k*n)::nat)"
- (fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
+Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
+qed "add_mult_distrib2";
(*Associative law for multiplication*)
-qed_goal "mult_assoc" thy "(m * n) * k = m * ((n * k)::nat)"
- (fn _ => [induct_tac "m" 1,
- ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]);
+Goal "(m * n) * k = m * ((n * k)::nat)";
+by (induct_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
+qed "mult_assoc";
-qed_goal "mult_left_commute" thy "x*(y*z) = y*((x*z)::nat)"
- (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
- rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
+Goal "x*(y*z) = y*((x*z)::nat)";
+by (rtac trans 1);
+by (rtac mult_commute 1);
+by (rtac trans 1);
+by (rtac mult_assoc 1);
+by (rtac (mult_commute RS arg_cong) 1);
+qed "mult_left_commute";
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
@@ -322,9 +347,11 @@
(*** Difference ***)
+Goal "m - m = 0";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_self_eq_0";
-qed_goal "diff_self_eq_0" thy "m - m = 0"
- (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
Addsimps [diff_self_eq_0];
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
--- a/src/HOL/Divides.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Divides.ML Thu Jul 15 10:27:54 1999 +0200
@@ -97,7 +97,7 @@
(*** Quotient ***)
Goal "(%m. m div n) = wfrec (trancl pred_nat) \
- \ (%f j. if j<n then 0 else Suc (f (j-n)))";
+\ (%f j. if j<n then 0 else Suc (f (j-n)))";
by (simp_tac (simpset() addsimps [div_def]) 1);
qed "div_eq";
@@ -116,7 +116,6 @@
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
qed "le_div_geq";
-(*NOT suitable for rewriting: loops*)
Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
qed "div_if";
@@ -306,7 +305,7 @@
(*** More division laws ***)
-Goal "0<n ==> m*n div n = m";
+Goal "0<n ==> (m*n) div n = m";
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
--- a/src/HOL/Prod.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Prod.ML Thu Jul 15 10:27:54 1999 +0200
@@ -321,24 +321,25 @@
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
-qed_goal "SigmaD1" Prod.thy "(a,b) : Sigma A B ==> a : A"
- (fn [major]=>
- [ (rtac (major RS SigmaE) 1),
- (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
+
+Goal "(a,b) : Sigma A B ==> a : A";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD1";
-qed_goal "SigmaD2" Prod.thy "(a,b) : Sigma A B ==> b : B(a)"
- (fn [major]=>
- [ (rtac (major RS SigmaE) 1),
- (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ]);
+Goal "(a,b) : Sigma A B ==> b : B(a)";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD2";
-qed_goal "SigmaE2" Prod.thy
+val [major,minor]= goal Prod.thy
"[| (a,b) : Sigma A B; \
\ [| a:A; b:B(a) |] ==> P \
-\ |] ==> P"
- (fn [major,minor]=>
- [ (rtac minor 1),
- (rtac (major RS SigmaD1) 1),
- (rtac (major RS SigmaD2) 1) ]);
+\ |] ==> P";
+by (rtac minor 1);
+by (rtac (major RS SigmaD1) 1);
+by (rtac (major RS SigmaD2) 1) ;
+qed "SigmaE2";
AddSEs [SigmaE2, SigmaE];
@@ -348,11 +349,13 @@
by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
qed "Sigma_mono";
-qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "Sigma {} B = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty1";
-qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "A Times {} = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty2";
Addsimps [Sigma_empty1,Sigma_empty2];
--- a/src/HOL/Relation.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Relation.ML Thu Jul 15 10:27:54 1999 +0200
@@ -207,14 +207,14 @@
by (Blast_tac 1);
qed "Domain_iff";
-qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)"
- (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
+Goal "(a,b): r ==> a: Domain(r)";
+by (etac (exI RS (Domain_iff RS iffD2)) 1) ;
+qed "DomainI";
-qed_goal "DomainE" thy
- "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P"
- (fn prems=>
- [ (rtac (Domain_iff RS iffD1 RS exE) 1),
- (REPEAT (ares_tac prems 1)) ]);
+val prems= Goal "[| a : Domain(r); !!y. (a,y): r ==> P |] ==> P";
+by (rtac (Domain_iff RS iffD1 RS exE) 1);
+by (REPEAT (ares_tac prems 1)) ;
+qed "DomainE";
AddIs [DomainI];
AddSEs [DomainE];
@@ -298,22 +298,23 @@
qed_goalw "Image_iff" thy [Image_def]
"b : r^^A = (? x:A. (x,b):r)"
- (fn _ => [ Blast_tac 1 ]);
+ (fn _ => [(Blast_tac 1)]);
qed_goalw "Image_singleton" thy [Image_def]
"r^^{a} = {b. (a,b):r}"
- (fn _ => [ Blast_tac 1 ]);
+ (fn _ => [(Blast_tac 1)]);
-qed_goal "Image_singleton_iff" thy
- "(b : r^^{a}) = ((a,b):r)"
- (fn _ => [ rtac (Image_iff RS trans) 1,
- Blast_tac 1 ]);
+Goal
+ "(b : r^^{a}) = ((a,b):r)";
+by (rtac (Image_iff RS trans) 1);
+by (Blast_tac 1);
+qed "Image_singleton_iff";
AddIffs [Image_singleton_iff];
-qed_goalw "ImageI" thy [Image_def]
- "!!a b r. [| (a,b): r; a:A |] ==> b : r^^A"
- (fn _ => [ (Blast_tac 1)]);
+Goalw [Image_def] "[| (a,b): r; a:A |] ==> b : r^^A";
+by (Blast_tac 1);
+qed "ImageI";
qed_goalw "ImageE" thy [Image_def]
"[| b: r^^A; !!x.[| (x,b): r; x:A |] ==> P |] ==> P"
@@ -327,9 +328,10 @@
AddSEs [ImageE];
-qed_goal "Image_empty" thy
- "R^^{} = {}"
- (fn _ => [ Blast_tac 1 ]);
+Goal
+ "R^^{} = {}";
+by (Blast_tac 1);
+qed "Image_empty";
Addsimps [Image_empty];
@@ -343,17 +345,18 @@
Addsimps [Image_Id, Image_diag];
-qed_goal "Image_Int_subset" thy
- "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "R ^^ (A Int B) <= R ^^ A Int R ^^ B";
+by (Blast_tac 1);
+qed "Image_Int_subset";
-qed_goal "Image_Un" thy "R ^^ (A Un B) = R ^^ A Un R ^^ B"
- (fn _ => [ Blast_tac 1 ]);
+Goal "R ^^ (A Un B) = R ^^ A Un R ^^ B";
+by (Blast_tac 1);
+qed "Image_Un";
-qed_goal "Image_subset" thy "!!A B r. r <= A Times B ==> r^^C <= B"
- (fn _ =>
- [ (rtac subsetI 1),
- (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
+Goal "r <= A Times B ==> r^^C <= B";
+by (rtac subsetI 1);
+by (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ;
+qed "Image_subset";
(*NOT suitable for rewriting*)
Goal "r^^B = (UN y: B. r^^{y})";
--- a/src/HOL/Set.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Set.ML Thu Jul 15 10:27:54 1999 +0200
@@ -71,10 +71,11 @@
by (Blast_tac 1);
qed "rev_bexI";
-qed_goal "bexCI" Set.thy
- "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)" (fn prems =>
- [ (rtac classical 1),
- (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
+val prems = goal Set.thy
+ "[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A. P(x)";
+by (rtac classical 1);
+by (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ;
+qed "bexCI";
val major::prems = Goalw [Bex_def]
"[| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q";
@@ -139,17 +140,20 @@
qed "subsetD";
(*The same, with reversed premises for use with etac -- cf rev_mp*)
-qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]);
+Goal "[| c:A; A <= B |] ==> c:B";
+by (REPEAT (ares_tac [subsetD] 1)) ;
+qed "rev_subsetD";
(*Converts A<=B to x:A ==> x:B*)
fun impOfSubs th = th RSN (2, rev_subsetD);
-qed_goal "contra_subsetD" Set.thy "!!c. [| A <= B; c ~: B |] ==> c ~: A"
- (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+Goal "[| A <= B; c ~: B |] ==> c ~: A";
+by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
+qed "contra_subsetD";
-qed_goal "rev_contra_subsetD" Set.thy "!!c. [| c ~: B; A <= B |] ==> c ~: A"
- (fn prems=> [ (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ]);
+Goal "[| c ~: B; A <= B |] ==> c ~: A";
+by (REPEAT (eresolve_tac [asm_rl, contrapos, subsetD] 1)) ;
+qed "rev_contra_subsetD";
(*Classical elimination rule*)
val major::prems = Goalw [subset_def]
@@ -164,8 +168,9 @@
AddSIs [subsetI];
AddEs [subsetD, subsetCE];
-qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
- (fn _=> [Fast_tac 1]); (*Blast_tac would try order_refl and fail*)
+Goal "A <= (A::'a set)";
+by (Fast_tac 1);
+qed "subset_refl"; (*Blast_tac would try order_refl and fail*)
Goal "[| A<=B; B<=C |] ==> A<=(C::'a set)";
by (Blast_tac 1);
@@ -242,29 +247,33 @@
section "The empty set -- {}";
-qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
- (fn _ => [ (Blast_tac 1) ]);
+Goalw [empty_def] "(c : {}) = False";
+by (Blast_tac 1) ;
+qed "empty_iff";
Addsimps [empty_iff];
-qed_goal "emptyE" Set.thy "!!a. a:{} ==> P"
- (fn _ => [Full_simp_tac 1]);
+Goal "a:{} ==> P";
+by (Full_simp_tac 1);
+qed "emptyE";
AddSEs [emptyE];
-qed_goal "empty_subsetI" Set.thy "{} <= A"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "{} <= A";
+by (Blast_tac 1) ;
+qed "empty_subsetI";
(*One effect is to delete the ASSUMPTION {} <= A*)
AddIffs [empty_subsetI];
-qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
- (fn [prem]=>
- [ (blast_tac (claset() addIs [prem RS FalseE]) 1) ]);
+val [prem]= goal Set.thy "[| !!y. y:A ==> False |] ==> A={}";
+by (blast_tac (claset() addIs [prem RS FalseE]) 1) ;
+qed "equals0I";
(*Use for reasoning about disjointness: A Int B = {} *)
-qed_goal "equals0D" Set.thy "!!a. A={} ==> a ~: A"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "A={} ==> a ~: A";
+by (Blast_tac 1) ;
+qed "equals0D";
AddDs [equals0D, sym RS equals0D];
@@ -286,16 +295,20 @@
section "The Powerset operator -- Pow";
-qed_goalw "Pow_iff" Set.thy [Pow_def] "(A : Pow(B)) = (A <= B)"
- (fn _ => [ (Asm_simp_tac 1) ]);
+Goalw [Pow_def] "(A : Pow(B)) = (A <= B)";
+by (Asm_simp_tac 1);
+qed "Pow_iff";
AddIffs [Pow_iff];
-qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
- (fn _ => [ (etac CollectI 1) ]);
+Goalw [Pow_def] "!!A B. A <= B ==> A : Pow(B)";
+by (etac CollectI 1);
+qed "PowI";
-qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B"
- (fn _=> [ (etac CollectD 1) ]);
+Goalw [Pow_def] "!!A B. A : Pow(B) ==> A<=B";
+by (etac CollectD 1);
+qed "PowD";
+
val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
val Pow_top = subset_refl RS PowI; (* A : Pow(A) *)
@@ -341,10 +354,11 @@
qed "UnI2";
(*Classical introduction rule: no commitment to A vs B*)
-qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B"
- (fn prems=>
- [ (Simp_tac 1),
- (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
+
+val prems= goal Set.thy "(c~:B ==> c:A) ==> c : A Un B";
+by (Simp_tac 1);
+by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
+qed "UnCI";
val major::prems = Goalw [Un_def]
"[| c : A Un B; c:A ==> P; c:B ==> P |] ==> P";
@@ -392,19 +406,22 @@
Addsimps [Diff_iff];
-qed_goal "DiffI" Set.thy "!!c. [| c : A; c ~: B |] ==> c : A - B"
- (fn _=> [ Asm_simp_tac 1 ]);
+Goal "[| c : A; c ~: B |] ==> c : A - B";
+by (Asm_simp_tac 1) ;
+qed "DiffI";
-qed_goal "DiffD1" Set.thy "!!c. c : A - B ==> c : A"
- (fn _=> [ (Asm_full_simp_tac 1) ]);
+Goal "c : A - B ==> c : A";
+by (Asm_full_simp_tac 1) ;
+qed "DiffD1";
-qed_goal "DiffD2" Set.thy "!!c. [| c : A - B; c : B |] ==> P"
- (fn _=> [ (Asm_full_simp_tac 1) ]);
+Goal "[| c : A - B; c : B |] ==> P";
+by (Asm_full_simp_tac 1) ;
+qed "DiffD2";
-qed_goal "DiffE" Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P"
- (fn prems=>
- [ (resolve_tac prems 1),
- (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
+val prems= goal Set.thy "[| c : A - B; [| c:A; c~:B |] ==> P |] ==> P";
+by (resolve_tac prems 1);
+by (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ;
+qed "DiffE";
AddSIs [DiffI];
AddSEs [DiffE];
@@ -417,31 +434,34 @@
Addsimps [insert_iff];
-qed_goal "insertI1" Set.thy "a : insert a B"
- (fn _ => [Simp_tac 1]);
-
-qed_goal "insertI2" Set.thy "!!a. a : B ==> a : insert b B"
- (fn _=> [Asm_simp_tac 1]);
+val _ = goal Set.thy "a : insert a B";
+by (Simp_tac 1);
+qed "insertI1";
-qed_goalw "insertE" Set.thy [insert_def]
- "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P"
- (fn major::prems=>
- [ (rtac (major RS UnE) 1),
- (REPEAT (eresolve_tac (prems @ [CollectE]) 1)) ]);
+Goal "!!a. a : B ==> a : insert b B";
+by (Asm_simp_tac 1);
+qed "insertI2";
+
+val major::prems = Goalw [insert_def]
+ "[| a : insert b A; a=b ==> P; a:A ==> P |] ==> P";
+by (rtac (major RS UnE) 1);
+by (REPEAT (eresolve_tac (prems @ [CollectE]) 1));
+qed "insertE";
(*Classical introduction rule*)
-qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert b B"
- (fn prems=>
- [ (Simp_tac 1),
- (REPEAT (ares_tac (prems@[disjCI]) 1)) ]);
+val prems= goal Set.thy "(a~:B ==> a=b) ==> a: insert b B";
+by (Simp_tac 1);
+by (REPEAT (ares_tac (prems@[disjCI]) 1)) ;
+qed "insertCI";
AddSIs [insertCI];
AddSEs [insertE];
section "Singletons, using insert";
-qed_goal "singletonI" Set.thy "a : {a}"
- (fn _=> [ (rtac insertI1 1) ]);
+Goal "a : {a}";
+by (rtac insertI1 1) ;
+qed "singletonI";
Goal "b : {a} ==> b=a";
by (Blast_tac 1);
@@ -449,8 +469,9 @@
bind_thm ("singletonE", make_elim singletonD);
-qed_goal "singleton_iff" thy "(b : {a}) = (b=a)"
-(fn _ => [Blast_tac 1]);
+Goal "(b : {a}) = (b=a)";
+by (Blast_tac 1);
+qed "singleton_iff";
Goal "{a}={b} ==> a=b";
by (blast_tac (claset() addEs [equalityE]) 1);
--- a/src/HOL/Trancl.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Trancl.ML Thu Jul 15 10:27:54 1999 +0200
@@ -251,7 +251,7 @@
\ !!x y. (x,y) : r ==> P x y; \
\ !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z \
\ |] ==> P x y";
-by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
+by (blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
qed "trancl_trans_induct";
(*elimination of r^+ -- NOT an induction rule*)
@@ -326,13 +326,13 @@
qed "converse_trancl_induct";
(*Unused*)
-qed_goal "irrefl_tranclI" Trancl.thy
- "!!r. r^-1 Int r^+ = {} ==> (x, x) ~: r^+"
- (K [subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1,
- Fast_tac 1,
- strip_tac 1,
- etac trancl_induct 1,
- auto_tac (claset() addIs [r_into_trancl], simpset())]);
+Goal "r^-1 Int r^+ = {} ==> (x, x) ~: r^+";
+by (subgoal_tac "!y. (x, y) : r^+ --> x~=y" 1);
+by (Fast_tac 1);
+by (strip_tac 1);
+by (etac trancl_induct 1);
+by (auto_tac (claset() addIs [r_into_trancl], simpset()));
+qed "irrefl_tranclI";
Goal "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A";
by (etac rtrancl_induct 1);
@@ -368,10 +368,13 @@
qed "trancl_reflcl";
Addsimps[trancl_reflcl];
-qed_goal "trancl_empty" Trancl.thy "{}^+ = {}"
- (K [auto_tac (claset() addEs [trancl_induct], simpset())]);
+Goal "{}^+ = {}";
+by (auto_tac (claset() addEs [trancl_induct], simpset()));
+qed "trancl_empty";
Addsimps[trancl_empty];
-qed_goal "rtrancl_empty" Trancl.thy "{}^* = Id"
- (K [rtac (reflcl_trancl RS subst) 1, Simp_tac 1]);
+Goal "{}^* = Id";
+by (rtac (reflcl_trancl RS subst) 1);
+by (Simp_tac 1);
+qed "rtrancl_empty";
Addsimps[rtrancl_empty];
--- a/src/HOL/cladata.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/cladata.ML Thu Jul 15 10:27:54 1999 +0200
@@ -53,15 +53,15 @@
claset_ref() := HOL_cs;
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
-qed_goal "alt_ex1E" thy
+val major::prems = goal thy
"[| ?! x. P(x); \
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \
-\ |] ==> R"
- (fn major::prems =>
- [ (rtac (major RS ex1E) 1),
- (REPEAT (ares_tac (allI::prems) 1)),
- (etac (dup_elim allE) 1),
- (Fast_tac 1)]);
+\ |] ==> R";
+by (rtac (major RS ex1E) 1);
+by (REPEAT (ares_tac (allI::prems) 1));
+by (etac (dup_elim allE) 1);
+by (Fast_tac 1);
+qed "alt_ex1E";
AddSEs [alt_ex1E];
--- a/src/HOL/subset.ML Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/subset.ML Thu Jul 15 10:27:54 1999 +0200
@@ -9,8 +9,10 @@
(*** insert ***)
-qed_goal "subset_insertI" Set.thy "B <= insert a B"
- (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
+Goal "B <= insert a B";
+by (rtac subsetI 1);
+by (etac insertI2 1) ;
+qed "subset_insertI";
Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
by (Blast_tac 1);
@@ -89,8 +91,9 @@
(*** Set difference ***)
-qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)"
- (fn _ => [ (Blast_tac 1) ]);
+Goal "A-B <= (A::'a set)";
+by (Blast_tac 1) ;
+qed "Diff_subset";
(*** Monotonicity ***)