theory HelperLemmasAutoCorres
imports
  "autocorres-1.4/autocorres/AutoCorres"
begin


(* Helper definitions and lemmas *)
 

install_C_file "exam.c"
autocorres [ts_rules = nondet] "exam.c"

abbreviation
  valid_node :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> bool"
where
  "valid_node s p \<equiv> \<exists>x. heap_node_C s p = x"

abbreviation
  node_next :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> node_C ptr"
where
  "node_next s p \<equiv> next_C (heap_node_C s p)"

abbreviation
  node_value :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> word32"
where
  "node_value s p \<equiv> value_C (heap_node_C s p)"

primrec
  linked_list :: "lifted_globals \<Rightarrow> node_C ptr list \<Rightarrow> node_C ptr \<Rightarrow> bool"
where
    "linked_list s [] p =
			(p = NULL)"
  | "linked_list s (x#xs) p =
			(p \<noteq> NULL \<and> p = x \<and> valid_node s p \<and> linked_list s xs (node_next s p))"

lemma linked_list_NULL [simp]:
    "linked_list s xs NULL = (xs = [])"
  by (case_tac xs, auto)

lemma linked_list_equal_list[iff]:
    "\<lbrakk> linked_list s xs p; linked_list s ys p \<rbrakk> \<Longrightarrow> xs = ys"
  apply (induct xs arbitrary: p ys)
   apply simp
  apply (case_tac ys, auto)
  done
  
lemma linked_list_equal_ptr[iff]:
    "\<lbrakk> linked_list s xs p; linked_list s xs q \<rbrakk> \<Longrightarrow> p = q"
  apply (induct xs arbitrary: p q)
   apply clarsimp
  apply clarsimp
  done
  
lemma linked_list_tail:
    "linked_list s (xs @ ys) p \<Longrightarrow> \<exists>q. linked_list s ys q"
  apply (induct xs arbitrary: p)
   apply force
  apply clarsimp
  done


definition
  is_linked_list :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> bool"
where
  "is_linked_list s p \<equiv> (\<exists>xs. linked_list s xs p)"

definition
  the_linked_list :: "lifted_globals \<Rightarrow> node_C ptr \<Rightarrow> node_C ptr list"
where
  "the_linked_list s p \<equiv> (THE xs. linked_list s xs p)"

lemma is_linked_list:
    "\<lbrakk> linked_list s xs p \<rbrakk> \<Longrightarrow> is_linked_list s p"
  by (fastforce simp: is_linked_list_def)

lemma the_linked_list_val:
    "\<lbrakk> linked_list s xs p \<rbrakk> \<Longrightarrow> the_linked_list s p = xs"
  by (auto simp: the_linked_list_def)

definition
  values_of :: "lifted_globals \<Rightarrow> node_C ptr list \<Rightarrow> word32 list"
where
  "values_of s xs = map (node_value s) xs"

lemma the_linked_list_next:
  "\<lbrakk> is_linked_list s next; next \<noteq> NULL \<rbrakk> \<Longrightarrow>
      the_linked_list s next = next # (the_linked_list s (node_next s next))"
  apply (clarsimp simp: is_linked_list_def)
  apply (subst the_linked_list_val, assumption)
  apply (metis linked_list.simps(2) linked_list_NULL
      linked_list_equal_ptr the_linked_list_val not_NilE)
  done

lemma is_linked_list_next [simp]:
  "\<lbrakk> is_linked_list s next; next \<noteq> NULL \<rbrakk> \<Longrightarrow>
      is_linked_list s (node_next s next)"
  apply (clarsimp simp: is_linked_list_def)
  apply (case_tac xs, auto)
  done

lemma the_linked_list_NULL [simp]:
   "the_linked_list s NULL = []"
  by (clarsimp simp: the_linked_list_def)
  
end