[STATEMENT]
lemma subst_0_lift:
  \<open>substt (liftt t) s 0 = t\<close>
  \<open>substts (liftts l) s 0 = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftt t[s/0] = t &&& liftts l[s/0] = l
[PROOF STEP]
by (induct t and l rule: substt.induct substts.induct) simp_all


[STATEMENT]
lemma params_lift [simp]:
  fixes t :: \<open>'a term\<close> and ts :: \<open>'a term list\<close>
  shows
    \<open>paramst (liftt t) = paramst t\<close>
    \<open>paramsts (liftts ts) = paramsts ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paramst (liftt t) = paramst t &&& paramsts (liftts ts) = paramsts ts
[PROOF STEP]
by (induct t and ts rule: paramst.induct paramsts.induct) simp_all


[STATEMENT]
lemma subst_new' [simp]:
  \<open>new_term c s \<Longrightarrow> new_term c t \<Longrightarrow> new_term c (substt t s m)\<close>
  \<open>new_term c s \<Longrightarrow> new_list c l \<Longrightarrow> new_list c (substts l s m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>new_term c s; new_term c t\<rbrakk> \<Longrightarrow> new_term c (t[s/m])) &&& (\<lbrakk>new_term c s; new_list c l\<rbrakk> \<Longrightarrow> new_list c (l[s/m]))
[PROOF STEP]
by (induct t and l rule: substt.induct substts.induct) simp_all


[STATEMENT]
lemma subst_new [simp]: \<open>new_term c s \<Longrightarrow> new c p \<Longrightarrow> new c (subst p s m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_term c s; new c p\<rbrakk> \<Longrightarrow> new c (p[s/m])
[PROOF STEP]
by (induct p arbitrary: m s) simp_all


[STATEMENT]
lemma subst_new_all:
  assumes \<open>a \<notin> set cs\<close> \<open>list_all (\<lambda>c. new c p) cs\<close>
  shows \<open>list_all (\<lambda>c. new c (subst p (App a []) m)) cs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>c. new c (p[App a []/m])) cs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<notin> set cs
list_all (\<lambda>c. new c p) cs

goal (1 subgoal):
 1. list_all (\<lambda>c. new c (p[App a []/m])) cs
[PROOF STEP]
by (induct cs) auto


[STATEMENT]
lemma subc_new' [simp]:
  \<open>new_term c t \<Longrightarrow> subc_term c s t = t\<close>
  \<open>new_list c l \<Longrightarrow> subc_list c s l = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c t \<Longrightarrow> subc_term c s t = t) &&& (new_list c l \<Longrightarrow> subc_list c s l = l)
[PROOF STEP]
by (induct t and l rule: subc_term.induct subc_list.induct) auto


[STATEMENT]
lemma subc_new [simp]: \<open>new c p \<Longrightarrow> subc c s p = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new c p \<Longrightarrow> subc c s p = p
[PROOF STEP]
by (induct p arbitrary: s) simp_all


[STATEMENT]
lemma subc_psubst' [simp]:
  \<open>(\<forall>x \<in> paramst t. x \<noteq> c \<longrightarrow> f x \<noteq> f c) \<Longrightarrow>
    psubstt f (subc_term c s t) = subc_term (f c) (psubstt f s) (psubstt f t)\<close>
  \<open>(\<forall>x \<in> paramsts l. x \<noteq> c \<longrightarrow> f x \<noteq> f c) \<Longrightarrow>
    psubstts f (subc_list c s l) = subc_list (f c) (psubstt f s) (psubstts f l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>paramst t. x \<noteq> c \<longrightarrow> f x \<noteq> f c \<Longrightarrow> psubstt f (subc_term c s t) = subc_term (f c) (psubstt f s) (psubstt f t)) &&& (\<forall>x\<in>paramsts l. x \<noteq> c \<longrightarrow> f x \<noteq> f c \<Longrightarrow> psubstts f (subc_list c s l) = subc_list (f c) (psubstt f s) (psubstts f l))
[PROOF STEP]
by (induct t and l rule: psubstt.induct psubstts.induct) simp_all


