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 4

This is the task corresponding to homework 4.

## Resources

### Definitions File

theory Defs imports Main begin

inductive ev :: "nat \<Rightarrow> bool" where
ev0: "ev 0" |
evSS: "ev n \<Longrightarrow> ev (Suc (Suc n))"

lemma "ev (Suc (Suc n)) \<Longrightarrow> ev n"
proof -
assume "ev (Suc (Suc n))" then show "ev n"
proof (cases)
txt \<open>\qquad ...\<close>  case evSS thus "ev n" .   qed
qed

inductive_cases evSS_elim: "ev (Suc (Suc n))"

lemma "ev (Suc (Suc n)) \<Longrightarrow> ev n"
by (auto elim: evSS_elim)

lemma "\<not> ev (Suc (Suc (Suc 0)))"
proof
assume "ev (Suc (Suc (Suc 0)))" then show "False"
proof (cases)
assume "ev (Suc 0)" then show "False"
proof (cases)
qed
qed
qed

inductive_cases evS0_elim: "ev (Suc 0)"

lemma "\<not> ev (Suc (Suc (Suc 0)))"
by (auto elim: evSS_elim evS0_elim)

lemma "\<not> ev (Suc (Suc (Suc 0)))"
by (auto elim: ev.cases)

type_synonym ('q,'l) lts = "'q \<Rightarrow> 'l \<Rightarrow> 'q \<Rightarrow> bool"

inductive word :: "('q,'l) lts \<Rightarrow> 'q \<Rightarrow> 'l list \<Rightarrow> 'q \<Rightarrow> bool" for \<delta>
where
empty: "word \<delta> q [] q"
| prepend: "\<lbrakk>\<delta> p l ph; word \<delta> ph ls q\<rbrakk> \<Longrightarrow> word \<delta> p (l # ls) q"

definition "det \<delta> \<equiv> \<forall>p l q1 q2. \<delta> p l q1 \<and> \<delta> p l q2 \<longrightarrow> q1 = q2"

lemma
assumes det: "det \<delta>"
shows "word \<delta> p ls q \<Longrightarrow> word \<delta> p ls q' \<Longrightarrow> q = q'"
proof (induction rule: word.induct)
case empty thus ?case by cases simp
next
case (prepend p l ph ls q)
from prepend.prems obtain ph' where step: "\<delta> p l ph'" and word: "word \<delta> ph' ls q'"
by cases
from det[unfolded det_def] step \<open>\<delta> p l ph\<close> have "ph' = ph"
by simp
with prepend.IH word show "q = q'"
by simp
qed

fun count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
"count x [] = 0"
| "count x (y # ys) = (if x=y then Suc (count x ys) else count x ys)"

lemma "count a xs = Suc n \<Longrightarrow> \<exists>ps ss. xs = ps @ a # ss \<and> count a ps = 0 \<and> count a ss = n"
proof (induction xs arbitrary: n)
case Nil thus ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "a = x")
case [simp]: True
from \<open>count a (x # xs) = Suc n\<close> have "count a xs = n" by simp
moreover have "x # xs = [] @ a # xs" by simp
moreover have "count a [] = 0" by simp
ultimately show ?thesis by blast
next
case [simp]: False
from Cons.prems have "count a xs = Suc n" by simp
from Cons.IH[OF this] obtain ps ss where "x # xs = (x # ps) @ a # ss" "count a (x # ps) = 0" "count a ss = n"
by auto
thus ?thesis by blast
qed
qed

end

### Template File

theory Submission imports Defs begin

inductive is_path :: "('v \<times> 'v) set \<Rightarrow> 'v \<Rightarrow> 'v list \<Rightarrow> 'v \<Rightarrow> bool"

lemma "is_path {(i, i+1) | i::nat. True} 3 [3, 4, 5] 6"
sorry

lemma "is_path {(i, i+1) | i::nat. True} 1 [] 1"
sorry

theorem path_appendI:
"\<lbrakk>is_path E u p1 v; is_path E v p2 w\<rbrakk> \<Longrightarrow> is_path E u (p1 @ p2) w"
sorry

theorem path_appendE:
"is_path E u (p1 @ p2) w \<Longrightarrow> \<exists>v. is_path E u p1 v \<and> is_path E v p2 w"
sorry

thm less_induct

theorem path_distinct:
"is_path E u p v \<Longrightarrow> \<exists>p'. distinct p' \<and> is_path E u p' v"
sorry

datatype ab = a | b

inductive S :: "ab list \<Rightarrow> bool" where
add: "S w \<Longrightarrow> S (a # w @ [b])"
| nil: "S []"

theorem S_correct:
"S w \<longleftrightarrow> (\<exists> n. w = replicate n a @ replicate n b)"
sorry

end

### Check File

theory Check imports Submission begin

theorem path_appendI:
"\<lbrakk>is_path E u p1 v; is_path E v p2 w\<rbrakk> \<Longrightarrow> is_path E u (p1 @ p2) w"
by (rule Submission.path_appendI)

theorem path_appendE:
"is_path E u (p1 @ p2) w \<Longrightarrow> \<exists>v. is_path E u p1 v \<and> is_path E v p2 w"
by (rule Submission.path_appendE)

theorem path_distinct:
"is_path E u p v \<Longrightarrow> \<exists>p'. distinct p' \<and> is_path E u p' v"
by (rule Submission.path_distinct)

theorem S_correct:
"S w \<longleftrightarrow> (\<exists> n. w = replicate n a @ replicate n b)"
by (rule Submission.S_correct)

end

Terms and Conditions