[STATEMENT]
lemma exi_cong: "H \<turnstile> A IFF A' \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (exi i A) IFF (exi i A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> H \<turnstile> exi i A IFF exi i A'
[PROOF STEP]
apply (rule Iff_I)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>H \<turnstile> A IFF A'; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (exi i A) H \<turnstile> exi i A'
 2. \<lbrakk>H \<turnstile> A IFF A'; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (exi i A') H \<turnstile> exi i A
[PROOF STEP]
apply (metis exi_mono Hyp Iff_MP_same Un_absorb Un_insert_right insertI1 thin_Un)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (exi i A') H \<turnstile> exi i A
[PROOF STEP]
apply (metis exi_mono Hyp Iff_MP2_same Un_absorb Un_insert_right insertI1 thin_Un)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma all_cong: "H \<turnstile> A IFF A' \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (all i A) IFF (all i A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> H \<turnstile> all i A IFF all i A'
[PROOF STEP]
by (metis exi_cong neg_cong)


[STATEMENT]
lemma Subst: "H \<turnstile> A \<Longrightarrow> \<forall>B \<in> H. atom i \<sharp> B \<Longrightarrow> H \<turnstile> A (i::=x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; \<forall>B\<in>H. atom i \<sharp> B\<rbrakk> \<Longrightarrow> H \<turnstile> A(i::=x)
[PROOF STEP]
by (metis all_D all_I)


[STATEMENT]
lemma eql_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (t EQ u IMP t' EQ u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
obtain v2::name and v3::name and v4::name
    where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
      and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
      and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v2 v3 v4. \<lbrakk>atom v2 \<sharp> (t, X1, X3, X4); atom v3 \<sharp> (t, t', X1, v2, X4); atom v4 \<sharp> (t, t', u, X1, v2, v3)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4
[PROOF STEP]
by (rule eql) (simp add: eq_cong_ax_def equality_axioms_def)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4
[PROOF STEP]
by (drule_tac i=X1 and x="Var X1" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var v2 EQ Var X4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var X2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var v2 EQ Var X4
[PROOF STEP]
by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var v2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var X4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var v2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var X4
[PROOF STEP]
using v2
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP Var X1 EQ Var X3 IMP Var v2 EQ Var X4
atom v2 \<sharp> (t, X1, X3, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var X4
[PROOF STEP]
by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var v4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var X4

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var v4
[PROOF STEP]
using v2 v3
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var X4
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var v4
[PROOF STEP]
by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP Var v2 EQ Var v4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP Var v2 EQ Var v4
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP Var X1 EQ Var v3 IMP Var v2 EQ Var v4
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP Var v2 EQ Var v4
[PROOF STEP]
by (drule_tac i=X1 and x=t in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP Var v2 EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP t' EQ Var v4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP Var v2 EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP t' EQ Var v4
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP Var v2 EQ Var v4
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP t' EQ Var v4
[PROOF STEP]
by (drule_tac i=v2 and x="t'" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP t' EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (t EQ u IMP t' EQ Var v4)"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP t' EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP t EQ u IMP t' EQ Var v4
[PROOF STEP]
using v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP t EQ Var v3 IMP t' EQ Var v4
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP t EQ u IMP t' EQ Var v4
[PROOF STEP]
by (drule_tac i=v3 and x=u in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP t EQ u IMP t' EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP t EQ u IMP t' EQ Var v4

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
using v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP t EQ u IMP t' EQ Var v4
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'
[PROOF STEP]
by (drule_tac i=v4 and x="u'" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ u' IMP t EQ u IMP t' EQ u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Refl [iff]: "H \<turnstile> t EQ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> t EQ t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> t EQ t
[PROOF STEP]
have "{} \<turnstile> Var X1 EQ Var X1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X1
[PROOF STEP]
by (rule eql) (simp add: equality_axioms_def refl_ax_def)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X1

goal (1 subgoal):
 1. H \<turnstile> t EQ t
[PROOF STEP]
hence "{} \<turnstile> t EQ t"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X1

goal (1 subgoal):
 1. {} \<turnstile> t EQ t
[PROOF STEP]
by (drule_tac i=X1 and x=t in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t

goal (1 subgoal):
 1. H \<turnstile> t EQ t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t

goal (1 subgoal):
 1. H \<turnstile> t EQ t
[PROOF STEP]
by (metis empty_subsetI thin)
[PROOF STATE]
proof (state)
this:
H \<turnstile> t EQ t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sym: assumes "H \<turnstile> t EQ u" shows "H \<turnstile> u EQ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
have "{} \<turnstile>  (t EQ u AND t EQ t) IMP (t EQ t IMP u EQ t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> t EQ u AND t EQ t IMP t EQ t IMP u EQ t
[PROOF STEP]
by (rule eql_cong1)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ u AND t EQ t IMP t EQ t IMP u EQ t

goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ u AND t EQ t IMP t EQ t IMP u EQ t

goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
have "{t EQ u} \<turnstile> t EQ u AND t EQ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t EQ u} \<turnstile> t EQ u AND t EQ t
[PROOF STEP]
by (metis Assume cnj_I Refl)
[PROOF STATE]
proof (state)
this:
{t EQ u} \<turnstile> t EQ u AND t EQ t

goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{} \<turnstile> t EQ u AND t EQ t IMP t EQ t IMP u EQ t
{t EQ u} \<turnstile> t EQ u AND t EQ t
[PROOF STEP]
have "{t EQ u} \<turnstile> u EQ t"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ u AND t EQ t IMP t EQ t IMP u EQ t
{t EQ u} \<turnstile> t EQ u AND t EQ t

goal (1 subgoal):
 1. {t EQ u} \<turnstile> u EQ t
[PROOF STEP]
by (metis MP_same MP Refl sup_bot_left)
[PROOF STATE]
proof (state)
this:
{t EQ u} \<turnstile> u EQ t

goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
thus "H \<turnstile> u EQ t"
[PROOF STATE]
proof (prove)
using this:
{t EQ u} \<turnstile> u EQ t

goal (1 subgoal):
 1. H \<turnstile> u EQ t
[PROOF STEP]
by (metis assms cut1)
[PROOF STATE]
proof (state)
this:
H \<turnstile> u EQ t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sym_L: "insert (t EQ u) H \<turnstile> A \<Longrightarrow> insert (u EQ t) H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (t EQ u) H \<turnstile> A \<Longrightarrow> insert (u EQ t) H \<turnstile> A
[PROOF STEP]
by (metis Assume Sym Un_empty_left Un_insert_left cut)


[STATEMENT]
lemma Trans: assumes "H \<turnstile> x EQ y" "H \<turnstile> y EQ z" shows "H \<turnstile> x EQ z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
have "\<And>H. H \<turnstile> (x EQ x AND y EQ z) IMP (x EQ y IMP x EQ z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>H. H \<turnstile> x EQ x AND y EQ z IMP x EQ y IMP x EQ z
[PROOF STEP]
by (metis eql_cong1 bot_least thin)
[PROOF STATE]
proof (state)
this:
?H \<turnstile> x EQ x AND y EQ z IMP x EQ y IMP x EQ z

goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?H \<turnstile> x EQ x AND y EQ z IMP x EQ y IMP x EQ z

goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
have "{x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z
[PROOF STEP]
by (metis Assume cnj_I Refl thin1)
[PROOF STATE]
proof (state)
this:
{x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z

goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?H \<turnstile> x EQ x AND y EQ z IMP x EQ y IMP x EQ z
{x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z
[PROOF STEP]
have "{x EQ y, y EQ z} \<turnstile> x EQ z"
[PROOF STATE]
proof (prove)
using this:
?H \<turnstile> x EQ x AND y EQ z IMP x EQ y IMP x EQ z
{x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z

goal (1 subgoal):
 1. {x EQ y, y EQ z} \<turnstile> x EQ z
[PROOF STEP]
by (metis Hyp MP_same insertI1)
[PROOF STATE]
proof (state)
this:
{x EQ y, y EQ z} \<turnstile> x EQ z

goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x EQ y, y EQ z} \<turnstile> x EQ z

goal (1 subgoal):
 1. H \<turnstile> x EQ z
[PROOF STEP]
by (metis assms cut2)
[PROOF STATE]
proof (state)
this:
H \<turnstile> x EQ z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eql_cong:
  assumes "H \<turnstile> t EQ t'" "H \<turnstile> u EQ u'" shows "H \<turnstile> t EQ u IFF t' EQ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
fix t t' u u'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
assume  "H \<turnstile> t EQ t'" "H \<turnstile> u EQ u'"
[PROOF STATE]
proof (state)
this:
H \<turnstile> t EQ t'
H \<turnstile> u EQ u'

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H \<turnstile> t EQ t'
H \<turnstile> u EQ u'

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
have "{t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'
[PROOF STEP]
using eql_cong1
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> ?t EQ ?t' AND ?u EQ ?u' IMP ?t EQ ?u IMP ?t' EQ ?u'

goal (1 subgoal):
 1. {t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'
[PROOF STEP]
by (metis Assume cnj_I MP_null insert_commute)
[PROOF STATE]
proof (state)
this:
{t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H \<turnstile> t EQ t'
H \<turnstile> u EQ u'
{t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'
[PROOF STEP]
have "H \<turnstile> t EQ u IMP t' EQ u'"
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> t EQ t'
H \<turnstile> u EQ u'
{t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'

goal (1 subgoal):
 1. H \<turnstile> t EQ u IMP t' EQ u'
[PROOF STEP]
by (metis cut2)
[PROOF STATE]
proof (state)
this:
H \<turnstile> t EQ u IMP t' EQ u'

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>H \<turnstile> ?ta2 EQ ?t'a2; H \<turnstile> ?ua2 EQ ?u'a2\<rbrakk> \<Longrightarrow> H \<turnstile> ?ta2 EQ ?ua2 IMP ?t'a2 EQ ?u'a2

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>H \<turnstile> ?ta2 EQ ?t'a2; H \<turnstile> ?ua2 EQ ?u'a2\<rbrakk> \<Longrightarrow> H \<turnstile> ?ta2 EQ ?ua2 IMP ?t'a2 EQ ?u'a2

goal (1 subgoal):
 1. H \<turnstile> t EQ u IFF t' EQ u'
[PROOF STEP]
by (metis Iff_def cnj_I assms Sym)
[PROOF STATE]
proof (state)
this:
H \<turnstile> t EQ u IFF t' EQ u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eql_Trans_E: "H \<turnstile> x EQ u \<Longrightarrow> insert (t EQ u) H \<turnstile> A \<Longrightarrow> insert (x EQ t) H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> x EQ u; insert (t EQ u) H \<turnstile> A\<rbrakk> \<Longrightarrow> insert (x EQ t) H \<turnstile> A
[PROOF STEP]
by (metis Assume Sym_L Trans cut_same thin1 thin2)


[STATEMENT]
lemma suc_cong1: "{} \<turnstile> (t EQ t') IMP (suc t EQ suc t')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
obtain v2::name and v3::name and v4::name
    where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
      and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
      and v4: "atom v4 \<sharp> (t,t',X1,v2,v3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v2 v3 v4. \<lbrakk>atom v2 \<sharp> (t, X1, X3, X4); atom v3 \<sharp> (t, t', X1, v2, X4); atom v4 \<sharp> (t, t', X1, v2, v3)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
have "{} \<turnstile> (Var X1 EQ Var X2) IMP (suc (Var X1) EQ suc (Var X2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X2 IMP suc (Var X1) EQ suc (Var X2)
[PROOF STEP]
by (metis syc_cong_ax_def equality_axioms_def insert_iff eql)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X2 IMP suc (Var X1) EQ suc (Var X2)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2) IMP (suc (Var X1) EQ suc (Var v2))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X2 IMP suc (Var X1) EQ suc (Var X2)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 IMP suc (Var X1) EQ suc (Var v2)
[PROOF STEP]
by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 IMP suc (Var X1) EQ suc (Var v2)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
hence "{} \<turnstile> (t EQ Var v2) IMP (suc t EQ suc (Var v2))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 IMP suc (Var X1) EQ suc (Var v2)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 IMP suc t EQ suc (Var v2)
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 IMP suc (Var X1) EQ suc (Var v2)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 IMP suc t EQ suc (Var v2)
[PROOF STEP]
by (drule_tac i=X1 and x=t in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ Var v2 IMP suc t EQ suc (Var v2)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t') IMP (suc t EQ suc t')"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 IMP suc t EQ suc (Var v2)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 IMP suc t EQ suc (Var v2)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
by (drule_tac i=v2 and x=t' in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' IMP suc t EQ suc t'

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' IMP suc t EQ suc t'

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
using v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' IMP suc t EQ suc t'
atom v4 \<sharp> (t, t', X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' IMP suc t EQ suc t'
[PROOF STEP]
by (drule_tac i=v4 in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' IMP suc t EQ suc t'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma suc_cong: "\<lbrakk>H \<turnstile> t EQ t'\<rbrakk> \<Longrightarrow> H \<turnstile> suc t EQ suc t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> t EQ t' \<Longrightarrow> H \<turnstile> suc t EQ suc t'
[PROOF STEP]
by (metis anti_deduction suc_cong1 cut1)


[STATEMENT]
lemma pls_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (pls t u EQ pls t' u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
obtain v2::name and v3::name and v4::name
    where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
      and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
      and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v2 v3 v4. \<lbrakk>atom v2 \<sharp> (t, X1, X3, X4); atom v3 \<sharp> (t, t', X1, v2, X4); atom v4 \<sharp> (t, t', u, X1, v2, v3)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (pls (Var X1) (Var X3) EQ pls (Var X2) (Var X4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var X2) (Var X4)
[PROOF STEP]
by (metis pls_cong_ax_def equality_axioms_def insert_iff eql)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var X2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var X2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4)
[PROOF STEP]
by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4)
[PROOF STEP]
using v2
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP pls (Var X1) (Var X3) EQ pls (Var v2) (Var X4)
atom v2 \<sharp> (t, X1, X3, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4)
[PROOF STEP]
by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4)
[PROOF STEP]
using v2 v3
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var X4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4)
[PROOF STEP]
by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (pls t (Var v3) EQ pls (Var v2) (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls (Var v2) (Var v4)
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP pls (Var X1) (Var v3) EQ pls (Var v2) (Var v4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls (Var v2) (Var v4)
[PROOF STEP]
by (drule_tac i=X1 and x=t in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (pls t (Var v3) EQ pls t' (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls t' (Var v4)
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls (Var v2) (Var v4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls t' (Var v4)
[PROOF STEP]
by (drule_tac i=v2 and x=t' in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (pls t u EQ pls t' (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP pls t u EQ pls t' (Var v4)
[PROOF STEP]
using v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP pls t (Var v3) EQ pls t' (Var v4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP pls t u EQ pls t' (Var v4)
[PROOF STEP]
by (drule_tac i=v3 and x=u in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP pls t u EQ pls t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP pls t u EQ pls t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
using v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP pls t u EQ pls t' (Var v4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'
[PROOF STEP]
by (drule_tac i=v4 and x=u' in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ u' IMP pls t u EQ pls t' u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pls_cong: "\<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> pls t u EQ pls t' u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> pls t u EQ pls t' u'
[PROOF STEP]
by (metis cnj_I anti_deduction pls_cong1 cut1)


[STATEMENT]
lemma tms_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (tms t u EQ tms t' u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
obtain v2::name and v3::name and v4::name
    where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
      and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
      and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v2 v3 v4. \<lbrakk>atom v2 \<sharp> (t, X1, X3, X4); atom v3 \<sharp> (t, t', X1, v2, X4); atom v4 \<sharp> (t, t', u, X1, v2, v3)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (tms (Var X1) (Var X3) EQ tms (Var X2) (Var X4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var X2) (Var X4)
[PROOF STEP]
by (metis tms_cong_ax_def equality_axioms_def insert_iff eql)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var X2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var X2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var X2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4)
[PROOF STEP]
by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4)
[PROOF STEP]
using v2
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var X3 EQ Var X4 IMP tms (Var X1) (Var X3) EQ tms (Var v2) (Var X4)
atom v2 \<sharp> (t, X1, X3, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4)
[PROOF STEP]
by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4)
[PROOF STEP]
using v2 v3
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var X4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var X4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)

goal (1 subgoal):
 1. {} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4)
[PROOF STEP]
by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (tms t (Var v3) EQ tms (Var v2) (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms (Var v2) (Var v4)
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Var X1 EQ Var v2 AND Var v3 EQ Var v4 IMP tms (Var X1) (Var v3) EQ tms (Var v2) (Var v4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms (Var v2) (Var v4)
[PROOF STEP]
by (drule_tac i=X1 and x=t in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (tms t (Var v3) EQ tms t' (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms (Var v2) (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms t' (Var v4)
[PROOF STEP]
using v2 v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ Var v2 AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms (Var v2) (Var v4)
atom v2 \<sharp> (t, X1, X3, X4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms t' (Var v4)
[PROOF STEP]
by (drule_tac i=v2 and x=t' in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (tms t u EQ tms t' (Var v4))"
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP tms t u EQ tms t' (Var v4)
[PROOF STEP]
using v3 v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND Var v3 EQ Var v4 IMP tms t (Var v3) EQ tms t' (Var v4)
atom v3 \<sharp> (t, t', X1, v2, X4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ Var v4 IMP tms t u EQ tms t' (Var v4)
[PROOF STEP]
by (drule_tac i=v3 and x=u in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP tms t u EQ tms t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP tms t u EQ tms t' (Var v4)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
using v4
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> t EQ t' AND u EQ Var v4 IMP tms t u EQ tms t' (Var v4)
atom v4 \<sharp> (t, t', u, X1, v2, v3)

goal (1 subgoal):
 1. {} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'
[PROOF STEP]
by (drule_tac i=v4 and x=u' in Subst) simp_all
[PROOF STATE]
proof (state)
this:
{} \<turnstile> t EQ t' AND u EQ u' IMP tms t u EQ tms t' u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tms_cong: "\<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> tms t u EQ tms t' u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> tms t u EQ tms t' u'
[PROOF STEP]
by (metis cnj_I anti_deduction tms_cong1 cut1)


[STATEMENT]
lemma eql_subst_trm_Iff: "{t EQ u} \<turnstile> subst i t trm EQ subst i u trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t EQ u} \<turnstile> subst i t trm EQ subst i u trm
[PROOF STEP]
by (induct trm rule: trm.induct) (auto simp: suc_cong pls_cong tms_cong)


[STATEMENT]
lemma eql_subst_fmla_Iff: "insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)
[PROOF STEP]
have "{ t EQ u } \<turnstile> A(i::=t) IFF A(i::=u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t EQ u} \<turnstile> A(i::=t) IFF A(i::=u)
[PROOF STEP]
by (nominal_induct A avoiding: i t u rule: fmla.strong_induct)
       (auto simp: dsj_cong neg_cong exi_cong eql_cong eql_subst_trm_Iff)
[PROOF STATE]
proof (state)
this:
{t EQ u} \<turnstile> A(i::=t) IFF A(i::=u)

goal (1 subgoal):
 1. insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{t EQ u} \<turnstile> A(i::=t) IFF A(i::=u)

goal (1 subgoal):
 1. insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)
[PROOF STEP]
by (metis Assume cut1)
[PROOF STATE]
proof (state)
this:
insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Var_eql_subst_Iff: "insert (Var i EQ t) H \<turnstile> A(i::=t) IFF A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (Var i EQ t) H \<turnstile> A(i::=t) IFF A
[PROOF STEP]
by (metis eql_subst_fmla_Iff Iff_sym subst_fmla_id)


[STATEMENT]
lemma Var_eql_imp_subst_Iff: "H \<turnstile> Var i EQ t \<Longrightarrow> H \<turnstile> A(i::=t) IFF A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> Var i EQ t \<Longrightarrow> H \<turnstile> A(i::=t) IFF A
[PROOF STEP]
by (metis Var_eql_subst_Iff cut_same)


[STATEMENT]
lemma P1_cong:
  fixes tms :: "trm list"
  assumes "\<And>i t x. atom i \<sharp> tms \<Longrightarrow> (P t)(i::=x) = P (subst i x t)" and "H \<turnstile> x EQ x'"
  shows "H \<turnstile> P x IFF P x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
obtain i::name where i: "atom i \<sharp> tms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. atom i \<sharp> tms \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> tms

goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
have "insert (x EQ x') H  \<turnstile> (P (Var i))(i::=x) IFF (P(Var i))(i::=x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (x EQ x') H \<turnstile> (P (Var i))(i::=x) IFF (P (Var i))(i::=x')
[PROOF STEP]
by (rule eql_subst_fmla_Iff)
[PROOF STATE]
proof (state)
this:
insert (x EQ x') H \<turnstile> (P (Var i))(i::=x) IFF (P (Var i))(i::=x')

goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
insert (x EQ x') H \<turnstile> (P (Var i))(i::=x) IFF (P (Var i))(i::=x')

goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
using assms i
[PROOF STATE]
proof (prove)
using this:
insert (x EQ x') H \<turnstile> (P (Var i))(i::=x) IFF (P (Var i))(i::=x')
atom ?i \<sharp> tms \<Longrightarrow> (P ?t)(?i::=?x) = P (subst ?i ?x ?t)
H \<turnstile> x EQ x'
atom i \<sharp> tms

goal (1 subgoal):
 1. H \<turnstile> P x IFF P x'
[PROOF STEP]
by (metis cut_same subst.simps(2))
[PROOF STATE]
proof (state)
this:
H \<turnstile> P x IFF P x'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P2_cong:
  fixes tms :: "trm list"
  assumes sub: "\<And>i t u x. atom i \<sharp> tms \<Longrightarrow> (P t u)(i::=x) = P (subst i x t) (subst i x u)"
      and eq:  "H \<turnstile> x EQ x'" "H \<turnstile> y EQ y'"
  shows "H \<turnstile> P x y IFF P x' y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
have yy': "{ y EQ y' } \<turnstile> P x' y IFF P x' y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y EQ y'} \<turnstile> P x' y IFF P x' y'
[PROOF STEP]
by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub)
[PROOF STATE]
proof (state)
this:
{y EQ y'} \<turnstile> P x' y IFF P x' y'

goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
have "{ x EQ x' } \<turnstile> P x y IFF P x' y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x EQ x'} \<turnstile> P x y IFF P x' y
[PROOF STEP]
by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub)
[PROOF STATE]
proof (state)
this:
{x EQ x'} \<turnstile> P x y IFF P x' y

goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
hence "{x EQ x', y EQ y'} \<turnstile> P x y IFF P x' y'"
[PROOF STATE]
proof (prove)
using this:
{x EQ x'} \<turnstile> P x y IFF P x' y

goal (1 subgoal):
 1. {x EQ x', y EQ y'} \<turnstile> P x y IFF P x' y'
[PROOF STEP]
by (metis Assume Iff_trans cut1 rotate2 yy')
[PROOF STATE]
proof (state)
this:
{x EQ x', y EQ y'} \<turnstile> P x y IFF P x' y'

goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x EQ x', y EQ y'} \<turnstile> P x y IFF P x' y'

goal (1 subgoal):
 1. H \<turnstile> P x y IFF P x' y'
[PROOF STEP]
by (metis cut2 eq)
[PROOF STATE]
proof (state)
this:
H \<turnstile> P x y IFF P x' y'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P3_cong:
  fixes tms :: "trm list"
  assumes sub: "\<And>i t u v x. atom i \<sharp> tms \<Longrightarrow>
                   (P t u v)(i::=x) = P (subst i x t) (subst i x u) (subst i x v)"
      and eq:  "H \<turnstile> x EQ x'" "H \<turnstile> y EQ y'" "H \<turnstile> z EQ z'"
  shows "H \<turnstile> P x y z IFF P x' y' z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
obtain i::name where i: "atom i \<sharp> (z,z',y,y',x,x')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. atom i \<sharp> (z, z', y, y', x, x') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> (z, z', y, y', x, x')

goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
have tl: "{ y EQ y', z EQ z' } \<turnstile> P x' y z IFF P x' y' z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y EQ y', z EQ z'} \<turnstile> P x' y z IFF P x' y' z'
[PROOF STEP]
by (rule P2_cong [where tms="[z,z',y,y',x,x']@tms"]) (auto simp: fresh_Cons sub)
[PROOF STATE]
proof (state)
this:
{y EQ y', z EQ z'} \<turnstile> P x' y z IFF P x' y' z'

goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
have hd: "{ x EQ x' } \<turnstile> P x y z IFF P x' y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x EQ x'} \<turnstile> P x y z IFF P x' y z
[PROOF STEP]
by (rule P1_cong [where tms="[z,y,x']@tms"]) (auto simp: fresh_Cons sub)
[PROOF STATE]
proof (state)
this:
{x EQ x'} \<turnstile> P x y z IFF P x' y z

goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
have "{x EQ x', y EQ y', z EQ z'} \<turnstile> P x y z IFF P x' y' z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x EQ x', y EQ y', z EQ z'} \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
by (metis Assume thin1 hd [THEN cut1] tl Iff_trans)
[PROOF STATE]
proof (state)
this:
{x EQ x', y EQ y', z EQ z'} \<turnstile> P x y z IFF P x' y' z'

goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x EQ x', y EQ y', z EQ z'} \<turnstile> P x y z IFF P x' y' z'

goal (1 subgoal):
 1. H \<turnstile> P x y z IFF P x' y' z'
[PROOF STEP]
by (rule cut3) (rule eq)+
[PROOF STATE]
proof (state)
this:
H \<turnstile> P x y z IFF P x' y' z'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P4_cong:
  fixes tms :: "trm list"
  assumes sub: "\<And>i t1 t2 t3 t4 x. atom i \<sharp> tms \<Longrightarrow>
                 (P t1 t2 t3 t4)(i::=x) = P (subst i x t1) (subst i x t2) (subst i x t3) (subst i x t4)"
      and eq:  "H \<turnstile> x1 EQ x1'" "H \<turnstile> x2 EQ x2'" "H \<turnstile> x3 EQ x3'" "H \<turnstile> x4 EQ x4'"
  shows "H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
obtain i::name where i: "atom i \<sharp> (x4,x4',x3,x3',x2,x2',x1,x1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. atom i \<sharp> (x4, x4', x3, x3', x2, x2', x1, x1') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> (x4, x4', x3, x3', x2, x2', x1, x1')

goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
have tl: "{ x2 EQ x2', x3 EQ x3', x4 EQ x4' } \<turnstile> P x1' x2 x3 x4 IFF P x1' x2' x3' x4'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1' x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
by (rule P3_cong [where tms="[x4,x4',x3,x3',x2,x2',x1,x1']@tms"]) (auto simp: fresh_Cons sub)
[PROOF STATE]
proof (state)
this:
{x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1' x2 x3 x4 IFF P x1' x2' x3' x4'

goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
have hd: "{ x1 EQ x1' } \<turnstile> P x1 x2 x3 x4 IFF P x1' x2 x3 x4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x1 EQ x1'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2 x3 x4
[PROOF STEP]
by (auto simp: fresh_Cons sub intro!: P1_cong [where tms="[x4,x3,x2,x1']@tms"])
[PROOF STATE]
proof (state)
this:
{x1 EQ x1'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2 x3 x4

goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
have "{x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
by (metis Assume thin1 hd [THEN cut1] tl Iff_trans)
[PROOF STATE]
proof (state)
this:
{x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'

goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'

goal (1 subgoal):
 1. H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'
[PROOF STEP]
by (rule cut4) (rule eq)+
[PROOF STATE]
proof (state)
this:
H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neg_I [intro!]: "insert A H \<turnstile> fls \<Longrightarrow> H \<turnstile> neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> fls \<Longrightarrow> H \<turnstile> neg A
[PROOF STEP]
unfolding fls_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> neg (zer EQ zer) \<Longrightarrow> H \<turnstile> neg A
[PROOF STEP]
by (meson neg_D neg_I0 Refl)


[STATEMENT]
lemma neg_E [intro!]: "H \<turnstile> A \<Longrightarrow> insert (neg A) H \<turnstile> fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A \<Longrightarrow> insert (neg A) H \<turnstile> fls
[PROOF STEP]
by (rule ContraProve)


[STATEMENT]
lemma neg_imp_I [intro!]: "H \<turnstile> A \<Longrightarrow> insert B H \<turnstile> fls \<Longrightarrow> H \<turnstile> neg (A IMP B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; insert B H \<turnstile> fls\<rbrakk> \<Longrightarrow> H \<turnstile> neg (A IMP B)
[PROOF STEP]
by (metis negneg_I neg_dsj_I neg_I)


[STATEMENT]
lemma neg_imp_E [intro!]: "insert (neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert (neg (A IMP B)) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert (neg (A IMP B)) H \<turnstile> C
[PROOF STEP]
apply (rule cut_same [where A=A])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. insert (neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert (neg (A IMP B)) H \<turnstile> A
 2. insert (neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert A (insert (neg (A IMP B)) H) \<turnstile> C
[PROOF STEP]
apply (metis Assume dsj_I1 negneg_D neg_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert A (insert (neg (A IMP B)) H) \<turnstile> C
[PROOF STEP]
apply (metis Swap imp_I rotate2 thin1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma truth_provable: "H \<turnstile> (neg fls)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> neg fls
[PROOF STEP]
by (metis fls_E neg_I)


[STATEMENT]
lemma exFalso: "H \<turnstile> fls \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> fls \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis neg_D truth_provable)


[STATEMENT]
theorem nprv_sound: assumes "H \<turnstile> A" shows "(\<forall>B\<in>H. eval_fmla e B) \<Longrightarrow> eval_fmla e A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>B\<in>H. eval_fmla e B \<Longrightarrow> eval_fmla e A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A

goal (1 subgoal):
 1. \<forall>B\<in>H. eval_fmla e B \<Longrightarrow> eval_fmla e A
[PROOF STEP]
proof (induct arbitrary: e)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> H; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> Q_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 5. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 6. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 7. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (Hyp A H)
[PROOF STATE]
proof (state)
this:
A \<in> H
\<forall>a\<in>H. eval_fmla e a

goal (7 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> H; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> Q_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 5. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 6. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 7. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> H
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval_fmla e A

goal (6 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> Q_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 5. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 6. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> Q_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 5. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 6. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (Q H)
[PROOF STATE]
proof (state)
this:
H \<in> Q_axioms
\<forall>a\<in>H_. eval_fmla e a

goal (6 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> Q_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 5. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 6. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H \<in> Q_axioms
\<forall>a\<in>H_. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e H
[PROOF STEP]
unfolding Q_axioms_def
[PROOF STATE]
proof (prove)
using this:
H \<in> {uu_. \<exists>A X1 X2. uu_ = A \<and> X1 \<noteq> X2 \<and> (A = neg (zer EQ suc (Var X1)) \<or> A = suc (Var X1) EQ suc (Var X2) IMP Var X1 EQ Var X2 \<or> A = Var X2 EQ zer OR exi X1 (Var X2 EQ suc (Var X1)) \<or> A = pls (Var X1) zer EQ Var X1 \<or> A = pls (Var X1) (suc (Var X2)) EQ suc (pls (Var X1) (Var X2)) \<or> A = tms (Var X1) zer EQ zer \<or> A = tms (Var X1) (suc (Var X2)) EQ pls (tms (Var X1) (Var X2)) (Var X1))}
\<forall>a\<in>H_. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e H
[PROOF STEP]
using not0_implies_Suc
[PROOF STATE]
proof (prove)
using this:
H \<in> {uu_. \<exists>A X1 X2. uu_ = A \<and> X1 \<noteq> X2 \<and> (A = neg (zer EQ suc (Var X1)) \<or> A = suc (Var X1) EQ suc (Var X2) IMP Var X1 EQ Var X2 \<or> A = Var X2 EQ zer OR exi X1 (Var X2 EQ suc (Var X1)) \<or> A = pls (Var X1) zer EQ Var X1 \<or> A = pls (Var X1) (suc (Var X2)) EQ suc (pls (Var X1) (Var X2)) \<or> A = tms (Var X1) zer EQ zer \<or> A = tms (Var X1) (suc (Var X2)) EQ pls (tms (Var X1) (Var X2)) (Var X1))}
\<forall>a\<in>H_. eval_fmla e a
?n \<noteq> 0 \<Longrightarrow> \<exists>m. ?n = Suc m

goal (1 subgoal):
 1. eval_fmla e H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
eval_fmla e H

goal (5 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 5. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 5. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (Bool A H)
[PROOF STATE]
proof (state)
this:
A \<in> boolean_axioms
\<forall>a\<in>H. eval_fmla e a

goal (5 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> boolean_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 4. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 5. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> boolean_axioms
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e A
[PROOF STEP]
by (metis boolean_axioms_hold)
[PROOF STATE]
proof (state)
this:
eval_fmla e A

goal (4 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 4. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 4. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (eql A H)
[PROOF STATE]
proof (state)
this:
A \<in> equality_axioms
\<forall>a\<in>H. eval_fmla e a

goal (4 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> equality_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 3. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 4. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> equality_axioms
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e A
[PROOF STEP]
by (metis equality_axioms_hold)
[PROOF STATE]
proof (state)
this:
eval_fmla e A

goal (3 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 3. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 3. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (Spec A H)
[PROOF STATE]
proof (state)
this:
A \<in> special_axioms
\<forall>a\<in>H. eval_fmla e a

goal (3 subgoals):
 1. \<And>A H e. \<lbrakk>A \<in> special_axioms; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e A
 2. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 3. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> special_axioms
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e A
[PROOF STEP]
by (metis special_axioms_hold)
[PROOF STATE]
proof (state)
this:
eval_fmla e A

goal (2 subgoals):
 1. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 2. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 2. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (MP H A B H')
[PROOF STATE]
proof (state)
this:
H \<turnstile> A IMP B
\<forall>a\<in>H. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e (A IMP B)
H' \<turnstile> A
\<forall>a\<in>H'. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e A
\<forall>a\<in>H \<union> H'. eval_fmla e a

goal (2 subgoals):
 1. \<And>H A B H' e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); H' \<turnstile> A; \<And>e. Ball H' (eval_fmla e) \<Longrightarrow> eval_fmla e A; Ball (H \<union> H') (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e B
 2. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
\<forall>a\<in>H. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e (A IMP B)
H' \<turnstile> A
\<forall>a\<in>H'. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e A
\<forall>a\<in>H \<union> H'. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval_fmla e B

goal (1 subgoal):
 1. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
case (exiists H A B i e)
[PROOF STATE]
proof (state)
this:
H \<turnstile> A IMP B
\<forall>a\<in>H. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e (A IMP B)
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. \<And>H A B i e. \<lbrakk>H \<turnstile> A IMP B; \<And>e. Ball H (eval_fmla e) \<Longrightarrow> eval_fmla e (A IMP B); atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; Ball H (eval_fmla e)\<rbrakk> \<Longrightarrow> eval_fmla e (exi i A IMP B)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
\<forall>a\<in>H. eval_fmla ?e a \<Longrightarrow> eval_fmla ?e (A IMP B)
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C
\<forall>a\<in>H. eval_fmla e a

goal (1 subgoal):
 1. eval_fmla e (exi i A IMP B)
[PROOF STEP]
by auto (metis forget_eval_fmla)
[PROOF STATE]
proof (state)
this:
eval_fmla e (exi i A IMP B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_instr_code [code]:
  "exec_instr (Load n) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (None, h, ((loc ! n) # stk, loc, C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr (Store n) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (None, h, (tl stk, loc[n:=hd stk], C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr (Push v) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (None, h, (v # stk, loc, C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr (New C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   (let HA = allocate h (Class_type C) in
    if HA = {} then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt OutOfMemory\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)}
    else do { (h', a) \<leftarrow> HA; {(\<lbrace>NewHeapElem a (Class_type C)\<rbrace>, None, h', (Addr a # stk, loc, C\<^sub>0, M\<^sub>0, pc + 1)#frs)} })"
  "exec_instr (NewArray T) P t h stk loc C0 M0 pc frs =
   (let si = the_Intg (hd stk);
        i = nat (sint si)
    in if si <s 0
       then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NegativeArraySize\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
       else let HA = allocate h (Array_type T i) in
         if HA = {} then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt OutOfMemory\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
         else do { (h', a) \<leftarrow> HA; {(\<lbrace>NewHeapElem a (Array_type T i)\<rbrace>, None, h', (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)}})"
  "exec_instr ALoad P t h stk loc C0 M0 pc frs =
   (let va = hd (tl stk)
    in (if va = Null then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
        else
          let i = the_Intg (hd stk);
              a = the_Addr va;
              len = alen_of_htype (the (typeof_addr h a))
          in if i <s 0 \<or> int len \<le> sint i then
               {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
             else do {
                 v \<leftarrow> heap_read h a (ACell (nat (sint i)));
                 {(\<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>, None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs)}
               }))"
  "exec_instr AStore P t h stk loc C0 M0 pc frs =
  (let ve = hd stk;
       vi = hd (tl stk);
       va = hd (tl (tl stk))
   in (if va = Null then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
       else (let i = the_Intg vi;
                 idx = nat (sint i);
                 a = the_Addr va;
                 hT = the (typeof_addr h a);
                 T = ty_of_htype hT;
                 len = alen_of_htype hT;
                 U = the (execute.typeof_h h ve)
             in (if i <s 0 \<or> int len \<le> sint i then
                      {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
                 else if P \<turnstile> U \<le> the_Array T then
                      do {
                         h' \<leftarrow> heap_write h a (ACell idx) ve;
                         {(\<lbrace>WriteMem a (ACell idx) ve\<rbrace>, None, h', (tl (tl (tl stk)), loc, C0, M0, pc+1) # frs)}
                      }
                 else {(\<epsilon>, (\<lfloor>execute.addr_of_sys_xcpt ArrayStore\<rfloor>, h, (stk, loc, C0, M0, pc) # frs))}))))"
  "exec_instr ALength P t h stk loc C0 M0 pc frs =
   {(\<epsilon>, (let va = hd stk
         in if va = Null
            then (\<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)
            else (None, h, (Intg (word_of_int (int (alen_of_htype (the (typeof_addr h (the_Addr va)))))) # tl stk, loc, C0, M0, pc+1) # frs)))}"
  "exec_instr (Getfield F C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   (let v = hd stk
    in if v = Null then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)}
       else let a = the_Addr v
            in do {
               v' \<leftarrow> heap_read h a (CField C F);
               {(\<lbrace>ReadMem a (CField C F) v'\<rbrace>, None, h, (v' # (tl stk), loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)}
            })"
  "exec_instr (Putfield F C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
  (let v = hd stk;
       r = hd (tl stk)
   in if r = Null then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)}
      else let a = the_Addr r
           in do {
                h' \<leftarrow> heap_write h a (CField C F) v;
                {(\<lbrace>WriteMem a (CField C F) v\<rbrace>, None, h', (tl (tl stk), loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)}
              })"
 "exec_instr (Checkcast T) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
  {(\<epsilon>, let U = the (typeof\<^bsub>h\<^esub> (hd stk))
       in if P \<turnstile> U \<le> T then (None, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)
          else (\<lfloor>execute.addr_of_sys_xcpt ClassCast\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs))}"
  "exec_instr (Instanceof T) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, None, h, (Bool (hd stk \<noteq> Null \<and> P \<turnstile> the (typeof\<^bsub>h\<^esub> (hd stk)) \<le> T) # tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)}"
  "exec_instr (Invoke M n) P t h stk loc C0 M0 pc frs =
   (let r = stk ! n
    in (if r = Null then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}
        else (let ps = rev (take n stk);
                  a = the_Addr r;
                  T = the (typeof_addr h a);
                  (D,M',Ts,meth)= method P (class_type_of T) M
         in case meth of
               Native \<Rightarrow>
                      do {
                        (ta, va, h') \<leftarrow> red_external_aggr P t a M ps h;
                        {(extTA2JVM P ta, extRet2JVM n h' stk loc C0 M0 pc frs va)}
                      }
            | \<lfloor>(mxs,mxl\<^sub>0,ins,xt)\<rfloor> \<Rightarrow>
              let f' = ([],[r]@ps@(replicate mxl\<^sub>0 undefined_value),D,M,0)
              in {(\<epsilon>, None, h, f' # (stk, loc, C0, M0, pc) # frs)})))"
  "exec_instr Return P t h stk\<^sub>0 loc\<^sub>0 C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (if frs=[] then (None, h, [])
         else
           let v = hd stk\<^sub>0;
               (stk,loc,C,m,pc) = hd frs;
                n = length (fst (snd (method P C\<^sub>0 M\<^sub>0)))
           in (None, h, (v#(drop (n+1) stk),loc,C,m,pc+1)#tl frs)))}"
  "exec_instr Pop P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<epsilon>, (None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr Dup P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<epsilon>, (None, h, (hd stk # stk, loc, C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr Swap P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<epsilon>, (None, h, (hd (tl stk) # hd stk # tl (tl stk), loc, C\<^sub>0, M\<^sub>0, pc+1)#frs))}"
  "exec_instr (BinOpInstr bop) P t h stk loc C0 M0 pc frs =
   {(\<epsilon>,
     case the (execute.binop bop (hd (tl stk)) (hd stk)) of
       Inl v \<Rightarrow> (None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs)
     | Inr a \<Rightarrow> (Some a, h, (stk, loc, C0, M0, pc) # frs))}"
  "exec_instr (IfFalse i) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (let pc' = if hd stk = Bool False then nat(int pc+i) else pc+1
         in (None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc')#frs)))}"
  "exec_instr (Goto i) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<epsilon>, (None, h, (stk, loc, C\<^sub>0, M\<^sub>0, nat(int pc+i))#frs))}"
  "exec_instr ThrowExc P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(\<epsilon>, (let xp' = if hd stk = Null then \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor> else \<lfloor>the_Addr(hd stk)\<rfloor>
         in (xp', h, (stk, loc, C\<^sub>0, M\<^sub>0, pc)#frs)))}"
  "exec_instr MEnter P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   {(let v = hd stk
     in if v = Null
        then (\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)
        else (\<lbrace>Lock\<rightarrow>the_Addr v, SyncLock (the_Addr v)\<rbrace>, None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs))}"
  "exec_instr MExit P t h stk loc C\<^sub>0 M\<^sub>0 pc frs =
   (let v = hd stk
    in if v = Null
       then {(\<epsilon>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)}
       else {(\<lbrace>Unlock\<rightarrow>the_Addr v, SyncUnlock (the_Addr v)\<rbrace>, None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs),
             (\<lbrace>UnlockFail\<rightarrow>the_Addr v\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt IllegalMonitorState\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((exec_instr (Load n) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (loc ! n # stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr (Store n) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (tl stk, loc[n := hd stk], C\<^sub>0, M\<^sub>0, pc + 1) # frs)}) &&& exec_instr (Push v) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (v # stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr (New C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = (let HA = allocate h (Class_type C) in if HA = {} then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt OutOfMemory\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)} else HA \<bind> (\<lambda>(h', a). {(\<lbrace>NewHeapElem a (Class_type C)\<rbrace>, None, h', (Addr a # stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)})) &&& exec_instr (NewArray T) P t h stk loc C0 M0 pc frs = (let si = the_Intg (hd stk); i = nat (sint si) in if si <s 0 then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NegativeArraySize\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else let HA = allocate h (Array_type T i) in if HA = {} then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt OutOfMemory\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else HA \<bind> (\<lambda>(h', a). {(\<lbrace>NewHeapElem a (Array_type T i)\<rbrace>, None, h', (Addr a # tl stk, loc, C0, M0, pc + 1) # frs)}))) &&& (exec_instr ALoad P t h stk loc C0 M0 pc frs = (let va = hd (tl stk) in if va = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else let i = the_Intg (hd stk); a = the_Addr va; len = alen_of_htype (the (typeof_addr h a)) in if i <s 0 \<or> int len \<le> sint i then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else heap_read h a (ACell (nat (sint i))) \<bind> (\<lambda>v. {(\<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>, None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs)})) &&& exec_instr AStore P t h stk loc C0 M0 pc frs = (let ve = hd stk; vi = hd (tl stk); va = hd (tl (tl stk)) in if va = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else let i = the_Intg vi; idx = nat (sint i); a = the_Addr va; hT = the (typeof_addr h a); T = ty_of_htype hT; len = alen_of_htype hT; U = the (typeof\<^bsub>h\<^esub> ve) in if i <s 0 \<or> int len \<le> sint i then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt ArrayIndexOutOfBounds\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else if P \<turnstile> U \<le> the_Array T then heap_write h a (ACell idx) ve \<bind> (\<lambda>h'. {(\<lbrace>WriteMem a (ACell idx) ve\<rbrace>, None, h', (tl (tl (tl stk)), loc, C0, M0, pc + 1) # frs)}) else {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt ArrayStore\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)}) &&& exec_instr ALength P t h stk loc C0 M0 pc frs = {(\<lbrace>\<rbrace>, let va = hd stk in if va = Null then (\<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs) else (None, h, (Intg (word_of_int (int (alen_of_htype (the (typeof_addr h (the_Addr va)))))) # tl stk, loc, C0, M0, pc + 1) # frs))}) &&& exec_instr (Getfield F C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = (let v = hd stk in if v = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)} else let a = the_Addr v in heap_read h a (CField C F) \<bind> (\<lambda>v'. {(\<lbrace>ReadMem a (CField C F) v'\<rbrace>, None, h, (v' # tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)})) &&& exec_instr (Putfield F C) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = (let v = hd stk; r = hd (tl stk) in if r = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)} else let a = the_Addr r in heap_write h a (CField C F) v \<bind> (\<lambda>h'. {(\<lbrace>WriteMem a (CField C F) v\<rbrace>, None, h', (tl (tl stk), loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)})) &&& exec_instr (Checkcast T) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, let U = the (typeof\<^bsub>h\<^esub> (hd stk)) in if P \<turnstile> U \<le> T then (None, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs) else (\<lfloor>execute.addr_of_sys_xcpt ClassCast\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs))}) &&& ((exec_instr (Instanceof T) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (Bool (hd stk \<noteq> Null \<and> P \<turnstile> the (typeof\<^bsub>h\<^esub> (hd stk)) \<le> T) # tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr (Invoke M n) P t h stk loc C0 M0 pc frs = (let r = stk ! n in if r = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C0, M0, pc) # frs)} else let ps = rev (take n stk); a = the_Addr r; T = the (typeof_addr h a); (D, M', Ts, meth) = method P (class_type_of T) M in case meth of None \<Rightarrow> red_external_aggr P t a M ps h \<bind> (\<lambda>(ta, va, h'). {(extTA2JVM P ta, extRet2JVM n h' stk loc C0 M0 pc frs va)}) | \<lfloor>(mxs, mxl\<^sub>0, ins, xt)\<rfloor> \<Rightarrow> let f' = ([], [r] @ ps @ replicate mxl\<^sub>0 undefined_value, D, M, 0) in {(\<lbrace>\<rbrace>, None, h, f' # (stk, loc, C0, M0, pc) # frs)}) &&& exec_instr Return P t h stk\<^sub>0 loc\<^sub>0 C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, if frs = [] then (None, h, []) else let v = hd stk\<^sub>0; (stk, loc, C, m, pc) = hd frs; n = length (fst (snd (method P C\<^sub>0 M\<^sub>0))) in (None, h, (v # drop (n + 1) stk, loc, C, m, pc + 1) # tl frs))}) &&& exec_instr Pop P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr Dup P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (hd stk # stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr Swap P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (hd (tl stk) # hd stk # tl (tl stk), loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)}) &&& (exec_instr (BinOpInstr bop) P t h stk loc C0 M0 pc frs = {(\<lbrace>\<rbrace>, case the (execute.binop bop (hd (tl stk)) (hd stk)) of Inl v \<Rightarrow> (None, h, (v # tl (tl stk), loc, C0, M0, pc + 1) # frs) | Inr a \<Rightarrow> (\<lfloor>a\<rfloor>, h, (stk, loc, C0, M0, pc) # frs))} &&& exec_instr (IfFalse i) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, let pc' = if hd stk = Bool False then nat (int pc + i) else pc + 1 in (None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc') # frs))} &&& exec_instr (Goto i) P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, None, h, (stk, loc, C\<^sub>0, M\<^sub>0, nat (int pc + i)) # frs)}) &&& exec_instr ThrowExc P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {(\<lbrace>\<rbrace>, let xp' = if hd stk = Null then \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor> else \<lfloor>the_Addr (hd stk)\<rfloor> in (xp', h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs))} &&& exec_instr MEnter P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = {let v = hd stk in if v = Null then (\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs) else (\<lbrace>(Lock, the_Addr v), SyncLock (the_Addr v)\<rbrace>, None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs)} &&& exec_instr MExit P t h stk loc C\<^sub>0 M\<^sub>0 pc frs = (let v = hd stk in if v = Null then {(\<lbrace>\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt NullPointer\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)} else {(\<lbrace>(Unlock, the_Addr v), SyncUnlock (the_Addr v)\<rbrace>, None, h, (tl stk, loc, C\<^sub>0, M\<^sub>0, pc + 1) # frs), (\<lbrace>(UnlockFail, the_Addr v)\<rbrace>, \<lfloor>execute.addr_of_sys_xcpt IllegalMonitorState\<rfloor>, h, (stk, loc, C\<^sub>0, M\<^sub>0, pc) # frs)})
[PROOF STEP]
by(auto 4 4 intro: rev_bexI)


[STATEMENT]
lemma exec_code:
  "exec P t (xcp, h, []) = {}"
  "exec P t (None, h, (stk, loc, C, M, pc) # frs) = exec_instr (instrs_of P C M ! pc) P t h stk loc C M pc frs"
  "exec P t (\<lfloor>a\<rfloor>, h, fr # frs) = {(\<epsilon>, execute.exception_step P a h fr frs)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec P t (xcp, h, []) = {} &&& exec P t (None, h, (stk, loc, C, M, pc) # frs) = exec_instr (instrs_of P C M ! pc) P t h stk loc C M pc frs &&& exec P t (\<lfloor>a\<rfloor>, h, fr # frs) = {(\<lbrace>\<rbrace>, execute.exception_step P a h fr frs)}
[PROOF STEP]
by(simp_all add: exec_def)


[STATEMENT]
lemma exec_1E:
  assumes "Predicate.eval (exec_1 P t \<sigma>) (ta, \<sigma>')"
  obtains "execute.exec_1 P t \<sigma> ta \<sigma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
pred.eval (exec_1 P t \<sigma>) (ta, \<sigma>')

goal (1 subgoal):
 1. (execute.exec_1 P t \<sigma> ta \<sigma>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: exec_1_def exec_def intro: execute.exec_1.intros)


[STATEMENT]
lemma exec_1_eq [simp]:
  "Predicate.eval (exec_1 P t \<sigma>) (ta, \<sigma>') \<longleftrightarrow> execute.exec_1 P t \<sigma> ta \<sigma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred.eval (exec_1 P t \<sigma>) (ta, \<sigma>') = execute.exec_1 P t \<sigma> ta \<sigma>'
[PROOF STEP]
by(auto intro: exec_1I elim: exec_1E)


[STATEMENT]
lemma exec_1_eq':
  "Predicate.eval (exec_1 P t \<sigma>) = (\<lambda>(ta, \<sigma>'). execute.exec_1 P t \<sigma> ta \<sigma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred.eval (exec_1 P t \<sigma>) = (\<lambda>(ta, \<sigma>'). execute.exec_1 P t \<sigma> ta \<sigma>')
[PROOF STEP]
by(rule ext)(simp split: prod.split)


[STATEMENT]
lemma INDEPI: "INDEP v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. INDEP v
[PROOF STEP]
by simp


[STATEMENT]
lemma is_gb_graph: "gb_graph G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gb_graph G
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma "is_acc_run r \<equiv> is_run r \<and> (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run r \<equiv> is_run r \<and> (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A)
[PROOF STEP]
unfolding is_acc_run_def is_acc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_run r \<and> (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A) \<equiv> is_run r \<and> (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A)
[PROOF STEP]
.


[STATEMENT]
lemma acc_run_run: "is_acc_run r \<Longrightarrow> is_run r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run r \<Longrightarrow> is_run r
[PROOF STEP]
unfolding is_acc_run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_run r \<and> is_acc r \<Longrightarrow> is_run r
[PROOF STEP]
by simp


[STATEMENT]
lemma acc_eq_limit:
    assumes FIN: "finite (range r)"
    shows "is_acc r \<longleftrightarrow> (\<forall>A\<in>F. limit r \<inter> A \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc r = (\<forall>A\<in>F. limit r \<inter> A \<noteq> {})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
 2. \<forall>A\<in>F. limit r \<inter> A \<noteq> {} \<Longrightarrow> is_acc r
[PROOF STEP]
assume "\<forall>A\<in>F. limit r \<inter> A \<noteq> {}"
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. limit r \<inter> A \<noteq> {}

goal (2 subgoals):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
 2. \<forall>A\<in>F. limit r \<inter> A \<noteq> {} \<Longrightarrow> is_acc r
[PROOF STEP]
thus "is_acc r"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. limit r \<inter> A \<noteq> {}

goal (1 subgoal):
 1. is_acc r
[PROOF STEP]
unfolding is_acc_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. limit r \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A
[PROOF STEP]
by (metis limit_inter_INF)
[PROOF STATE]
proof (state)
this:
is_acc r

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
from FIN
[PROOF STATE]
proof (chain)
picking this:
finite (range r)
[PROOF STEP]
have FIN': "\<And>A. finite (A \<inter> range r)"
[PROOF STATE]
proof (prove)
using this:
finite (range r)

goal (1 subgoal):
 1. \<And>A. finite (A \<inter> range r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (?A \<inter> range r)

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
assume "is_acc r"
[PROOF STATE]
proof (state)
this:
is_acc r

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
hence AUX: "\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> (A \<inter> range r)"
[PROOF STATE]
proof (prove)
using this:
is_acc r

goal (1 subgoal):
 1. \<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A \<inter> range r
[PROOF STEP]
unfolding is_acc_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A

goal (1 subgoal):
 1. \<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A \<inter> range r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A \<inter> range r

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
have "\<forall>A\<in>F. limit r \<inter> (A \<inter> range r) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>F. limit r \<inter> (A \<inter> range r) \<noteq> {}
[PROOF STEP]
apply (rule ballI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. A \<in> F \<Longrightarrow> limit r \<inter> (A \<inter> range r) \<noteq> {}
[PROOF STEP]
apply (drule bspec[OF AUX])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<exists>\<^sub>\<infinity>i. r i \<in> A \<inter> range r \<Longrightarrow> limit r \<inter> (A \<inter> range r) \<noteq> {}
[PROOF STEP]
apply (subst (asm) fin_ex_inf_eq_limit[OF FIN'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. limit r \<inter> (A \<inter> range r) \<noteq> {} \<Longrightarrow> limit r \<inter> (A \<inter> range r) \<noteq> {}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. limit r \<inter> (A \<inter> range r) \<noteq> {}

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
thus "\<forall>A\<in>F. limit r \<inter> A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. limit r \<inter> (A \<inter> range r) \<noteq> {}

goal (1 subgoal):
 1. \<forall>A\<in>F. limit r \<inter> A \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. limit r \<inter> A \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_acc_run_limit_alt:
    assumes "finite (E\<^sup>* `` V0)"
    shows "is_acc_run r \<longleftrightarrow> is_run r \<and> (\<forall>A\<in>F. limit r \<inter> A \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run r = (is_run r \<and> (\<forall>A\<in>F. limit r \<inter> A \<noteq> {}))
[PROOF STEP]
using assms acc_eq_limit[symmetric]
[PROOF STATE]
proof (prove)
using this:
finite reachable
finite (range ?r) \<Longrightarrow> (\<forall>A\<in>F. limit ?r \<inter> A \<noteq> {}) = is_acc ?r

goal (1 subgoal):
 1. is_acc_run r = (is_run r \<and> (\<forall>A\<in>F. limit r \<inter> A \<noteq> {}))
[PROOF STEP]
unfolding is_acc_run_def
[PROOF STATE]
proof (prove)
using this:
finite reachable
finite (range ?r) \<Longrightarrow> (\<forall>A\<in>F. limit ?r \<inter> A \<noteq> {}) = is_acc ?r

goal (1 subgoal):
 1. (is_run r \<and> is_acc r) = (is_run r \<and> (\<forall>A\<in>F. limit r \<inter> A \<noteq> {}))
[PROOF STEP]
by (auto dest: run_reachable finite_subset)