src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
changeset 37771 1bec64044b5e
parent 37719 271ecd4fb9f9
child 37792 ba0bc31b90d7
child 37796 08bd610b2583
     1.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 11:39:27 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Mon Jul 12 16:05:08 2010 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* An imperative in-place reversal on arrays *}
     1.5  
     1.6  theory Imperative_Reverse
     1.7 -imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray
     1.8 +imports Imperative_HOL Subarray
     1.9  begin
    1.10  
    1.11  hide_const (open) swap rev
    1.12 @@ -36,7 +36,7 @@
    1.13        else if k = j then get_array a h ! i
    1.14        else get_array a h ! k)"
    1.15  using assms unfolding swap.simps
    1.16 -by (elim crel_elim_all)
    1.17 +by (elim crel_elims)
    1.18   (auto simp: length_def)
    1.19  
    1.20  lemma rev_pointwise: assumes "crel (rev a i j) h h' r"
    1.21 @@ -52,7 +52,7 @@
    1.22      obtain h' where
    1.23        swp: "crel (swap a i j) h h' ()"
    1.24        and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    1.25 -      by (auto elim: crel_elim_all)
    1.26 +      by (auto elim: crel_elims)
    1.27      from rev 1 True
    1.28      have eq: "?P a (i + 1) (j - 1) h' h''" by auto
    1.29  
    1.30 @@ -63,7 +63,7 @@
    1.31      case False
    1.32      with 1[unfolded rev.simps[of a i j]]
    1.33      show ?thesis
    1.34 -      by (cases "k = j") (auto elim: crel_elim_all)
    1.35 +      by (cases "k = j") (auto elim: crel_elims)
    1.36    qed
    1.37  qed
    1.38  
    1.39 @@ -80,15 +80,15 @@
    1.40      obtain h' where
    1.41        swp: "crel (swap a i j) h h' ()"
    1.42        and rev: "crel (rev a (i + 1) (j - 1)) h' h'' ()"
    1.43 -      by (auto elim: crel_elim_all)
    1.44 +      by (auto elim: crel_elims)
    1.45      from swp rev 1 True show ?thesis
    1.46        unfolding swap.simps
    1.47 -      by (elim crel_elim_all) fastsimp
    1.48 +      by (elim crel_elims) fastsimp
    1.49    next
    1.50      case False
    1.51      with 1[unfolded rev.simps[of a i j]]
    1.52      show ?thesis
    1.53 -      by (auto elim: crel_elim_all)
    1.54 +      by (auto elim: crel_elims)
    1.55    qed
    1.56  qed
    1.57  
    1.58 @@ -112,7 +112,7 @@
    1.59    shows "get_array a h' = List.rev (get_array a h)"
    1.60    using rev2_rev'[OF assms] rev_length[OF assms] assms
    1.61      by (cases "Array.length a h = 0", auto simp add: Array.length_def
    1.62 -      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elim_all)
    1.63 +      subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
    1.64    (drule sym[of "List.length (get_array a h)"], simp)
    1.65  
    1.66  end