[STATEMENT]
lemma subc_psubst: \<open>(\<forall>x \<in> params p. x \<noteq> c \<longrightarrow> f x \<noteq> f c) \<Longrightarrow>
    psubst f (subc c s p) = subc (f c) (psubstt f s) (psubst f p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>params p. x \<noteq> c \<longrightarrow> f x \<noteq> f c \<Longrightarrow> psubst f (subc c s p) = subc (f c) (psubstt f s) (psubst f p)
[PROOF STEP]
by (induct p arbitrary: s) simp_all


[STATEMENT]
lemma subcs_psubst: \<open>(\<forall>x \<in> (\<Union>p \<in> set z. params p). x \<noteq> c \<longrightarrow> f x \<noteq> f c) \<Longrightarrow>
    map (psubst f) (subcs c s z) = subcs (f c) (psubstt f s) (map (psubst f) z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<Union> (params ` set z). x \<noteq> c \<longrightarrow> f x \<noteq> f c \<Longrightarrow> map (psubst f) (subcs c s z) = subcs (f c) (psubstt f s) (map (psubst f) z)
[PROOF STEP]
by (induct z) (simp_all add: subc_psubst)


[STATEMENT]
lemma new_lift:
  \<open>new_term c t \<Longrightarrow> new_term c (liftt t)\<close>
  \<open>new_list c l \<Longrightarrow> new_list c (liftts l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c t \<Longrightarrow> new_term c (liftt t)) &&& (new_list c l \<Longrightarrow> new_list c (liftts l))
[PROOF STEP]
by (induct t and l rule: liftt.induct liftts.induct) simp_all


[STATEMENT]
lemma new_subc' [simp]:
  \<open>new_term d s \<Longrightarrow> new_term d t \<Longrightarrow> new_term d (subc_term c s t)\<close>
  \<open>new_term d s \<Longrightarrow> new_list d l \<Longrightarrow> new_list d (subc_list c s l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>new_term d s; new_term d t\<rbrakk> \<Longrightarrow> new_term d (subc_term c s t)) &&& (\<lbrakk>new_term d s; new_list d l\<rbrakk> \<Longrightarrow> new_list d (subc_list c s l))
[PROOF STEP]
by (induct t and l rule: substt.induct substts.induct) simp_all


[STATEMENT]
lemma news_subcs: \<open>new_term d s \<Longrightarrow> news d z \<Longrightarrow> news d (subcs c s z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new_term d s; news d z\<rbrakk> \<Longrightarrow> news d (subcs c s z)
[PROOF STEP]
by (induct z) simp_all


[STATEMENT]
lemma psubst_new_free':
  \<open>c \<noteq> n \<Longrightarrow> new_term n (psubstt (id(n := c)) t)\<close>
  \<open>c \<noteq> n \<Longrightarrow> new_list n (psubstts (id(n := c)) l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c \<noteq> n \<Longrightarrow> new_term n (psubstt (id(n := c)) t)) &&& (c \<noteq> n \<Longrightarrow> new_list n (psubstts (id(n := c)) l))
[PROOF STEP]
by (induct t and l rule: paramst.induct paramsts.induct) simp_all


[STATEMENT]
lemma psubst_new_free: \<open>c \<noteq> n \<Longrightarrow> new n (psubst (id(n := c)) p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> n \<Longrightarrow> new n (psubst (id(n := c)) p)
[PROOF STEP]
using psubst_new_free'
[PROOF STATE]
proof (prove)
using this:
?c \<noteq> ?n \<Longrightarrow> new_term ?n (psubstt (id(?n := ?c)) ?t)
?c \<noteq> ?n \<Longrightarrow> new_list ?n (psubstts (id(?n := ?c)) ?l)

goal (1 subgoal):
 1. c \<noteq> n \<Longrightarrow> new n (psubst (id(n := c)) p)
[PROOF STEP]
by (induct p) fastforce+


[STATEMENT]
lemma map_psubst_new_free: \<open>c \<noteq> n \<Longrightarrow> news n (map (psubst (id(n := c))) z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> n \<Longrightarrow> news n (map (psubst (id(n := c))) z)
[PROOF STEP]
using psubst_new_free
[PROOF STATE]
proof (prove)
using this:
?c \<noteq> ?n \<Longrightarrow> new ?n (psubst (id(?n := ?c)) ?p)

goal (1 subgoal):
 1. c \<noteq> n \<Longrightarrow> news n (map (psubst (id(n := c))) z)
[PROOF STEP]
by (induct z) fastforce+


[STATEMENT]
lemma psubst_new_away' [simp]:
  \<open>new_term fresh t \<Longrightarrow> psubstt (id(fresh := c)) (psubstt (id(c := fresh)) t) = t\<close>
  \<open>new_list fresh l \<Longrightarrow> psubstts (id(fresh := c)) (psubstts (id(c := fresh)) l) = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term fresh t \<Longrightarrow> psubstt (id(fresh := c)) (psubstt (id(c := fresh)) t) = t) &&& (new_list fresh l \<Longrightarrow> psubstts (id(fresh := c)) (psubstts (id(c := fresh)) l) = l)
[PROOF STEP]
by (induct t and l rule: psubstt.induct psubstts.induct) auto


[STATEMENT]
lemma psubst_new_away [simp]: \<open>new fresh p \<Longrightarrow> psubst (id(fresh := c)) (psubst (id(c := fresh)) p) = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new fresh p \<Longrightarrow> psubst (id(fresh := c)) (psubst (id(c := fresh)) p) = p
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
lemma map_psubst_new_away:
  \<open>news fresh z \<Longrightarrow> map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z) = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news fresh z \<Longrightarrow> map (psubst (id(fresh := c))) (map (psubst (id(c := fresh))) z) = z
[PROOF STEP]
by (induct z) simp_all


[STATEMENT]
lemma psubst_new':
  \<open>new_term c t \<Longrightarrow> psubstt (id(c := x)) t = t\<close>
  \<open>new_list c l \<Longrightarrow> psubstts (id(c := x)) l = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c t \<Longrightarrow> psubstt (id(c := x)) t = t) &&& (new_list c l \<Longrightarrow> psubstts (id(c := x)) l = l)
[PROOF STEP]
by (induct t and l rule: psubstt.induct psubstts.induct) auto


[STATEMENT]
lemma psubst_new: \<open>new c p \<Longrightarrow> psubst (id(c := x)) p = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new c p \<Longrightarrow> psubst (id(c := x)) p = p
[PROOF STEP]
using psubst_new'
[PROOF STATE]
proof (prove)
using this:
new_term ?c ?t \<Longrightarrow> psubstt (id(?c := ?x)) ?t = ?t
new_list ?c ?l \<Longrightarrow> psubstts (id(?c := ?x)) ?l = ?l

goal (1 subgoal):
 1. new c p \<Longrightarrow> psubst (id(c := x)) p = p
[PROOF STEP]
by (induct p) fastforce+


[STATEMENT]
lemma map_psubst_new: \<open>news c z \<Longrightarrow> map (psubst (id(c := x))) z = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. news c z \<Longrightarrow> map (psubst (id(c := x))) z = z
[PROOF STEP]
using psubst_new
[PROOF STATE]
proof (prove)
using this:
new ?c ?p \<Longrightarrow> psubst (id(?c := ?x)) ?p = ?p

goal (1 subgoal):
 1. news c z \<Longrightarrow> map (psubst (id(c := x))) z = z
[PROOF STEP]
by (induct z) auto


[STATEMENT]
lemma lift_subst [simp]:
  \<open>liftt (substt t u m) = substt (liftt t) (liftt u) (m + 1)\<close>
  \<open>liftts (substts l u m) = substts (liftts l) (liftt u) (m + 1)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftt (t[u/m]) = liftt t[liftt u/m + 1] &&& liftts (l[u/m]) = liftts l[liftt u/m + 1]
[PROOF STEP]
by (induct t and l rule: substt.induct substts.induct) simp_all


[STATEMENT]
lemma new_subc_same' [simp]:
  \<open>new_term c s \<Longrightarrow> new_term c (subc_term c s t)\<close>
  \<open>new_term c s \<Longrightarrow> new_list c (subc_list c s l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c s \<Longrightarrow> new_term c (subc_term c s t)) &&& (new_term c s \<Longrightarrow> new_list c (subc_list c s l))
[PROOF STEP]
by (induct t and l rule: subc_term.induct subc_list.induct) simp_all


[STATEMENT]
lemma new_subc_same: \<open>new_term c s \<Longrightarrow> new c (subc c s p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_term c s \<Longrightarrow> new c (subc c s p)
[PROOF STEP]
by (induct p arbitrary: s) simp_all


[STATEMENT]
lemma lift_subc:
  \<open>liftt (subc_term c s t) = subc_term c (liftt s) (liftt t)\<close>
  \<open>liftts (subc_list c s l) = subc_list c (liftt s) (liftts l)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftt (subc_term c s t) = subc_term c (liftt s) (liftt t) &&& liftts (subc_list c s l) = subc_list c (liftt s) (liftts l)
[PROOF STEP]
by (induct t and l rule: liftt.induct liftts.induct) simp_all


[STATEMENT]
lemma new_subc_put':
  \<open>new_term c s \<Longrightarrow> subc_term c s (substt t u m) = subc_term c s (substt t (subc_term c s u) m)\<close>
  \<open>new_term c s \<Longrightarrow> subc_list c s (substts l u m) = subc_list c s (substts l (subc_term c s u) m)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c s \<Longrightarrow> subc_term c s (t[u/m]) = subc_term c s (t[subc_term c s u/m])) &&& (new_term c s \<Longrightarrow> subc_list c s (l[u/m]) = subc_list c s (l[subc_term c s u/m]))
[PROOF STEP]
by (induct t and l rule: subc_term.induct subc_list.induct) simp_all


[STATEMENT]
lemma subc_subst_new':
  \<open>new_term c u \<Longrightarrow> subc_term c (substt s u m) (substt t u m) = substt (subc_term c s t) u m\<close>
  \<open>new_term c u \<Longrightarrow> subc_list c (substt s u m) (substts l u m) = substts (subc_list c s l) u m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_term c u \<Longrightarrow> subc_term c (s[u/m]) (t[u/m]) = subc_term c s t[u/m]) &&& (new_term c u \<Longrightarrow> subc_list c (s[u/m]) (l[u/m]) = subc_list c s l[u/m])
[PROOF STEP]
by (induct t and l rule: subc_term.induct subc_list.induct) simp_all


[STATEMENT]
lemma subc_subst_new:
  \<open>new_term c t \<Longrightarrow> subc c (substt s t m) (subst p t m) = subst (subc c s p) t m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_term c t \<Longrightarrow> subc c (s[t/m]) (p[t/m]) = subc c s p[t/m]
[PROOF STEP]
using subc_subst_new'
[PROOF STATE]
proof (prove)
using this:
new_term ?c ?u \<Longrightarrow> subc_term ?c (?s[?u/?m]) (?t[?u/?m]) = subc_term ?c ?s ?t[?u/?m]
new_term ?c ?u \<Longrightarrow> subc_list ?c (?s[?u/?m]) (?l[?u/?m]) = subc_list ?c ?s ?l[?u/?m]

goal (1 subgoal):
 1. new_term c t \<Longrightarrow> subc c (s[t/m]) (p[t/m]) = subc c s p[t/m]
[PROOF STEP]
by (induct p arbitrary: m t s) fastforce+


[STATEMENT]
lemma subc_sub_0_new [simp]:
  \<open>new_term c t \<Longrightarrow> subc c s (subst p t 0) = subst (subc c (liftt s) p) t 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_term c t \<Longrightarrow> subc c s (p[t/0]) = subc c (liftt s) p[t/0]
[PROOF STEP]
using subc_subst_new subst_0_lift(1)
[PROOF STATE]
proof (prove)
using this:
new_term ?c ?t \<Longrightarrow> subc ?c (?s[?t/?m]) (?p[?t/?m]) = subc ?c ?s ?p[?t/?m]
liftt ?t[?s/0] = ?t

goal (1 subgoal):
 1. new_term c t \<Longrightarrow> subc c s (p[t/0]) = subc c (liftt s) p[t/0]
[PROOF STEP]
by metis


[STATEMENT]
lemma member_subc: \<open>p \<in> set z \<Longrightarrow> subc c s p \<in> set (subcs c s z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> set z \<Longrightarrow> subc c s p \<in> set (subcs c s z)
[PROOF STEP]
by (induct z) auto