theory SR_lemmas_C

lemma cmap_relation_cong:
  assumes adom: "dom am = dom am'"
  and     cdom: "dom cm = dom cm'"
  and   rel: "\<And>p a a' b b'.
  \<lbrakk> am p = Some a; am' p = Some a'; cm (f p) = Some b; cm' (f p) = Some b' \<rbrakk> \<Longrightarrow> rel a b = rel' a' b'"
  shows "cmap_relation am cm f rel = cmap_relation am' cm' f rel'" unfolding cmap_relation_def apply (clarsimp simp: adom cdom) apply (rule iffI) apply simp apply (erule conjE) apply (drule equalityD1) apply (rule ballI) apply (drule (1) bspec) apply (erule iffD1 [OF rel, rotated -1]) apply (rule Some_the, erule ssubst [OF adom]) apply (erule Some_the) apply (rule Some_the [where f = cm]) apply (drule subsetD) apply (erule imageI) apply (simp add: cdom) apply (rule Some_the [where f = cm']) apply (erule subsetD) apply (erule imageI)
  \<comment> \<open>clag\<close> apply simp apply (erule conjE) apply (drule equalityD1) apply (rule ballI) apply (drule (1) bspec) apply (erule iffD2 [OF rel, rotated -1]) apply (rule Some_the, erule ssubst [OF adom]) apply (erule Some_the) apply (rule Some_the [where f = cm]) apply (drule subsetD) apply (erule imageI) apply (simp add: cdom) apply (rule Some_the [where f = cm']) apply (erule subsetD) apply (erule imageI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation am cm f rel = cmap_relation am' cm' f rel' proof (prove)
goal (1 subgoal):
 1. (f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))))) = (f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x))))) proof (prove)
goal (1 subgoal):
 1. (f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))))) = (f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x))))) proof (prove)
goal (2 subgoals):
 1. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x))))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) \<Longrightarrow> \<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f ` dom am' = dom cm'; \<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))); f ` dom am' \<subseteq> dom cm'\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))); f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> rel' (the (am' x)) (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'; rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> rel' (the (am' x)) (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am (?p17 x) = Some (the (am x))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am' (?p17 x) = Some (the (am' x))
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f (?p17 x)) = Some (the (cm (f x)))
 4. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f (?p17 x)) = Some (the (cm' (f x)))
 5. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am' x = Some (the (am' x))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f x) = Some (the (cm (f x)))
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 4. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f x) = Some (the (cm (f x)))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 3. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 3. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (4 subgoals):
 1. \<And>x. x \<in> dom am' \<Longrightarrow> ?c28 x \<in> f ` dom am'
 2. \<And>x. \<lbrakk>x \<in> dom am'; ?c28 x \<in> dom cm'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 4. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<in> dom am'; f x \<in> dom cm'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 3. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x)))
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> f x \<in> dom cm'
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> dom am' \<Longrightarrow> f x \<in> f ` dom am'
 2. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (1 subgoal):
 1. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x)))) proof (prove)
goal (1 subgoal):
 1. f ` dom am' = dom cm' \<and> (\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))) \<Longrightarrow> \<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am' = dom cm'; \<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x))); f ` dom am' \<subseteq> dom cm'\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am'. rel (the (am x)) (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom am'. rel' (the (am' x)) (the (cm' (f x))); f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'; rel' (the (am' x)) (the (cm' (f x)))\<rbrakk> \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am (?p47 x) = Some (the (am x))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am' (?p47 x) = Some (the (am' x))
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f (?p47 x)) = Some (the (cm (f x)))
 4. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f (?p47 x)) = Some (the (cm' (f x))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> am' x = Some (the (am' x))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f x) = Some (the (cm (f x)))
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm (f x) = Some (the (cm (f x)))
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> dom am' \<Longrightarrow> ?c58 x \<in> f ` dom am'
 2. \<And>x. \<lbrakk>x \<in> dom am'; ?c58 x \<in> dom cm'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 3. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> dom am'; f x \<in> dom cm'\<rbrakk> \<Longrightarrow> f x \<in> dom cm
 2. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> cm' (f x) = Some (the (cm' (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f ` dom am' \<subseteq> dom cm'; x \<in> dom am'\<rbrakk> \<Longrightarrow> f x \<in> dom cm' proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> dom am' \<Longrightarrow> f x \<in> f ` dom am' proof (prove)
goal:
No subgoals!