[STATEMENT]
lemma star:
  fixes p :: perm and F :: "name \<Rightarrow> tm"
  assumes C: "ss_fm \<alpha>"
      and p: "atom ` (p \<bullet> V) \<sharp>* V" "-p = p"
      and V: "finite V" "supp \<alpha> \<subseteq> atom ` V"
      and F: "F = make_F V p"
    shows "insert \<alpha> (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert \<alpha> (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)
[PROOF STEP]
using C V p F
[PROOF STATE]
proof (prove)
using this:
ss_fm \<alpha>
finite V
supp \<alpha> \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. insert \<alpha> (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>\<alpha>\<rfloor>V V F)
[PROOF STEP]
proof (nominal_induct avoiding: p arbitrary: V F rule: ss_fm.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>i j p V F. \<lbrakk>finite V; supp (Var i IN Var j) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 3. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 4. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 5. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
case (MemI i j)
[PROOF STATE]
proof (state)
this:
finite V
supp (Var i IN Var j) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (5 subgoals):
 1. \<And>i j p V F. \<lbrakk>finite V; supp (Var i IN Var j) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 3. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 4. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 5. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
proof (cases "i=j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
 2. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = j

goal (2 subgoals):
 1. i = j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
 2. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i = j

goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
hence ij: "atom i \<sharp> j" "{i, j} \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j

goal (1 subgoal):
 1. atom i \<sharp> j &&& {i, j} \<subseteq> V
[PROOF STEP]
using MemI
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
finite V
supp (Var i IN Var j) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. atom i \<sharp> j &&& {i, j} \<subseteq> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom i \<sharp> j
{i, j} \<subseteq> V

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
interpret qp: quote_perm p V F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p V &&& F \<equiv> make_F V p
[PROOF STEP]
by unfold_locales (auto simp: image_iff F make_F_def p MemI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
have "insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j)))
[PROOF STEP]
apply (rule QuoteP_Mem_imp_QMem [of i j, THEN cut3])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. atom i \<sharp> (j, p \<bullet> j, p \<bullet> i)
 2. atom (p \<bullet> i) \<sharp> (j, p \<bullet> j)
 3. atom j \<sharp> p \<bullet> j
 4. insert (Var i IN Var j) (quote_all p V) \<turnstile> QuoteP (Var i) (Var (p \<bullet> i))
 5. insert (Var i IN Var j) (quote_all p V) \<turnstile> QuoteP (Var j) (Var (p \<bullet> j))
 6. insert (Var i IN Var j) (quote_all p V) \<turnstile> Var i IN Var j
[PROOF STEP]
using ij
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> j
{i, j} \<subseteq> V

goal (6 subgoals):
 1. atom i \<sharp> (j, p \<bullet> j, p \<bullet> i)
 2. atom (p \<bullet> i) \<sharp> (j, p \<bullet> j)
 3. atom j \<sharp> p \<bullet> j
 4. insert (Var i IN Var j) (quote_all p V) \<turnstile> QuoteP (Var i) (Var (p \<bullet> i))
 5. insert (Var i IN Var j) (quote_all p V) \<turnstile> QuoteP (Var j) (Var (p \<bullet> j))
 6. insert (Var i IN Var j) (quote_all p V) \<turnstile> Var i IN Var j
[PROOF STEP]
apply (auto simp: quote_all_def qp.atom_fresh_perm intro: Hyp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom i \<sharp> j; i \<in> V; j \<in> V\<rbrakk> \<Longrightarrow> atom (p \<bullet> i) \<sharp> (j, p \<bullet> j)
[PROOF STEP]
apply (metis atom_eqvt fresh_Pair fresh_at_base(2) fresh_permute_iff qp.atom_fresh_perm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j)))

goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j)))

goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)
[PROOF STEP]
apply (simp add: vquot_fm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j))) \<Longrightarrow> (i \<in> V \<longrightarrow> (j \<in> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (F i) (F j))) \<and> (j \<notin> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (F i) (SUCC (ORD_OF (nat_of_name j)))))) \<and> (i \<notin> V \<longrightarrow> (j \<in> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (SUCC (ORD_OF (nat_of_name i))) (F j))) \<and> (j \<notin> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (SUCC (ORD_OF (nat_of_name i))) (SUCC (ORD_OF (nat_of_name j))))))
[PROOF STEP]
using MemI
[PROOF STATE]
proof (prove)
using this:
finite V
supp (Var i IN Var j) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (Var (p \<bullet> i)) (Var (p \<bullet> j))) \<Longrightarrow> (i \<in> V \<longrightarrow> (j \<in> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (F i) (F j))) \<and> (j \<notin> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (F i) (SUCC (ORD_OF (nat_of_name j)))))) \<and> (i \<notin> V \<longrightarrow> (j \<in> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (SUCC (ORD_OF (nat_of_name i))) (F j))) \<and> (j \<notin> V \<longrightarrow> insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (Q_Mem (SUCC (ORD_OF (nat_of_name i))) (SUCC (ORD_OF (nat_of_name j))))))
[PROOF STEP]
apply (auto simp: make_F_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert (Var i IN Var j) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Var i IN Var j\<rfloor>V V F)

goal (4 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 3. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 4. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 3. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 4. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
case (DisjI A B)
[PROOF STATE]
proof (state)
this:
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
ss_fm B
\<lbrakk>finite ?V; supp B \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert B (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>?V ?V ?F)
finite V
supp (A OR B) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (4 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 3. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 4. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp: quote_perm p V F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p V &&& F \<equiv> make_F V p
[PROOF STEP]
by unfold_locales (auto simp: image_iff DisjI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A OR B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 3. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 4. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. insert B (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
[PROOF STEP]
apply (rule_tac [2] qp.quote_all_Disj_I2_PfP_ssubst)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)
 2. V \<subseteq> V
 3. supp A \<subseteq> atom ` V
 4. supp B \<subseteq> atom ` V
 5. insert B (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F)
 6. quote_all p V \<subseteq> insert B (quote_all p V)
[PROOF STEP]
apply (rule qp.quote_all_Disj_I1_PfP_ssubst)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. V \<subseteq> V
 2. supp A \<subseteq> atom ` V
 3. supp B \<subseteq> atom ` V
 4. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F)
 5. quote_all p V \<subseteq> insert A (quote_all p V)
 6. V \<subseteq> V
 7. supp A \<subseteq> atom ` V
 8. supp B \<subseteq> atom ` V
 9. insert B (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F)
 10. quote_all p V \<subseteq> insert B (quote_all p V)
[PROOF STEP]
using DisjI
[PROOF STATE]
proof (prove)
using this:
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
ss_fm B
\<lbrakk>finite ?V; supp B \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert B (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>?V ?V ?F)
finite V
supp (A OR B) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (10 subgoals):
 1. V \<subseteq> V
 2. supp A \<subseteq> atom ` V
 3. supp B \<subseteq> atom ` V
 4. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F)
 5. quote_all p V \<subseteq> insert A (quote_all p V)
 6. V \<subseteq> V
 7. supp A \<subseteq> atom ` V
 8. supp B \<subseteq> atom ` V
 9. insert B (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F)
 10. quote_all p V \<subseteq> insert B (quote_all p V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (A OR B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A OR B\<rfloor>V V F)

goal (3 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 2. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 3. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 2. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 3. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
case (ConjI A B)
[PROOF STATE]
proof (state)
this:
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
ss_fm B
\<lbrakk>finite ?V; supp B \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert B (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>?V ?V ?F)
finite V
supp (A AND B) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (3 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 2. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 3. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp: quote_perm p V F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p V &&& F \<equiv> make_F V p
[PROOF STEP]
by unfold_locales (auto simp: image_iff ConjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A B p V F. \<lbrakk>ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); ss_fm B; \<And>b V F. \<lbrakk>finite V; supp B \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert B (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F); finite V; supp (A AND B) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
 2. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 3. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)
[PROOF STEP]
apply (rule qp.quote_all_Conj_I_PfP_ssubst)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. V \<subseteq> V
 2. supp A \<subseteq> atom ` V
 3. supp B \<subseteq> atom ` V
 4. insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F)
 5. insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F)
 6. quote_all p V \<subseteq> insert (A AND B) (quote_all p V)
[PROOF STEP]
using ConjI
[PROOF STATE]
proof (prove)
using this:
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
ss_fm B
\<lbrakk>finite ?V; supp B \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert B (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>?V ?V ?F)
finite V
supp (A AND B) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (6 subgoals):
 1. V \<subseteq> V
 2. supp A \<subseteq> atom ` V
 3. supp B \<subseteq> atom ` V
 4. insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F)
 5. insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>B\<rfloor>V V F)
 6. quote_all p V \<subseteq> insert (A AND B) (quote_all p V)
