[STATEMENT]
lemma proved_imp_Pf: assumes "H \<turnstile> \<alpha>" "H={}" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> \<alpha>
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> H; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>H. H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 7. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 8. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 9. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Hyp A H)
[PROOF STATE]
proof (state)
this:
A \<in> H
H = {}

goal (9 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> H; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>H. H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 7. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 8. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 9. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> H
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (8 subgoals):
 1. \<And>H. H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 7. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 8. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>H. H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 7. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 8. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Extra H)
[PROOF STATE]
proof (state)
this:
H = {}

goal (8 subgoals):
 1. \<And>H. H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 7. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 8. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis extra_axiom_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e

goal (7 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 7. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 7. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Bool A H)
[PROOF STATE]
proof (state)
this:
A \<in> boolean_axioms
H = {}

goal (7 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> boolean_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 6. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 7. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> boolean_axioms
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis boolean_axioms_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (6 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 6. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 6. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Eq A H)
[PROOF STATE]
proof (state)
this:
A \<in> equality_axioms
H = {}

goal (6 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> equality_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 5. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 6. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> equality_axioms
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis equality_axioms_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (5 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 5. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 5. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (HF A H)
[PROOF STATE]
proof (state)
this:
A \<in> HF_axioms
H = {}

goal (5 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> HF_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 4. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 5. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> HF_axioms
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis HF_axioms_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (4 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 4. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 4. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Spec A H)
[PROOF STATE]
proof (state)
this:
A \<in> special_axioms
H = {}

goal (4 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> special_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 4. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> special_axioms
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis special_axioms_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (3 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 3. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 3. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Ind A H)
[PROOF STATE]
proof (state)
this:
A \<in> induction_axioms
H = {}

goal (3 subgoals):
 1. \<And>A H. \<lbrakk>A \<in> induction_axioms; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 2. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 3. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
A \<in> induction_axioms
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis induction_axioms_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (2 subgoals):
 1. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 2. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 2. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (MP H A B H')
[PROOF STATE]
proof (state)
this:
H \<turnstile> A IMP B
H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
H' \<turnstile> A
H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
H \<union> H' = {}

goal (2 subgoals):
 1. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; H' \<turnstile> A; H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; H \<union> H' = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
 2. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
H' \<turnstile> A
H' = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
H \<union> H' = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis quot_ModPon_imp_Pf Un_empty)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
case (Exists H A B i)
[PROOF STATE]
proof (state)
this:
H \<turnstile> A IMP B
H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C
H = {}

goal (1 subgoal):
 1. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C; H = {}\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
H = {} \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C
H = {}

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis quot_Exists_imp_Pf)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sent_imp_hfthm:
  assumes "x \<in> Sent" shows "\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
obtain y z w where "Form y" "Form z" "Form w" and axs: "Sent_axioms x y z w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y z w. \<lbrakk>Form y; Form z; Form w; Sent_axioms x y z w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Sent

goal (1 subgoal):
 1. (\<And>y z w. \<lbrakk>Form y; Form z; Form w; Sent_axioms x y z w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Sent_def)
[PROOF STATE]
proof (state)
this:
Form y
Form z
Form w
Sent_axioms x y z w

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Form y
Form z
Form w
Sent_axioms x y z w
[PROOF STEP]
obtain A::fm and B::fm and C::fm
         where A: "y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e" and B: "z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e" and C: "w = \<lbrakk>\<guillemotleft>C\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
Form y
Form z
Form w
Sent_axioms x y z w

goal (1 subgoal):
 1. (\<And>A B C. \<lbrakk>y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e; w = \<lbrakk>\<guillemotleft>C\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Form_imp_is_fm)
[PROOF STATE]
proof (state)
this:
y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
w = \<lbrakk>\<guillemotleft>C\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
have "\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (force simp add: A quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
have "\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (force intro!: exI [where x="A IMP (A OR B)"]
                simp add: A B quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
have "\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (force intro!: exI [where x="(A OR A) IMP A"]
                simp add: A quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
have "\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (force intro!: exI [where x="(A OR (B OR C)) IMP ((A OR B) OR C)"]
                simp add: A B C quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
have "\<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (force intro!: exI [where x="(A OR B) IMP ((Neg A OR C) IMP (B OR C))"]
                simp add: A B C quot_Disj quot_Neg q_defs hfthm.Bool boolean_axioms.intros)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
using axs [unfolded Sent_axioms_def]
[PROOF STATE]
proof (prove)
using this:
\<exists>A. q_Imp y y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp y (q_Disj y z) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y y) y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
x = q_Imp y y \<or> x = q_Imp y (q_Disj y z) \<or> x = q_Imp (q_Disj y y) y \<or> x = q_Imp (q_Disj y (q_Disj z w)) (q_Disj (q_Disj y z) w) \<or> x = q_Imp (q_Disj y z) (q_Imp (q_Disj (q_Neg y) w) (q_Disj z w))

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Extra_ax_imp_hfthm:
  assumes "x \<in> Extra_ax" obtains A where "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Extra_ax

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Extra_ax_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {\<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e0}

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: eval_quot_fm_ignore hfthm.Extra)


[STATEMENT]
lemma Equality_ax_imp_hfthm:
  assumes "x \<in> Equality_ax" obtains A where "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Equality_ax

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Equality_ax_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {\<lbrakk>\<guillemotleft>refl_ax\<guillemotright>\<rbrakk>e0, \<lbrakk>\<guillemotleft>eq_cong_ax\<guillemotright>\<rbrakk>e0, \<lbrakk>\<guillemotleft>mem_cong_ax\<guillemotright>\<rbrakk>e0, \<lbrakk>\<guillemotleft>eats_cong_ax\<guillemotright>\<rbrakk>e0}

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: eval_quot_fm_ignore hfthm.Eq [unfolded equality_axioms_def])


[STATEMENT]
lemma HF_ax_imp_hfthm:
  assumes "x \<in> HF_ax" obtains A where "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> HF_ax

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding HF_ax_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {\<lbrakk>\<guillemotleft>HF1\<guillemotright>\<rbrakk>e0, \<lbrakk>\<guillemotleft>HF2\<guillemotright>\<rbrakk>e0}

goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto intro: eval_quot_fm_ignore hfthm.HF [unfolded HF_axioms_def])


