Theory ListRev

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory ListRev
imports "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file "list_rev.c"

autocorres [heap_abs_syntax] "list_rev.c"

primrec
  list :: "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list ⇒ bool"
where
  "list s p [] = (p = NULL)"
| "list s p (x#xs) = (
       p = x ∧ p ≠ NULL ∧ ptr_valid (heap_typing s) p ∧ list s (s[p]→next) xs)"

lemma list_empty [simp]:
  "list s NULL xs = (xs = [])"
  by (induct xs) auto

lemma list_in [simp]:
  "⟦ list s p xs; p ≠ NULL ⟧ ⟹ p ∈ set xs"
  by (induct xs) auto

lemma list_non_NULL:
  "⟦ p ≠ NULL ⟧ ⟹
    list s p xs = (∃ys. xs = p # ys ∧ ptr_valid (heap_typing s) p ∧ list s (s[p]→next) ys)"
  by (cases xs) auto

lemma list_unique:
  "list s p xs ⟹ list s p ys ⟹ xs = ys"
  by (induct xs arbitrary: p ys) (auto simp add: list_non_NULL)

lemma list_append_Ex:
  "list s p (xs @ ys) ⟹ (∃q. list s q ys)"
  by (induct xs arbitrary: p) auto

lemma list_distinct [simp]:
  "list s p xs ⟹ distinct xs"
  apply (induct xs arbitrary: p)
   apply simp
  apply (clarsimp dest!: split_list)
  apply (frule list_append_Ex)
  apply (auto dest: list_unique)
  done

lemma list_heap_update_ignore [simp]:
  "q ∉ set xs ⟹ list (s[q→next := v]) p xs = list s p xs"
  apply (induct xs arbitrary: p)
   apply clarsimp
  apply (clarsimp simp: fun_upd_def )
  done

definition
  the_list :: "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list"
where
  "the_list s p = (THE xs. list s p xs)"

lemma the_list_val [simp]: "list s p xs ⟹ the_list s p = xs"
  apply (clarsimp simp: the_list_def)
  apply (metis (lifting) list_unique the_equality)
  done

lemma [simp]:
   "⟦ q ∉ set xs; list s p xs ⟧ ⟹ the_list s[q→next := v] p = the_list s p"
  apply (subgoal_tac "list s[q→next := v] p xs")
   apply (metis the_list_val)
  apply clarsimp
  done

definition "reverse_inv xs list' rev' s =
                 (∃ys zs. list s list' ys
                    ∧ list s rev' zs
                    ∧ rev xs = rev ys @ zs
                    ∧ distinct (rev xs))"

lemmas runs_to_whileLoop2 =  runs_to_whileLoop_res' [split_tuple C and B arity: 2]

lemma (in ts_definition_reverse) reverse_correct:
  "list s p xs ⟹
     reverse' p ∙ s
   ⦃ λr s. ∃rv. r = Result rv ∧ list s rv (rev xs) ⦄"
  unfolding reverse'_def
  apply (runs_to_vcg)
  apply (rule runs_to_whileLoop2 [where
        I="λ(list', rev') s. reverse_inv xs list' rev' s"
        and R="measure (λ((list', rev'), s). length (the_list s list'))",
        unfolded reverse_inv_def])
  subgoal by simp
  subgoal by simp
  subgoal by (simp split: prod.splits)
  supply distinct_rev[simp del]
    apply runs_to_vcg
    subgoal 
      using list_non_NULL by blast
    subgoal for p_ys p_zs s1 ys zs
      apply (case_tac ys, fastforce)
      apply clarsimp
      subgoal for ys'
        apply (rule_tac x=ys' in exI)
        apply (simp add: fun_upd_def)
        done
      done
    subgoal for p_ys p_zs s1 ys zs
      apply (case_tac ys, fastforce)
      apply clarsimp
      subgoal for ys'
        apply (subgoal_tac "the_list s1 p_ys = (p_ys#ys')")
         apply (simp only:)
         apply simp
        apply simp
        done
      done
    done

end