[STATEMENT]
lemma gen_cast_fun_set_rel[autoref_rules_raw]:
  assumes INS: "GEN_OP mem (\<in>) (Rk\<rightarrow>\<langle>Rk\<rangle>Rs\<rightarrow>bool_rel)"
  shows "(\<lambda>s x. mem x s,CAST) \<in> (\<langle>Rk\<rangle>Rs) \<rightarrow> (\<langle>Rk\<rangle>fun_set_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
have A: "\<And>s. (\<lambda>x. x\<in>s,CAST s) \<in> br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<lambda>x. x \<in> s, CAST s) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> ?s, CAST ?s) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
unfolding fun_set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> (Rk \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, CAST a') \<in> (Rk \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, ?b2 a a') \<in> Rk \<rightarrow> bool_rel
 2. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (?b2 a a', CAST a') \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (?b2 a a', CAST a') \<in> br Collect (\<lambda>_. True)
 2. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, ?b2 a a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
apply (rule A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, \<lambda>x. x \<in> a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
using INS[simplified]
[PROOF STATE]
proof (prove)
using this:
(mem, (\<in>)) \<in> Rk \<rightarrow> \<langle>Rk\<rangle>Rs \<rightarrow> bool_rel

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, \<lambda>x. x \<in> a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
apply parametricity
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel

goal:
No subgoals!
[PROOF STEP]
qed