theory soln 
imports AutoCorres.AutoCorres
begin

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

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

\<close>

section "Question 1: Lambda Calculus"

text \<open>
  (a) -- (c): Write your answers as Isabelle comments or include them in a separate .pdf 
              or .txt file.
\<close>

section "Question 2: Induction"

text \<open>
  (a-i)
\<close>

inductive_set pal_lists where
  pal_empty: "[] \<in> pal_lists" |
  pal_singleton: "[x] \<in> pal_lists" |
  pal_dblappend: "\<lbrakk>xs \<in> pal_lists\<rbrakk> \<Longrightarrow> a # xs @ [b] \<in> pal_lists"

text \<open>
  (a-ii)
\<close>

lemma pal_lists_Cons:
  "xs \<in> pal_lists \<Longrightarrow> a # xs \<in> pal_lists"
  apply(induct xs arbitrary: a rule: pal_lists.induct) 
  (*---OPTION 1: sledgehammer *)
 (*   (*sledgehammer*)
    apply (simp add: pal_lists.pal_singleton)
   (*sledgehammer*)
   using pal_lists.pal_dblappend pal_lists.pal_empty apply fastforce
  (*sledgehammer*)
  using pal_lists.simps by fastforce*)
  (*---OPTION 2 manually*)
    apply(rule pal_singleton)
   apply(rule pal_dblappend[OF pal_empty, simplified])
   (* The one line above with "OF" can be replaced by:
    apply (cut_tac pal_empty)
    apply (drule pal_dblappend) 
    apply simp
   OR
    apply (subgoal_tac "[]\<in>pal_lists") 
     prefer 2 
     apply (rule pal_empty) 
    apply (drule pal_dblappend) 
    apply simp
    *)
  apply(subst append.simps(2)[symmetric])
  apply(rule pal_dblappend)
  apply blast
  done

text \<open>
  (a-iii)
\<close>
   
lemma pal_univ: "xs \<in> pal_lists"
  apply(induct xs)
   apply(rule pal_empty)
  apply(erule pal_lists_Cons)
  done

text \<open>
  (a-iv)
\<close>

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"
  using pal_univ assms
  by(rule pal_lists.induct)

(* Direct proof with no detour through an inductive relation *)
lemma pal_induct2:
  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"
  apply(induct rule: length_induct)
  subgoal for xs
    apply(cases xs)
     apply(simp add: nil)
    subgoal for x xxs
      apply(cases "rev xxs")
       apply(simp add: one)
      apply simp
      apply(rule two)
      apply auto
      done
    done
  done

text \<open>
  (b)
\<close>

definition
  palindrome :: "'a list \<Rightarrow> bool"
where
  "palindrome xs \<equiv> rev xs = xs"


text \<open>
  (c)
\<close>

lemma pal_eq:
  "palindrome (a # xs @ [b]) \<Longrightarrow> a = b"
  apply(unfold palindrome_def) 
  apply(simp del: rev.simps) (*OR sledgehammer*)
  done   

text \<open>
  (d)
\<close>

inductive_set palindromes where
  palindrome_empty: "[] \<in> palindromes" |
  palindrome_singleton: "[a] \<in> palindromes" |
  palindrome_step: "xs \<in> palindromes ==> a # xs @ [a] \<in> palindromes"

text \<open>
  (e)
\<close>

text \<open> Produces a helpful elimination rule for doing case
   analysis on the derivation of @{term "(x#xs@[y]) \<in> palindromes"}
     \<close>
inductive_cases sandwichE: "(x#xs@[y]) \<in> palindromes"

lemma "palindrome xs = (xs \<in> palindromes)"
  unfolding palindrome_def
  apply(induct rule: pal_induct)
    apply(simp add: palindrome_empty)
   apply(simp add: palindrome_singleton)
  apply clarsimp
  apply(rule iffI)
   apply(blast intro: palindrome_step)
  apply(force elim: sandwichE)
  done
(* Alternative proof where each direction of the iff gets
   its own induction
   apply(rule iffI)
   apply(induct xs rule: pal_induct)
     apply(rule palindrome_empty)
    apply(rule palindrome_singleton)
   apply(frule pal_eq)
   apply(erule ssubst)
   apply(rule palindrome_step)
   apply (simp add: palindrome_def)
  apply(induct xs rule: palindromes.induct)
  apply(auto simp: palindrome_def)
  done*)
   
section "C Verification"

external_file "divmod.c"
install_C_file "divmod.c"

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

context divmod begin

text \<open>
  (a)
