[STATEMENT]
lemma (in irules) compile_rules:
  assumes "finished rs"
  shows "prules C_info (compile rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prules C_info (Rewriting_Pterm.compile rs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. is_fmap (Rewriting_Pterm.compile rs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 6. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
show "is_fmap (compile rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_fmap (Rewriting_Pterm.compile rs)
[PROOF STEP]
using fmap
[PROOF STATE]
proof (prove)
using this:
is_fmap rs

goal (1 subgoal):
 1. is_fmap (Rewriting_Pterm.compile rs)
[PROOF STEP]
unfolding compile_def map_prod_def id_apply
[PROOF STATE]
proof (prove)
using this:
is_fmap rs

goal (1 subgoal):
 1. is_fmap ((\<lambda>(x, y). (x, translate_rhs y)) |`| rs)
[PROOF STEP]
by (rule is_fmap_image)
[PROOF STATE]
proof (state)
this:
is_fmap (Rewriting_Pterm.compile rs)

goal (5 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
 2. distinct all_constructors
 3. fBall (Rewriting_Pterm.compile rs) prule
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 5. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
show "fdisjnt (fst |`| compile rs) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt (fst |`| Rewriting_Pterm.compile rs) C
[PROOF STEP]
unfolding compile_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt (fst |`| map_prod id translate_rhs |`| rs) C
[PROOF STEP]
using disjnt
[PROOF STATE]
proof (prove)
using this:
fdisjnt (fst |`| rs) C

