theory Ex06_Template imports Small_Step begin inductive n_steps :: "com * state \ nat \ com * state \ bool" ("_ \^_ _" [60,1000,60]999) where zero_steps: "cs \^0 cs" | one_step: "cs \ cs' \ cs' \^n cs'' \ cs \^(Suc n) cs''" inductive_cases zero_stepsE[elim!]: "cs \^0 cs'" thm zero_stepsE inductive_cases one_stepE[elim!]: "cs \^(Suc n) cs''" thm one_stepE lemma small_steps_n: "cs \* cs' \ (\n. cs \^n cs')" oops lemma n_small_steps: "cs \^n cs' \ cs \* cs'" oops definition small_step_equiv :: "com \ com \ bool" (infix "\" 50) where "c \ c' == (\s t n. (c,s) \^n (SKIP, t) = (c', s) \^n (SKIP, t))" lemma small_eqv_implies_big_eqv: "c \ c' \ c \ c'" oops end