Homework 4

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