# HG changeset patch
# User paulson
# Date 1084546453 -7200
# Node ID 8f1ee65bd3ea57e55b1b8eab2cf15dbb1fedcf8c
# Parent  9ccfd0f59e118a306554b50842d05ce90a51ca74
tidied

diff -r 9ccfd0f59e11 -r 8f1ee65bd3ea src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Fri May 14 16:53:15 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Fri May 14 16:54:13 2004 +0200
@@ -9,9 +9,9 @@
 
 theory FiniteProduct = Group:
 
-text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
-  possible, because here we have explicit typing rules like @{text "x
-  : carrier G"}.  We introduce an explicit argument for the domain
+text {* Instantiation of locale @{text LC} of theory @{text Finite_Set} is not
+  possible, because here we have explicit typing rules like 
+  @{text "x \<in> carrier G"}.  We introduce an explicit argument for the domain
   @{text D}. *}
 
 consts
@@ -19,41 +19,41 @@
 
 inductive "foldSetD D f e"
   intros
-    emptyI [intro]: "e : D ==> ({}, e) : foldSetD D f e"
-    insertI [intro]: "[| x ~: A; f x y : D; (A, y) : foldSetD D f e |] ==>
-                      (insert x A, f x y) : foldSetD D f e"
+    emptyI [intro]: "e \<in> D ==> ({}, e) \<in> foldSetD D f e"
+    insertI [intro]: "[| x ~: A; f x y \<in> D; (A, y) \<in> foldSetD D f e |] ==>
+                      (insert x A, f x y) \<in> foldSetD D f e"
 
-inductive_cases empty_foldSetDE [elim!]: "({}, x) : foldSetD D f e"
+inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
 
 constdefs
   foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
-  "foldD D f e A == THE x. (A, x) : foldSetD D f e"
+  "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
 
 lemma foldSetD_closed:
-  "[| (A, z) : foldSetD D f e ; e : D; !!x y. [| x : A; y : D |] ==> f x y : D 
-      |] ==> z : D";
+  "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
+      |] ==> z \<in> D";
   by (erule foldSetD.elims) auto
 
 lemma Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; f x y : D |] ==>
-   (A, f x y) : foldSetD D f e"
+  "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; f x y \<in> D |] ==>
+   (A, f x y) \<in> foldSetD D f e"
   apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
     apply auto
   done
 
-lemma foldSetD_imp_finite [simp]: "(A, x) : foldSetD D f e ==> finite A"
+lemma foldSetD_imp_finite [simp]: "(A, x) \<in> foldSetD D f e ==> finite A"
   by (induct set: foldSetD) auto
 
 lemma finite_imp_foldSetD:
-  "[| finite A; e : D; !!x y. [| x : A; y : D |] ==> f x y : D |] ==>
-   EX x. (A, x) : foldSetD D f e"
+  "[| finite A; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D |] ==>
+   EX x. (A, x) \<in> foldSetD D f e"
 proof (induct set: Finites)
   case empty then show ?case by auto
 next
   case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by (auto dest: foldSetD_closed)
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+  then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
+  with insert have "y \<in> D" by (auto dest: foldSetD_closed)
+  with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
     by (intro foldSetD.intros) auto
   then show ?case ..
 qed
@@ -65,42 +65,42 @@
   and D :: "'a set"
   and f :: "'b => 'a => 'a"    (infixl "\<cdot>" 70)
   assumes left_commute:
-    "[| x : B; y : B; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
-  and f_closed [simp, intro!]: "!!x y. [| x : B; y : D |] ==> f x y : D"
+    "[| x \<in> B; y \<in> B; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+  and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
 
 lemma (in LCD) foldSetD_closed [dest]:
-  "(A, z) : foldSetD D f e ==> z : D";
+  "(A, z) \<in> foldSetD D f e ==> z \<in> D";
   by (erule foldSetD.elims) auto
 
 lemma (in LCD) Diff1_foldSetD:
-  "[| (A - {x}, y) : foldSetD D f e; x : A; A <= B |] ==>
-  (A, f x y) : foldSetD D f e"
-  apply (subgoal_tac "x : B")
+  "[| (A - {x}, y) \<in> foldSetD D f e; x \<in> A; A \<subseteq> B |] ==>
+  (A, f x y) \<in> foldSetD D f e"
+  apply (subgoal_tac "x \<in> B")
    prefer 2 apply fast
   apply (erule insert_Diff [THEN subst], rule foldSetD.intros)
     apply auto
   done
 
 lemma (in LCD) foldSetD_imp_finite [simp]:
