[STATEMENT]
lemma fresh_trans_fm [simp]: "i \<sharp> trans_fm e A \<longleftrightarrow> i \<sharp> A \<or> i \<in> atom ` set e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sharp> trans_fm e A = (i \<sharp> A \<or> i \<in> atom ` set e)
[PROOF STEP]
by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base)


[STATEMENT]
lemma trans_fm_Conj [simp]: "trans_fm e (Conj A B) = DBConj (trans_fm e A) (trans_fm e B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans_fm e (A AND B) = DBConj (trans_fm e A) (trans_fm e B)
[PROOF STEP]
by (simp add: Conj_def)


[STATEMENT]
lemma trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) \<longleftrightarrow> t = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_tm e t = trans_tm e u) = (t = u)
[PROOF STEP]
proof (induct t arbitrary: e u rule: tm.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>e u. (trans_tm e Zero = trans_tm e u) = (Zero = u)
 2. \<And>x e u. (trans_tm e (Var x) = trans_tm e u) = (Var x = u)
 3. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
case Zero
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>e u. (trans_tm e Zero = trans_tm e u) = (Zero = u)
 2. \<And>x e u. (trans_tm e (Var x) = trans_tm e u) = (Var x = u)
 3. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_tm e Zero = trans_tm e u) = (Zero = u)
[PROOF STEP]
apply (cases u rule: tm.exhaust, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>u = Var x2; DBZero = lookup e 0 x2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(trans_tm e Zero = trans_tm e u) = (Zero = u)

goal (2 subgoals):
 1. \<And>x e u. (trans_tm e (Var x) = trans_tm e u) = (Var x = u)
 2. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x e u. (trans_tm e (Var x) = trans_tm e u) = (Var x = u)
 2. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
case (Var i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x e u. (trans_tm e (Var x) = trans_tm e u) = (Var x = u)
 2. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_tm e (Var i) = trans_tm e u) = (Var i = u)
[PROOF STEP]
apply (cases u rule: tm.exhaust, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>u = Zero; lookup e 0 i = DBZero\<rbrakk> \<Longrightarrow> False
 2. \<And>x31 x32. \<lbrakk>u = Eats x31 x32; lookup e 0 i = DBEats (trans_tm e x31) (trans_tm e x32)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32. \<lbrakk>u = Eats x31 x32; lookup e 0 i = DBEats (trans_tm e x31) (trans_tm e x32)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis dbtm.distinct(10) dbtm.distinct(11) lookup_in lookup_notin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(trans_tm e (Var i) = trans_tm e u) = (Var i = u)

goal (1 subgoal):
 1. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
case (Eats tm1 tm2)
[PROOF STATE]
proof (state)
this:
(trans_tm ?e tm1 = trans_tm ?e ?u) = (tm1 = ?u)
(trans_tm ?e tm2 = trans_tm ?e ?u) = (tm2 = ?u)

goal (1 subgoal):
 1. \<And>x1 x2a e u. \<lbrakk>\<And>e u. (trans_tm e x1 = trans_tm e u) = (x1 = u); \<And>e u. (trans_tm e x2a = trans_tm e u) = (x2a = u)\<rbrakk> \<Longrightarrow> (trans_tm e (Eats x1 x2a) = trans_tm e u) = (Eats x1 x2a = u)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(trans_tm ?e tm1 = trans_tm ?e ?u) = (tm1 = ?u)
(trans_tm ?e tm2 = trans_tm ?e ?u) = (tm2 = ?u)

goal (1 subgoal):
 1. (trans_tm e (Eats tm1 tm2) = trans_tm e u) = (Eats tm1 tm2 = u)
[PROOF STEP]
apply (cases u rule: tm.exhaust, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>u = Var x2; \<And>e u. (trans_tm e tm1 = trans_tm e u) = (tm1 = u); \<And>e u. (trans_tm e tm2 = trans_tm e u) = (tm2 = u); DBEats (trans_tm e tm1) (trans_tm e tm2) = lookup e 0 x2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis dbtm.distinct(12) dbtm.distinct(9) lookup_in lookup_notin)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(trans_tm e (Eats tm1 tm2) = trans_tm e u) = (Eats tm1 tm2 = u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm e A = trans_fm e B) = (A = B)
[PROOF STEP]
proof (nominal_induct A avoiding: e B rule: fm.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2 e B. (trans_fm e (x1 IN x2) = trans_fm e B) = (x1 IN x2 = B)
 2. \<And>x1 x2 e B. (trans_fm e (x1 EQ x2) = trans_fm e B) = (x1 EQ x2 = B)
 3. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 4. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 5. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
case (Mem tm1 tm2)
[PROOF STATE]
proof (state)
this:

goal (5 subgoals):
 1. \<And>x1 x2 e B. (trans_fm e (x1 IN x2) = trans_fm e B) = (x1 IN x2 = B)
 2. \<And>x1 x2 e B. (trans_fm e (x1 EQ x2) = trans_fm e B) = (x1 EQ x2 = B)
 3. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 4. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 5. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm e (tm1 IN tm2) = trans_fm e B) = (tm1 IN tm2 = B)
[PROOF STEP]
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
[PROOF STATE]
proof (state)
this:
(trans_fm e (tm1 IN tm2) = trans_fm e B) = (tm1 IN tm2 = B)

goal (4 subgoals):
 1. \<And>x1 x2 e B. (trans_fm e (x1 EQ x2) = trans_fm e B) = (x1 EQ x2 = B)
 2. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 3. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 4. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2 e B. (trans_fm e (x1 EQ x2) = trans_fm e B) = (x1 EQ x2 = B)
 2. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 3. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 4. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
case (Eq tm1 tm2)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>x1 x2 e B. (trans_fm e (x1 EQ x2) = trans_fm e B) = (x1 EQ x2 = B)
 2. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 3. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 4. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm e (tm1 EQ tm2) = trans_fm e B) = (tm1 EQ tm2 = B)
[PROOF STEP]
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
[PROOF STATE]
proof (state)
this:
(trans_fm e (tm1 EQ tm2) = trans_fm e B) = (tm1 EQ tm2 = B)

goal (3 subgoals):
 1. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 2. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 3. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 2. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 3. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
case (Disj fm1 fm2)
[PROOF STATE]
proof (state)
this:
(trans_fm ?b fm1 = trans_fm ?b ?ba) = (fm1 = ?ba)
(trans_fm ?b fm2 = trans_fm ?b ?ba) = (fm2 = ?ba)

goal (3 subgoals):
 1. \<And>x1 x2 e B. \<lbrakk>\<And>b ba. (trans_fm b x1 = trans_fm b ba) = (x1 = ba); \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (x1 OR x2) = trans_fm e B) = (x1 OR x2 = B)
 2. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 3. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm e (fm1 OR fm2) = trans_fm e B) = (fm1 OR fm2 = B)
[PROOF STEP]
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Disj fresh_star_def)
[PROOF STATE]
proof (state)
this:
(trans_fm e (fm1 OR fm2) = trans_fm e B) = (fm1 OR fm2 = B)

goal (2 subgoals):
 1. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 2. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 2. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
case (Neg fm)
[PROOF STATE]
proof (state)
this:
(trans_fm ?b fm = trans_fm ?b ?ba) = (fm = ?ba)

goal (2 subgoals):
 1. \<And>x e B. (\<And>b ba. (trans_fm b x = trans_fm b ba) = (x = ba)) \<Longrightarrow> (trans_fm e (Neg x) = trans_fm e B) = (Neg x = B)
 2. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm e (Neg fm) = trans_fm e B) = (Neg fm = B)
