Theory SemiIdTM

(* Title: thys/SemiIdTM.thy
   Author: Franz Regensburger (FABR) 02/2022
 *)

section ‹SemiId: Turing machines acting as partial identity functions›

theory SemiIdTM
  imports Turing_Hoare
begin

(* Cleanup the global simpset *)

declare adjust.simps[simp del]

declare seq_tm.simps [simp del] 
declare shift.simps[simp del]
declare composable_tm.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]

subsection ‹The Turing Machine tm\_semi\_id\_eq0›

(* ---------------------------------------------------------- *)
(* Machine tm_semi_id_eq0                                     *)
(* ---------------------------------------------------------- *)
(*
The machine tm_semi_id_eq0
terminates on: Oc ↑ 1 with result Oc ↑ 1, which is the numeral <0>

     loops on: []      which is the empty input
     loops on: Oc ↑ n, where n ≥ 2
*)

text ‹
  If the input is @{term "Oc↑1"} the machine @{term "tm_semi_id_eq0"} will reach the
  final state in a standard configuration with output identical to its input.
  For other inputs @{term "Oc↑n"} with @{term "1 ≠ (n::nat)"} it will 
  loop forever.

  Please note that our short notation  @{term "<n::nat>"} means @{term "Oc↑(n+1)"}
  where @{term "0 ≤ (n::nat)"}.
›

definition tm_semi_id_eq0 :: "instr list"
  where
    "tm_semi_id_eq0 ≡ [(WB, 1), (R, 2), (L, 0), (L, 1)]"

(* ------ Important properties used in subsequent theories ------ *)

lemma composable_tm0_tm_semi_id_eq0[intro, simp]: "composable_tm0 tm_semi_id_eq0"
  by (auto simp: composable_tm.simps tm_semi_id_eq0_def)

