src/HOL/Library/Permutation.thy
changeset 60502 aa58872267ee
parent 60495 d7ff0a1df90a
parent 60500 903bb1495239
child 60515 484559628038
     1.1 --- a/src/HOL/Library/Permutation.thy	Wed Jun 17 17:33:22 2015 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jun 17 17:54:09 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Lawrence C Paulson and Thomas M Rasmussen and Norbert Voelker
     1.5  *)
     1.6  
     1.7 -section {* Permutations *}
     1.8 +section \<open>Permutations\<close>
     1.9  
    1.10  theory Permutation
    1.11  imports Multiset
    1.12 @@ -19,13 +19,13 @@
    1.13    by (induct l) auto
    1.14  
    1.15  
    1.16 -subsection {* Some examples of rule induction on permutations *}
    1.17 +subsection \<open>Some examples of rule induction on permutations\<close>
    1.18  
    1.19  lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
    1.20    by (induct xs == "[] :: 'a list" ys pred: perm) simp_all
    1.21  
    1.22  
    1.23 -text {* \medskip This more general theorem is easier to understand! *}
    1.24 +text \<open>\medskip This more general theorem is easier to understand!\<close>
    1.25  
    1.26  lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
    1.27    by (induct pred: perm) simp_all
    1.28 @@ -37,9 +37,9 @@
    1.29    by (induct pred: perm) auto
    1.30  
    1.31  
    1.32 -subsection {* Ways of making new permutations *}
    1.33 +subsection \<open>Ways of making new permutations\<close>
    1.34  
    1.35 -text {* We can insert the head anywhere in the list. *}
    1.36 +text \<open>We can insert the head anywhere in the list.\<close>
    1.37  
    1.38  lemma perm_append_Cons: "a # xs @ ys <~~> xs @ a # ys"
    1.39    by (induct xs) auto
    1.40 @@ -66,7 +66,7 @@
    1.41    by (blast intro!: perm_append_swap perm_append1)
    1.42  
    1.43  
    1.44 -subsection {* Further results *}
    1.45 +subsection \<open>Further results\<close>
    1.46  
    1.47  lemma perm_empty [iff]: "[] <~~> xs \<longleftrightarrow> xs = []"
    1.48    by (blast intro: perm_empty_imp)
    1.49 @@ -86,13 +86,13 @@
    1.50    by (blast dest: perm_sym)
    1.51  
    1.52  
    1.53 -subsection {* Removing elements *}
    1.54 +subsection \<open>Removing elements\<close>
    1.55  
    1.56  lemma perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
    1.57    by (induct ys) auto
    1.58  
    1.59  
    1.60 -text {* \medskip Congruence rule *}
    1.61 +text \<open>\medskip Congruence rule\<close>
    1.62  
    1.63  lemma perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
    1.64    by (induct pred: perm) auto
    1.65 @@ -116,7 +116,7 @@
    1.66    apply (safe intro!: perm_append2)
    1.67    apply (rule append_perm_imp_perm)
    1.68    apply (rule perm_append_swap [THEN perm.trans])
    1.69 -    -- {* the previous step helps this @{text blast} call succeed quickly *}
    1.70 +    -- \<open>the previous step helps this @{text blast} call succeed quickly\<close>
    1.71    apply (blast intro: perm_append_swap)
    1.72    done
    1.73  
    1.74 @@ -241,7 +241,7 @@
    1.75      assume "i < length xs"
    1.76      with bij have "f i < length ys"
    1.77        unfolding bij_betw_def by force
    1.78 -    with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
    1.79 +    with \<open>i < length xs\<close> show "xs ! i = zs ! (g \<circ> f) i"
    1.80        using trans(1,3)[THEN perm_length] perm by auto
    1.81    qed
    1.82  qed