src/HOL/Groups_List.thy
changeset 60758 d8d85a8172b5
parent 60541 4246da644cca
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Groups_List.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Groups_List.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Tobias Nipkow, TU Muenchen *)
     1.5  
     1.6 -section {* Sum and product over lists *}
     1.7 +section \<open>Sum and product over lists\<close>
     1.8  
     1.9  theory Groups_List
    1.10  imports List
    1.11 @@ -56,7 +56,7 @@
    1.12  notation Groups.one ("1")
    1.13  
    1.14  
    1.15 -subsection {* List summation *}
    1.16 +subsection \<open>List summation\<close>
    1.17  
    1.18  context monoid_add
    1.19  begin
    1.20 @@ -101,7 +101,7 @@
    1.21  
    1.22  end
    1.23  
    1.24 -text {* Some syntactic sugar for summing a function over a list: *}
    1.25 +text \<open>Some syntactic sugar for summing a function over a list:\<close>
    1.26  
    1.27  syntax
    1.28    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    1.29 @@ -110,11 +110,11 @@
    1.30  syntax (HTML output)
    1.31    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    1.32  
    1.33 -translations -- {* Beware of argument permutation! *}
    1.34 +translations -- \<open>Beware of argument permutation!\<close>
    1.35    "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    1.36    "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    1.37  
    1.38 -text {* TODO duplicates *}
    1.39 +text \<open>TODO duplicates\<close>
    1.40  lemmas listsum_simps = listsum.Nil listsum.Cons
    1.41  lemmas listsum_append = listsum.append
    1.42  lemmas listsum_rev = listsum.rev
    1.43 @@ -190,7 +190,7 @@
    1.44    "(\<Sum>x\<leftarrow>xs. 0) = 0"
    1.45    by (induct xs) (simp_all add: distrib_right)
    1.46  
    1.47 -text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
    1.48 +text\<open>For non-Abelian groups @{text xs} needs to be reversed on one side:\<close>
    1.49  lemma (in ab_group_add) uminus_listsum_map:
    1.50    "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
    1.51    by (induct xs) simp_all
    1.52 @@ -232,7 +232,7 @@
    1.53    "listsum (map f [k..l]) = setsum f (set [k..l])"
    1.54    by (simp add: listsum_distinct_conv_setsum_set)
    1.55  
    1.56 -text {* General equivalence between @{const listsum} and @{const setsum} *}
    1.57 +text \<open>General equivalence between @{const listsum} and @{const setsum}\<close>
    1.58  lemma (in monoid_add) listsum_setsum_nth:
    1.59    "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
    1.60    using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
    1.61 @@ -245,14 +245,14 @@
    1.62    proof cases
    1.63      assume "x \<in> set xs"
    1.64      have "?l = f x + (\<Sum>x\<in>set xs. count_list xs x * f x)" by (simp add: Cons.IH)
    1.65 -    also have "set xs = insert x (set xs - {x})" using `x \<in> set xs`by blast
    1.66 +    also have "set xs = insert x (set xs - {x})" using \<open>x \<in> set xs\<close>by blast
    1.67      also have "f x + (\<Sum>x\<in>insert x (set xs - {x}). count_list xs x * f x) = ?r"
    1.68        by (simp add: setsum.insert_remove eq_commute)
    1.69      finally show ?thesis .
    1.70    next
    1.71      assume "x \<notin> set xs"
    1.72      hence "\<And>xa. xa \<in> set xs \<Longrightarrow> x \<noteq> xa" by blast
    1.73 -    thus ?thesis by (simp add: Cons.IH `x \<notin> set xs`)
    1.74 +    thus ?thesis by (simp add: Cons.IH \<open>x \<notin> set xs\<close>)
    1.75    qed
    1.76  qed simp
    1.77  
    1.78 @@ -270,7 +270,7 @@
    1.79  qed
    1.80  
    1.81  
    1.82 -subsection {* Further facts about @{const List.n_lists} *}
    1.83 +subsection \<open>Further facts about @{const List.n_lists}\<close>
    1.84  
    1.85  lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
    1.86    by (induct n) (auto simp add: comp_def length_concat listsum_triv)
    1.87 @@ -298,7 +298,7 @@
    1.88  qed
    1.89  
    1.90  
    1.91 -subsection {* Tools setup *}
    1.92 +subsection \<open>Tools setup\<close>
    1.93  
    1.94  lemmas setsum_code = setsum.set_conv_list
    1.95  
    1.96 @@ -325,7 +325,7 @@
    1.97  end
    1.98  
    1.99  
   1.100 -subsection {* List product *}
   1.101 +subsection \<open>List product\<close>
   1.102  
   1.103  context monoid_mult
   1.104  begin
   1.105 @@ -370,7 +370,7 @@
   1.106  
   1.107  end
   1.108  
   1.109 -text {* Some syntactic sugar: *}
   1.110 +text \<open>Some syntactic sugar:\<close>
   1.111  
   1.112  syntax
   1.113    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
   1.114 @@ -379,7 +379,7 @@
   1.115  syntax (HTML output)
   1.116    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
   1.117  
   1.118 -translations -- {* Beware of argument permutation! *}
   1.119 +translations -- \<open>Beware of argument permutation!\<close>
   1.120    "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
   1.121    "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
   1.122