theory week09A_sol imports "~~/src/HOL/Hoare/HeapSyntax" begin lemma "VARS (A::int) B { a\0 \ b\0 } A:=0; B:=0; WHILE A \ a INV { B = A * b } DO B := B + b; A := A + 1 OD {B = a * b }" apply vcg apply simp (*sledgehammer*) apply (smt semiring_normalization_rules(3)) apply simp done lemma "VARS (A::int) B { a\0 \ b\0 } A:=0; B:=0; WHILE A < a INV { B = A * b \ A\a} DO B := B + b; A := A + 1 OD {B = a * b }" apply vcg apply simp (*sledgehammer*) apply (smt semiring_normalization_rules(3)) apply simp done lemma "VARS (A::nat) (B::int) { b\0 } A:=a; B:=1; WHILE A \ 0 INV { B = (b^(a-A)) \A\a} DO B := B * b; A := A - 1 OD {B = (b^a) }" apply vcg apply simp (*sledgehammer*) using Suc_diff_le apply auto[1] (*sledgehammer*) using Suc_diff_le by auto (* Note: if you forget A\a then you get an unsolvable goal; you can try nitpick which will find a counter example. The added condition is required to use the theorem thm Suc_diff_le *) lemma "VARS (X::int list) (Y::int list) { True } X:=x; Y:=[]; WHILE X \ [] INV { (rev X)@Y = rev x } DO Y := (hd X # Y); X := tl X OD {Y = rev x }" apply vcg apply simp (*sledgehammer*) apply (metis append.left_neutral append_eq_append_conv2 list.collapse rev.simps(2) rev_append rev_rev_ident) apply clarsimp done lemma "VARS (A::int) (B::nat) (C::int) { a\0 } A:=a; B:=b; C:=1; WHILE B \ 0 INV { a^b = C*A^B} DO WHILE ((B mod 2) = 0) INV {a^b = C*A^B} DO A:=A*A; B:=B div 2 OD; C := C * A; B := B - 1 OD {C = (a^b) }" apply vcg apply simp_all (*sledgehammer*) apply (metis (no_types, lifting) mod_eq_0_iff nonzero_mult_div_cancel_left power2_eq_square power_mult zero_not_eq_two) (*sledgehammer*) by (metis One_nat_def mod_greater_zero_iff_not_dvd odd_pos power_minus_mult semiring_normalization_rules(7) zero_less_Suc) -- "Pointers" thm List_def Path.simps (* "List nxt p Ps" represents a linked list, starting at pointer p, with 'nxt' being the function to find the next pointer, and Ps the list of all the content of the linked list *) (* define a function that takes X, p and nxt function, assuming that X in the set of the linked list, then it returns the pointer to that element *) (* think about its loop invariant *) lemma "VARS nxt p { List nxt p Ps \ X \ set Ps } WHILE p \ Null \ p \ Ref X INV { \Ps. List nxt p Ps \ X \ set Ps } DO p := p^.nxt OD { p = Ref X }" apply vcg apply auto done lemma "VARS nxt p { List nxt p Ps \ X \ set Ps } WHILE p \ Null \ p \ Ref X INV { \Ps. Path nxt p Ps (Ref X) } DO p := p^.nxt OD { p = Ref X }" apply vcg (* try find_theorems "_\_" "_@_" *) (* sledghammer also works *) apply (simp add: in_set_conv_decomp) apply clarsimp apply (simp add: List_app) apply blast apply auto done (* define a function that "splices" 2 disjoint linked lists together *) (* think about its loop invariant *) lemma "VARS tl p q pp qq {List tl p Ps \ List tl q Qs \ set Ps \ set Qs = {} \ size Qs \ size Ps} pp := p; WHILE q \ Null INV {\as bs qs. distinct as \ Path tl p as pp \ List tl pp bs \ List tl q qs \ set bs \ set qs = {} \ set as \ (set bs \ set qs) = {} \ size qs \ size bs \ splice Ps Qs = as @ splice bs qs} DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD {List tl p (splice Ps Qs)}" apply (vcg; simp) apply(rule_tac x = "[]" in exI) apply fastforce apply clarsimp apply(rename_tac y bs qqs) apply(case_tac bs; clarsimp) apply(rename_tac x bbs) apply(rule_tac x = "as @ [x,y]" in exI) apply simp apply(rule_tac x = "bbs" in exI) apply simp apply(rule_tac x = "qqs" in exI) apply simp apply (fastforce simp: List_app) done end