Commit 2025-02-10 11:41 88b0d633

View on Github →

Chore: split TuringMachine.lean into smaller files (#21623) A rather minimal change, just splitting the files and mentioning that in the introductions. Since TuringMachine imports PostTuringMachine, any file that imported TuringMachine before can still do so.

Estimated changes

added def Turing.FRespects
added theorem Turing.Reaches.to₀
added def Turing.Reaches
added theorem Turing.Reaches₀.head
added theorem Turing.Reaches₀.refl
added theorem Turing.Reaches₀.tail
added def Turing.Respects
added structure Turing.TM0.Cfg
added inductive Turing.TM0.Stmt
added def Turing.TM0.eval
added def Turing.TM0.init
added theorem Turing.TM0.map_init
added def Turing.TM0.step
added def Turing.TM0to1.tr
added inductive Turing.TM0to1.Λ'
added structure Turing.TM1.Cfg
added inductive Turing.TM1.Stmt
added def Turing.TM1.eval
added def Turing.TM1.init
added def Turing.TM1.step
added theorem Turing.TM1.stmts_trans
added def Turing.TM1to0.tr
added theorem Turing.TM1to0.tr_eval
added def Turing.TM1to1.tr
added inductive Turing.TM1to1.Λ'
added def Turing.eval
added theorem Turing.eval_maximal
added theorem Turing.eval_maximal₁
added theorem Turing.frespects_eq
added theorem Turing.fun_respects
added theorem Turing.mem_eval
added theorem Turing.reaches_eval
added theorem Turing.reaches_total
added theorem Turing.reaches₀_eq
added theorem Turing.reaches₁_eq
added theorem Turing.reaches₁_fwd
added theorem Turing.tr_eval'
added theorem Turing.tr_eval
added theorem Turing.tr_eval_dom
added theorem Turing.tr_eval_rev
added theorem Turing.tr_reaches
added theorem Turing.tr_reaches_rev
added theorem Turing.tr_reaches₁
deleted def Turing.FRespects
deleted theorem Turing.Reaches.to₀
deleted def Turing.Reaches
deleted theorem Turing.Reaches₀.head
deleted theorem Turing.Reaches₀.refl
deleted theorem Turing.Reaches₀.single
deleted theorem Turing.Reaches₀.tail'
deleted theorem Turing.Reaches₀.tail
deleted theorem Turing.Reaches₀.trans
deleted def Turing.Reaches₀
deleted theorem Turing.Reaches₁.to₀
deleted def Turing.Reaches₁
deleted def Turing.Respects
deleted def Turing.TM0.Cfg.map
deleted structure Turing.TM0.Cfg
deleted def Turing.TM0.Machine
deleted def Turing.TM0.Reaches
deleted def Turing.TM0.Stmt.map
deleted inductive Turing.TM0.Stmt
deleted def Turing.TM0.Supports
deleted def Turing.TM0.eval
deleted def Turing.TM0.init
deleted theorem Turing.TM0.map_init
deleted def Turing.TM0.step
deleted theorem Turing.TM0.step_supports
deleted theorem Turing.TM0.univ_supports
deleted def Turing.TM0to1.tr
deleted def Turing.TM0to1.trCfg
deleted theorem Turing.TM0to1.tr_respects
deleted inductive Turing.TM0to1.Λ'
deleted structure Turing.TM1.Cfg
deleted inductive Turing.TM1.Stmt
deleted def Turing.TM1.Supports
deleted def Turing.TM1.eval
deleted def Turing.TM1.init
deleted def Turing.TM1.step
deleted def Turing.TM1.stepAux
deleted theorem Turing.TM1.step_supports
deleted theorem Turing.TM1.stmts_trans
deleted theorem Turing.TM1.stmts₁_self
deleted theorem Turing.TM1.stmts₁_trans
deleted def Turing.TM1to0.tr
deleted def Turing.TM1to0.trAux
deleted def Turing.TM1to0.trCfg
deleted theorem Turing.TM1to0.tr_eval
deleted theorem Turing.TM1to0.tr_respects
deleted theorem Turing.TM1to0.tr_supports
deleted def Turing.TM1to0.Λ'
deleted def Turing.TM1to1.move
deleted def Turing.TM1to1.read
deleted def Turing.TM1to1.tr
deleted def Turing.TM1to1.trCfg
deleted theorem Turing.TM1to1.trTape_mk'
deleted theorem Turing.TM1to1.tr_respects
deleted theorem Turing.TM1to1.tr_supports
deleted def Turing.TM1to1.write
deleted inductive Turing.TM1to1.Λ'
deleted def Turing.eval
deleted theorem Turing.eval_maximal
deleted theorem Turing.eval_maximal₁
deleted theorem Turing.frespects_eq
deleted theorem Turing.fun_respects
deleted theorem Turing.mem_eval
deleted theorem Turing.reaches_eval
deleted theorem Turing.reaches_total
deleted theorem Turing.reaches₀_eq
deleted theorem Turing.reaches₁_eq
deleted theorem Turing.reaches₁_fwd
deleted theorem Turing.tr_eval'
deleted theorem Turing.tr_eval
deleted theorem Turing.tr_eval_dom
deleted theorem Turing.tr_eval_rev
deleted theorem Turing.tr_reaches
deleted theorem Turing.tr_reaches_rev
deleted theorem Turing.tr_reaches₁