src/ZF/Perm.ML

 by (etac CollectD1 1);
 qed "inj_is_fun";
 
 (*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
 Goalw [inj_def]
-    "!!f A B. [| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
+    "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
 by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
 by (Blast_tac 1);
 qed "inj_equality";
 
 Goalw [inj_def] "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";

 
 (** Equations for converse(f) **)
 
 (*The premises are equivalent to saying that f is injective...*) 
 Goal
-    "!!f. [| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
+    "[| f: A->B;  converse(f): C->A;  a: A |] ==> converse(f)`(f`a) = a";
 by (blast_tac (claset() addIs [apply_Pair, apply_equality, converseI]) 1);
 qed "left_inverse_lemma";
 
 Goal
-    "!!f. [| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
+    "[| f: inj(A,B);  a: A |] ==> converse(f)`(f`a) = a";
 by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
 			      inj_is_fun]) 1);
 qed "left_inverse";
 
 val left_inverse_bij = bij_is_inj RS left_inverse;

 
 
 (** Composition preserves functions, injections, and surjections **)
 
 Goalw [function_def]
-    "!!f g. [| function(g);  function(f) |] ==> function(f O g)";
+    "[| function(g);  function(f) |] ==> function(f O g)";
 by (Blast_tac 1);
 qed "comp_function";
 
 Goal "[| g: A->B;  f: B->C |] ==> (f O g) : A->C";
 by (asm_full_simp_tac

 by (asm_simp_tac (simpset()  addsimps [left_inverse] 
                         setSolver type_auto_tac [inj_is_fun, apply_type]) 1);
 qed "comp_inj";
 
 Goalw [surj_def]
-    "!!f g. [| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
+    "[| g: surj(A,B);  f: surj(B,C) |] ==> (f O g) : surj(A,C)";
 by (blast_tac (claset() addSIs [comp_fun,comp_fun_apply]) 1);
 qed "comp_surj";
 
 Goalw [bij_def]
-    "!!f g. [| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
+    "[| g: bij(A,B);  f: bij(B,C) |] ==> (f O g) : bij(A,C)";
 by (blast_tac (claset() addIs [comp_inj,comp_surj]) 1);
 qed "comp_bij";
 
 
 (** Dual properties of inj and surj -- useful for proofs from
     D Pastre.  Automatic theorem proving in set theory. 
     Artificial Intelligence, 10:1--27, 1978. **)
 
 Goalw [inj_def]
-    "!!f g. [| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
+    "[| (f O g): inj(A,C);  g: A->B;  f: B->C |] ==> g: inj(A,B)";
 by Safe_tac;
 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
 by (asm_simp_tac (simpset() ) 1);
 qed "comp_mem_injD1";
 
 Goalw [inj_def,surj_def]
-    "!!f g. [| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
+    "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)";
 by Safe_tac;
 by (res_inst_tac [("x1", "x")] (bspec RS bexE) 1);
 by (eres_inst_tac [("x1", "w")] (bspec RS bexE) 3);
 by (REPEAT (assume_tac 1));
 by Safe_tac;

 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp] 1));
 by (asm_simp_tac (simpset() ) 1);
 qed "comp_mem_injD2";
 
 Goalw [surj_def]
-    "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
+    "[| (f O g): surj(A,C);  g: A->B;  f: B->C |] ==> f: surj(B,C)";
 by (blast_tac (claset() addSIs [comp_fun_apply RS sym, apply_funtype]) 1);
 qed "comp_mem_surjD1";
 
 Goal
-    "!!f g. [| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
+    "[| (f O g)`a = c;  g: A->B;  f: B->C;  a:A |] ==> f`(g`a) = c";
 by (REPEAT (ares_tac [comp_fun_apply RS sym RS trans] 1));
 qed "comp_fun_applyD";
 
 Goalw [inj_def,surj_def]
-    "!!f g. [| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
+    "[| (f O g): surj(A,C);  g: A->B;  f: inj(B,C) |] ==> g: surj(A,B)";
 by Safe_tac;
 by (eres_inst_tac [("x1", "f`y")] (bspec RS bexE) 1);
 by (REPEAT (ares_tac [apply_type] 1 ORELSE dtac comp_fun_applyD 1));
 by (blast_tac (claset() addSIs [apply_funtype]) 1);
 qed "comp_mem_surjD2";

 qed "right_comp_inverse";
 
 (** Proving that a function is a bijection **)
 
 Goalw [id_def]
