theory Solution09 imports "../../SimplC/SimplC" begin declare [[heap_model=seplogic]] section {* Exercise 1 *} text {* Complete specification and proof *} verify_statement swap vars: "int *p; int *q; int t;" pre: "(p\cty_int. X \ q\cty_int. Y) heap" post: "(p\cty_int. Y \ q\cty_int. X) heap" {* t = *p; *p = *q; *q = t; *} apply vcg apply prep_vc apply run apply heap done section {* Exercise 2 *} define_struct "struct node { int data; struct node *next; }" lemma node_NULL[simp]: "node NULL v = (\h. False)" by (simp add: node_def points_to_def fo_node_data_def seplogic_defs) lemma test_simps: "ty_ok cs_node" "ty_size cs_node = 2" by simp_all fun list :: "addr \ int list \ addr \ hassn" where "list p [] q = (emp \ (p = q))" | "list p (x # xs') q = (\ v. node p v \ list (node_next v) xs' q \ x = node_data v)" lemma list_append[simp]: "list p (xs @ ys) q = (\ r. list p xs r \ list r ys q)" by (induct xs arbitrary: p) (auto intro!: ext) lemma list_NULL_NULL[simp]: "list NULL xs NULL = (emp \ (xs = []))" by (cases xs) (auto intro!: ext simp add: heap_ex_def) lemma list_step[sep_unfold]: "p \ q \ list p xs q = (\ v xs'. node p v \ (list (node_next v) xs' q) \ (xs = node_data v # xs'))" apply (rule ext) apply (cases xs) apply auto done text {* Complete specification and proof *} verify_statement list_add_front vars: "struct node *p; struct node *q;" pre: "(list p XS NULL \ node q v) heap" post: "(list q (node_data v # XS) NULL) heap" "q->next = p;" apply vcg apply prep_vc apply run apply heap apply auto done section {* Exercise 3 *} definition sep_conj :: "hassn \ hassn \ hassn" (infix "\\" 58) where "P \\ Q \ \h. P h \ Q h" definition sep_all :: "('a \ hassn) \ hassn" (binder "\\" 10) where "\\x. P x \ \h. \x. P x h" text {* Proof that the following lemmas hold: *} lemma sep_conj_distr: "((P \\ Q) \ R) h \ ((P \ R) \\ (Q \ R)) h" unfolding sep_conj_def star_def by auto lemma sep_all_push_out: "((\\x. P x) \ Q) h \ (\\x. P x \ Q) h" unfolding sep_all_def star_def by auto text {* Moreover, prove that the converse of @{thm sep_conj_distr} and @{thm sep_all_push_out} does not hold. I.e., construct values for @{term P}, @{term Q}, and @{term R} such that from @{term "((P \ R) \\ (Q \ R)) h"} resp. @{term "(\\x. P x \ Q) h"} you you can prove @{term "\((P \\ Q) \ R) h"} resp. @{term "\((\\x. P x) \ Q) h"}. *} lemma points_to_disjD: "(p \ cty_int. x) h \ h \ h' \ \(p \ cty_int. x') h'" unfolding points_to_def heap_disjoint_def by (cases p) (auto simp: addr_ivl_def) lemma points_to_singleton[simp]: "p \ NULL \ (p \ cty_int. x) (Heap [p \ VInt x])" unfolding points_to_def by (cases p) (auto simp: addr_ivl_def cty_int_def heap_get_def) lemma neq_null[simp]: "n \ 0 \ Addr n \ NULL" "n \ 0 \ NULL \ Addr n" unfolding NULL_def by auto lemma "\(\P Q R h. ((P \ R) \\ (Q \ R)) h \ ((P \\ Q) \ R) h)" txt {* Push \ in the term *} apply simp txt {* Instantiate witnesses for counter-example*} apply (rule exI[where x="Addr 1 \ cty_int. 0"]) apply (rule exI[where x="Addr 2 \ cty_int. 0"]) apply (rule exI[where x="(\h. (Addr 1 \ cty_int. 0) h \ (Addr 2 \ cty_int. 0) h)"]) apply (rule exI[where x="Heap [Addr 1 \ VInt 0] \ Heap [Addr 2 \ VInt 0]"]) txt {* Simplify and split *} apply (simp add: sep_conj_def star_def) apply safe apply (rule exI[where x="Heap [Addr 1 \ VInt 0]"]) apply (rule exI[where x="Heap [Addr 2 \ VInt 0]"]) apply (simp add: heap_disjoint_def heap_union_def) apply (rule exI[where x="Heap [Addr 2 \ VInt 0]"]) apply (rule exI[where x="Heap [Addr 1 \ VInt 0]"]) apply (simp add: heap_disjoint_def heap_union_def fun_upd_twist) apply (auto dest: points_to_disjD) done lemma "\(\P Q h. (\\x :: bool. P x \ Q) h \ ((\\x. P x) \ Q) h)" txt {* Push \ in the term *} apply simp txt {* Instantiate witnesses for counter-example*} apply (rule exI[where x="\x. (if x then Addr 1 else Addr 2) \ cty_int. 0"]) apply (rule exI[where x="\ x. (if x then Addr 1 else Addr 2) \ cty_int. 0"]) apply (rule exI[where x="Heap [Addr 1 \ VInt 0, Addr 2 \ VInt 0]"]) txt {* Simplify and split *} apply (simp add: sep_all_def star_def heap_ex_def split del: split_if) apply safe apply (rule_tac x="Heap [(if x then Addr 1 else Addr 2) \ VInt 0]" in exI) apply (rule_tac x="Heap [(if \x then Addr 1 else Addr 2) \ VInt 0]" in exI) apply (fastforce simp: heap_union_def heap_disjoint_def) apply (auto dest: points_to_disjD) done end