1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory ListRev 8imports "AutoCorres.AutoCorres" 9begin 10 11external_file "list_rev.c" 12install_C_file "list_rev.c" 13 14autocorres [heap_abs_syntax] "list_rev.c" 15 16primrec 17 list :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> node_C ptr list \<Rightarrow> bool" 18where 19 "list s p [] = (p = NULL)" 20| "list s p (x#xs) = ( 21 p = x \<and> p \<noteq> NULL \<and> is_valid_node_C s p \<and> list s (s[p]\<rightarrow>next) xs)" 22 23lemma list_empty [simp]: 24 "list s NULL xs = (xs = [])" 25 by (induct xs) auto 26 27lemma list_in [simp]: 28 "\<lbrakk> list s p xs; p \<noteq> NULL \<rbrakk> \<Longrightarrow> p \<in> set xs" 29 by (induct xs) auto 30 31lemma list_non_NULL: 32 "\<lbrakk> p \<noteq> NULL \<rbrakk> \<Longrightarrow> 33 list s p xs = (\<exists>ys. xs = p # ys \<and> is_valid_node_C s p \<and> list s (s[p]\<rightarrow>next) ys)" 34 by (cases xs) auto 35 36lemma list_unique: 37 "list s p xs \<Longrightarrow> list s p ys \<Longrightarrow> xs = ys" 38 by (induct xs arbitrary: p ys) (auto simp add: list_non_NULL) 39 40lemma list_append_Ex: 41 "list s p (xs @ ys) \<Longrightarrow> (\<exists>q. list s q ys)" 42 by (induct xs arbitrary: p) auto 43 44lemma list_distinct [simp]: 45 "list s p xs \<Longrightarrow> distinct xs" 46 apply (induct xs arbitrary: p) 47 apply simp 48 apply (clarsimp dest!: split_list) 49 apply (frule list_append_Ex) 50 apply (auto dest: list_unique) 51 done 52 53lemma list_heap_update_ignore [simp]: 54 "q \<notin> set xs \<Longrightarrow> list (s[q\<rightarrow>next := v]) p xs = list s p xs" 55 apply (induct xs arbitrary: p) 56 apply clarsimp 57 apply (clarsimp simp: fun_upd_def) 58 done 59 60definition 61 the_list :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> node_C ptr list" 62where 63 "the_list s p = (THE xs. list s p xs)" 64 65lemma the_list_val [simp]: "list s p xs \<Longrightarrow> the_list s p = xs" 66 apply (clarsimp simp: the_list_def) 67 apply (metis (lifting) list_unique the_equality) 68 done 69 70lemma [simp]: 71 "\<lbrakk> q \<notin> set xs; list s p xs \<rbrakk> \<Longrightarrow> the_list s[q\<rightarrow>next := v] p = the_list s p" 72 apply (subgoal_tac "list s[q\<rightarrow>next := v] p xs") 73 apply (metis the_list_val) 74 apply clarsimp 75 done 76 77definition "reverse_inv xs list' rev' s = 78 (\<exists>ys zs. list s list' ys 79 \<and> list s rev' zs 80 \<and> rev xs = rev ys @ zs 81 \<and> distinct (rev xs))" 82 83lemma (in list_rev) reverse_correct: 84 "\<lbrace> \<lambda>s. list s p xs \<rbrace> 85 reverse' p 86 \<lbrace> \<lambda>rv s. list s rv (rev xs) \<rbrace>!" 87 apply (clarsimp simp: reverse'_def) 88 apply (subst whileLoop_add_inv [where 89 I="\<lambda>(list', rev') s. reverse_inv xs list' rev' s" 90 and M="\<lambda>((list', rev'), s). length (the_list s list')", 91 unfolded reverse_inv_def]) 92 apply wp 93 apply (clarsimp simp del: distinct_rev) 94 apply (case_tac ys, fastforce) 95 apply (clarsimp simp del: distinct_rev) 96 apply (rule_tac x=lista in exI) 97 apply (simp add: fun_upd_def) 98 apply (clarsimp simp del: distinct_rev) 99 apply simp 100 done 101 102end 103