\<close>
thm divmod'_def
thm even'_def

term divmod'
term even'
(*
Functions produced by AutoCorres:

divmod' ?n ?m ?domod \<equiv>
DO (d, n) \<leftarrow>
   owhile (\<lambda>(d, n) a. ?m \<le> n)
    (\<lambda>(d, n). DO oguard (\<lambda>s. Suc d \<le> UINT_MAX);
                  oreturn (Suc d, n - ?m)
               OD)
    (0, ?n);
   oreturn (if 0 < ?domod then n else d)
OD

even' ?n \<equiv> DO ret' \<leftarrow> divmod' ?n 2 1;
               oreturn (if ret' = 0 then 1 else 0)
            OD
Types:

"divmod'"
  :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> lifted_globals \<Rightarrow> nat option"

"even'"
  :: "nat \<Rightarrow> lifted_globals \<Rightarrow> nat option"

AutoCorres uses the option monad to represent both functions.

*)


text \<open>
  (b)
\<close>

(*
 No, if m=0 the program divmod does not terminate.  
*)

text \<open>
  (c)
\<close>
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)"
  unfolding divmod'_def divmod_spec_def
  apply(subst owhile_add_inv[where I="\<lambda>(d,n') s. n = n' + d * m"])
  apply(wpsimp)
  done

text \<open>
  (d): replace PRE below with a suitable weakest precondition and prove it correct
\<close>
lemma ovalid_to_wp:
  "ovalid (\<lambda>_. True) f (\<lambda>r s. r = X) \<Longrightarrow>
   ovalid (P X) f P"
  apply(clarsimp simp: ovalid_def)
  done

lemma divmod'_wp:
  "ovalid (Q (divmod_spec n m domod)) (divmod' n m domod) Q"
  using divmod'_correct
  unfolding ovalid_def
  by blast

text \<open>
  (e)
\<close>

