tidied
authorpaulson
Fri May 14 16:54:13 2004 +0200 (2004-05-14)
changeset 147508f1ee65bd3ea
parent 14749 9ccfd0f59e11
child 14751 0d7850e27fed
tidied
src/HOL/Algebra/FiniteProduct.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri May 14 16:53:15 2004 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri May 14 16:54:13 2004 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  
     1.5  theory FiniteProduct = Group:
     1.6  
     1.7 -text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
     1.8 -  possible, because here we have explicit typing rules like @{text "x
     1.9 -  : carrier G"}.  We introduce an explicit argument for the domain
    1.10 +text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
    1.11 +  possible, because here we have explicit typing rules like 
    1.12 +  @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
    1.13    @{text D}. *}
    1.14  
    1.15  consts
    1.16 @@ -19,41 +19,41 @@
    1.17  
    1.18  inductive "foldSetD D f e"
    1.19    intros
    1.20 -    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
    1.21 -    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
    1.22 -                      (insert x A, f x y) : foldSetD D f e"
    1.23 +    emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e"
    1.24 +    insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
    1.25 +                      (insert x A, f x y) \<in> foldSetD D f e"
    1.26  
    1.27 -inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
    1.28 +inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
    1.29  
    1.30  constdefs
    1.31    foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
    1.32 -  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
    1.33 +  "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
    1.34  
    1.35  lemma foldSetD_closed:
    1.36 -  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
    1.37 -      |] ==> z : D";
    1.38 +  "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
    1.39 +      |] ==> z \<in> D";
    1.40    by (erule foldSetD.elims) auto
    1.41  
    1.42  lemma Diff1_foldSetD:
    1.43 -  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
    1.44 -   (A, f x y) : foldSetD D f e"
    1.45 +  "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D |] ==>
    1.46 +   (A, f x y) \<in> foldSetD D f e"
    1.47    apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    1.48      apply auto
    1.49    done
    1.50  
    1.51 -lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
    1.52 +lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e ==> finite A"
    1.53    by (induct set: foldSetD) auto
    1.54  
    1.55  lemma finite_imp_foldSetD:
    1.56 -  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
    1.57 -   EX x. (A, x) : foldSetD D f e"
    1.58 +  "[| finite A; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |] ==>
    1.59 +   EX x. (A, x) \<in> foldSetD D f e"
    1.60  proof (induct set: Finites)
    1.61    case empty then show ?case by auto
    1.62  next
    1.63    case (insert F x)
    1.64 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
    1.65 -  with insert have "y : D" by (auto dest: foldSetD_closed)
    1.66 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
    1.67 +  then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
    1.68 +  with insert have "y \<in> D" by (auto dest: foldSetD_closed)
    1.69 +  with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
    1.70      by (intro foldSetD.intros) auto
    1.71    then show ?case ..
    1.72  qed
    1.73 @@ -65,42 +65,42 @@
    1.74    and D :: "'a set"
    1.75    and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
    1.76    assumes left_commute:
    1.77 -    "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    1.78 -  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
    1.79 +    "[| x \<in> B; y \<in> B; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
    1.80 +  and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
    1.81  
    1.82  lemma (in LCD) foldSetD_closed [dest]:
    1.83 -  "(A, z) : foldSetD D f e ==> z : D";
    1.84 +  "(A, z) \<in> foldSetD D f e ==> z \<in> D";
    1.85    by (erule foldSetD.elims) auto
    1.86  
    1.87  lemma (in LCD) Diff1_foldSetD:
    1.88 -  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
    1.89 -  (A, f x y) : foldSetD D f e"
    1.90 -  apply (subgoal_tac "x : B")
    1.91 +  "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B |] ==>
    1.92 +  (A, f x y) \<in> foldSetD D f e"
    1.93 +  apply (subgoal_tac "x \<in> B")
    1.94     prefer 2 apply fast
    1.95    apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
    1.96      apply auto
    1.97    done
    1.98  
    1.99  lemma (in LCD) foldSetD_imp_finite [simp]:
   1.100 -  "(A, x) : foldSetD D f e ==> finite A"
   1.101 +  "(A, x) \<in> foldSetD D f e ==> finite A"
   1.102    by (induct set: foldSetD) auto
   1.103  
   1.104  lemma (in LCD) finite_imp_foldSetD:
   1.105 -  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
   1.106 +  "[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e"
   1.107  proof (induct set: Finites)
   1.108    case empty then show ?case by auto
   1.109  next
   1.110    case (insert F x)
   1.111 -  then obtain y where y: "(F, y) : foldSetD D f e" by auto
   1.112 -  with insert have "y : D" by auto
   1.113 -  with y and insert have "(insert x F, f x y) : foldSetD D f e"
   1.114 +  then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
   1.115 +  with insert have "y \<in> D" by auto
   1.116 +  with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
   1.117      by (intro foldSetD.intros) auto
   1.118    then show ?case ..
   1.119  qed
   1.120  
   1.121  lemma (in LCD) foldSetD_determ_aux:
   1.122 -  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
   1.123 -    (ALL y. (A, y) : foldSetD D f e --> y = x)"
   1.124 +  "e \<in> D ==> \<forall>A x. A \<subseteq> B & card A < n --> (A, x) \<in> foldSetD D f e -->
   1.125 +    (\<forall>y. (A, y) \<in> foldSetD D f e --> y = x)"
   1.126    apply (induct n)
   1.127     apply (auto simp add: less_Suc_eq) (* slow *)
   1.128    apply (erule foldSetD.cases)
   1.129 @@ -117,12 +117,12 @@
   1.130      prefer 2 apply (blast elim!: equalityE)
   1.131     apply blast
   1.132    txt {* case @{prop "xa \<notin> xb"}. *}
   1.133 -  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
   1.134 +  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
   1.135     prefer 2 apply (blast elim!: equalityE)
   1.136    apply clarify
   1.137    apply (subgoal_tac "Aa = insert xb Ab - {xa}")
   1.138     prefer 2 apply blast
   1.139 -  apply (subgoal_tac "card Aa <= card Ab")
   1.140 +  apply (subgoal_tac "card Aa \<le> card Ab")
   1.141     prefer 2
   1.142     apply (rule Suc_le_mono [THEN subst])
   1.143     apply (simp add: card_Suc_Diff1)
   1.144 @@ -134,10 +134,10 @@
   1.145     apply best
   1.146    apply (subgoal_tac "ya = f xb x")
   1.147     prefer 2
   1.148 -   apply (subgoal_tac "Aa <= B")
   1.149 +   apply (subgoal_tac "Aa \<subseteq> B")
   1.150      prefer 2 apply best (* slow *)
   1.151     apply (blast del: equalityCE)
   1.152 -  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
   1.153 +  apply (subgoal_tac "(Ab - {xa}, x) \<in> foldSetD D f e")
   1.154     prefer 2 apply simp
   1.155    apply (subgoal_tac "yb = f xa x")
   1.156     prefer 2 
   1.157 @@ -150,22 +150,22 @@
   1.158    done
   1.159  
   1.160  lemma (in LCD) foldSetD_determ:
   1.161 -  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
   1.162 +  "[| (A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |]
   1.163    ==> y = x"
   1.164    by (blast intro: foldSetD_determ_aux [rule_format])
   1.165  
   1.166  lemma (in LCD) foldD_equality:
   1.167 -  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
   1.168 +  "[| (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |] ==> foldD D f e A = y"
   1.169    by (unfold foldD_def) (blast intro: foldSetD_determ)
   1.170  
   1.171  lemma foldD_empty [simp]:
   1.172 -  "e : D ==> foldD D f e {} = e"
   1.173 +  "e \<in> D ==> foldD D f e {} = e"
   1.174    by (unfold foldD_def) blast
   1.175  
   1.176  lemma (in LCD) foldD_insert_aux:
   1.177 -  "[| x ~: A; x : B; e : D; A <= B |] ==>
   1.178 -    ((insert x A, v) : foldSetD D f e) =
   1.179 -    (EX y. (A, y) : foldSetD D f e & v = f x y)"
   1.180 +  "[| x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
   1.181 +    ((insert x A, v) \<in> foldSetD D f e) =
   1.182 +    (EX y. (A, y) \<in> foldSetD D f e & v = f x y)"
   1.183    apply auto
   1.184    apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
   1.185       apply (fastsimp dest: foldSetD_imp_finite)
   1.186 @@ -175,7 +175,7 @@
   1.187    done
   1.188  
   1.189  lemma (in LCD) foldD_insert:
   1.190 -    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
   1.191 +    "[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
   1.192       foldD D f e (insert x A) = f x (foldD D f e A)"
   1.193    apply (unfold foldD_def)
   1.194    apply (simp add: foldD_insert_aux)
   1.195 @@ -185,7 +185,7 @@
   1.196    done
   1.197  
   1.198  lemma (in LCD) foldD_closed [simp]:
   1.199 -  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
   1.200 +  "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
   1.201  proof (induct set: Finites)
   1.202    case empty then show ?case by (simp add: foldD_empty)
   1.203  next
   1.204 @@ -193,7 +193,7 @@
   1.205  qed
   1.206  
   1.207  lemma (in LCD) foldD_commute:
   1.208 -  "[| finite A; x : B; e : D; A <= B |] ==>
   1.209 +  "[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
   1.210     f x (foldD D f e A) = foldD D f (f x e) A"
   1.211    apply (induct set: Finites)
   1.212     apply simp
   1.213 @@ -201,11 +201,11 @@
   1.214    done
   1.215  
   1.216  lemma Int_mono2:
   1.217 -  "[| A <= C; B <= C |] ==> A Int B <= C"
   1.218 +  "[| A \<subseteq> C; B \<subseteq> C |] ==> A Int B \<subseteq> C"
   1.219    by blast
   1.220  
   1.221  lemma (in LCD) foldD_nest_Un_Int:
   1.222 -  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
   1.223 +  "[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==>
   1.224     foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   1.225    apply (induct set: Finites)
   1.226     apply simp
   1.227 @@ -214,7 +214,7 @@
   1.228    done
   1.229  
   1.230  lemma (in LCD) foldD_nest_Un_disjoint:
   1.231 -  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
   1.232 +  "[| finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B |]
   1.233      ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   1.234    by (simp add: foldD_nest_Un_Int)
   1.235  
   1.236 @@ -237,16 +237,16 @@
   1.237    fixes D :: "'a set"
   1.238      and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
   1.239      and e :: 'a
   1.240 -  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
   1.241 -    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
   1.242 -    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   1.243 -    and e_closed [simp]: "e : D"
   1.244 -    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
   1.245 +  assumes ident [simp]: "x \<in> D ==> x \<cdot> e = x"
   1.246 +    and commute: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y = y \<cdot> x"
   1.247 +    and assoc: "[| x \<in> D; y \<in> D; z \<in> D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
   1.248 +    and e_closed [simp]: "e \<in> D"
   1.249 +    and f_closed [simp]: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y \<in> D"
   1.250  
   1.251  lemma (in ACeD) left_commute:
   1.252 -  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   1.253 +  "[| x \<in> D; y \<in> D; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
   1.254  proof -
   1.255 -  assume D: "x : D" "y : D" "z : D"
   1.256 +  assume D: "x \<in> D" "y \<in> D" "z \<in> D"
   1.257    then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   1.258    also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   1.259    also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
   1.260 @@ -255,15 +255,15 @@
   1.261  
   1.262  lemmas (in ACeD) AC = assoc commute left_commute
   1.263  
   1.264 -lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
   1.265 +lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
   1.266  proof -
   1.267 -  assume D: "x : D"
   1.268 +  assume D: "x \<in> D"
   1.269    have "x \<cdot> e = x" by (rule ident)
   1.270    with D show ?thesis by (simp add: commute)
   1.271  qed
   1.272  
   1.273  lemma (in ACeD) foldD_Un_Int:
   1.274 -  "[| finite A; finite B; A <= D; B <= D |] ==>
   1.275 +  "[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==>
   1.276      foldD D f e A \<cdot> foldD D f e B =
   1.277      foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   1.278    apply (induct set: Finites)
   1.279 @@ -275,7 +275,7 @@
   1.280    done
   1.281  
   1.282  lemma (in ACeD) foldD_Un_disjoint:
   1.283 -  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
   1.284 +  "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
   1.285      foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   1.286    by (simp add: foldD_Un_Int
   1.287      left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
   1.288 @@ -396,11 +396,11 @@
   1.289    case empty show ?case by simp
   1.290  next
   1.291    case (insert A a) then
   1.292 -  have fA: "f : A -> carrier G" by fast
   1.293 -  from insert have fa: "f a : carrier G" by fast
   1.294 -  from insert have gA: "g : A -> carrier G" by fast
   1.295 -  from insert have ga: "g a : carrier G" by fast
   1.296 -  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
   1.297 +  have fA: "f \<in> A -> carrier G" by fast
   1.298 +  from insert have fa: "f a \<in> carrier G" by fast
   1.299 +  from insert have gA: "g \<in> A -> carrier G" by fast
   1.300 +  from insert have ga: "g a \<in> carrier G" by fast
   1.301 +  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
   1.302      by (simp add: Pi_def)
   1.303    show ?case  (* check if all simps are really necessary *)
   1.304      by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
   1.305 @@ -408,16 +408,16 @@
   1.306  qed
   1.307  
   1.308  lemma (in comm_monoid) finprod_cong':
   1.309 -  "[| A = B; g : B -> carrier G;
   1.310 -      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.311 +  "[| A = B; g \<in> B -> carrier G;
   1.312 +      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.313  proof -
   1.314 -  assume prems: "A = B" "g : B -> carrier G"
   1.315 -    "!!i. i : B ==> f i = g i"
   1.316 +  assume prems: "A = B" "g \<in> B -> carrier G"
   1.317 +    "!!i. i \<in> B ==> f i = g i"
   1.318    show ?thesis
   1.319    proof (cases "finite B")
   1.320      case True
   1.321 -    then have "!!A. [| A = B; g : B -> carrier G;
   1.322 -      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.323 +    then have "!!A. [| A = B; g \<in> B -> carrier G;
   1.324 +      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.325      proof induct
   1.326        case empty thus ?case by simp
   1.327      next
   1.328 @@ -431,7 +431,7 @@
   1.329        next
   1.330  	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.331  	  "g \<in> insert x B \<rightarrow> carrier G"
   1.332 -	thus "f : B -> carrier G" by fastsimp
   1.333 +	thus "f \<in> B -> carrier G" by fastsimp
   1.334        next
   1.335  	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   1.336  	  "g \<in> insert x B \<rightarrow> carrier G"
   1.337 @@ -449,13 +449,13 @@
   1.338  qed
   1.339  
   1.340  lemma (in comm_monoid) finprod_cong:
   1.341 -  "[| A = B; f : B -> carrier G = True;
   1.342 -      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.343 +  "[| A = B; f \<in> B -> carrier G = True;
   1.344 +      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   1.345    (* This order of prems is slightly faster (3%) than the last two swapped. *)
   1.346    by (rule finprod_cong') force+
   1.347  
   1.348  text {*Usually, if this rule causes a failed congruence proof error,
   1.349 -  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
   1.350 +  the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   1.351    Adding @{thm [source] Pi_def} to the simpset is often useful.
   1.352    For this reason, @{thm [source] comm_monoid.finprod_cong}
   1.353    is not added to the simpset by default.
   1.354 @@ -465,16 +465,16 @@
   1.355    funcset_mem [rule del]
   1.356  
   1.357  lemma (in comm_monoid) finprod_0 [simp]:
   1.358 -  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
   1.359 +  "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
   1.360  by (simp add: Pi_def)
   1.361  
   1.362  lemma (in comm_monoid) finprod_Suc [simp]:
   1.363 -  "f : {..Suc n} -> carrier G ==>
   1.364 +  "f \<in> {..Suc n} -> carrier G ==>
   1.365     finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
   1.366  by (simp add: Pi_def atMost_Suc)
   1.367  
   1.368  lemma (in comm_monoid) finprod_Suc2:
   1.369 -  "f : {..Suc n} -> carrier G ==>
   1.370 +  "f \<in> {..Suc n} -> carrier G ==>
   1.371     finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
   1.372  proof (induct n)
   1.373    case 0 thus ?case by (simp add: Pi_def)
   1.374 @@ -483,7 +483,7 @@
   1.375  qed
   1.376  
   1.377  lemma (in comm_monoid) finprod_mult [simp]:
   1.378 -  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
   1.379 +  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
   1.380       finprod G (%i. f i \<otimes> g i) {..n::nat} =
   1.381       finprod G f {..n} \<otimes> finprod G g {..n}"
   1.382    by (induct n) (simp_all add: m_ac Pi_def)