[STATEMENT]
lemma Special_ax_imp_hfthm:
  assumes "x \<in> Special_ax" obtains A where "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e" "{} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. \<lbrakk>x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; {} \<turnstile> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Spec Special_ax_imp_special_axioms assms)


[STATEMENT]
lemma Induction_ax_imp_hfthm:
  assumes "x \<in> Induction_ax" obtains A where "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e" "{} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. \<lbrakk>x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; {} \<turnstile> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Induction_ax_imp_induction_axioms assms hfthm.Ind)


[STATEMENT]
lemma Exists_imp_hfthm: "\<lbrakk>Exists \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e y; {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>B. y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Exists \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e y; {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>B. y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> B
[PROOF STEP]
by (drule Exists_imp_exists [where e=e]) (auto intro: anti_deduction)


[STATEMENT]
lemma Subst_imp_hfthm:  "\<lbrakk>Subst \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e y; {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>B. y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subst \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e y; {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>B. y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> B
[PROOF STEP]
by (drule Subst_imp_subst [where e=e], auto intro: Subst)


[STATEMENT]
lemma eval_Neg_imp_Neg: "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e = q_Neg x \<Longrightarrow> \<exists>A. \<alpha> = Neg A \<and> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e = q_Neg x \<Longrightarrow> \<exists>A. \<alpha> = Neg A \<and> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = x
[PROOF STEP]
by (cases \<alpha> rule: fm.exhaust) (auto simp: quot_simps q_defs htuple_minus_1)


[STATEMENT]
lemma eval_Disj_imp_Disj: "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e = q_Disj x y \<Longrightarrow> \<exists>A B. \<alpha> = A OR B \<and> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = x \<and> \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e = q_Disj x y \<Longrightarrow> \<exists>A B. \<alpha> = A OR B \<and> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = x \<and> \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e = y
[PROOF STEP]
by (cases \<alpha> rule: fm.exhaust) (auto simp: quot_simps q_defs htuple_minus_1)