lemma even'_correct:
  "ovalid (\<lambda>_. True) (even' n) (\<lambda>r s. r = (if even n then 1 else 0))"
  unfolding even'_def
  apply(wp divmod'_wp)
  apply(simp add: divmod_spec_def)
  apply arith (* OR: sledgehammer *)
  done
    
  (* NOTE: you need to remember that you can add rules to wp.
     Otherwise you can prove it as follows: 
     replace the line "apply(wp divmod'_wp)" by:

  apply wp 
  apply(rule ohoare_weaken_pre)
  apply (rule divmod'_wp)
 
     The issue is that the hoare_weaken_pre rule doesn't exist (yet)
     for the option monad (i.e. for ovalid). But you can prove it:
     you basically copy-paste the proof of hoare_weaken_pre 
     and replace the \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>  (i.e. the valid Q a R) 
     by ovalid Q a R:

lemma ohoare_pre_imp: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s; ovalid Q a R \<rbrakk> \<Longrightarrow> ovalid P a R"
  by (fastforce simp add:ovalid_def)

lemma ohoare_weaken_pre:
  "\<lbrakk>ovalid Q a R; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> ovalid P a R"
  apply (rule ohoare_pre_imp)
   prefer 2
   apply assumption
  apply blast
  done
 *)

    
    
    
    
text \<open>
  (f)
\<close>

(*
  Yes, even always terminates because it doesn't contain 
  any loops and calls divmod with argument m=2. Therefore, 
  for the loop in divmod, the value of n decreases by 2 in 
  each iteration, hence, the number of iterations is less 
  than or equal to n/2.
*)

end

text \<open> Bonus question: Recursive functions \<close>

datatype regexp =
   Atom char
 | Alt regexp regexp
 | Conc regexp regexp (infixl "\<cdot>"  60)
 | Star regexp
 | Neg regexp

(* Match everything: *)
definition
  "Univ = Alt (Neg (Atom (CHR ''x''))) (Atom (CHR ''x''))"

(* Match nothing: *)
definition
  "null = Neg Univ"

(* Match only the empty string: *)
definition
  "epsilon = Star null"

(* For examples/testing. *)
primrec string :: "char list \<Rightarrow> regexp"
  where
  "string []     = epsilon"
| "string (x#xs) = Atom x \<cdot> string xs"

(* Automatically coerce type "char list" into "regexp" using the function "string" *)
declare [[coercion string, coercion_enabled]]
term "Star ''abc''"

(* A set of strings repeated 0 or more times *)
inductive_set star :: "string set \<Rightarrow> string set" for L
  where
  star_empty[simp,intro!]: "[] \<in> star L"
| star_app[elim]: "\<lbrakk> u \<in> L; v \<in> star L \<rbrakk> \<Longrightarrow> u@v \<in> star L"

(* The concatenation of two sets of strings *)
definition conc :: "string set \<Rightarrow> string set \<Rightarrow> string set"
  where
  "conc A B \<equiv> { xs@ys |xs ys. xs \<in> A \<and> ys \<in> B}"

(* The sets of strings matched by an expression *)
primrec
  lang :: "regexp \<Rightarrow> string set"
  where
  "lang (Atom c) = {[c]}"
| "lang (Alt e1 e2) = lang e1 \<union> lang e2"
| "lang (Conc e1 e2) = conc (lang e1) (lang e2)"
| "lang (Star e) = star (lang e)"
| "lang (Neg e) = -lang e"

(* ------------------------------------------------------------ *)
(* New for the exam: *)

primrec split :: "('a list \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  where
  "split P Q xs [] = (P xs \<and> Q [])"
| "split P Q xs (y#ys) = (P xs \<and> Q (y#ys) \<or> split P Q (xs@[y]) ys)"

(* --------- 1a ------------ *)
lemma split_eq[simp]:
  "split P Q xs ys = (\<exists>as bs. ys = as @ bs \<and> P (xs@as) \<and> Q bs)"
  apply(induct ys arbitrary: xs)
   apply simp
  apply(clarsimp;safe)
     apply force
    apply(rule_tac x="x1#as" in exI)
    apply simp
   apply (metis Cons_eq_append_conv append_Nil2)
  by (metis Cons_eq_append_conv)


lemma split_cong[fundef_cong,cong]:
  "\<lbrakk> xs = xs'; ys = ys'; P = P'; \<And>bs. length bs \<le> length ys' \<Longrightarrow> Q bs = Q' bs \<rbrakk> 
  \<Longrightarrow> split P Q xs ys = split P' Q' xs' ys'"
  by force

declare nat_le_Suc_less[simp]

(* Executable version of determining a regular expression match with negation. *)
fun matches :: "regexp \<Rightarrow> string \<Rightarrow> bool"
  where
  "matches (Atom c) cs     = (cs = [c])"
| "matches (Alt r1 r2) cs  = (matches r1 cs \<or> matches r2 cs)"
| "matches (Conc r1 r2) cs = split (matches r1) (matches r2) [] cs"
| "matches (Neg r) cs      = (\<not> matches r cs)"
| "matches (Star r) cs     = (cs \<noteq> [] \<longrightarrow> split (matches r) (matches (Star r)) [hd cs] (tl cs))"

(* Unfold matches_Star manually with "subst" because it's prone to simplifier loops *)
lemmas matches_Star[simp del] = matches.simps(5)

(* Examples *)
value "matches (Star (Alt ''ab'' ''a'')) ''''"
value "matches (Star (Alt ''ab'' ''a'')) ''ababa''"
value "matches (Star (Alt ''ab'' ''a'')) ''abba''"
value "matches (Neg (Star (Alt ''ab'' ''a''))) ''abba''"


(* --------- 1b ------------ *)

lemma matches_null[simp]:
 "matches null cs = False"
by(simp add: null_def Univ_def)

lemma matches_epsilon_[simp]:
 "matches epsilon cs = (cs = [])"
  unfolding epsilon_def
  apply(subst matches.simps)
  apply(cases cs;auto)
  done

lemma matches_string:
  "matches (string xs) cs = (cs = xs)"
  apply(induct xs arbitrary: cs)
   apply simp
  apply simp
  done

(* --------- 1c ------------ *)

lemma star_cons_append[elim]:
  "\<lbrakk> a # as \<in> L; bs \<in> star L\<rbrakk> \<Longrightarrow> a # as @ bs \<in> star L"
  by(auto dest: star.intros(2))

lemma star_cases:
  "xs \<in> star A \<Longrightarrow> xs = [] \<or> (\<exists>u v. xs = u@v \<and> u \<in> A \<and> v \<in> star A \<and> u \<noteq> [])"
  by (induct rule: star.induct) auto

lemma star_cons_case[dest!]:
  "x#xs \<in> star L \<Longrightarrow> (\<exists>u v. xs = u@v \<and> x#u \<in> L \<and> v \<in> star L)"
  by(drule star_cases,clarsimp) (case_tac u;force)

lemma matches_correct:
  "matches r cs = (cs \<in> lang r)"
  apply(induct rule: matches.induct)
      apply(auto simp add: conc_def)[4]
  apply(subst matches.simps)
  apply(case_tac cs;force)
  done

end