-    "!!f A B. [| f: A->B;  g: B->A |] ==> \
+    "[| f: A->B;  g: B->A |] ==> \
 \             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
 by Safe_tac;
 by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
 by (Asm_full_simp_tac 1);
 by (rtac fun_extension 1);
 by (REPEAT (ares_tac [comp_fun, lam_type] 1));
 by Auto_tac;
 qed "comp_eq_id_iff";
 
 Goalw [bij_def]
-    "!!f A B. [| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) \
+    "[| f: A->B;  g: B->A;  f O g = id(B);  g O f = id(A) \
 \             |] ==> f : bij(A,B)";
 by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff]) 1);
 by (REPEAT (ares_tac [conjI, f_imp_injective, f_imp_surjective] 1
        ORELSE eresolve_tac [bspec, apply_type] 1));
 qed "fg_imp_bijective";

 
 (** Unions of functions -- cf similar theorems on func.ML **)
 
 (*Theorem by KG, proof by LCP*)
 Goal
-    "!!f g. [| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] ==> \
+    "[| f: inj(A,B);  g: inj(C,D);  B Int D = 0 |] ==> \
 \           (lam a: A Un C. if(a:A, f`a, g`a)) : inj(A Un C, B Un D)";
 by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, converse(g)`z)")]
         lam_injective 1);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] 
                          setloop (split_tac [split_if] ORELSE' etac UnE))));
 by (blast_tac (claset() addIs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
 qed "inj_disjoint_Un";
 
 Goalw [surj_def]
-    "!!f g. [| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
+    "[| f: surj(A,B);  g: surj(C,D);  A Int C = 0 |] ==> \
 \           (f Un g) : surj(A Un C, B Un D)";
 by (blast_tac (claset() addIs [fun_disjoint_apply1, fun_disjoint_apply2,
 			      fun_disjoint_Un, trans]) 1);
 qed "surj_disjoint_Un";
 
 (*A simple, high-level proof; the version for injections follows from it,
   using  f:inj(A,B) <-> f:bij(A,range(f))  *)
 Goal
-    "!!f g. [| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
+    "[| f: bij(A,B);  g: bij(C,D);  A Int C = 0;  B Int D = 0 |] ==> \
 \           (f Un g) : bij(A Un C, B Un D)";
 by (rtac invertible_imp_bijective 1);
 by (stac converse_Un 1);
 by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
 qed "bij_disjoint_Un";

      ORELSE ares_tac [subsetI,lamI,imageI] 2));
 by (REPEAT (ares_tac [image_mono,restrict_subset,subset_refl] 1));
 qed "restrict_image";
 
 Goalw [inj_def]
-    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
+    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): inj(C,B)";
 by (safe_tac (claset() addSEs [restrict_type2]));
 by (REPEAT (eresolve_tac [asm_rl, bspec RS bspec RS mp, subsetD,
                           box_equals, restrict] 1));
 qed "restrict_inj";
 

 by (rtac (restrict_type2 RS surj_image) 3);
 by (REPEAT (resolve_tac prems 1));
 qed "restrict_surj";
 
 Goalw [inj_def,bij_def]
-    "!!f. [| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
+    "[| f: inj(A,B);  C<=A |] ==> restrict(f,C): bij(C, f``C)";
 by (blast_tac (claset() addSIs [restrict, restrict_surj]
 		       addIs [box_equals, surj_is_fun]) 1);
 qed "restrict_bij";
 
 

 by (fast_tac (claset() addEs [range_type, mem_irrefl] 
 	              addDs [apply_equality]) 1);
 qed "inj_succ_restrict";
 
 Goalw [inj_def]
-    "!!f. [| f: inj(A,B);  a~:A;  b~:B |]  ==> \
+    "[| f: inj(A,B);  a~:A;  b~:B |]  ==> \
 \         cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
 by (fast_tac (claset() addIs [apply_type]
                addss (simpset() addsimps [fun_extend, fun_extend_apply2,
 						fun_extend_apply1])) 1);
 qed "inj_extend";