theory Trace_RG

lemma put_trace_eq_drop:
  "put_trace xs s
   = ((\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {.. length xs})" apply (induct xs) apply (clarsimp simp: return_def) apply (clarsimp simp: put_trace_elem_def bind_def) apply (simp add: atMost_Suc_eq_insert_0 image_image) apply (rule equalityI; clarsimp) apply (split if_split_asm; clarsimp) apply (auto intro: image_eqI[where x=0])[1] apply (rule rev_bexI, simp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs} proof (prove)
goal (2 subgoals):
 1. put_trace [] s = (\<lambda>n. (drop n [], if n = 0 then Result ((), s) else Incomplete)) ` {..length []}
 2. \<And>a xs. put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs} \<Longrightarrow> put_trace (a # xs) s = (\<lambda>n. (drop n (a # xs), if n = 0 then Result ((), s) else Incomplete)) ` {..length (a # xs)} proof (prove)
goal (1 subgoal):
 1. \<And>a xs. put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs} \<Longrightarrow> put_trace (a # xs) s = (\<lambda>n. (drop n (a # xs), if n = 0 then Result ((), s) else Incomplete)) ` {..length (a # xs)} proof (prove)
goal (1 subgoal):
 1. \<And>a b xs. put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs} \<Longrightarrow> (\<Union>x\<le>length xs. case if x = 0 then Result ((), s) else Incomplete of Failed \<Rightarrow> {(drop x xs, Failed)} | Incomplete \<Rightarrow> {(drop x xs, Incomplete)} | Result (rv, s) \<Rightarrow> {(drop x xs, Incomplete), ((a, b) # drop x xs, Result ((), s))}) = (\<lambda>x. (drop x ((a, b) # xs), if x = 0 then Result ((), s) else Incomplete)) ` {..Suc (length xs)} proof (prove)
goal (1 subgoal):
 1. \<And>a b xs. put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs} \<Longrightarrow> (\<Union>x\<le>length xs. case if x = 0 then Result ((), s) else Incomplete of Failed \<Rightarrow> {(drop x xs, Failed)} | Incomplete \<Rightarrow> {(drop x xs, Incomplete)} | Result (rv, s) \<Rightarrow> {(drop x xs, Incomplete), ((a, b) # drop x xs, Result ((), s))}) = insert ((a, b) # xs, Result ((), s)) ((\<lambda>x. (drop x xs, Incomplete)) ` {..length xs}) proof (prove)
goal (2 subgoals):
 1. \<And>a b xs aa ba x. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; (aa, ba) \<in> (case if x = 0 then Result ((), s) else Incomplete of Failed \<Rightarrow> {(drop x xs, Failed)} | Incomplete \<Rightarrow> {(drop x xs, Incomplete)} | Result (rv, s) \<Rightarrow> {(drop x xs, Incomplete), ((a, b) # drop x xs, Result ((), s))}); x \<le> length xs; (aa, ba) \<notin> (\<lambda>x. (drop x xs, Incomplete)) ` {..length xs}\<rbrakk> \<Longrightarrow> aa = (a, b) # xs \<and> ba = Result ((), s)
 2. \<And>xs x. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; x \<le> length xs\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{..length xs}. (xa = 0 \<longrightarrow> drop x xs = xs) \<and> (0 < xa \<longrightarrow> drop x xs = drop xa xs) proof (prove)
goal (2 subgoals):
 1. \<And>xs. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; (xs, Incomplete) \<notin> (\<lambda>x. (drop x xs, Incomplete)) ` {..length xs}\<rbrakk> \<Longrightarrow> False
 2. \<And>xs x. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; x \<le> length xs\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{..length xs}. (xa = 0 \<longrightarrow> drop x xs = xs) \<and> (0 < xa \<longrightarrow> drop x xs = drop xa xs) proof (prove)
goal (1 subgoal):
 1. \<And>xs x. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; x \<le> length xs\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{..length xs}. (xa = 0 \<longrightarrow> drop x xs = xs) \<and> (0 < xa \<longrightarrow> drop x xs = drop xa xs) proof (prove)
goal (1 subgoal):
 1. \<And>xs x. \<lbrakk>put_trace xs s = (\<lambda>n. (drop n xs, if n = 0 then Result ((), s) else Incomplete)) ` {..length xs}; x \<le> length xs\<rbrakk> \<Longrightarrow> (x = 0 \<longrightarrow> drop x xs = xs) \<and> (0 < x \<longrightarrow> drop x xs = drop x xs) proof (prove)
goal:
No subgoals!