I agree 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.
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
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
theory Check imports Submission begin end