theory week01A_demo2 imports Main begin text "lambda terms" term "\x. x" text "alpha" thm refl lemma "(\x. x) = (\y. y)" apply (rule refl) done text "eta" term "\x. f x" text "beta" term "(\x. x y) t" text \beta with renaming\ term "(\z. (\x. f x z)) x" text "definitions and unfold" definition c_0 :: "('a \ 'a) \ 'a \ 'a" where "c_0 \ \f x. x" definition c_1 :: "('a \ 'a) \ 'a \ 'a" where "c_1 \ \f x. f x" definition c_2 :: "('a \ 'a) \ 'a \ 'a" where "c_2 \ \f x. f (f x)" definition c_3 :: "('a \ 'a) \ 'a \ 'a" where "c_3 \ \f x. f (f (f x))" definition succ :: "(('a \ 'a) \ 'a \ 'a) \ ('a \ 'a) \ 'a \ 'a" where "succ \ \n f x. f (n f x)" definition add :: "(('a \ 'a) \ 'a \ 'a) \ (('a \ 'a) \ 'a \ 'a) \ ('a \ 'a) \ 'a \ 'a" where "add \ \m n f x. m f (n f x)" definition mult :: "(('a \ 'a) \ 'a \ 'a) \ (('a \ 'a) \ 'a \ 'a) \ ('a \ 'a) \ 'a \ 'a" where "mult \ \m n f x. m (n f) x" text "unfolding a definition" lemma "c_0 = (\f x. x)" apply (unfold c_0_def) apply (rule refl) done lemma "succ (succ c_0) = c_2" apply (unfold succ_def c_0_def c_2_def) apply (rule refl) done lemma "add c_2 c_2 = succ c_3" apply (unfold add_def succ_def c_3_def c_2_def) apply (rule refl) done lemma "add x c_0 = x" apply (unfold add_def c_0_def) apply (rule refl) done lemma "mult c_1 x = x" apply (unfold mult_def c_1_def) apply (rule refl) done end