src/HOL/Algebra/FiniteProduct.thy
changeset 67613 ce654b0e6d69
parent 67341 df79ef3b3a41
child 68445 c183a6a69f2d
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    for D :: "'a set" and f :: "'b => 'a => 'a" and e :: 'a
     1.5    where
     1.6      emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e"
     1.7 -  | insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
     1.8 +  | insertI [intro]: "[| x \<notin> A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
     1.9                        (insert x A, f x y) \<in> foldSetD D f e"
    1.10  
    1.11  inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
    1.12 @@ -178,7 +178,7 @@
    1.13    done
    1.14  
    1.15  lemma (in LCD) foldD_insert:
    1.16 -    "[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
    1.17 +    "[| finite A; x \<notin> A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
    1.18       foldD D f e (insert x A) = f x (foldD D f e A)"
    1.19    apply (unfold foldD_def)
    1.20    apply (simp add: foldD_insert_aux)
    1.21 @@ -423,13 +423,13 @@
    1.22        proof (intro finprod_insert)
    1.23          show "finite B" by fact
    1.24        next
    1.25 -        show "x ~: B" by fact
    1.26 +        show "x \<notin> B" by fact
    1.27        next
    1.28 -        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
    1.29 +        assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
    1.30            "g \<in> insert x B \<rightarrow> carrier G"
    1.31          thus "f \<in> B \<rightarrow> carrier G" by fastforce
    1.32        next
    1.33 -        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
    1.34 +        assume "x \<notin> B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
    1.35            "g \<in> insert x B \<rightarrow> carrier G"
    1.36          thus "f x \<in> carrier G" by fastforce
    1.37        qed
    1.38 @@ -491,8 +491,8 @@
    1.39  (* The following two were contributed by Jeremy Avigad. *)
    1.40  
    1.41  lemma finprod_reindex:
    1.42 -  "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
    1.43 -        inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
    1.44 +  "f \<in> (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
    1.45 +        inj_on h A \<Longrightarrow> finprod G f (h ` A) = finprod G (\<lambda>x. f (h x)) A"
    1.46  proof (induct A rule: infinite_finite_induct)
    1.47    case (infinite A)
    1.48    hence "\<not> finite (h ` A)"
    1.49 @@ -501,8 +501,8 @@
    1.50  qed (auto simp add: Pi_def)
    1.51  
    1.52  lemma finprod_const:
    1.53 -  assumes a [simp]: "a : carrier G"
    1.54 -    shows "finprod G (%x. a) A = a [^] card A"
    1.55 +  assumes a [simp]: "a \<in> carrier G"
    1.56 +    shows "finprod G (\<lambda>x. a) A = a [^] card A"
    1.57  proof (induct A rule: infinite_finite_induct)
    1.58    case (insert b A)
    1.59    show ?case