[STATEMENT]
lemma (in quote_perm) quote_all_Mem_imp_All2:
  assumes IH: "insert (QuoteP (Var i) (Var i')) (quote_all p Vs)
               \<turnstile> \<alpha> IMP PfP (ssubst \<lfloor>\<alpha>\<rfloor>(insert i Vs) (insert i Vs) Fi)"
      and "supp (All2 i (Var j) \<alpha>) \<subseteq> atom ` Vs"
      and j: "atom j \<sharp> (i,\<alpha>)" and i: "atom i \<sharp> p" and i': "atom i' \<sharp> (i,p,\<alpha>)"
      and pi: "pi = (atom i \<rightleftharpoons> atom i') + p"
      and Fi: "Fi = make_F (insert i Vs) pi"
  shows "insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
have sp: "supp \<alpha> - {atom i} \<subseteq> atom ` Vs" and jV: "j \<in> Vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp \<alpha> - {atom i} \<subseteq> atom ` Vs &&& j \<in> Vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert (QuoteP (Var i) (Var i')) (quote_all p Vs) \<turnstile> \<alpha> IMP PfP (ssubst \<lfloor>\<alpha>\<rfloor>(insert i Vs) (insert i Vs) Fi)
supp (All2 i (Var j) \<alpha>) \<subseteq> atom ` Vs
atom j \<sharp> (i, \<alpha>)
atom i \<sharp> p
atom i' \<sharp> (i, p, \<alpha>)
pi = (atom i \<rightleftharpoons> atom i') + p
Fi = make_F (insert i Vs) pi

goal (1 subgoal):
 1. supp \<alpha> - {atom i} \<subseteq> atom ` Vs &&& j \<in> Vs
[PROOF STEP]
by (auto simp: fresh_def supp_Pair)
[PROOF STATE]
proof (state)
this:
supp \<alpha> - {atom i} \<subseteq> atom ` Vs
j \<in> Vs

goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
obtain s::name and k::name
    where atoms: "atom s \<sharp> (k,i,j,p\<bullet>j,\<alpha>,p)" "atom k \<sharp> (i,j,p\<bullet>j,\<alpha>,p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s k. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)

goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
hence ii: "atom i \<sharp> (j, p \<bullet> j, s, k, p)"
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)

goal (1 subgoal):
 1. atom i \<sharp> (j, p \<bullet> j, s, k, p)
[PROOF STEP]
using i j
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)
atom i \<sharp> p
atom j \<sharp> (i, \<alpha>)

goal (1 subgoal):
 1. atom i \<sharp> (j, p \<bullet> j, s, k, p)
[PROOF STEP]
by (simp add: fresh_Pair) (metis fresh_at_base(2) fresh_perm fresh_permute_left pinv)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> (j, p \<bullet> j, s, k, p)

goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
have jj: "atom j \<sharp> (p \<bullet> j, s, k, \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> (p \<bullet> j, s, k, \<alpha>)
[PROOF STEP]
using atoms j
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)
atom j \<sharp> (i, \<alpha>)

goal (1 subgoal):
 1. atom j \<sharp> (p \<bullet> j, s, k, \<alpha>)
[PROOF STEP]
by (auto simp: fresh_Pair) (metis atom_fresh_perm jV)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (p \<bullet> j, s, k, \<alpha>)

goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
have pj: "atom (p \<bullet> j) \<sharp> (s, k, \<alpha>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom (p \<bullet> j) \<sharp> (s, k, \<alpha>)
[PROOF STEP]
using atoms ii sp jV
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)
atom i \<sharp> (j, p \<bullet> j, s, k, p)
supp \<alpha> - {atom i} \<subseteq> atom ` Vs
j \<in> Vs

goal (1 subgoal):
 1. atom (p \<bullet> j) \<sharp> (s, k, \<alpha>)
[PROOF STEP]
by (simp add: fresh_Pair) (auto simp: fresh_def perm_exits_Vs dest!: subsetD)
[PROOF STATE]
proof (state)
this:
atom (p \<bullet> j) \<sharp> (s, k, \<alpha>)

goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
apply (rule cut_same [where A = "QuoteP (Var j) (Var (p \<bullet> j))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> QuoteP (Var j) (Var (p \<bullet> j))
 2. insert (QuoteP (Var j) (Var (p \<bullet> j))) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
apply (force intro: jV Hyp simp add: quote_all_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (QuoteP (Var j) (Var (p \<bullet> j))) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
using atoms
[PROOF STATE]
proof (prove)
using this:
atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p)
atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)

goal (1 subgoal):
 1. insert (QuoteP (Var j) (Var (p \<bullet> j))) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
[PROOF STEP]
apply (auto simp: QuoteP.simps [of s _ _ k] elim!: fresh_quote_all_mem)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
 2. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom k \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
 3. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom s \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
[PROOF STEP]
apply (rule MP_same)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> ?A40 IMP PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)
 2. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> ?A40
 3. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom k \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
 4. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom s \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
[PROOF STEP]
apply (rule SeqQuoteP_Mem_imp_All2 [OF IH sp jV refl pi Fi ii i' jj pj, THEN thin])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom s \<sharp> (k, \<alpha>)
 2. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom k \<sharp> (\<alpha>, p)
 3. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (quote_all p (Vs - {j})) \<subseteq> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs))
 4. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> insert (SeqQuoteP (Var j) (Var (p \<bullet> j)) (Var s) (Var k)) (insert (All2 i (Var j) \<alpha>) (quote_all p Vs)) \<turnstile> All2 i (Var j) \<alpha>
 5. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom k \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
 6. \<lbrakk>atom s \<sharp> (k, i, j, p \<bullet> j, \<alpha>, p); atom k \<sharp> (i, j, p \<bullet> j, \<alpha>, p)\<rbrakk> \<Longrightarrow> atom s \<sharp> ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F
[PROOF STEP]
apply (auto simp: fresh_at_base_permI quote_all_def intro!: fresh_ssubst')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert (All2 i (Var j) \<alpha>) (quote_all p Vs) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) \<alpha>\<rfloor>Vs Vs F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SpecI: "H \<turnstile> A IMP Ex i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IMP SyntaxN.Ex i A
[PROOF STEP]
by (metis Imp_I Assume Ex_I subst_fm_id)