theory Detype_C

lemma cmap_relation_restrict_both_proj:
  "\<lbrakk> cmap_relation (projectKO_opt \<circ>\<^sub>m am) cm f rel; bij f\<rbrakk>
  \<Longrightarrow> cmap_relation (projectKO_opt \<circ>\<^sub>m (am |` (- S))) (cm |` (- f ` S)) f rel" unfolding cmap_relation_def apply (rule conjI) apply (rule equalityI) apply rule apply (clarsimp simp: map_comp_restrict_map_Some_iff image_iff2 bij_def) apply (erule (1) cmap_domE1) apply simp apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def) apply (erule (1) cmap_domE2) apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def map_comp_restrict_map_Some_iff intro!: imageI) apply clarsimp apply (subst restrict_in) apply (clarsimp simp add: image_iff map_comp_restrict_map_Some_iff inj_eq bij_def) apply (clarsimp simp add: map_comp_restrict_map_Some_iff) apply (drule (1) bspec [OF _ domI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (projectKO_opt \<circ>\<^sub>m am) cm f rel; bij f\<rbrakk> \<Longrightarrow> cmap_relation (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) (cm|\<^bsub>(- f ` S)\<^esub>) f rel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) = dom (cm|\<^bsub>(- f ` S)\<^esub>) \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) = dom (cm|\<^bsub>(- f ` S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) \<subseteq> dom (cm|\<^bsub>(- f ` S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> dom (cm|\<^bsub>(- f ` S)\<^esub>) \<subseteq> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 3. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f; x \<in> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)\<rbrakk> \<Longrightarrow> x \<in> dom (cm|\<^bsub>(- f ` S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> dom (cm|\<^bsub>(- f ` S)\<^esub>) \<subseteq> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 3. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x))); inj f; surj f; (projectKO_opt \<circ>\<^sub>m am) xa = Some y; xa \<notin> S\<rbrakk> \<Longrightarrow> \<exists>y. cm (f xa) = Some y
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> dom (cm|\<^bsub>(- f ` S)\<^esub>) \<subseteq> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 3. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (3 subgoals):
 1. \<And>xa y v'. \<lbrakk>\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x))); inj f; surj f; (projectKO_opt \<circ>\<^sub>m am) xa = Some y; xa \<notin> S; cm (f xa) = Some v'\<rbrakk> \<Longrightarrow> \<exists>y. cm (f xa) = Some y
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> dom (cm|\<^bsub>(- f ` S)\<^esub>) \<subseteq> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 3. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> dom (cm|\<^bsub>(- f ` S)\<^esub>) \<subseteq> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<notin> f ` S; cm x = Some y; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x))); inj f; surj f\<rbrakk> \<Longrightarrow> x \<in> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y x' v. \<lbrakk>x \<notin> f ` S; cm x = Some y; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x))); inj f; surj f; x = f x'; (projectKO_opt \<circ>\<^sub>m am) x' = Some v\<rbrakk> \<Longrightarrow> x \<in> f ` dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>)
 2. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>). rel (the ((projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bij f; (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x = Some y; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> rel y (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>bij f; (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x = Some y; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> f x \<in> - f ` S
 2. \<And>x y. \<lbrakk>bij f; (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x = Some y; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> rel y (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bij f; (projectKO_opt \<circ>\<^sub>m am|\<^bsub>(- S)\<^esub>) x = Some y; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> rel y (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bij f; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m am). rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x))); (projectKO_opt \<circ>\<^sub>m am) x = Some y; x \<notin> S\<rbrakk> \<Longrightarrow> rel y (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bij f; f ` dom (projectKO_opt \<circ>\<^sub>m am) = dom cm; (projectKO_opt \<circ>\<^sub>m am) x = Some y; x \<notin> S; rel (the ((projectKO_opt \<circ>\<^sub>m am) x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> rel y (the (cm (f x))) proof (prove)
goal:
No subgoals!