Cookies disclaimer

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.

Exercise 1 (Inductive Paths)

This is the task corresponding to exercise 1.

Resources

Download Files

Definitions File

theory Defs imports Main begin

inductive path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool" for r where
path0: "path r x 0 x" |
path1: "r x y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (Suc n) z"

end

Template File

theory Submission imports Defs begin        

lemma Q1: "path r x m y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (m+n) z"
  sorry


lemma Q2: "path r x n y \<Longrightarrow> path R y n x"
  oops


lemma Q3: "path r x k x \<Longrightarrow> path r x (n*k) x"
  sorry

end

Check File

theory Check imports Submission begin

theorem Q1: "path r x m y \<Longrightarrow> path r y n z \<Longrightarrow> path r x (m+n) z"
  by (rule Submission.Q1)

theorem Q3: "path r x k x \<Longrightarrow> path r x (n*k) x"
  by (rule Submission.Q3)

end

Terms and Conditions