diff --git a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
@@ -1,669 +1,669 @@
 (*  Title:      HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
 section \<open>An imperative implementation of Quicksort on arrays\<close>
 
 theory Imperative_Quicksort
 imports
-  "~~/src/HOL/Imperative_HOL/Imperative_HOL"
+  "../Imperative_HOL"
   Subarray
   "HOL-Library.Multiset"
   "HOL-Library.Code_Target_Numeral"
 begin
 
 text \<open>We prove QuickSort correct in the Relational Calculus.\<close>
 
 definition swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
 where
   "swap arr i j =
      do {
        x \<leftarrow> Array.nth arr i;
        y \<leftarrow> Array.nth arr j;
        Array.upd i y arr;
        Array.upd j x arr;
        return ()
      }"
 
 lemma effect_swapI [effect_intros]:
   assumes "i < Array.length h a" "j < Array.length h a"
     "x = Array.get h a ! i" "y = Array.get h a ! j"
     "h' = Array.update a j x (Array.update a i y h)"
   shows "effect (swap a i j) h h' r"
   unfolding swap_def using assms by (auto intro!: effect_intros)
 
 lemma swap_permutes:
   assumes "effect (swap a i j) h h' rs"
   shows "mset (Array.get h' a) 
   = mset (Array.get h a)"
   using assms
   unfolding swap_def
   by (auto simp add: Array.length_def mset_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
 
 function part1 :: "'a::{heap,ord} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat Heap"
 where
   "part1 a left right p = (
      if (right \<le> left) then return right
      else do {
        v \<leftarrow> Array.nth a left;
        (if (v \<le> p) then (part1 a (left + 1) right p)
                     else (do { swap a left right;
   part1 a left (right - 1) p }))
      })"
 by pat_completeness auto
 
 termination
 by (relation "measure (\<lambda>(_,l,r,_). r - l )") auto
 
 declare part1.simps[simp del]
 
 lemma part_permutes:
   assumes "effect (part1 a l r p) h h' rs"
   shows "mset (Array.get h' a) 
   = mset (Array.get h a)"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   thus ?case
     unfolding part1.simps [of a l r p]
     by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
 qed
 
 lemma part_returns_index_in_bounds:
   assumes "effect (part1 a l r p) h h' rs"
   assumes "l \<le> r"
   shows "l \<le> rs \<and> rs \<le> r"
 using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   note cr = \<open>effect (part1 a l r p) h h' rs\<close>
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr \<open>l \<le> r\<close> show ?thesis
       unfolding part1.simps[of a l r p]
       by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
     let ?v = "Array.get h a ! l"
     show ?thesis
     proof (cases "?v \<le> p")
       case True
       with cr False
       have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from rec_condition have "l + 1 \<le> r" by arith
       from 1(1)[OF rec_condition True rec1 \<open>l + 1 \<le> r\<close>]
       show ?thesis by simp
     next
       case False
       with rec_condition cr
       obtain h1 where swp: "effect (swap a l r) h h1 ()"
         and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from rec_condition have "l \<le> r - 1" by arith
       from 1(2) [OF rec_condition False rec2 \<open>l \<le> r - 1\<close>] show ?thesis by fastforce
     qed
   qed
 qed
 
 lemma part_length_remains:
   assumes "effect (part1 a l r p) h h' rs"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   note cr = \<open>effect (part1 a l r p) h h' rs\<close>
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
       by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     with cr 1 show ?thesis
       unfolding part1.simps [of a l r p] swap_def
       by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastforce
   qed
 qed
 
 lemma part_outer_remains:
   assumes "effect (part1 a l r p) h h' rs"
   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   note cr = \<open>effect (part1 a l r p) h h' rs\<close>
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr show ?thesis
       unfolding part1.simps[of a l r p]
       by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   next
     case False (* recursive case *)
     note rec_condition = this
     let ?v = "Array.get h a ! l"
     show ?thesis
     proof (cases "?v \<le> p")
       case True
       with cr False
       have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from 1(1)[OF rec_condition True rec1]
       show ?thesis by fastforce
     next
       case False
       with rec_condition cr
       obtain h1 where swp: "effect (swap a l r) h h1 ()"
         and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from swp rec_condition have
         "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
         unfolding swap_def
         by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
       with 1(2) [OF rec_condition False rec2] show ?thesis by fastforce
     qed
   qed
 qed
 
 
 lemma part_partitions:
   assumes "effect (part1 a l r p) h h' rs"
   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::'a::{heap,linorder} array) ! i \<le> p)
   \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
   using assms
 proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   case (1 a l r p h h' rs)
   note cr = \<open>effect (part1 a l r p) h h' rs\<close>
   
   show ?case
   proof (cases "r \<le> l")
     case True (* Terminating case *)
     with cr have "rs = r"
       unfolding part1.simps[of a l r p]
       by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
     with True
     show ?thesis by auto
   next
     case False (* recursive case *)
     note lr = this
     let ?v = "Array.get h a ! l"
     show ?thesis
     proof (cases "?v \<le> p")
       case True
       with lr cr
       have rec1: "effect (part1 a (l + 1) r p) h h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
         by fastforce
       have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
       with 1(1)[OF False True rec1] a_l show ?thesis
         by auto
     next
       case False
       with lr cr
       obtain h1 where swp: "effect (swap a l r) h h1 ()"
         and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
         unfolding part1.simps[of a l r p]
         by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
       from swp False have "Array.get h1 a ! r \<ge> p"
         unfolding swap_def
         by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
       with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
         by fastforce
       have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
       with 1(2)[OF lr False rec2] a_r show ?thesis
         by auto
     qed
   qed
 qed
 
 
 fun partition :: "'a::{heap,linorder} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
 where
   "partition a left right = do {
      pivot \<leftarrow> Array.nth a right;
      middle \<leftarrow> part1 a left (right - 1) pivot;
      v \<leftarrow> Array.nth a middle;
      m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
      swap a m right;
      return m
    }"
 
 declare partition.simps[simp del]
 
 lemma partition_permutes:
   assumes "effect (partition a l r) h h' rs"
   shows "mset (Array.get h' a) 
   = mset (Array.get h a)"
 proof -
     from assms part_permutes swap_permutes show ?thesis
       unfolding partition.simps
       by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
 qed
 
 lemma partition_length_remains:
   assumes "effect (partition a l r) h h' rs"
   shows "Array.length h a = Array.length h' a"
 proof -
   from assms part_length_remains show ?thesis
     unfolding partition.simps swap_def
     by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
 qed
 
 lemma partition_outer_remains:
   assumes "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
 proof -
   from assms part_outer_remains part_returns_index_in_bounds show ?thesis
     unfolding partition.simps swap_def
     by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastforce
 qed
 
 lemma partition_returns_index_in_bounds:
   assumes effect: "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "l \<le> rs \<and> rs \<le> r"
 proof -
   from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
     and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
          else middle)"
     unfolding partition.simps
     by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp 
   from \<open>l < r\<close> have "l \<le> r - 1" by arith
   from part_returns_index_in_bounds[OF part this] rs_equals \<open>l < r\<close> show ?thesis by auto
 qed
 
 lemma partition_partitions:
   assumes effect: "effect (partition a l r) h h' rs"
   assumes "l < r"
   shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::'a::{heap,linorder} array) ! i \<le> Array.get h' a ! rs) \<and>
   (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
 proof -
   let ?pivot = "Array.get h a ! r" 
   from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
     and swap: "effect (swap a rs r) h1 h' ()"
     and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
          else middle)"
     unfolding partition.simps
     by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
   from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
     (Array.update a rs (Array.get h1 a ! r) h1)"
     unfolding swap_def
     by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
     unfolding swap_def
     by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
     unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
   from \<open>l < r\<close> have "l \<le> r - 1" by simp
   note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   from part_outer_remains[OF part] \<open>l < r\<close>
   have "Array.get h a ! r = Array.get h1 a ! r"
     by fastforce
   with swap
   have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
     unfolding swap_def
     by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
   from part_partitions [OF part]
   show ?thesis
   proof (cases "Array.get h1 a ! middle \<le> ?pivot")
     case True
     with rs_equals have rs_equals: "rs = middle + 1" by simp
     { 
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals \<open>l < r\<close>
       have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
       from i_is_left rs_equals have "l \<le> i \<and> i < middle \<or> i = middle" by arith
       with part_partitions[OF part] right_remains True
       have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
       with i_props h'_def in_bounds have "Array.get h' a ! i \<le> Array.get h' a ! rs"
         unfolding Array.update_def Array.length_def by simp
     }
     moreover
     {
       fix i
       assume "rs < i \<and> i \<le> r"
 
       hence "(rs < i \<and> i \<le> r - 1) \<or> (rs < i \<and> i = r)" by arith
       hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
       proof
         assume i_is: "rs < i \<and> i \<le> r - 1"
         with swap_length_remains in_bounds middle_in_bounds rs_equals
         have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
         from part_partitions[OF part] rs_equals right_remains i_is
         have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
           by fastforce
         with i_props h'_def show ?thesis by fastforce
       next
         assume i_is: "rs < i \<and> i = r"
         with rs_equals have "Suc middle \<noteq> r" by arith
         with middle_in_bounds \<open>l < r\<close> have "Suc middle \<le> r - 1" by arith
         with part_partitions[OF part] right_remains 
         have "Array.get h' a ! rs \<le> Array.get h1 a ! (Suc middle)"
           by fastforce
         with i_is True rs_equals right_remains h'_def
         show ?thesis using in_bounds
           unfolding Array.update_def Array.length_def
           by auto
       qed
     }
     ultimately show ?thesis by auto
   next
     case False
     with rs_equals have rs_equals: "middle = rs" by simp
     { 
       fix i
       assume i_is_left: "l \<le> i \<and> i < rs"
       with swap_length_remains in_bounds middle_in_bounds rs_equals
       have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
       from part_partitions[OF part] rs_equals right_remains i_is_left
       have "Array.get h1 a ! i \<le> Array.get h' a ! rs" by fastforce
       with i_props h'_def have "Array.get h' a ! i \<le> Array.get h' a ! rs"
         unfolding Array.update_def by simp
     }
     moreover
     {
       fix i
       assume "rs < i \<and> i \<le> r"
       hence "(rs < i \<and> i \<le> r - 1) \<or> i = r" by arith
       hence "Array.get h' a ! rs \<le> Array.get h' a ! i"
       proof
         assume i_is: "rs < i \<and> i \<le> r - 1"
         with swap_length_remains in_bounds middle_in_bounds rs_equals
         have i_props: "i < Array.length h' a" "i \<noteq> r" "i \<noteq> rs" by auto
         from part_partitions[OF part] rs_equals right_remains i_is
         have "Array.get h' a ! rs \<le> Array.get h1 a ! i"
           by fastforce
         with i_props h'_def show ?thesis by fastforce
       next
         assume i_is: "i = r"
         from i_is False rs_equals right_remains h'_def
         show ?thesis using in_bounds
           unfolding Array.update_def Array.length_def
           by auto
       qed
     }
     ultimately
     show ?thesis by auto
   qed
 qed
 
 
 function quicksort :: "'a::{heap,linorder} array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap"
 where
   "quicksort arr left right =
      (if (right > left)  then
         do {
           pivotNewIndex \<leftarrow> partition arr left right;
           pivotNewIndex \<leftarrow> assert (\<lambda>x. left \<le> x \<and> x \<le> right) pivotNewIndex;
           quicksort arr left (pivotNewIndex - 1);
           quicksort arr (pivotNewIndex + 1) right
         }
      else return ())"
 by pat_completeness auto
 
 (* For termination, we must show that the pivotNewIndex is between left and right *) 
 termination
 by (relation "measure (\<lambda>(a, l, r). (r - l))") auto
 
 declare quicksort.simps[simp del]
 
 
 lemma quicksort_permutes:
   assumes "effect (quicksort a l r) h h' rs"
   shows "mset (Array.get h' a) 
   = mset (Array.get h a)"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   with partition_permutes show ?case
     unfolding quicksort.simps [of a l r]
     by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
 qed
 
 lemma length_remains:
   assumes "effect (quicksort a l r) h h' rs"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   with partition_length_remains show ?case
     unfolding quicksort.simps [of a l r]
     by (elim effect_ifE effect_bindE effect_assertE effect_returnE) fastforce+
 qed
 
 lemma quicksort_outer_remains:
   assumes "effect (quicksort a l r) h h' rs"
    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::'a::{heap,linorder} array) ! i = Array.get h' a ! i"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   note cr = \<open>effect (quicksort a l r) h h' rs\<close>
   thus ?case
   proof (cases "r > l")
     case False
     with cr have "h' = h"
       unfolding quicksort.simps [of a l r]
       by (elim effect_ifE effect_returnE) auto
     thus ?thesis by simp
   next
   case True
    { 
       fix h1 h2 p ret1 ret2 i
       assume part: "effect (partition a l r) h h1 p"
       assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
       assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
       assume pivot: "l \<le> p \<and> p \<le> r"
       assume i_outer: "i < l \<or> r < i"
       from  partition_outer_remains [OF part True] i_outer
       have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce
       moreover
       from 1(1) [OF True pivot qs1] pivot i_outer 2
       have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto
       moreover
       from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3
       have "Array.get h2 a ! i = Array.get h' a ! i" by auto
       ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
     }
     with cr show ?thesis
       unfolding quicksort.simps [of a l r]
       by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   qed
 qed
 
 lemma quicksort_is_skip:
   assumes "effect (quicksort a l r) h h' rs"
   shows "r \<le> l \<longrightarrow> h = h'"
   using assms
   unfolding quicksort.simps [of a l r]
   by (elim effect_ifE effect_returnE) auto
  
 lemma quicksort_sorts:
   assumes "effect (quicksort a l r) h h' rs"
   assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
   shows "sorted (subarray l (r + 1) a h')"
   using assms
 proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   case (1 a l r h h' rs)
   note cr = \<open>effect (quicksort a l r) h h' rs\<close>
   thus ?case
   proof (cases "r > l")
     case False
     hence "l \<ge> r + 1 \<or> l = r" by arith 
     with length_remains[OF cr] 1(5) show ?thesis
       by (auto simp add: subarray_Nil subarray_single)
   next
     case True
     { 
       fix h1 h2 p
       assume part: "effect (partition a l r) h h1 p"
       assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
       assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
       from partition_returns_index_in_bounds [OF part True]
       have pivot: "l\<le> p \<and> p \<le> r" .
      note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
       from quicksort_outer_remains [OF qs2] quicksort_outer_remains [OF qs1] pivot quicksort_is_skip[OF qs1]
       have pivot_unchanged: "Array.get h1 a ! p = Array.get h' a ! p" by (cases p, auto)
         (*-- First of all, by induction hypothesis both sublists are sorted. *)
       from 1(1)[OF True pivot qs1] length_remains pivot 1(5) 
       have IH1: "sorted (subarray l p a h2)"  by (cases p, auto simp add: subarray_Nil)
       from quicksort_outer_remains [OF qs2] length_remains
       have left_subarray_remains: "subarray l p a h2 = subarray l p a h'"
         by (simp add: subarray_eq_samelength_iff)
       with IH1 have IH1': "sorted (subarray l p a h')" by simp
       from 1(2)[OF True pivot qs2] pivot 1(5) length_remains
       have IH2: "sorted (subarray (p + 1) (r + 1) a h')"
         by (cases "Suc p \<le> r", auto simp add: subarray_Nil)
            (* -- Secondly, both sublists remain partitioned. *)
       from partition_partitions[OF part True]
       have part_conds1: "\<forall>j. j \<in> set (subarray l p a h1) \<longrightarrow> j \<le> Array.get h1 a ! p "
         and part_conds2: "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h1) \<longrightarrow> Array.get h1 a ! p \<le> j"
         by (auto simp add: all_in_set_subarray_conv)
       from quicksort_outer_remains [OF qs1] quicksort_permutes [OF qs1] True
         length_remains 1(5) pivot mset_nths [of l p "Array.get h1 a" "Array.get h2 a"]
       have multiset_partconds1: "mset (subarray l p a h2) = mset (subarray l p a h1)"
         unfolding Array.length_def subarray_def by (cases p, auto)
       with left_subarray_remains part_conds1 pivot_unchanged
       have part_conds2': "\<forall>j. j \<in> set (subarray l p a h') \<longrightarrow> j \<le> Array.get h' a ! p"
         by (simp, subst set_mset_mset[symmetric], simp)
           (* -- These steps are the analogous for the right sublist \<dots> *)
       from quicksort_outer_remains [OF qs1] length_remains
       have right_subarray_remains: "subarray (p + 1) (r + 1) a h1 = subarray (p + 1) (r + 1) a h2"
         by (auto simp add: subarray_eq_samelength_iff)
       from quicksort_outer_remains [OF qs2] quicksort_permutes [OF qs2] True
         length_remains 1(5) pivot mset_nths [of "p + 1" "r + 1" "Array.get h2 a" "Array.get h' a"]
       have multiset_partconds2: "mset (subarray (p + 1) (r + 1) a h') = mset (subarray (p + 1) (r + 1) a h2)"
         unfolding Array.length_def subarray_def by auto
       with right_subarray_remains part_conds2 pivot_unchanged
       have part_conds1': "\<forall>j. j \<in> set (subarray (p + 1) (r + 1) a h') \<longrightarrow> Array.get h' a ! p \<le> j"
         by (simp, subst set_mset_mset[symmetric], simp)
           (* -- Thirdly and finally, we show that the array is sorted
           following from the facts above. *)
       from True pivot 1(5) length_remains have "subarray l (r + 1) a h' = subarray l p a h' @ [Array.get h' a ! p] @ subarray (p + 1) (r + 1) a h'"
         by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil)
       with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis
         unfolding subarray_def
         apply (auto simp add: sorted_append all_in_set_nths'_conv)
         by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"])
     }
     with True cr show ?thesis
       unfolding quicksort.simps [of a l r]
       by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
   qed
 qed
 
 
 lemma quicksort_is_sort:
   assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
   shows "Array.get h' a = sort (Array.get h a)"
 proof (cases "Array.get h a = []")
   case True
   with quicksort_is_skip[OF effect] show ?thesis
   unfolding Array.length_def by simp
 next
   case False
   from quicksort_sorts [OF effect] False have "sorted (nths' 0 (List.length (Array.get h a)) (Array.get h' a))"
     unfolding Array.length_def subarray_def by auto
   with length_remains[OF effect] have "sorted (Array.get h' a)"
     unfolding Array.length_def by simp
   with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastforce
 qed
 
 subsection \<open>No Errors in quicksort\<close>
 text \<open>We have proved that quicksort sorts (if no exceptions occur).
 We will now show that exceptions do not occur.\<close>
 
 lemma success_part1I: 
   assumes "l < Array.length h a" "r < Array.length h a"
   shows "success (part1 a l r p) h"
   using assms
 proof (induct a l r p arbitrary: h rule: part1.induct)
   case (1 a l r p)
   thus ?case unfolding part1.simps [of a l r]
   apply (auto intro!: success_intros simp add: not_le)
   apply (auto intro!: effect_intros)
   done
 qed
 
 lemma success_bindI' [success_intros]: (*FIXME move*)
   assumes "success f h"
   assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
   shows "success (f \<bind> g) h"
 using assms(1) proof (rule success_effectE)
   fix h' r
   assume *: "effect f h h' r"
   with assms(2) have "success (g r) h'" .
   with * show "success (f \<bind> g) h" by (rule success_bind_effectI)
 qed
 
 lemma success_partitionI:
   assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   shows "success (partition a l r) h"
 using assms unfolding partition.simps swap_def
 apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: effect_bindE effect_updE effect_nthE effect_returnE simp add:)
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
 apply auto
 apply (frule part_length_remains)
 apply (frule part_returns_index_in_bounds)
 apply auto
 apply (frule part_length_remains)
 apply auto
 done
 
 lemma success_quicksortI:
   assumes "l < Array.length h a" "r < Array.length h a"
   shows "success (quicksort a l r) h"
 using assms
 proof (induct a l r arbitrary: h rule: quicksort.induct)
   case (1 a l ri h)
   thus ?case
     unfolding quicksort.simps [of a l ri]
     apply (auto intro!: success_ifI success_bindI' success_returnI success_nthI success_updI success_assertI success_partitionI)
     apply (frule partition_returns_index_in_bounds)
     apply auto
     apply (frule partition_returns_index_in_bounds)
     apply auto
     apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
     apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
     apply (erule disjE)
     apply auto
     unfolding quicksort.simps [of a "Suc ri" ri]
     apply (auto intro!: success_ifI success_returnI)
     done
 qed
 
 
 subsection \<open>Example\<close>
 
 definition "qsort a = do {
     k \<leftarrow> Array.len a;
     quicksort a 0 (k - 1);
     return a
   }"
 
 code_reserved SML upto
 
 definition "example = do {
     a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);
     qsort a
   }"
 
 ML_val \<open>@{code example} ()\<close>
 
 export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
