# HG changeset patch
# User paulson
# Date 920456118 -3600
# Node ID 08245f5a436d564ce4389dc4476981a05766cc63
# Parent  3815b5b095cb2d757a7597368a754da0dc9a3372
expandshort

diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Arith.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -105,13 +105,13 @@
 AddIffs [zero_is_add];
 
 Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
-by(exhaust_tac "m" 1);
-by(Auto_tac);
+by (exhaust_tac "m" 1);
+by (Auto_tac);
 qed "add_is_1";
 
 Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
-by(exhaust_tac "m" 1);
-by(Auto_tac);
+by (exhaust_tac "m" 1);
+by (Auto_tac);
 qed "one_is_add";
 
 Goal "(0<m+n) = (0<m | 0<n)";
@@ -185,7 +185,7 @@
 Goal "i+j < (k::nat) --> i<k";
 by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
-by(blast_tac (claset() addDs [Suc_lessD]) 1);
+by (blast_tac (claset() addDs [Suc_lessD]) 1);
 qed_spec_mp "add_lessD1";
 
 Goal "~ (i+j < (i::nat))";
@@ -972,10 +972,10 @@
 
 (* Elimination of `-' on nat due to John Harrison *)
 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
-by(case_tac "a <= b" 1);
-by(Auto_tac);
-by(eres_inst_tac [("x","b-a")] allE 1);
-by(Auto_tac);
+by (case_tac "a <= b" 1);
+by (Auto_tac);
+by (eres_inst_tac [("x","b-a")] allE 1);
+by (Auto_tac);
 qed "nat_diff_split";
 
 (* FIXME: K true should be replaced by a sensible test to speed things up
@@ -995,75 +995,75 @@
 (*** Subtraction laws -- mostly from Clemens Ballarin ***)
 
 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_less_mono";
 
 Goal "a+b < (c::nat) ==> a < c-b";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "add_less_imp_less_diff";
 
 Goal "(i < j-k) = (i+k < (j::nat))";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "less_diff_conv";
 
 Goal "(j-k <= (i::nat)) = (j <= i+k)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "le_diff_conv";
 
 Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "le_diff_conv2";
 
 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "Suc_diff_Suc";
 
 Goal "i <= (n::nat) ==> n - (n - i) = i";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_diff_cancel";
 Addsimps [diff_diff_cancel];
 
 Goal "k <= (n::nat) ==> m <= n + m - k";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "le_add_diff";
 
 Goal "[| 0<k; j<i |] ==> j+k-i < k";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "add_diff_less";
 
 Goal "m-1 < n ==> m <= n";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "pred_less_imp_le";
 
 Goal "j<=i ==> i - j < Suc i - j";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_less_Suc_diff";
 
 Goal "i - j <= Suc i - j";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_le_Suc_diff";
 AddIffs [diff_le_Suc_diff];
 
 Goal "n - Suc i <= n - i";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_Suc_le_diff";
 AddIffs [diff_Suc_le_diff];
 
 Goal "0 < n ==> (m <= n-1) = (m<n)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "le_pred_eq";
 
 Goal "0 < n ==> (m-1 < n) = (m<=n)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "less_pred_eq";
 
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
 Goal "[| 0<n; ~ m<n |] ==> m - n < m";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_less";
 
 Goal "[| 0<n; n<=m |] ==> m - n < m";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "le_diff_less";
 
 
@@ -1072,19 +1072,19 @@
 
 (* Monotonicity of subtraction in first argument *)
 Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_le_mono";
 
 Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_le_mono2";
 
 
 (*This proof requires natdiff_cancel_sums*)
 Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diff_less_mono2";
 
 Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "diffs0_imp_equal";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Fun.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -213,6 +213,14 @@
 by Auto_tac;
 qed "inv_image_comp";
 
+Goal "inj f ==> (f a : f``A) = (a : A)";
+by (blast_tac (claset() addDs [injD]) 1);
+qed "inj_image_mem_iff";
+
+Goal "inj f ==> (f``A = f``B) = (A = B)";
+by (blast_tac (claset() addSEs [equalityE] addDs [injD]) 1);
+qed "inj_image_eq_iff";
+
 val set_cs = claset() delrules [equalityI];
 
 
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Induct/Acc.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -45,7 +45,7 @@
 
 Goal "!x. x : acc(r) ==> wf(r)";
 by (rtac wfUNIVI 1);
-by(deepen_tac (claset() addEs [acc_induct]) 1 1);
+by (deepen_tac (claset() addEs [acc_induct]) 1 1);
 qed "acc_wfI";
 
 Goal "wf(r) ==> x : acc(r)";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Induct/Multiset0.ML
--- a/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -7,5 +7,5 @@
 *)
 
 Goal "(%x.0) : {f. finite {x. 0 < f x}}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "multiset_witness";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Integ/Bin.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -500,33 +500,33 @@
 
 (* Some test data
 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
 \     ==> a+a <= j+j";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
 \     ==> a+a - - #-1 < j+j - #3";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
-by(arith_tac 1);
+by (arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a <= l";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a <= l+l+l+l";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a <= l+l+l+l+i";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 *)
 
 (*---------------------------------------------------------------------------*)
@@ -548,50 +548,50 @@
 (** Simplification of inequalities involving numerical constants **)
 
 Goal "(w <= z + #1) = (w<=z | w = z + #1)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "zle_add1_eq";
 
 Goal "(w <= z - #1) = (w<z)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "zle_diff1_eq";
 Addsimps [zle_diff1_eq];
 
 (*2nd premise can be proved automatically if v is a literal*)
 Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zle_imp_zle_zadd";
 
 Goal "w <= z ==> w <= z + #1";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zle_imp_zle_zadd1";
 
 (*2nd premise can be proved automatically if v is a literal*)
 Goal "[| w < z; #0 <= v |] ==> w < z + v";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zless_imp_zless_zadd";
 
 Goal "w < z ==> w < z + #1";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zless_imp_zless_zadd1";
 
 Goal "(w < z + #1) = (w<=z)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "zle_add1_eq_le";
 Addsimps [zle_add1_eq_le];
 
 Goal "(z = z + w) = (w = #0)";
-by(arith_tac 1);
+by (arith_tac 1);
 qed "zadd_left_cancel0";
 Addsimps [zadd_left_cancel0];
 
 (*LOOPS as a simprule!*)
 Goal "[| w + v < z; #0 <= v |] ==> w < z";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zless_zadd_imp_zless";
 
 (*LOOPS as a simprule!  Analogous to Suc_lessD*)
 Goal "w + #1 < z ==> w < z";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 qed "zless_zadd1_imp_zless";
 
 Goal "w + #-1 = w - #1";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Lambda/Eta.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -28,8 +28,8 @@
 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
 by (induct_tac "t" 1);
   by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
- by(arith_tac 1);
-by(Auto_tac);
+ by (arith_tac 1);
+by (Auto_tac);
 qed "free_lift";
 Addsimps [free_lift];
 
@@ -115,7 +115,7 @@
 
 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
 by (induct_tac "t" 1);
-by(auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
+by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
 
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Lambda/ListApplication.ML
--- a/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Lambda/ListApplication.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -88,7 +88,7 @@
 Addsimps [size_apps];
 
 Goal "[| 0 < k; m <= n |] ==> m < n+k";
-by(fast_arith_tac 1);
+by (fast_arith_tac 1);
 val lemma = result();
 
 (* a customized induction schema for $$ *)
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Lex/NA.ML
--- a/src/HOL/Lex/NA.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Lex/NA.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -7,23 +7,23 @@
 Goal
  "steps A (v@w) = steps A w  O  steps A v";
 by (induct_tac "v" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed "steps_append";
 Addsimps [steps_append];
 
 Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
-by(rtac (steps_append RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (steps_append RS equalityE) 1);
+by (Blast_tac 1);
 qed "in_steps_append";
 AddIffs [in_steps_append];
 
 Goal
  "!p. delta A w p = {q. (p,q) : steps A w}";
-by(induct_tac "w" 1);
-by(auto_tac (claset(), simpset() addsimps [step_def]));
+by (induct_tac "w" 1);
+by (auto_tac (claset(), simpset() addsimps [step_def]));
 qed_spec_mp "delta_conv_steps";
 
 Goalw [accepts_def]
  "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
-by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
+by (simp_tac (simpset() addsimps [delta_conv_steps]) 1);
 qed "accepts_conv_steps";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Map.ML
--- a/src/HOL/Map.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Map.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -120,7 +120,7 @@
 	Asm_full_simp_tac 1]);
 
 Goalw [dom_def] "dom(m++n) = dom n Un dom m";
-by(Simp_tac 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "dom_override";
 Addsimps [dom_override];
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Nat.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -39,8 +39,8 @@
 AddIffs [neq0_conv];
 
 Goal "(0 ~= n) = (0 < n)";
-by(exhaust_tac "n" 1);
-by(Auto_tac);
+by (exhaust_tac "n" 1);
+by (Auto_tac);
 qed "zero_neq_conv";
 AddIffs [zero_neq_conv];
 
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Ord.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -161,10 +161,10 @@
 
 Goalw [min_def]
  "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "split_min";
 
 Goalw [max_def]
  "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "split_max";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Set.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -467,7 +467,7 @@
 Addsimps [singleton_conv];
 
 Goal "{x. a=x} = {a}";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "singleton_conv2";
 Addsimps [singleton_conv2];
 
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/TLA/Action.ML
--- a/src/HOL/TLA/Action.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/TLA/Action.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -253,6 +253,6 @@
 
 val [prem] = goal thy "basevars (x,y,z) ==> |- x --> Enabled ($x & (y$ = #False))";
 by (enabled_tac prem 1);
-auto();
+by Auto_tac;
 
 *)
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/equalities.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -747,7 +747,7 @@
 qed "ex_bool_eq";
 
 Goal "A Un B = (UN b. if b then A else B)";
-by(auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
+by (auto_tac(claset()delWrapper"bspec",simpset()addsimps [split_if_mem2]));
 qed "Un_eq_UN";
 
 Goal "(UN b::bool. A b) = (A True Un A False)";
diff -r 3815b5b095cb -r 08245f5a436d src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/simpdata.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -498,7 +498,7 @@
       val refute_prems_tac =
         REPEAT(eresolve_tac [conjE, exE] 1 ORELSE
                filter_prems_tac test 1 ORELSE
-               eresolve_tac [disjE] 1) THEN
+               etac disjE 1) THEN
         ref_tac 1;
   in EVERY'[TRY o filter_prems_tac test,
             DETERM o REPEAT o etac rev_mp, prep_tac, rtac ccontr, prem_nnf_tac,