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.

Download Files
### Definitions File

### Template File

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

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

Terms and Conditions