[STATEMENT]
lemma compile_env_imp_rel_option:
  assumes "compile_env F1 = Some F2"
  shows "rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
compile_env F1 = Some F2
[PROOF STEP]
obtain xs where
    ap_map_list_F1: "ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs" and
    F2_def: "F2 = Sinca.Fenv.from_list xs"
[PROOF STATE]
proof (prove)
using this:
compile_env F1 = Some F2

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs; F2 = Sinca.Fenv.from_list xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: compile_env_def ap_option_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs
F2 = Sinca.Fenv.from_list xs

goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
unfolding F2_def Sinca.Fenv.from_list_correct[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get (Sinca.Fenv.from_list xs) f)
[PROOF STEP]
unfolding Sinca.Fenv.from_list_correct
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (map_of xs f)
[PROOF STEP]
unfolding Sstd.Fenv.to_list_correct[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (map_of (Fstd_to_list F1) f) (map_of xs f)
[PROOF STEP]
using ap_map_list_F1
[PROOF STATE]
proof (prove)
using this:
ap_map_list (ap_map_prod Some compile_fundef) (Fstd_to_list F1) = Some xs

goal (1 subgoal):
 1. rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (map_of (Fstd_to_list F1) f) (map_of xs f)
[PROOF STEP]
by (simp add: ap_map_list_ap_map_prod_imp_rel_option_map_of)
[PROOF STATE]
proof (state)
this:
rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)

goal:
No subgoals!
[PROOF STEP]
qed