[STATEMENT]
lemma list_map_autoref_update[autoref_rules]:
  assumes eq: "GEN_OP eq (=) (Rk\<rightarrow>Rk\<rightarrow>Id)"
  shows "(list_map_update eq, op_map_update) \<in>
      Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk,Rv\<rangle>list_map_rel \<rightarrow> \<langle>Rk,Rv\<rangle>list_map_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_map_update eq, op_map_update) \<in> Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk, Rv\<rangle>list_map_rel \<rightarrow> \<langle>Rk, Rv\<rangle>list_map_rel
[PROOF STEP]
unfolding list_map_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_map_update eq, op_map_update) \<in> Rk \<rightarrow> Rv \<rightarrow> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel O br map_of list_map_invar \<rightarrow> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel O br map_of list_map_invar
[PROOF STEP]
apply (intro fun_relI, elim relcompE, intro relcompI, clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a a'b x y. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, a'b) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (list_map_update eq a aa x, ?b4 a a' aa a'a x a'b x y a'b) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel
 2. \<And>a a' aa a'a ab a'b x y z. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (ab, a'b) = (x, z); (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, z) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (?b4 a a' aa a'a ab a'b x y z, op_map_update a' a'a a'b) \<in> br map_of list_map_invar
[PROOF STEP]
apply (erule (2) list_map_autoref_update1[param_fo, OF eq[simplified]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b x y z. \<lbrakk>(a, a') \<in> Rk; (aa, a'a) \<in> Rv; (ab, a'b) = (x, z); (x, y) \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; (y, z) \<in> br map_of list_map_invar\<rbrakk> \<Longrightarrow> (list_map_update (=) a' a'a y, op_map_update a' a'a a'b) \<in> br map_of list_map_invar
[PROOF STEP]
apply (rule list_map_autoref_update2[param_fo], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done