--- a/Arith.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Arith.ML Wed Jun 29 12:04:04 1994 +0200
@@ -53,14 +53,14 @@
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"
+val add_assoc = prove_goal 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"
+val add_commute = prove_goal 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"
+val add_left_commute = prove_goal 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]);
@@ -82,25 +82,25 @@
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"
+val mult_commute = prove_goal 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"
+val add_mult_distrib = prove_goal 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"
+val add_mult_distrib2 = prove_goal 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"
+val mult_assoc = prove_goal 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"
+val mult_left_commute = prove_goal 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]);
@@ -112,7 +112,7 @@
(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. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS(asm_simp_tac arith_ss));
@@ -223,14 +223,14 @@
(**** Additional theorems about "less than" ****)
-goal Arith.thy "n <= (m + n)::nat";
+goal Arith.thy "n <= ((m + n)::nat)";
by (nat_ind_tac "m" 1);
by (ALLGOALS(simp_tac arith_ss));
by (etac le_trans 1);
by (rtac (lessI RS less_imp_le) 1);
val le_add2 = result();
-goal Arith.thy "n <= (n + m)::nat";
+goal Arith.thy "n <= ((n + m)::nat)";
by (simp_tac (arith_ss addsimps add_ac) 1);
by (rtac le_add2 1);
val le_add1 = result();
@@ -238,7 +238,7 @@
val less_add_Suc1 = standard (lessI RS (le_add1 RS le_less_trans));
val less_add_Suc2 = standard (lessI RS (le_add2 RS le_less_trans));
-goal Arith.thy "m+k<=n --> m<=n::nat";
+goal Arith.thy "m+k<=n --> m<=(n::nat)";
by (nat_ind_tac "k" 1);
by (ALLGOALS (asm_simp_tac arith_ss));
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
--- a/HOL.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/HOL.ML Wed Jun 29 12:04:04 1994 +0200
@@ -103,7 +103,7 @@
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
val cong = prove_goal HOL.thy
- "[| f = g; x::'a = y |] ==> f(x) = g(y)"
+ "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
(fn [prem1,prem2] =>
[rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
--- a/HOL.thy Fri Jun 24 15:11:39 1994 +0200
+++ b/HOL.thy Wed Jun 29 12:04:04 1994 +0200
@@ -93,9 +93,9 @@
(* Basic Rules *)
- refl "t = t::'a"
+ refl "t = (t::'a)"
subst "[| s = t; P(s) |] ==> P(t::'a)"
- ext "(!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))"
+ ext "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
selectI "P(x::'a) ==> P(@x.P(x))"
impI "(P ==> Q) ==> P-->Q"
--- a/LList.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/LList.ML Wed Jun 29 12:04:04 1994 +0200
@@ -715,7 +715,7 @@
"[| f(LNil)=g(LNil); \
\ !!x l. <f(LCons(x,l)),g(LCons(x,l))> : \
\ llistD_Fun(range(%u. <f(u),g(u)>) Un range(%v. <v,v>)) \
-\ |] ==> f(l) = g(l :: 'a llist) :: 'b llist";
+\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
by (res_inst_tac [("r", "range(%u. <f(u),g(u)>)")] llist_equalityI 1);
by (rtac rangeI 1);
by (rtac subsetI 1);
--- a/Nat.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Nat.ML Wed Jun 29 12:04:04 1994 +0200
@@ -196,7 +196,7 @@
(** Introduction properties **)
-val prems = goalw Nat.thy [less_def] "[| i<j; j<k |] ==> i<k::nat";
+val prems = goalw Nat.thy [less_def] "[| i<j; j<k |] ==> i<(k::nat)";
by (rtac (trans_trancl RS transD) 1);
by (resolve_tac prems 1);
by (resolve_tac prems 1);
@@ -218,14 +218,14 @@
(** Elimination properties **)
-val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<n::nat";
+val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
val less_not_sym = result();
(* [| n<m; m<n |] ==> R *)
val less_asym = standard (less_not_sym RS notE);
-goalw Nat.thy [less_def] "~ n<n::nat";
+goalw Nat.thy [less_def] "~ n<(n::nat)";
by (rtac notI 1);
by (etac (wf_pred_nat RS wf_trancl RS wf_anti_refl) 1);
val less_not_refl = result();
@@ -233,7 +233,7 @@
(* n<n ==> R *)
val less_anti_refl = standard (less_not_refl RS notE);
-goal Nat.thy "!!m. n<m ==> m ~= n::nat";
+goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
val less_not_refl2 = result();
@@ -318,7 +318,7 @@
val not_Suc_n_less_n = result();
(*"Less than" is a linear ordering*)
-goal Nat.thy "m<n | m=n | n<m::nat";
+goal Nat.thy "m<n | m=n | n<(m::nat)";
by (nat_ind_tac "m" 1);
by (nat_ind_tac "n" 1);
by (rtac (refl RS disjI1 RS disjI2) 1);
@@ -364,17 +364,17 @@
"m=n ==> nat_rec(m,a,f) = nat_rec(n,a,f)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
-val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=n::nat";
+val prems = goalw Nat.thy [le_def] "~(n<m) ==> m<=(n::nat)";
by (resolve_tac prems 1);
val leI = result();
-val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<m::nat)";
+val prems = goalw Nat.thy [le_def] "m<=n ==> ~(n<(m::nat))";
by (resolve_tac prems 1);
val leD = result();
val leE = make_elim leD;
-goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<m::nat";
+goalw Nat.thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
by (fast_tac HOL_cs 1);
val not_leE = result();
@@ -388,40 +388,40 @@
by(fast_tac HOL_cs 1);
val Suc_leD = result();
-goalw Nat.thy [le_def] "!!m. m < n ==> m <= n::nat";
+goalw Nat.thy [le_def] "!!m. m < n ==> m <= (n::nat)";
by (fast_tac (HOL_cs addEs [less_asym]) 1);
val less_imp_le = result();
-goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=n::nat";
+goalw Nat.thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
by (cut_facts_tac [less_linear] 1);
by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
val le_imp_less_or_eq = result();
-goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <= n::nat";
+goalw Nat.thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
by (cut_facts_tac [less_linear] 1);
by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
by (flexflex_tac);
val less_or_eq_imp_le = result();
-goal Nat.thy "(x <= y::nat) = (x < y | x=y)";
+goal Nat.thy "(x <= (y::nat)) = (x < y | x=y)";
by (REPEAT(ares_tac [iffI,less_or_eq_imp_le,le_imp_less_or_eq] 1));
val le_eq_less_or_eq = result();
-goal Nat.thy "n <= n::nat";
+goal Nat.thy "n <= (n::nat)";
by(simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
val le_refl = result();
-val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < k::nat";
+val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
by (dtac le_imp_less_or_eq 1);
by (fast_tac (HOL_cs addIs [less_trans]) 1);
val le_less_trans = result();
-goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= k::nat";
+goal Nat.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
rtac less_or_eq_imp_le, fast_tac (HOL_cs addIs [less_trans])]);
val le_trans = result();
-val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = n::nat";
+val prems = goal Nat.thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
fast_tac (HOL_cs addEs [less_anti_refl,less_asym])]);
val le_anti_sym = result();
--- a/Nat.thy Fri Jun 24 15:11:39 1994 +0200
+++ b/Nat.thy Wed Jun 29 12:04:04 1994 +0200
@@ -49,7 +49,7 @@
less_def "m<n == <m,n>:trancl(pred_nat)"
- le_def "m<=n::nat == ~(n<m)"
+ le_def "m<=(n::nat) == ~(n<m)"
nat_rec_def "nat_rec(n,c,d) == wfrec(pred_nat, n, \
\ %l g. nat_case(l, c, %m. d(m,g(m))))"
--- a/Set.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Set.ML Wed Jun 29 12:04:04 1994 +0200
@@ -117,10 +117,10 @@
(*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"
+val subset_refl = prove_goal 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";
+val prems = goal Set.thy "[| A<=B; B<=C |] ==> A<=(C::'a set)";
by (cut_facts_tac prems 1);
by (REPEAT (ares_tac [subsetI] 1 ORELSE set_mp_tac 1));
val subset_trans = result();
@@ -129,25 +129,25 @@
(*** Equality ***)
(*Anti-symmetry of the subset relation*)
-val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = B::'a set";
+val prems = goal Set.thy "[| A <= B; B <= A |] ==> A = (B::'a set)";
by (rtac (iffI RS set_ext) 1);
by (REPEAT (ares_tac (prems RL [subsetD]) 1));
val subset_antisym = result();
val equalityI = subset_antisym;
(* Equality rules from ZF set theory -- are they appropriate here? *)
-val prems = goal Set.thy "A = B ==> A<=B::'a set";
+val prems = goal Set.thy "A = B ==> A<=(B::'a set)";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
val equalityD1 = result();
-val prems = goal Set.thy "A = B ==> B<=A::'a set";
+val prems = goal Set.thy "A = B ==> B<=(A::'a set)";
by (resolve_tac (prems RL [subst]) 1);
by (rtac subset_refl 1);
val equalityD2 = result();
val prems = goal Set.thy
- "[| A = B; [| A<=B; B<=A::'a set |] ==> P |] ==> P";
+ "[| A = B; [| A<=B; B<=(A::'a set) |] ==> P |] ==> P";
by (resolve_tac prems 1);
by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
val equalityE = result();
--- a/Subst/Setplus.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Subst/Setplus.ML Wed Jun 29 12:04:04 1994 +0200
@@ -20,7 +20,7 @@
by (rtac refl 1);
val ssubset_iff = result();
-goal Setplus.thy "(A::'a set <= B) = ((A < B) | (A=B))";
+goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))";
by (simp_tac (set_ss addsimps [ssubset_iff]) 1);
by (fast_tac set_cs 1);
val subseteq_iff_subset_eq = result();
--- a/Trancl.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/Trancl.ML Wed Jun 29 12:04:04 1994 +0200
@@ -151,7 +151,7 @@
"[| <a::'a,b> : r^*; (a = b) ==> P; \
\ !!y.[| <a,y> : r^*; <y,b> : r |] ==> P \
\ |] ==> P";
-by (subgoal_tac "a::'a = b | (? y. <a,y> : r^* & <y,b> : r)" 1);
+by (subgoal_tac "(a::'a) = b | (? y. <a,y> : r^* & <y,b> : r)" 1);
by (rtac (major RS rtrancl_induct) 2);
by (fast_tac (set_cs addIs prems) 2);
by (fast_tac (set_cs addIs prems) 2);
--- a/equalities.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/equalities.ML Wed Jun 29 12:04:04 1994 +0200
@@ -307,7 +307,7 @@
by (fast_tac eq_cs 1);
val Diff_partition = result();
-goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = A :: 'a set";
+goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
by (fast_tac eq_cs 1);
val double_diff = result();
--- a/ex/cla.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/cla.ML Wed Jun 29 12:04:04 1994 +0200
@@ -336,8 +336,8 @@
writeln"Problem 43 NOT PROVED AUTOMATICALLY";
goal HOL.thy
- "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = p(z,y)::bool)) \
-\ --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+ "(! x::'a. ! y::'a. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \
+\ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
writeln"Problem 44";
--- a/ex/mesontest.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/mesontest.ML Wed Jun 29 12:04:04 1994 +0200
@@ -75,8 +75,8 @@
writeln"Problem 43 NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool)) \
-\ --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \
+\ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
by (rtac ccontr 1);
val [prem43] = gethyps 1;
val nnf43 = make_nnf prem43;
@@ -161,7 +161,7 @@
result();
(*11. Proved in each direction (incorrectly, says Pelletier!!) *)
-goal HOL.thy "P=P::bool";
+goal HOL.thy "P=(P::bool)";
by (safe_meson_tac 1);
result();
@@ -404,8 +404,8 @@
result();
writeln"Problem 43 NOW PROVED AUTOMATICALLY!!";
-goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = p(z,y)::bool)) \
-\ --> (! x. (! y. q(x,y) = q(y,x)::bool))";
+goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \
+\ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))";
by (safe_meson_tac 1);
result();
--- a/ex/set.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/ex/set.ML Wed Jun 29 12:04:04 1994 +0200
@@ -109,7 +109,7 @@
by (fast_tac (set_cs addEs [inj_ontoD, f_eq_gE]) 1);
val bij_if_then_else = result();
-goal Lfp.thy "? X. X = Compl(g``Compl(f:: 'a=>'b``X))";
+goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))";
by (rtac exI 1);
by (rtac lfp_Tarski 1);
by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1));
--- a/subset.ML Fri Jun 24 15:11:39 1994 +0200
+++ b/subset.ML Wed Jun 29 12:04:04 1994 +0200
@@ -117,7 +117,7 @@
(*** Set difference ***)
-val Diff_subset = prove_goal Set.thy "A-B <= A::'a set"
+val Diff_subset = prove_goal Set.thy "A-B <= (A::'a set)"
(fn _ => [ (REPEAT (ares_tac [subsetI] 1 ORELSE etac DiffE 1)) ]);
(*** Monotonicity ***)