theory EquivValid

lemma trancl_subset_equivalence:
  "\<lbrakk>(a, b) \<in> r'\<^sup>+; \<forall>x. (a, x)\<in>r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+" apply(induct a b rule: trancl.induct) apply(blast) apply(simp) apply(rule_tac b=b in trancl_into_trancl) apply(simp) apply(erule_tac x=c in allE) apply(subgoal_tac "(a, c) \<in> r'\<^sup>+") apply(auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r'\<^sup>+; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+
 2. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; \<lbrakk>\<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; \<lbrakk>\<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x y. Q x \<longrightarrow> ((y, x) \<in> r) = ((y, x) \<in> r')\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r'))\<rbrakk> \<Longrightarrow> (a, c) \<in> r\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r'))\<rbrakk> \<Longrightarrow> (a, b) \<in> r\<^sup>+
 2. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r'))\<rbrakk> \<Longrightarrow> (b, c) \<in> r proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. (a, x) \<in> r'\<^sup>+ \<longrightarrow> Q x; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r'))\<rbrakk> \<Longrightarrow> (b, c) \<in> r proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r')); (a, c) \<in> r'\<^sup>+ \<longrightarrow> Q c\<rbrakk> \<Longrightarrow> (b, c) \<in> r proof (prove)
goal (2 subgoals):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r')); (a, c) \<in> r'\<^sup>+ \<longrightarrow> Q c; (a, c) \<in> r'\<^sup>+\<rbrakk> \<Longrightarrow> (b, c) \<in> r
 2. \<And>a b c. \<lbrakk>(a, b) \<in> r'\<^sup>+; (a, b) \<in> r\<^sup>+; (b, c) \<in> r'; \<forall>x. Q x \<longrightarrow> (\<forall>y. ((y, x) \<in> r) = ((y, x) \<in> r')); (a, c) \<in> r'\<^sup>+ \<longrightarrow> Q c\<rbrakk> \<Longrightarrow> (a, c) \<in> r'\<^sup>+ proof (prove)
goal:
No subgoals!