theory ADT_C

lemma cmap_relation_unique:
  assumes inj_f: "inj f"
  assumes r: "\<And>x y z. r x z \<Longrightarrow> r y z \<Longrightarrow> x=y"
  shows "cmap_relation a c f r \<Longrightarrow> cmap_relation a' c f r \<Longrightarrow> a' = a"
        (is "PROP ?goal") apply (clarsimp simp add: cmap_relation_def) apply (drule inj_image_inv[OF inj_f])+ apply simp apply (rule ext) apply (case_tac "x:dom a") apply (drule bspec, assumption)+ apply (simp add: dom_def Collect_eq, drule_tac x=x in spec) apply (drule (1) r) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation a c f r; cmap_relation a' c f r\<rbrakk> \<Longrightarrow> a' = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom a = dom c; \<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); f ` dom a' = dom c; \<forall>x\<in>dom a'. r (the (a' x)) (the (c (f x)))\<rbrakk> \<Longrightarrow> a' = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a'. r (the (a' x)) (the (c (f x))); inv f ` dom c = dom a; inv f ` dom c = dom a'\<rbrakk> \<Longrightarrow> a' = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a\<rbrakk> \<Longrightarrow> a' = a proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<in> dom a\<rbrakk> \<Longrightarrow> a' x = a x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<notin> dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>dom a' = dom a; inv f ` dom c = dom a; x \<in> dom a; r (the (a x)) (the (c (f x))); r (the (a' x)) (the (c (f x)))\<rbrakk> \<Longrightarrow> a' x = a x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<notin> dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv f ` {a. \<exists>y. c a = Some y} = {aa. \<exists>y. a aa = Some y}; \<exists>y. a x = Some y; r (the (a x)) (the (c (f x))); r (the (a' x)) (the (c (f x))); (\<exists>y. a' x = Some y) = (\<exists>y. a x = Some y)\<rbrakk> \<Longrightarrow> a' x = a x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<notin> dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>inv f ` {a. \<exists>y. c a = Some y} = {aa. \<exists>y. a aa = Some y}; \<exists>y. a x = Some y; r (the (a' x)) (the (c (f x))); (\<exists>y. a' x = Some y) = (\<exists>y. a x = Some y); the (a x) = the (a' x)\<rbrakk> \<Longrightarrow> a' x = a x
 2. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<notin> dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>dom a. r (the (a x)) (the (c (f x))); \<forall>x\<in>dom a. r (the (a' x)) (the (c (f x))); dom a' = dom a; inv f ` dom c = dom a; x \<notin> dom a\<rbrakk> \<Longrightarrow> a' x = a x proof (prove)
goal:
No subgoals!