-  "(A, x) : foldSetD D f e ==> finite A"
+  "(A, x) \<in> foldSetD D f e ==> finite A"
   by (induct set: foldSetD) auto
 
 lemma (in LCD) finite_imp_foldSetD:
-  "[| finite A; A <= B; e : D |] ==> EX x. (A, x) : foldSetD D f e"
+  "[| finite A; A \<subseteq> B; e \<in> D |] ==> EX x. (A, x) \<in> foldSetD D f e"
 proof (induct set: Finites)
   case empty then show ?case by auto
 next
   case (insert F x)
-  then obtain y where y: "(F, y) : foldSetD D f e" by auto
-  with insert have "y : D" by auto
-  with y and insert have "(insert x F, f x y) : foldSetD D f e"
+  then obtain y where y: "(F, y) \<in> foldSetD D f e" by auto
+  with insert have "y \<in> D" by auto
+  with y and insert have "(insert x F, f x y) \<in> foldSetD D f e"
     by (intro foldSetD.intros) auto
   then show ?case ..
 qed
 
 lemma (in LCD) foldSetD_determ_aux:
-  "e : D ==> ALL A x. A <= B & card A < n --> (A, x) : foldSetD D f e -->
-    (ALL y. (A, y) : foldSetD D f e --> y = x)"
+  "e \<in> D ==> \<forall>A x. A \<subseteq> B & card A < n --> (A, x) \<in> foldSetD D f e -->
+    (\<forall>y. (A, y) \<in> foldSetD D f e --> y = x)"
   apply (induct n)
    apply (auto simp add: less_Suc_eq) (* slow *)
   apply (erule foldSetD.cases)
@@ -117,12 +117,12 @@
     prefer 2 apply (blast elim!: equalityE)
    apply blast
   txt {* case @{prop "xa \<notin> xb"}. *}
-  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb : Aa & xa : Ab")
+  apply (subgoal_tac "Aa - {xb} = Ab - {xa} & xb \<in> Aa & xa \<in> Ab")
    prefer 2 apply (blast elim!: equalityE)
   apply clarify
   apply (subgoal_tac "Aa = insert xb Ab - {xa}")
    prefer 2 apply blast
-  apply (subgoal_tac "card Aa <= card Ab")
+  apply (subgoal_tac "card Aa \<le> card Ab")
    prefer 2
    apply (rule Suc_le_mono [THEN subst])
    apply (simp add: card_Suc_Diff1)
@@ -134,10 +134,10 @@
    apply best
   apply (subgoal_tac "ya = f xb x")
    prefer 2
-   apply (subgoal_tac "Aa <= B")
+   apply (subgoal_tac "Aa \<subseteq> B")
     prefer 2 apply best (* slow *)
    apply (blast del: equalityCE)
-  apply (subgoal_tac "(Ab - {xa}, x) : foldSetD D f e")
+  apply (subgoal_tac "(Ab - {xa}, x) \<in> foldSetD D f e")
    prefer 2 apply simp
   apply (subgoal_tac "yb = f xa x")
    prefer 2 
@@ -150,22 +150,22 @@
   done
 
 lemma (in LCD) foldSetD_determ:
-  "[| (A, x) : foldSetD D f e; (A, y) : foldSetD D f e; e : D; A <= B |]
+  "[| (A, x) \<in> foldSetD D f e; (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |]
   ==> y = x"
   by (blast intro: foldSetD_determ_aux [rule_format])
 
 lemma (in LCD) foldD_equality:
-  "[| (A, y) : foldSetD D f e; e : D; A <= B |] ==> foldD D f e A = y"
+  "[| (A, y) \<in> foldSetD D f e; e \<in> D; A \<subseteq> B |] ==> foldD D f e A = y"
   by (unfold foldD_def) (blast intro: foldSetD_determ)
 
 lemma foldD_empty [simp]:
-  "e : D ==> foldD D f e {} = e"
+  "e \<in> D ==> foldD D f e {} = e"
   by (unfold foldD_def) blast
 
 lemma (in LCD) foldD_insert_aux:
-  "[| x ~: A; x : B; e : D; A <= B |] ==>
-    ((insert x A, v) : foldSetD D f e) =
-    (EX y. (A, y) : foldSetD D f e & v = f x y)"
+  "[| x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
+    ((insert x A, v) \<in> foldSetD D f e) =
+    (EX y. (A, y) \<in> foldSetD D f e & v = f x y)"
   apply auto
   apply (rule_tac A1 = A in finite_imp_foldSetD [THEN exE])
      apply (fastsimp dest: foldSetD_imp_finite)
