theory week09A_demo 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 }" (*TODO*) sorry 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 }" (* TODO *) sorry 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) }" (* TODO *) sorry 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 }" (* TODO *) sorry 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) }" (* TODO *) sorry -- "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 }" (* TODO *) sorry 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 }" (* TODO *) sorry (* 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)}" (* todo*) sorry end