lemma tm_semi_id_eq0_loops_aux: 
  "(steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 stp = (1, [], [Oc, Oc])) ∨ 
   (steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 stp = (2, Oc # [], [Oc]))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_eq0_def numeral_eqs_upto_12)

lemma tm_semi_id_eq0_loops_aux': 
  "(steps0 (1, [], [Oc, Oc] @ (Bk ↑ q)) tm_semi_id_eq0 stp = (1, [], [Oc,Oc] @ Bk ↑ q)) ∨ 
   (steps0 (1, [], [Oc, Oc] @ (Bk ↑ q)) tm_semi_id_eq0 stp = (2, Oc # [], [Oc] @ (Bk ↑ q)))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_eq0_def numeral_eqs_upto_12)

lemma tm_semi_id_eq0_loops_aux'': 
  "(steps0 (1, [], [Oc, Oc] @ (Oc ↑ q) @ (Bk ↑ q)) tm_semi_id_eq0 stp = (1, [], [Oc,Oc] @ (Oc ↑ q) @ Bk ↑ q)) ∨ 
   (steps0 (1, [], [Oc, Oc] @ (Oc ↑ q) @ (Bk ↑ q)) tm_semi_id_eq0 stp = (2, Oc # [], [Oc] @ (Oc ↑ q) @ (Bk ↑ q)))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_eq0_def numeral_eqs_upto_12)

lemma tm_semi_id_eq0_loops_aux''': 
  "(steps0 (1, [], []) tm_semi_id_eq0 stp = (1, [], [])) ∨ 
   (steps0 (1, [], []) tm_semi_id_eq0 stp = (1, [], [Bk]))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_eq0_def numeral_eqs_upto_12)

(* ------ Auxiliary properties for clarification           ------ *)

lemma "<0::nat> = [Oc]" by (simp add: tape_of_nat_def)
lemma "Oc↑(0+1) = [Oc]" by (simp)
lemma "<n::nat> = Oc↑(n+1)" by (auto simp add: tape_of_nat_def)
lemma "<1::nat> = [Oc, Oc]" by (simp add: tape_of_nat_def)

subsubsection ‹The machine tm\_semi\_id\_eq0 in action›

(* steps0 (1, [], []) tm_semi_id_eq0 n loops forever in state 1 *)
lemma "steps0 (1, [], []) tm_semi_id_eq0 0 = (1, [], [])"   by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], []) tm_semi_id_eq0 1 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], []) tm_semi_id_eq0 2 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], []) tm_semi_id_eq0 3 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)

(*     steps0 (1, [], [Oc]) tm_semi_id_eq0 n terminates after 2 steps with final configuration "(0, [], [Oc])" *)
lemma "steps0 (1, [], [Oc]) tm_semi_id_eq0 0 = (1, [], [Oc])" by (simp add: step.simps steps.simps tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_eq0 1 = (2, [Oc], [])" by (simp add: step.simps steps.simps tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_eq0 2 = (0, [], [Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)

(* steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 loops forever *)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 0 = (1, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 1 = (2, [Oc], [Oc])"   by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 2 = (1, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 3 = (2, [Oc], [Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_eq0 4 = (1, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_eq0_def)

subsection ‹The Turing Machine tm\_semi\_id\_gt0›

(* ---------------------------------------------------------- *)
(* Machine tm_semi_id_gt0                                     *)
(* ---------------------------------------------------------- *)
(*
The machine tm_semi_id_gt0 (aka dither) has behaviour that is complementary
to the behaviour of tm_semi_id_eq0.

The machine tm_semi_id_gt0
terminates on: Oc ↑ n  with result Oc ↑ n for 1 < n

     loops on: []     , which is the empty input
     loops on: Oc ↑ 1 , which is the numeral <0>
*)

text ‹
  If the input is @{term "Oc↑0"} or @{term "Oc↑1"} the machine @{term "tm_semi_id_gt0"}
  (aka dither) will loop forever.
  For other non-blank inputs @{term "Oc↑n"} with @{term  "1 < (n::nat)"} it will 
  reach the final state in a standard configuration with output identical to its input.

  Please note that our short notation  @{term "<n::nat>"} means @{term "Oc↑(n+1)"}
  where @{term "0 ≤ (n::nat)"}.
›

definition tm_semi_id_gt0 :: "instr list"
  where
    "tm_semi_id_gt0 ≡ [(WB, 1), (R, 2), (L, 1), (L, 0)]"

(* ------ Important properties used in subsequent theories ------ *)

lemma tm_semi_id_gt0[intro, simp]: "composable_tm0 tm_semi_id_gt0"
  by (auto simp: composable_tm.simps tm_semi_id_gt0_def)

lemma tm_semi_id_gt0_loops_aux: 
  "(steps0 (1, [], [Oc]) tm_semi_id_gt0 stp = (1, [], [Oc])) ∨ 
   (steps0 (1, [], [Oc]) tm_semi_id_gt0 stp = (2, Oc # [], []))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_gt0_def numeral_eqs_upto_12)

lemma tm_semi_id_gt0_loops_aux': 
  "(steps0 (1, [], [Oc] @ Bk ↑ n) tm_semi_id_gt0 stp = (1, [], [Oc] @ Bk ↑ n)) ∨ 
   (steps0 (1, [], [Oc] @ Bk ↑ n) tm_semi_id_gt0 stp = (2, Oc # [], Bk ↑ n))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_gt0_def numeral_eqs_upto_12)

lemma tm_semi_id_gt0_loops_aux''': 
  "(steps0 (1, [], []) tm_semi_id_gt0 stp = (1, [], [])) ∨ 
   (steps0 (1, [], []) tm_semi_id_gt0 stp = (1, [], [Bk]))"
  by (induct stp) (auto simp: steps.simps step.simps tm_semi_id_gt0_def numeral_eqs_upto_12)

subsubsection ‹The machine tm\_semi\_id\_gt0 in action›

(* steps0 (1, [], []) tm_semi_id_gt0 n loops forever in state 1 *)
lemma "steps0 (1, [], []) tm_semi_id_gt0 0 = (1, [], [])"   by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], []) tm_semi_id_gt0 1 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], []) tm_semi_id_gt0 2 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], []) tm_semi_id_gt0 3 = (1, [], [Bk])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)

