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