@@ -175,7 +175,7 @@
   done
 
 lemma (in LCD) foldD_insert:
-    "[| finite A; x ~: A; x : B; e : D; A <= B |] ==>
+    "[| finite A; x ~: A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
      foldD D f e (insert x A) = f x (foldD D f e A)"
   apply (unfold foldD_def)
   apply (simp add: foldD_insert_aux)
@@ -185,7 +185,7 @@
   done
 
 lemma (in LCD) foldD_closed [simp]:
-  "[| finite A; e : D; A <= B |] ==> foldD D f e A : D"
+  "[| finite A; e \<in> D; A \<subseteq> B |] ==> foldD D f e A \<in> D"
 proof (induct set: Finites)
   case empty then show ?case by (simp add: foldD_empty)
 next
@@ -193,7 +193,7 @@
 qed
 
 lemma (in LCD) foldD_commute:
-  "[| finite A; x : B; e : D; A <= B |] ==>
+  "[| finite A; x \<in> B; e \<in> D; A \<subseteq> B |] ==>
    f x (foldD D f e A) = foldD D f (f x e) A"
   apply (induct set: Finites)
    apply simp
@@ -201,11 +201,11 @@
   done
 
 lemma Int_mono2:
-  "[| A <= C; B <= C |] ==> A Int B <= C"
+  "[| A \<subseteq> C; B \<subseteq> C |] ==> A Int B \<subseteq> C"
   by blast
 
 lemma (in LCD) foldD_nest_Un_Int:
-  "[| finite A; finite C; e : D; A <= B; C <= B |] ==>
+  "[| finite A; finite C; e \<in> D; A \<subseteq> B; C \<subseteq> B |] ==>
    foldD D f (foldD D f e C) A = foldD D f (foldD D f e (A Int C)) (A Un C)"
   apply (induct set: Finites)
    apply simp
@@ -214,7 +214,7 @@
   done
 
 lemma (in LCD) foldD_nest_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; e : D; A <= B; C <= B |]
+  "[| finite A; finite B; A Int B = {}; e \<in> D; A \<subseteq> B; C \<subseteq> B |]
     ==> foldD D f e (A Un B) = foldD D f (foldD D f e B) A"
   by (simp add: foldD_nest_Un_Int)
 
@@ -237,16 +237,16 @@
   fixes D :: "'a set"
     and f :: "'a => 'a => 'a"    (infixl "\<cdot>" 70)
     and e :: 'a
-  assumes ident [simp]: "x : D ==> x \<cdot> e = x"
-    and commute: "[| x : D; y : D |] ==> x \<cdot> y = y \<cdot> x"
-    and assoc: "[| x : D; y : D; z : D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
-    and e_closed [simp]: "e : D"
-    and f_closed [simp]: "[| x : D; y : D |] ==> x \<cdot> y : D"
+  assumes ident [simp]: "x \<in> D ==> x \<cdot> e = x"
+    and commute: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y = y \<cdot> x"
+    and assoc: "[| x \<in> D; y \<in> D; z \<in> D |] ==> (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
+    and e_closed [simp]: "e \<in> D"
+    and f_closed [simp]: "[| x \<in> D; y \<in> D |] ==> x \<cdot> y \<in> D"
 
 lemma (in ACeD) left_commute:
-  "[| x : D; y : D; z : D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
+  "[| x \<in> D; y \<in> D; z \<in> D |] ==> x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"
 proof -
-  assume D: "x : D" "y : D" "z : D"
+  assume D: "x \<in> D" "y \<in> D" "z \<in> D"
   then have "x \<cdot> (y \<cdot> z) = (y \<cdot> z) \<cdot> x" by (simp add: commute)
   also from D have "... = y \<cdot> (z \<cdot> x)" by (simp add: assoc)
   also from D have "z \<cdot> x = x \<cdot> z" by (simp add: commute)
@@ -255,15 +255,15 @@
 
 lemmas (in ACeD) AC = assoc commute left_commute
 
-lemma (in ACeD) left_ident [simp]: "x : D ==> e \<cdot> x = x"
+lemma (in ACeD) left_ident [simp]: "x \<in> D ==> e \<cdot> x = x"
 proof -
-  assume D: "x : D"
+  assume D: "x \<in> D"
   have "x \<cdot> e = x" by (rule ident)
   with D show ?thesis by (simp add: commute)
 qed
 
 lemma (in ACeD) foldD_Un_Int:
