theory Finalise_DR

lemma trancl_image:
  assumes inj: "inj_on f (Domain S \<union> Range S)"
  shows "trancl ((\<lambda>(x, y). (f x, f y)) ` S) = (\<lambda>(x, y). (f x, f y)) ` trancl S"
  (is "?lhs = ?rhs") apply safe apply (erule trancl.induct) apply clarsimp apply (erule image_eqI[rotated, OF r_into_trancl]) apply simp apply (clarsimp simp: inj_on_eq_iff[OF inj]
                         RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]]
                         DomainI) apply (erule(1) image_eqI[rotated, OF trancl_into_trancl]) apply simp apply (erule trancl.induct) apply (rule r_into_trancl, erule image_eqI[rotated]) apply simp apply (erule trancl_into_trancl) apply (erule image_eqI[rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ = (\<lambda>(x, y). (f x, f y)) ` S\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ \<Longrightarrow> (a, b) \<in> (\<lambda>(x, y). (f x, f y)) ` S\<^sup>+
 2. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b aa ba. (aa, ba) \<in> (\<lambda>(x, y). (f x, f y)) ` S \<Longrightarrow> (aa, ba) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 2. \<And>a b aa ba c. \<lbrakk>(aa, ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+; (aa, ba) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+; (ba, c) \<in> (\<lambda>(x, y). (f x, f y)) ` S\<rbrakk> \<Longrightarrow> (aa, c) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 3. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b. (a, b) \<in> S \<Longrightarrow> (f a, f b) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 2. \<And>a b aa ba c. \<lbrakk>(aa, ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+; (aa, ba) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+; (ba, c) \<in> (\<lambda>(x, y). (f x, f y)) ` S\<rbrakk> \<Longrightarrow> (aa, c) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 3. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (3 subgoals):
 1. \<And>a b. (f a, f b) = (case (a, b) of (x, y) \<Rightarrow> (f x, f y))
 2. \<And>a b aa ba c. \<lbrakk>(aa, ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+; (aa, ba) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+; (ba, c) \<in> (\<lambda>(x, y). (f x, f y)) ` S\<rbrakk> \<Longrightarrow> (aa, c) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 3. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba c. \<lbrakk>(aa, ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+; (aa, ba) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+; (ba, c) \<in> (\<lambda>(x, y). (f x, f y)) ` S\<rbrakk> \<Longrightarrow> (aa, c) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 2. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ab bb. \<lbrakk>(f a, f ab) \<in> ((\<lambda>x. case x of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+; (a, ab) \<in> S\<^sup>+; (ab, bb) \<in> S\<rbrakk> \<Longrightarrow> (f a, f bb) \<in> (\<lambda>x. case x of (x, y) \<Rightarrow> (f x, f y)) ` S\<^sup>+
 2. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a ab bb. \<lbrakk>(f a, f ab) \<in> ((\<lambda>x. case x of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+; (ab, bb) \<in> S\<rbrakk> \<Longrightarrow> (f a, f bb) = (case (a, bb) of (x, y) \<Rightarrow> (f x, f y))
 2. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. (aa, ba) \<in> S\<^sup>+ \<Longrightarrow> (f aa, f ba) \<in> ((\<lambda>(x, y). (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. (ab, bb) \<in> S \<Longrightarrow> (f ab, f bb) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+
 2. \<And>a b aa ba ab bb c. \<lbrakk>(ab, bb) \<in> S\<^sup>+; (f ab, f bb) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+; (bb, c) \<in> S\<rbrakk> \<Longrightarrow> (f ab, f c) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. (f ab, f bb) = (case (ab, bb) of (x, y) \<Rightarrow> (f x, f y))
 2. \<And>a b aa ba ab bb c. \<lbrakk>(ab, bb) \<in> S\<^sup>+; (f ab, f bb) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+; (bb, c) \<in> S\<rbrakk> \<Longrightarrow> (f ab, f c) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb c. \<lbrakk>(ab, bb) \<in> S\<^sup>+; (f ab, f bb) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+; (bb, c) \<in> S\<rbrakk> \<Longrightarrow> (f ab, f c) \<in> ((\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb c. \<lbrakk>(ab, bb) \<in> S\<^sup>+; (bb, c) \<in> S\<rbrakk> \<Longrightarrow> (f bb, f c) \<in> (\<lambda>a. case a of (x, y) \<Rightarrow> (f x, f y)) ` S proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb c. (ab, bb) \<in> S\<^sup>+ \<Longrightarrow> (f bb, f c) = (case (bb, c) of (x, y) \<Rightarrow> (f x, f y)) proof (prove)
goal:
No subgoals!