[PROOF STEP]
by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Neg fresh_star_def)
[PROOF STATE]
proof (state)
this:
(trans_fm e (Neg fm) = trans_fm e B) = (Neg fm = B)

goal (1 subgoal):
 1. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
case (Ex name fm)
[PROOF STATE]
proof (state)
this:
atom name \<sharp> e
atom name \<sharp> B
(trans_fm ?b fm = trans_fm ?b ?ba) = (fm = ?ba)

goal (1 subgoal):
 1. \<And>x1 x2 e B. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> B; \<And>b ba. (trans_fm b x2 = trans_fm b ba) = (x2 = ba)\<rbrakk> \<Longrightarrow> (trans_fm e (SyntaxN.Ex x1 x2) = trans_fm e B) = (SyntaxN.Ex x1 x2 = B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom name \<sharp> e
atom name \<sharp> B
(trans_fm ?b fm = trans_fm ?b ?ba) = (fm = ?ba)

goal (1 subgoal):
 1. (trans_fm e (SyntaxN.Ex name fm) = trans_fm e B) = (SyntaxN.Ex name fm = B)
[PROOF STEP]
using [[simproc del: alpha_lst]]
[PROOF STATE]
proof (prove)
using this:
atom name \<sharp> e
atom name \<sharp> B
(trans_fm ?b fm = trans_fm ?b ?ba) = (fm = ?ba)

goal (1 subgoal):
 1. (trans_fm e (SyntaxN.Ex name fm) = trans_fm e B) = (SyntaxN.Ex name fm = B)
[PROOF STEP]
proof (cases rule: fm.strong_exhaust [where y=B and c="(e, name)"], simp_all add: fresh_star_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x51 x52. \<lbrakk>atom name \<sharp> x52 \<or> name = x51; atom x51 \<sharp> (e, name); B = SyntaxN.Ex x51 x52; atom name \<sharp> e; \<And>b ba. (trans_fm b fm = trans_fm b ba) = (fm = ba)\<rbrakk> \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (x51 # e) x52) = ([[atom name]]lst. fm = [[atom x51]]lst. x52)
[PROOF STEP]
fix name'::name and fm'::fm
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x51 x52. \<lbrakk>atom name \<sharp> x52 \<or> name = x51; atom x51 \<sharp> (e, name); B = SyntaxN.Ex x51 x52; atom name \<sharp> e; \<And>b ba. (trans_fm b fm = trans_fm b ba) = (fm = ba)\<rbrakk> \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (x51 # e) x52) = ([[atom name]]lst. fm = [[atom x51]]lst. x52)
[PROOF STEP]
assume name': "atom name' \<sharp> (e, name)"
[PROOF STATE]
proof (state)
this:
atom name' \<sharp> (e, name)

goal (1 subgoal):
 1. \<And>x51 x52. \<lbrakk>atom name \<sharp> x52 \<or> name = x51; atom x51 \<sharp> (e, name); B = SyntaxN.Ex x51 x52; atom name \<sharp> e; \<And>b ba. (trans_fm b fm = trans_fm b ba) = (fm = ba)\<rbrakk> \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (x51 # e) x52) = ([[atom name]]lst. fm = [[atom x51]]lst. x52)
[PROOF STEP]
assume "atom name \<sharp> fm' \<or> name = name'"
[PROOF STATE]
proof (state)
this:
atom name \<sharp> fm' \<or> name = name'

goal (1 subgoal):
 1. \<And>x51 x52. \<lbrakk>atom name \<sharp> x52 \<or> name = x51; atom x51 \<sharp> (e, name); B = SyntaxN.Ex x51 x52; atom name \<sharp> e; \<And>b ba. (trans_fm b fm = trans_fm b ba) = (fm = ba)\<rbrakk> \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (x51 # e) x52) = ([[atom name]]lst. fm = [[atom x51]]lst. x52)
[PROOF STEP]
thus "(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')"
         (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
using this:
atom name \<sharp> fm' \<or> name = name'

goal (1 subgoal):
 1. (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
proof (rule disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
 2. name = name' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
assume "name = name'"
[PROOF STATE]
proof (state)
this:
name = name'

goal (2 subgoals):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
 2. name = name' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
thus "?lhs = ?rhs"
[PROOF STATE]
proof (prove)
using this:
name = name'

goal (1 subgoal):
 1. (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
by (metis fresh_Pair fresh_at_base(2) name')
[PROOF STATE]
proof (state)
this:
(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')

goal (1 subgoal):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
assume name: "atom name \<sharp> fm'"
[PROOF STATE]
proof (state)
this:
atom name \<sharp> fm'

goal (1 subgoal):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
have eq1: "(name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'
[PROOF STEP]
by (simp add: flip_fresh_fresh name)
[PROOF STATE]
proof (state)
this:
(name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'

goal (1 subgoal):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
have eq2: "(name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'
[PROOF STEP]
by (rule flip_fresh_fresh) (auto simp: Abs_fresh_iff name)
[PROOF STATE]
proof (state)
this:
(name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'

goal (1 subgoal):
 1. atom name \<sharp> fm' \<Longrightarrow> (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
show "?lhs = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
using name' eq1 eq2 Ex(1) Ex(3) [of "name#e" "(name \<leftrightarrow> name') \<bullet> fm'"]
[PROOF STATE]
proof (prove)
using this:
atom name' \<sharp> (e, name)
(name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'
(name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'
atom name \<sharp> e
(trans_fm (name # e) fm = trans_fm (name # e) ((name \<leftrightarrow> name') \<bullet> fm')) = (fm = (name \<leftrightarrow> name') \<bullet> fm')

goal (1 subgoal):
 1. (trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')
[PROOF STEP]
by (simp add: flip_fresh_fresh) (metis Abs1_eq(3))
[PROOF STATE]
proof (state)
this:
(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(trans_fm e (SyntaxN.Ex name fm) = trans_fm e B) = (SyntaxN.Ex name fm = B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trans_fm_perm:
  assumes c: "atom c \<sharp> (i,j,A,B)"
  and     t: "trans_fm [i] A = trans_fm [j] B"
  shows "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
have c_fresh1: "atom c \<sharp> trans_fm [i] A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom c \<sharp> trans_fm [i] A
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
atom c \<sharp> (i, j, A, B)

goal (1 subgoal):
 1. atom c \<sharp> trans_fm [i] A
[PROOF STEP]
by (auto simp: supp_Pair)
[PROOF STATE]
proof (state)
this:
atom c \<sharp> trans_fm [i] A

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom c \<sharp> trans_fm [i] A

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
have i_fresh: "atom i \<sharp> trans_fm [i] A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> trans_fm [i] A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom i \<sharp> trans_fm [i] A

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom i \<sharp> trans_fm [i] A

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
have c_fresh2: "atom c \<sharp> trans_fm [j] B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom c \<sharp> trans_fm [j] B
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
atom c \<sharp> (i, j, A, B)

goal (1 subgoal):
 1. atom c \<sharp> trans_fm [j] B
[PROOF STEP]
by (auto simp: supp_Pair)
[PROOF STATE]
proof (state)
this:
atom c \<sharp> trans_fm [j] B

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom c \<sharp> trans_fm [j] B

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
have j_fresh: "atom j \<sharp> trans_fm [j] B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> trans_fm [j] B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom j \<sharp> trans_fm [j] B

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom c \<sharp> trans_fm [i] A
atom i \<sharp> trans_fm [i] A
atom c \<sharp> trans_fm [j] B
atom j \<sharp> trans_fm [j] B
[PROOF STEP]
have "((i \<leftrightarrow> c) \<bullet> (trans_fm [i] A)) = ((j \<leftrightarrow> c) \<bullet> trans_fm [j] B)"
[PROOF STATE]
proof (prove)
using this:
atom c \<sharp> trans_fm [i] A
atom i \<sharp> trans_fm [i] A
atom c \<sharp> trans_fm [j] B
atom j \<sharp> trans_fm [j] B

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> trans_fm [i] A = (j \<leftrightarrow> c) \<bullet> trans_fm [j] B
[PROOF STEP]
by (simp only: flip_fresh_fresh t)
[PROOF STATE]
proof (state)
this:
(i \<leftrightarrow> c) \<bullet> trans_fm [i] A = (j \<leftrightarrow> c) \<bullet> trans_fm [j] B

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i \<leftrightarrow> c) \<bullet> trans_fm [i] A = (j \<leftrightarrow> c) \<bullet> trans_fm [j] B
[PROOF STEP]
have "trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)"
[PROOF STATE]
proof (prove)
using this:
(i \<leftrightarrow> c) \<bullet> trans_fm [i] A = (j \<leftrightarrow> c) \<bullet> trans_fm [j] B

goal (1 subgoal):
 1. trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)
[PROOF STEP]
show "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B"
[PROOF STATE]
proof (prove)
using this:
trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)

goal (1 subgoal):
 1. (i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_dbtm_imp_is_tm:
  assumes "wf_dbtm x"
  shows "\<exists>t::tm. x = trans_tm [] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. x = trans_tm [] t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dbtm x

goal (1 subgoal):
 1. \<exists>t. x = trans_tm [] t
[PROOF STEP]
proof (induct rule: wf_dbtm.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<exists>t. DBZero = trans_tm [] t
 2. \<And>name. \<exists>t. DBVar name = trans_tm [] t
 3. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
case Zero
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<exists>t. DBZero = trans_tm [] t
 2. \<And>name. \<exists>t. DBVar name = trans_tm [] t
 3. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. DBZero = trans_tm [] t
[PROOF STEP]
by (metis trans_tm.simps(1))
[PROOF STATE]
proof (state)
this:
\<exists>t. DBZero = trans_tm [] t

goal (2 subgoals):
 1. \<And>name. \<exists>t. DBVar name = trans_tm [] t
 2. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>name. \<exists>t. DBVar name = trans_tm [] t
 2. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
case (Var i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>name. \<exists>t. DBVar name = trans_tm [] t
 2. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. DBVar i = trans_tm [] t
[PROOF STEP]
by (metis lookup.simps(1) trans_tm.simps(2))
[PROOF STATE]
proof (state)
this:
\<exists>t. DBVar i = trans_tm [] t

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
case (Eats dt1 dt2)
[PROOF STATE]
proof (state)
this:
wf_dbtm dt1
\<exists>t. dt1 = trans_tm [] t
wf_dbtm dt2
\<exists>t. dt2 = trans_tm [] t

goal (1 subgoal):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; \<exists>t. t1 = trans_tm [] t; wf_dbtm t2; \<exists>t. t2 = trans_tm [] t\<rbrakk> \<Longrightarrow> \<exists>t. DBEats t1 t2 = trans_tm [] t
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbtm dt1
\<exists>t. dt1 = trans_tm [] t
wf_dbtm dt2
\<exists>t. dt2 = trans_tm [] t

goal (1 subgoal):
 1. \<exists>t. DBEats dt1 dt2 = trans_tm [] t
[PROOF STEP]
by (metis trans_tm.simps(3))
[PROOF STATE]
proof (state)
this:
\<exists>t. DBEats dt1 dt2 = trans_tm [] t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_dbtm_trans_tm: "wf_dbtm (trans_tm [] t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dbtm (trans_tm [] t)
[PROOF STEP]
by (induct t rule: tm.induct) auto


[STATEMENT]
theorem wf_dbtm_iff_is_tm: "wf_dbtm x \<longleftrightarrow> (\<exists>t::tm. x = trans_tm [] t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dbtm x = (\<exists>t. x = trans_tm [] t)
[PROOF STEP]
by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm)


[STATEMENT]
lemma fresh_iff_non_subst_dbtm: "subst_dbtm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_dbtm DBZero i t = t) = atom i \<sharp> t
[PROOF STEP]
by (induct t rule: dbtm.induct) (auto simp: pure_fresh fresh_at_base(2))


[STATEMENT]
lemma lookup_append: "lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)
[PROOF STEP]
by (induct e arbitrary: n) (auto simp: fresh_Cons)


[STATEMENT]
lemma trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans_tm (e @ [name]) t = abst_dbtm name (length e) (trans_tm e t)
[PROOF STEP]
by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append)


[STATEMENT]
lemma fresh_iff_non_subst_dbfm: "subst_dbfm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (subst_dbfm DBZero i t = t) = atom i \<sharp> t
[PROOF STEP]
by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm)


[STATEMENT]
lemma atom_fresh_abst_dbtm [simp]: "atom i \<sharp> abst_dbtm i n t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> abst_dbtm i n t
[PROOF STEP]
by (induct t rule: dbtm.induct) (auto simp: pure_fresh)


[STATEMENT]
lemma trans_fm_abs: "trans_fm (e@[name]) A = abst_dbfm name (length e) (trans_fm e A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans_fm (e @ [name]) A = abst_dbfm name (length e) (trans_fm e A)
[PROOF STEP]
apply (nominal_induct A avoiding: name e rule: fm.strong_induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 name e. trans_fm (e @ [name]) (x1 IN x2) = abst_dbfm name (length e) (trans_fm e (x1 IN x2))
 2. \<And>x1 x2 name e. trans_fm (e @ [name]) (x1 EQ x2) = abst_dbfm name (length e) (trans_fm e (x1 EQ x2))
 3. \<And>x1 x2 name e. \<lbrakk>\<And>b ba. trans_fm (ba @ [b]) x1 = abst_dbfm b (length ba) (trans_fm ba x1); \<And>b ba. trans_fm (ba @ [b]) x2 = abst_dbfm b (length ba) (trans_fm ba x2)\<rbrakk> \<Longrightarrow> trans_fm (e @ [name]) (x1 OR x2) = abst_dbfm name (length e) (trans_fm e (x1 OR x2))
 4. \<And>x name e. (\<And>b ba. trans_fm (ba @ [b]) x = abst_dbfm b (length ba) (trans_fm ba x)) \<Longrightarrow> trans_fm (e @ [name]) (Neg x) = abst_dbfm name (length e) (trans_fm e (Neg x))
 5. \<And>x1 x2 name e. \<lbrakk>atom x1 \<sharp> name; atom x1 \<sharp> e; \<And>b ba. trans_fm (ba @ [b]) x2 = abst_dbfm b (length ba) (trans_fm ba x2)\<rbrakk> \<Longrightarrow> trans_fm (e @ [name]) (SyntaxN.Ex x1 x2) = abst_dbfm name (length e) (trans_fm e (SyntaxN.Ex x1 x2))
[PROOF STEP]
apply (auto simp: trans_tm_abs fresh_Cons fresh_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 name e. \<lbrakk>atom x1 \<sharp> name; atom x1 \<sharp> e; \<And>b ba. trans_fm (ba @ [b]) x2 = abst_dbfm b (length ba) (trans_fm ba x2)\<rbrakk> \<Longrightarrow> trans_fm (x1 # e @ [name]) x2 = abst_dbfm name (Suc (length e)) (trans_fm (x1 # e) x2)
[PROOF STEP]
apply (metis One_nat_def Suc_eq_plus1 append_Cons list.size(4))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma abst_trans_fm: "abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A
[PROOF STEP]
by (metis append_Nil list.size(3) trans_fm_abs)


[STATEMENT]
lemma abst_trans_fm2: "i \<noteq> j \<Longrightarrow> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j,i] A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j, i] A
[PROOF STEP]
using trans_fm_abs [where e="[j]" and name=i]
[PROOF STATE]
proof (prove)
using this:
trans_fm ([j] @ [i]) ?A = abst_dbfm i (length [j]) (trans_fm [j] ?A)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j, i] A
[PROOF STEP]
by auto


[STATEMENT]
lemma wf_dbfm_imp_is_fm:
  assumes "wf_dbfm x" shows "\<exists>A::fm. x = trans_fm [] A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. x = trans_fm [] A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_dbfm x

goal (1 subgoal):
 1. \<exists>A. x = trans_fm [] A
[PROOF STEP]
proof (induct rule: wf_dbfm.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBMem t1 t2 = trans_fm [] A
 2. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBEq t1 t2 = trans_fm [] A
 3. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 4. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 5. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
case (Mem t1 t2)
[PROOF STATE]
proof (state)
this:
wf_dbtm t1
wf_dbtm t2

goal (5 subgoals):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBMem t1 t2 = trans_fm [] A
 2. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBEq t1 t2 = trans_fm [] A
 3. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 4. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 5. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbtm t1
wf_dbtm t2

goal (1 subgoal):
 1. \<exists>A. DBMem t1 t2 = trans_fm [] A
[PROOF STEP]
by (metis trans_fm.simps(1) wf_dbtm_imp_is_tm)
[PROOF STATE]
proof (state)
this:
\<exists>A. DBMem t1 t2 = trans_fm [] A

goal (4 subgoals):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBEq t1 t2 = trans_fm [] A
 2. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 3. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 4. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBEq t1 t2 = trans_fm [] A
 2. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 3. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 4. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
case (Eq t1 t2)
[PROOF STATE]
proof (state)
this:
wf_dbtm t1
wf_dbtm t2

goal (4 subgoals):
 1. \<And>t1 t2. \<lbrakk>wf_dbtm t1; wf_dbtm t2\<rbrakk> \<Longrightarrow> \<exists>A. DBEq t1 t2 = trans_fm [] A
 2. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 3. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 4. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbtm t1
wf_dbtm t2

goal (1 subgoal):
 1. \<exists>A. DBEq t1 t2 = trans_fm [] A
[PROOF STEP]
by (metis trans_fm.simps(2) wf_dbtm_imp_is_tm)
[PROOF STATE]
proof (state)
this:
\<exists>A. DBEq t1 t2 = trans_fm [] A

goal (3 subgoals):
 1. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 2. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 3. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 2. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 3. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
case (Disj fm1 fm2)
[PROOF STATE]
proof (state)
this:
wf_dbfm fm1
\<exists>A. fm1 = trans_fm [] A
wf_dbfm fm2
\<exists>A. fm2 = trans_fm [] A

goal (3 subgoals):
 1. \<And>A1 A2. \<lbrakk>wf_dbfm A1; \<exists>A. A1 = trans_fm [] A; wf_dbfm A2; \<exists>A. A2 = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>A. DBDisj A1 A2 = trans_fm [] A
 2. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 3. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbfm fm1
\<exists>A. fm1 = trans_fm [] A
wf_dbfm fm2
\<exists>A. fm2 = trans_fm [] A

goal (1 subgoal):
 1. \<exists>A. DBDisj fm1 fm2 = trans_fm [] A
[PROOF STEP]
by (metis trans_fm.simps(3))
[PROOF STATE]
proof (state)
this:
\<exists>A. DBDisj fm1 fm2 = trans_fm [] A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 2. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 2. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
case (Neg fm)
[PROOF STATE]
proof (state)
this:
wf_dbfm fm
\<exists>A. fm = trans_fm [] A

goal (2 subgoals):
 1. \<And>A. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBNeg A = trans_fm [] Aa
 2. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbfm fm
\<exists>A. fm = trans_fm [] A

goal (1 subgoal):
 1. \<exists>A. DBNeg fm = trans_fm [] A
[PROOF STEP]
by (metis trans_fm.simps(4))
[PROOF STATE]
proof (state)
this:
\<exists>A. DBNeg fm = trans_fm [] A

goal (1 subgoal):
 1. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
case (Ex fm name)
[PROOF STATE]
proof (state)
this:
wf_dbfm fm
\<exists>A. fm = trans_fm [] A

goal (1 subgoal):
 1. \<And>A name. \<lbrakk>wf_dbfm A; \<exists>Aa. A = trans_fm [] Aa\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 A) = trans_fm [] Aa
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
wf_dbfm fm
\<exists>A. fm = trans_fm [] A

goal (1 subgoal):
 1. \<exists>A. DBEx (abst_dbfm name 0 fm) = trans_fm [] A
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>wf_dbfm (trans_fm [] A); fm = trans_fm [] A\<rbrakk> \<Longrightarrow> \<exists>Aa. DBEx (abst_dbfm name 0 (trans_fm [] A)) = trans_fm [] Aa
[PROOF STEP]
apply (rule_tac x="Ex name A" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>wf_dbfm (trans_fm [] A); fm = trans_fm [] A\<rbrakk> \<Longrightarrow> DBEx (abst_dbfm name 0 (trans_fm [] A)) = trans_fm [] (SyntaxN.Ex name A)
[PROOF STEP]
apply (auto simp: abst_trans_fm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>A. DBEx (abst_dbfm name 0 fm) = trans_fm [] A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_dbfm_trans_fm: "wf_dbfm (trans_fm [] A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dbfm (trans_fm [] A)
[PROOF STEP]
apply (nominal_induct A rule: fm.strong_induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2. wf_dbfm (trans_fm [] (x1 IN x2))
 2. \<And>x1 x2. wf_dbfm (trans_fm [] (x1 EQ x2))
 3. \<And>x1 x2. \<lbrakk>wf_dbfm (trans_fm [] x1); wf_dbfm (trans_fm [] x2)\<rbrakk> \<Longrightarrow> wf_dbfm (trans_fm [] (x1 OR x2))
 4. \<And>x. wf_dbfm (trans_fm [] x) \<Longrightarrow> wf_dbfm (trans_fm [] (Neg x))
 5. \<And>x1 x2. wf_dbfm (trans_fm [] x2) \<Longrightarrow> wf_dbfm (trans_fm [] (SyntaxN.Ex x1 x2))
[PROOF STEP]
apply (auto simp: wf_dbtm_trans_tm abst_trans_fm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. wf_dbfm (trans_fm [] x2) \<Longrightarrow> wf_dbfm (DBEx (trans_fm [x1] x2))
[PROOF STEP]
apply (metis abst_trans_fm wf_dbfm.Ex)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_dbfm_iff_is_fm: "wf_dbfm x \<longleftrightarrow> (\<exists>A::fm. x = trans_fm [] A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_dbfm x = (\<exists>A. x = trans_fm [] A)
[PROOF STEP]
by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm)


[STATEMENT]
lemma dbtm_abst_ignore [simp]:
  "abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t
[PROOF STEP]
by (induct t rule: dbtm.induct) auto


[STATEMENT]
lemma abst_dbtm_fresh_ignore [simp]: "atom name \<sharp> u \<Longrightarrow> abst_dbtm name j u = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom name \<sharp> u \<Longrightarrow> abst_dbtm name j u = u
[PROOF STEP]
by (induct u rule: dbtm.induct) auto


[STATEMENT]
lemma dbtm_subst_ignore [simp]:
  "subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t
[PROOF STEP]
by (induct t rule: dbtm.induct) auto


[STATEMENT]
lemma dbtm_abst_swap_subst:
  "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
   subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>name \<noteq> name'; atom name' \<sharp> u\<rbrakk> \<Longrightarrow> subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)
[PROOF STEP]
by (induct t rule: dbtm.induct) auto


[STATEMENT]
lemma dbfm_abst_swap_subst:
  "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
   subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>name \<noteq> name'; atom name' \<sharp> u\<rbrakk> \<Longrightarrow> subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)
[PROOF STEP]
by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst)


[STATEMENT]
lemma subst_trans_commute [simp]:
  "atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)
[PROOF STEP]
apply (induct t rule: tm.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e Zero) = trans_tm e (subst i u Zero)
 2. \<And>x. atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e (Var x)) = trans_tm e (subst i u (Var x))
 3. \<And>x1 x2a. \<lbrakk>atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e x1) = trans_tm e (subst i u x1); atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e x2a) = trans_tm e (subst i u x2a); atom i \<sharp> e\<rbrakk> \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e (Eats x1 x2a)) = trans_tm e (subst i u (Eats x1 x2a))
[PROOF STEP]
apply (auto simp: lookup_notin fresh_imp_notin_env)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>atom i \<sharp> e; i \<noteq> x\<rbrakk> \<Longrightarrow> subst_dbtm (trans_tm e u) i (lookup e 0 x) = lookup e 0 x
[PROOF STEP]
apply (metis abst_dbtm_fresh_ignore dbtm_subst_ignore lookup_fresh lookup_notin subst_dbtm.simps(2))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subst_fm_trans_commute [simp]:
  "subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A (name::= u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A(name::=u))
[PROOF STEP]
apply (nominal_induct A avoiding: name u rule: fm.strong_induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 name u. subst_dbfm (trans_tm [] u) name (trans_fm [] (x1 IN x2)) = trans_fm [] ((x1 IN x2)(name::=u))
 2. \<And>x1 x2 name u. subst_dbfm (trans_tm [] u) name (trans_fm [] (x1 EQ x2)) = trans_fm [] ((x1 EQ x2)(name::=u))
 3. \<And>x1 x2 name u. \<lbrakk>\<And>b ba. subst_dbfm (trans_tm [] ba) b (trans_fm [] x1) = trans_fm [] (x1(b::=ba)); \<And>b ba. subst_dbfm (trans_tm [] ba) b (trans_fm [] x2) = trans_fm [] (x2(b::=ba))\<rbrakk> \<Longrightarrow> subst_dbfm (trans_tm [] u) name (trans_fm [] (x1 OR x2)) = trans_fm [] ((x1 OR x2)(name::=u))
 4. \<And>x name u. (\<And>b ba. subst_dbfm (trans_tm [] ba) b (trans_fm [] x) = trans_fm [] (x(b::=ba))) \<Longrightarrow> subst_dbfm (trans_tm [] u) name (trans_fm [] (Neg x)) = trans_fm [] ((Neg x)(name::=u))
 5. \<And>x1 x2 name u. \<lbrakk>atom x1 \<sharp> name; atom x1 \<sharp> u; \<And>b ba. subst_dbfm (trans_tm [] ba) b (trans_fm [] x2) = trans_fm [] (x2(b::=ba))\<rbrakk> \<Longrightarrow> subst_dbfm (trans_tm [] u) name (trans_fm [] (SyntaxN.Ex x1 x2)) = trans_fm [] ((SyntaxN.Ex x1 x2)(name::=u))
[PROOF STEP]
apply (auto simp: lookup_notin abst_trans_fm [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 name u. \<lbrakk>atom x1 \<sharp> name; atom x1 \<sharp> u; \<And>b ba. subst_dbfm (trans_tm [] ba) b (trans_fm [] x2) = trans_fm [] (x2(b::=ba))\<rbrakk> \<Longrightarrow> subst_dbfm (trans_tm [] u) name (abst_dbfm x1 0 (trans_fm [] x2)) = abst_dbfm x1 0 (trans_fm [] (x2(name::=u)))
[PROOF STEP]
apply (metis dbfm_abst_swap_subst fresh_at_base(2) fresh_trans_tm_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma subst_fm_trans_commute_eq:
  "du = trans_tm [] u \<Longrightarrow> subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. du = trans_tm [] u \<Longrightarrow> subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))
[PROOF STEP]
by (metis subst_fm_trans_commute)


[STATEMENT]
lemma fresh_HTuple [simp]: "x \<sharp> HTuple n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> HTuple n
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma HTuple_eqvt[eqvt]: "(p \<bullet> HTuple n) = HTuple (p \<bullet> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> HTuple n = HTuple (p \<bullet> n)
[PROOF STEP]
by (induct n, auto simp: HPair_eqvt permute_pure)


[STATEMENT]
lemma nat_of_name_inject [simp]: "nat_of_name n1 = nat_of_name n2 \<longleftrightarrow> n1 = n2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (nat_of_name n1 = nat_of_name n2) = (n1 = n2)
[PROOF STEP]
by (metis nat_of_name_def atom_components_eq_iff atom_eq_iff sort_of_atom_eq)


[STATEMENT]
lemma nat_of_name_Abs_eq [simp]: "nat_of_name (Abs_name (Atom (Sort ''SyntaxN.name'' []) n)) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_of_name (Abs_name (Atom (Sort ''SyntaxN.name'' []) n)) = n
[PROOF STEP]
by (auto simp: nat_of_name_def atom_name_def Abs_name_inverse)


[STATEMENT]
lemma nat_of_name_name_eq [simp]: "nat_of_name (name_of_nat n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat_of_name (name_of_nat n) = n
[PROOF STEP]
by (simp add: name_of_nat_def)


[STATEMENT]
lemma name_of_nat_nat_of_name [simp]: "name_of_nat (nat_of_name i) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. name_of_nat (nat_of_name i) = i
[PROOF STEP]
by (metis nat_of_name_inject nat_of_name_name_eq)


[STATEMENT]
lemma HPair_neq_ORD_OF [simp]: "HPair x y \<noteq> ORD_OF i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HPair x y \<noteq> ORD_OF i
[PROOF STEP]
by (metis HPair_def ORD_OF.elims SUCC_def tm.distinct(3) tm.eq_iff(3))


[STATEMENT]
lemma HTuple_minus_1: "n > 0 \<Longrightarrow> HTuple n = HPair Zero (HTuple (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> HTuple n = HPair Zero (HTuple (n - 1))
[PROOF STEP]
by (metis Suc_diff_1 HTuple.simps(2))


[STATEMENT]
lemma quot_dbtm_fresh [simp]: "s \<sharp> (quot_dbtm t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<sharp> quot_dbtm t
[PROOF STEP]
by (induct t rule: dbtm.induct) auto


[STATEMENT]
lemma quot_tm_fresh [simp]: fixes t::tm shows "s \<sharp> \<guillemotleft>t\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<sharp> \<guillemotleft>t\<guillemotright>
[PROOF STEP]
by (simp add: quot_tm_def)


[STATEMENT]
lemma quot_Zero [simp]: "\<guillemotleft>Zero\<guillemotright> = Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>Zero\<guillemotright> = Zero
[PROOF STEP]
by (simp add: quot_tm_def)


[STATEMENT]
lemma quot_Var: "\<guillemotleft>Var x\<guillemotright> = SUCC (ORD_OF (nat_of_name x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>Var x\<guillemotright> = SUCC (ORD_OF (nat_of_name x))
[PROOF STEP]
by (simp add: quot_tm_def)


[STATEMENT]
lemma quot_Eats: "\<guillemotleft>Eats x y\<guillemotright> = HPair (HTuple 1) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>Eats x y\<guillemotright> = HPair (HTuple 1) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)
[PROOF STEP]
by (simp add: quot_tm_def)


[STATEMENT]
lemma quot_dbfm_fresh [simp]: "s \<sharp> (quot_dbfm A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<sharp> quot_dbfm A
[PROOF STEP]
by (induct A rule: dbfm.induct) auto


[STATEMENT]
lemma quot_fm_fresh [simp]: fixes A::fm shows "s \<sharp> \<guillemotleft>A\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<sharp> \<guillemotleft>A\<guillemotright>
[PROOF STEP]
by (simp add: quot_fm_def)


[STATEMENT]
lemma quot_fm_permute [simp]: fixes A:: fm shows "p \<bullet> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A\<guillemotright>
[PROOF STEP]
by (metis fresh_star_def perm_supp_eq quot_fm_fresh)


[STATEMENT]
lemma quot_Mem: "\<guillemotleft>x IN y\<guillemotright> = HPair (HTuple 0) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>x IN y\<guillemotright> = HPair (HTuple 0) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)
[PROOF STEP]
by (simp add: quot_fm_def quot_tm_def)


[STATEMENT]
lemma quot_Eq: "\<guillemotleft>x EQ y\<guillemotright> = HPair (HTuple 2) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>x EQ y\<guillemotright> = HPair (HTuple 2) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)
[PROOF STEP]
by (simp add: quot_fm_def quot_tm_def)


[STATEMENT]
lemma quot_Disj: "\<guillemotleft>A OR B\<guillemotright> = HPair (HTuple 3) (HPair (\<guillemotleft>A\<guillemotright>) (\<guillemotleft>B\<guillemotright>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>A OR B\<guillemotright> = HPair (HTuple 3) (HPair \<guillemotleft>A\<guillemotright> \<guillemotleft>B\<guillemotright>)
[PROOF STEP]
by (simp add: quot_fm_def)


[STATEMENT]
lemma quot_Neg: "\<guillemotleft>Neg A\<guillemotright> = HPair (HTuple 4) (\<guillemotleft>A\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>Neg A\<guillemotright> = HPair (HTuple 4) \<guillemotleft>A\<guillemotright>
[PROOF STEP]
by (simp add: quot_fm_def)


[STATEMENT]
lemma quot_Ex: "\<guillemotleft>Ex i A\<guillemotright> = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>SyntaxN.Ex i A\<guillemotright> = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))
[PROOF STEP]
by (simp add: quot_fm_def)


[STATEMENT]
lemma quot_Succ: "\<guillemotleft>SUCC x\<guillemotright> = Q_Succ \<guillemotleft>x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>SUCC x\<guillemotright> = Q_Succ \<guillemotleft>x\<guillemotright>
[PROOF STEP]
by (auto simp: SUCC_def quot_Eats)


[STATEMENT]
lemma quot_subst_eq: "\<guillemotleft>A(i::=t)\<guillemotright> = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>A(i::=t)\<guillemotright> = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))
[PROOF STEP]
by (metis quot_fm_def subst_fm_trans_commute)


[STATEMENT]
lemma Q_Succ_cong: "H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> Q_Succ x EQ Q_Succ x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> Q_Succ x EQ Q_Succ x'
[PROOF STEP]
by (metis HPair_cong Refl)


[STATEMENT]
lemma coding_tm_Zero [intro]: "coding_tm Zero"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm Zero
[PROOF STEP]
by (metis ORD_OF.simps(1) Ord)


[STATEMENT]
lemma coding_tm_HTuple [intro]: "coding_tm (HTuple k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm (HTuple k)
[PROOF STEP]
by (induct k, auto)


[STATEMENT]
lemma quot_dbtm_coding [simp]: "coding_tm (quot_dbtm t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm (quot_dbtm t)
[PROOF STEP]
apply (induct t rule: dbtm.induct, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. coding_tm (SUCC (ORD_OF (nat_of_name x)))
[PROOF STEP]
apply (metis ORD_OF.simps(2) Ord)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma quot_dbfm_coding [simp]: "coding_tm (quot_dbfm fm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm (quot_dbfm fm)
[PROOF STEP]
by (induct fm rule: dbfm.induct, auto)


[STATEMENT]
lemma quot_fm_coding: fixes A::fm shows "coding_tm \<guillemotleft>A\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm \<guillemotleft>A\<guillemotright>
[PROOF STEP]
by (metis quot_dbfm_coding quot_fm_def)


[STATEMENT]
lemma fresh_vquot_dbtm [simp]: "i \<sharp> vquot_dbtm V tm \<longleftrightarrow> i \<sharp> tm \<or> i \<notin> atom ` V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sharp> vquot_dbtm V tm = (i \<sharp> tm \<or> i \<notin> atom ` V)
[PROOF STEP]
by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh)


[STATEMENT]
lemma fresh_vquot_dbfm [simp]: "i \<sharp> vquot_dbfm V fm \<longleftrightarrow> i \<sharp> fm \<or> i \<notin> atom ` V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sharp> vquot_dbfm V fm = (i \<sharp> fm \<or> i \<notin> atom ` V)
[PROOF STEP]
by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1)


[STATEMENT]
lemma vquot_dbtm_empty [simp]: "vquot_dbtm {} t = quot_dbtm t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vquot_dbtm {} t = quot_dbtm t
[PROOF STEP]
by (induct t rule: dbtm.induct) auto


[STATEMENT]
lemma vquot_tm_empty [simp]: fixes t::tm shows "\<lfloor>t\<rfloor>{} = \<guillemotleft>t\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>t\<rfloor>{} = \<guillemotleft>t\<guillemotright>
[PROOF STEP]
by (simp add: vquot_tm_def quot_tm_def)


[STATEMENT]
lemma vquot_dbtm_eq: "atom ` V \<inter> supp t = atom ` W \<inter> supp t \<Longrightarrow> vquot_dbtm V t = vquot_dbtm W t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` V \<inter> supp t = atom ` W \<inter> supp t \<Longrightarrow> vquot_dbtm V t = vquot_dbtm W t
[PROOF STEP]
by (induct t rule: dbtm.induct) (auto simp: image_iff, blast+)


[STATEMENT]
lemma vquot_fm_fresh [simp]: fixes A::fm shows "i \<sharp> \<lfloor>A\<rfloor>V \<longleftrightarrow> i \<sharp> A \<or> i \<notin> atom ` V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<sharp> \<lfloor>A\<rfloor>V = (i \<sharp> A \<or> i \<notin> atom ` V)
[PROOF STEP]
by (simp add: vquot_fm_def)


[STATEMENT]
lemma vquot_dbfm_empty [simp]: "vquot_dbfm {} A = quot_dbfm A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vquot_dbfm {} A = quot_dbfm A
[PROOF STEP]
by (induct A rule: dbfm.induct) auto


[STATEMENT]
lemma vquot_fm_empty [simp]: fixes A::fm shows "\<lfloor>A\<rfloor>{} = \<guillemotleft>A\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>A\<rfloor>{} = \<guillemotleft>A\<guillemotright>
[PROOF STEP]
by (simp add: vquot_fm_def quot_fm_def)


[STATEMENT]
lemma vquot_dbfm_eq: "atom ` V \<inter> supp A = atom ` W \<inter> supp A \<Longrightarrow> vquot_dbfm V A = vquot_dbfm W A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom ` V \<inter> supp A = atom ` W \<inter> supp A \<Longrightarrow> vquot_dbfm V A = vquot_dbfm W A
[PROOF STEP]
by (induct A rule: dbfm.induct) (auto simp: intro!: vquot_dbtm_eq, blast+)


[STATEMENT]
lemma vquot_fm_insert:
  fixes A::fm shows "atom i \<notin> supp A \<Longrightarrow> \<lfloor>A\<rfloor>(insert i V) = \<lfloor>A\<rfloor>V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<notin> supp A \<Longrightarrow> \<lfloor>A\<rfloor>(insert i V) = \<lfloor>A\<rfloor>V
[PROOF STEP]
by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq)


[STATEMENT]
lemma coeff_int_eq_0: "i < 0 \<or> i > int (degree p) \<Longrightarrow> coeff_int p i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < 0 \<or> int (degree p) < i \<Longrightarrow> coeff_int p i = (0::'a)
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < 0 \<or> int (degree p) < i \<Longrightarrow> (if i < 0 then 0::'a else coeff p (nat i)) = (0::'a)
[PROOF STEP]
by (cases "i < 0", auto intro: coeff_eq_0)


[STATEMENT]
lemma coeff_int_smult[simp]: "coeff_int (smult c p) i = c * coeff_int p i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (smult c p) i = c * coeff_int p i
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < 0 then 0::'a else coeff (smult c p) (nat i)) = c * (if i < 0 then 0::'a else coeff p (nat i))
[PROOF STEP]
by simp


[STATEMENT]
lemma coeff_int_signof_mult: "coeff_int (of_int (sign x) * f) i = of_int (sign x) * coeff_int f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (of_int (sign x) * f) i = of_int (sign x) * coeff_int f i
[PROOF STEP]
by (auto simp: coeff_int_def sign_def)


[STATEMENT]
lemma coeff_int_sum: "coeff_int (sum p A) i = (\<Sum>x\<in>A. coeff_int (p x) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (sum p A) i = (\<Sum>x\<in>A. coeff_int (p x) i)
[PROOF STEP]
using coeff_sum[of p A "nat i"]
[PROOF STATE]
proof (prove)
using this:
coeff (sum p A) (nat i) = (\<Sum>x\<in>A. coeff (p x) (nat i))

goal (1 subgoal):
 1. coeff_int (sum p A) i = (\<Sum>x\<in>A. coeff_int (p x) i)
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
using this:
coeff (sum p A) (nat i) = (\<Sum>x\<in>A. coeff (p x) (nat i))

goal (1 subgoal):
 1. (if i < 0 then 0::'a else coeff (sum p A) (nat i)) = (\<Sum>x\<in>A. if i < 0 then 0::'a else coeff (p x) (nat i))
[PROOF STEP]
by (cases "i < 0", auto)


[STATEMENT]
lemma coeff_int_0[simp]: "coeff_int f 0 = coeff f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int f 0 = coeff f 0
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 < 0 then 0::'a else coeff f (nat 0)) = coeff f 0
[PROOF STEP]
by simp


[STATEMENT]
lemma coeff_int_monom_mult: "coeff_int (monom a d * f) i = (a * coeff_int f (i - d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
proof (cases "i < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
 2. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < 0

goal (2 subgoals):
 1. i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
 2. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i < 0

goal (1 subgoal):
 1. coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
using this:
i < 0

goal (1 subgoal):
 1. (if i < 0 then 0::'a else coeff (monom a d * f) (nat i)) = a * (if i - int d < 0 then 0::'a else coeff f (nat (i - int d)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff_int (monom a d * f) i = a * coeff_int f (i - int d)

goal (1 subgoal):
 1. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < 0

goal (1 subgoal):
 1. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
hence "i \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> i < 0

goal (1 subgoal):
 1. 0 \<le> i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> i

goal (1 subgoal):
 1. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> i
[PROOF STEP]
obtain j where i: "i = int j"
[PROOF STATE]
proof (prove)
using this:
0 \<le> i

goal (1 subgoal):
 1. (\<And>j. i = int j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule nonneg_eq_int)
[PROOF STATE]
proof (state)
this:
i = int j

goal (1 subgoal):
 1. \<not> i < 0 \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
proof (cases "i \<ge> d")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
 2. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
int d \<le> i

goal (2 subgoals):
 1. int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
 2. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i = int j
int d \<le> i
[PROOF STEP]
have "nat (int j - int d) = j - d"
[PROOF STATE]
proof (prove)
using this:
i = int j
int d \<le> i

goal (1 subgoal):
 1. nat (int j - int d) = j - d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (int j - int d) = j - d

goal (2 subgoals):
 1. int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
 2. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
with coeff_monom_mult[of a]
[PROOF STATE]
proof (chain)
picking this:
coeff (monom a ?d * ?p) ?i = (if ?d \<le> ?i then a * coeff ?p (?i - ?d) else (0::'a))
nat (int j - int d) = j - d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff (monom a ?d * ?p) ?i = (if ?d \<le> ?i then a * coeff ?p (?i - ?d) else (0::'a))
nat (int j - int d) = j - d

goal (1 subgoal):
 1. coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
unfolding coeff_int_def i
[PROOF STATE]
proof (prove)
using this:
coeff (monom a ?d * ?p) ?i = (if ?d \<le> ?i then a * coeff ?p (?i - ?d) else (0::'a))
nat (int j - int d) = j - d

goal (1 subgoal):
 1. (if int j < 0 then 0::'a else coeff (monom a d * f) (nat (int j))) = a * (if int j - int d < 0 then 0::'a else coeff f (nat (int j - int d)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff_int (monom a d * f) i = a * coeff_int f (i - int d)

goal (1 subgoal):
 1. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> int d \<le> i

goal (1 subgoal):
 1. \<not> int d \<le> i \<Longrightarrow> coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> int d \<le> i

goal (1 subgoal):
 1. coeff_int (monom a d * f) i = a * coeff_int f (i - int d)
[PROOF STEP]
unfolding i
[PROOF STATE]
proof (prove)
using this:
\<not> int d \<le> int j

goal (1 subgoal):
 1. coeff_int (monom a d * f) (int j) = a * coeff_int f (int j - int d)
[PROOF STEP]
by (simp add: coeff_int_def coeff_monom_mult)
[PROOF STATE]
proof (state)
this:
coeff_int (monom a d * f) i = a * coeff_int f (i - int d)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coeff_int (monom a d * f) i = a * coeff_int f (i - int d)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_prod_const: assumes "finite xs" and "y \<notin> xs"
  and "\<And> x. x \<in> xs \<Longrightarrow> degree (f x) = 0"
shows "coeff (prod f (insert y xs)) i = prod (\<lambda> x. coeff (f x) 0) xs * coeff (f y) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite xs
y \<notin> xs
?x \<in> xs \<Longrightarrow> degree (f ?x) = 0

goal (1 subgoal):
 1. coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
proof (induct xs rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
case (insert x xs)
[PROOF STATE]
proof (state)
this:
finite xs
x \<notin> xs
\<lbrakk>y \<notin> xs; \<And>x. x \<in> xs \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
y \<notin> insert x xs
?x \<in> insert x xs \<Longrightarrow> degree (f ?x) = 0

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
from insert(2,4)
[PROOF STATE]
proof (chain)
picking this:
x \<notin> xs
y \<notin> insert x xs
[PROOF STEP]
have id: "insert y (insert x xs) - {x} = insert y xs"
[PROOF STATE]
proof (prove)
using this:
x \<notin> xs
y \<notin> insert x xs

goal (1 subgoal):
 1. insert y (insert x xs) - {x} = insert y xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert y (insert x xs) - {x} = insert y xs

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
have "prod f (insert y (insert x xs)) = f x * prod f (insert y xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod f (insert y (insert x xs)) = f x * prod f (insert y xs)
[PROOF STEP]
by (subst prod.remove[of _ x], insert insert(1,2) id, auto)
[PROOF STATE]
proof (state)
this:
prod f (insert y (insert x xs)) = f x * prod f (insert y xs)

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
hence "coeff (prod f (insert y (insert x xs))) i = coeff (f x * prod f (insert y xs)) i"
[PROOF STATE]
proof (prove)
using this:
prod f (insert y (insert x xs)) = f x * prod f (insert y xs)

goal (1 subgoal):
 1. coeff (prod f (insert y (insert x xs))) i = coeff (f x * prod f (insert y xs)) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff (prod f (insert y (insert x xs))) i = coeff (f x * prod f (insert y xs)) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (prod f (insert y (insert x xs))) i = coeff (f x * prod f (insert y xs)) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
have "\<dots> = coeff (f x) 0 * (coeff (prod f (insert y xs)) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i
[PROOF STEP]
from insert(5)[of x] degree0_coeffs[of "f x"]
[PROOF STATE]
proof (chain)
picking this:
x \<in> insert x xs \<Longrightarrow> degree (f x) = 0
degree (f x) = 0 \<Longrightarrow> \<exists>a. f x = [:a:]
[PROOF STEP]
obtain c where fx: "f x = [: c :]"
[PROOF STATE]
proof (prove)
using this:
x \<in> insert x xs \<Longrightarrow> degree (f x) = 0
degree (f x) = 0 \<Longrightarrow> \<exists>a. f x = [:a:]

goal (1 subgoal):
 1. (\<And>c. f x = [:c:] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x = [:c:]

goal (1 subgoal):
 1. coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i
[PROOF STEP]
unfolding fx
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff ([:c:] * prod f (insert y xs)) i = coeff [:c:] 0 * coeff (prod f (insert y xs)) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (f x * prod f (insert y xs)) i = coeff (f x) 0 * coeff (prod f (insert y xs)) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
have "(coeff (prod f (insert y xs)) i) = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite xs
x \<notin> xs
\<lbrakk>y \<notin> xs; \<And>x. x \<in> xs \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
y \<notin> insert x xs
?x \<in> insert x xs \<Longrightarrow> degree (f ?x) = 0

goal (1 subgoal):
 1. coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coeff (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
have "coeff (f x) 0 * \<dots> = prod (\<lambda> x. coeff (f x) 0) (insert x xs) * coeff (f y) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (f x) 0 * ((\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i) = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
by (subst prod.insert_remove, insert insert(1,2,4), auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
coeff (f x) 0 * ((\<Prod>x\<in>xs. coeff (f x) 0) * coeff (f y) i) = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i

goal (2 subgoals):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>y \<notin> F; \<And>x. x \<in> F \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y F)) i = (\<Prod>x\<in>F. coeff (f x) 0) * coeff (f y) i; y \<notin> insert x F; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) = 0\<rbrakk> \<Longrightarrow> coeff (prod f (insert y (insert x F))) i = (\<Prod>x\<in>insert x F. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
coeff (prod f (insert y (insert x xs))) i = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
coeff (prod f (insert y (insert x xs))) i = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i

goal (1 subgoal):
 1. coeff (prod f (insert y (insert x xs))) i = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
coeff (prod f (insert y (insert x xs))) i = (\<Prod>x\<in>insert x xs. coeff (f x) 0) * coeff (f y) i

goal (1 subgoal):
 1. \<lbrakk>y \<notin> {}; \<And>x. x \<in> {} \<Longrightarrow> degree (f x) = 0\<rbrakk> \<Longrightarrow> coeff (prod f {y}) i = (\<Prod>x\<in>{}. coeff (f x) 0) * coeff (f y) i
[PROOF STEP]
qed simp


[STATEMENT]
lemma coeff_int_prod_const: assumes "finite xs" and "y \<notin> xs"
  and "\<And> x. x \<in> xs \<Longrightarrow> degree (f x) = 0"
shows "coeff_int (prod f (insert y xs)) i = prod (\<lambda> x. coeff_int (f x) 0) xs * coeff_int (f y) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff_int (f x) 0) * coeff_int (f y) i
[PROOF STEP]
using coeff_prod_const[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> xs \<Longrightarrow> ?x1 x \<in> xs) \<Longrightarrow> coeff (\<Prod>x\<in>insert y xs. f (?x1 x)) ?i = (\<Prod>x\<in>xs. coeff (f (?x1 x)) 0) * coeff (f (?x1 y)) ?i

goal (1 subgoal):
 1. coeff_int (prod f (insert y xs)) i = (\<Prod>x\<in>xs. coeff_int (f x) 0) * coeff_int (f y) i
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> xs \<Longrightarrow> ?x1 x \<in> xs) \<Longrightarrow> coeff (\<Prod>x\<in>insert y xs. f (?x1 x)) ?i = (\<Prod>x\<in>xs. coeff (f (?x1 x)) 0) * coeff (f (?x1 y)) ?i

goal (1 subgoal):
 1. (if i < 0 then 0::'b else coeff (prod f (insert y xs)) (nat i)) = (\<Prod>x\<in>xs. if 0 < 0 then 0::'b else coeff (f x) (nat 0)) * (if i < 0 then 0::'b else coeff (f y) (nat i))
[PROOF STEP]
by (cases "i < 0", auto)


[STATEMENT]
lemma coeff_int[simp]: "coeff_int p n = coeff p n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int p (int n) = coeff p n
[PROOF STEP]
unfolding coeff_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if int n < 0 then 0::'a else coeff p (nat (int n))) = coeff p n
[PROOF STEP]
by auto


[STATEMENT]
lemma coeff_int_minus[simp]:
  "coeff_int (a - b) i = coeff_int a i - coeff_int b i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff_int (a - b) i = coeff_int a i - coeff_int b i
[PROOF STEP]
by (auto simp: coeff_int_def)


[STATEMENT]
lemma slice_path_length:
  "length(slice_path as) = length as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (slice_path as) = length as
[PROOF STEP]
by(induct as) auto


[STATEMENT]
lemma slice_path_right_Cons:
  assumes slice:"slice_path as = x#xs"
  obtains a' as' where "as = a'#as'" and "slice_path as' = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a' as'. \<lbrakk>as = a' # as'; slice_path as' = xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a' as'. as = a' # as' \<and> slice_path as' = xs
[PROOF STEP]
from slice
[PROOF STATE]
proof (chain)
picking this:
slice_path as = x # xs
[PROOF STEP]
show "\<exists>a' as'. as = a'#as' \<and> slice_path as' = xs"
[PROOF STATE]
proof (prove)
using this:
slice_path as = x # xs

goal (1 subgoal):
 1. \<exists>a' as'. as = a' # as' \<and> slice_path as' = xs
[PROOF STEP]
by(induct as) auto
[PROOF STATE]
proof (state)
this:
\<exists>a' as'. as = a' # as' \<and> slice_path as' = xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma select_edge_kinds_max_bv:
  "select_edge_kinds as (replicate (length as) True) = kinds as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select_edge_kinds as (replicate (length as) True) = kinds as
[PROOF STEP]
by(induct as,auto simp:kinds_def)