theory Inductive_Exercises
imports Main
begin
inductive coinfinite :: "nat set \ bool" where
"coinfinite UNIV" |
"\coinfinite S; S' = S \ {m}\ \ coinfinite S'" |
"\coinfinite S; S' = S - {m}\ \ coinfinite S'"
lemma
assumes "finite T" and "coinfinite S"
shows "coinfinite (S - T)"
sorry
lemma
assumes "coinfinite S"
shows "\T. finite T \ S = UNIV - T"
using assms
sorry
lemma
assumes "coinfinite S" and "coinfinite T"
shows "coinfinite (S \ T)"
sorry
lemma
assumes "coinfinite S" and "coinfinite T"
shows "coinfinite (S \ T)"
sorry
inductive map :: "('a \ 'b) \ 'a list \ 'b list \ bool" where
"\ys = []\ \ map f [] ys" |
"\map f xs ys; ys' = (f x)#ys\ \ map f (x#xs) ys'"
lemma
shows "map id xs xs"
sorry
lemma
assumes "map f xs ys" and "map g ys zs"
shows "map (g o f) xs zs"
using assms
sorry
inductive every_other_same :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool"
and every_other_diff :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where
"ys' = [] \ every_other_same R [] ys'" |
"\every_other_diff R xs ys; R x y; ys' = (y#ys)\ \ every_other_same R (x#xs) ys'" |
"\\ R x y; y' = [y]\ \ every_other_diff R [x] y'" |
"\every_other_same R xs ys; \ R x y; ys' = (y#ys)\ \ every_other_diff R (x#xs) ys'"
lemma
shows "every_other_same R xs ys \ length xs = length ys"
and "every_other_diff R xs ys \ length xs = length ys"
sorry
inductive_set strings :: "'a set \ 'a list set" for \ where
"[] \ strings \" |
"\a \ \; as \ strings \\ \ a#as \ strings \"
lemma
assumes "\1 \ \2"
shows "strings \1 \ strings \2"
sorry
lemma
assumes "as \ strings \" and "bs \ strings \"
shows "as@bs \ strings \"
using assms
sorry
section\A more ambitious exercise: Glivenko's theorem\
(* Theorem (Glivenko): If \ is a propositional formula, then {} \\<^sub>C \ if and only if {} \\<^sub>I \\\.
That is, for propositional formulae, \ is a classical tautology if and only if \\\ is an
intuitionistic tautology.
*)
section\A more ambitious exercise: SKI combinators\
(* Read up on the SKI combinator calculus. Embed the calculus and its reduction relation in
Isabelle. Show that the reduction relation is confluent.
(A relation \ is confluent when:
If r \\<^sup>\ s and r \\<^sup>\ t then there exists u such that s \\<^sup>\ u and t \\<^sup>\ u
where \\<^sup>\ is the reflexive, transitive closure of \)
You will need to model \ and \\<^sup>\ as inductive relations and define the set of SKI terms as
a datatype.
*)
end