theory SimplRewrite

lemma exec_statefn_simulates_call:
  "\<lbrakk> bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s);
            \<And>s t. f (ret1 s t) = ret2 (f s) (f t);
            \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (call init1 c ret1 save1) (call init2 c ret2 save2)" apply (simp add: call_def block_def block_exn_def) apply (intro exec_statefn_simulates_Seq exec_statefn_simulates_Catch
               exec_statefn_simulates_DynCom
               exec_statefn_simulates_Basic exec_statefn_simulates_Call
               exec_statefn_simulates_Skip_Throw) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t))\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (call init1 c ret1 save1) (call init2 c ret2 save2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t))\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (DynCom (\<lambda>s. TRY
  Basic init1;;
Call c
CATCH Basic (ret1 s);;
THROW
END;;
DynCom (\<lambda>t. Basic (ret1 s);;
save1 s t))) (DynCom (\<lambda>s. TRY
  Basic init2;;
Call c
CATCH Basic (ret2 s);;
THROW
END;;
DynCom (\<lambda>t. Basic (ret2 s);;
save2 s t))) proof (prove)
goal (5 subgoals):
 1. \<And>s sa. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)); s \<in> S; sa \<in> S; init2 (f sa) \<notin> f ` (- {s. f s \<in> com_initial_guards (Call c)})\<rbrakk> \<Longrightarrow> f (init1 sa) = init2 (f sa)
 2. \<And>s. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)); s \<in> S\<rbrakk> \<Longrightarrow> bij f
 3. \<And>s sa. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)); s \<in> S; sa \<in> UNIV; ret2 (f s) (f sa) \<notin> f ` (- {s. f s \<in> com_initial_guards THROW})\<rbrakk> \<Longrightarrow> f (ret1 s sa) = ret2 (f s) (f sa)
 4. \<And>s sa sb. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)); s \<in> S; sa \<in> UNIV; sb \<in> UNIV; ret2 (f s) (f sb) \<notin> f ` (- {sb. f sb \<in> com_initial_guards (save2 (f s) (f sa))})\<rbrakk> \<Longrightarrow> f (ret1 s sb) = ret2 (f s) (f sb)
 5. \<And>s sa. \<lbrakk>bij f; \<And>s. s \<in> S \<Longrightarrow> f (init1 s) = init2 (f s); \<And>s t. f (ret1 s t) = ret2 (f s) (f t); \<And>s t. exec_statefn_simulates f UNIV T (save1 s t) (save2 (f s) (f t)); s \<in> S; sa \<in> UNIV\<rbrakk> \<Longrightarrow> exec_statefn_simulates f UNIV T (save1 s sa) (save2 (f s) (f sa)) proof (prove)
goal:
No subgoals!