[STATEMENT]
lemma Prf_imp_proved: assumes "Prf s k x" shows "\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
using assms [unfolded Prf_def Axiom_def]
[PROOF STATE]
proof (prove)
using this:
BuildSeq (\<lambda>x. x \<in> Extra_ax \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax) (\<lambda>u v w. ModPon v w u \<or> Exists v u \<or> Subst v u) s k x

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
proof (induction x rule: BuildSeq_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> Extra_ax \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
 2. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
case (B x)
[PROOF STATE]
proof (state)
this:
x \<in> Extra_ax \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax

goal (2 subgoals):
 1. \<And>x. x \<in> Extra_ax \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
 2. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
x \<in> Extra_ax \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (auto intro: Extra_ax_imp_hfthm Sent_imp_hfthm Equality_ax_imp_hfthm HF_ax_imp_hfthm
                    Special_ax_imp_hfthm Induction_ax_imp_hfthm)
[PROOF STATE]
proof (state)
this:
\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
case (C x y z)
[PROOF STATE]
proof (state)
this:
ModPon y z x \<or> Exists y x \<or> Subst y x
\<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ModPon y z x \<or> Exists y x \<or> Subst y x
\<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
obtain A::fm and B::fm where "y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e" "{} \<turnstile> A" "z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e" "{} \<turnstile> B"
[PROOF STATE]
proof (prove)
using this:
ModPon y z x \<or> Exists y x \<or> Subst y x
\<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
\<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; {} \<turnstile> A; z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e; {} \<turnstile> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
{} \<turnstile> A
z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
{} \<turnstile> B

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>ModPon y z x \<or> Exists y x \<or> Subst y x; \<exists>A. y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A; \<exists>A. z = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A\<rbrakk> \<Longrightarrow> \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
{} \<turnstile> A
z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
{} \<turnstile> B

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
using C.hyps ModPon_def q_Imp_def
[PROOF STATE]
proof (prove)
using this:
y = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
{} \<turnstile> A
z = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
{} \<turnstile> B
ModPon y z x \<or> Exists y x \<or> Subst y x
ModPon ?x ?y ?z \<equiv> ?y = q_Imp ?x ?z
q_Imp ?t ?u \<equiv> q_Disj (q_Neg ?t) ?u

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A
[PROOF STEP]
by (auto dest!: MP_same eval_Neg_imp_Neg eval_Disj_imp_Disj Exists_imp_hfthm Subst_imp_hfthm)
[PROOF STATE]
proof (state)
this:
\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> {} \<turnstile> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem proved_iff_proved_PfP: "{} \<turnstile> \<alpha> \<longleftrightarrow> {} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> \<alpha> = {} \<turnstile> PfP \<guillemotleft>\<alpha>\<guillemotright>
[PROOF STEP]
by (metis Pf_quot_imp_is_proved emptyE eval_fm_PfP hfthm_sound proved_imp_proved_PfP)


[STATEMENT]
lemma  override_on_belowI:
  assumes "\<And> a. a \<in> S \<Longrightarrow> y a \<sqsubseteq> z a"
  and "\<And> a. a \<notin> S \<Longrightarrow> x a \<sqsubseteq> z a"
  shows  "x ++\<^bsub>S\<^esub> y \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ++\<^bsub>S\<^esub> y \<sqsubseteq> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> S \<Longrightarrow> y ?a \<sqsubseteq> z ?a
?a \<notin> S \<Longrightarrow> x ?a \<sqsubseteq> z ?a

goal (1 subgoal):
 1. x ++\<^bsub>S\<^esub> y \<sqsubseteq> z
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. a \<in> S \<Longrightarrow> y a \<sqsubseteq> z a; \<And>a. a \<notin> S \<Longrightarrow> x a \<sqsubseteq> z a\<rbrakk> \<Longrightarrow> x ++\<^bsub>S\<^esub> y \<sqsubseteq> z
[PROOF STEP]
apply (rule fun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>a. a \<in> S \<Longrightarrow> y a \<sqsubseteq> z a; \<And>a. a \<notin> S \<Longrightarrow> x a \<sqsubseteq> z a\<rbrakk> \<Longrightarrow> (x ++\<^bsub>S\<^esub> y) xa \<sqsubseteq> z xa
[PROOF STEP]
apply (case_tac "xa \<in> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>\<And>a. a \<in> S \<Longrightarrow> y a \<sqsubseteq> z a; \<And>a. a \<notin> S \<Longrightarrow> x a \<sqsubseteq> z a; xa \<in> S\<rbrakk> \<Longrightarrow> (x ++\<^bsub>S\<^esub> y) xa \<sqsubseteq> z xa
 2. \<And>xa. \<lbrakk>\<And>a. a \<in> S \<Longrightarrow> y a \<sqsubseteq> z a; \<And>a. a \<notin> S \<Longrightarrow> x a \<sqsubseteq> z a; xa \<notin> S\<rbrakk> \<Longrightarrow> (x ++\<^bsub>S\<^esub> y) xa \<sqsubseteq> z xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma override_on_cont1: "cont (\<lambda> x. x ++\<^bsub>S\<^esub> m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. x ++\<^bsub>S\<^esub> m)
[PROOF STEP]
by (rule cont2cont_lambda) (auto simp add: override_on_def)


[STATEMENT]
lemma override_on_cont2: "cont (\<lambda> x. m ++\<^bsub>S\<^esub> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (override_on_syn m S)
[PROOF STEP]
by (rule cont2cont_lambda) (auto simp add: override_on_def)


[STATEMENT]
lemma override_on_cont2cont[simp, cont2cont]:
  assumes "cont f"
  assumes "cont g"
  shows "cont (\<lambda> x. f x ++\<^bsub>S\<^esub> g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. f x ++\<^bsub>S\<^esub> g x)
[PROOF STEP]
by (rule cont_apply[OF assms(1) override_on_cont1 cont_compose[OF override_on_cont2 assms(2)]])


[STATEMENT]
lemma override_on_mono:
  assumes "x1 \<sqsubseteq> (x2 :: 'a::type \<Rightarrow> 'b::cpo)"
  assumes "y1 \<sqsubseteq> y2"
  shows "x1 ++\<^bsub>S\<^esub> y1 \<sqsubseteq> x2 ++\<^bsub>S\<^esub> y2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 ++\<^bsub>S\<^esub> y1 \<sqsubseteq> x2 ++\<^bsub>S\<^esub> y2
[PROOF STEP]
by (rule below_trans[OF cont2monofunE[OF override_on_cont1 assms(1)] cont2monofunE[OF override_on_cont2 assms(2)]])


[STATEMENT]
lemma fun_upd_below_env_deleteI:
  assumes "env_delete x \<rho> \<sqsubseteq> env_delete x \<rho>'"
  assumes "y \<sqsubseteq> \<rho>' x"
  shows  "\<rho>(x := y) \<sqsubseteq> \<rho>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho>(x := y) \<sqsubseteq> \<rho>'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
env_delete x \<rho> \<sqsubseteq> env_delete x \<rho>'
y \<sqsubseteq> \<rho>' x

goal (1 subgoal):
 1. \<rho>(x := y) \<sqsubseteq> \<rho>'
[PROOF STEP]
apply (auto intro!: fun_upd_belowI   simp add: env_delete_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>\<rho>(x := \<bottom>) \<sqsubseteq> \<rho>'(x := \<bottom>); y \<sqsubseteq> \<rho>' x; z \<noteq> x\<rbrakk> \<Longrightarrow> \<rho> z \<sqsubseteq> \<rho>' z
[PROOF STEP]
by (metis fun_belowD fun_upd_other)


[STATEMENT]
lemma fun_upd_belowI2:
  assumes "\<And> z . z \<noteq> x \<Longrightarrow> \<rho> z \<sqsubseteq> \<rho>' z"
  assumes "\<rho> x \<sqsubseteq> y"
  shows  "\<rho> \<sqsubseteq> \<rho>'(x := y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<sqsubseteq> \<rho>'(x := y)
[PROOF STEP]
apply (rule fun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<rho> xa \<sqsubseteq> (\<rho>'(x := y)) xa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?z \<noteq> x \<Longrightarrow> \<rho> ?z \<sqsubseteq> \<rho>' ?z
\<rho> x \<sqsubseteq> y

goal (1 subgoal):
 1. \<And>xa. \<rho> xa \<sqsubseteq> (\<rho>'(x := y)) xa
[PROOF STEP]
by auto


[STATEMENT]
lemma env_restr_belowI:
  assumes  "\<And> x. x \<in> S \<Longrightarrow> (m1 f|` S) x \<sqsubseteq> (m2 f|` S) x"
  shows "m1 f|` S \<sqsubseteq> m2 f|` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 f|` S \<sqsubseteq> m2 f|` S
[PROOF STEP]
apply (rule fun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (m1 f|` S) x \<sqsubseteq> (m2 f|` S) x
[PROOF STEP]
by (metis assms below_bottom_iff lookup_env_restr_not_there)


[STATEMENT]
lemma env_restr_belowI2:
  assumes  "\<And> x. x \<in> S \<Longrightarrow> m1 x \<sqsubseteq> m2 x"
  shows "m1 f|` S \<sqsubseteq> m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 f|` S \<sqsubseteq> m2
[PROOF STEP]
by (rule fun_belowI)
     (simp add: assms env_restr_def)


[STATEMENT]
lemma env_restr_below_itself:
  shows "m f|` S \<sqsubseteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m f|` S \<sqsubseteq> m
[PROOF STEP]
apply (rule fun_belowI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (m f|` S) x \<sqsubseteq> m x
[PROOF STEP]
apply (case_tac "x \<in> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> (m f|` S) x \<sqsubseteq> m x
 2. \<And>x. x \<notin> S \<Longrightarrow> (m f|` S) x \<sqsubseteq> m x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma env_restr_cont:  "cont (env_restr S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (env_restr S)
[PROOF STEP]
apply (rule cont2cont_lambda)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. cont (\<lambda>x. (x f|` S) y)
[PROOF STEP]
apply (case_tac "y \<in> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. y \<in> S \<Longrightarrow> cont (\<lambda>x. (x f|` S) y)
 2. \<And>y. y \<notin> S \<Longrightarrow> cont (\<lambda>x. (x f|` S) y)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma env_restr_belowD:
  assumes "m1 f|` S \<sqsubseteq> m2 f|` S"
  assumes "x \<in> S"
  shows "m1 x \<sqsubseteq> m2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 x \<sqsubseteq> m2 x
[PROOF STEP]
using fun_belowD[OF assms(1), where x = x] assms(2)
[PROOF STATE]
proof (prove)
using this:
(m1 f|` S) x \<sqsubseteq> (m2 f|` S) x
x \<in> S

goal (1 subgoal):
 1. m1 x \<sqsubseteq> m2 x
[PROOF STEP]
by simp


[STATEMENT]
lemma env_restr_eqD:
  assumes "m1 f|` S = m2 f|` S"
  assumes "x \<in> S"
  shows "m1 x = m2  x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 x = m2 x
[PROOF STEP]
by (metis assms(1) assms(2) lookup_env_restr)


[STATEMENT]
lemma env_restr_below_subset:
  assumes "S \<subseteq> S'"
  and "m1 f|` S' \<sqsubseteq> m2 f|` S'"
  shows "m1 f|` S \<sqsubseteq> m2 f|` S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m1 f|` S \<sqsubseteq> m2 f|` S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> S'
m1 f|` S' \<sqsubseteq> m2 f|` S'

goal (1 subgoal):
 1. m1 f|` S \<sqsubseteq> m2 f|` S
[PROOF STEP]
by (auto intro!: env_restr_belowI dest: env_restr_belowD)


[STATEMENT]
lemma  override_on_below_restrI:
  assumes " x f|` (-S) \<sqsubseteq> z f|` (-S)"
  and "y f|` S \<sqsubseteq> z f|` S"
  shows  "x ++\<^bsub>S\<^esub> y \<sqsubseteq> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ++\<^bsub>S\<^esub> y \<sqsubseteq> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x f|` (- S) \<sqsubseteq> z f|` (- S)
y f|` S \<sqsubseteq> z f|` S

goal (1 subgoal):
 1. x ++\<^bsub>S\<^esub> y \<sqsubseteq> z
[PROOF STEP]
by (auto intro: override_on_belowI dest:env_restr_belowD)


[STATEMENT]
lemma  fmap_below_add_restrI:
  assumes "x f|` (-S) \<sqsubseteq> y f|` (-S)"
  and     "x f|` S \<sqsubseteq> z f|` S"
  shows  "x \<sqsubseteq> y ++\<^bsub>S\<^esub> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqsubseteq> y ++\<^bsub>S\<^esub> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x f|` (- S) \<sqsubseteq> y f|` (- S)
x f|` S \<sqsubseteq> z f|` S

goal (1 subgoal):
 1. x \<sqsubseteq> y ++\<^bsub>S\<^esub> z
[PROOF STEP]
by (auto intro!: fun_belowI dest:env_restr_belowD simp add: lookup_override_on_eq)


[STATEMENT]
lemma env_delete_cont:  "cont (env_delete x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (env_delete x)
[PROOF STEP]
apply (rule cont2cont_lambda)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. cont (\<lambda>xa. env_delete x xa y)
[PROOF STEP]
apply (case_tac "y = x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. y = x \<Longrightarrow> cont (\<lambda>xa. env_delete x xa y)
 2. \<And>y. y \<noteq> x \<Longrightarrow> cont (\<lambda>xa. env_delete x xa y)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma state_\<alpha>_conv [simp]:
  "locks (state_\<alpha> s) = locks s"
  "thr (state_\<alpha> s) = thr_\<alpha> (thr s)"
  "shr (state_\<alpha> s) = shr s"
  "wset (state_\<alpha> s) = ws_\<alpha> (wset s)"
  "interrupts (state_\<alpha> s) = is_\<alpha> (interrupts s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (locks (state_\<alpha> s) = locks s &&& thr (state_\<alpha> s) = thr_\<alpha> (thr s)) &&& shr (state_\<alpha> s) = shr s &&& wset (state_\<alpha> s) = ws_\<alpha> (wset s) &&& interrupts (state_\<alpha> s) = is_\<alpha> (interrupts s)
[PROOF STEP]
by(case_tac [!] s) auto


[STATEMENT]
lemma state_invarD [simp]:
  assumes "state_invar s"
  shows "thr_invar (thr s)" "ws_invar (wset s)" "is_invar (interrupts s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thr_invar (thr s) &&& ws_invar (wset s) &&& is_invar (interrupts s)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state_invar s

goal (1 subgoal):
 1. thr_invar (thr s) &&& ws_invar (wset s) &&& is_invar (interrupts s)
[PROOF STEP]
by(case_tac [!] s) auto


[STATEMENT]
lemma is_path_nonempty [forward]: "is_path n S p \<Longrightarrow> p \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_path n S p \<Longrightarrow> p \<noteq> []
[PROOF STEP]
by auto2


[STATEMENT]
lemma nonempty_is_not_path [resolve]: "\<not>is_path n S []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_path n S []
[PROOF STEP]
by auto2


[STATEMENT]
lemma is_path_extend [forward]:
  "is_path n S p \<Longrightarrow> S \<subseteq> T \<Longrightarrow> is_path n T p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path n S p; S \<subseteq> T\<rbrakk> \<Longrightarrow> is_path n T p
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path n S p; S \<subseteq> T\<rbrakk> \<Longrightarrow> is_path n T p
[PROOF STEP]
@induct p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_path n S p; S \<subseteq> T\<rbrakk> \<Longrightarrow> is_path n T p
[PROOF STEP]
@qed


[STATEMENT]
lemma has_path_extend [forward]:
  "has_path n S i j \<Longrightarrow> S \<subseteq> T \<Longrightarrow> has_path n T i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; S \<subseteq> T\<rbrakk> \<Longrightarrow> has_path n T i j
[PROOF STEP]
by auto2


[STATEMENT]
lemma path_join_hd [rewrite]: "p \<noteq> [] \<Longrightarrow> hd (path_join p q) = hd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> hd (path_join p q) = hd p
[PROOF STEP]
by auto2


[STATEMENT]
lemma path_join_last [rewrite]: "joinable p q \<Longrightarrow> q \<noteq> [] \<Longrightarrow> last (path_join p q) = last q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; q \<noteq> []\<rbrakk> \<Longrightarrow> last (path_join p q) = last q
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; q \<noteq> []\<rbrakk> \<Longrightarrow> last (path_join p q) = last q
[PROOF STEP]
@have "q = hd q # tl q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; q \<noteq> []\<rbrakk> \<Longrightarrow> last (path_join p q) = last q
[PROOF STEP]
@case "tl q = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; q \<noteq> []\<rbrakk> \<Longrightarrow> last (path_join p q) = last q
[PROOF STEP]
@qed


[STATEMENT]
lemma path_join_is_path [backward]:
  "joinable p q \<Longrightarrow> is_path n S p \<Longrightarrow> is_path n S q \<Longrightarrow> is_path n S (path_join p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; is_path n S p; is_path n S q\<rbrakk> \<Longrightarrow> is_path n S (path_join p q)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; is_path n S p; is_path n S q\<rbrakk> \<Longrightarrow> is_path n S (path_join p q)
[PROOF STEP]
@induct p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>joinable p q; is_path n S p; is_path n S q\<rbrakk> \<Longrightarrow> is_path n S (path_join p q)
[PROOF STEP]
@qed


[STATEMENT]
lemma has_path_trans [forward]:
  "has_path n S i j \<Longrightarrow> has_path n S j k \<Longrightarrow> has_path n S i k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; has_path n S j k\<rbrakk> \<Longrightarrow> has_path n S i k
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; has_path n S j k\<rbrakk> \<Longrightarrow> has_path n S i k
[PROOF STEP]
@obtain p where "is_path n S p" "hd p = i" "last p = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; has_path n S j k\<rbrakk> \<Longrightarrow> has_path n S i k
[PROOF STEP]
@obtain q where "is_path n S q" "hd q = j" "last q = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; has_path n S j k\<rbrakk> \<Longrightarrow> has_path n S i k
[PROOF STEP]
@have "is_path n S (path_join p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_path n S i j; has_path n S j k\<rbrakk> \<Longrightarrow> has_path n S i k
[PROOF STEP]
@qed


[STATEMENT]
lemma has_path_single1 [backward1]:
  "is_valid_graph n S \<Longrightarrow> (a, b) \<in> S \<Longrightarrow> has_path n S a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S a b
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S a b
[PROOF STEP]
@have "is_path n S [a, b]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S a b
[PROOF STEP]
@qed


[STATEMENT]
lemma has_path_single2 [backward1]:
  "is_valid_graph n S \<Longrightarrow> (a, b) \<in> S \<Longrightarrow> has_path n S b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S b a
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S b a
[PROOF STEP]
@have "is_path n S [b, a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; (a, b) \<in> S\<rbrakk> \<Longrightarrow> has_path n S b a
[PROOF STEP]
@qed


[STATEMENT]
lemma has_path_refl [backward2]:
  "is_valid_graph n S \<Longrightarrow> a < n \<Longrightarrow> has_path n S a a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; a < n\<rbrakk> \<Longrightarrow> has_path n S a a
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; a < n\<rbrakk> \<Longrightarrow> has_path n S a a
[PROOF STEP]
@have "is_path n S [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; a < n\<rbrakk> \<Longrightarrow> has_path n S a a
[PROOF STEP]
@qed


[STATEMENT]
lemma connected_rel_iff [rewrite]:
  "(a, b) \<in> connected_rel n S \<longleftrightarrow> has_path n S a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> connected_rel n S) = has_path n S a b
[PROOF STEP]
using connected_rel_def
[PROOF STATE]
proof (prove)
using this:
connected_rel ?n ?S = {(a, b). has_path ?n ?S a b}

goal (1 subgoal):
 1. ((a, b) \<in> connected_rel n S) = has_path n S a b
[PROOF STEP]
by simp


[STATEMENT]
lemma connected_rel_trans [forward]:
  "trans (connected_rel n S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trans (connected_rel n S)
[PROOF STEP]
by auto2


[STATEMENT]
lemma connected_rel_refl [backward2]:
  "is_valid_graph n S \<Longrightarrow> a < n \<Longrightarrow> (a, a) \<in> connected_rel n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n S; a < n\<rbrakk> \<Longrightarrow> (a, a) \<in> connected_rel n S
[PROOF STEP]
by auto2


[STATEMENT]
lemma is_path_per_union [rewrite]:
  "is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow>
   has_path n (S \<union> {(a, b)}) i j \<longleftrightarrow> (i, j) \<in> per_union (connected_rel n S) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@let "R = connected_rel n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@let "S' = S \<union> {(a, b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "S \<subseteq> S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(i, j) \<in> per_union R a b" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(i, a) \<in> R \<and> (b, j) \<in> R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' i a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' b j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(i, b) \<in> R \<and> (a, j) \<in> R" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' i b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "has_path n S' a j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "has_path n S' i j" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have (@rule) "\<forall>p. is_path n S' p \<longrightarrow> (hd p, last p) \<in> per_union R a b" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@induct p @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@subgoal "p = x # xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "(x, hd xs) \<in> per_union R a b" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@have "is_valid_graph n S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(x, hd xs) \<in> S'" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(x, hd xs) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(hd xs, x) \<in> S'" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@case "(hd xs, x) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@obtain p where "is_path n S' p" "hd p = i" "last p = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> has_path n (S \<union> {(a, b)}) i j = ((i, j) \<in> per_union (connected_rel n S) a b)
[PROOF STEP]
@qed


[STATEMENT]
lemma connected_rel_union [rewrite]:
  "is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow>
   connected_rel n (S \<union> {(a, b)}) = per_union (connected_rel n S) a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (S \<union> {(a, b)}) \<Longrightarrow> connected_rel n (S \<union> {(a, b)}) = per_union (connected_rel n S) a b
[PROOF STEP]
by auto2


[STATEMENT]
lemma connected_rel_init [rewrite]:
  "connected_rel n {} = uf_init_rel n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@have "is_valid_graph n {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@have "\<forall>i j. has_path n {} i j \<longleftrightarrow> (i, j) \<in> uf_init_rel n" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@case "has_path n {} i j" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@obtain p where "is_path n {} p" "hd p = i" "last p = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@have "p = hd p # tl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected_rel n {} = uf_init_rel n
[PROOF STEP]
@qed


[STATEMENT]
lemma connected_rel_ind_rule [rewrite]:
  "is_valid_graph n (set es) \<Longrightarrow> k \<le> length es \<Longrightarrow>
   connected_rel_ind n es k = connected_rel n (set (take k es))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@induct k @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@subgoal "k = Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@have "is_valid_graph n (set (take (Suc m) es))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@endgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_valid_graph n (set es); k \<le> length es\<rbrakk> \<Longrightarrow> connected_rel_ind n es k = connected_rel n (set (take k es))
[PROOF STEP]
@qed


[STATEMENT]
theorem connected_rel_ind_compute [rewrite]:
  "is_valid_graph n (set es) \<Longrightarrow>
   connected_rel_ind n es (length es) = connected_rel n (set es)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_valid_graph n (set es) \<Longrightarrow> connected_rel_ind n es (length es) = connected_rel n (set es)
[PROOF STEP]
by auto2


[STATEMENT]
lemma height_size_braun: "braun t \<Longrightarrow> 2 ^ (height t) \<le> 2 * size t + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun t \<Longrightarrow> 2 ^ height t \<le> 2 * size t + 1
[PROOF STEP]
proof(induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. braun \<langle>\<rangle> \<Longrightarrow> 2 ^ height \<langle>\<rangle> \<le> 2 * size \<langle>\<rangle> + 1
 2. \<And>t1 x2 t2. \<lbrakk>braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1; braun t2 \<Longrightarrow> 2 ^ height t2 \<le> 2 * size t2 + 1; braun \<langle>t1, x2, t2\<rangle>\<rbrakk> \<Longrightarrow> 2 ^ height \<langle>t1, x2, t2\<rangle> \<le> 2 * size \<langle>t1, x2, t2\<rangle> + 1
[PROOF STEP]
case (Node t1)
[PROOF STATE]
proof (state)
this:
braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1
braun t2_ \<Longrightarrow> 2 ^ height t2_ \<le> 2 * size t2_ + 1
braun \<langle>t1, x2_, t2_\<rangle>

goal (2 subgoals):
 1. braun \<langle>\<rangle> \<Longrightarrow> 2 ^ height \<langle>\<rangle> \<le> 2 * size \<langle>\<rangle> + 1
 2. \<And>t1 x2 t2. \<lbrakk>braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1; braun t2 \<Longrightarrow> 2 ^ height t2 \<le> 2 * size t2 + 1; braun \<langle>t1, x2, t2\<rangle>\<rbrakk> \<Longrightarrow> 2 ^ height \<langle>t1, x2, t2\<rangle> \<le> 2 * size \<langle>t1, x2, t2\<rangle> + 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
proof (cases "height t1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. height t1 = 0 \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
 2. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
height t1 = 0

goal (2 subgoals):
 1. height t1 = 0 \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
 2. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
height t1 = 0

goal (1 subgoal):
 1. 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
using Node
[PROOF STATE]
proof (prove)
using this:
height t1 = 0
braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1
braun t2_ \<Longrightarrow> 2 ^ height t2_ \<le> 2 * size t2_ + 1
braun \<langle>t1, x2_, t2_\<rangle>

goal (1 subgoal):
 1. 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1

goal (1 subgoal):
 1. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
height t1 = Suc n

goal (1 subgoal):
 1. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
hence "2 ^ n \<le> size t1"
[PROOF STATE]
proof (prove)
using this:
height t1 = Suc n

goal (1 subgoal):
 1. 2 ^ n \<le> size t1
[PROOF STEP]
using Node
[PROOF STATE]
proof (prove)
using this:
height t1 = Suc n
braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1
braun t2_ \<Longrightarrow> 2 ^ height t2_ \<le> 2 * size t2_ + 1
braun \<langle>t1, x2_, t2_\<rangle>

goal (1 subgoal):
 1. 2 ^ n \<le> size t1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ n \<le> size t1

goal (1 subgoal):
 1. \<And>nat. height t1 = Suc nat \<Longrightarrow> 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> size t1

goal (1 subgoal):
 1. 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
using Suc Node
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> size t1
height t1 = Suc n
braun t1 \<Longrightarrow> 2 ^ height t1 \<le> 2 * size t1 + 1
braun t2_ \<Longrightarrow> 2 ^ height t2_ \<le> 2 * size t2_ + 1
braun \<langle>t1, x2_, t2_\<rangle>

goal (1 subgoal):
 1. 2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1
[PROOF STEP]
by(auto simp: max_def)
[PROOF STATE]
proof (state)
this:
2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ height \<langle>t1, x2_, t2_\<rangle> \<le> 2 * size \<langle>t1, x2_, t2_\<rangle> + 1

goal (1 subgoal):
 1. braun \<langle>\<rangle> \<Longrightarrow> 2 ^ height \<langle>\<rangle> \<le> 2 * size \<langle>\<rangle> + 1
[PROOF STEP]
qed simp


[STATEMENT]
lemma get_min: "\<lbrakk> heap t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min t = Min_mset (mset_tree t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap t; t \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> get_min t = Min_mset (mset_tree t)
[PROOF STEP]
by (auto simp add: eq_Min_iff neq_Leaf_iff)


[STATEMENT]
lemma size_insert[simp]: "size(insert x t) = size t + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (insert x t) = size t + 1
[PROOF STEP]
by(induction t arbitrary: x) auto


[STATEMENT]
lemma set_insert[simp]: "set_tree(insert x t) = {x} \<union> (set_tree t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_tree (insert x t) = {x} \<union> set_tree t
[PROOF STEP]
by(simp add: mset_insert flip: set_mset_tree)


[STATEMENT]
lemma braun_insert: "braun t \<Longrightarrow> braun(insert x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun t \<Longrightarrow> braun (insert x t)
[PROOF STEP]
by(induction t arbitrary: x) auto


[STATEMENT]
lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap t \<Longrightarrow> heap (insert x t)
[PROOF STEP]
by(induction t arbitrary: x) (auto  simp add: ball_Un)


[STATEMENT]
lemma del_left_mset_plus:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf
  \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'
[PROOF STEP]
by (induction t arbitrary: x t' rule: del_left.induct;
    auto split: prod.splits)


[STATEMENT]
lemma del_left_mset:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf
  \<Longrightarrow> x \<in># mset_tree t \<and> mset_tree t' = mset_tree t - {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> x \<in># mset_tree t \<and> mset_tree t' = mset_tree t - {#x#}
[PROOF STEP]
by (simp add: del_left_mset_plus)


[STATEMENT]
lemma del_left_set:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> set_tree t = {x} \<union> set_tree t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> set_tree t = {x} \<union> set_tree t'
[PROOF STEP]
by(simp add: del_left_mset_plus flip: set_mset_tree)


[STATEMENT]
lemma del_left_heap:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> heap t \<Longrightarrow> heap t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>; heap t\<rbrakk> \<Longrightarrow> heap t'
[PROOF STEP]
by (induction t arbitrary: x t' rule: del_left.induct;
    fastforce split: prod.splits dest: del_left_set[THEN equalityD2])


[STATEMENT]
lemma del_left_size:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> size t = size t' + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>\<rbrakk> \<Longrightarrow> size t = size t' + 1
[PROOF STEP]
by(induction t arbitrary: x t' rule: del_left.induct;
    auto split: prod.splits)


[STATEMENT]
lemma del_left_braun:
  "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t \<Longrightarrow> braun t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>del_left t = (x, t'); t \<noteq> \<langle>\<rangle>; braun t\<rbrakk> \<Longrightarrow> braun t'
[PROOF STEP]
by(induction t arbitrary: x t' rule: del_left.induct;
    auto split: prod.splits dest: del_left_size)


[STATEMENT]
lemma size_sift_down:
  "braun(Node l a r) \<Longrightarrow> size(sift_down l a r) = size l + size r + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun \<langle>l, a, r\<rangle> \<Longrightarrow> size (sift_down l a r) = size l + size r + 1
[PROOF STEP]
by(induction l a r rule: sift_down.induct) (auto simp: Let_def)


[STATEMENT]
lemma braun_sift_down:
  "braun(Node l a r) \<Longrightarrow> braun(sift_down l a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun \<langle>l, a, r\<rangle> \<Longrightarrow> braun (sift_down l a r)
[PROOF STEP]
by(induction l a r rule: sift_down.induct) (auto simp: size_sift_down Let_def)


[STATEMENT]
lemma mset_sift_down:
  "braun(Node l a r) \<Longrightarrow> mset_tree(sift_down l a r) = {#a#} + (mset_tree l + mset_tree r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun \<langle>l, a, r\<rangle> \<Longrightarrow> mset_tree (sift_down l a r) = {#a#} + (mset_tree l + mset_tree r)
[PROOF STEP]
by(induction l a r rule: sift_down.induct) (auto simp: ac_simps Let_def)


[STATEMENT]
lemma set_sift_down: "braun(Node l a r)
  \<Longrightarrow> set_tree(sift_down l a r) = {a} \<union> (set_tree l \<union> set_tree r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun \<langle>l, a, r\<rangle> \<Longrightarrow> set_tree (sift_down l a r) = {a} \<union> (set_tree l \<union> set_tree r)
[PROOF STEP]
by(drule arg_cong[where f=set_mset, OF mset_sift_down]) (simp)


[STATEMENT]
lemma heap_sift_down:
  "braun(Node l a r) \<Longrightarrow> heap l \<Longrightarrow> heap r \<Longrightarrow> heap(sift_down l a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>braun \<langle>l, a, r\<rangle>; heap l; heap r\<rbrakk> \<Longrightarrow> heap (sift_down l a r)
[PROOF STEP]
by (induction l a r rule: sift_down.induct) (auto simp: set_sift_down ball_Un Let_def)


[STATEMENT]
lemma braun_del_min: "braun t \<Longrightarrow> braun(del_min t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. braun t \<Longrightarrow> braun (del_min t)
[PROOF STEP]
apply(cases t rule: del_min.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>braun t; t = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
 2. \<And>x r. \<lbrakk>braun t; t = \<langle>\<langle>\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
 3. \<And>v va vb x r. \<lbrakk>braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>braun t; t = \<langle>\<langle>\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
 2. \<And>v va vb x r. \<lbrakk>braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v va vb x r. \<lbrakk>braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> braun (del_min t)
[PROOF STEP]
apply (fastforce split: prod.split intro!: braun_sift_down
  dest: del_left_size del_left_braun)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heap_del_min: "heap t \<Longrightarrow> braun t \<Longrightarrow> heap(del_min t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap t; braun t\<rbrakk> \<Longrightarrow> heap (del_min t)
[PROOF STEP]
apply(cases t rule: del_min.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heap t; braun t; t = \<langle>\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
 2. \<And>x r. \<lbrakk>heap t; braun t; t = \<langle>\<langle>\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
 3. \<And>v va vb x r. \<lbrakk>heap t; braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>heap t; braun t; t = \<langle>\<langle>\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
 2. \<And>v va vb x r. \<lbrakk>heap t; braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v va vb x r. \<lbrakk>heap t; braun t; t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle>\<rbrakk> \<Longrightarrow> heap (del_min t)
[PROOF STEP]
apply (fastforce split: prod.split intro!: heap_sift_down
  dest: del_left_size del_left_braun del_left_heap)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done