diff --git a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
@@ -1,118 +1,118 @@
 (*  Title:      HOL/Imperative_HOL/ex/Imperative_Reverse.thy
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
 section \<open>An imperative in-place reversal on arrays\<close>
 
 theory Imperative_Reverse
-imports Subarray "~~/src/HOL/Imperative_HOL/Imperative_HOL"
+imports Subarray "../Imperative_HOL"
 begin
 
 fun swap :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
   "swap a i j = do {
      x \<leftarrow> Array.nth a i;
      y \<leftarrow> Array.nth a j;
      Array.upd i y a;
      Array.upd j x a;
      return ()
    }"
 
 fun rev :: "'a::heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
   "rev a i j = (if (i < j) then do {
      swap a i j;
      rev a (i + 1) (j - 1)
    }
    else return ())"
 
 declare swap.simps [simp del] rev.simps [simp del]
 
 lemma swap_pointwise: assumes "effect (swap a i j) h h' r"
   shows "Array.get h' a ! k = (if k = i then Array.get h a ! j
       else if k = j then Array.get h a ! i
       else Array.get h a ! k)"
 using assms unfolding swap.simps
 by (elim effect_elims)
  (auto simp: length_def)
 
 lemma rev_pointwise: assumes "effect (rev a i j) h h' r"
   shows "Array.get h' a ! k = (if k < i then Array.get h a ! k
       else if j < k then Array.get h a ! k
       else Array.get h a ! (j - (k - i)))" (is "?P a i j h h'")
 using assms proof (induct a i j arbitrary: h h' rule: rev.induct)
   case (1 a i j h h'')
   thus ?case
   proof (cases "i < j")
     case True
     with 1[unfolded rev.simps[of a i j]]
     obtain h' where
       swp: "effect (swap a i j) h h' ()"
       and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
       by (auto elim: effect_elims)
     from rev 1 True
     have eq: "?P a (i + 1) (j - 1) h' h''" by auto
 
     have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith
     with True show ?thesis
       by (elim disjE) (auto simp: eq swap_pointwise[OF swp])
   next
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
       by (cases "k = j") (auto elim: effect_elims)
   qed
 qed
 
 lemma rev_length:
   assumes "effect (rev a i j) h h' r"
   shows "Array.length h a = Array.length h' a"
 using assms
 proof (induct a i j arbitrary: h h' rule: rev.induct)
   case (1 a i j h h'')
   thus ?case
   proof (cases "i < j")
     case True
     with 1[unfolded rev.simps[of a i j]]
     obtain h' where
       swp: "effect (swap a i j) h h' ()"
       and rev: "effect (rev a (i + 1) (j - 1)) h' h'' ()"
       by (auto elim: effect_elims)
     from swp rev 1 True show ?thesis
       unfolding swap.simps
       by (elim effect_elims) fastforce
   next
     case False
     with 1[unfolded rev.simps[of a i j]]
     show ?thesis
       by (auto elim: effect_elims)
   qed
 qed
 
 lemma rev2_rev': assumes "effect (rev a i j) h h' u"
   assumes "j < Array.length h a"
   shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)"
 proof - 
   {
     fix k
     assume "k < Suc j - i"
     with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j - k)"
       by auto
   } 
   with assms(2) rev_length[OF assms(1)] show ?thesis
   unfolding subarray_def Array.length_def
   by (auto simp add: length_nths' rev_nth min_def nth_nths' intro!: nth_equalityI)
 qed
 
 lemma rev2_rev: 
   assumes "effect (rev a 0 (Array.length h a - 1)) h h' u"
   shows "Array.get h' a = List.rev (Array.get h a)"
   using rev2_rev'[OF assms] rev_length[OF assms] assms
     by (cases "Array.length h a = 0", auto simp add: Array.length_def
       subarray_def rev.simps[where j=0] elim!: effect_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
 definition "example = (Array.make 10 id \<bind> (\<lambda>a. rev a 0 9))"
 
 export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
 
 end
 
diff --git a/src/HOL/Imperative_HOL/ex/Subarray.thy b/src/HOL/Imperative_HOL/ex/Subarray.thy
--- a/src/HOL/Imperative_HOL/ex/Subarray.thy
+++ b/src/HOL/Imperative_HOL/ex/Subarray.thy
@@ -1,71 +1,71 @@
 (*  Title:      HOL/Imperative_HOL/ex/Subarray.thy
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
 section \<open>Theorems about sub arrays\<close>
 
 theory Subarray
-imports "~~/src/HOL/Imperative_HOL/Array" List_Sublist
+imports "../Array" List_Sublist
 begin
 
 definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
   "subarray n m a h \<equiv> nths' n m (Array.get h a)"
 
 lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
 apply (simp add: subarray_def Array.update_def)
 apply (simp add: nths'_update1)
 done
 
 lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
 apply (simp add: subarray_def Array.update_def)
 apply (subst nths'_update2)
 apply fastforce
 apply simp
 done
 
 lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = (subarray n m a h)[i - n := v]"
 unfolding subarray_def Array.update_def
 by (simp add: nths'_update3)
 
 lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"
 by (simp add: subarray_def nths'_Nil')
 
 lemma subarray_single: "\<lbrakk> n < Array.length h a \<rbrakk> \<Longrightarrow> subarray n (Suc n) a h = [Array.get h a ! n]" 
 by (simp add: subarray_def length_def nths'_single)
 
 lemma length_subarray: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray n m a h) = m - n"
 by (simp add: subarray_def length_def length_nths')
 
 lemma length_subarray_0: "m \<le> Array.length h a \<Longrightarrow> List.length (subarray 0 m a h) = m"
 by (simp add: length_subarray)
 
 lemma subarray_nth_array_Cons: "\<lbrakk> i < Array.length h a; i < j \<rbrakk> \<Longrightarrow> (Array.get h a ! i) # subarray (Suc i) j a h = subarray i j a h"
 unfolding Array.length_def subarray_def
 by (simp add: nths'_front)
 
 lemma subarray_nth_array_back: "\<lbrakk> i < j; j \<le> Array.length h a\<rbrakk> \<Longrightarrow> subarray i j a h = subarray i (j - 1) a h @ [Array.get h a ! (j - 1)]"
 unfolding Array.length_def subarray_def
 by (simp add: nths'_back)
 
 lemma subarray_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow> subarray i j a h @ subarray j k a h = subarray i k a h"
 unfolding subarray_def
 by (simp add: nths'_append)
 
 lemma subarray_all: "subarray 0 (Array.length h a) a h = Array.get h a"
 unfolding Array.length_def subarray_def
 by (simp add: nths'_all)
 
 lemma nth_subarray: "\<lbrakk> k < j - i; j \<le> Array.length h a \<rbrakk> \<Longrightarrow> subarray i j a h ! k = Array.get h a ! (i + k)"
 unfolding Array.length_def subarray_def
 by (simp add: nth_nths')
 
 lemma subarray_eq_samelength_iff: "Array.length h a = Array.length h' a \<Longrightarrow> (subarray i j a h = subarray i j a h') = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> Array.get h a ! i' = Array.get h' a ! i')"
 unfolding Array.length_def subarray_def by (rule nths'_eq_samelength_iff)
 
 lemma all_in_set_subarray_conv: "(\<forall>j. j \<in> set (subarray l r a h) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
 unfolding subarray_def Array.length_def by (rule all_in_set_nths'_conv)
 
 lemma ball_in_set_subarray_conv: "(\<forall>j \<in> set (subarray l r a h). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < Array.length h a \<longrightarrow> P (Array.get h a ! k))"
 unfolding subarray_def Array.length_def by (rule ball_in_set_nths'_conv)
 
 end
diff --git a/src/HOL/Number_Theory/Totient.thy b/src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy
+++ b/src/HOL/Number_Theory/Totient.thy
@@ -1,561 +1,561 @@
 (*  Title:      HOL/Number_Theory/Totient.thy
     Author:     Jeremy Avigad
     Author:     Florian Haftmann
     Author:     Manuel Eberl
 *)
 
 section \<open>Fundamental facts about Euler's totient function\<close>
 
 theory Totient
 imports
   Complex_Main
   "HOL-Computational_Algebra.Primes"
-  "~~/src/HOL/Number_Theory/Cong"
+  Cong
 begin
   
 definition totatives :: "nat \<Rightarrow> nat set" where
   "totatives n = {k \<in> {0<..n}. coprime k n}"
 
 lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
   by (simp add: totatives_def)
   
 lemma totatives_code [code]: "totatives n = Set.filter (\<lambda>k. coprime k n) {0<..n}"
   by (simp add: totatives_def Set.filter_def)
   
 lemma finite_totatives [simp]: "finite (totatives n)"
   by (simp add: totatives_def)
     
 lemma totatives_subset: "totatives n \<subseteq> {0<..n}"
   by (auto simp: totatives_def)
     
 lemma zero_not_in_totatives [simp]: "0 \<notin> totatives n"
   by (auto simp: totatives_def)
     
 lemma totatives_le: "x \<in> totatives n \<Longrightarrow> x \<le> n"
   by (auto simp: totatives_def)
     
 lemma totatives_less: 
   assumes "x \<in> totatives n" "n > 1"
   shows   "x < n"
 proof -
   from assms have "x \<noteq> n" by (auto simp: totatives_def)
   with totatives_le[OF assms(1)] show ?thesis by simp
 qed
 
 lemma totatives_0 [simp]: "totatives 0 = {}"
   by (auto simp: totatives_def)
 
 lemma totatives_1 [simp]: "totatives 1 = {Suc 0}"
   by (auto simp: totatives_def)
 
 lemma totatives_Suc_0 [simp]: "totatives (Suc 0) = {Suc 0}"
   by (auto simp: totatives_def)
 
 lemma one_in_totatives [simp]: "n > 0 \<Longrightarrow> Suc 0 \<in> totatives n"
   by (auto simp: totatives_def)
 
 lemma totatives_eq_empty_iff [simp]: "totatives n = {} \<longleftrightarrow> n = 0"
   using one_in_totatives[of n] by (auto simp del: one_in_totatives)
     
 lemma minus_one_in_totatives:
   assumes "n \<ge> 2"
   shows "n - 1 \<in> totatives n"
   using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
 
 lemma power_in_totatives:
   assumes "m > 1" "coprime m g"
   shows   "g ^ i mod m \<in> totatives m"
 proof -
   have "\<not>m dvd g ^ i"
   proof
     assume "m dvd g ^ i"
     hence "\<not>coprime m (g ^ i)"
       using \<open>m > 1\<close> by (subst coprime_absorb_left) auto
     with \<open>coprime m g\<close> show False by simp
   qed
   with assms show ?thesis
     by (auto simp: totatives_def coprime_commute intro!: Nat.gr0I)
 qed
 
 lemma totatives_prime_power_Suc:
   assumes "prime p"
   shows   "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m) ` {0<..p^n}"
 proof safe
   fix m assume m: "p * m \<in> totatives (p ^ Suc n)" and m: "m \<in> {0<..p^n}"
   thus False using assms by (auto simp: totatives_def gcd_mult_left)
 next
   fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
   from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
   hence "coprime k (p ^ Suc n)"
     using prime_imp_coprime [OF assms, of k]
     by (cases "n > 0") (auto simp add: ac_simps)
   with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
 qed (auto simp: totatives_def)
 
 lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
   using totatives_prime_power_Suc [of p 0] by auto
 
 lemma bij_betw_totatives:
   assumes "m1 > 1" "m2 > 1" "coprime m1 m2"
   shows   "bij_betw (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2)) 
              (totatives m1 \<times> totatives m2)"
   unfolding bij_betw_def
 proof
   show "inj_on (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2))"
   proof (intro inj_onI, clarify)
     fix x y assume xy: "x \<in> totatives (m1 * m2)" "y \<in> totatives (m1 * m2)"
                        "x mod m1 = y mod m1" "x mod m2 = y mod m2"
     have ex: "\<exists>!z. z < m1 * m2 \<and> [z = x] (mod m1) \<and> [z = x] (mod m2)"
       by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all)
     have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)"
          "y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)"
       using xy assms by (simp_all add: totatives_less one_less_mult cong_def)
     from this[THEN the1_equality[OF ex]] show "x = y" by simp
   qed
 next
   show "(\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1 * m2) = totatives m1 \<times> totatives m2"
   proof safe
     fix x assume "x \<in> totatives (m1 * m2)"
     with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
       using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
       by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
   next
     fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
     with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
     with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
       where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
     from x ab assms(3) have "x \<in> totatives (m1 * m2)"
       by (auto intro: ccontr simp add: in_totatives_iff)
     with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   qed
 qed
 
 lemma bij_betw_totatives_gcd_eq:
   fixes n d :: nat
   assumes "d dvd n" "n > 0"
   shows   "bij_betw (\<lambda>k. k * d) (totatives (n div d)) {k\<in>{0<..n}. gcd k n = d}"
   unfolding bij_betw_def
 proof
   show "inj_on (\<lambda>k. k * d) (totatives (n div d))"
     by (auto simp: inj_on_def)
 next
   show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
   proof (intro equalityI subsetI, goal_cases)
     case (1 k)
     then show ?case using assms
       by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
   next
     case (2 k)
     hence "d dvd k" by auto
     then obtain l where k: "k = l * d" by (elim dvdE) auto
     from 2 assms show ?case
       using gcd_mult_right [of _ d l]
       by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
   qed
 qed
 
 definition totient :: "nat \<Rightarrow> nat" where
   "totient n = card (totatives n)"
   
 primrec totient_naive :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "totient_naive 0 acc n = acc"
 | "totient_naive (Suc k) acc n =
      (if coprime (Suc k) n then totient_naive k (acc + 1) n else totient_naive k acc n)"
   
 lemma totient_naive:
   "totient_naive k acc n = card {x \<in> {0<..k}. coprime x n} + acc"
 proof (induction k arbitrary: acc)
   case (Suc k acc)
   have "totient_naive (Suc k) acc n = 
           (if coprime (Suc k) n then 1 else 0) + card {x \<in> {0<..k}. coprime x n} + acc"
     using Suc by simp
   also have "(if coprime (Suc k) n then 1 else 0) = 
                card (if coprime (Suc k) n then {Suc k} else {})" by auto
   also have "\<dots> + card {x \<in> {0<..k}. coprime x n} =
                card ((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n})"
     by (intro card_Un_disjoint [symmetric]) auto
   also have "((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n}) =
                {x \<in> {0<..Suc k}. coprime x n}" by (auto elim: le_SucE)
   finally show ?case .
 qed simp_all
   
 lemma totient_code_naive [code]: "totient n = totient_naive n 0 n"
   by (subst totient_naive) (simp add: totient_def totatives_def)
 
 lemma totient_le: "totient n \<le> n"
 proof -
   have "card (totatives n) \<le> card {0<..n}"
     by (intro card_mono) (auto simp: totatives_def)
   thus ?thesis by (simp add: totient_def)
 qed
   
 lemma totient_less: 
   assumes "n > 1"
   shows "totient n < n"
 proof -
   from assms have "card (totatives n) \<le> card {0<..<n}"
     using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto
   with assms show ?thesis by (simp add: totient_def)
 qed    
 
 lemma totient_0 [simp]: "totient 0 = 0"
   by (simp add: totient_def)
 
 lemma totient_Suc_0 [simp]: "totient (Suc 0) = Suc 0"
   by (simp add: totient_def)
 
 lemma totient_1 [simp]: "totient 1 = Suc 0"
   by simp
 
 lemma totient_0_iff [simp]: "totient n = 0 \<longleftrightarrow> n = 0"
   by (auto simp: totient_def)
 
 lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0"
   by (auto intro: Nat.gr0I)
 
 lemma totient_gt_1:
   assumes "n > 2"
   shows   "totient n > 1"
 proof -
   have "{1, n - 1} \<subseteq> totatives n"
     using assms coprime_diff_one_left_nat[of n] by (auto simp: totatives_def)
   hence "card {1, n - 1} \<le> card (totatives n)"
     by (intro card_mono) auto
   thus ?thesis using assms
     by (simp add: totient_def)
 qed
 
 lemma card_gcd_eq_totient:
   "n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)"
   unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq])
   
 lemma totient_divisor_sum: "(\<Sum>d | d dvd n. totient d) = n"
 proof (cases "n = 0")
   case False
   hence "n > 0" by simp
   define A where "A = (\<lambda>d. {k\<in>{0<..n}. gcd k n = d})"
   have *: "card (A d) = totient (n div d)" if d: "d dvd n" for d
     using \<open>n > 0\<close> and d unfolding A_def by (rule card_gcd_eq_totient)  
   have "n = card {1..n}" by simp
   also have "{1..n} = (\<Union>d\<in>{d. d dvd n}. A d)" by safe (auto simp: A_def)
   also have "card \<dots> = (\<Sum>d | d dvd n. card (A d))"
     using \<open>n > 0\<close> by (intro card_UN_disjoint) (auto simp: A_def)
   also have "\<dots> = (\<Sum>d | d dvd n. totient (n div d))" by (intro sum.cong refl *) auto
   also have "\<dots> = (\<Sum>d | d dvd n. totient d)" using \<open>n > 0\<close>
     by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim: dvdE)
   finally show ?thesis ..
 qed auto
 
 lemma totient_mult_coprime:
   assumes "coprime m n"
   shows   "totient (m * n) = totient m * totient n"
 proof (cases "m > 1 \<and> n > 1")
   case True
   hence mn: "m > 1" "n > 1" by simp_all
   have "totient (m * n) = card (totatives (m * n))" by (simp add: totient_def)
   also have "\<dots> = card (totatives m \<times> totatives n)"
     using bij_betw_totatives [OF mn \<open>coprime m n\<close>] by (rule bij_betw_same_card)
   also have "\<dots> = totient m * totient n" by (simp add: totient_def)
   finally show ?thesis .
 next
   case False
   with assms show ?thesis by (cases m; cases n) auto
 qed
 
 lemma totient_prime_power_Suc:
   assumes "prime p"
   shows   "totient (p ^ Suc n) = p ^ n * (p - 1)"
 proof -
   from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - (*) p ` {0<..p ^ n})"
     unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
   also from assms have "\<dots> = p ^ Suc n - card ((*) p ` {0<..p^n})"
     by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
   also from assms have "card ((*) p ` {0<..p^n}) = p ^ n"
     by (subst card_image) (auto simp: inj_on_def)
   also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
   finally show ?thesis .
 qed
 
 lemma totient_prime_power:
   assumes "prime p" "n > 0"
   shows   "totient (p ^ n) = p ^ (n - 1) * (p - 1)"
   using totient_prime_power_Suc[of p "n - 1"] assms by simp
 
 lemma totient_imp_prime:
   assumes "totient p = p - 1" "p > 0"
   shows   "prime p"
 proof (cases "p = 1")
   case True
   with assms show ?thesis by auto
 next
   case False
   with assms have p: "p > 1" by simp
   have "x \<in> {0<..<p}" if "x \<in> totatives p" for x
     using that and p by (cases "x = p") (auto simp: totatives_def)
   with assms have *: "totatives p = {0<..<p}"
     by (intro card_subset_eq) (auto simp: totient_def)
   have **: False if "x \<noteq> 1" "x \<noteq> p" "x dvd p" for x
   proof -
     from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
     from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
     from that and nz have "\<not>coprime x p"
       by (auto elim: dvdE)
     hence "x \<notin> totatives p" by (simp add: totatives_def)
     also note *
     finally show False using that and le by auto
   qed
   hence "(\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)" by blast
   with p show ?thesis by (subst prime_nat_iff) (auto dest: **)
 qed
     
 lemma totient_prime:
   assumes "prime p"
   shows   "totient p = p - 1"
   using totient_prime_power_Suc[of p 0] assms by simp
 
 lemma totient_2 [simp]: "totient 2 = 1"
   and totient_3 [simp]: "totient 3 = 2"
   and totient_5 [simp]: "totient 5 = 4"
   and totient_7 [simp]: "totient 7 = 6"
   by (subst totient_prime; simp)+
     
 lemma totient_4 [simp]: "totient 4 = 2"
   and totient_8 [simp]: "totient 8 = 4"
   and totient_9 [simp]: "totient 9 = 6"
   using totient_prime_power[of 2 2] totient_prime_power[of 2 3] totient_prime_power[of 3 2] 
   by simp_all
     
 lemma totient_6 [simp]: "totient 6 = 2"
   using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
   by simp
 
 lemma totient_even:
   assumes "n > 2"
   shows   "even (totient n)"
 proof (cases "\<exists>p. prime p \<and> p \<noteq> 2 \<and> p dvd n")
   case True
   then obtain p where p: "prime p" "p \<noteq> 2" "p dvd n" by auto
   from \<open>p \<noteq> 2\<close> have "p = 0 \<or> p = 1 \<or> p > 2" by auto
   with p(1) have "odd p" using prime_odd_nat[of p] by auto
   define k where "k = multiplicity p n"
   from p assms have k_pos: "k > 0" unfolding k_def by (subst multiplicity_gt_zero_iff) auto
   have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
   then obtain m where m: "n = p ^ k * m" by (elim dvdE)
   with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
   from k_def m_pos p have "\<not> p dvd m"
     by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib 
                           prime_elem_multiplicity_eq_zero_iff)
   with \<open>prime p\<close> have "coprime p m"
     by (rule prime_imp_coprime)
   with \<open>k > 0\<close> have "coprime (p ^ k) m"
     by simp
   then show ?thesis using p k_pos \<open>odd p\<close> 
     by (auto simp add: m totient_mult_coprime totient_prime_power)
 next
   case False
   from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
     by (intro Primes.prime_factorization_nat) auto
   also from False have "\<dots> = (\<Prod>p\<in>prime_factors n. if p = 2 then 2 ^ multiplicity 2 n else 1)"
     by (intro prod.cong refl) auto
   also have "\<dots> = 2 ^ multiplicity 2 n" 
     by (subst prod.delta[OF finite_set_mset]) (auto simp: prime_factors_multiplicity)
   finally have n: "n = 2 ^ multiplicity 2 n" .
   have "multiplicity 2 n = 0 \<or> multiplicity 2 n = 1 \<or> multiplicity 2 n > 1" by force
   with n assms have "multiplicity 2 n > 1" by auto
   thus ?thesis by (subst n) (simp add: totient_prime_power)
 qed
 
 lemma totient_prod_coprime:
   assumes "pairwise coprime (f ` A)" "inj_on f A"
   shows   "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))"
   using assms
 proof (induction A rule: infinite_finite_induct)
   case (insert x A)
   have *: "coprime (prod f A) (f x)"
   proof (rule prod_coprime_left)
     fix y
     assume "y \<in> A"
     with \<open>x \<notin> A\<close> have "y \<noteq> x"
       by auto
     with \<open>x \<notin> A\<close> \<open>y \<in> A\<close> \<open>inj_on f (insert x A)\<close> have "f y \<noteq> f x"
       using inj_onD [of f "insert x A" y x]
       by auto
     with \<open>y \<in> A\<close> show "coprime (f y) (f x)"
       using pairwiseD [OF \<open>pairwise coprime (f ` insert x A)\<close>]
       by auto
   qed
   from insert.hyps have "prod f (insert x A) = prod f A * f x" by simp
   also have "totient \<dots> = totient (prod f A) * totient (f x)"
     using insert.hyps insert.prems by (intro totient_mult_coprime *)
   also have "totient (prod f A) = (\<Prod>a\<in>A. totient (f a))" 
     using insert.prems by (intro insert.IH) (auto dest: pairwise_subset)
   also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>a\<in>insert x A. totient (f a))" by simp
   finally show ?case .
 qed simp_all
 
 (* TODO Move *)
 lemma prime_power_eq_imp_eq:
   fixes p q :: "'a :: factorial_semiring"
   assumes "prime p" "prime q" "m > 0"
   assumes "p ^ m = q ^ n"
   shows   "p = q"
 proof (rule ccontr)
   assume pq: "p \<noteq> q"
   from assms have "m = multiplicity p (p ^ m)" 
     by (subst multiplicity_prime_power) auto
   also note \<open>p ^ m = q ^ n\<close>
   also from assms pq have "multiplicity p (q ^ n) = 0"
     by (subst multiplicity_distinct_prime_power) auto
   finally show False using \<open>m > 0\<close> by simp
 qed
 
 lemma totient_formula1:
   assumes "n > 0"
   shows   "totient n = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))"
 proof -
   from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
     by (rule prime_factorization_nat)
   also have "totient \<dots> = (\<Prod>x\<in>prime_factors n. totient (x ^ multiplicity x n))"
   proof (rule totient_prod_coprime)
     show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
     proof (rule pairwiseI, clarify)
       fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
                      "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
       then have "multiplicity p n > 0" "multiplicity q n > 0"
         by (simp_all add: prime_factors_multiplicity)
       with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
         by auto
     qed
   next
     show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
     proof
       fix p q assume pq: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
                          "p ^ multiplicity p n = q ^ multiplicity q n"
       from assms and pq have "prime p" "prime q" "multiplicity p n > 0" 
         by (simp_all add: prime_factors_multiplicity)
       from prime_power_eq_imp_eq[OF this pq(3)] show "p = q" .
     qed
   qed
   also have "\<dots> = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))"
     by (intro prod.cong refl totient_prime_power) (auto simp: prime_factors_multiplicity)
   finally show ?thesis .
 qed
 
 lemma totient_dvd:
   assumes "m dvd n"
   shows   "totient m dvd totient n"
 proof (cases "m = 0 \<or> n = 0")
   case False
   let ?M = "\<lambda>p m :: nat. multiplicity p m - 1"
   have "(\<Prod>p\<in>prime_factors m. p ^ ?M p m * (p - 1)) dvd
           (\<Prod>p\<in>prime_factors n. p ^ ?M p n * (p - 1))" using assms False
     by (intro prod_dvd_prod_subset2 mult_dvd_mono dvd_refl le_imp_power_dvd diff_le_mono
               dvd_prime_factors dvd_imp_multiplicity_le) auto
   with False show ?thesis by (simp add: totient_formula1)
 qed (insert assms, auto)
   
 lemma totient_dvd_mono:
   assumes "m dvd n" "n > 0"
   shows   "totient m \<le> totient n"
   by (cases "m = 0") (insert assms, auto intro: dvd_imp_le totient_dvd)
 
 (* TODO Move *)
 lemma prime_factors_power: "n > 0 \<Longrightarrow> prime_factors (x ^ n) = prime_factors x"
   by (cases "x = 0"; cases "n = 0")
      (auto simp: prime_factors_multiplicity prime_elem_multiplicity_power_distrib zero_power)
 
 lemma totient_formula2:
   "real (totient n) = real n * (\<Prod>p\<in>prime_factors n. 1 - 1 / real p)"
 proof (cases "n = 0")
   case False
   have "real (totient n) = (\<Prod>p\<in>prime_factors n. real
           (p ^ (multiplicity p n - 1) * (p - 1)))" 
     using False by (subst totient_formula1) simp_all
   also have "\<dots> = (\<Prod>p\<in>prime_factors n. real (p ^ multiplicity p n) * (1 - 1 / real p))"
     by (intro prod.cong refl) (auto simp add: field_simps prime_factors_multiplicity 
           prime_ge_Suc_0_nat of_nat_diff power_Suc [symmetric] simp del: power_Suc)
   also have "\<dots> = real (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) * 
                     (\<Prod>p\<in>prime_factors n. 1 - 1 / real p)" by (subst prod.distrib) auto
   also have "(\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n"
     using False by (intro Primes.prime_factorization_nat [symmetric]) auto
   finally show ?thesis .
 qed auto
 
 lemma totient_gcd: "totient (a * b) * totient (gcd a b) = totient a * totient b * gcd a b"
 proof (cases "a = 0 \<or> b = 0")
   case False
   let ?P = "prime_factors :: nat \<Rightarrow> nat set"
   have "real (totient a * totient b * gcd a b) = real (a * b * gcd a b) *
           ((\<Prod>p\<in>?P a. 1 - 1 / real p) * (\<Prod>p\<in>?P b. 1 - 1 / real p))"
     by (simp add: totient_formula2)
   also have "?P a = (?P a - ?P b) \<union> (?P a \<inter> ?P b)" by auto
   also have "(\<Prod>p\<in>\<dots>. 1 - 1 / real p) = 
                  (\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)"
     by (rule prod.union_disjoint) blast+
   also have "\<dots> * (\<Prod>p\<in>?P b. 1 - 1 / real p) = (\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * 
                (\<Prod>p\<in>?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)" (is "_ = ?A * _")
     by (simp only: mult_ac)
   also have "?A = (\<Prod>p\<in>?P a - ?P b \<union> ?P b. 1 - 1 / real p)"
     by (rule prod.union_disjoint [symmetric]) blast+
   also have "?P a - ?P b \<union> ?P b = ?P a \<union> ?P b" by blast
   also have "real (a * b * gcd a b) * ((\<Prod>p\<in>\<dots>. 1 - 1 / real p) * 
                  (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)) = real (totient (a * b) * totient (gcd a b))"
     using False by (simp add: totient_formula2 prime_factors_product prime_factorization_gcd)
   finally show ?thesis by (simp only: of_nat_eq_iff)
 qed auto
   
 lemma totient_mult: "totient (a * b) = totient a * totient b * gcd a b div totient (gcd a b)"
   by (subst totient_gcd [symmetric]) simp
 
 lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
   by (fact of_nat_eq_1_iff)
 
 (* TODO Move *)
 lemma odd_imp_coprime_nat:
   assumes "odd (n::nat)"
   shows   "coprime n 2"
 proof -
   from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
   have "coprime (Suc (2 * k)) (2 * k)"
     by (fact coprime_Suc_left_nat)
   then show ?thesis using n
     by simp
 qed
 
 lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
   by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
 
 lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
 proof (induction m arbitrary: n)
   case (Suc m n)
   have "totient (n ^ Suc (Suc m)) = totient (n * n ^ Suc m)" by simp
   also have "\<dots> = n ^ Suc m * totient n"
     using Suc.IH by (subst totient_mult) simp
   finally show ?case .
 qed simp_all
   
 lemma totient_power: "m > 0 \<Longrightarrow> totient (n ^ m) = n ^ (m - 1) * totient n"
   using totient_power_Suc[of n "m - 1"] by (cases m) simp_all
 
 lemma totient_gcd_lcm: "totient (gcd a b) * totient (lcm a b) = totient a * totient b"
 proof (cases "a = 0 \<or> b = 0")
   case False
   let ?P = "prime_factors :: nat \<Rightarrow> nat set" and ?f = "\<lambda>p::nat. 1 - 1 / real p"
   have "real (totient (gcd a b) * totient (lcm a b)) = real (gcd a b * lcm a b) * 
           (prod ?f (?P a \<inter> ?P b) * prod ?f (?P a \<union> ?P b))"
     using False unfolding of_nat_mult 
     by (simp add: totient_formula2 prime_factorization_gcd prime_factorization_lcm)
   also have "gcd a b * lcm a b = a * b" by simp
   also have "?P a \<union> ?P b = (?P a - ?P a \<inter> ?P b) \<union> ?P b" by blast
   also have "prod ?f \<dots> = prod ?f (?P a - ?P a \<inter> ?P b) * prod ?f (?P b)"
     by (rule prod.union_disjoint) blast+
   also have "prod ?f (?P a \<inter> ?P b) * \<dots> = 
                prod ?f (?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b)) * prod ?f (?P b)"
     by (subst prod.union_disjoint) auto
   also have "?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b) = ?P a" by blast
   also have "real (a * b) * (prod ?f (?P a) * prod ?f (?P b)) = real (totient a * totient b)"
     using False by (simp add: totient_formula2)
   finally show ?thesis by (simp only: of_nat_eq_iff)
 qed auto    
 
 end
diff --git a/src/HOL/Probability/Random_Permutations.thy b/src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy
+++ b/src/HOL/Probability/Random_Permutations.thy
@@ -1,231 +1,231 @@
 (*  
   Title:    Random_Permutations.thy
   Author:   Manuel Eberl, TU München
 
   Random permutations and folding over them.
   This provides the basic theory for the concept of doing something
   in a random order, e.g. inserting elements from a fixed set into a 
   data structure in random order.
 *)
 
 section \<open>Random Permutations\<close>
 
 theory Random_Permutations
 imports 
-  "~~/src/HOL/Probability/Probability_Mass_Function" 
+  Probability_Mass_Function
   "HOL-Library.Multiset_Permutations"
 begin
 
 text \<open>
   Choosing a set permutation (i.e. a distinct list with the same elements as the set)
   uniformly at random is the same as first choosing the first element of the list
   and then choosing the rest of the list as a permutation of the remaining set.
 \<close>
 lemma random_permutation_of_set:
   assumes "finite A" "A \<noteq> {}"
   shows   "pmf_of_set (permutations_of_set A) = 
              do {
                x \<leftarrow> pmf_of_set A;
                xs \<leftarrow> pmf_of_set (permutations_of_set (A - {x})); 
                return_pmf (x#xs)
              }" (is "?lhs = ?rhs")
 proof -
   from assms have "permutations_of_set A = (\<Union>x\<in>A. (#) x ` permutations_of_set (A - {x}))"
     by (simp add: permutations_of_set_nonempty)
   also from assms have "pmf_of_set \<dots> = ?rhs"
     by (subst pmf_of_set_UN[where n = "fact (card A - 1)"])
        (auto simp: card_image disjoint_family_on_def map_pmf_def [symmetric] map_pmf_of_set_inj)
   finally show ?thesis .
 qed
 
 
 text \<open>
   A generic fold function that takes a function, an initial state, and a set 
   and chooses a random order in which it then traverses the set in the same 
   fashion as a left fold over a list.
     We first give a recursive definition.
 \<close>
 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where
   "fold_random_permutation f x {} = return_pmf x"
 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x"
 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> 
      fold_random_permutation f x A = 
        pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))"
   by simp_all fastforce
 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)")
   fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a
   assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
   then have "card A > 0" by (simp add: card_gt_0_iff)
   with A show "((f, f y x, A - {y}), f, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, A). card A)"
     by simp
 qed simp_all
 
 
 text \<open>
   We can now show that the above recursive definition is equivalent to 
   choosing a random set permutation and folding over it (in any direction).
 \<close>
 lemma fold_random_permutation_foldl:
   assumes "finite A"
   shows   "fold_random_permutation f x A =
              map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))"
 using assms
 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove])
   case (remove A f x)
   from remove 
     have "fold_random_permutation f x A = 
             pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))" by simp
   also from remove
     have "\<dots> = pmf_of_set A \<bind> (\<lambda>a. map_pmf (foldl (\<lambda>x y. f y x) x)
                  (map_pmf ((#) a) (pmf_of_set (permutations_of_set (A - {a})))))"
       by (intro bind_pmf_cong) (simp_all add: pmf.map_comp o_def)
   also from remove have "\<dots> = map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set A))"
     by (simp_all add: random_permutation_of_set map_bind_pmf map_pmf_def [symmetric])
   finally show ?case .
 qed (simp_all add: pmf_of_set_singleton)
 
 lemma fold_random_permutation_foldr:
   assumes "finite A"
   shows   "fold_random_permutation f x A =
              map_pmf (\<lambda>xs. foldr f xs x) (pmf_of_set (permutations_of_set A))"
 proof -
   have "fold_random_permutation f x A =
           map_pmf (foldl (\<lambda>x y. f y x) x \<circ> rev) (pmf_of_set (permutations_of_set A))"
     using assms by (subst fold_random_permutation_foldl [OF assms])
                    (simp_all add: pmf.map_comp [symmetric] map_pmf_of_set_inj)
   also have "foldl (\<lambda>x y. f y x) x \<circ> rev = (\<lambda>xs. foldr f xs x)"
     by (intro ext) (simp add: foldl_conv_foldr)
   finally show ?thesis .
 qed
 
 lemma fold_random_permutation_fold:
   assumes "finite A"
   shows   "fold_random_permutation f x A =
              map_pmf (\<lambda>xs. fold f xs x) (pmf_of_set (permutations_of_set A))"
   by (subst fold_random_permutation_foldl [OF assms], intro map_pmf_cong)
      (simp_all add: foldl_conv_fold)
      
 lemma fold_random_permutation_code [code]: 
   "fold_random_permutation f x (set xs) =
      map_pmf (foldl (\<lambda>x y. f y x) x) (pmf_of_set (permutations_of_set (set xs)))"
   by (simp add: fold_random_permutation_foldl)
 
 text \<open>
   We now introduce a slightly generalised version of the above fold 
   operation that does not simply return the result in the end, but applies
   a monadic bind to it.
     This may seem somewhat arbitrary, but it is a common use case, e.g. 
   in the Social Decision Scheme of Random Serial Dictatorship, where 
   voters narrow down a set of possible winners in a random order and 
   the winner is chosen from the remaining set uniformly at random.
 \<close>
 function fold_bind_random_permutation 
     :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c pmf) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'c pmf" where
   "fold_bind_random_permutation f g x {} = g x"
 | "\<not>finite A \<Longrightarrow> fold_bind_random_permutation f g x A = g x"
 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> 
      fold_bind_random_permutation f g x A = 
        pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))"
   by simp_all fastforce
 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)")
   fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b 
     and y :: 'a and g :: "'b \<Rightarrow> 'c pmf"
   assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
   then have "card A > 0" by (simp add: card_gt_0_iff)
   with A show "((f, g, f y x, A - {y}), f, g, x, A) \<in> Wellfounded.measure (\<lambda>(_, _, _, A). card A)"
     by simp
 qed simp_all
 
 text \<open>
   We now show that the recursive definition is equivalent to 
   a random fold followed by a monadic bind.
 \<close>
 lemma fold_bind_random_permutation_altdef [code]:
   "fold_bind_random_permutation f g x A = fold_random_permutation f x A \<bind> g"
 proof (induction f x A rule: fold_random_permutation.induct [case_names empty infinite remove])
   case (remove A f x)
   from remove have "pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a})) =
                       pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}) \<bind> g)"
     by (intro bind_pmf_cong) simp_all
   with remove show ?case by (simp add: bind_return_pmf bind_assoc_pmf)
 qed (simp_all add: bind_return_pmf)
 
 
 text \<open>
   We can now derive the following nice monadic representations of the 
   combined fold-and-bind:
 \<close>
 lemma fold_bind_random_permutation_foldl:
   assumes "finite A"
   shows   "fold_bind_random_permutation f g x A =
              do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldl (\<lambda>x y. f y x) x xs)}"
   using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf
                             fold_random_permutation_foldl bind_return_pmf map_pmf_def)
 
 lemma fold_bind_random_permutation_foldr:
   assumes "finite A"
   shows   "fold_bind_random_permutation f g x A =
              do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (foldr f xs x)}"
   using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf
                             fold_random_permutation_foldr bind_return_pmf map_pmf_def)
 
 lemma fold_bind_random_permutation_fold:
   assumes "finite A"
   shows   "fold_bind_random_permutation f g x A =
              do {xs \<leftarrow> pmf_of_set (permutations_of_set A); g (fold f xs x)}"
   using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf
                             fold_random_permutation_fold bind_return_pmf map_pmf_def)
 
 text \<open>
   The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a 
   predicate and drawing a random permutation of that set.
 \<close>
 lemma partition_random_permutations:
   assumes "finite A"
   shows   "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) = 
              pair_pmf (pmf_of_set (permutations_of_set {x\<in>A. P x}))
                       (pmf_of_set (permutations_of_set {x\<in>A. \<not>P x}))" (is "?lhs = ?rhs")
 proof (rule pmf_eqI, clarify, goal_cases)
   case (1 xs ys)
   show ?case
   proof (cases "xs \<in> permutations_of_set {x\<in>A. P x} \<and> ys \<in> permutations_of_set {x\<in>A. \<not>P x}")
     case True
     let ?n1 = "card {x\<in>A. P x}" and ?n2 = "card {x\<in>A. \<not>P x}"
     have card_eq: "card A = ?n1 + ?n2"
     proof -
       have "?n1 + ?n2 = card ({x\<in>A. P x} \<union> {x\<in>A. \<not>P x})"
         using assms by (intro card_Un_disjoint [symmetric]) auto
       also have "{x\<in>A. P x} \<union> {x\<in>A. \<not>P x} = A" by blast
       finally show ?thesis ..
     qed
 
     from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2"
       by (auto intro!: length_finite_permutations_of_set)
     have "pmf ?lhs (xs, ys) = 
             real (card (permutations_of_set A \<inter> partition P -` {(xs, ys)})) / fact (card A)"
       using assms by (auto simp: pmf_map measure_pmf_of_set)
     also have "partition P -` {(xs, ys)} = shuffles xs ys" 
       using True by (intro inv_image_partition) (auto simp: permutations_of_set_def)
     also have "permutations_of_set A \<inter> shuffles xs ys = shuffles xs ys"
       using True distinct_disjoint_shuffles[of xs ys] 
       by (auto simp: permutations_of_set_def dest: set_shuffles)
     also have "card (shuffles xs ys) = length xs + length ys choose length xs"
       using True by (intro card_disjoint_shuffles) (auto simp: permutations_of_set_def)
     also have "length xs + length ys = card A" by (simp add: card_eq)
     also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))"
       by (subst binomial_fact) (auto intro!: card_mono assms)
     also have "\<dots> / fact (card A) = 1 / (fact ?n1 * fact ?n2)"
       by (simp add: field_split_simps card_eq)
     also have "\<dots> = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair)
     finally show ?thesis .
   next
     case False
     hence *: "xs \<notin> permutations_of_set {x\<in>A. P x} \<or> ys \<notin> permutations_of_set {x\<in>A. \<not>P x}" by blast
     hence eq: "permutations_of_set A \<inter> (partition P -` {(xs, ys)}) = {}"
       by (auto simp: o_def permutations_of_set_def)
     from * show ?thesis
       by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set)
   qed
 qed
 
 end