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.

# Exercise 2

This is the task corresponding to exercise 2.

## Resources

### Definitions File

```theory Defs
imports "HOL-Data_Structures.Braun_Tree"
begin

definition "has_size t n = (size t = n)"

consts size2 :: "'a tree \<Rightarrow> nat"

consts has_size2 :: "'a tree \<Rightarrow> nat \<Rightarrow> bool"

end```

### Template File

```theory Submission
imports Defs
begin

fun size2 :: "'a tree \<Rightarrow> nat" where
"size2 _ = 0"

lemma size2_correct: "braun t \<Longrightarrow> size2 t = size t"
sorry

fun has_size2 :: "'a tree \<Rightarrow> nat \<Rightarrow> bool" where
"has_size2 _ _ = False"

lemma "braun t \<Longrightarrow> n \<le> size t \<Longrightarrow> has_size2 t n = has_size t n"
oops \<comment>\<open>no proof required\<close>

end```

### Check File

```theory Check
imports Submission
begin

lemma size2_correct: "braun t \<Longrightarrow> size2 t = size t"
by (rule Submission.size2_correct)

lemma "braun t \<Longrightarrow> n \<le> size t \<Longrightarrow> has_size2 t n = has_size t n"
quickcheck
oops

end```

Terms and Conditions