-  "[| finite A; finite B; A <= D; B <= D |] ==>
+  "[| finite A; finite B; A \<subseteq> D; B \<subseteq> D |] ==>
     foldD D f e A \<cdot> foldD D f e B =
     foldD D f e (A Un B) \<cdot> foldD D f e (A Int B)"
   apply (induct set: Finites)
@@ -275,7 +275,7 @@
   done
 
 lemma (in ACeD) foldD_Un_disjoint:
-  "[| finite A; finite B; A Int B = {}; A <= D; B <= D |] ==>
+  "[| finite A; finite B; A Int B = {}; A \<subseteq> D; B \<subseteq> D |] ==>
     foldD D f e (A Un B) = foldD D f e A \<cdot> foldD D f e B"
   by (simp add: foldD_Un_Int
     left_commute LCD.foldD_closed [OF LCD.intro [of D]] Un_subset_iff)
@@ -396,11 +396,11 @@
   case empty show ?case by simp
 next
   case (insert A a) then
-  have fA: "f : A -> carrier G" by fast
-  from insert have fa: "f a : carrier G" by fast
-  from insert have gA: "g : A -> carrier G" by fast
-  from insert have ga: "g a : carrier G" by fast
-  from insert have fgA: "(%x. f x \<otimes> g x) : A -> carrier G"
+  have fA: "f \<in> A -> carrier G" by fast
+  from insert have fa: "f a \<in> carrier G" by fast
+  from insert have gA: "g \<in> A -> carrier G" by fast
+  from insert have ga: "g a \<in> carrier G" by fast
+  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
     by (simp add: Pi_def)
   show ?case  (* check if all simps are really necessary *)
     by (simp add: insert fA fa gA ga fgA m_ac Int_insert_left insert_absorb
@@ -408,16 +408,16 @@
 qed
 
 lemma (in comm_monoid) finprod_cong':
-  "[| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+  "[| A = B; g \<in> B -> carrier G;
+      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
 proof -
-  assume prems: "A = B" "g : B -> carrier G"
-    "!!i. i : B ==> f i = g i"
+  assume prems: "A = B" "g \<in> B -> carrier G"
+    "!!i. i \<in> B ==> f i = g i"
   show ?thesis
   proof (cases "finite B")
     case True
-    then have "!!A. [| A = B; g : B -> carrier G;
-      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+    then have "!!A. [| A = B; g \<in> B -> carrier G;
+      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
     proof induct
       case empty thus ?case by simp
     next
@@ -431,7 +431,7 @@
       next
 	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
 	  "g \<in> insert x B \<rightarrow> carrier G"
-	thus "f : B -> carrier G" by fastsimp
+	thus "f \<in> B -> carrier G" by fastsimp
       next
 	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
 	  "g \<in> insert x B \<rightarrow> carrier G"
@@ -449,13 +449,13 @@
 qed
 
 lemma (in comm_monoid) finprod_cong:
-  "[| A = B; f : B -> carrier G = True;
-      !!i. i : B ==> f i = g i |] ==> finprod G f A = finprod G g B"
+  "[| A = B; f \<in> B -> carrier G = True;
+      !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   (* This order of prems is slightly faster (3%) than the last two swapped. *)
   by (rule finprod_cong') force+
 
 text {*Usually, if this rule causes a failed congruence proof error,
-  the reason is that the premise @{text "g : B -> carrier G"} cannot be shown.
+  the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   Adding @{thm [source] Pi_def} to the simpset is often useful.
   For this reason, @{thm [source] comm_monoid.finprod_cong}
   is not added to the simpset by default.
@@ -465,16 +465,16 @@
   funcset_mem [rule del]
 
 lemma (in comm_monoid) finprod_0 [simp]:
-  "f : {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
+  "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
 by (simp add: Pi_def)
 
 lemma (in comm_monoid) finprod_Suc [simp]:
-  "f : {..Suc n} -> carrier G ==>
+  "f \<in> {..Suc n} -> carrier G ==>
    finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
 by (simp add: Pi_def atMost_Suc)
 
 lemma (in comm_monoid) finprod_Suc2:
-  "f : {..Suc n} -> carrier G ==>
+  "f \<in> {..Suc n} -> carrier G ==>
    finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
 proof (induct n)
   case 0 thus ?case by (simp add: Pi_def)
@@ -483,7 +483,7 @@
 qed
 
 lemma (in comm_monoid) finprod_mult [simp]:
-  "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
+  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
      finprod G (%i. f i \<otimes> g i) {..n::nat} =
      finprod G f {..n} \<otimes> finprod G g {..n}"
   by (induct n) (simp_all add: m_ac Pi_def)