Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 02

This is the homework corresponding to exercise sheet 02.

## Resources

### Definitions File

```theory Defs
imports "HOL-IMP.AExp" "HOL-IMP.BExp"
begin

end```

### Template File

```theory Submission
imports Defs
begin

text \<open>Delta Encoding\<close>
text \<open>
We want to encode a list of integers as follows:
The first element is unchanged, and every next element
only indicates the difference to its predecessor.

For example: (Hint: Use this as test cases for your spec!)
\<^item> \<open>enc [1,2,4,8] = [1,1,2,4]\<close>
\<^item> \<open>enc [3,4,5] = [3,1,1]\<close>
\<^item> \<open>enc  = \<close>
\<^item> \<open>enc [] = []\<close>

Background: This algorithm may be used in lossless data compression,
when the difference between two adjacent values is expected to be
small, as e.g. in audio data, image data, or sensor data.

It typically requires much less space to store the small deltas than  the absolute values.

Disadvantage: If the stream gets corrupted, recovery is only
possible  when the next absolute value is transmitted. For this reason,
in practice, one will submit the current absolute value from
time to time. (This is not modeled in this exercise!)
\<close>
text \<open>
Specify a function to encode a list with delta-encoding.
The first argument is used to represent the previous value, and can
be initialized to 0.\<close>

fun denc :: "int \<Rightarrow> int list \<Rightarrow> int list" where
"denc prv _ = undefined"

text \<open>
Specify the decoder. Again, the first argument represents the
previous decoded value, and can be initialized to 0.\<close>

fun ddec :: "int \<Rightarrow> int list \<Rightarrow> int list" where
"ddec prv _ = undefined"

text \<open>
Show that encoding and then decoding yields the same list. \<^emph>\<open>Hint:\<close>
The lemma will need generalization.\<close>

lemma decode_code: "ddec 0 (denc 0 l) = l"
sorry

text \<open>Boolean Expressions With Equality\<close>
text \<open>
Our current version of Boolean expressions is missing an equality operator on arithmetic expressions.
In this exercise your task is to define a function \<open>beq\<close> that, given two arithmetic expressions
\<open>a\<^sub>1\<close> and \<open>a\<^sub>2\<close>, constructs a Boolean expression \<open>beq a\<^sub>1 a\<^sub>2\<close> such that:
\<close>

definition beq :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
"beq a1 a2 = Bc False"

lemma bval_beq:
"bval (beq a1 a2) s \<longleftrightarrow> aval a1 s = aval a2 s"
sorry

text \<open>Models for Boolean Formulas\<close>
text \<open>
Consider the following datatype modeling Boolean formulas:
\<close>

datatype 'a bexp' = V 'a | And "'a bexp'" "'a bexp'" | Not "'a bexp'" | TT | FF

text \<open>Define a function \<open>sat\<close> that decides whether a given assignment satisfies a formula:\<close>
fun sat :: "'a bexp' \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
where
"sat _ _ \<longleftrightarrow> undefined"

text \<open>Define a function \<open>models\<close> that computes the set of satisfying assignments for a given
Boolean formula:\<close>

fun models :: "'a bexp' \<Rightarrow> ('a \<Rightarrow> bool) set"
where
"models _ = undefined"

text \<open>Here @{thm UNIV_def}. Fill in the remaining cases!
\<^emph>\<open>Hint:\<close> You can use the set operators \<open>-\<close>, \<open>\<inter>\<close>, \<open>\<union>\<close> for complement/difference, intersection,
and union of sets.\<close>

text \<open>Finally prove that a formula is a satisfying assignment for a formula \<open>\<phi>\<close> iff it is contained
in \<open>models \<phi>\<close>:\<close>

lemma models_correct:
"sat \<phi> \<sigma> \<longleftrightarrow> \<sigma> \<in> models \<phi>"
sorry

text \<open>Simplifying Boolean Formulas (Bonus)\<close>
text \<open>\<^emph>\<open>Note:\<close> This is a bonus exercise worth three additional points.
In the end, the total number of achievable points will be the sum of all the points you can
get for all regular exercises. When we calculate the percentage of the total points you reached,
we will just add the bonus points on top of the points you got in the regular exercises.
\<close>

text \<open>In this exercise, we want to simplify the Boolean formulas defined in the previous exercise
by removing the constants @{term FF} and @{term TT} from them where possible.
We will say that a formula is \<^emph>\<open>simplified\<close> if does not contain a constant or if it is
@{term FF} or @{term TT} itself.
\<close>
fun has_const where
"has_const TT = True"
| "has_const FF = True"
| "has_const (Not a) = has_const a"
| "has_const (And a b) \<longleftrightarrow> has_const a \<or> has_const b"
| "has_const _ = False"

definition "simplified \<phi> \<longleftrightarrow> \<phi> = TT \<or> \<phi> = FF \<or> \<not> has_const \<phi>"

fun simplify :: "'a bexp' \<Rightarrow> 'a bexp'" where
"simplify x = undefined"

text \<open>Define a function @{term [show_types] simplify} that simplifies Boolean formulas and
prove that it produces only simplified formulas:\<close>

lemma simplify_simplifies: "simplified (simplify \<phi>)"
sorry

text \<open>Even more importantly, you need to prove that \<open>simplify\<close> does not alter the semantics of
the formula:\<close>

lemma simplify_correct: "models (simplify \<phi>) = models \<phi>"
sorry

end```

### Check File

```theory Check
imports Submission
begin

text \<open>Test cases for @{term denc}:\<close>
lemma
"denc 0 [1,2,4,8] = [1,1,2,4]"
"denc 0 [3,4,5] = [3,1,1]"
"denc 0  = "
"denc 0 [] = []"
by simp+

lemma decode_code:
"ddec 0 (denc 0 l) = l"
by (rule Submission.decode_code)

lemma bval_beq:
"bval (beq a1 a2) s \<longleftrightarrow> aval a1 s = aval a2 s"
by (rule Submission.bval_beq)

lemma models_correct:
"sat \<phi> \<sigma> \<longleftrightarrow> \<sigma> \<in> models \<phi>"
by (rule Submission.models_correct)

lemma simplify_simplifies: "simplified (simplify \<phi>)"
by (rule Submission.simplify_simplifies)

lemma simplify_correct: "models (simplify \<phi>) = models \<phi>"
by (rule Submission.simplify_correct)

end```

Terms and Conditions