--- a/Arith.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Arith.ML Fri Nov 25 09:12:16 1994 +0100
@@ -21,13 +21,13 @@
val diff_0 = diff_def RS def_nat_rec_0;
-val diff_0_eq_0 = prove_goalw Arith.thy [diff_def, pred_def]
+qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
"0 - n = 0"
(fn _ => [nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *)
-val diff_Suc_Suc = prove_goalw Arith.thy [diff_def, pred_def]
+qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def]
"Suc(m) - Suc(n) = m - n"
(fn _ =>
[simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]);
@@ -44,23 +44,23 @@
(*** Addition ***)
-val add_0_right = prove_goal Arith.thy "m + 0 = m"
+qed_goal "add_0_right" Arith.thy "m + 0 = m"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val add_Suc_right = prove_goal Arith.thy "m + Suc(n) = Suc(m+n)"
+qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
(*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "(m + n) + k = m + ((n + k)::nat)"
+qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Commutative law for addition*)
-val add_commute = prove_goal Arith.thy "m + n = n + (m::nat)"
+qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+((x+z)::nat)"
+qed_goal "add_left_commute" Arith.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]);
@@ -71,36 +71,36 @@
(*** Multiplication ***)
(*right annihilation in product*)
-val mult_0_right = prove_goal Arith.thy "m * 0 = 0"
+qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*right Sucessor law for multiplication*)
-val mult_Suc_right = prove_goal Arith.thy "m * Suc(n) = m + (m * n)"
+qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)"
(fn _ => [nat_ind_tac "m" 1,
ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
(*Commutative law for multiplication*)
-val mult_commute = prove_goal Arith.thy "m * n = n * (m::nat)"
+qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]);
(*addition distributes over multiplication*)
-val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
+qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
(fn _ => [nat_ind_tac "m" 1,
ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
-val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
+qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
(fn _ => [nat_ind_tac "m" 1,
ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
(*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * ((n * k)::nat)"
+qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*((x*z)::nat)"
+qed_goal "mult_left_commute" Arith.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]);
@@ -108,7 +108,7 @@
(*** Difference ***)
-val diff_self_eq_0 = prove_goal Arith.thy "m - m = 0"
+qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
--- a/Nat.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Nat.ML Fri Nov 25 09:12:16 1994 +0100
@@ -354,11 +354,11 @@
val nat_ss0 = sum_ss addsimps nat_simps;
(*Prevents simplification of f and g: much faster*)
-val nat_case_weak_cong = prove_goal Nat.thy
+qed_goal "nat_case_weak_cong" Nat.thy
"m=n ==> nat_case(a,f,m) = nat_case(a,f,n)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
-val nat_rec_weak_cong = prove_goal Nat.thy
+qed_goal "nat_rec_weak_cong" Nat.thy
"m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
--- a/Prod.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Prod.ML Fri Nov 25 09:12:16 1994 +0100
@@ -67,7 +67,7 @@
qed "Pair_fst_snd_eq";
(*Prevents simplification of c: much faster*)
-val split_weak_cong = prove_goal Prod.thy
+qed_goal "split_weak_cong" Prod.thy
"p=q ==> split(c,p) = split(c,q)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
@@ -152,12 +152,12 @@
(*** Disjoint union of a family of sets - Sigma ***)
-val SigmaI = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaI" Prod.thy [Sigma_def]
"[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
(fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
(*The general elimination rule*)
-val SigmaE = prove_goalw Prod.thy [Sigma_def]
+qed_goalw "SigmaE" Prod.thy [Sigma_def]
"[| c: Sigma(A,B); \
\ !!x y.[| x:A; y:B(x); c=<x,y> |] ==> P \
\ |] ==> P"
@@ -166,17 +166,17 @@
(REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
(** Elimination of <a,b>:A*B -- introduces no eigenvariables **)
-val SigmaD1 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> a : A"
+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)) ]);
-val SigmaD2 = prove_goal Prod.thy "<a,b> : Sigma(A,B) ==> b : B(a)"
+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)) ]);
-val SigmaE2 = prove_goal Prod.thy
+qed_goal "SigmaE2" Prod.thy
"[| <a,b> : Sigma(A,B); \
\ [| a:A; b:B(a) |] ==> P \
\ |] ==> P"
--- a/Set.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Set.ML Fri Nov 25 09:12:16 1994 +0100
@@ -55,7 +55,7 @@
by (REPEAT (ares_tac (prems @ [exI,conjI]) 1));
qed "bexI";
-val bexCI = prove_goal Set.thy
+qed_goal "bexCI" Set.thy
"[| ! x:A. ~P(x) ==> P(a); a:A |] ==> ? x:A.P(x)"
(fn prems=>
[ (rtac classical 1),
@@ -104,7 +104,7 @@
qed "subsetD";
(*The same, with reversed premises for use with etac -- cf rev_mp*)
-val rev_subsetD = prove_goal Set.thy "[| c:A; A <= B |] ==> c:B"
+qed_goal "rev_subsetD" Set.thy "[| c:A; A <= B |] ==> c:B"
(fn prems=> [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]);
(*Classical elimination rule*)
@@ -117,7 +117,7 @@
(*Takes assumptions A<=B; c:A and creates the assumption c:B *)
fun set_mp_tac i = etac subsetCE i THEN mp_tac i;
-val subset_refl = prove_goal Set.thy "A <= (A::'a set)"
+qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
(fn _=> [ (REPEAT (ares_tac [subsetI] 1)) ]);
val prems = goal Set.thy "[| A<=B; B<=C |] ==> A<=(C::'a set)";
@@ -197,7 +197,7 @@
qed "UnI2";
(*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"
+qed_goal "UnCI" Set.thy "(c~:B ==> c:A) ==> c : A Un B"
(fn prems=>
[ (rtac classical 1),
(REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -235,76 +235,76 @@
(*** Set difference ***)
-val DiffI = prove_goalw Set.thy [set_diff_def]
+qed_goalw "DiffI" Set.thy [set_diff_def]
"[| c : A; c ~: B |] ==> c : A - B"
(fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]);
-val DiffD1 = prove_goalw Set.thy [set_diff_def]
+qed_goalw "DiffD1" Set.thy [set_diff_def]
"c : A - B ==> c : A"
(fn [major]=> [ (rtac (major RS CollectD RS conjunct1) 1) ]);
-val DiffD2 = prove_goalw Set.thy [set_diff_def]
+qed_goalw "DiffD2" Set.thy [set_diff_def]
"[| c : A - B; c : B |] ==> P"
(fn [major,minor]=>
[rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]);
-val DiffE = prove_goal Set.thy
+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 Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & c~:B)"
+qed_goal "Diff_iff" Set.thy "(c : A-B) = (c:A & c~:B)"
(fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
(*** The empty set -- {} ***)
-val emptyE = prove_goalw Set.thy [empty_def] "a:{} ==> P"
+qed_goalw "emptyE" Set.thy [empty_def] "a:{} ==> P"
(fn [prem] => [rtac (prem RS CollectD RS FalseE) 1]);
-val empty_subsetI = prove_goal Set.thy "{} <= A"
+qed_goal "empty_subsetI" Set.thy "{} <= A"
(fn _ => [ (REPEAT (ares_tac [equalityI,subsetI,emptyE] 1)) ]);
-val equals0I = prove_goal Set.thy "[| !!y. y:A ==> False |] ==> A={}"
+qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
(fn prems=>
[ (REPEAT (ares_tac (prems@[empty_subsetI,subsetI,equalityI]) 1
ORELSE eresolve_tac (prems RL [FalseE]) 1)) ]);
-val equals0D = prove_goal Set.thy "[| A={}; a:A |] ==> P"
+qed_goal "equals0D" Set.thy "[| A={}; a:A |] ==> P"
(fn [major,minor]=>
[ (rtac (minor RS (major RS equalityD1 RS subsetD RS emptyE)) 1) ]);
(*** Augmenting a set -- insert ***)
-val insertI1 = prove_goalw Set.thy [insert_def] "a : insert(a,B)"
+qed_goalw "insertI1" Set.thy [insert_def] "a : insert(a,B)"
(fn _ => [rtac (CollectI RS UnI1) 1, rtac refl 1]);
-val insertI2 = prove_goalw Set.thy [insert_def] "a : B ==> a : insert(b,B)"
+qed_goalw "insertI2" Set.thy [insert_def] "a : B ==> a : insert(b,B)"
(fn [prem]=> [ (rtac (prem RS UnI2) 1) ]);
-val insertE = prove_goalw Set.thy [insert_def]
+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)) ]);
-val insert_iff = prove_goal Set.thy "a : insert(b,A) = (a=b | a:A)"
+qed_goal "insert_iff" Set.thy "a : insert(b,A) = (a=b | a:A)"
(fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
(*Classical introduction rule*)
-val insertCI = prove_goal Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)"
+qed_goal "insertCI" Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)"
(fn [prem]=>
[ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
(etac prem 1) ]);
(*** Singletons, using insert ***)
-val singletonI = prove_goal Set.thy "a : {a}"
+qed_goal "singletonI" Set.thy "a : {a}"
(fn _=> [ (rtac insertI1 1) ]);
-val singletonE = prove_goal Set.thy "[| a: {b}; a=b ==> P |] ==> P"
+qed_goal "singletonE" Set.thy "[| a: {b}; a=b ==> P |] ==> P"
(fn major::prems=>
[ (rtac (major RS insertE) 1),
(REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
@@ -437,10 +437,10 @@
(*** Powerset ***)
-val PowI = prove_goalw Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
+qed_goalw "PowI" Set.thy [Pow_def] "!!A B. A <= B ==> A : Pow(B)"
(fn _ => [ (etac CollectI 1) ]);
-val PowD = prove_goalw Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B"
+qed_goalw "PowD" Set.thy [Pow_def] "!!A B. A : Pow(B) ==> A<=B"
(fn _=> [ (etac CollectD 1) ]);
val Pow_bottom = empty_subsetI RS PowI; (* {}: Pow(B) *)
--- a/Sum.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/Sum.ML Fri Nov 25 09:12:16 1994 +0100
@@ -161,7 +161,7 @@
sum_case_Inl, sum_case_Inr];
(*Prevents simplification of f and g: much faster*)
-val sum_case_weak_cong = prove_goal Sum.thy
+qed_goal "sum_case_weak_cong" Sum.thy
"s=t ==> sum_case(f,g,s) = sum_case(f,g,t)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
--- a/subset.ML Thu Nov 24 20:31:09 1994 +0100
+++ b/subset.ML Fri Nov 25 09:12:16 1994 +0100
@@ -9,7 +9,7 @@
(*** insert ***)
-val subset_insertI = prove_goal Set.thy "B <= insert(a,B)"
+qed_goal "subset_insertI" Set.thy "B <= insert(a,B)"
(fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
(*** Big Union -- least upper bound of a set ***)
@@ -117,7 +117,7 @@
(*** Set difference ***)
-val Diff_subset = prove_goal Set.thy "A-B <= (A::'a set)"
+qed_goal "Diff_subset" Set.thy "A-B <= (A::'a set)"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
(*** Monotonicity ***)