# 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)"

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
```