Exercise 4

Definitions File

theory Defs
  imports "HOL-IMP.BExp"
begin

type_synonym vname = string
type_synonym val = "int list"
type_synonym state = "vname \<Rightarrow> val"

datatype exp = N val | V vname | Square exp | Append exp exp | Take nat exp

definition square :: "val \<Rightarrow> val" where "square \<equiv> map (\<lambda>x. x * x)"

fun lval :: "exp \<Rightarrow> state \<Rightarrow> val" where
"lval (N xs) s = xs" |
"lval (V x) s = s x" |
"lval (Square e) s = square (lval e s)" |
"lval (Append e1 e2) s = lval e1 s @ lval e2 s" |
"lval (Take n e) s = take n (lval e s)"

datatype eint = Z int
  | NInf   \<comment>\<open>negative infinity "\<open>-\<infinity>\<close>"\<close>
  | PInf   \<comment>\<open>positive infinity "\<open>\<infinity>\<close>"\<close>

fun \<gamma>_eint :: "eint \<Rightarrow> val set" where
"\<gamma>_eint NInf = {[]}" |
"\<gamma>_eint PInf = UNIV" |
"\<gamma>_eint (Z i) = {xs. xs = [] \<or> Max (set xs) \<le> i}"

fun num_eint :: "val \<Rightarrow> eint" where
"num_eint [] = NInf" |
"num_eint xs = Z (Max (set xs))"

(*just some dummy function (DO NOT MODIFY)*)
fun inv_square :: "eint \<Rightarrow> eint \<Rightarrow> eint" where "inv_square _ _ = undefined"

end

Template File

theory Submission
  imports Defs
begin

section \<open>Abstract Listification\<close>

text \<open>For this exercise, we will consider a modification of IMP that computes on integer lists:\<close>

text \<open>Next to constants and variables, the language offers expressions (@{typ exp}) to
  \<^item> square all numbers contained in a list,
  \<^item> append two lists, and
  \<^item> take \<open>n\<close> elements of a list.

The semantics is given in @{term lval}.

Consider an abstract interpreter on the domain consisting of \<open>\<int> \<union> {-\<infinity>, \<infinity>}\<close> for this language
(@{typ eint}), indicating the least upper bound of all elements contained in a list.

The concretization and abstraction functions are given in @{term \<gamma>_eint} and @{term num_eint}.

Your task is to define the abstract operations
and to show that they are sound with respect to the concretization function.
Your abstract operations should be as precise as possible!

\<^emph>\<open>Hint for the proofs:\<close> If you want to perform nested case splittings on variables \<open>x_1,...,x_n\<close>,
you can use \<open>apply (cases x_1; cases x_2; ...; cases x_n)\<close>.\<close>

fun square_eint :: "eint \<Rightarrow> eint" where
"square_eint _ = undefined"

fun append_eint :: "eint \<Rightarrow> eint \<Rightarrow> eint" where
"append_eint _ = undefined"

fun take_eint :: "nat \<Rightarrow> eint \<Rightarrow> eint" where
"take_eint _ = undefined"

lemma square_sound: "\<lbrakk> xs \<in> \<gamma>_eint ei \<rbrakk> \<Longrightarrow> square xs \<in> \<gamma>_eint (square_eint ei)"
  sorry

lemma append_sound:
  "\<lbrakk> xs1 \<in> \<gamma>_eint ei1; xs2 \<in> \<gamma>_eint ei2 \<rbrakk> \<Longrightarrow> (xs1 @ xs2) \<in> \<gamma>_eint (append_eint ei1 ei2)"
  sorry

lemma take_sound: "\<lbrakk> xs \<in> \<gamma>_eint ei \<rbrakk> \<Longrightarrow> take n xs \<in> \<gamma>_eint (take_eint n ei)"
  sorry

text \<open>Now assume that we have an inverse analyses @{term "inv_square :: eint \<Rightarrow> eint \<Rightarrow> eint"} for
@{term Square}. Write down the statement of the correctness theorem for @{term inv_square} as a
definition called \<open>inv_square_correct\<close>:\<close>

definition inv_square_correct :: bool where
  "inv_square_correct \<equiv> undefined"

end

Check File

theory Check
  imports Submission
begin


end