theory Solution06 imports "../../SimplC/SimplC" begin text {* more *} verify_statement acopy vars: {* int a[]; int b[]; int i; int n; *} pre: "n \ alength a \ n \ alength b \ elems a 0 n = A \ 0 \ n" post: "elems b 0 n = A" {* i = 0; /*@ 0 \ i \ i \ n \ elems b 0 i = elems a 0 i \ n \ alength a \ n \ alength b \ elems a 0 n = A */ while (i < n) { b[i] = a[i]; i = i + 1; } *} apply vcg apply auto apply (simp add: elems_split_update) apply (simp add: elems_split_last) done verify_statement arev vars: {* int a[]; int i; int j; int t; int n; *} pre: "n \ alength a \ n \ alength b \ elems a 0 n = A \ 0 \ n" post: "elems a 0 n = rev A" {* i = 0; j = n; /*@ 0 \ i \ i \ j \ j \ n \ A = rev (elems a j n) @ elems a i j @ rev (elems a 0 i) \ n \ alength a */ while (i < j) { t = a[i]; a[i] = a[j-1]; a[j-1] = t; i = i + 1; if (i < j) j = j - 1; } *} (*** Apply vcg and simplify trivial things ***) apply vcg apply simp_all apply safe (*** Split at updates ***) apply (simp_all add: elems_split_update) (*** Solve first goal ***) apply (subst elems_split_first) apply assumption apply simp apply simp apply (subst elems_split_last) apply simp apply simp apply simp (*** Alternative to this block: apply (simp add: elems_split_first[symmetric] elems_split_last[symmetric]) ***) (*** Reading the assumptions, we see that "j = i + 1". We need to give Isabelle a hint in this direction ***) apply (case_tac "j = i + 1") apply simp apply simp apply (subst elems_split) apply simp apply assumption apply simp apply simp (*** Alternative to this block: apply (simp add: elems_split[symmetric]) ***) done end