theory ExerciseSession_2 imports Main begin hide_const even Ball (* 1. Let's prove together the Knaster-Tarski theorem. *) definition Lower :: "'a::order set \ 'a set" where "Lower X \ {a . \x\X. a \ x}" theorem Knaster_Tarski: fixes F :: "'a::complete_lattice \ 'a" assumes "mono F" defines "IF \ Inf {a . F a \ a}" shows "F IF = IF" (is ?A) "(\a. F a = a \ IF \ a)" (is ?B) "F IF \ IF" (is ?C) "\a. F a \ a \ IF \ a" (is ?D) sorry (* 2. Let's have a look at the most basic induction principle: structural induction for natural numbers.*) thm nat.induct thm nat.induct[where P = "\x. \k. x = 2 * k \ x = 2 * k + 1"] lemma "\k. n = 2 * k \ n = 2 * k + 1" sorry (* 3. Working out the examples from the slides: *) inductive even :: "nat \ bool" where Zero: "even 0" | Suc: "even n \ even (n+2)" thm even.Zero even.Suc thm even.cases thm even.induct lemma "even 4" sorry lemma "\ even 3" sorry lemma "even m \ \k. m = 2 * k" sorry lemma " \k. m = 2 * k \ even m" sorry (* 4. Variations *) (* This definition works out of the box: *) inductive eeven :: "nat \ bool" where Zero: "eeven 0" | Suc: "\m\n. \k\m. eeven k \ eeven n" definition Ball :: "nat \ (nat \ bool) \ bool" where "Ball n P \ \i bool" where Zero: "eeeven 0" | Suc: "Ball n eeeven \ eeeven n" *) (* Let's convince Isabelle that the definition is correct. *) (* 5. If time allows, define the sublist predicate on lists and prove properties about it. *) inductive subl :: "'a list \ 'a list \ bool" where Nil: "subl [] bs" |ConsR: "subl as bs \ subl as (b#bs)" |Cons: "subl as bs \ subl (a#as) (a#bs)" thm subl.Nil subl.ConsR thm subl.cases thm subl.induct lemma "subl [a,c] [a,b,c]" sorry lemma "\ subl [a,b,c] [a,c]" sorry lemma subl_nth_length: assumes "subl as bs" shows (* there exists a list of positions... *) "\ks. (\j (\j. Suc j < length ks \ ks!j < ks!(Suc j)) \ as = map (nth bs) ks" sorry end