(* steps0 (1, [], [Oc]) tm_semi_id_gt0 n loops forever; it dithers between states 1 and 2 *)
lemma "steps0 (1, [], [Oc]) tm_semi_id_gt0 0 = (1, [], [Oc])" by (simp add: step.simps steps.simps tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_gt0 1 = (2, [Oc], [])" by (simp add: step.simps steps.simps tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_gt0 2 = (1, [], [Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_gt0 3 = (2, [Oc], [])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc]) tm_semi_id_gt0 4 = (1, [], [Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)

(* steps0 (1, [], [Oc, Oc]) tm_semi_id_gt0 n terminates after 2 steps with final configuration "(0, [], [Oc, Oc])" *)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_gt0 0 = (1, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_gt0 1 = (2, [Oc], [Oc])"   by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_gt0 2 = (0, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)
lemma "steps0 (1, [], [Oc, Oc]) tm_semi_id_gt0 3 = (0, [], [Oc, Oc])" by (simp add: step.simps steps.simps numeral_eqs_upto_12 tm_semi_id_gt0_def)


subsection ‹Properties of the SemiId machines›

(*
declare adjust.simps[simp del]

declare seq_tm.simps [simp del] 
declare shift.simps[simp del]
declare composable_tm.simps[simp del]
declare step.simps[simp del]
declare steps.simps[simp del]
*)

text ‹Using Hoare style rules is more elegant since they allow for compositional
 reasoning. Therefore, its preferable to use them, if the program that we reason about
 can be decomposed appropriately.›

subsubsection ‹Proving properties of tm\_semi\_id\_eq0 with Hoare Rules›

lemma tm_semi_id_eq0_loops_Nil:
  shows "⦃λtap. tap = ([], [])⦄ tm_semi_id_eq0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_eq0_loops_aux'''
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_eq0_loops:
  shows "⦃λtap. tap = ([], <1::nat>)⦄ tm_semi_id_eq0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_eq0_loops_aux
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_eq0_loops':
  shows "⦃λtap. ∃l. tap = ([], [Oc, Oc] @ Bk↑ l)⦄ tm_semi_id_eq0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_eq0_loops_aux'
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def )
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_eq0_loops'':
  shows "⦃λtap. ∃k l. tap = (Bk↑k, [Oc, Oc] @ Bk↑ l)⦄ tm_semi_id_eq0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_eq0_loops_aux'
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis is_final_del_Bks Zero_neq_Suc is_final_eq)



lemma tm_semi_id_eq0_halts_aux:
  shows "steps0 (1, Bk ↑ m, [Oc]) tm_semi_id_eq0 2 = (0, Bk ↑ m, [Oc])"
  unfolding tm_semi_id_eq0_def
  by (simp add: steps.simps step.simps numeral_eqs_upto_12)

lemma tm_semi_id_eq0_halts_aux':
  shows "steps0 (1, Bk ↑ m, [Oc]@Bk ↑ n) tm_semi_id_eq0 2 = (0, Bk ↑ m, [Oc]@Bk ↑ n)"
  unfolding tm_semi_id_eq0_def
  by (simp add: steps.simps step.simps numeral_eqs_upto_12)

lemma tm_semi_id_eq0_halts:
  shows "⦃λtap. tap = ([], <0::nat>)⦄ tm_semi_id_eq0 ⦃λtap. tap = ([], <0::nat>)⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_eq0_halts_aux
  apply(auto simp add: tape_of_nat_def)
  by (metis (full_types) holds_for.simps is_finalI  replicate_0)

lemma tm_semi_id_eq0_halts':
  shows "⦃λtap. ∃l. tap = ([], [Oc] @ Bk↑ l)⦄ tm_semi_id_eq0 ⦃λtap. ∃l. tap = ([], [Oc] @ Bk↑ l)⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_eq0_halts_aux'
  apply(auto simp add: tape_of_nat_def)
  by (metis (mono_tags, lifting) holds_for.simps is_finalI numeral_1_eq_Suc_0 numeral_One replicate_0)

