author  haftmann 
Wed, 14 Jul 2010 16:13:14 +0200  
changeset 37826  4c0a5e35931a 
parent 37806  a7679be14442 
child 37845  b70d7a347964 
permissions  rwrr 
36098
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

1 
(* Title: HOL/Imperative_HOL/ex/Imperative_Reverse.thy 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

2 
Author: Lukas Bulwahn, TU Muenchen 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

3 
*) 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

4 

53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

5 
header {* An imperative inplace reversal on arrays *} 
53992c639da5
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
bulwahn
parents:
34051
diff
changeset

6 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

7 
theory Imperative_Reverse 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

8 
imports Imperative_HOL Subarray 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

9 
begin 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

10 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

11 
fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where 
37792  12 
"swap a i j = do { 
37798
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

13 
x \<leftarrow> Array.nth a i; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

14 
y \<leftarrow> Array.nth a j; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

15 
Array.upd i y a; 
0b0570445a2a
proper merge of operation changes and generic dosyntax
haftmann
parents:
37797
diff
changeset

16 
Array.upd j x a; 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

17 
return () 
37792  18 
}" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

19 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

20 
fun rev :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where 
37792  21 
"rev a i j = (if (i < j) then do { 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

22 
swap a i j; 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

23 
rev a (i + 1) (j  1) 
37792  24 
} 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

25 
else return ())" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

26 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

27 
declare swap.simps [simp del] rev.simps [simp del] 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

28 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

29 
lemma swap_pointwise: assumes "crel (swap a i j) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

30 
shows "Array.get h' a ! k = (if k = i then Array.get h a ! j 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

31 
else if k = j then Array.get h a ! i 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

32 
else Array.get h a ! k)" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

33 
using assms unfolding swap.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

34 
by (elim crel_elims) 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset

35 
(auto simp: length_def) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

36 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

37 
lemma rev_pointwise: assumes "crel (rev a i j) h h' r" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

38 
shows "Array.get h' a ! k = (if k < i then Array.get h a ! k 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

39 
else if j < k then Array.get h a ! k 
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

40 
else Array.get h a ! (j  (k  i)))" (is "?P a i j h h'") 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

41 
using assms proof (induct a i j arbitrary: h h' rule: rev.induct) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

42 
case (1 a i j h h'') 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

43 
thus ?case 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

44 
proof (cases "i < j") 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

45 
case True 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

46 
with 1[unfolded rev.simps[of a i j]] 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

47 
obtain h' where 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

48 
swp: "crel (swap a i j) h h' ()" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

49 
and rev: "crel (rev a (i + 1) (j  1)) h' h'' ()" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

50 
by (auto elim: crel_elims) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

51 
from rev 1 True 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

52 
have eq: "?P a (i + 1) (j  1) h' h''" by auto 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

53 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

54 
have "k < i \<or> i = k \<or> (i < k \<and> k < j) \<or> j = k \<or> j < k" by arith 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

55 
with True show ?thesis 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

56 
by (elim disjE) (auto simp: eq swap_pointwise[OF swp]) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

57 
next 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

58 
case False 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

59 
with 1[unfolded rev.simps[of a i j]] 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

60 
show ?thesis 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

61 
by (cases "k = j") (auto elim: crel_elims) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

62 
qed 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

63 
qed 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

64 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

65 
lemma rev_length: 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

66 
assumes "crel (rev a i j) h h' r" 
37802  67 
shows "Array.length h a = Array.length h' a" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

68 
using assms 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

69 
proof (induct a i j arbitrary: h h' rule: rev.induct) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

70 
case (1 a i j h h'') 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

71 
thus ?case 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

72 
proof (cases "i < j") 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

73 
case True 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

74 
with 1[unfolded rev.simps[of a i j]] 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

75 
obtain h' where 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

76 
swp: "crel (swap a i j) h h' ()" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

77 
and rev: "crel (rev a (i + 1) (j  1)) h' h'' ()" 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

78 
by (auto elim: crel_elims) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

79 
from swp rev 1 True show ?thesis 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

80 
unfolding swap.simps 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

81 
by (elim crel_elims) fastsimp 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

82 
next 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

83 
case False 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

84 
with 1[unfolded rev.simps[of a i j]] 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

85 
show ?thesis 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

86 
by (auto elim: crel_elims) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

87 
qed 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

88 
qed 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

89 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

90 
lemma rev2_rev': assumes "crel (rev a i j) h h' u" 
37802  91 
assumes "j < Array.length h a" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

92 
shows "subarray i (j + 1) a h' = List.rev (subarray i (j + 1) a h)" 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

93 
proof  
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

94 
{ 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

95 
fix k 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

96 
assume "k < Suc j  i" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

97 
with rev_pointwise[OF assms(1)] have "Array.get h' a ! (i + k) = Array.get h a ! (j  k)" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

98 
by auto 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

99 
} 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

100 
with assms(2) rev_length[OF assms(1)] show ?thesis 
37719
271ecd4fb9f9
moved "open" operations from Heap.thy to Array.thy and Ref.thy
haftmann
parents:
36176
diff
changeset

101 
unfolding subarray_def Array.length_def 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

102 
by (auto simp add: length_sublist' rev_nth min_def nth_sublist' intro!: nth_equalityI) 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

103 
qed 
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

104 

1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

105 
lemma rev2_rev: 
37802  106 
assumes "crel (rev a 0 (Array.length h a  1)) h h' u" 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

107 
shows "Array.get h' a = List.rev (Array.get h a)" 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

108 
using rev2_rev'[OF assms] rev_length[OF assms] assms 
37802  109 
by (cases "Array.length h a = 0", auto simp add: Array.length_def 
37771
1bec64044b5e
spelt out relational framework in a consistent way
haftmann
parents:
37719
diff
changeset

110 
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims) 
37806
a7679be14442
qualified names for (really) all array operations
haftmann
parents:
37805
diff
changeset

111 
(drule sym[of "List.length (Array.get h a)"], simp) 
34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

112 

37826  113 
export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? 
114 

34051
1a82e2e29d67
added Imperative_HOL examples; added tailrecursive combinator for monadic heap functions; adopted code generation of references; added lemmas
bulwahn
parents:
diff
changeset

115 
end 