theory Trace_RG

lemma Await_redef:
  "Await P = do
     s1 \<leftarrow> select {s. P s};
     env_steps;
     s \<leftarrow> get;
     select (if P s then {()} else {})
   od" apply (simp add: Await_def env_steps_def bind_assoc) apply (cases "{s. P s} = {}") apply (simp add: select_def bind_def get_def) apply (rule ext) apply (simp add: exec_get select_bind_UN put_then_get_then) apply (simp add: bind_promote_If2 if_distribR if_distrib[where f=select]) apply (simp add: exec_put_trace cong: if_cong) apply (simp add: put_def bind_def select_def cong: if_cong) apply (strengthen equalityI) apply clarsimp apply (strengthen exI[where x="s # xs" for s xs]) apply (strengthen exI[where x="Suc n" for n]) apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Await P = do s1 <- select {s. P s};
env_steps;
s <- get;
select (if P s then {()} else {})
od proof (prove)
goal (1 subgoal):
 1. do s <- get;
xs <- select {xs. P (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = do s1 <- select {s. P s};
x <- get;
xa <- select UNIV;
xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
s <- get;
select (if P s then {()} else {})
od proof (prove)
goal (2 subgoals):
 1. {s. P s} = {} \<Longrightarrow> do s <- get;
xs <- select {xs. P (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = do s1 <- select {s. P s};
x <- get;
xa <- select UNIV;
xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
s <- get;
select (if P s then {()} else {})
od
 2. {s. P s} \<noteq> {} \<Longrightarrow> do s <- get;
xs <- select {xs. P (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = do s1 <- select {s. P s};
x <- get;
xa <- select UNIV;
xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
s <- get;
select (if P s then {()} else {})
od proof (prove)
goal (1 subgoal):
 1. {s. P s} \<noteq> {} \<Longrightarrow> do s <- get;
xs <- select {xs. P (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od = do s1 <- select {s. P s};
x <- get;
xa <- select UNIV;
xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
s <- get;
select (if P s then {()} else {})
od proof (prove)
goal (1 subgoal):
 1. \<And>x. {s. P s} \<noteq> {} \<Longrightarrow> (do s <- get;
xs <- select {xs. P (last_st_tr (map (Pair Env) xs) s)};
y <- put_trace (map (Pair Env) xs);
put (last_st_tr (map (Pair Env) xs) s)
od) x = (do s1 <- select {s. P s};
x <- get;
xa <- select UNIV;
xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
s <- get;
select (if P s then {()} else {})
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>x. P x \<Longrightarrow> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. (do y <- put_trace (map (Pair Env) xa);
put (last_st_tr (map (Pair Env) xa) x)
od) x) = (\<Union>xa. (do xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
select (if P (last_st_tr (map (Pair Env) xa) x) then {()} else {})
od) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>x. P x \<Longrightarrow> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. (do y <- put_trace (map (Pair Env) xa);
put (last_st_tr (map (Pair Env) xa) x)
od) x) = (\<Union>xa\<in>{xa. P (last_st_tr (map (Pair Env) xa) x)}. (do xb <- put_trace (map (Pair Env) xa);
put (last_st_tr (map (Pair Env) xa) x)
od) x) \<union> (\<Union>xa\<in>{xa. \<not> P (last_st_tr (map (Pair Env) xa) x)}. (do xb <- put_trace (map (Pair Env) xa);
y <- put (last_st_tr (map (Pair Env) xa) x);
select {}
od) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>x. P x \<Longrightarrow> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)}) \<union> (\<lambda>x. case x of (a, b) \<Rightarrow> (a @ map (Pair Env) xa, b)) ` put (last_st_tr (map (Pair Env) xa) x) x) = (\<Union>xa\<in>{xa. P (last_st_tr (map (Pair Env) xa) x)}. (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)}) \<union> (\<lambda>x. case x of (a, b) \<Rightarrow> (a @ map (Pair Env) xa, b)) ` put (last_st_tr (map (Pair Env) xa) x) x) \<union> (\<Union>xa\<in>{xa. \<not> P (last_st_tr (map (Pair Env) xa) x)}. (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)}) \<union> (\<lambda>x. case x of (a, b) \<Rightarrow> (a @ map (Pair Env) xa, b)) ` (do y <- put (last_st_tr (map (Pair Env) xa) x);
select {}
od) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>x. P x \<Longrightarrow> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) = (\<Union>xa\<in>{xa. P (last_st_tr (map (Pair Env) xa) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) \<union> (\<Union>x\<in>{xa. \<not> P (last_st_tr (map (Pair Env) xa) x)}. \<Union>xa\<in>{n. 0 < n \<and> n \<le> length x}. {(drop xa (map (Pair Env) x), Incomplete)}) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>x. P x \<Longrightarrow> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) \<subseteq> (\<Union>xa\<in>{xa. P (last_st_tr (map (Pair Env) xa) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) \<union> (\<Union>x\<in>{xa. \<not> P (last_st_tr (map (Pair Env) xa) x)}. \<Union>xa\<in>{n. 0 < n \<and> n \<le> length x}. {(drop xa (map (Pair Env) x), Incomplete)}) \<and> (\<Union>xa\<in>{xa. P (last_st_tr (map (Pair Env) xa) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) \<union> (\<Union>x\<in>{xa. \<not> P (last_st_tr (map (Pair Env) xa) x)}. \<Union>xa\<in>{n. 0 < n \<and> n \<le> length x}. {(drop xa (map (Pair Env) x), Incomplete)}) \<subseteq> (\<Union>xa\<in>{xs. P (last_st_tr (map (Pair Env) xs) x)}. insert (map (Pair Env) xa, Result ((), last_st_tr (map (Pair Env) xa) x)) (\<Union>x\<in>{n. 0 < n \<and> n \<le> length xa}. {(drop x (map (Pair Env) xa), Incomplete)})) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>\<not> P (last_st_tr (map (Pair Env) xa) x); P xc; 0 < xb; xb \<le> length xa\<rbrakk> \<Longrightarrow> \<exists>xc. P (last_st_tr (map (Pair Env) xc) x) \<and> (\<exists>x>0. x \<le> length xc \<and> drop xb (map (Pair Env) xa) = drop x (map (Pair Env) xc)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>\<not> P (last_st_tr (map (Pair Env) xa) x); P xc; 0 < xb; xb \<le> length xa\<rbrakk> \<Longrightarrow> \<exists>xs s. P (last_st_tr (map (Pair Env) (s # xs)) x) \<and> (\<exists>x>0. x \<le> length (s # xs) \<and> drop xb (map (Pair Env) xa) = drop x (map (Pair Env) (s # xs))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>\<not> P (last_st_tr (map (Pair Env) xa) x); P xc; 0 < xb; xb \<le> length xa\<rbrakk> \<Longrightarrow> \<exists>xc xd. P (last_st_tr (map (Pair Env) (xd # xc)) x) \<and> (\<exists>n. 0 < Suc n \<and> Suc n \<le> length (xd # xc) \<and> drop xb (map (Pair Env) xa) = drop (Suc n) (map (Pair Env) (xd # xc))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>\<not> P (last_st_tr (map (Pair Env) xa) x); P xc; 0 < xb; xb \<le> length xa\<rbrakk> \<Longrightarrow> Ex P \<and> (\<exists>x n. n \<le> length x \<and> drop xb (map (Pair Env) xa) = drop n (map (Pair Env) x)) proof (prove)
goal:
No subgoals!