Exercise 1

Definitions File

theory Defs
  imports
    Main
begin

inductive to_zero :: "nat list \<Rightarrow> bool" where
tz0: "to_zero [0]" |
tzS: "to_zero (x # xs) \<Longrightarrow> to_zero (Suc x # x # xs)"

end

Template File

theory Submission
  imports Defs
begin

section \<open>Induction\<close>

text \<open>Consider the inductive predicate @{term to_zero}.\<close>

text \<open>Define an executable, recursive function \<open>enum :: nat \<Rightarrow> nat list\<close> that makes the
following two theorems true and prove the theorems!\<close>

fun enum :: "nat \<Rightarrow> nat list" where
"enum _ = undefined"

(*make sure that your function is executable, i.e. these commands should work*)
value "enum 0"
value "enum 7"
value "enum 42"

text \<open>Now prove:\<close>

lemma enum_if_to_zero:
  assumes "to_zero xs"
  shows "\<exists>n. enum n = xs"
sorry


lemma to_zero_enum: "to_zero (enum n)"
sorry

end

Check File

theory Check
  imports Submission
begin

end