theory Trace_RG

lemma trace_steps_nth:
  "trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), (if i = 0 then s0 else snd (xs ! (i - 1))), snd (xs ! i))) ` {..< length xs}" proof (induct xs arbitrary: s0) case Nil show ?case by simp next case (Cons a xs) show ?case apply (simp add: lessThan_Suc_eq_insert_0 Cons image_image nth_Cons') apply (intro arg_cong2[where f=insert] refl image_cong) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs} proof (state)
goal (2 subgoals):
 1. \<And>s0. trace_steps [] s0 = (\<lambda>i. (fst ([] ! i), if i = 0 then s0 else snd ([] ! (i - 1)), snd ([] ! i))) ` {..<length []}
 2. \<And>a xs s0. (\<And>s0. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) \<Longrightarrow> trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (state)
this:


goal (2 subgoals):
 1. \<And>s0. trace_steps [] s0 = (\<lambda>i. (fst ([] ! i), if i = 0 then s0 else snd ([] ! (i - 1)), snd ([] ! i))) ` {..<length []}
 2. \<And>a xs s0. (\<And>s0. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) \<Longrightarrow> trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (prove)
goal (1 subgoal):
 1. trace_steps [] s0 = (\<lambda>i. (fst ([] ! i), if i = 0 then s0 else snd ([] ! (i - 1)), snd ([] ! i))) ` {..<length []} proof (state)
this:
trace_steps [] s0 = (\<lambda>i. (fst ([] ! i), if i = 0 then s0 else snd ([] ! (i - 1)), snd ([] ! i))) ` {..<length []}

goal (1 subgoal):
 1. \<And>a xs s0. (\<And>s0. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) \<Longrightarrow> trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (state)
goal (1 subgoal):
 1. \<And>a xs s0. (\<And>s0. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) \<Longrightarrow> trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (state)
this:
trace_steps xs ?s0.0 = (\<lambda>i. (fst (xs ! i), if i = 0 then ?s0.0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}

goal (1 subgoal):
 1. \<And>a xs s0. (\<And>s0. trace_steps xs s0 = (\<lambda>i. (fst (xs ! i), if i = 0 then s0 else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) \<Longrightarrow> trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (prove)
goal (1 subgoal):
 1. trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)} proof (prove)
goal (1 subgoal):
 1. insert (fst a, s0, snd a) ((\<lambda>i. (fst (xs ! i), if i = 0 then snd a else snd (xs ! (i - 1)), snd (xs ! i))) ` {..<length xs}) = insert (fst a, s0, snd a) ((\<lambda>x. (fst (xs ! x), snd (if x = 0 then a else xs ! (x - 1)), snd (xs ! x))) ` {..<length xs}) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<length xs} \<Longrightarrow> (fst (xs ! x), if x = 0 then snd a else snd (xs ! (x - 1)), snd (xs ! x)) = (fst (xs ! x), snd (if x = 0 then a else xs ! (x - 1)), snd (xs ! x)) proof (prove)
goal:
No subgoals! proof (state)
this:
trace_steps (a # xs) s0 = (\<lambda>i. (fst ((a # xs) ! i), if i = 0 then s0 else snd ((a # xs) ! (i - 1)), snd ((a # xs) ! i))) ` {..<length (a # xs)}

goal:
No subgoals!