Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-30 00:43 913f702a

View on Github →

feat(computability/turing_machine): rework proofs, simplify TM lang

Estimated changes

Modified algebra/group_power.lean

Modified computability/turing_machine.lean

modified def turing.TM0.eval

added def turing.TM0.init

modified def turing.TM1.eval

added def turing.TM1.init

deleted def turing.TM1.reaches

added def turing.TM1.step_aux

deleted def turing.TM1to0.tr'

modified def turing.TM1to0.tr

added def turing.TM1to0.tr_aux

modified def turing.TM1to0.tr_cfg

added theorem turing.TM1to0.tr_eval

deleted theorem turing.TM1to0.tr_reaches

added theorem turing.TM1to0.tr_respects

modified theorem turing.TM1to0.tr_supports

modified def turing.TM1to0.Λ'

modified def turing.TM2.eval

added def turing.TM2.init

deleted theorem turing.TM2.move_until_left_reaches₁

deleted theorem turing.TM2.move_until_right_reaches₁

deleted def turing.TM2.reaches₁

deleted theorem turing.TM2.reaches₁_step

added inductive turing.TM2to1.st_act

added def turing.TM2to1.st_run

added def turing.TM2to1.st_var

added def turing.TM2to1.st_write

added def turing.TM2to1.stackel.get

added def turing.TM2to1.stackel.is_bottom

added def turing.TM2to1.stackel.is_top

added inductive turing.TM2to1.stackel

added def turing.TM2to1.stackel_equiv

added theorem turing.TM2to1.step_run

added theorem turing.TM2to1.supports_run

deleted def turing.TM2to1.tr'

added inductive turing.TM2to1.tr_cfg

deleted def turing.TM2to1.tr_cfg

added theorem turing.TM2to1.tr_cfg_init

added theorem turing.TM2to1.tr_eval

added theorem turing.TM2to1.tr_eval_dom

added def turing.TM2to1.tr_init

added def turing.TM2to1.tr_normal

added theorem turing.TM2to1.tr_normal_run

deleted theorem turing.TM2to1.tr_reaches

added theorem turing.TM2to1.tr_respects

added theorem turing.TM2to1.tr_respects_aux

added theorem turing.TM2to1.tr_respects_aux₁

added theorem turing.TM2to1.tr_respects_aux₂

added theorem turing.TM2to1.tr_respects_aux₃

added def turing.TM2to1.tr_st_act

added def turing.TM2to1.tr_stk

added theorem turing.TM2to1.tr_stmts₁_run

added theorem turing.TM2to1.{l}

added def turing.TM2to1.Γ'

added inductive turing.TM2to1.Λ'

deleted def turing.TM2to1.Λ'

added def turing.TM2to1.Λ'_inh

deleted structure turing.TM3.cfg

deleted def turing.TM3.eval

deleted def turing.TM3.reaches

deleted def turing.TM3.step

deleted def turing.TM3.step_aux

deleted theorem turing.TM3.step_supports

deleted inductive turing.TM3.stmt

deleted theorem turing.TM3.stmts_supports_stmt

deleted theorem turing.TM3.stmts_trans

deleted theorem turing.TM3.stmts₁_self

deleted theorem turing.TM3.stmts₁_supports_stmt_mono

deleted theorem turing.TM3.stmts₁_trans

deleted def turing.TM3.supports

deleted def turing.TM3.supports_stmt

deleted def turing.TM3to2.at_stack

deleted def turing.TM3to2.stackel.get

deleted def turing.TM3to2.stackel.is_bottom

deleted def turing.TM3to2.stackel.is_top

deleted inductive turing.TM3to2.stackel

deleted def turing.TM3to2.stackel_equiv

deleted def turing.TM3to2.tr

deleted inductive turing.TM3to2.tr_cfg

deleted theorem turing.TM3to2.tr_reaches

deleted def turing.TM3to2.tr_stk

deleted theorem turing.TM3to2.tr_supports

deleted def turing.TM3to2.Γ'

deleted def turing.TM3to2.Λ'

deleted def turing.dir.rev

added theorem turing.eval_maximal

added theorem turing.eval_maximal₁

added def turing.frespects

added theorem turing.frespects_eq

added theorem turing.fun_respects

added theorem turing.mem_eval

added def turing.reaches

added theorem turing.reaches_eval

added theorem turing.reaches_total

added def turing.reaches₁

added theorem turing.reaches₁_eq

added def turing.respects

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₁

Modified data/fintype.lean

added def finset.insert_none

added theorem finset.mem_insert_none

added theorem finset.some_mem_insert_none

Modified data/list/basic.lean

added theorem list.map_repeat

added theorem list.map_reverse_core

added theorem list.map_tail

modified theorem list.repeat_add

added theorem list.repeat_succ

added theorem list.reverse_core_eq

added theorem list.tail_repeat

Modified data/option.lean

added theorem option.eq_none_iff_forall_not_mem

added theorem option.mem_unique

Modified data/pfun.lean

modified theorem pfun.fix_induction

Modified logic/relation.lean

added theorem relation.refl_trans_gen.total_of_right_unique