theory exam_14
imports "AutoCorres"
begin

text {* 
  This theory is designed to be loaded with the AutoCorres logic/image via e.g.
  
  L4V_ARCH=X64 isabelle jedit -d autocorres-1.4 -l AutoCorres exam_14.thy
OR:
  L4V_ARCH=ARM isabelle jedit -d autocorres-1.4 -l AutoCorres exam_14.thy

(it was an older version back in 2014, but updated here to autocorres-1.4 
to have the same version than the one used in this year's lecture)

*}

section "Question 1: Lambda Calculus"

text {*
  (a) -- (c): Write your answers as Isabelle comments or include them in a separate .pdf 
              or .txt file.
*}

section "Question 2: Induction"

text {*
  (a-i)
*}

inductive_set pal_lists where
  pal_nil: "\<dots>" 

text {*
  (a-ii)
*}

lemma pal_lists_Cons:
  "xs \<in> pal_lists ==> x # xs \<in> pal_lists"
  sorry

text {*
  (a-iii)
*}

lemma pal_univ: "xs \<in> pal_lists"
  sorry


text {*
  (a-iv)
*}

lemma pal_induct:
  assumes nil: "P []"
  assumes one: "\<And>x. P [x]"
  assumes two: "\<And>a xs b. P xs \<Longrightarrow> P (a # xs @ [b])"
  shows "P list"
sorry


text {*
  (b)
*}

(* define palindrome *)


text {*
  (c)
*}

lemma pal_eq:
  "palindrome (a # xs @ [b]) \<Longrightarrow> a = b"
  sorry


text {*
  (d)
*}

inductive_set palindromes where
  p_nil: "\<dots>"


text {*
  (e)
*}

lemma "palindrome xs = (xs \<in> palindromes)"
  oops

section "C Verification"

install_C_file "divmod.c"

autocorres [unsigned_word_abs = divmod even] "divmod.c"

context divmod begin

text {*
  (a) -- (b): Write your answers as Isabelle comments or include them in a separate .pdf 
              or .txt file.
*}

text {*
  (c)
*}
definition
  divmod_spec :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "divmod_spec n m domod \<equiv> if domod \<noteq> 0 then n mod m else n div m"

lemma divmod'_correct:
  "ovalid (\<lambda>_. True) (divmod' n m domod) (\<lambda>r s. r = divmod_spec n m domod)"
  sorry

text {*
  (d): replace PRE below with a suitable weakest precondition and prove it correct
*}
lemma divmod'_wp:
  "ovalid PRE (divmod' n m domod) Q"
  sorry

text {*
  (e)
*}
lemma even'_correct:
  "ovalid (\<lambda>_. True) (even' n) (\<lambda>r s. r = (if even n then 1 else 0))"
  sorry

text {*
  (f): Write your answer as an Isabelle comment or in a separate .pdf or .txt file
*}

end
end