# Theory Three_Steps

theory Three_Steps
imports "../Consensus_Misc"
begin
subsection ‹Step definitions for 3-step algorithms›
abbreviation (input) "nr_steps ≡ 3"
definition three_phase where "three_phase (r::nat) ≡ r div nr_steps"
definition three_step where "three_step (r::nat) ≡ r mod nr_steps"
lemma three_phase_zero [simp]: "three_phase 0 = 0"
by (simp add: three_phase_def)
lemma three_step_zero [simp]: "three_step 0 = 0"
by (simp add: three_step_def)
lemma three_phase_step: "(three_phase r * nr_steps) + three_step r = r"
by (auto simp add: three_phase_def three_step_def)
lemma three_step_Suc:
"three_step r = 0 ⟹ three_step (Suc (Suc r)) = 2"
"three_step r = 0 ⟹ three_step (Suc r) = 1"
"three_step r = (Suc 0) ⟹ three_step (Suc r) = 2"
"three_step r = (Suc 0) ⟹ three_step (Suc (Suc r)) = 0"
"three_step r = (Suc (Suc 0)) ⟹ three_step ((Suc r)) = 0"
by(unfold three_step_def, simp_all add: mod_Suc)
lemma three_step_phase_Suc:
"three_step r = 0 ⟹ three_phase (Suc r) = three_phase r"
"three_step r = 0 ⟹ three_phase (Suc (Suc r)) = three_phase r"
"three_step r = 0 ⟹ three_phase (Suc (Suc (Suc r))) = Suc (three_phase r)"
"three_step r = (Suc 0) ⟹ three_phase (Suc r) = three_phase r"
"three_step r = (Suc 0) ⟹ three_phase (Suc (Suc r)) = Suc (three_phase r)"
"three_step r = (Suc (Suc 0)) ⟹ three_phase (Suc r) = Suc (three_phase r)"
by(simp_all add: three_step_def three_phase_def mod_Suc div_Suc)
lemma three_step2_phase_Suc:
"three_step r = 2 ⟹ (3 * (Suc (three_phase r)) - 1) = r"
apply(simp add: three_step_def three_phase_def)
by (metis add_2_eq_Suc' mult_div_mod_eq)
lemma three_stepE:
"⟦ three_step r = 0 ⟹ P; three_step r = 1 ⟹ P; three_step r = 2 ⟹ P ⟧ ⟹ P"
by(unfold three_step_def, arith)
end