lemma tm_semi_id_eq0_halts'':
  shows "⦃ λtap. ∃k l. tap = (Bk↑ k, [Oc] @ Bk↑ l) ⦄ tm_semi_id_eq0 ⦃ λtap. ∃k l. tap = (Bk↑ k, [Oc] @ Bk↑ l) ⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_eq0_halts_aux'
  apply(auto simp add: tape_of_nat_def)
  by (metis (mono_tags, lifting) holds_for.simps is_finalI numeral_1_eq_Suc_0 numeral_One)

subsubsection ‹Proving properties of tm\_semi\_id\_gt0 with Hoare Rules›

lemma tm_semi_id_gt0_loops_Nil:
  shows "⦃λtap. tap = ([], [])⦄ tm_semi_id_gt0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_gt0_loops_aux'''
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_gt0_loops:
  shows "⦃λtap. tap = ([], <0::nat>)⦄ tm_semi_id_gt0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_gt0_loops_aux
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_gt0_loops':
  shows "⦃λtap. ∃l. tap = ([], [Oc] @ Bk↑ l)⦄ tm_semi_id_gt0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_gt0_loops_aux'
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis Suc_neq_Zero is_final_eq)

lemma tm_semi_id_gt0_loops'':
  shows "⦃λtap. ∃k l. tap = (Bk↑k, [Oc] @ Bk↑ l)⦄ tm_semi_id_gt0 ↑"
  apply(rule Hoare_unhaltI)
  using tm_semi_id_gt0_loops_aux'
  apply(auto simp add: numeral_eqs_upto_12 tape_of_nat_def)
  by (metis is_final_del_Bks Zero_neq_Suc is_final_eq)

lemma tm_semi_id_gt0_halts_aux:
  shows "steps0 (1, Bk ↑ m, [Oc, Oc]) tm_semi_id_gt0 2 = (0, Bk ↑ m, [Oc, Oc])"
  unfolding tm_semi_id_gt0_def
  by (simp add: steps.simps step.simps numeral_eqs_upto_12)

lemma tm_semi_id_gt0_halts_aux':
  shows "steps0 (1, Bk ↑ m, [Oc, Oc]@Bk ↑ n) tm_semi_id_gt0 2 = (0, Bk ↑ m, [Oc, Oc]@Bk ↑ n)"
  unfolding tm_semi_id_gt0_def
  by (simp add: steps.simps step.simps numeral_eqs_upto_12)

lemma tm_semi_id_gt0_halts:
  shows "⦃λtap. tap = ([], <1::nat>)⦄ tm_semi_id_gt0 ⦃λtap. tap = ([], <1::nat>)⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_gt0_halts_aux
  apply(auto simp add: tape_of_nat_def)
  by (metis (full_types) empty_replicate holds_for.simps is_final_eq numeral_2_eq_2)

lemma tm_semi_id_gt0_halts':
  shows "⦃λtap. ∃l. tap = ([], [Oc, Oc] @ Bk↑ l)⦄ tm_semi_id_gt0 ⦃λtap. ∃l. tap = ([], [Oc, Oc] @ Bk↑ l)⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_gt0_halts_aux'
  apply(auto simp add: tape_of_nat_def)
  by (metis (mono_tags, lifting) Suc_1 holds_for.simps is_finalI numeral_1_eq_Suc_0 numeral_One replicate_0)

lemma tm_semi_id_gt0_halts'':
  shows "⦃ λtap. ∃k l. tap = (Bk↑ k, [Oc, Oc] @ Bk↑ l)⦄ tm_semi_id_gt0 ⦃λtap. ∃k l. tap = (Bk↑ k, [Oc, Oc] @ Bk↑ l)⦄"
  apply(rule Hoare_haltI)
  using tm_semi_id_gt0_halts_aux'
  apply(auto simp add: tape_of_nat_def)
  by (metis (mono_tags, lifting) Suc_1 holds_for.simps is_finalI numeral_1_eq_Suc_0 numeral_One)

end