theory SR_lemmas_C

lemma cor_map_relI:
  assumes dm: "dom am = dom am'"
  and     rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';
  rel y z \<rbrakk> \<Longrightarrow> rel y' z"
  shows "cmap_relation am cm sz rel \<Longrightarrow> cmap_relation am' cm sz rel" unfolding cmap_relation_def apply - apply clarsimp apply rule apply (simp add: dm) apply rule apply (frule_tac P = "\<lambda>s. x \<in> s" in ssubst [OF dm]) apply (drule (1) bspec) apply (erule domD [where m = am, THEN exE]) apply (rule rl, assumption+) apply (clarsimp simp add: dom_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation am cm sz rel \<Longrightarrow> cmap_relation am' cm sz rel proof (prove)
goal (1 subgoal):
 1. sz ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))) \<Longrightarrow> sz ` dom am' = dom cm \<and> (\<forall>x\<in>dom am'. rel (the (am' x)) (the (cm (sz x)))) proof (prove)
goal (1 subgoal):
 1. sz ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))) \<Longrightarrow> sz ` dom am' = dom cm \<and> (\<forall>x\<in>dom am'. rel (the (am' x)) (the (cm (sz x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))\<rbrakk> \<Longrightarrow> sz ` dom am' = dom cm \<and> (\<forall>x\<in>dom am'. rel (the (am' x)) (the (cm (sz x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))\<rbrakk> \<Longrightarrow> sz ` dom am' = dom cm
 2. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x))); x \<in> dom am'\<rbrakk> \<Longrightarrow> rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (sz x))); x \<in> dom am'; x \<in> dom am\<rbrakk> \<Longrightarrow> rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sz ` dom am = dom cm; x \<in> dom am'; x \<in> dom am; rel (the (am x)) (the (cm (sz x)))\<rbrakk> \<Longrightarrow> rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>sz ` dom am = dom cm; x \<in> dom am'; rel (the (am x)) (the (cm (sz x))); am x = Some xa\<rbrakk> \<Longrightarrow> rel (the (am' x)) (the (cm (sz x))) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>sz ` dom am = dom cm; x \<in> dom am'; rel (the (am x)) (the (cm (sz x))); am x = Some xa\<rbrakk> \<Longrightarrow> am' x = Some (the (am' x))
 2. \<And>x xa. \<lbrakk>sz ` dom am = dom cm; x \<in> dom am'; rel (the (am x)) (the (cm (sz x))); am x = Some xa\<rbrakk> \<Longrightarrow> rel xa (the (cm (sz x))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>sz ` dom am = dom cm; x \<in> dom am'; rel (the (am x)) (the (cm (sz x))); am x = Some xa\<rbrakk> \<Longrightarrow> rel xa (the (cm (sz x))) proof (prove)
goal:
No subgoals!