# HG changeset patch # User paulson # Date 900505142 -7200 # Node ID 74919e8f221cc29210707f41b35407bd14f4f8bf # Parent 8258771906189b6a37520fb11806137fd97a4cea More tidying and removal of "\!\!... from Goal commands diff -r 825877190618 -r 74919e8f221c src/HOL/Finite.ML --- 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 \ + "[| x ~: A; insert x A = {f i|i. i \ \ ? m::nat. m 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Fun.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Gfp.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/IOA/IOA.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Induct/Comb.ML --- 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]; diff -r 825877190618 -r 74919e8f221c src/HOL/Induct/Exp.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Induct/LList.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Induct/SList.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Induct/Simult.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Integ/Equiv.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Integ/Integ.ML --- 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 ? n. z = w + $#(Suc(n))"; + "w ? 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; diff -r 825877190618 -r 74919e8f221c src/HOL/NatDef.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/Real/Lubs.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Real/PNat.ML --- 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 f(i) < f(j); \ +"!!f. [| !!i j::pnat. i f(i) < f(j); \ \ i <= j \ \ |] ==> f(i) <= (f(j)::pnat)"; by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD], diff -r 825877190618 -r 74919e8f221c src/HOL/Real/PRat.ML --- 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 @ diff -r 825877190618 -r 74919e8f221c src/HOL/Real/PReal.ML --- 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, diff -r 825877190618 -r 74919e8f221c src/HOL/Real/Real.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Relation.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Set.ML --- 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} (x ~: A) & A<=B | x:A & A-{x} a : Part A h"; +Goalw [Part_def] "[| a : A; a=h(b) |] ==> a : Part A h"; by (Blast_tac 1); qed "Part_eqI"; diff -r 825877190618 -r 74919e8f221c src/HOL/Trancl.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/Univ.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/W0/Type.ML --- 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 new_tv m (s n)"; + "[| n 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 m $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 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); diff -r 825877190618 -r 74919e8f221c src/HOL/WF.ML --- 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*) diff -r 825877190618 -r 74919e8f221c src/HOL/equalities.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/ex/MT.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/ex/Primes.ML --- 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"; diff -r 825877190618 -r 74919e8f221c src/HOL/ex/Primrec.ML --- 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); diff -r 825877190618 -r 74919e8f221c src/HOL/ex/Qsort.ML --- 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]);