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





(*siehe  lemma small_steps_trans[trans]*)
lemma small_steps_n: "cs ->* cs' ==> (\<exists>n. cs ->^n cs')"
proof(induct rule: small_steps.induct)
  case refl thus ?case by (metis zero_steps)
  case step thus ?case by (metis one_step)
qed  


lemma steps_trans[simp]: "[| cs ->* cs'; cs' ->* cs'' |] ==> cs ->* cs''"
apply(induct rule: small_steps.induct)
apply assumption
apply(rule step)
apply assumption
apply assumption
done

lemma steps_if_step[simp]: "cs -> cs' ==> cs ->* cs'"
by(rule step[OF _ refl])


lemma n_small_steps: "cs ->^n cs' ==> cs ->* cs'"
apply(rule step)apply(auto) 
sorry



definition
  small_step_equiv :: "com => com => bool" (infix "\<approx>" 50) where
  "c \<approx> c' == (\<forall>s t n. (c,s) ->^n (SKIP, t)  =  (c', s) ->^n (SKIP, t))"

lemma small_eqv_implies_big_eqv: assumes "c \<approx> c'" shows "c \<sim> c'"
proof-
  have x:"c' \<approx> c" using assms unfolding small_step_equiv_def by auto
  { fix c c' s t assume as:"c \<approx> c'" "(c, s) => t"
    hence "(c, s) ->* (SKIP, t)" using as unfolding big_iff_small by auto
    note small_steps_n[OF this] then guess n .. 
    hence "(c', s) ->^n (SKIP, t)" using as(1)[unfolded small_step_equiv_def] 
      by auto
    hence "(c', s) => t" apply-apply(drule n_small_steps)
      unfolding big_iff_small .
  }
  thus ?thesis using assms x by auto
qed

end