src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 40671 5e46057ba8e0
parent 38058 e4640c2ceb43
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Nov 22 09:19:34 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Mon Nov 22 09:37:39 2010 +0100
     1.3 @@ -21,20 +21,20 @@
     1.4         return ()
     1.5       }"
     1.6  
     1.7 -lemma crel_swapI [crel_intros]:
     1.8 +lemma effect_swapI [effect_intros]:
     1.9    assumes "i < Array.length h a" "j < Array.length h a"
    1.10      "x = Array.get h a ! i" "y = Array.get h a ! j"
    1.11      "h' = Array.update a j x (Array.update a i y h)"
    1.12 -  shows "crel (swap a i j) h h' r"
    1.13 -  unfolding swap_def using assms by (auto intro!: crel_intros)
    1.14 +  shows "effect (swap a i j) h h' r"
    1.15 +  unfolding swap_def using assms by (auto intro!: effect_intros)
    1.16  
    1.17  lemma swap_permutes:
    1.18 -  assumes "crel (swap a i j) h h' rs"
    1.19 +  assumes "effect (swap a i j) h h' rs"
    1.20    shows "multiset_of (Array.get h' a) 
    1.21    = multiset_of (Array.get h a)"
    1.22    using assms
    1.23    unfolding swap_def
    1.24 -  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: crel_bindE crel_nthE crel_returnE crel_updE)
    1.25 +  by (auto simp add: Array.length_def multiset_of_swap dest: sym [of _ "h'"] elim!: effect_bindE effect_nthE effect_returnE effect_updE)
    1.26  
    1.27  function part1 :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    1.28  where
    1.29 @@ -54,7 +54,7 @@
    1.30  declare part1.simps[simp del]
    1.31  
    1.32  lemma part_permutes:
    1.33 -  assumes "crel (part1 a l r p) h h' rs"
    1.34 +  assumes "effect (part1 a l r p) h h' rs"
    1.35    shows "multiset_of (Array.get h' a) 
    1.36    = multiset_of (Array.get h a)"
    1.37    using assms
    1.38 @@ -62,23 +62,23 @@
    1.39    case (1 a l r p h h' rs)
    1.40    thus ?case
    1.41      unfolding part1.simps [of a l r p]
    1.42 -    by (elim crel_bindE crel_ifE crel_returnE crel_nthE) (auto simp add: swap_permutes)
    1.43 +    by (elim effect_bindE effect_ifE effect_returnE effect_nthE) (auto simp add: swap_permutes)
    1.44  qed
    1.45  
    1.46  lemma part_returns_index_in_bounds:
    1.47 -  assumes "crel (part1 a l r p) h h' rs"
    1.48 +  assumes "effect (part1 a l r p) h h' rs"
    1.49    assumes "l \<le> r"
    1.50    shows "l \<le> rs \<and> rs \<le> r"
    1.51  using assms
    1.52  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
    1.53    case (1 a l r p h h' rs)
    1.54 -  note cr = `crel (part1 a l r p) h h' rs`
    1.55 +  note cr = `effect (part1 a l r p) h h' rs`
    1.56    show ?case
    1.57    proof (cases "r \<le> l")
    1.58      case True (* Terminating case *)
    1.59      with cr `l \<le> r` show ?thesis
    1.60        unfolding part1.simps[of a l r p]
    1.61 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
    1.62 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
    1.63    next
    1.64      case False (* recursive case *)
    1.65      note rec_condition = this
    1.66 @@ -87,19 +87,19 @@
    1.67      proof (cases "?v \<le> p")
    1.68        case True
    1.69        with cr False
    1.70 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
    1.71 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
    1.72          unfolding part1.simps[of a l r p]
    1.73 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    1.74 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    1.75        from rec_condition have "l + 1 \<le> r" by arith
    1.76        from 1(1)[OF rec_condition True rec1 `l + 1 \<le> r`]
    1.77        show ?thesis by simp
    1.78      next
    1.79        case False
    1.80        with rec_condition cr
    1.81 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
    1.82 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
    1.83 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
    1.84 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
    1.85          unfolding part1.simps[of a l r p]
    1.86 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
    1.87 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
    1.88        from rec_condition have "l \<le> r - 1" by arith
    1.89        from 1(2) [OF rec_condition False rec2 `l \<le> r - 1`] show ?thesis by fastsimp
    1.90      qed
    1.91 @@ -107,41 +107,41 @@
    1.92  qed
    1.93  
    1.94  lemma part_length_remains:
    1.95 -  assumes "crel (part1 a l r p) h h' rs"
    1.96 +  assumes "effect (part1 a l r p) h h' rs"
    1.97    shows "Array.length h a = Array.length h' a"
    1.98  using assms
    1.99  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   1.100    case (1 a l r p h h' rs)
   1.101 -  note cr = `crel (part1 a l r p) h h' rs`
   1.102 +  note cr = `effect (part1 a l r p) h h' rs`
   1.103    
   1.104    show ?case
   1.105    proof (cases "r \<le> l")
   1.106      case True (* Terminating case *)
   1.107      with cr show ?thesis
   1.108        unfolding part1.simps[of a l r p]
   1.109 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   1.110 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   1.111    next
   1.112      case False (* recursive case *)
   1.113      with cr 1 show ?thesis
   1.114        unfolding part1.simps [of a l r p] swap_def
   1.115 -      by (auto elim!: crel_bindE crel_ifE crel_nthE crel_returnE crel_updE) fastsimp
   1.116 +      by (auto elim!: effect_bindE effect_ifE effect_nthE effect_returnE effect_updE) fastsimp
   1.117    qed
   1.118  qed
   1.119  
   1.120  lemma part_outer_remains:
   1.121 -  assumes "crel (part1 a l r p) h h' rs"
   1.122 +  assumes "effect (part1 a l r p) h h' rs"
   1.123    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   1.124    using assms
   1.125  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   1.126    case (1 a l r p h h' rs)
   1.127 -  note cr = `crel (part1 a l r p) h h' rs`
   1.128 +  note cr = `effect (part1 a l r p) h h' rs`
   1.129    
   1.130    show ?case
   1.131    proof (cases "r \<le> l")
   1.132      case True (* Terminating case *)
   1.133      with cr show ?thesis
   1.134        unfolding part1.simps[of a l r p]
   1.135 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   1.136 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   1.137    next
   1.138      case False (* recursive case *)
   1.139      note rec_condition = this
   1.140 @@ -150,22 +150,22 @@
   1.141      proof (cases "?v \<le> p")
   1.142        case True
   1.143        with cr False
   1.144 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   1.145 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
   1.146          unfolding part1.simps[of a l r p]
   1.147 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   1.148 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   1.149        from 1(1)[OF rec_condition True rec1]
   1.150        show ?thesis by fastsimp
   1.151      next
   1.152        case False
   1.153        with rec_condition cr
   1.154 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   1.155 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   1.156 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
   1.157 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
   1.158          unfolding part1.simps[of a l r p]
   1.159 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   1.160 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   1.161        from swp rec_condition have
   1.162          "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h a ! i = Array.get h1 a ! i"
   1.163          unfolding swap_def
   1.164 -        by (elim crel_bindE crel_nthE crel_updE crel_returnE) auto
   1.165 +        by (elim effect_bindE effect_nthE effect_updE effect_returnE) auto
   1.166        with 1(2) [OF rec_condition False rec2] show ?thesis by fastsimp
   1.167      qed
   1.168    qed
   1.169 @@ -173,20 +173,20 @@
   1.170  
   1.171  
   1.172  lemma part_partitions:
   1.173 -  assumes "crel (part1 a l r p) h h' rs"
   1.174 +  assumes "effect (part1 a l r p) h h' rs"
   1.175    shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> p)
   1.176    \<and> (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! i \<ge> p)"
   1.177    using assms
   1.178  proof (induct a l r p arbitrary: h h' rs rule:part1.induct)
   1.179    case (1 a l r p h h' rs)
   1.180 -  note cr = `crel (part1 a l r p) h h' rs`
   1.181 +  note cr = `effect (part1 a l r p) h h' rs`
   1.182    
   1.183    show ?case
   1.184    proof (cases "r \<le> l")
   1.185      case True (* Terminating case *)
   1.186      with cr have "rs = r"
   1.187        unfolding part1.simps[of a l r p]
   1.188 -      by (elim crel_bindE crel_ifE crel_returnE crel_nthE) auto
   1.189 +      by (elim effect_bindE effect_ifE effect_returnE effect_nthE) auto
   1.190      with True
   1.191      show ?thesis by auto
   1.192    next
   1.193 @@ -197,9 +197,9 @@
   1.194      proof (cases "?v \<le> p")
   1.195        case True
   1.196        with lr cr
   1.197 -      have rec1: "crel (part1 a (l + 1) r p) h h' rs"
   1.198 +      have rec1: "effect (part1 a (l + 1) r p) h h' rs"
   1.199          unfolding part1.simps[of a l r p]
   1.200 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   1.201 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   1.202        from True part_outer_remains[OF rec1] have a_l: "Array.get h' a ! l \<le> p"
   1.203          by fastsimp
   1.204        have "\<forall>i. (l \<le> i = (l = i \<or> Suc l \<le> i))" by arith
   1.205 @@ -208,13 +208,13 @@
   1.206      next
   1.207        case False
   1.208        with lr cr
   1.209 -      obtain h1 where swp: "crel (swap a l r) h h1 ()"
   1.210 -        and rec2: "crel (part1 a l (r - 1) p) h1 h' rs"
   1.211 +      obtain h1 where swp: "effect (swap a l r) h h1 ()"
   1.212 +        and rec2: "effect (part1 a l (r - 1) p) h1 h' rs"
   1.213          unfolding part1.simps[of a l r p]
   1.214 -        by (elim crel_bindE crel_nthE crel_ifE crel_returnE) auto
   1.215 +        by (elim effect_bindE effect_nthE effect_ifE effect_returnE) auto
   1.216        from swp False have "Array.get h1 a ! r \<ge> p"
   1.217          unfolding swap_def
   1.218 -        by (auto simp add: Array.length_def elim!: crel_bindE crel_nthE crel_updE crel_returnE)
   1.219 +        by (auto simp add: Array.length_def elim!: effect_bindE effect_nthE effect_updE effect_returnE)
   1.220        with part_outer_remains [OF rec2] lr have a_r: "Array.get h' a ! r \<ge> p"
   1.221          by fastsimp
   1.222        have "\<forall>i. (i \<le> r = (i = r \<or> i \<le> r - 1))" by arith
   1.223 @@ -239,70 +239,70 @@
   1.224  declare partition.simps[simp del]
   1.225  
   1.226  lemma partition_permutes:
   1.227 -  assumes "crel (partition a l r) h h' rs"
   1.228 +  assumes "effect (partition a l r) h h' rs"
   1.229    shows "multiset_of (Array.get h' a) 
   1.230    = multiset_of (Array.get h a)"
   1.231  proof -
   1.232      from assms part_permutes swap_permutes show ?thesis
   1.233        unfolding partition.simps
   1.234 -      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   1.235 +      by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
   1.236  qed
   1.237  
   1.238  lemma partition_length_remains:
   1.239 -  assumes "crel (partition a l r) h h' rs"
   1.240 +  assumes "effect (partition a l r) h h' rs"
   1.241    shows "Array.length h a = Array.length h' a"
   1.242  proof -
   1.243    from assms part_length_remains show ?thesis
   1.244      unfolding partition.simps swap_def
   1.245 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) auto
   1.246 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) auto
   1.247  qed
   1.248  
   1.249  lemma partition_outer_remains:
   1.250 -  assumes "crel (partition a l r) h h' rs"
   1.251 +  assumes "effect (partition a l r) h h' rs"
   1.252    assumes "l < r"
   1.253    shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   1.254  proof -
   1.255    from assms part_outer_remains part_returns_index_in_bounds show ?thesis
   1.256      unfolding partition.simps swap_def
   1.257 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) fastsimp
   1.258 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) fastsimp
   1.259  qed
   1.260  
   1.261  lemma partition_returns_index_in_bounds:
   1.262 -  assumes crel: "crel (partition a l r) h h' rs"
   1.263 +  assumes effect: "effect (partition a l r) h h' rs"
   1.264    assumes "l < r"
   1.265    shows "l \<le> rs \<and> rs \<le> r"
   1.266  proof -
   1.267 -  from crel obtain middle h'' p where part: "crel (part1 a l (r - 1) p) h h'' middle"
   1.268 +  from effect obtain middle h'' p where part: "effect (part1 a l (r - 1) p) h h'' middle"
   1.269      and rs_equals: "rs = (if Array.get h'' a ! middle \<le> Array.get h a ! r then middle + 1
   1.270           else middle)"
   1.271      unfolding partition.simps
   1.272 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp 
   1.273 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp 
   1.274    from `l < r` have "l \<le> r - 1" by arith
   1.275    from part_returns_index_in_bounds[OF part this] rs_equals `l < r` show ?thesis by auto
   1.276  qed
   1.277  
   1.278  lemma partition_partitions:
   1.279 -  assumes crel: "crel (partition a l r) h h' rs"
   1.280 +  assumes effect: "effect (partition a l r) h h' rs"
   1.281    assumes "l < r"
   1.282    shows "(\<forall>i. l \<le> i \<and> i < rs \<longrightarrow> Array.get h' (a::nat array) ! i \<le> Array.get h' a ! rs) \<and>
   1.283    (\<forall>i. rs < i \<and> i \<le> r \<longrightarrow> Array.get h' a ! rs \<le> Array.get h' a ! i)"
   1.284  proof -
   1.285    let ?pivot = "Array.get h a ! r" 
   1.286 -  from crel obtain middle h1 where part: "crel (part1 a l (r - 1) ?pivot) h h1 middle"
   1.287 -    and swap: "crel (swap a rs r) h1 h' ()"
   1.288 +  from effect obtain middle h1 where part: "effect (part1 a l (r - 1) ?pivot) h h1 middle"
   1.289 +    and swap: "effect (swap a rs r) h1 h' ()"
   1.290      and rs_equals: "rs = (if Array.get h1 a ! middle \<le> ?pivot then middle + 1
   1.291           else middle)"
   1.292      unfolding partition.simps
   1.293 -    by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
   1.294 +    by (elim effect_bindE effect_returnE effect_nthE effect_ifE effect_updE) simp
   1.295    from swap have h'_def: "h' = Array.update a r (Array.get h1 a ! rs)
   1.296      (Array.update a rs (Array.get h1 a ! r) h1)"
   1.297      unfolding swap_def
   1.298 -    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   1.299 +    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   1.300    from swap have in_bounds: "r < Array.length h1 a \<and> rs < Array.length h1 a"
   1.301      unfolding swap_def
   1.302 -    by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
   1.303 +    by (elim effect_bindE effect_returnE effect_nthE effect_updE) simp
   1.304    from swap have swap_length_remains: "Array.length h1 a = Array.length h' a"
   1.305 -    unfolding swap_def by (elim crel_bindE crel_returnE crel_nthE crel_updE) auto
   1.306 +    unfolding swap_def by (elim effect_bindE effect_returnE effect_nthE effect_updE) auto
   1.307    from `l < r` have "l \<le> r - 1" by simp
   1.308    note middle_in_bounds = part_returns_index_in_bounds[OF part this]
   1.309    from part_outer_remains[OF part] `l < r`
   1.310 @@ -311,7 +311,7 @@
   1.311    with swap
   1.312    have right_remains: "Array.get h a ! r = Array.get h' a ! rs"
   1.313      unfolding swap_def
   1.314 -    by (auto simp add: Array.length_def elim!: crel_bindE crel_returnE crel_nthE crel_updE) (cases "r = rs", auto)
   1.315 +    by (auto simp add: Array.length_def elim!: effect_bindE effect_returnE effect_nthE effect_updE) (cases "r = rs", auto)
   1.316    from part_partitions [OF part]
   1.317    show ?thesis
   1.318    proof (cases "Array.get h1 a ! middle \<le> ?pivot")
   1.319 @@ -419,7 +419,7 @@
   1.320  
   1.321  
   1.322  lemma quicksort_permutes:
   1.323 -  assumes "crel (quicksort a l r) h h' rs"
   1.324 +  assumes "effect (quicksort a l r) h h' rs"
   1.325    shows "multiset_of (Array.get h' a) 
   1.326    = multiset_of (Array.get h a)"
   1.327    using assms
   1.328 @@ -427,41 +427,41 @@
   1.329    case (1 a l r h h' rs)
   1.330    with partition_permutes show ?case
   1.331      unfolding quicksort.simps [of a l r]
   1.332 -    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   1.333 +    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   1.334  qed
   1.335  
   1.336  lemma length_remains:
   1.337 -  assumes "crel (quicksort a l r) h h' rs"
   1.338 +  assumes "effect (quicksort a l r) h h' rs"
   1.339    shows "Array.length h a = Array.length h' a"
   1.340  using assms
   1.341  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   1.342    case (1 a l r h h' rs)
   1.343    with partition_length_remains show ?case
   1.344      unfolding quicksort.simps [of a l r]
   1.345 -    by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   1.346 +    by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   1.347  qed
   1.348  
   1.349  lemma quicksort_outer_remains:
   1.350 -  assumes "crel (quicksort a l r) h h' rs"
   1.351 +  assumes "effect (quicksort a l r) h h' rs"
   1.352     shows "\<forall>i. i < l \<or> r < i \<longrightarrow> Array.get h (a::nat array) ! i = Array.get h' a ! i"
   1.353    using assms
   1.354  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   1.355    case (1 a l r h h' rs)
   1.356 -  note cr = `crel (quicksort a l r) h h' rs`
   1.357 +  note cr = `effect (quicksort a l r) h h' rs`
   1.358    thus ?case
   1.359    proof (cases "r > l")
   1.360      case False
   1.361      with cr have "h' = h"
   1.362        unfolding quicksort.simps [of a l r]
   1.363 -      by (elim crel_ifE crel_returnE) auto
   1.364 +      by (elim effect_ifE effect_returnE) auto
   1.365      thus ?thesis by simp
   1.366    next
   1.367    case True
   1.368     { 
   1.369        fix h1 h2 p ret1 ret2 i
   1.370 -      assume part: "crel (partition a l r) h h1 p"
   1.371 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ret1"
   1.372 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ret2"
   1.373 +      assume part: "effect (partition a l r) h h1 p"
   1.374 +      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ret1"
   1.375 +      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ret2"
   1.376        assume pivot: "l \<le> p \<and> p \<le> r"
   1.377        assume i_outer: "i < l \<or> r < i"
   1.378        from  partition_outer_remains [OF part True] i_outer
   1.379 @@ -476,25 +476,25 @@
   1.380      }
   1.381      with cr show ?thesis
   1.382        unfolding quicksort.simps [of a l r]
   1.383 -      by (elim crel_ifE crel_bindE crel_assertE crel_returnE) auto
   1.384 +      by (elim effect_ifE effect_bindE effect_assertE effect_returnE) auto
   1.385    qed
   1.386  qed
   1.387  
   1.388  lemma quicksort_is_skip:
   1.389 -  assumes "crel (quicksort a l r) h h' rs"
   1.390 +  assumes "effect (quicksort a l r) h h' rs"
   1.391    shows "r \<le> l \<longrightarrow> h = h'"
   1.392    using assms
   1.393    unfolding quicksort.simps [of a l r]
   1.394 -  by (elim crel_ifE crel_returnE) auto
   1.395 +  by (elim effect_ifE effect_returnE) auto
   1.396   
   1.397  lemma quicksort_sorts:
   1.398 -  assumes "crel (quicksort a l r) h h' rs"
   1.399 +  assumes "effect (quicksort a l r) h h' rs"
   1.400    assumes l_r_length: "l < Array.length h a" "r < Array.length h a" 
   1.401    shows "sorted (subarray l (r + 1) a h')"
   1.402    using assms
   1.403  proof (induct a l r arbitrary: h h' rs rule: quicksort.induct)
   1.404    case (1 a l r h h' rs)
   1.405 -  note cr = `crel (quicksort a l r) h h' rs`
   1.406 +  note cr = `effect (quicksort a l r) h h' rs`
   1.407    thus ?case
   1.408    proof (cases "r > l")
   1.409      case False
   1.410 @@ -505,9 +505,9 @@
   1.411      case True
   1.412      { 
   1.413        fix h1 h2 p
   1.414 -      assume part: "crel (partition a l r) h h1 p"
   1.415 -      assume qs1: "crel (quicksort a l (p - 1)) h1 h2 ()"
   1.416 -      assume qs2: "crel (quicksort a (p + 1) r) h2 h' ()"
   1.417 +      assume part: "effect (partition a l r) h h1 p"
   1.418 +      assume qs1: "effect (quicksort a l (p - 1)) h1 h2 ()"
   1.419 +      assume qs2: "effect (quicksort a (p + 1) r) h2 h' ()"
   1.420        from partition_returns_index_in_bounds [OF part True]
   1.421        have pivot: "l\<le> p \<and> p \<le> r" .
   1.422       note length_remains = length_remains[OF qs2] length_remains[OF qs1] partition_length_remains[OF part]
   1.423 @@ -557,25 +557,25 @@
   1.424      }
   1.425      with True cr show ?thesis
   1.426        unfolding quicksort.simps [of a l r]
   1.427 -      by (elim crel_ifE crel_returnE crel_bindE crel_assertE) auto
   1.428 +      by (elim effect_ifE effect_returnE effect_bindE effect_assertE) auto
   1.429    qed
   1.430  qed
   1.431  
   1.432  
   1.433  lemma quicksort_is_sort:
   1.434 -  assumes crel: "crel (quicksort a 0 (Array.length h a - 1)) h h' rs"
   1.435 +  assumes effect: "effect (quicksort a 0 (Array.length h a - 1)) h h' rs"
   1.436    shows "Array.get h' a = sort (Array.get h a)"
   1.437  proof (cases "Array.get h a = []")
   1.438    case True
   1.439 -  with quicksort_is_skip[OF crel] show ?thesis
   1.440 +  with quicksort_is_skip[OF effect] show ?thesis
   1.441    unfolding Array.length_def by simp
   1.442  next
   1.443    case False
   1.444 -  from quicksort_sorts [OF crel] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
   1.445 +  from quicksort_sorts [OF effect] False have "sorted (sublist' 0 (List.length (Array.get h a)) (Array.get h' a))"
   1.446      unfolding Array.length_def subarray_def by auto
   1.447 -  with length_remains[OF crel] have "sorted (Array.get h' a)"
   1.448 +  with length_remains[OF effect] have "sorted (Array.get h' a)"
   1.449      unfolding Array.length_def by simp
   1.450 -  with quicksort_permutes [OF crel] properties_for_sort show ?thesis by fastsimp
   1.451 +  with quicksort_permutes [OF effect] properties_for_sort show ?thesis by fastsimp
   1.452  qed
   1.453  
   1.454  subsection {* No Errors in quicksort *}
   1.455 @@ -590,26 +590,26 @@
   1.456    case (1 a l r p)
   1.457    thus ?case unfolding part1.simps [of a l r]
   1.458    apply (auto intro!: success_intros del: success_ifI simp add: not_le)
   1.459 -  apply (auto intro!: crel_intros crel_swapI)
   1.460 +  apply (auto intro!: effect_intros effect_swapI)
   1.461    done
   1.462  qed
   1.463  
   1.464  lemma success_bindI' [success_intros]: (*FIXME move*)
   1.465    assumes "success f h"
   1.466 -  assumes "\<And>h' r. crel f h h' r \<Longrightarrow> success (g r) h'"
   1.467 +  assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
   1.468    shows "success (f \<guillemotright>= g) h"
   1.469 -using assms(1) proof (rule success_crelE)
   1.470 +using assms(1) proof (rule success_effectE)
   1.471    fix h' r
   1.472 -  assume "crel f h h' r"
   1.473 +  assume "effect f h h' r"
   1.474    moreover with assms(2) have "success (g r) h'" .
   1.475 -  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_crelI)
   1.476 +  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
   1.477  qed
   1.478  
   1.479  lemma success_partitionI:
   1.480    assumes "l < r" "l < Array.length h a" "r < Array.length h a"
   1.481    shows "success (partition a l r) h"
   1.482  using assms unfolding partition.simps swap_def
   1.483 -apply (auto intro!: success_bindI' success_ifI success_returnI success_nthI success_updI success_part1I elim!: crel_bindE crel_updE crel_nthE crel_returnE simp add:)
   1.484 +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:)
   1.485  apply (frule part_length_remains)
   1.486  apply (frule part_returns_index_in_bounds)
   1.487  apply auto
   1.488 @@ -633,7 +633,7 @@
   1.489      apply auto
   1.490      apply (frule partition_returns_index_in_bounds)
   1.491      apply auto
   1.492 -    apply (auto elim!: crel_assertE dest!: partition_length_remains length_remains)
   1.493 +    apply (auto elim!: effect_assertE dest!: partition_length_remains length_remains)
   1.494      apply (subgoal_tac "Suc r \<le> ri \<or> r = ri") 
   1.495      apply (erule disjE)
   1.496      apply auto