[STATEMENT]
lemma foldr_cong_plus: (* a more elaborate version of foldr_cong. Using f'=id, g'=id and s = set lst would give foldr_cong exactly. *)
  assumes f_is_g : "\<And> a b c. b \<in> s \<Longrightarrow> f' a = f b (f' c) \<Longrightarrow> g' a = g b (g' c)" (* main assumption *)
      and f'_inj : "\<And> a b. f' a = f' b \<Longrightarrow> a = b"
      and f_bit_sur : "\<And> a b c. f' a = f b c \<Longrightarrow> \<exists> c'. c = f' c'" (* should be provable by cases c *)
      and lst_in_s : "set lst \<subseteq> s" (* formulated like this to make induction easier *)
  shows "f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)
[PROOF STEP]
using lst_in_s
[PROOF STATE]
proof (prove)
using this:
set lst \<subseteq> s

goal (1 subgoal):
 1. f' a = foldr f lst (f' b) \<Longrightarrow> g' a = foldr g lst (g' b)
[PROOF STEP]
proof (induct lst arbitrary: a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>f' ?a = foldr f xs (f' b); set xs \<subseteq> s\<rbrakk> \<Longrightarrow> g' ?a = foldr g xs (g' b)
f' a = foldr f (x # xs) (f' b)
set (x # xs) \<subseteq> s

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
have prems: "f' a = (f x \<circ> foldr f xs) (f' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
f' a = foldr f (x # xs) (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
unfolding foldr_Cons
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. f' a = (f x \<circ> foldr f xs) (f' b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' a = (f x \<circ> foldr f xs) (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "\<exists> c'. f' c' = foldr f xs (f' b)"
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)

goal (1 subgoal):
 1. \<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
using f_bit_sur
[PROOF STATE]
proof (prove)
using this:
f' a = (f x \<circ> foldr f xs) (f' b)
f' ?a = f ?b ?c \<Longrightarrow> \<exists>c'. ?c = f' c'

goal (1 subgoal):
 1. \<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>c'. f' c' = foldr f xs (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c'. f' c' = foldr f xs (f' b)
[PROOF STEP]
obtain c' where c'_def: "f' c' = foldr f xs (f' b)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c'. f' c' = foldr f xs (f' b)

goal (1 subgoal):
 1. (\<And>c'. f' c' = foldr f xs (f' b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' c' = foldr f xs (f' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "f' a = f x (f' c')"
[PROOF STATE]
proof (prove)
using this:
f' c' = foldr f xs (f' b)

goal (1 subgoal):
 1. f' a = f x (f' c')
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
f' c' = foldr f xs (f' b)
f' a = (f x \<circ> foldr f xs) (f' b)

goal (1 subgoal):
 1. f' a = f x (f' c')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' a = f x (f' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
hence "g' a = g x (g' c')"
[PROOF STATE]
proof (prove)
using this:
f' a = f x (f' c')

goal (1 subgoal):
 1. g' a = g x (g' c')
[PROOF STEP]
using f_is_g Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
f' a = f x (f' c')
\<lbrakk>?b \<in> s; f' ?a = f ?b (f' ?c)\<rbrakk> \<Longrightarrow> g' ?a = g ?b (g' ?c)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. g' a = g x (g' c')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = g x (g' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g' a = g x (g' c')

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
have "g' c' = foldr g xs (g' b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g' c' = foldr g xs (g' b)
[PROOF STEP]
using Cons.hyps[of c'] c'_def Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f' c' = foldr f xs (f' b); set xs \<subseteq> s\<rbrakk> \<Longrightarrow> g' c' = foldr g xs (g' b)
f' c' = foldr f xs (f' b)
set (x # xs) \<subseteq> s

goal (1 subgoal):
 1. g' c' = foldr g xs (g' b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g' c' = foldr g xs (g' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
g' a = g x (foldr g xs (g' b))
[PROOF STEP]
have "g' a = (g x \<circ> foldr g xs) (g' b)"
[PROOF STATE]
proof (prove)
using this:
g' a = g x (foldr g xs (g' b))

goal (1 subgoal):
 1. g' a = (g x \<circ> foldr g xs) (g' b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = (g x \<circ> foldr g xs) (g' b)

goal (2 subgoals):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
 2. \<And>a lst aa. \<lbrakk>\<And>a. \<lbrakk>f' a = foldr f lst (f' b); set lst \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g lst (g' b); f' aa = foldr f (a # lst) (f' b); set (a # lst) \<subseteq> s\<rbrakk> \<Longrightarrow> g' aa = foldr g (a # lst) (g' b)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
g' a = (g x \<circ> foldr g xs) (g' b)

goal (1 subgoal):
 1. g' a = foldr g (x # xs) (g' b)
[PROOF STEP]
using foldr_Cons
[PROOF STATE]
proof (prove)
using this:
g' a = (g x \<circ> foldr g xs) (g' b)
foldr ?f (?x # ?xs) = ?f ?x \<circ> foldr ?f ?xs

goal (1 subgoal):
 1. g' a = foldr g (x # xs) (g' b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g' a = foldr g (x # xs) (g' b)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>f' a = foldr f [] (f' b); set [] \<subseteq> s\<rbrakk> \<Longrightarrow> g' a = foldr g [] (g' b)
[PROOF STEP]
qed (insert f'_inj, auto)