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 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
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
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