src/HOL/Library/Groups_Big_Fun.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -49,17 +49,17 @@
     1.4    assumes "g a = 1"
     1.5    shows "G (g(a := b)) = b * G g"
     1.6  proof (cases "b = 1")
     1.7 -  case True with `g a = 1` show ?thesis
     1.8 +  case True with \<open>g a = 1\<close> show ?thesis
     1.9      by (simp add: expand_set) (rule F.cong, auto)
    1.10  next
    1.11    case False
    1.12    moreover have "{a'. a' \<noteq> a \<longrightarrow> g a' \<noteq> 1} = insert a {a. g a \<noteq> 1}"
    1.13      by auto
    1.14 -  moreover from `g a = 1` have "a \<notin> {a. g a \<noteq> 1}"
    1.15 +  moreover from \<open>g a = 1\<close> have "a \<notin> {a. g a \<noteq> 1}"
    1.16      by simp
    1.17    moreover have "F.F (\<lambda>a'. if a' = a then b else g a') {a. g a \<noteq> 1} = F.F g {a. g a \<noteq> 1}"
    1.18 -    by (rule F.cong) (auto simp add: `g a = 1`)
    1.19 -  ultimately show ?thesis using `finite {a. g a \<noteq> 1}` by (simp add: expand_set)
    1.20 +    by (rule F.cong) (auto simp add: \<open>g a = 1\<close>)
    1.21 +  ultimately show ?thesis using \<open>finite {a. g a \<noteq> 1}\<close> by (simp add: expand_set)
    1.22  qed
    1.23  
    1.24  lemma infinite [simp]:
    1.25 @@ -87,9 +87,9 @@
    1.26    shows "G g = G h"
    1.27  proof -
    1.28    from assms have unfold: "h = g \<circ> l" by simp
    1.29 -  from `bij l` have "inj l" by (rule bij_is_inj)
    1.30 +  from \<open>bij l\<close> have "inj l" by (rule bij_is_inj)
    1.31    then have "inj_on l {a. h a \<noteq> 1}" by (rule subset_inj_on) simp
    1.32 -  moreover from `bij l` have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
    1.33 +  moreover from \<open>bij l\<close> have "{a. g a \<noteq> 1} = l ` {a. h a \<noteq> 1}"
    1.34      by (auto simp add: image_Collect unfold elim: bij_pointE)
    1.35    moreover have "\<And>x. x \<in> {a. h a \<noteq> 1} \<Longrightarrow> g (l x) = h x"
    1.36      by (simp add: unfold)
    1.37 @@ -115,7 +115,7 @@
    1.38    assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
    1.39    shows "G (\<lambda>a. G (g a)) = G (\<lambda>b. G (\<lambda>a. g a b))"
    1.40  proof -
    1.41 -  from `finite C` subset
    1.42 +  from \<open>finite C\<close> subset
    1.43      have "finite ({a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1})"
    1.44      by (rule rev_finite_subset)
    1.45    then have fins:
    1.46 @@ -143,17 +143,17 @@
    1.47    assumes subset: "{a. \<exists>b. g a b \<noteq> 1} \<times> {b. \<exists>a. g a b \<noteq> 1} \<subseteq> C" (is "?A \<times> ?B \<subseteq> C")
    1.48    shows "G (\<lambda>a. G (g a)) = G (\<lambda>(a, b). g a b)"
    1.49  proof -
    1.50 -  from subset `finite C` have fin_prod: "finite (?A \<times> ?B)"
    1.51 +  from subset \<open>finite C\<close> have fin_prod: "finite (?A \<times> ?B)"
    1.52      by (rule finite_subset)
    1.53    from fin_prod have "finite ?A" and "finite ?B"
    1.54      by (auto simp add: finite_cartesian_product_iff)
    1.55    have *: "G (\<lambda>a. G (g a)) =
    1.56      (F.F (\<lambda>a. F.F (g a) {b. \<exists>a. g a b \<noteq> 1}) {a. \<exists>b. g a b \<noteq> 1})"
    1.57      apply (subst expand_superset [of "?B"])
    1.58 -    apply (rule `finite ?B`)
    1.59 +    apply (rule \<open>finite ?B\<close>)
    1.60      apply auto
    1.61      apply (subst expand_superset [of "?A"])
    1.62 -    apply (rule `finite ?A`)
    1.63 +    apply (rule \<open>finite ?A\<close>)
    1.64      apply auto
    1.65      apply (erule F.not_neutral_contains_not_neutral)
    1.66      apply auto
    1.67 @@ -166,10 +166,10 @@
    1.68      apply (simp add: *)
    1.69      apply (simp add: F.cartesian_product)
    1.70      apply (subst expand_superset [of C])
    1.71 -    apply (rule `finite C`)
    1.72 +    apply (rule \<open>finite C\<close>)
    1.73      apply (simp_all add: **)
    1.74      apply (rule F.same_carrierI [of C])
    1.75 -    apply (rule `finite C`)
    1.76 +    apply (rule \<open>finite C\<close>)
    1.77      apply (simp_all add: subset)
    1.78      apply auto
    1.79      done
    1.80 @@ -330,9 +330,9 @@
    1.81    assumes "f a = 0"
    1.82    shows "(\<Prod>a. f a) = 0"
    1.83  proof -
    1.84 -  from `f a = 0` have "f a \<noteq> 1" by simp
    1.85 -  with `f a = 0` have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
    1.86 -  with `finite {a. f a \<noteq> 1}` show ?thesis
    1.87 +  from \<open>f a = 0\<close> have "f a \<noteq> 1" by simp
    1.88 +  with \<open>f a = 0\<close> have "\<exists>a. f a \<noteq> 1 \<and> f a = 0" by blast
    1.89 +  with \<open>finite {a. f a \<noteq> 1}\<close> show ?thesis
    1.90      by (simp add: Prod_any.expand_set setprod_zero)
    1.91  qed
    1.92