Theory TM_Common

section ‹Preparations›

theory TM_Common
  imports 
    "HOL-Library.FuncSet"
begin

text ‹A direction of a TM: go right, go left, or neutral (stay)›
datatype dir = R | L | N

fun go_dir :: "dir ⇒ nat ⇒ nat" where
  "go_dir R n = Suc n" 
| "go_dir L n = n - 1" 
| "go_dir N n = n" 

lemma finite_UNIV_dir[simp, intro]: "finite (UNIV :: dir set)" 
proof -
  have id: "UNIV = {L,R,N}"
    using dir.exhaust by auto
  show ?thesis unfolding id by auto
qed

hide_const (open) L R N

lemma fin_funcsetI[intro]: "finite A ⟹ finite ((UNIV :: 'a :: finite set) → A)" 
  by (metis PiE_UNIV_domain finite_PiE finite_code)

lemma finite_UNIV_fun_dir[simp,intro]: "finite (UNIV :: ('k :: finite ⇒ dir) set)" 
  using fin_funcsetI[OF finite_UNIV_dir] by auto

lemma relpow_transI: "(x,y) ∈ R^^n ⟹ (y,z) ∈ R^^m ⟹ (x,z) ∈ R^^(n+m)"
  by (simp add: relcomp.intros relpow_add)

lemma relpow_mono: fixes R :: "'a rel" shows "R ⊆ S ⟹ R^^n ⊆ S^^n"
  by (induct n, auto)

lemma finite_infinite_inj_on: assumes A: "finite (A :: 'a set)" and inf: "infinite (UNIV :: 'b set)" 
  shows "∃ f :: 'a ⇒ 'b. inj_on f A"
proof -
  from inf obtain B :: "'b set" where B: "finite B" "card B = card A"
    by (meson infinite_arbitrarily_large)
  from A B obtain f :: "'a ⇒ 'b" where "bij_betw f A B"
    by (metis bij_betw_iff_card)
  thus ?thesis by (intro exI[of _ f], auto simp: bij_betw_def)
qed

lemma gauss_sum_nat2: "(∑i< (n :: nat). i) = (n - 1) * n div 2"
proof (cases n)
  case (Suc m)
  hence id: "{..<n} = {0..m}" by auto
  show ?thesis unfolding id unfolding gauss_sum_nat unfolding Suc by auto
qed auto

lemma aux_sum_formula: "(∑i<n. 10 + 5 * i) ≤ 3 * n^2 + 7 * (n :: nat)" 
proof -
  have "(∑i<n. 10 + 5 * i) = 10 * n + 5 * (∑i<n. i)" 
    by (subst sum.distrib, auto simp: sum_distrib_left)
  also have "… ≤ 10 * n + 3 * ((n - 1) * n)" 
    by (unfold gauss_sum_nat2, rule add_left_mono, cases n, auto)
  also have "… = 3 * n^2 + 7 * n" 
    unfolding power2_eq_square by (cases n, auto)
  finally show ?thesis .
qed

end