goal (1 subgoal):
 1. fdisjnt (fst |`| map_prod id translate_rhs |`| rs) C
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fdisjnt (fst |`| Rewriting_Pterm.compile rs) C

goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
have
    "fBall (compile rs) prule"
    "fBall (compile rs) (\<lambda>(_, rhs). \<not> shadows_consts rhs)"
    "fBall (compile rs) (\<lambda>(_, rhs). welldefined rhs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)
[PROOF STEP]
proof (safe del: fsubsetI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
fix name rhs
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
assume "(name, rhs) |\<in>| compile rs"
[PROOF STATE]
proof (state)
this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
(* FIXME clone of compile_correct *)
[PROOF STATE]
proof (state)
this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs
[PROOF STEP]
obtain irs where "(name, irs) |\<in>| rs" "rhs = translate_rhs irs"
[PROOF STATE]
proof (prove)
using this:
(name, rhs) |\<in>| Rewriting_Pterm.compile rs

goal (1 subgoal):
 1. (\<And>irs. \<lbrakk>(name, irs) |\<in>| rs; rhs = translate_rhs irs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding compile_def
[PROOF STATE]
proof (prove)
using this:
(name, rhs) |\<in>| map_prod id translate_rhs |`| rs

goal (1 subgoal):
 1. (\<And>irs. \<lbrakk>(name, irs) |\<in>| rs; rhs = translate_rhs irs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "is_fmap irs" "irs \<noteq> {||}" "arity irs = 0"
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
using assms inner
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs
finished rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
unfolding finished_def
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
rhs = translate_rhs irs
fBall rs (\<lambda>(uu_, irs). arity irs = 0)
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. is_fmap irs &&& irs \<noteq> {||} &&& arity irs = 0
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "arity_compatibles irs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
using \<open>(name, irs) |\<in>| rs\<close> inner
[PROOF STATE]
proof (prove)
using this:
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
by (blast dest: fpairwiseD)
[PROOF STATE]
proof (state)
this:
Rewriting_Nterm.arity_compatibles irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0
Rewriting_Nterm.arity_compatibles irs
[PROOF STEP]
obtain u where "irs = {| ([], u) |}"
[PROOF STATE]
proof (prove)
using this:
is_fmap irs
irs \<noteq> {||}
arity irs = 0
Rewriting_Nterm.arity_compatibles irs

goal (1 subgoal):
 1. (\<And>u. irs = {|([], u)|} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis arity_zero_shape)
[PROOF STATE]
proof (state)
this:
irs = {|([], u)|}

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "rhs = u" and u: "([], u) |\<in>| irs"
[PROOF STATE]
proof (prove)
using this:
irs = {|([], u)|}

goal (1 subgoal):
 1. rhs = u &&& ([], u) |\<in>| irs
[PROOF STEP]
unfolding \<open>rhs = _\<close> translate_rhs_def
[PROOF STATE]
proof (prove)
using this:
irs = {|([], u)|}

goal (1 subgoal):
 1. (snd \<circ> fthe_elem) irs = u &&& ([], u) |\<in>| irs
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
rhs = u
([], u) |\<in>| irs

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "abs_ish [] u"
[PROOF STATE]
proof (prove)
using this:
rhs = u
([], u) |\<in>| irs

goal (1 subgoal):
 1. abs_ish [] u
[PROOF STEP]
using inner \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
rhs = u
([], u) |\<in>| irs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
(name, irs) |\<in>| rs

goal (1 subgoal):
 1. abs_ish [] u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
abs_ish [] u

goal (5 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> is_abs b
 4. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 5. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "is_abs rhs"
[PROOF STATE]
proof (prove)
using this:
abs_ish [] u

goal (1 subgoal):
 1. is_abs rhs
[PROOF STEP]
unfolding abs_ish_def \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> [] \<or> is_abs u

goal (1 subgoal):
 1. is_abs u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_abs rhs

goal (4 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> pre_strong_term_class.wellformed b
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 3. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
show "wellformed rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
using u \<open>(name, irs) |\<in>| rs\<close> inner
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. pre_strong_term_class.wellformed rhs
[PROOF STEP]
unfolding \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
(name, irs) |\<in>| rs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))

goal (1 subgoal):
 1. pre_strong_term_class.wellformed u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pre_strong_term_class.wellformed rhs

goal (3 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 2. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "closed_except u {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed u
[PROOF STEP]
using u inner \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
([], u) |\<in>| irs
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
(name, irs) |\<in>| rs

goal (1 subgoal):
 1. closed u
[PROOF STEP]
by (metis (mono_tags, lifting) case_prod_conv fbspec freess_empty)
[PROOF STATE]
proof (state)
this:
closed u

goal (3 subgoals):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> closed b
 2. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "closed rhs"
[PROOF STATE]
proof (prove)
using this:
closed u

goal (1 subgoal):
 1. closed rhs
[PROOF STEP]
unfolding \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
closed u

goal (1 subgoal):
 1. closed u
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
closed rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
closed rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
assume "shadows_consts rhs"
[PROOF STATE]
proof (state)
this:
shadows_consts rhs

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
hence "shadows_consts u"
[PROOF STATE]
proof (prove)
using this:
shadows_consts rhs

goal (1 subgoal):
 1. shadows_consts u
[PROOF STEP]
unfolding compile_def \<open>rhs = u\<close>
[PROOF STATE]
proof (prove)
using this:
shadows_consts u

goal (1 subgoal):
 1. shadows_consts u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
shadows_consts u

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
shadows_consts u

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "\<not> shadows_consts u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> shadows_consts u
[PROOF STEP]
using inner \<open>([], u) |\<in>| irs\<close> \<open>(name, irs) |\<in>| rs\<close>
[PROOF STATE]
proof (prove)
using this:
fBall rs (\<lambda>(uu_, irs). Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts))
([], u) |\<in>| irs
(name, irs) |\<in>| rs

goal (1 subgoal):
 1. \<not> shadows_consts u
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> shadows_consts u

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) |\<in>| Rewriting_Pterm.compile rs; shadows_consts b\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
shadows_consts u
\<not> shadows_consts u
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
shadows_consts u
\<not> shadows_consts u

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
shadows_consts rhs \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
have "welldefined u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
using fbspec[OF inner \<open>(name, irs) |\<in>| rs\<close>, simplified] \<open>([], u) |\<in>| irs\<close>
[PROOF STATE]
proof (prove)
using this:
Rewriting_Nterm.arity_compatibles irs \<and> is_fmap irs \<and> patterns_compatibles irs \<and> irs \<noteq> {||} \<and> fBall irs (\<lambda>(pats, rhs). linears pats \<and> abs_ish pats rhs \<and> closed_except rhs (freess pats) \<and> fdisjnt (freess pats) all_consts \<and> pre_strong_term_class.wellformed rhs \<and> \<not> shadows_consts rhs \<and> consts rhs |\<subseteq>| all_consts)
([], u) |\<in>| irs

goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. \<And>a b. (a, b) |\<in>| Rewriting_Pterm.compile rs \<Longrightarrow> consts b |\<subseteq>| all_consts
[PROOF STEP]
thus "welldefined rhs"
[PROOF STATE]
proof (prove)
using this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. consts rhs |\<subseteq>| all_consts
[PROOF STEP]
unfolding \<open>rhs = u\<close> compile_def
[PROOF STATE]
proof (prove)
using this:
consts u |\<subseteq>| all_consts

goal (1 subgoal):
 1. consts u |\<subseteq>| all_consts
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
consts rhs |\<subseteq>| all_consts

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (4 subgoals):
 1. distinct all_constructors
 2. fBall (Rewriting_Pterm.compile rs) prule
 3. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
 4. fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
thus
    "fBall (compile rs) prule"
    "fBall (compile rs) (\<lambda>(_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| compile rs) rhs)"
    "fBall (compile rs) (\<lambda>(_, rhs). pre_constants.welldefined C_info (fst |`| compile rs) rhs)"
[PROOF STATE]
proof (prove)
using this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))
[PROOF STEP]
unfolding compile_heads
[PROOF STATE]
proof (prove)
using this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)

goal (1 subgoal):
 1. fBall (Rewriting_Pterm.compile rs) prule &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> shadows_consts rhs) &&& fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| all_consts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fBall (Rewriting_Pterm.compile rs) prule
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). \<not> pre_constants.shadows_consts C_info (fst |`| Rewriting_Pterm.compile rs) rhs)
fBall (Rewriting_Pterm.compile rs) (\<lambda>(uu_, rhs). consts rhs |\<subseteq>| pre_constants.all_consts C_info (fst |`| Rewriting_Pterm.compile rs))

goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
show "distinct all_constructors"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct all_constructors
[PROOF STEP]
by (fact distinct_ctr)
[PROOF STATE]
proof (state)
this:
distinct all_constructors

goal:
No subgoals!
[PROOF STEP]
qed