[PROOF STEP]
by (auto intro: thin1 thin2)
[PROOF STATE]
proof (state)
this:
insert (A AND B) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>A AND B\<rfloor>V V F)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
case (ExI A i)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
finite V
supp (SyntaxN.Ex i A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp: quote_perm p V F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p V &&& F \<equiv> make_F V p
[PROOF STEP]
by unfold_locales (auto simp: image_iff ExI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
obtain i'::name where i': "atom i' \<sharp> (i,p,A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. atom i' \<sharp> (i, p, A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i' \<sharp> (i, p, A)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
define p' where "p' = (atom i \<rightleftharpoons> atom i') + p"
[PROOF STATE]
proof (state)
this:
p' = (atom i \<rightleftharpoons> atom i') + p

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
define F' where "F' = make_F (insert i V) p'"
[PROOF STATE]
proof (state)
this:
F' = make_F (insert i V) p'

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have p'_apply [simp]: "!!v. p' \<bullet> v = (if v=i then i' else if v=i' then i else p \<bullet> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. p' \<bullet> v = (if v = i then i' else if v = i' then i else p \<bullet> v)
[PROOF STEP]
using  \<open>atom i \<sharp> p\<close>  i'
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> p
atom i' \<sharp> (i, p, A)

goal (1 subgoal):
 1. \<And>v. p' \<bullet> v = (if v = i then i' else if v = i' then i else p \<bullet> v)
[PROOF STEP]
by (auto simp: p'_def fresh_Pair fresh_at_base_permI)
         (metis atom_eq_iff fresh_at_base_permI permute_eq_iff swap_at_base_simps(3))
[PROOF STATE]
proof (state)
this:
p' \<bullet> ?v = (if ?v = i then i' else if ?v = i' then i else p \<bullet> ?v)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have p'V: "p' \<bullet> V = p \<bullet> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<bullet> V = p \<bullet> V
[PROOF STEP]
by (metis i' p'_def permute_plus fresh_Pair qp.fresh_pVs swap_fresh_fresh \<open>atom i \<sharp> p\<close>)
[PROOF STATE]
proof (state)
this:
p' \<bullet> V = p \<bullet> V

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have i: "i \<notin> V" "i \<notin> p \<bullet> V"  "atom i \<sharp> V" "atom i \<sharp> p \<bullet> V"  "atom i \<sharp> p' \<bullet> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i \<notin> V &&& i \<notin> p \<bullet> V) &&& atom i \<sharp> V &&& atom i \<sharp> p \<bullet> V &&& atom i \<sharp> p' \<bullet> V
[PROOF STEP]
using ExI
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
finite V
supp (SyntaxN.Ex i A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. (i \<notin> V &&& i \<notin> p \<bullet> V) &&& atom i \<sharp> V &&& atom i \<sharp> p \<bullet> V &&& atom i \<sharp> p' \<bullet> V
[PROOF STEP]
by (auto simp: p'V fresh_finite_set_at_base notin_V)
[PROOF STATE]
proof (state)
this:
i \<notin> V
i \<notin> p \<bullet> V
atom i \<sharp> V
atom i \<sharp> p \<bullet> V
atom i \<sharp> p' \<bullet> V

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp': quote_perm p' "insert i V" F'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p' (insert i V) &&& F' \<equiv> make_F (insert i V) p'
[PROOF STEP]
by (auto simp: qp.qp_insert i' p'_def F'_def  \<open>atom i \<sharp> p\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
fix W t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
assume W: "W \<subseteq> V" "i\<notin>W" "i'\<notin>W"
[PROOF STATE]
proof (state)
this:
W \<subseteq> V
i \<notin> W
i' \<notin> W

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence "finite W"
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> V
i \<notin> W
i' \<notin> W

goal (1 subgoal):
 1. finite W
[PROOF STEP]
by (metis \<open>finite V\<close> infinite_super)
[PROOF STATE]
proof (state)
this:
finite W

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence "ssubst t W F' = ssubst t W F"
[PROOF STATE]
proof (prove)
using this:
finite W

goal (1 subgoal):
 1. ssubst t W F' = ssubst t W F
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
finite W
W \<subseteq> V
i \<notin> W
i' \<notin> W

goal (1 subgoal):
 1. ssubst t W F' = ssubst t W F
[PROOF STEP]
by induct (auto simp: qp.ssubst_insert_if qp'.ssubst_insert_if qp.F_unfold qp'.F_unfold)
[PROOF STATE]
proof (state)
this:
ssubst t W F' = ssubst t W F

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?W2 \<subseteq> V; i \<notin> ?W2; i' \<notin> ?W2\<rbrakk> \<Longrightarrow> ssubst ?t2 ?W2 F' = ssubst ?t2 ?W2 F

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence ss_simp: "ssubst \<lfloor>Ex i A\<rfloor>(insert i V) (insert i V) F' = ssubst \<lfloor>Ex i A\<rfloor>V V F"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?W2 \<subseteq> V; i \<notin> ?W2; i' \<notin> ?W2\<rbrakk> \<Longrightarrow> ssubst ?t2 ?W2 F' = ssubst ?t2 ?W2 F

goal (1 subgoal):
 1. ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F' = ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?W2 \<subseteq> V; i \<notin> ?W2; i' \<notin> ?W2\<rbrakk> \<Longrightarrow> ssubst ?t2 ?W2 F' = ssubst ?t2 ?W2 F
i \<notin> V
i \<notin> p \<bullet> V
atom i \<sharp> V
atom i \<sharp> p \<bullet> V
atom i \<sharp> p' \<bullet> V

goal (1 subgoal):
 1. ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F' = ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F
[PROOF STEP]
by (metis equalityE insertCI p'_apply qp'.perm_exits_Vs qp'.ssubst_vquot_Ex qp.Vs)
[PROOF STATE]
proof (state)
this:
ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F' = ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have qa_p': "quote_all p' V = quote_all p V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p' V = quote_all p V
[PROOF STEP]
using i i' ExI.hyps(1)
[PROOF STATE]
proof (prove)
using this:
i \<notin> V
i \<notin> p \<bullet> V
atom i \<sharp> V
atom i \<sharp> p \<bullet> V
atom i \<sharp> p' \<bullet> V
atom i' \<sharp> (i, p, A)
atom i \<sharp> p

goal (1 subgoal):
 1. quote_all p' V = quote_all p V
[PROOF STEP]
by (auto simp: p'_def quote_all_perm_eq)
[PROOF STATE]
proof (state)
this:
quote_all p' V = quote_all p V

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have ss: "(quote_all p' (insert i V))
              \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F') IMP
                PfP (ssubst \<lfloor>Ex i A\<rfloor>(insert i V) (insert i V) F')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p' (insert i V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F') IMP PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')
[PROOF STEP]
apply (rule qp'.quote_all_MonPon_PfP_ssubst [OF SpecI])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. insert i V \<subseteq> insert i V
 2. supp A \<subseteq> atom ` insert i V
 3. supp (SyntaxN.Ex i A) \<subseteq> atom ` insert i V
[PROOF STEP]
using ExI
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
finite V
supp (SyntaxN.Ex i A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (3 subgoals):
 1. insert i V \<subseteq> insert i V
 2. supp A \<subseteq> atom ` insert i V
 3. supp (SyntaxN.Ex i A) \<subseteq> atom ` insert i V
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
quote_all p' (insert i V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F') IMP PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence "insert A (quote_all p' (insert i V))
           \<turnstile> PfP (ssubst \<lfloor>Ex i A\<rfloor>(insert i V) (insert i V) F')"
[PROOF STATE]
proof (prove)
using this:
quote_all p' (insert i V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F') IMP PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')

goal (1 subgoal):
 1. insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')
[PROOF STEP]
apply (rule MP_thin)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ?HB \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F')
 2. quote_all p' (insert i V) \<union> ?HB \<subseteq> insert A (quote_all p' (insert i V))
[PROOF STEP]
apply (rule ExI(3) [of "insert i V" p' F'])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. finite (insert i V)
 2. supp A \<subseteq> atom ` insert i V
 3. atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
 4. - p' = p'
 5. F' = make_F (insert i V) p'
 6. quote_all p' (insert i V) \<union> insert A (quote_all p' (insert i V)) \<subseteq> insert A (quote_all p' (insert i V))
[PROOF STEP]
apply (metis \<open>finite V\<close> finite_insert)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. supp A \<subseteq> atom ` insert i V
 2. atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
 3. - p' = p'
 4. F' = make_F (insert i V) p'
 5. quote_all p' (insert i V) \<union> insert A (quote_all p' (insert i V)) \<subseteq> insert A (quote_all p' (insert i V))
[PROOF STEP]
using \<open>supp (Ex i A) \<subseteq> _\<close> qp'.p qp'.pinv i'
[PROOF STATE]
proof (prove)
using this:
supp (SyntaxN.Ex i A) \<subseteq> atom ` V
atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
- p' = p'
atom i' \<sharp> (i, p, A)

goal (5 subgoals):
 1. supp A \<subseteq> atom ` insert i V
 2. atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
 3. - p' = p'
 4. F' = make_F (insert i V) p'
 5. quote_all p' (insert i V) \<union> insert A (quote_all p' (insert i V)) \<subseteq> insert A (quote_all p' (insert i V))
[PROOF STEP]
apply (auto simp: F'_def fresh_finite_insert)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence "insert (QuoteP (Var i) (Var i')) (insert A (quote_all p V))
           \<turnstile> PfP (ssubst \<lfloor>Ex i A\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>(insert i V) (insert i V) F')

goal (1 subgoal):
 1. insert (QuoteP (Var i) (Var i')) (insert A (quote_all p V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
[PROOF STEP]
by (auto simp: insert_commute ss_simp qa_p')
[PROOF STATE]
proof (state)
this:
insert (QuoteP (Var i) (Var i')) (insert A (quote_all p V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence Exi': "insert (Ex i' (QuoteP (Var i) (Var i'))) (insert A (quote_all p V))
                 \<turnstile> PfP (ssubst \<lfloor>Ex i A\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
insert (QuoteP (Var i) (Var i')) (insert A (quote_all p V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (1 subgoal):
 1. insert (SyntaxN.Ex i' (QuoteP (Var i) (Var i'))) (insert A (quote_all p V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
[PROOF STEP]
by (auto intro!: qp.fresh_ssubst_fm) (auto simp: ExI i' fresh_quote_all_mem)
[PROOF STATE]
proof (state)
this:
insert (SyntaxN.Ex i' (QuoteP (Var i) (Var i'))) (insert A (quote_all p V)) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have "insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Ex i A\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
[PROOF STEP]
using i'
[PROOF STATE]
proof (prove)
using this:
atom i' \<sharp> (i, p, A)

goal (1 subgoal):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
[PROOF STEP]
by (auto intro: cut0 [OF exists_QuoteP Exi'])
[PROOF STATE]
proof (state)
this:
insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (2 subgoals):
 1. \<And>A i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); finite V; supp (SyntaxN.Ex i A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
 2. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
thus "insert (Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>Ex i A\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (1 subgoal):
 1. insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)
[PROOF STEP]
apply (rule Ex_E, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F) \<Longrightarrow> atom i \<sharp> ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F
 2. \<forall>C\<in>quote_all p V. atom i \<sharp> C
[PROOF STEP]
apply (rule qp.fresh_ssubst_fm)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F) \<Longrightarrow> atom i \<sharp> p \<bullet> V
 2. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F) \<Longrightarrow> V \<subseteq> V
 3. \<forall>C\<in>quote_all p V. atom i \<sharp> C
[PROOF STEP]
using i ExI
[PROOF STATE]
proof (prove)
using this:
i \<notin> V
i \<notin> p \<bullet> V
atom i \<sharp> V
atom i \<sharp> p \<bullet> V
atom i \<sharp> p' \<bullet> V
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
finite V
supp (SyntaxN.Ex i A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (3 subgoals):
 1. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F) \<Longrightarrow> atom i \<sharp> p \<bullet> V
 2. insert A (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F) \<Longrightarrow> V \<subseteq> V
 3. \<forall>C\<in>quote_all p V. atom i \<sharp> C
[PROOF STEP]
apply (auto simp: fresh_quote_all_mem)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert (SyntaxN.Ex i A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>SyntaxN.Ex i A\<rfloor>V V F)

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
case (All2I A j i p V F)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
atom j \<sharp> i
atom j \<sharp> A
finite V
supp (All2 i (Var j) A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp: quote_perm p V F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p V &&& F \<equiv> make_F V p
[PROOF STEP]
by unfold_locales (auto simp: image_iff All2I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
obtain i'::name where i': "atom i' \<sharp> (i,p,A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i'. atom i' \<sharp> (i, p, A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i' \<sharp> (i, p, A)

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
define p' where "p' = (atom i \<rightleftharpoons> atom i') + p"
[PROOF STATE]
proof (state)
this:
p' = (atom i \<rightleftharpoons> atom i') + p

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
define F' where "F' = make_F (insert i V) p'"
[PROOF STATE]
proof (state)
this:
F' = make_F (insert i V) p'

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
interpret qp': quote_perm p' "insert i V" F'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_perm p' (insert i V) &&& F' \<equiv> make_F (insert i V) p'
[PROOF STEP]
using \<open>atom i \<sharp> p\<close> i'
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> p
atom i' \<sharp> (i, p, A)

goal (1 subgoal):
 1. quote_perm p' (insert i V) &&& F' \<equiv> make_F (insert i V) p'
[PROOF STEP]
by (auto simp: qp.qp_insert p'_def F'_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have p'_apply [simp]: "p' \<bullet> i = i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p' \<bullet> i = i'
[PROOF STEP]
using \<open>atom i \<sharp> p\<close>
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> p

goal (1 subgoal):
 1. p' \<bullet> i = i'
[PROOF STEP]
by (auto simp: p'_def fresh_at_base_permI)
[PROOF STATE]
proof (state)
this:
p' \<bullet> i = i'

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have qa_p': "quote_all p' V = quote_all p V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quote_all p' V = quote_all p V
[PROOF STEP]
using i' All2I
[PROOF STATE]
proof (prove)
using this:
atom i' \<sharp> (i, p, A)
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
atom j \<sharp> i
atom j \<sharp> A
finite V
supp (All2 i (Var j) A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p

goal (1 subgoal):
 1. quote_all p' V = quote_all p V
[PROOF STEP]
by (auto simp: p'_def quote_all_perm_eq)
[PROOF STATE]
proof (state)
this:
quote_all p' V = quote_all p V

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
have "insert A (quote_all p' (insert i V))
          \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F')
[PROOF STEP]
apply (rule All2I.hyps)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. finite (insert i V)
 2. supp A \<subseteq> atom ` insert i V
 3. atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
 4. - p' = p'
 5. F' = make_F (insert i V) p'
[PROOF STEP]
using \<open>supp (All2 i _ A) \<subseteq> _\<close>   qp'.p qp'.pinv
[PROOF STATE]
proof (prove)
using this:
supp (All2 i (Var j) A) \<subseteq> atom ` V
atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
- p' = p'

goal (5 subgoals):
 1. finite (insert i V)
 2. supp A \<subseteq> atom ` insert i V
 3. atom ` (p' \<bullet> insert i V) \<sharp>* insert i V
 4. - p' = p'
 5. F' = make_F (insert i V) p'
[PROOF STEP]
apply (auto simp: F'_def fresh_finite_insert)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F')

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
hence "insert (QuoteP (Var i) (Var i')) (quote_all p V)
           \<turnstile> A IMP PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) (make_F (insert i V) p'))"
[PROOF STATE]
proof (prove)
using this:
insert A (quote_all p' (insert i V)) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) F')

goal (1 subgoal):
 1. insert (QuoteP (Var i) (Var i')) (quote_all p V) \<turnstile> A IMP PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) (make_F (insert i V) p'))
[PROOF STEP]
by (auto simp: insert_commute qa_p' F'_def)
[PROOF STATE]
proof (state)
this:
insert (QuoteP (Var i) (Var i')) (quote_all p V) \<turnstile> A IMP PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) (make_F (insert i V) p'))

goal (1 subgoal):
 1. \<And>A j i p V F. \<lbrakk>atom i \<sharp> p; ss_fm A; \<And>b V F. \<lbrakk>finite V; supp A \<subseteq> atom ` V; atom ` (b \<bullet> V) \<sharp>* V; - b = b; F = make_F V b\<rbrakk> \<Longrightarrow> insert A (quote_all b V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>V V F); atom j \<sharp> i; atom j \<sharp> A; finite V; supp (All2 i (Var j) A) \<subseteq> atom ` V; atom ` (p \<bullet> V) \<sharp>* V; - p = p; F = make_F V p\<rbrakk> \<Longrightarrow> insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
thus "insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)"
[PROOF STATE]
proof (prove)
using this:
insert (QuoteP (Var i) (Var i')) (quote_all p V) \<turnstile> A IMP PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) (make_F (insert i V) p'))

goal (1 subgoal):
 1. insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
using All2I i' qp.quote_all_Mem_imp_All2
[PROOF STATE]
proof (prove)
using this:
insert (QuoteP (Var i) (Var i')) (quote_all p V) \<turnstile> A IMP PfP (ssubst \<lfloor>A\<rfloor>(insert i V) (insert i V) (make_F (insert i V) p'))
atom i \<sharp> p
ss_fm A
\<lbrakk>finite ?V; supp A \<subseteq> atom ` ?V; atom ` (?b \<bullet> ?V) \<sharp>* ?V; - ?b = ?b; ?F = make_F ?V ?b\<rbrakk> \<Longrightarrow> insert A (quote_all ?b ?V) \<turnstile> PfP (ssubst \<lfloor>A\<rfloor>?V ?V ?F)
atom j \<sharp> i
atom j \<sharp> A
finite V
supp (All2 i (Var j) A) \<subseteq> atom ` V
atom ` (p \<bullet> V) \<sharp>* V
- p = p
F = make_F V p
atom i' \<sharp> (i, p, A)
\<lbrakk>insert (QuoteP (Var ?i) (Var ?i')) (quote_all p V) \<turnstile> ?\<alpha> IMP PfP (ssubst \<lfloor>?\<alpha>\<rfloor>(insert ?i V) (insert ?i V) ?Fi); supp (All2 ?i (Var ?j) ?\<alpha>) \<subseteq> atom ` V; 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 V) ?pi\<rbrakk> \<Longrightarrow> insert (All2 ?i (Var ?j) ?\<alpha>) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 ?i (Var ?j) ?\<alpha>\<rfloor>V V F)

goal (1 subgoal):
 1. insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)
[PROOF STEP]
by (simp add: p'_def)
[PROOF STATE]
proof (state)
this:
insert (All2 i (Var j) A) (quote_all p V) \<turnstile> PfP (ssubst \<lfloor>All2 i (Var j) A\<rfloor>V V F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Provability:
  assumes "Sigma_fm \<alpha>" "ground_fm \<alpha>"
    shows "{\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
obtain \<beta> where \<beta>: "ss_fm \<beta>" "ground_fm \<beta>" "{} \<turnstile> \<alpha> IFF \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<beta>. \<lbrakk>ss_fm \<beta>; ground_fm \<beta>; {} \<turnstile> \<alpha> IFF \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Sigma_fm \<alpha>
ground_fm \<alpha>

goal (1 subgoal):
 1. (\<And>\<beta>. \<lbrakk>ss_fm \<beta>; ground_fm \<beta>; {} \<turnstile> \<alpha> IFF \<beta>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Sigma_fm_def ground_fm_aux_def)
[PROOF STATE]
proof (state)
this:
ss_fm \<beta>
ground_fm \<beta>
{} \<turnstile> \<alpha> IFF \<beta>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
hence "{\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>"
[PROOF STATE]
proof (prove)
using this:
ss_fm \<beta>
ground_fm \<beta>
{} \<turnstile> \<alpha> IFF \<beta>

goal (1 subgoal):
 1. {\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
using star [of \<beta> 0 "{}"]
[PROOF STATE]
proof (prove)
using this:
ss_fm \<beta>
ground_fm \<beta>
{} \<turnstile> \<alpha> IFF \<beta>
\<lbrakk>ss_fm \<beta>; atom ` (0 \<bullet> {}) \<sharp>* {}; - 0 = 0; finite {}; supp \<beta> \<subseteq> atom ` {}; ?F = make_F {} 0\<rbrakk> \<Longrightarrow> insert \<beta> (quote_all 0 {}) \<turnstile> PfP (ssubst \<lfloor>\<beta>\<rfloor>{} {} ?F)

goal (1 subgoal):
 1. {\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
by (auto simp: ground_fm_aux_def fresh_star_def)
[PROOF STATE]
proof (state)
this:
{\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
have "{\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>"
[PROOF STATE]
proof (prove)
using this:
{\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
using \<beta>
[PROOF STATE]
proof (prove)
using this:
{\<beta>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
ss_fm \<beta>
ground_fm \<beta>
{} \<turnstile> \<alpha> IFF \<beta>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
[PROOF STEP]
by (metis Iff_MP_left')
[PROOF STATE]
proof (state)
this:
{\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
have "{} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>
[PROOF STEP]
using \<beta>
[PROOF STATE]
proof (prove)
using this:
ss_fm \<beta>
ground_fm \<beta>
{} \<turnstile> \<alpha> IFF \<beta>

goal (1 subgoal):
 1. {} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>
[PROOF STEP]
by (metis Conj_E2 Iff_def proved_imp_proved_PfP)
[PROOF STATE]
proof (state)
this:
{} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
{} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{\<alpha>} \<turnstile> PfP \<guillemotleft>\<beta>\<guillemotright>
{} \<turnstile> PfP \<guillemotleft>\<beta> IMP \<alpha>\<guillemotright>

goal (1 subgoal):
 1. {\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
by (metis PfP_implies_ModPon_PfP_quot thin0)
[PROOF STATE]
proof (state)
this:
{\<alpha>} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>

goal:
No subgoals!
[PROOF STEP]
qed