More tidying and removal of "\!\!... from Goal commands
--- a/src/HOL/Finite.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Finite.ML Wed Jul 15 14:19:02 1998 +0200
@@ -144,7 +144,7 @@
(** Sigma of finite sets **)
Goalw [Sigma_def]
- "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
+ "[| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
by (blast_tac (claset() addSIs [finite_UnionI]) 1);
bind_thm("finite_SigmaI", ballI RSN (2,result()));
Addsimps [finite_SigmaI];
@@ -212,7 +212,7 @@
qed "finite_has_card";
Goal
- "!!A.[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
+ "[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
\ ? m::nat. m<n & (? g. A = {g i|i. i<m})";
by (res_inst_tac [("n","n")] natE 1);
by (hyp_subst_tac 1);
@@ -303,7 +303,7 @@
val lemma = result();
Goalw [card_def]
- "!!A. [| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
+ "[| finite A; x ~: A |] ==> card(insert x A) = Suc(card A)";
by (etac lemma 1);
by (assume_tac 1);
qed "card_insert_disjoint";
@@ -396,8 +396,7 @@
(*Proper subsets*)
-Goalw [psubset_def]
- "!!B. finite B ==> !A. A < B --> card(A) < card(B)";
+Goalw [psubset_def] "finite B ==> !A. A < B --> card(A) < card(B)";
by (etac finite_induct 1);
by (Simp_tac 1);
by (Clarify_tac 1);
--- a/src/HOL/Fun.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Fun.ML Wed Jul 15 14:19:02 1998 +0200
@@ -109,7 +109,7 @@
qed "inj_on_contraD";
Goalw [inj_on_def]
- "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
+ "[| A<=B; inj_on f B |] ==> inj_on f A";
by (Blast_tac 1);
qed "subset_inj_on";
@@ -117,7 +117,7 @@
(*** Lemmas about inj ***)
Goalw [o_def]
- "!!f g. [| inj(f); inj_on g (range f) |] ==> inj(g o f)";
+ "[| inj(f); inj_on g (range f) |] ==> inj(g o f)";
by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
qed "comp_inj";
@@ -141,12 +141,12 @@
qed "inj_on_inv";
Goalw [inj_on_def]
- "!!f. [| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B";
+ "[| inj_on f C; A<=C; B<=C |] ==> f``(A Int B) = f``A Int f``B";
by (Blast_tac 1);
qed "inj_on_image_Int";
Goalw [inj_on_def]
- "!!f. [| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B";
+ "[| inj_on f C; A<=C; B<=C |] ==> f``(A-B) = f``A - f``B";
by (Blast_tac 1);
qed "inj_on_image_set_diff";
--- a/src/HOL/Gfp.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Gfp.ML Wed Jul 15 14:19:02 1998 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-For gfp.thy. The Knaster-Tarski Theorem for greatest fixed points.
+The Knaster-Tarski Theorem for greatest fixed points.
*)
open Gfp;
@@ -12,9 +12,8 @@
(* gfp(f) is the least upper bound of {u. u <= f(u)} *)
-val prems = goalw Gfp.thy [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
-by (rtac (CollectI RS Union_upper) 1);
-by (resolve_tac prems 1);
+Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)";
+by (etac (CollectI RS Union_upper) 1);
qed "gfp_upperbound";
val prems = goalw Gfp.thy [gfp_def]
@@ -40,10 +39,9 @@
(*** Coinduction rules for greatest fixed points ***)
(*weak version*)
-val prems = goal Gfp.thy
- "[| a: X; X <= f(X) |] ==> a : gfp(f)";
+Goal "[| a: X; X <= f(X) |] ==> a : gfp(f)";
by (rtac (gfp_upperbound RS subsetD) 1);
-by (REPEAT (ares_tac prems 1));
+by Auto_tac;
qed "weak_coinduct";
val [prem,mono] = goal Gfp.thy
@@ -56,8 +54,7 @@
qed "coinduct_lemma";
(*strong version, thanks to Coen & Frost*)
-Goal
- "!!X. [| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
+Goal "[| mono(f); a: X; X <= f(X Un gfp(f)) |] ==> a : gfp(f)";
by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1);
by (REPEAT (ares_tac [UnI1, Un_least] 1));
qed "coinduct";
@@ -129,16 +126,6 @@
qed "def_coinduct3";
(*Monotonicity of gfp!*)
-val prems = goal Gfp.thy
- "[| mono(f); !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
-by (rtac gfp_upperbound 1);
-by (rtac subset_trans 1);
-by (rtac gfp_lemma2 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-val gfp_mono = result();
-
-(*Monotonicity of gfp!*)
val [prem] = goal Gfp.thy "[| !!Z. f(Z)<=g(Z) |] ==> gfp(f) <= gfp(g)";
by (rtac (gfp_upperbound RS gfp_least) 1);
by (etac (prem RSN (2,subset_trans)) 1);
--- a/src/HOL/IOA/IOA.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/IOA/IOA.ML Wed Jul 15 14:19:02 1998 +0200
@@ -20,7 +20,7 @@
qed "ioa_triple_proj";
Goalw [ioa_def,state_trans_def,actions_def, is_asig_def]
- "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
+ "[| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:actions(asig_of(A))";
by (REPEAT(etac conjE 1));
by (EVERY1[etac allE, etac impE, atac]);
by (Asm_full_simp_tac 1);
@@ -118,7 +118,7 @@
(* Every state in an execution is reachable *)
Goalw [reachable_def]
-"!!A. ex:executions(A) ==> !n. reachable A (snd ex n)";
+"ex:executions(A) ==> !n. reachable A (snd ex n)";
by (Fast_tac 1);
qed "states_of_exec_reachable";
@@ -161,13 +161,13 @@
qed"externals_of_par";
Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
- "!! a. [| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
+ "[| compat_ioas A1 A2; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
by (Asm_full_simp_tac 1);
by (best_tac (claset() addEs [equalityCE]) 1);
qed"ext1_is_not_int2";
Goalw [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
- "!! a. [| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
+ "[| compat_ioas A2 A1 ; a:externals(asig_of(A1))|] ==> a~:internals(asig_of(A2))";
by (Asm_full_simp_tac 1);
by (best_tac (claset() addEs [equalityCE]) 1);
qed"ext2_is_not_int1";
--- a/src/HOL/Induct/Comb.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Induct/Comb.ML Wed Jul 15 14:19:02 1998 +0200
@@ -25,7 +25,7 @@
(*Strip lemma. The induction hyp is all but the last diamond of the strip.*)
Goalw [diamond_def]
- "!!r. [| diamond(r); (x,y):r^* |] ==> \
+ "[| diamond(r); (x,y):r^* |] ==> \
\ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
by (etac rtrancl_induct 1);
by (Blast_tac 1);
@@ -118,8 +118,7 @@
qed "S1_parcontractD";
AddSDs [S1_parcontractD];
-Goal
- "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
+Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
by (Blast_tac 1);
qed "S2_parcontractD";
AddSDs [S2_parcontractD];
--- a/src/HOL/Induct/Exp.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Induct/Exp.ML Wed Jul 15 14:19:02 1998 +0200
@@ -67,9 +67,8 @@
the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
functional on the argument (c,s).
*)
-Goal
- "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
-\ ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
+Goal "(c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
+\ ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
by (etac exec.induct 1);
by (ALLGOALS Full_simp_tac);
by (Blast_tac 3);
--- a/src/HOL/Induct/LList.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Induct/LList.ML Wed Jul 15 14:19:02 1998 +0200
@@ -32,7 +32,7 @@
***)
Goalw [list_Fun_def]
- "!!M. [| M : X; X <= list_Fun A (X Un llist(A)) |] ==> M : llist(A)";
+ "[| M : X; X <= list_Fun A (X Un llist(A)) |] ==> M : llist(A)";
by (etac llist.coinduct 1);
by (etac (subsetD RS CollectD) 1);
by (assume_tac 1);
@@ -44,7 +44,7 @@
AddIffs [list_Fun_NIL_I];
Goalw [list_Fun_def,CONS_def]
- "!!M N. [| M: A; N: X |] ==> CONS M N : list_Fun A X";
+ "[| M: A; N: X |] ==> CONS M N : list_Fun A X";
by (Fast_tac 1);
qed "list_Fun_CONS_I";
Addsimps [list_Fun_CONS_I];
@@ -52,7 +52,7 @@
(*Utilise the "strong" part, i.e. gfp(f)*)
Goalw (llist.defs @ [list_Fun_def])
- "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
+ "M: llist(A) ==> M : list_Fun A (X Un llist(A))";
by (etac (llist.mono RS gfp_fun_UnI2) 1);
qed "list_Fun_llist_I";
@@ -195,7 +195,7 @@
qed "LListD_Fun_mono";
Goalw [LListD_Fun_def]
- "!!M. [| M : X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M : LListD(r)";
+ "[| M : X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M : LListD(r)";
by (etac LListD.coinduct 1);
by (etac (subsetD RS CollectD) 1);
by (assume_tac 1);
@@ -206,13 +206,13 @@
qed "LListD_Fun_NIL_I";
Goalw [LListD_Fun_def,CONS_def]
- "!!x. [| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
+ "[| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
by (Fast_tac 1);
qed "LListD_Fun_CONS_I";
(*Utilise the "strong" part, i.e. gfp(f)*)
Goalw (LListD.defs @ [LListD_Fun_def])
- "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
+ "M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
by (etac (LListD.mono RS gfp_fun_UnI2) 1);
qed "LListD_Fun_LListD_I";
@@ -236,7 +236,7 @@
qed "LListD_eq_diag";
Goal
- "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
+ "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
by (rtac (LListD_eq_diag RS subst) 1);
by (rtac LListD_Fun_LListD_I 1);
by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
@@ -247,7 +247,7 @@
[also admits true equality]
Replace "A" by some particular set, like {x.True}??? *)
Goal
- "!!r. [| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
+ "[| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
\ |] ==> M=N";
by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
by (etac LListD_coinduct 1);
@@ -539,7 +539,7 @@
(*weak co-induction: bisimulation and case analysis on both variables*)
Goal
- "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+ "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac
[("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
by (Fast_tac 1);
@@ -552,7 +552,7 @@
(*strong co-induction: bisimulation and case analysis on one variable*)
Goal
- "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+ "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
by (etac imageI 1);
by (rtac image_subsetI 1);
@@ -620,7 +620,7 @@
(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
Goalw [LListD_Fun_def]
- "!!r A. r <= (llist A) Times (llist A) ==> \
+ "r <= (llist A) Times (llist A) ==> \
\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
by (stac llist_unfold 1);
by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
@@ -654,7 +654,7 @@
(*Surprisingly hard to prove. Used with lfilter*)
Goalw [llistD_Fun_def, prod_fun_def]
- "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
+ "A<=B ==> llistD_Fun A <= llistD_Fun B";
by Auto_tac;
by (rtac image_eqI 1);
by (fast_tac (claset() addss (simpset())) 1);
@@ -693,7 +693,7 @@
(*Utilise the "strong" part, i.e. gfp(f)*)
Goalw [llistD_Fun_def]
- "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
+ "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
by (rtac (Rep_llist_inverse RS subst) 1);
by (rtac prod_fun_imageI 1);
by (stac image_Un 1);
--- a/src/HOL/Induct/SList.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Induct/SList.ML Wed Jul 15 14:19:02 1998 +0200
@@ -165,12 +165,12 @@
(** pred_sexp lemmas **)
Goalw [CONS_def,In1_def]
- "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
+ "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
by (Asm_simp_tac 1);
qed "pred_sexp_CONS_I1";
Goalw [CONS_def,In1_def]
- "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
+ "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
by (Asm_simp_tac 1);
qed "pred_sexp_CONS_I2";
--- a/src/HOL/Induct/Simult.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Induct/Simult.ML Wed Jul 15 14:19:02 1998 +0200
@@ -56,7 +56,7 @@
(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
Goalw [Part_def]
- "!!A. ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
+ "! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
\ (M: Part (TF A) In1 --> Q(M)) \
\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
by (Blast_tac 1);
@@ -135,7 +135,7 @@
AddSEs [Scons_inject];
Goalw TF_Rep_defs
- "!!A. [| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
+ "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
by (Blast_tac 1);
qed "TCONS_I";
@@ -145,7 +145,7 @@
qed "FNIL_I";
Goalw TF_Rep_defs
- "!!A. [| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
+ "[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
\ FCONS M N : Part (TF A) In1";
by (Blast_tac 1);
qed "FCONS_I";
@@ -244,7 +244,7 @@
(** conversion rules for TF_rec **)
Goalw [TCONS_def]
- "!!M N. [| M: sexp; N: sexp |] ==> \
+ "[| M: sexp; N: sexp |] ==> \
\ TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
by (rtac (TF_rec_unfold RS trans) 1);
by (simp_tac (simpset() addsimps [Case_In0, Split]) 1);
@@ -257,7 +257,7 @@
qed "TF_rec_FNIL";
Goalw [FCONS_def]
- "!!M N. [| M: sexp; N: sexp |] ==> \
+ "[| M: sexp; N: sexp |] ==> \
\ TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
by (rtac (TF_rec_unfold RS trans) 1);
by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
--- a/src/HOL/Integ/Equiv.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Integ/Equiv.ML Wed Jul 15 14:19:02 1998 +0200
@@ -17,17 +17,17 @@
(** first half: equiv A r ==> r^-1 O r = r **)
Goalw [trans_def,sym_def,converse_def]
- "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
+ "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
by (Blast_tac 1);
qed "sym_trans_comp_subset";
Goalw [refl_def]
- "!!A r. refl A r ==> r <= r^-1 O r";
+ "refl A r ==> r <= r^-1 O r";
by (Blast_tac 1);
qed "refl_comp_subset";
Goalw [equiv_def]
- "!!A r. equiv A r ==> r^-1 O r = r";
+ "equiv A r ==> r^-1 O r = r";
by (Clarify_tac 1);
by (rtac equalityI 1);
by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
@@ -35,7 +35,7 @@
(*second half*)
Goalw [equiv_def,refl_def,sym_def,trans_def]
- "!!A r. [| r^-1 O r = r; Domain(r) = A |] ==> equiv A r";
+ "[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r";
by (etac equalityE 1);
by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
by (ALLGOALS Fast_tac);
@@ -45,7 +45,7 @@
(*Lemma for the next result*)
Goalw [equiv_def,trans_def,sym_def]
- "!!A r. [| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
+ "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
by (Blast_tac 1);
qed "equiv_class_subset";
@@ -56,24 +56,24 @@
qed "equiv_class_eq";
Goalw [equiv_def,refl_def]
- "!!A r. [| equiv A r; a: A |] ==> a: r^^{a}";
+ "[| equiv A r; a: A |] ==> a: r^^{a}";
by (Blast_tac 1);
qed "equiv_class_self";
(*Lemma for the next result*)
Goalw [equiv_def,refl_def]
- "!!A r. [| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r";
+ "[| equiv A r; r^^{b} <= r^^{a}; b: A |] ==> (a,b): r";
by (Blast_tac 1);
qed "subset_equiv_class";
Goal
- "!!A r. [| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r";
+ "[| r^^{a} = r^^{b}; equiv A r; b: A |] ==> (a,b): r";
by (REPEAT (ares_tac [equalityD2, subset_equiv_class] 1));
qed "eq_equiv_class";
(*thus r^^{a} = r^^{b} as well*)
Goalw [equiv_def,trans_def,sym_def]
- "!!A r. [| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
+ "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
by (Blast_tac 1);
qed "equiv_class_nondisjoint";
@@ -83,13 +83,13 @@
qed "equiv_type";
Goal
- "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
+ "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
by (blast_tac (claset() addSIs [equiv_class_eq]
addDs [eq_equiv_class, equiv_type]) 1);
qed "equiv_class_eq_iff";
Goal
- "!!A r. [| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
+ "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
by (blast_tac (claset() addSIs [equiv_class_eq]
addDs [eq_equiv_class, equiv_type]) 1);
qed "eq_equiv_class_iff";
@@ -112,12 +112,12 @@
qed "quotientE";
Goalw [equiv_def,refl_def,quotient_def]
- "!!A r. equiv A r ==> Union(A/r) = A";
+ "equiv A r ==> Union(A/r) = A";
by (blast_tac (claset() addSIs [equalityI]) 1);
qed "Union_quotient";
Goalw [quotient_def]
- "!!A r. [| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})";
+ "[| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})";
by (safe_tac (claset() addSIs [equiv_class_eq]));
by (assume_tac 1);
by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
@@ -178,12 +178,12 @@
Goalw [congruent_def,congruent2_def,equiv_def,refl_def]
- "!!A r. [| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)";
+ "[| equiv A r; congruent2 r b; a: A |] ==> congruent r (b a)";
by (Blast_tac 1);
qed "congruent2_implies_congruent";
Goalw [congruent_def]
- "!!A r. [| equiv A r; congruent2 r b; a: A |] ==> \
+ "[| equiv A r; congruent2 r b; a: A |] ==> \
\ congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
by (Clarify_tac 1);
by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
@@ -194,7 +194,7 @@
qed "congruent2_implies_congruent_UN";
Goal
- "!!A r. [| equiv A r; congruent2 r b; a1: A; a2: A |] \
+ "[| equiv A r; congruent2 r b; a1: A; a2: A |] \
\ ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
by (asm_simp_tac (simpset() addsimps [UN_equiv_class,
congruent2_implies_congruent,
@@ -252,7 +252,7 @@
qed "finite_quotient";
Goalw [quotient_def]
- "!!A. [| finite A; r <= A Times A; X : A/r |] ==> finite X";
+ "[| finite A; r <= A Times A; X : A/r |] ==> finite X";
by (rtac finite_subset 1);
by (assume_tac 2);
by (Blast_tac 1);
--- a/src/HOL/Integ/Integ.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Wed Jul 15 14:19:02 1998 +0200
@@ -551,7 +551,7 @@
(* Theorems about less and less_equal *)
Goalw [zless_def, znegative_def, zdiff_def, znat_def]
- "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
+ "w<z ==> ? n. z = w + $#(Suc(n))";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
by Safe_tac;
--- a/src/HOL/NatDef.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/NatDef.ML Wed Jul 15 14:19:02 1998 +0200
@@ -519,8 +519,7 @@
qed "Suc_leD";
(* stronger version of Suc_leD *)
-Goalw [le_def]
- "!!m. Suc m <= n ==> m < n";
+Goalw [le_def] "Suc m <= n ==> m < n";
by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
by (cut_facts_tac [less_linear] 1);
by (Blast_tac 1);
--- a/src/HOL/Real/Lubs.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Real/Lubs.ML Wed Jul 15 14:19:02 1998 +0200
@@ -42,12 +42,12 @@
qed "leastPD3";
Goalw [isLub_def,isUb_def,leastP_def]
- "!!x. isLub R S x ==> S *<= x";
+ "isLub R S x ==> S *<= x";
by (Step_tac 1);
qed "isLubD1";
Goalw [isLub_def,isUb_def,leastP_def]
- "!!x. isLub R S x ==> x: R";
+ "isLub R S x ==> x: R";
by (Step_tac 1);
qed "isLubD1a";
@@ -68,7 +68,7 @@
qed "isLubI1";
Goalw [isLub_def,leastP_def]
- "!!x. [| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x";
+ "[| isUb R S x; x <=* Collect (isUb R S) |] ==> isLub R S x";
by (Step_tac 1);
qed "isLubI2";
--- a/src/HOL/Real/PNat.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Real/PNat.ML Wed Jul 15 14:19:02 1998 +0200
@@ -241,7 +241,7 @@
(*** pnat_less ***)
Goalw [pnat_less_def]
- "!!x. [| x < (y::pnat); y < z |] ==> x < z";
+ "[| x < (y::pnat); y < z |] ==> x < z";
by ((etac less_trans 1) THEN assume_tac 1);
qed "pnat_less_trans";
@@ -259,7 +259,7 @@
bind_thm ("pnat_less_irrefl",pnat_less_not_refl RS notE);
Goalw [pnat_less_def]
- "!!x. x < (y::pnat) ==> x ~= y";
+ "x < (y::pnat) ==> x ~= y";
by Auto_tac;
qed "pnat_less_not_refl2";
@@ -279,7 +279,7 @@
bind_thm ("Rep_pnat_less_oneE",Rep_pnat_not_less_one RS notE);
Goalw [pnat_less_def]
- "!!x. x < (y::pnat) ==> Rep_pnat y ~= 1";
+ "x < (y::pnat) ==> Rep_pnat y ~= 1";
by (auto_tac (claset(),simpset()
addsimps [Rep_pnat_not_less_one] delsimps [less_one]));
qed "Rep_pnat_gt_implies_not0";
@@ -526,7 +526,7 @@
qed "pnat_add_less_mono";
Goalw [pnat_less_def]
- "!!f. [| !!i j::pnat. i<j ==> f(i) < f(j); \
+"!!f. [| !!i j::pnat. i<j ==> f(i) < f(j); \
\ i <= j \
\ |] ==> f(i) <= (f(j)::pnat)";
by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
--- a/src/HOL/Real/PRat.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Real/PRat.ML Wed Jul 15 14:19:02 1998 +0200
@@ -12,7 +12,7 @@
(*** Proving that ratrel is an equivalence relation ***)
Goal
- "!! x1. [| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
+ "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
\ ==> x1 * y3 = x3 * y1";
by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
@@ -30,7 +30,7 @@
qed "ratrel_iff";
Goalw [ratrel_def]
- "!!x1 x2. [| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
+ "[| x1 * y2 = x2 * y1 |] ==> ((x1,y1),(x2,y2)): ratrel";
by (Fast_tac 1);
qed "ratrelI";
@@ -143,8 +143,7 @@
by (simp_tac (simpset() addsimps [qinv]) 1);
qed "qinv_1";
-Goal
- "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
+Goal "!!(x1::pnat). [| x1 * y2 = x2 * y1 |] ==> \
\ (x * y1 + x1 * ya) * (ya * y2) = (x * y2 + x2 * ya) * (ya * y1)";
by (auto_tac (claset() addSIs [pnat_same_multI2],
simpset() addsimps [pnat_add_mult_distrib,
@@ -367,17 +366,15 @@
by (Fast_tac 1);
qed "prat_lessE_lemma";
-Goal
- "!! Q1. [| Q1 < (Q2::prat); \
-\ !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
-\ ==> P";
+Goal "!!P. [| Q1 < (Q2::prat); \
+\ !! (Q3::prat). Q1 + Q3 = Q2 ==> P |] \
+\ ==> P";
by (dtac (prat_lessE_lemma RS mp) 1);
by Auto_tac;
qed "prat_lessE";
(* qless is a strong order i.e nonreflexive and transitive *)
-Goal
- "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
+Goal "!!(q1::prat). [| q1 < q2; q2 < q3 |] ==> q1 < q3";
by (REPEAT(dtac (prat_lessE_lemma RS mp) 1));
by (REPEAT(etac exE 1));
by (hyp_subst_tac 1);
@@ -653,14 +650,14 @@
qed "not_less_not_eq_prat_less";
Goalw [prat_less_def]
- "!!x. [| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
+ "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::prat)";
by (REPEAT(etac exE 1));
by (res_inst_tac [("x","T+Ta")] exI 1);
by (auto_tac (claset(),simpset() addsimps prat_add_ac));
qed "prat_add_less_mono";
Goalw [prat_less_def]
- "!!x. [| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
+ "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::prat)";
by (REPEAT(etac exE 1));
by (res_inst_tac [("x","T*Ta+T*x2+x1*Ta")] exI 1);
by (auto_tac (claset(),simpset() addsimps prat_add_ac @
--- a/src/HOL/Real/PReal.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Real/PReal.ML Wed Jul 15 14:19:02 1998 +0200
@@ -50,21 +50,21 @@
qed "mem_Rep_preal_Ex";
Goalw [preal_def]
- "!!A. [| {} < A; A < {q::prat. True}; \
+ "[| {} < A; A < {q::prat. True}; \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? u: A. y < u))) |] ==> A : preal";
by (Fast_tac 1);
qed "prealI1";
Goalw [preal_def]
- "!!A. [| {} < A; A < {q::prat. True}; \
+ "[| {} < A; A < {q::prat. True}; \
\ !y: A. (!z. z < y --> z: A); \
\ !y: A. (? u: A. y < u) |] ==> A : preal";
by (Best_tac 1);
qed "prealI2";
Goalw [preal_def]
- "!!A. A : preal ==> {} < A & A < {q::prat. True} & \
+ "A : preal ==> {} < A & A < {q::prat. True} & \
\ (!y: A. ((!z. z < y --> z: A) & \
\ (? u: A. y < u)))";
by (Fast_tac 1);
@@ -76,38 +76,31 @@
Addsimps [Abs_preal_inverse];
-Goalw [preal_def]
- "!!A. A : preal ==> {} < A";
+Goalw [preal_def] "A : preal ==> {} < A";
by (Fast_tac 1);
qed "prealE_lemma1";
-Goalw [preal_def]
- "!!A. A : preal ==> A < {q::prat. True}";
+Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
by (Fast_tac 1);
qed "prealE_lemma2";
-Goalw [preal_def]
- "!!A. A : preal ==> !y: A. (!z. z < y --> z: A)";
+Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
by (Fast_tac 1);
qed "prealE_lemma3";
-Goal
- "!!A. [| A : preal; y: A |] ==> (!z. z < y --> z: A)";
+Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
qed "prealE_lemma3a";
-Goal
- "!!A. [| A : preal; y: A; z < y |] ==> z: A";
+Goal "[| A : preal; y: A; z < y |] ==> z: A";
by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
qed "prealE_lemma3b";
-Goalw [preal_def]
- "!!A. A : preal ==> !y: A. (? u: A. y < u)";
+Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
by (Fast_tac 1);
qed "prealE_lemma4";
-Goal
- "!!A. [| A : preal; y: A |] ==> ? u: A. y < u";
+Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
qed "prealE_lemma4a";
@@ -177,10 +170,9 @@
by (Fast_tac 1);
qed "preal_lessE_lemma";
-Goal
- "!! R1. [| R1 < (R2::preal); \
-\ (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
-\ ==> P";
+Goal "!!P. [| R1 < (R2::preal); \
+\ (Rep_preal(R1) < Rep_preal(R2)) ==> P |] \
+\ ==> P";
by (dtac (preal_lessE_lemma RS mp) 1);
by Auto_tac;
qed "preal_lessE";
@@ -445,14 +437,14 @@
(** lemmas **)
Goalw [preal_add_def]
- "!!R. z: Rep_preal(R+S) ==> \
+ "z: Rep_preal(R+S) ==> \
\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_addD";
Goalw [preal_add_def]
- "!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
+ "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
\ ==> z: Rep_preal(R+S)";
by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
@@ -464,14 +456,14 @@
qed "mem_Rep_preal_add_iff";
Goalw [preal_mult_def]
- "!!R. z: Rep_preal(R*S) ==> \
+ "z: Rep_preal(R*S) ==> \
\ ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
by (Fast_tac 1);
qed "mem_Rep_preal_multD";
Goalw [preal_mult_def]
- "!!R. ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
+ "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
\ ==> z: Rep_preal(R*S)";
by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
by (Fast_tac 1);
@@ -774,14 +766,14 @@
(*** Properties of <= ***)
Goalw [preal_le_def,psubset_def,preal_less_def]
- "!!w. z<=w ==> ~(w<(z::preal))";
+ "z<=w ==> ~(w<(z::preal))";
by (auto_tac (claset() addDs [equalityI],simpset()));
qed "preal_leD";
val preal_leE = make_elim preal_leD;
Goalw [preal_le_def,psubset_def,preal_less_def]
- "!!z. ~ z <= w ==> w<(z::preal)";
+ "~ z <= w ==> w<(z::preal)";
by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
by (auto_tac (claset(),simpset() addsimps [preal_less_def,psubset_def]));
qed "not_preal_leE";
@@ -795,7 +787,7 @@
qed "preal_less_le_iff";
Goalw [preal_le_def,preal_less_def,psubset_def]
- "!!z. z < w ==> z <= (w::preal)";
+ "z < w ==> z <= (w::preal)";
by (Fast_tac 1);
qed "preal_less_imp_le";
@@ -878,7 +870,7 @@
(** Part 1 of Dedekind sections def **)
Goalw [preal_less_def]
- "!!A. A < B ==> \
+ "A < B ==> \
\ ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
@@ -886,7 +878,7 @@
qed "lemma_ex_mem_less_left_add1";
Goal
- "!!A. A < B ==> \
+ "A < B ==> \
\ {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
by (dtac lemma_ex_mem_less_left_add1 1);
by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
@@ -1074,16 +1066,14 @@
Addsimps [preal_add_less_iff2];
-Goal
- "!!x1. [| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
+Goal "[| x1 < y1; x2 < y2 |] ==> x1 + x2 < y1 + (y2::preal)";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps preal_add_ac));
by (rtac (preal_add_assoc RS subst) 1);
by (rtac preal_self_less_add_right 1);
qed "preal_add_less_mono";
-Goal
- "!!x1. [| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
+Goal "[| x1 < y1; x2 < y2 |] ==> x1 * x2 < y1 * (y2::preal)";
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
simpset() addsimps [preal_add_mult_distrib,
preal_add_mult_distrib2,preal_self_less_add_left,
--- a/src/HOL/Real/Real.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Real/Real.ML Wed Jul 15 14:19:02 1998 +0200
@@ -8,8 +8,7 @@
(*** Proving that realrel is an equivalence relation ***)
-Goal
- "!! x1. [| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
+Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
\ ==> x1 + y3 = x3 + y1";
by (res_inst_tac [("C","y2")] preal_add_right_cancel 1);
by (rotate_tac 1 1 THEN dtac sym 1);
@@ -27,7 +26,7 @@
qed "realrel_iff";
Goalw [realrel_def]
- "!!x1 x2. [| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
+ "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
by (Fast_tac 1);
qed "realrelI";
@@ -504,13 +503,13 @@
qed "real_less_iff";
Goalw [real_less_def]
- "!!P. [| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
+ "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
\ (x2,y2):Rep_real(Q) |] ==> P < (Q::real)";
by (Fast_tac 1);
qed "real_lessI";
Goalw [real_less_def]
- "!! R1. [| R1 < (R2::real); \
+ "!!P. [| R1 < (R2::real); \
\ !!x1 x2 y1 y2. x1 + y2 < x2 + y1 ==> P; \
\ !!x1 y1. (x1,y1::preal):Rep_real(R1) ==> P; \
\ !!x2 y2. (x2,y2::preal):Rep_real(R2) ==> P |] \
@@ -519,7 +518,7 @@
qed "real_lessE";
Goalw [real_less_def]
- "!!R1. R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
+ "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
\ (x1,y1::preal):Rep_real(R1) & \
\ (x2,y2):Rep_real(R2))";
by (Fast_tac 1);
@@ -636,7 +635,7 @@
by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
qed "real_preal_trichotomy";
-Goal "!!x. [| !!m. x = %#m ==> P; \
+Goal "!!P. [| !!m. x = %#m ==> P; \
\ x = 0r ==> P; \
\ !!m. x = %~(%#m) ==> P |] ==> P";
by (cut_inst_tac [("x","x")] real_preal_trichotomy 1);
@@ -781,9 +780,8 @@
real_preal_zero_less,real_preal_minus_less_all]));
qed "real_linear";
-Goal
- "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \
-\ R2 < R1 ==> P |] ==> P";
+Goal "!!(R1::real). [| R1 < R2 ==> P; R1 = R2 ==> P; \
+\ R2 < R1 ==> P |] ==> P";
by (cut_inst_tac [("R1.0","R1"),("R2.0","R2")] real_linear 1);
by Auto_tac;
qed "real_linear_less2";
@@ -1172,7 +1170,7 @@
qed "real_le_add_order";
Goal
- "!!x. [| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
+ "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
by (dtac (real_less_iffdef RS iffD2) 1);
by (dtac (real_less_iffdef RS iffD2) 1);
by (rtac (real_less_iffdef RS iffD1) 1);
@@ -1456,8 +1454,7 @@
(*------------------------------------------------------------------
lemmas about upper bounds and least upper bound
------------------------------------------------------------------*)
-Goalw [real_ub_def]
- "!!S. [| real_ub u S; x : S |] ==> x <= u";
+Goalw [real_ub_def] "[| real_ub u S; x : S |] ==> x <= u";
by Auto_tac;
qed "real_ubD";
--- a/src/HOL/Relation.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Relation.ML Wed Jul 15 14:19:02 1998 +0200
@@ -29,7 +29,7 @@
(** Composition of two relations **)
Goalw [comp_def]
- "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
+ "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
by (Blast_tac 1);
qed "compI";
@@ -72,8 +72,7 @@
by (Blast_tac 1);
qed "comp_mono";
-Goal
- "!!r s. [| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C";
+Goal "[| s <= A Times B; r <= B Times C |] ==> (r O s) <= A Times C";
by (Blast_tac 1);
qed "comp_subset_Sigma";
@@ -84,8 +83,7 @@
by (REPEAT (ares_tac (prems@[allI,impI]) 1));
qed "transI";
-Goalw [trans_def]
- "!!r. [| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
+Goalw [trans_def] "[| trans(r); (a,b):r; (b,c):r |] ==> (a,c):r";
by (Blast_tac 1);
qed "transD";
--- a/src/HOL/Set.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Set.ML Wed Jul 15 14:19:02 1998 +0200
@@ -681,8 +681,7 @@
by (Blast_tac 1);
qed "psubsetI";
-Goalw [psubset_def]
- "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
+Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
by Auto_tac;
qed "psubset_insertD";
--- a/src/HOL/Sum.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Sum.ML Wed Jul 15 14:19:02 1998 +0200
@@ -166,8 +166,7 @@
(** Rules for the Part primitive **)
-Goalw [Part_def]
- "!!a b A h. [| a : A; a=h(b) |] ==> a : Part A h";
+Goalw [Part_def] "[| a : A; a=h(b) |] ==> a : Part A h";
by (Blast_tac 1);
qed "Part_eqI";
--- a/src/HOL/Trancl.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Trancl.ML Wed Jul 15 14:19:02 1998 +0200
@@ -281,7 +281,7 @@
bind_thm ("trancl_trans", trans_trancl RS transD);
Goalw [trancl_def]
- "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
+ "[| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
by (blast_tac (claset() addIs [rtrancl_trans,r_into_rtrancl]) 1);
qed "rtrancl_trancl_trancl";
@@ -329,8 +329,7 @@
by (Blast_tac 1);
val lemma = result();
-Goalw [trancl_def]
- "!!r. r <= A Times A ==> r^+ <= A Times A";
+Goalw [trancl_def] "r <= A Times A ==> r^+ <= A Times A";
by (blast_tac (claset() addSDs [lemma]) 1);
qed "trancl_subset_Sigma";
--- a/src/HOL/Univ.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/Univ.ML Wed Jul 15 14:19:02 1998 +0200
@@ -73,7 +73,7 @@
qed "Node_K0_I";
Goalw [Node_def,Push_def]
- "!!p. p: Node ==> apfst (Push i) p : Node";
+ "p: Node ==> apfst (Push i) p : Node";
by (blast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
qed "Node_Push_I";
@@ -489,7 +489,7 @@
(*** Equality for Cartesian Product ***)
Goalw [dprod_def]
- "!!r s. [| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
+ "[| (M,M'):r; (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
by (Blast_tac 1);
qed "dprodI";
--- a/src/HOL/W0/Type.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/W0/Type.ML Wed Jul 15 14:19:02 1998 +0200
@@ -8,7 +8,7 @@
(* mgu does not introduce new type variables *)
Goalw [new_tv_def]
- "!! n. [|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
+ "[|mgu t1 t2 = Ok u; new_tv n t1; new_tv n t2|] ==> \
\ new_tv n u";
by (fast_tac (set_cs addDs [mgu_free]) 1);
qed "mgu_new";
@@ -56,7 +56,7 @@
Addsimps [free_tv_id_subst];
Goalw [dom_def,cod_def,UNION_def,Bex_def]
- "!!v. [| v : free_tv(s n); v~=n |] ==> v : cod s";
+ "[| v : free_tv(s n); v~=n |] ==> v : cod s";
by (Simp_tac 1);
by (safe_tac (empty_cs addSIs [exI,conjI,notI]));
by (assume_tac 2);
@@ -190,7 +190,7 @@
Addsimps [lessI RS less_imp_le RS new_tv_list_le];
Goal
- "!! n. [| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
+ "[| n<=m; new_tv n (s::subst) |] ==> new_tv m s";
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
by (rtac conjI 1);
by (slow_tac (HOL_cs addIs [le_trans]) 1);
@@ -203,7 +203,7 @@
(* new_tv property remains if a substitution is applied *)
Goal
- "!!n. [| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
+ "[| n<m; new_tv m (s::subst) |] ==> new_tv m (s n)";
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
qed "new_tv_subst_var";
@@ -233,13 +233,13 @@
(* composition of substitutions preserves new_tv proposition *)
Goal
- "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
+ "[| new_tv n (s::subst); new_tv n r |] ==> \
\ new_tv n (($ r) o s)";
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
qed "new_tv_subst_comp_1";
Goal
- "!! n. [| new_tv n (s::subst); new_tv n r |] ==> \
+ "[| new_tv n (s::subst); new_tv n r |] ==> \
\ new_tv n (%v.$ r (s v))";
by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1);
qed "new_tv_subst_comp_2";
@@ -248,7 +248,7 @@
(* new type variables do not occur freely in a type structure *)
Goalw [new_tv_def]
- "!!n. new_tv n ts ==> n~:(free_tv ts)";
+ "new_tv n ts ==> n~:(free_tv ts)";
by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
qed "new_tv_not_free_tv";
Addsimps [new_tv_not_free_tv];
@@ -285,8 +285,7 @@
by (fast_tac (HOL_cs addss simpset()) 1);
qed_spec_mp "eq_free_eq_subst_te";
-Goal
- "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
+Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
by (list.induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
@@ -294,8 +293,7 @@
by (fast_tac (HOL_cs addIs [eq_subst_te_eq_free] addss (simpset())) 1);
qed_spec_mp "eq_subst_tel_eq_free";
-Goal
- "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
+Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
by (list.induct_tac "ts" 1);
(* case [] *)
by (fast_tac (HOL_cs addss simpset()) 1);
@@ -305,29 +303,26 @@
(* some useful theorems *)
Goalw [free_tv_subst]
- "!!v. v : cod s ==> v : free_tv s";
+ "v : cod s ==> v : free_tv s";
by (fast_tac set_cs 1);
qed "codD";
Goalw [free_tv_subst,dom_def]
- "!! x. x ~: free_tv s ==> s x = TVar x";
+ "x ~: free_tv s ==> s x = TVar x";
by (fast_tac set_cs 1);
qed "not_free_impl_id";
-Goalw [new_tv_def]
- "!! n. [| new_tv n t; m:free_tv t |] ==> m<n";
+Goalw [new_tv_def] "[| new_tv n t; m:free_tv t |] ==> m<n";
by (fast_tac HOL_cs 1 );
qed "free_tv_le_new_tv";
-Goal
- "free_tv (s (v::nat)) <= insert v (cod s)";
+Goal "free_tv (s (v::nat)) <= insert v (cod s)";
by (expand_case_tac "v:dom s" 1);
by (fast_tac (set_cs addss (simpset() addsimps [cod_def])) 1);
by (fast_tac (set_cs addss (simpset() addsimps [dom_def])) 1);
qed "free_tv_subst_var";
-Goal
- "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
+Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
by (typ.induct_tac "t" 1);
(* case TVar n *)
by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
@@ -335,8 +330,7 @@
by (fast_tac (set_cs addss simpset()) 1);
qed "free_tv_app_subst_te";
-Goal
- "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
+Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
by (list.induct_tac "ts" 1);
(* case [] *)
by (Simp_tac 1);
--- a/src/HOL/W0/W.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/W0/W.ML Wed Jul 15 14:19:02 1998 +0200
@@ -10,8 +10,7 @@
Delsimps (ex_simps @ all_simps);
(* correctness of W with respect to has_type *)
-Goal
- "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
+Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
by (expr.induct_tac "e" 1);
(* case Var n *)
by (Asm_simp_tac 1);
@@ -41,8 +40,7 @@
(* the resulting type variable is always greater or equal than the given one *)
-Goal
- "!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
+Goal "!a n s t m. W e a n = Ok (s,t,m) --> n<=m";
by (expr.induct_tac "e" 1);
(* case Var(n) *)
by (fast_tac (HOL_cs addss simpset()) 1);
@@ -72,8 +70,7 @@
Addsimps [W_var_ge];
-Goal
- "!! s. Ok (s,t,m) = W e a n ==> n<=m";
+Goal "Ok (s,t,m) = W e a n ==> n<=m";
by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
qed "W_var_geD";
@@ -152,8 +149,7 @@
qed_spec_mp "new_tv_W";
-Goal
- "!n a s t m v. W e a n = Ok (s,t,m) --> \
+Goal "!n a s t m v. W e a n = Ok (s,t,m) --> \
\ (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
by (expr.induct_tac "e" 1);
(* case Var n *)
@@ -361,8 +357,7 @@
by (Fast_tac 1);
qed_spec_mp "W_complete_lemma";
-Goal
- "!!e. [] |- e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \
+Goal "[] |- e :: t' ==> (? s t. (? m. W e [] n = Ok(s,t,m)) & \
\ (? r. t' = $r t))";
by (cut_inst_tac [("a","[]"),("s'","id_subst"),("e","e"),("t'","t'")]
W_complete_lemma 1);
--- a/src/HOL/WF.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/WF.ML Wed Jul 15 14:19:02 1998 +0200
@@ -79,7 +79,7 @@
val lemma1 = result();
Goalw [wf_def]
- "!!r. (! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
+ "(! Q x. x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)) ==> wf r";
by (Clarify_tac 1);
by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1);
by (Blast_tac 1);
@@ -140,7 +140,7 @@
"!!r. !x. (x, x) ~: r^+ ==> acyclic r" (K [atac 1]);
Goalw [acyclic_def]
- "!!r. wf r ==> acyclic r";
+ "wf r ==> acyclic r";
by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
qed "wf_acyclic";
@@ -171,7 +171,7 @@
(*** is_recfun ***)
Goalw [is_recfun_def,cut_def]
- "!!f. [| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary";
+ "[| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary";
by (etac ssubst 1);
by (asm_simp_tac HOL_ss 1);
qed "is_recfun_undef";
@@ -261,7 +261,7 @@
(trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun)));
Goalw [wfrec_def]
- "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+ "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
by (rtac H_cong 1);
by (rtac refl 2);
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
@@ -297,7 +297,7 @@
(*--------------Old proof-----------------------------------------------------
Goalw [wfrec_def]
- "!!r. wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
+ "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a";
by (etac (wf_trancl RS wftrec RS ssubst) 1);
by (rtac trans_trancl 1);
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*)
--- a/src/HOL/equalities.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/equalities.ML Wed Jul 15 14:19:02 1998 +0200
@@ -86,7 +86,7 @@
"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
Goal
- "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
+ "A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
by (Blast_tac 1);
qed "UN_insert_distrib";
@@ -477,8 +477,7 @@
qed "INT_insert";
Addsimps[INT_insert];
-Goal
- "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
+Goal "A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
by (Blast_tac 1);
qed "INT_insert_distrib";
--- a/src/HOL/ex/MT.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/ex/MT.ML Wed Jul 15 14:19:02 1998 +0200
@@ -27,17 +27,15 @@
by (simp_tac (simpset() addsimps prems) 1);
qed "infsys_p1";
-val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
+Goal "P (fst (a,b)) (snd (a,b)) ==> P a b";
by (Asm_full_simp_tac 1);
qed "infsys_p2";
-val prems = goal MT.thy
- "!!a. P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
+Goal "P a b c ==> P (fst(fst((a,b),c))) (snd(fst ((a,b),c))) (snd ((a,b),c))";
by (Asm_full_simp_tac 1);
qed "infsys_pp1";
-val prems = goal MT.thy
- "!!a. P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
+Goal "P (fst(fst((a,b),c))) (snd(fst((a,b),c))) (snd((a,b),c)) ==> P a b c";
by (Asm_full_simp_tac 1);
qed "infsys_pp2";
@@ -154,51 +152,46 @@
by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_const";
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+Goalw [eval_def, eval_rel_def]
"ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev";
-by (cut_facts_tac prems 1);
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_var2";
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+Goalw [eval_def, eval_rel_def]
"ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)";
-by (cut_facts_tac prems 1);
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_fn";
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+Goalw [eval_def, eval_rel_def]
" cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \
\ ve |- fix ev2(ev1) = e ---> v_clos(cl)";
-by (cut_facts_tac prems 1);
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_fix";
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+Goalw [eval_def, eval_rel_def]
" [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \
\ ve |- e1 @ e2 ---> v_const(c_app c1 c2)";
-by (cut_facts_tac prems 1);
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_app1";
-val prems = goalw MT.thy [eval_def, eval_rel_def]
+Goalw [eval_def, eval_rel_def]
" [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \
\ ve |- e2 ---> v2; \
\ vem + {xm |-> v2} |- em ---> v \
\ |] ==> \
\ ve |- e1 @ e2 ---> v";
-by (cut_facts_tac prems 1);
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
@@ -270,7 +263,7 @@
(* Introduction rules *)
Goalw [elab_def, elab_rel_def]
- "!!te. c isof ty ==> te |- e_const(c) ===> ty";
+ "c isof ty ==> te |- e_const(c) ===> ty";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
@@ -278,7 +271,7 @@
qed "elab_const";
Goalw [elab_def, elab_rel_def]
- "!!te. x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
+ "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
@@ -286,7 +279,7 @@
qed "elab_var";
Goalw [elab_def, elab_rel_def]
- "!!te. te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
+ "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
@@ -294,7 +287,7 @@
qed "elab_fn";
Goalw [elab_def, elab_rel_def]
- "!!te. te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
+ "te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \
\ te |- fix f(x) = e ===> ty1->ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
@@ -303,7 +296,7 @@
qed "elab_fix";
Goalw [elab_def, elab_rel_def]
- "!!te. [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
+ "[| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \
\ te |- e1 @ e2 ===> ty2";
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
@@ -425,8 +418,7 @@
by (elab_e_elim_tac prems);
qed "elab_const_elim_lem";
-val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t";
-by (cut_facts_tac prems 1);
+Goal "te |- e_const(c) ===> t ==> c isof t";
by (dtac elab_const_elim_lem 1);
by (Blast_tac 1);
qed "elab_const_elim";
@@ -436,9 +428,7 @@
by (elab_e_elim_tac prems);
qed "elab_var_elim_lem";
-val prems = goal MT.thy
- "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
-by (cut_facts_tac prems 1);
+Goal "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)";
by (dtac elab_var_elim_lem 1);
by (Blast_tac 1);
qed "elab_var_elim";
@@ -451,10 +441,9 @@
by (elab_e_elim_tac prems);
qed "elab_fn_elim_lem";
-val prems = goal MT.thy
+Goal
" te |- fn x1 => e1 ===> t ==> \
\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)";
-by (cut_facts_tac prems 1);
by (dtac elab_fn_elim_lem 1);
by (Blast_tac 1);
qed "elab_fn_elim";
@@ -466,10 +455,9 @@
by (elab_e_elim_tac prems);
qed "elab_fix_elim_lem";
-val prems = goal MT.thy
+Goal
" te |- fix ev1(ev2) = e1 ===> t ==> \
\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)";
-by (cut_facts_tac prems 1);
by (dtac elab_fix_elim_lem 1);
by (Blast_tac 1);
qed "elab_fix_elim";
@@ -480,9 +468,8 @@
by (elab_e_elim_tac prems);
qed "elab_app_elim_lem";
-val prems = goal MT.thy
+Goal
"te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)";
-by (cut_facts_tac prems 1);
by (dtac elab_app_elim_lem 1);
by (Blast_tac 1);
qed "elab_app_elim";
@@ -505,9 +492,7 @@
(* First strong indtroduction (co-induction) rule for hasty_rel *)
-val prems =
Goalw [hasty_rel_def] "c isof t ==> (v_const(c),t) : hasty_rel";
-by (cut_facts_tac prems 1);
by (rtac gfp_coind2 1);
by (rewtac MT.hasty_fun_def);
by (rtac CollectI 1);
@@ -518,7 +503,7 @@
(* Second strong introduction (co-induction) rule for hasty_rel *)
-val prems = goalw MT.thy [hasty_rel_def]
+Goalw [hasty_rel_def]
" [| te |- fn ev => e ===> t; \
\ ve_dom(ve) = te_dom(te); \
\ ! ev1. \
@@ -526,7 +511,6 @@
\ (ve_app ve ev1,te_app te ev1) : {(v_clos(<|ev,e,ve|>),t)} Un hasty_rel \
\ |] ==> \
\ (v_clos(<|ev,e,ve|>),t) : hasty_rel";
-by (cut_facts_tac prems 1);
by (rtac gfp_coind2 1);
by (rewtac hasty_fun_def);
by (rtac CollectI 1);
@@ -579,7 +563,7 @@
qed "hasty_const";
Goalw [hasty_def,hasty_env_def]
- "!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
+ "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
by (rtac hasty_rel_clos_coind 1);
by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
qed "hasty_clos";
@@ -587,7 +571,7 @@
(* Elimination on constants for hasty *)
Goalw [hasty_def]
- "!!v. v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
+ "v hasty t ==> (!c.(v = v_const(c) --> c isof t))";
by (rtac hasty_rel_elim 1);
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_const_lem";
@@ -599,17 +583,16 @@
(* Elimination on closures for hasty *)
-val prems = goalw MT.thy [hasty_env_def,hasty_def]
+Goalw [hasty_env_def,hasty_def]
" v hasty t ==> \
\ ! x e ve. \
\ v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
-by (cut_facts_tac prems 1);
by (rtac hasty_rel_elim 1);
by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
qed "hasty_elim_clos_lem";
Goal
- "!!t. v_clos(<|ev,e,ve|>) hasty t ==> \
+ "v_clos(<|ev,e,ve|>) hasty t ==> \
\ ? te. te |- fn ev => e ===> t & ve hastyenv te ";
by (dtac hasty_elim_clos_lem 1);
by (Blast_tac 1);
@@ -620,7 +603,7 @@
(* ############################################################ *)
Goal
- "!!ve. [| ve hastyenv te; v hasty t |] ==> \
+ "[| ve hastyenv te; v hasty t |] ==> \
\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
by (rewtac hasty_env_def);
by (asm_full_simp_tac (simpset() delsimps mem_simps
@@ -637,27 +620,27 @@
(* ############################################################ *)
Goal
- "!!t. [| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
+ "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t";
by (dtac elab_const_elim 1);
by (etac hasty_const 1);
qed "consistency_const";
Goalw [hasty_env_def]
- "!!t. [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
+ "[| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \
\ ve_app ve ev hasty t";
by (dtac elab_var_elim 1);
by (Blast_tac 1);
qed "consistency_var";
Goal
- "!!t. [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
+ "[| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \
\ v_clos(<| ev, e, ve |>) hasty t";
by (rtac hasty_clos 1);
by (Blast_tac 1);
qed "consistency_fn";
Goalw [hasty_env_def,hasty_def]
- "!!t. [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
+ "[| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \
\ ve hastyenv te ; \
\ te |- fix ev2 ev1 = e ===> t \
\ |] ==> \
@@ -684,7 +667,7 @@
qed "consistency_fix";
Goal
- "!!t. [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
+ "[| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t;\
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \
\ ve hastyenv te ; te |- e1 @ e2 ===> t \
\ |] ==> \
@@ -700,7 +683,7 @@
qed "consistency_app1";
Goal
- "!!t. [| ! t te. \
+ "[| ! t te. \
\ ve hastyenv te --> \
\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \
\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \
@@ -726,13 +709,13 @@
by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
qed "consistency_app2";
-val [major] = goal MT.thy
+Goal
"ve |- e ---> v ==> \
\ (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)";
(* Proof by induction on the structure of evaluations *)
-by (rtac (major RS eval_ind) 1);
+by (etac eval_ind 1);
by Safe_tac;
by (DEPTH_SOLVE
(ares_tac [consistency_const, consistency_var, consistency_fn,
@@ -743,9 +726,8 @@
(* The Basic Consistency theorem *)
(* ############################################################ *)
-val prems = goalw MT.thy [isof_env_def,hasty_env_def]
+Goalw [isof_env_def,hasty_env_def]
"ve isofenv te ==> ve hastyenv te";
-by (cut_facts_tac prems 1);
by Safe_tac;
by (etac allE 1);
by (etac impE 1);
@@ -756,9 +738,8 @@
by (Asm_simp_tac 1);
qed "basic_consistency_lem";
-val prems = goal MT.thy
+Goal
"[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t";
-by (cut_facts_tac prems 1);
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
--- a/src/HOL/ex/Primes.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/ex/Primes.ML Wed Jul 15 14:19:02 1998 +0200
@@ -90,7 +90,7 @@
(*USED??*)
Goalw [is_gcd_def]
- "!!m n. [| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
+ "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m";
by (Blast_tac 1);
qed "is_gcd_dvd";
--- a/src/HOL/ex/Primrec.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/ex/Primrec.ML Wed Jul 15 14:19:02 1998 +0200
@@ -195,9 +195,8 @@
(** COMP case **)
-Goal
- "!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
-\ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
+Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
+\ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
by (etac lists.induct 1);
by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
by Safe_tac;
@@ -206,9 +205,9 @@
qed "COMP_map_lemma";
Goalw [COMP_def]
- "!!g. [| ALL l. g l < ack(kg, list_add l); \
-\ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
-\ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)";
+ "[| ALL l. g l < ack(kg, list_add l); \
+\ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
+\ |] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)";
by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1);
by (etac (COMP_map_lemma RS exE) 1);
by (rtac exI 1);
@@ -221,9 +220,9 @@
(** PREC case **)
Goalw [PREC_def]
- "!!f g. [| ALL l. f l + list_add l < ack(kf, list_add l); \
-\ ALL l. g l + list_add l < ack(kg, list_add l) \
-\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
+ "[| ALL l. f l + list_add l < ack(kf, list_add l); \
+\ ALL l. g l + list_add l < ack(kg, list_add l) \
+\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
by (exhaust_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [less_trans]) 1);
@@ -244,10 +243,9 @@
by (etac ack_less_mono2 1);
qed "PREC_case_lemma";
-Goal
- "!!f g. [| ALL l. f l < ack(kf, list_add l); \
-\ ALL l. g l < ack(kg, list_add l) \
-\ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
+Goal "[| ALL l. f l < ack(kf, list_add l); \
+\ ALL l. g l < ack(kg, list_add l) \
+\ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
by (rtac exI 1);
by (rtac allI 1);
by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
--- a/src/HOL/ex/Qsort.ML Wed Jul 15 14:13:18 1998 +0200
+++ b/src/HOL/ex/Qsort.ML Wed Jul 15 14:19:02 1998 +0200
@@ -49,8 +49,7 @@
qed "sorted_append";
Addsimps [sorted_append];
-Goal
- "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)";
+Goal "[| total(le); transf(le) |] ==> sorted le (qsort le xs)";
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
by (ALLGOALS Asm_simp_tac);
by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);