theory Functor
imports Main
begin

constdefs
  const :: "'a => 'b => 'a"
  "const x y == x"

theorem comp_id [simp]: "comp id == id"
proof -
  have "comp id == %g x. (id o g) x" .
  also have "... == %g x. id (g x)" by simp
  also have "... == %g x. g x" by simp
  also have "... == id" by (simp only: id_def)
  finally show "comp id == id" .
qed

theorem comp_comp [simp]: "comp (f o g) == (comp f) o (comp g)"
proof -
  have "comp (f o g) == %h y. ((f o g) o h) y" .
  also have "... == %h y. (f o g o h) y" by simp
  also have "... == %h y. ((comp f) ((comp g) h)) y" by simp
  also have "... == %h y. ((comp f) o (comp g)) h y" by simp
  finally show "comp (comp f g) == comp (comp f) (comp g)" .
qed

constdefs
  rpipe2 :: "['b => 'c, 'a => 'a1 => 'b, 'a, 'a1] => 'c"
  "rpipe2 == comp o comp"
  rpipe3 :: "['b => 'c, 'a => 'a1 => 'a2 => 'b, 'a, 'a1, 'a2] => 'c"
  "rpipe3 == rpipe2 o comp"
  apBoth :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
  "apBoth f g x == (f x, g x)"
  tt :: "['c => 'a => 'b, 'c => 'a, 'c] => 'b"
  "tt == rpipe3 (split id) apBoth"

lemma rpipe3_simp [simp]: "rpipe3 f g x y z == f (g x y z)"
proof -
  have "rpipe3 f g x y z == (rpipe2 o comp) f g x y z" by (unfold rpipe3_def)
  also have "... == ((comp o comp) o comp) f g x y z" by (unfold rpipe2_def)
  also have "... == (comp (comp (comp f))) g x y z" by simp
  also have "... == f (g x y z)" by simp
  finally show "rpipe3 f g x y z == f (g x y z)" .
qed

lemma tt_simp [simp]: "tt f g x == f x (g x)"
proof -
  have "tt f g x == rpipe3 (split id) apBoth f g x" by (unfold tt_def)
  also have "... == split id (apBoth f g x)" by simp
  also have "... == split id (f x, g x)" by (unfold apBoth_def)
  also have "... == f x (g x)" by simp
  finally show "tt f g x == f x (g x)" .
qed

theorem tt_o_const [simp]: "tt o const == comp"
proof -
  have "tt o const == %f g x. (tt o const) f g x" .
  also have "... == %f g x. tt (const f) g x" by simp
  also have "... == %f g x. (const f) x (g x)" by simp
  also have "... == %f g x. f (g x)" by (unfold const_def)
  also have "... == %f g. comp f g" by (unfold o_def)
  finally show "tt o const == comp" .
qed

theorem "tt (const id) == id"
proof -
  have "tt (const id) == (tt o const) id" by (unfold o_def)
  also have "... == comp id" by simp
  also have "... == id" by simp
  finally show "tt (const id) == id" .
qed

theorem "tt (tt (comp comp u) v) w == tt u (tt v w)"
proof -
  have "tt (tt (comp comp u) v) w == tt (tt (comp o u) v) w" .
  also have "... == tt (tt (%x. comp (u x)) v) w" by (unfold o_def)
  also have "... == tt (%y. (%x. comp (u x)) y (v y)) w" .