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.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.70      apply (subst expand_superset [of C])
1.71 -    apply (rule `finite C`)
1.72 +    apply (rule \<open>finite C\<close>)
1.74      apply (rule F.same_carrierI [of C])
1.75 -    apply (rule `finite C`)
1.76 +    apply (rule \<open>finite C\<close>)
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
```