1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Title: Adaptation of example from HOL/Hoare/Separation 8 Author: Gerwin Klein, 2012 9 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> 10 Rafal Kolanski <rafal.kolanski at nicta.com.au> 11*) 12 13chapter "Example from HOL/Hoare/Separation" 14 15theory Simple_Separation_Example 16imports 17 "HOL-Hoare.Hoare_Logic_Abort" 18 Sep_Heap_Instance 19 Sep_Tactics 20begin 21 22declare [[syntax_ambiguity_warning = false]] 23 24type_synonym heap = "(nat \<Rightarrow> nat option)" 25 26(* This syntax isn't ideal, but this is what is used in the original *) 27definition maps_to:: "nat \<Rightarrow> nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> _" [56,51] 56) 28 where "x \<mapsto> y \<equiv> \<lambda>h. h = [x \<mapsto> y]" 29 30(* If you don't mind syntax ambiguity: *) 31notation pred_ex (binder "\<exists>" 10) 32 33(* could be generated automatically *) 34definition maps_to_ex :: "nat \<Rightarrow> heap \<Rightarrow> bool" ("_ \<mapsto> -" [56] 56) 35 where "x \<mapsto> - \<equiv> \<exists>y. x \<mapsto> y" 36 37 38(* could be generated automatically *) 39lemma maps_to_maps_to_ex [elim!]: 40 "(p \<mapsto> v) s \<Longrightarrow> (p \<mapsto> -) s" 41 by (auto simp: maps_to_ex_def) 42 43(* The basic properties of maps_to: *) 44lemma maps_to_write: 45 "(p \<mapsto> - ** P) H \<Longrightarrow> (p \<mapsto> v ** P) (H (p \<mapsto> v))" 46 apply (clarsimp simp: sep_conj_def maps_to_def maps_to_ex_def split: option.splits) 47 apply (rule_tac x=y in exI) 48 apply (auto simp: sep_disj_fun_def map_convs map_add_def split: option.splits) 49 done 50 51lemma points_to: 52 "(p \<mapsto> v ** P) H \<Longrightarrow> the (H p) = v" 53 by (auto elim!: sep_conjE 54 simp: sep_disj_fun_def maps_to_def map_convs map_add_def 55 split: option.splits) 56 57 58(* This differs from the original and uses separation logic for the definition. *) 59primrec 60 list :: "nat \<Rightarrow> nat list \<Rightarrow> heap \<Rightarrow> bool" 61where 62 "list i [] = (\<langle>i=0\<rangle> and \<box>)" 63| "list i (x#xs) = (\<langle>i=x \<and> i\<noteq>0\<rangle> and (EXS j. i \<mapsto> j ** list j xs))" 64 65lemma list_empty [simp]: 66 shows "list 0 xs = (\<lambda>s. xs = [] \<and> \<box> s)" 67 by (cases xs) auto 68 69(* The examples from Hoare/Separation.thy *) 70lemma "VARS x y z w h 71 {(x \<mapsto> y ** z \<mapsto> w) h} 72 SKIP 73 {x \<noteq> z}" 74 apply vcg 75 apply(auto elim!: sep_conjE simp: maps_to_def sep_disj_fun_def domain_conv) 76done 77 78lemma "VARS H x y z w 79 {(P ** Q) H} 80 SKIP 81 {(Q ** P) H}" 82 apply vcg 83 apply(simp add: sep_conj_commute) 84done 85 86lemma "VARS H 87 {p\<noteq>0 \<and> (p \<mapsto> - ** list q qs) H} 88 H := H(p \<mapsto> q) 89 {list p (p#qs) H}" 90 apply vcg 91 apply (auto intro: maps_to_write) 92done 93 94text \<open>First a proof without using tactics\<close> 95lemma "VARS H p q r 96 {(list p Ps ** list q Qs) H} 97 WHILE p \<noteq> 0 98 INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs} 99 DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD 100 {list q (rev Ps @ Qs) H}" 101 apply vcg 102 apply fastforce 103 apply clarsimp 104 apply (case_tac ps, simp) 105 apply (rename_tac p ps') 106 apply (rule_tac x = "ps'" in exI) 107 apply (rule_tac x = "p # qs" in exI) 108 apply clarsimp 109 apply (clarsimp simp: sep_conj_exists sep_conj_ac) 110 apply (rule_tac x = "q" in exI) 111 thm points_to 112 apply (subst (asm) sep_conj_ac) 113 apply (subst (asm) sep_conj_commute) 114 apply (simp add: sep_conj_assoc) 115 apply (frule points_to) 116 apply simp 117 thm maps_to_write 118 apply (subst sep_conj_assoc[symmetric]) 119 apply (subst sep_conj_commute) 120 apply (simp add: sep_conj_assoc) 121 apply (rule maps_to_write) 122 thm maps_to_maps_to_ex 123 apply (drule sep_conj_impl1[rotated]) 124 apply (erule maps_to_maps_to_ex) 125 apply (rule sep_conj_impl1[rotated]) 126 apply (subst sep_conj_ac, assumption) 127 apply assumption 128 apply clarsimp 129 done 130 131text \<open>Now with tactics\<close> 132lemma "VARS H p q r 133 {(list p Ps ** list q Qs) H} 134 WHILE p \<noteq> 0 135 INV {\<exists>ps qs. (list p ps ** list q qs) H \<and> rev ps @ qs = rev Ps @ Qs} 136 DO r := p; p := the(H p); H := H(r \<mapsto> q); q := r OD 137 {list q (rev Ps @ Qs) H}" 138 apply vcg 139 apply fastforce 140 apply clarsimp 141 apply (case_tac ps, simp) 142 apply (rename_tac p ps') 143 apply (clarsimp simp: sep_conj_exists sep_conj_ac) 144 apply (subst points_to, sep_solve) 145 apply (rule_tac x = "ps'" in exI) 146 apply (rule_tac x = "p # qs" in exI) 147 apply (simp add: sep_conj_exists sep_conj_ac) 148 apply (rule exI) 149 apply (sep_rule (direct) maps_to_write) \<comment> \<open>note: demonstrates computation\<close> 150 apply (sep_solve add: maps_to_maps_to_ex) 151 apply clarsimp 152 done 153 154end 155