[STATEMENT]
theorem Rice_3: "\<lbrakk> C \<subseteq> ce_sets; computable { n. nat_to_ce_set n \<in> C} \<rbrakk> \<Longrightarrow> C = {} \<or> C = ce_sets"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}\<rbrakk> \<Longrightarrow> C = {} \<or> C = ce_sets
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A1: "C \<subseteq> ce_sets"
[PROOF STATE]
proof (state)
this:
C \<subseteq> ce_sets

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A2: "computable { n. nat_to_ce_set n \<in> C}"
[PROOF STATE]
proof (state)
this:
computable {n. nat_to_ce_set n \<in> C}

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume A3: "\<not> (C = {} \<or> C = ce_sets)"
[PROOF STATE]
proof (state)
this:
\<not> (C = {} \<or> C = ce_sets)

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
\<not> (C = {} \<or> C = ce_sets)
[PROOF STEP]
have A4: "C \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<not> (C = {} \<or> C = ce_sets)

goal (1 subgoal):
 1. C \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from A3
[PROOF STATE]
proof (chain)
picking this:
\<not> (C = {} \<or> C = ce_sets)
[PROOF STEP]
have A5: "C \<noteq> ce_sets"
[PROOF STATE]
proof (prove)
using this:
\<not> (C = {} \<or> C = ce_sets)

goal (1 subgoal):
 1. C \<noteq> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C \<noteq> ce_sets

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define A where "A = { n. nat_to_ce_set n \<in> C}"
[PROOF STATE]
proof (state)
this:
A = {n. nat_to_ce_set n \<in> C}

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have S1: "index_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_set A
[PROOF STEP]
proof (unfold index_set_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A
[PROOF STEP]
show "\<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A
[PROOF STEP]
proof (rule allI, rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
assume A1_1: "n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m"
[PROOF STATE]
proof (state)
this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
from A1_1
[PROOF STATE]
proof (chain)
picking this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have "n \<in> A"
[PROOF STATE]
proof (prove)
using this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. n \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in> A

goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<in> A
[PROOF STEP]
have S1_1: "nat_to_ce_set n \<in> C"
[PROOF STATE]
proof (prove)
using this:
n \<in> A

goal (1 subgoal):
 1. nat_to_ce_set n \<in> C
[PROOF STEP]
by (unfold A_def, auto)
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n \<in> C

goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
from A1_1
[PROOF STATE]
proof (chain)
picking this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have "nat_to_ce_set n = nat_to_ce_set m"
[PROOF STATE]
proof (prove)
using this:
n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
with S1_1
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set n \<in> C
nat_to_ce_set n = nat_to_ce_set m
[PROOF STEP]
have "nat_to_ce_set m \<in> C"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set n \<in> C
nat_to_ce_set n = nat_to_ce_set m

goal (1 subgoal):
 1. nat_to_ce_set m \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set m \<in> C

goal (1 subgoal):
 1. \<And>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<Longrightarrow> m \<in> A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set m \<in> C
[PROOF STEP]
show "m \<in> A"
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set m \<in> C

goal (1 subgoal):
 1. m \<in> A
[PROOF STEP]
by (unfold A_def, auto)
[PROOF STATE]
proof (state)
this:
m \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n m. n \<in> A \<and> nat_to_ce_set n = nat_to_ce_set m \<longrightarrow> m \<in> A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
index_set A

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have S2: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
from A4
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> {}
[PROOF STEP]
obtain B where S2_1: "B \<in> C"
[PROOF STATE]
proof (prove)
using this:
C \<noteq> {}

goal (1 subgoal):
 1. (\<And>B. B \<in> C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> C

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
with A1
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> ce_sets
B \<in> C
[PROOF STEP]
have "B \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> ce_sets
B \<in> C

goal (1 subgoal):
 1. B \<in> ce_sets
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> ce_sets

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
[PROOF STEP]
have "\<exists> n. B = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<exists>n. B = nat_to_ce_set n
[PROOF STEP]
by (rule nat_to_ce_set_srj)
[PROOF STATE]
proof (state)
this:
\<exists>n. B = nat_to_ce_set n

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. B = nat_to_ce_set n
[PROOF STEP]
obtain n where "B = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. B = nat_to_ce_set n

goal (1 subgoal):
 1. (\<And>n. B = nat_to_ce_set n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
B = nat_to_ce_set n

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
with S2_1
[PROOF STATE]
proof (chain)
picking this:
B \<in> C
B = nat_to_ce_set n
[PROOF STEP]
have "nat_to_ce_set n \<in> C"
[PROOF STATE]
proof (prove)
using this:
B \<in> C
B = nat_to_ce_set n

goal (1 subgoal):
 1. nat_to_ce_set n \<in> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n \<in> C

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set n \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set n \<in> C

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
by (unfold A_def, auto)
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have S3: "A \<noteq> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
from A1 A5
[PROOF STATE]
proof (chain)
picking this:
C \<subseteq> ce_sets
C \<noteq> ce_sets
[PROOF STEP]
obtain B where S2_1: "B \<notin> C" and S2_2: "B \<in> ce_sets"
[PROOF STATE]
proof (prove)
using this:
C \<subseteq> ce_sets
C \<noteq> ce_sets

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<notin> C; B \<in> ce_sets\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<notin> C
B \<in> ce_sets

goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
from S2_2
[PROOF STATE]
proof (chain)
picking this:
B \<in> ce_sets
[PROOF STEP]
have "\<exists> n. B = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
B \<in> ce_sets

goal (1 subgoal):
 1. \<exists>n. B = nat_to_ce_set n
[PROOF STEP]
by (rule nat_to_ce_set_srj)
[PROOF STATE]
proof (state)
this:
\<exists>n. B = nat_to_ce_set n

goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n. B = nat_to_ce_set n
[PROOF STEP]
obtain n where "B = nat_to_ce_set n"
[PROOF STATE]
proof (prove)
using this:
\<exists>n. B = nat_to_ce_set n

goal (1 subgoal):
 1. (\<And>n. B = nat_to_ce_set n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
B = nat_to_ce_set n

goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
with S2_1
[PROOF STATE]
proof (chain)
picking this:
B \<notin> C
B = nat_to_ce_set n
[PROOF STEP]
have "nat_to_ce_set n \<notin> C"
[PROOF STATE]
proof (prove)
using this:
B \<notin> C
B = nat_to_ce_set n

goal (1 subgoal):
 1. nat_to_ce_set n \<notin> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat_to_ce_set n \<notin> C

goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nat_to_ce_set n \<notin> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nat_to_ce_set n \<notin> C

goal (1 subgoal):
 1. A \<noteq> UNIV
[PROOF STEP]
by (unfold A_def, auto)
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A \<noteq> UNIV

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from S1 S2 S3
[PROOF STATE]
proof (chain)
picking this:
index_set A
A \<noteq> {}
A \<noteq> UNIV
[PROOF STEP]
have "\<not> computable A"
[PROOF STATE]
proof (prove)
using this:
index_set A
A \<noteq> {}
A \<noteq> UNIV

goal (1 subgoal):
 1. \<not> computable A
[PROOF STEP]
by (rule Rice_2)
[PROOF STATE]
proof (state)
this:
\<not> computable A

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> ce_sets; computable {n. nat_to_ce_set n \<in> C}; \<not> (C = {} \<or> C = ce_sets)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with A2
[PROOF STATE]
proof (chain)
picking this:
computable {n. nat_to_ce_set n \<in> C}
\<not> computable A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
computable {n. nat_to_ce_set n \<in> C}
\<not> computable A

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
computable {n. nat_to_ce_set n \<in> C}
\<not> computable {n. nat_to_ce_set n \<in> C}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma supp_name [simp]: fixes i::name shows "supp i = {atom i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp i = {atom i}
[PROOF STEP]
by (rule supp_at_base)


[STATEMENT]
lemma fresh_subst_if [simp]:
  "j \<sharp> subst i x t \<longleftrightarrow> (atom i \<sharp> t \<and> j \<sharp> t) \<or> (j \<sharp> x \<and> (j \<sharp> t \<or> j = atom i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<sharp> subst i x t = (atom i \<sharp> t \<and> j \<sharp> t \<or> j \<sharp> x \<and> (j \<sharp> t \<or> j = atom i))
[PROOF STEP]
by (induct t rule: trm.induct) (auto simp: fresh_at_base)


[STATEMENT]
lemma forget_subst_trm [simp]: "atom a \<sharp> trm \<Longrightarrow> subst a x trm = trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom a \<sharp> trm \<Longrightarrow> subst a x trm = trm
[PROOF STEP]
by (induct trm rule: trm.induct) (simp_all add: fresh_at_base)


[STATEMENT]
lemma subst_trm_id [simp]: "subst a (Var a) trm = trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst a (Var a) trm = trm
[PROOF STEP]
by (induct trm rule: trm.induct) simp_all


[STATEMENT]
lemma subst_trm_commute [simp]:
  "atom j \<sharp> trm \<Longrightarrow> subst j u (subst i t trm) = subst i (subst j u t) trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> trm \<Longrightarrow> subst j u (subst i t trm) = subst i (subst j u t) trm
[PROOF STEP]
by (induct trm rule: trm.induct) (auto simp: fresh_Pair)


[STATEMENT]
lemma subst_trm_commute2 [simp]:
  "atom j \<sharp> t \<Longrightarrow> atom i \<sharp> u \<Longrightarrow> i \<noteq> j \<Longrightarrow> subst j u (subst i t trm) = subst i t (subst j u trm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> t; atom i \<sharp> u; i \<noteq> j\<rbrakk> \<Longrightarrow> subst j u (subst i t trm) = subst i t (subst j u trm)
[PROOF STEP]
by (induct trm rule: trm.induct) auto


[STATEMENT]
lemma repeat_subst_trm [simp]: "subst i u (subst i t trm) = subst i (subst i u t) trm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst i u (subst i t trm) = subst i (subst i u t) trm
[PROOF STEP]
by (induct trm rule: trm.induct) auto


[STATEMENT]
lemma size_subst_fmla [simp]: "size (A(i::=x)) = size A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (A(i::=x)) = size A
[PROOF STEP]
by (nominal_induct A avoiding: i x rule: fmla.strong_induct) auto


[STATEMENT]
lemma forget_subst_fmla [simp]: "atom a \<sharp> A \<Longrightarrow> A(a::=x) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom a \<sharp> A \<Longrightarrow> A(a::=x) = A
[PROOF STEP]
by (nominal_induct A avoiding: a x rule: fmla.strong_induct) (auto simp: fresh_at_base)


[STATEMENT]
lemma subst_fmla_id [simp]: "A(a::=Var a) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A(a::=Var a) = A
[PROOF STEP]
by (nominal_induct A avoiding: a rule: fmla.strong_induct) (auto simp: fresh_at_base)


[STATEMENT]
lemma fresh_subst_fmla_if [simp]:
  "j \<sharp> (A(i::=x)) \<longleftrightarrow> (atom i \<sharp> A \<and> j \<sharp> A) \<or> (j \<sharp> x \<and> (j \<sharp> A \<or> j = atom i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<sharp> A(i::=x) = (atom i \<sharp> A \<and> j \<sharp> A \<or> j \<sharp> x \<and> (j \<sharp> A \<or> j = atom i))
[PROOF STEP]
by (nominal_induct A avoiding: i x rule: fmla.strong_induct) (auto simp: fresh_at_base)


[STATEMENT]
lemma subst_fmla_commute [simp]:
  "atom j \<sharp> A \<Longrightarrow> (A(i::=t))(j::=u) = A(i ::= subst j u t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> A \<Longrightarrow> (A(i::=t))(j::=u) = A(i::=subst j u t)
[PROOF STEP]
by (nominal_induct A avoiding: i j t u rule: fmla.strong_induct) (auto simp: fresh_at_base)


[STATEMENT]
lemma repeat_subst_fmla [simp]: "(A(i::=t))(i::=u) = A(i ::= subst i u t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A(i::=t))(i::=u) = A(i::=subst i u t)
[PROOF STEP]
by (nominal_induct A avoiding: i t u rule: fmla.strong_induct) auto


[STATEMENT]
lemma subst_fmla_exi_with_renaming:
  "atom i' \<sharp> (A, i, j, t) \<Longrightarrow> (exi i A)(j ::= t) = exi i' (((i \<leftrightarrow> i') \<bullet> A)(j ::= t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i' \<sharp> (A, i, j, t) \<Longrightarrow> (exi i A)(j::=t) = exi i' (((i \<leftrightarrow> i') \<bullet> A)(j::=t))
[PROOF STEP]
by (rule subst [of "exi i' ((i \<leftrightarrow> i') \<bullet> A)" "exi i A"])
     (auto simp: Abs1_eq_iff flip_def swap_commute)


[STATEMENT]
lemma flip_subst_trm: "atom y \<sharp> t \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> t = subst x (Var y) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom y \<sharp> t \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> t = subst x (Var y) t
[PROOF STEP]
apply(nominal_induct t avoiding: x y rule: trm.strong_induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x y. atom y \<sharp> zer \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> zer = subst x (Var y) zer
 2. \<And>x xa y. atom y \<sharp> Var x \<Longrightarrow> (xa \<leftrightarrow> y) \<bullet> Var x = subst xa (Var y) (Var x)
 3. \<And>x xa y. \<lbrakk>\<And>b ba. atom ba \<sharp> x \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x = subst b (Var ba) x; atom y \<sharp> suc x\<rbrakk> \<Longrightarrow> (xa \<leftrightarrow> y) \<bullet> suc x = subst xa (Var y) (suc x)
 4. \<And>x1 x2a x y. \<lbrakk>\<And>b ba. atom ba \<sharp> x1 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x1 = subst b (Var ba) x1; \<And>b ba. atom ba \<sharp> x2a \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2a = subst b (Var ba) x2a; atom y \<sharp> pls x1 x2a\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> pls x1 x2a = subst x (Var y) (pls x1 x2a)
 5. \<And>x1 x2a x y. \<lbrakk>\<And>b ba. atom ba \<sharp> x1 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x1 = subst b (Var ba) x1; \<And>b ba. atom ba \<sharp> x2a \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2a = subst b (Var ba) x2a; atom y \<sharp> tms x1 x2a\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> tms x1 x2a = subst x (Var y) (tms x1 x2a)
[PROOF STEP]
by auto


[STATEMENT]
lemma flip_subst_fmla: "atom y \<sharp> \<phi> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> \<phi> = \<phi>(x::=Var y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom y \<sharp> \<phi> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> \<phi> = \<phi>(x::=Var y)
[PROOF STEP]
apply(nominal_induct \<phi> avoiding: x y rule: fmla.strong_induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x y. atom y \<sharp> x1 EQ x2 \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> x1 EQ x2 = (x1 EQ x2)(x::=Var y)
 2. \<And>x1 x2 x y. \<lbrakk>\<And>b ba. atom ba \<sharp> x1 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x1 = x1(b::=Var ba); \<And>b ba. atom ba \<sharp> x2 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2 = x2(b::=Var ba); atom y \<sharp> x1 OR x2\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> x1 OR x2 = (x1 OR x2)(x::=Var y)
 3. \<And>x xa y. \<lbrakk>\<And>b ba. atom ba \<sharp> x \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x = x(b::=Var ba); atom y \<sharp> neg x\<rbrakk> \<Longrightarrow> (xa \<leftrightarrow> y) \<bullet> neg x = (neg x)(xa::=Var y)
 4. \<And>x1 x2 x y. \<lbrakk>atom x1 \<sharp> x; atom x1 \<sharp> y; \<And>b ba. atom ba \<sharp> x2 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2 = x2(b::=Var ba); atom y \<sharp> exi x1 x2\<rbrakk> \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> exi x1 x2 = (exi x1 x2)(x::=Var y)
[PROOF STEP]
apply (auto simp: flip_subst_trm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x c. \<lbrakk>atom x1 \<sharp> x; atom x1 \<sharp> x1; \<And>b ba. atom ba \<sharp> x2 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2 = x2(b::=Var ba); atom c \<sharp> (x1, x, x2); atom c \<sharp> (x1, x1, (x \<leftrightarrow> x1) \<bullet> x2, x2(x::=Var x1))\<rbrakk> \<Longrightarrow> (x1 \<leftrightarrow> c) \<bullet> (x \<leftrightarrow> x1) \<bullet> x2 = (x2(x1::=Var c))(x::=Var x1)
[PROOF STEP]
using fresh_at_base(2)
[PROOF STATE]
proof (prove)
using this:
?a \<sharp> ?b = (?a \<noteq> atom ?b)

goal (1 subgoal):
 1. \<And>x1 x2 x c. \<lbrakk>atom x1 \<sharp> x; atom x1 \<sharp> x1; \<And>b ba. atom ba \<sharp> x2 \<Longrightarrow> (b \<leftrightarrow> ba) \<bullet> x2 = x2(b::=Var ba); atom c \<sharp> (x1, x, x2); atom c \<sharp> (x1, x1, (x \<leftrightarrow> x1) \<bullet> x2, x2(x::=Var x1))\<rbrakk> \<Longrightarrow> (x1 \<leftrightarrow> c) \<bullet> (x \<leftrightarrow> x1) \<bullet> x2 = (x2(x1::=Var c))(x::=Var x1)
[PROOF STEP]
by blast


[STATEMENT]
lemma exi_ren_subst_fresh: "atom y \<sharp> \<phi> \<Longrightarrow> exi x \<phi> = exi y (\<phi>(x::=Var y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom y \<sharp> \<phi> \<Longrightarrow> exi x \<phi> = exi y (\<phi>(x::=Var y))
[PROOF STEP]
using flip_subst_fmla
[PROOF STATE]
proof (prove)
using this:
atom ?y \<sharp> ?\<phi> \<Longrightarrow> (?x \<leftrightarrow> ?y) \<bullet> ?\<phi> = ?\<phi>(?x::=Var ?y)

goal (1 subgoal):
 1. atom y \<sharp> \<phi> \<Longrightarrow> exi x \<phi> = exi y (\<phi>(x::=Var y))
[PROOF STEP]
by auto


[STATEMENT]
lemma eval_trm_rename:
  assumes "atom k' \<sharp> t"
  shows "eval_trm (finfun_update e k x) t =
         eval_trm (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_trm (finfun_update e k x) t = eval_trm (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> t)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom k' \<sharp> t

goal (1 subgoal):
 1. eval_trm (finfun_update e k x) t = eval_trm (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> t)
[PROOF STEP]
by (induct t rule: trm.induct) (auto simp: permute_flip_at)


[STATEMENT]
lemma eval_fmla_rename:
  assumes "atom k' \<sharp> A"
  shows "eval_fmla (finfun_update e k x) A = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla (finfun_update e k x) A = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom k' \<sharp> A

goal (1 subgoal):
 1. eval_fmla (finfun_update e k x) A = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)
[PROOF STEP]
apply (nominal_induct A avoiding: e k k' x rule: fmla.strong_induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 e k k' x. atom k' \<sharp> x1 EQ x2 \<Longrightarrow> eval_fmla (finfun_update e k x) (x1 EQ x2) = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> x1 EQ x2)
 2. \<And>x1 x2 e k k' x. \<lbrakk>\<And>b ba bb bc. atom bb \<sharp> x1 \<Longrightarrow> eval_fmla (finfun_update b ba bc) x1 = eval_fmla (finfun_update b bb bc) ((bb \<leftrightarrow> ba) \<bullet> x1); \<And>b ba bb bc. atom bb \<sharp> x2 \<Longrightarrow> eval_fmla (finfun_update b ba bc) x2 = eval_fmla (finfun_update b bb bc) ((bb \<leftrightarrow> ba) \<bullet> x2); atom k' \<sharp> x1 OR x2\<rbrakk> \<Longrightarrow> eval_fmla (finfun_update e k x) (x1 OR x2) = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> x1 OR x2)
 3. \<And>x e k k' xa. \<lbrakk>\<And>b ba bb bc. atom bb \<sharp> x \<Longrightarrow> eval_fmla (finfun_update b ba bc) x = eval_fmla (finfun_update b bb bc) ((bb \<leftrightarrow> ba) \<bullet> x); atom k' \<sharp> neg x\<rbrakk> \<Longrightarrow> eval_fmla (finfun_update e k xa) (neg x) = eval_fmla (finfun_update e k' xa) ((k' \<leftrightarrow> k) \<bullet> neg x)
 4. \<And>x1 x2 e k k' x. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> k; atom x1 \<sharp> k'; atom x1 \<sharp> x; \<And>b ba bb bc. atom bb \<sharp> x2 \<Longrightarrow> eval_fmla (finfun_update b ba bc) x2 = eval_fmla (finfun_update b bb bc) ((bb \<leftrightarrow> ba) \<bullet> x2); atom k' \<sharp> exi x1 x2\<rbrakk> \<Longrightarrow> eval_fmla (finfun_update e k x) (exi x1 x2) = eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> exi x1 x2)
[PROOF STEP]
apply (simp_all add: eval_trm_rename[symmetric], metis)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 e k k' x. \<lbrakk>atom x1 \<sharp> e; atom x1 \<sharp> k; atom x1 \<sharp> k'; atom x1 \<sharp> x; \<And>b ba bb bc. atom bb \<sharp> x2 \<Longrightarrow> eval_fmla (finfun_update b ba bc) x2 = eval_fmla (finfun_update b bb bc) ((bb \<leftrightarrow> ba) \<bullet> x2); atom k' \<sharp> x2 \<or> k' = x1\<rbrakk> \<Longrightarrow> eval_fmla (finfun_update e k x) (exi x1 x2) = eval_fmla (finfun_update e k' x) (exi x1 ((k' \<leftrightarrow> k) \<bullet> x2))
[PROOF STEP]
apply (simp add: fresh_finfun_update fresh_at_base finfun_update_twist)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma better_ex_eval_fmla[simp]:
  "eval_fmla e (exi k A) \<longleftrightarrow> (\<exists>x. eval_fmla (finfun_update e k x) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
obtain k'::name where k': "atom k' \<sharp> (k, e, A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k'. atom k' \<sharp> (k, e, A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom k' \<sharp> (k, e, A)

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom k' \<sharp> (k, e, A)
[PROOF STEP]
have eq: "exi k' ((k' \<leftrightarrow> k) \<bullet> A) = exi k A"
[PROOF STATE]
proof (prove)
using this:
atom k' \<sharp> (k, e, A)

goal (1 subgoal):
 1. exi k' ((k' \<leftrightarrow> k) \<bullet> A) = exi k A
[PROOF STEP]
by (simp add: Abs1_eq_iff flip_def)
[PROOF STATE]
proof (state)
this:
exi k' ((k' \<leftrightarrow> k) \<bullet> A) = exi k A

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
have "eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))
[PROOF STEP]
using k'
[PROOF STATE]
proof (prove)
using this:
atom k' \<sharp> (k, e, A)

goal (1 subgoal):
 1. eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
have "... = (\<exists>x. eval_fmla (finfun_update e k x) A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
by (metis eval_fmla_rename k' fresh_Pair)
[PROOF STATE]
proof (state)
this:
(\<exists>x. eval_fmla (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k x) A)

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval_fmla e (exi k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fmla (finfun_update e k x) A)

goal (1 subgoal):
 1. eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)
[PROOF STEP]
by (metis eq)
[PROOF STATE]
proof (state)
this:
eval_fmla e (exi k A) = (\<exists>x. eval_fmla (finfun_update e k x) A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma forget_eval_trm [simp]: "atom i \<sharp> t \<Longrightarrow>
    eval_trm (finfun_update e i x) t = eval_trm e t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> t \<Longrightarrow> eval_trm (finfun_update e i x) t = eval_trm e t
[PROOF STEP]
by (induct t rule: trm.induct) (simp_all add: fresh_at_base)


[STATEMENT]
lemma forget_eval_fmla [simp]:
   "atom k \<sharp> A \<Longrightarrow> eval_fmla (finfun_update e k x) A = eval_fmla e A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom k \<sharp> A \<Longrightarrow> eval_fmla (finfun_update e k x) A = eval_fmla e A
[PROOF STEP]
by (nominal_induct A avoiding: k e rule: fmla.strong_induct)
     (simp_all add: fresh_at_base finfun_update_twist)


[STATEMENT]
lemma eval_subst_trm: "eval_trm e (subst i t u) =
   eval_trm (finfun_update e i (eval_trm e t)) u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_trm e (subst i t u) = eval_trm (finfun_update e i (eval_trm e t)) u
[PROOF STEP]
by (induct u rule: trm.induct) (auto)


[STATEMENT]
lemma eval_subst_fmla: "eval_fmla e (fmla(i::= t)) =
   eval_fmla (finfun_update e i (eval_trm e t)) fmla"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e (fmla(i::=t)) = eval_fmla (finfun_update e i (eval_trm e t)) fmla
[PROOF STEP]
by (nominal_induct fmla avoiding: i t e rule: fmla.strong_induct)
     (simp_all add: eval_subst_trm finfun_update_twist fresh_at_base)


[STATEMENT]
lemma cnj_eqvt [eqvt]: "p \<bullet> (A AND B) = (p \<bullet> A) AND (p \<bullet> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> A AND B = (p \<bullet> A) AND (p \<bullet> B)
[PROOF STEP]
by (simp add: cnj_def)


[STATEMENT]
lemma fresh_cnj [simp]: "a \<sharp> A AND B \<longleftrightarrow> (a \<sharp> A \<and> a \<sharp> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> A AND B = (a \<sharp> A \<and> a \<sharp> B)
[PROOF STEP]
by (auto simp: cnj_def)


[STATEMENT]
lemma supp_cnj [simp]: "supp (A AND B) = supp A \<union> supp B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (A AND B) = supp A \<union> supp B
[PROOF STEP]
by (auto simp: cnj_def)


[STATEMENT]
lemma size_cnj [simp]: "size (A AND B) = size A + size B + 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (A AND B) = size A + size B + 4
[PROOF STEP]
by (simp add: cnj_def)


[STATEMENT]
lemma cnj_injective_iff [iff]: "(A AND B) = (A' AND B') \<longleftrightarrow> (A = A' \<and> B = B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A AND B = A' AND B') = (A = A' \<and> B = B')
[PROOF STEP]
by (auto simp: cnj_def)


[STATEMENT]
lemma subst_fmla_cnj [simp]: "(A AND B)(i::=x) = (A(i::=x)) AND (B(i::=x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A AND B)(i::=x) = A(i::=x) AND B(i::=x)
[PROOF STEP]
by (auto simp: cnj_def)


[STATEMENT]
lemma eval_fmla_cnj [simp]: "eval_fmla e (cnj A B) \<longleftrightarrow> (eval_fmla e A \<and> eval_fmla e B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e (A AND B) = (eval_fmla e A \<and> eval_fmla e B)
[PROOF STEP]
by (auto simp: cnj_def)


[STATEMENT]
lemma Iff_eqvt [eqvt]: "p \<bullet> (A IFF B) = (p \<bullet> A) IFF (p \<bullet> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> A IFF B = (p \<bullet> A) IFF (p \<bullet> B)
[PROOF STEP]
by (simp add: Iff_def)


[STATEMENT]
lemma fresh_Iff [simp]: "a \<sharp> A IFF B \<longleftrightarrow> (a \<sharp> A \<and> a \<sharp> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> A IFF B = (a \<sharp> A \<and> a \<sharp> B)
[PROOF STEP]
by (auto simp: cnj_def Iff_def)


[STATEMENT]
lemma size_Iff [simp]: "size (A IFF B) = 2*(size A + size B) + 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (A IFF B) = 2 * (size A + size B) + 8
[PROOF STEP]
by (simp add: Iff_def)


[STATEMENT]
lemma Iff_injective_iff [iff]: "(A IFF B) = (A' IFF B') \<longleftrightarrow> (A = A' \<and> B = B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A IFF B = A' IFF B') = (A = A' \<and> B = B')
[PROOF STEP]
by (auto simp: Iff_def)


[STATEMENT]
lemma subst_fmla_Iff [simp]: "(A IFF B)(i::=x) = (A(i::=x)) IFF (B(i::=x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A IFF B)(i::=x) = A(i::=x) IFF B(i::=x)
[PROOF STEP]
by (auto simp: Iff_def)


[STATEMENT]
lemma eval_fmla_Iff [simp]: "eval_fmla e (Iff A B) \<longleftrightarrow> (eval_fmla e A  \<longleftrightarrow>  eval_fmla e B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e (A IFF B) = (eval_fmla e A = eval_fmla e B)
[PROOF STEP]
by (auto simp: Iff_def)


[STATEMENT]
lemma fls_eqvt [eqvt]: "(p \<bullet> fls) = fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> fls = fls
[PROOF STEP]
by (simp add: fls_def)


[STATEMENT]
lemma fls_fresh [simp]: "a \<sharp> fls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> fls
[PROOF STEP]
by (simp add: fls_def)


[STATEMENT]
lemma boolean_axioms_hold: "A \<in> boolean_axioms \<Longrightarrow> eval_fmla e A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> boolean_axioms \<Longrightarrow> eval_fmla e A
[PROOF STEP]
by (induct rule: boolean_axioms.induct, auto)


[STATEMENT]
lemma special_axioms_hold: "A \<in> special_axioms \<Longrightarrow> eval_fmla e A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> special_axioms \<Longrightarrow> eval_fmla e A
[PROOF STEP]
by (induct rule: special_axioms.induct, auto) (metis eval_subst_fmla)


[STATEMENT]
lemma twist_forget_eval_fmla [simp]:
   "atom j \<sharp> (i, A)
    \<Longrightarrow> eval_fmla (finfun_update (finfun_update (finfun_update e i x) j y) i z) A =
        eval_fmla (finfun_update e i z) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> (i, A) \<Longrightarrow> eval_fmla (finfun_update (finfun_update (finfun_update e i x) j y) i z) A = eval_fmla (finfun_update e i z) A
[PROOF STEP]
by (metis finfun_update_twice finfun_update_twist forget_eval_fmla fresh_Pair)


[STATEMENT]
lemma refl_ax_holds: "eval_fmla e refl_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e refl_ax
[PROOF STEP]
by (auto simp: refl_ax_def)


[STATEMENT]
lemma eq_cong_ax_holds: "eval_fmla e eq_cong_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e eq_cong_ax
[PROOF STEP]
by (auto simp: cnj_def eq_cong_ax_def)


[STATEMENT]
lemma syc_cong_ax_holds: "eval_fmla e syc_cong_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e syc_cong_ax
[PROOF STEP]
by (auto simp: cnj_def syc_cong_ax_def)


[STATEMENT]
lemma pls_cong_ax_holds: "eval_fmla e pls_cong_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e pls_cong_ax
[PROOF STEP]
by (auto simp: cnj_def pls_cong_ax_def)


[STATEMENT]
lemma tms_cong_ax_holds: "eval_fmla e tms_cong_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla e tms_cong_ax
[PROOF STEP]
by (auto simp: cnj_def tms_cong_ax_def)


[STATEMENT]
lemma equality_axioms_hold: "A \<in> equality_axioms \<Longrightarrow> eval_fmla e A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> equality_axioms \<Longrightarrow> eval_fmla e A
[PROOF STEP]
by (auto simp: equality_axioms_def refl_ax_holds eq_cong_ax_holds
       syc_cong_ax_holds pls_cong_ax_holds tms_cong_ax_holds)


[STATEMENT]
lemma contraction: "insert A (insert A H) \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A (insert A H) \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B
[PROOF STEP]
by (metis insert_absorb2)


[STATEMENT]
lemma thin_Un: "H \<turnstile> A \<Longrightarrow> H \<union> H' \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A \<Longrightarrow> H \<union> H' \<turnstile> A
[PROOF STEP]
by (metis Bool MP boolean_axioms.Ident sup_commute)


[STATEMENT]
lemma thin: "H \<turnstile> A \<Longrightarrow> H \<subseteq> H' \<Longrightarrow> H' \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; H \<subseteq> H'\<rbrakk> \<Longrightarrow> H' \<turnstile> A
[PROOF STEP]
by (metis Un_absorb1 thin_Un)


[STATEMENT]
lemma thin0: "{} \<turnstile> A \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> A \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis sup_bot_left thin_Un)


[STATEMENT]
lemma thin1: "H \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B
[PROOF STEP]
by (metis subset_insertI thin)


[STATEMENT]
lemma thin2: "insert A1 H \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A1 H \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma thin4:
  "insert A1 (insert A2 (insert A3 H)) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 H))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A1 (insert A2 (insert A3 H)) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 H))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate2: "insert A2 (insert A1 H) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A2 (insert A1 H) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate3: "insert A3 (insert A1 (insert A2 H)) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 H)) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A3 (insert A1 (insert A2 H)) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 H)) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate4:
  "insert A4 (insert A1 (insert A2 (insert A3 H))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 H))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A4 (insert A1 (insert A2 (insert A3 H))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 H))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate5:
  "insert A5 (insert A1 (insert A2 (insert A3 (insert A4 H)))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H)))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A5 (insert A1 (insert A2 (insert A3 (insert A4 H)))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H)))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate6:
  "insert A6 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A6 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 H))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate7:
  "insert A7 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H)))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H)))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A7 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 H)))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H)))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate8:
  "insert A8 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A8 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 H))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate9:
  "insert A9 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H)))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H)))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A9 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 H)))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H)))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate10:
  "insert A10 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A10 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 H))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate11:
  "insert A11 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H)))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H)))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A11 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 H)))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H)))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate12:
  "insert A12 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H))))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H))))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A12 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 H))))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H))))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate13:
  "insert A13 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H)))))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H)))))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A13 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 H)))))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H)))))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate14:
  "insert A14 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H))))))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H))))))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A14 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 H))))))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H))))))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma rotate15:
  "insert A15 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H)))))))))))))) \<turnstile> B
   \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 (insert A15 H)))))))))))))) \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A15 (insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 H)))))))))))))) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 (insert A5 (insert A6 (insert A7 (insert A8 (insert A9 (insert A10 (insert A11 (insert A12 (insert A13 (insert A14 (insert A15 H)))))))))))))) \<turnstile> B
[PROOF STEP]
by (blast intro: thin)


[STATEMENT]
lemma MP_same: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IMP B; H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis MP Un_absorb)


[STATEMENT]
lemma MP_thin: "HA \<turnstile> A IMP B \<Longrightarrow> HB \<turnstile> A \<Longrightarrow> HA \<union> HB \<subseteq> H \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HA \<turnstile> A IMP B; HB \<turnstile> A; HA \<union> HB \<subseteq> H\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis MP_same le_sup_iff thin)


[STATEMENT]
lemma MP_null: "{} \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{} \<turnstile> A IMP B; H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis MP_same thin0)


[STATEMENT]
lemma dsj_commute: "H \<turnstile> B OR A \<Longrightarrow> H \<turnstile> A OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B OR A \<Longrightarrow> H \<turnstile> A OR B
[PROOF STEP]
using dsjcnj [of B A B] Ident [of B]
[PROOF STATE]
proof (prove)
using this:
B OR A IMP (B IMP B) IMP A OR B \<in> boolean_axioms
B IMP B \<in> boolean_axioms

goal (1 subgoal):
 1. H \<turnstile> B OR A \<Longrightarrow> H \<turnstile> A OR B
[PROOF STEP]
by (metis Bool MP_same)


[STATEMENT]
lemma S: assumes  "H \<turnstile> A IMP (B IMP C)" "H' \<turnstile> A IMP B" shows "H \<union> H' \<turnstile> A IMP C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<union> H' \<turnstile> A IMP C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H \<union> H' \<turnstile> A IMP C
[PROOF STEP]
have "H' \<union> H \<turnstile> (neg A) OR (C OR (neg A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H' \<union> H \<turnstile> A IMP C OR neg A
[PROOF STEP]
by (metis Bool MP MP_same boolean_axioms.dsjcnj dsj_commute dsjAssoc assms)
[PROOF STATE]
proof (state)
this:
H' \<union> H \<turnstile> A IMP C OR neg A

goal (1 subgoal):
 1. H \<union> H' \<turnstile> A IMP C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H' \<union> H \<turnstile> A IMP C OR neg A

goal (1 subgoal):
 1. H \<union> H' \<turnstile> A IMP C
[PROOF STEP]
by (metis Bool dsj_commute Un_commute MP_same dsjAssoc dsjCont dsjI1)
[PROOF STATE]
proof (state)
this:
H \<union> H' \<turnstile> A IMP C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Assume: "insert A H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> A
[PROOF STEP]
by (metis Hyp insertI1)


[STATEMENT]
lemma imp_triv_I: "H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B
[PROOF STEP]
by (metis Bool dsj_commute MP_same boolean_axioms.dsjI1)


[STATEMENT]
lemma dsjAssoc1: "H \<turnstile> A OR (B OR C) \<Longrightarrow> H \<turnstile> (A OR B) OR C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A OR B OR C \<Longrightarrow> H \<turnstile> (A OR B) OR C
[PROOF STEP]
by (metis Bool MP_same boolean_axioms.dsjAssoc)


[STATEMENT]
lemma dsjAssoc2: "H \<turnstile> (A OR B) OR C \<Longrightarrow> H \<turnstile> A OR (B OR C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> (A OR B) OR C \<Longrightarrow> H \<turnstile> A OR B OR C
[PROOF STEP]
by (metis dsjAssoc1 dsj_commute)


[STATEMENT]
lemma dsj_commute_imp: "H \<turnstile> (B OR A) IMP (A OR B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B OR A IMP A OR B
[PROOF STEP]
using dsjcnj [of B A B] Ident [of B]
[PROOF STATE]
proof (prove)
using this:
B OR A IMP (B IMP B) IMP A OR B \<in> boolean_axioms
B IMP B \<in> boolean_axioms

goal (1 subgoal):
 1. H \<turnstile> B OR A IMP A OR B
[PROOF STEP]
by (metis Bool dsjAssoc2 dsj_commute MP_same)


[STATEMENT]
lemma dsj_Semicong_1: "H \<turnstile> A OR C \<Longrightarrow> H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> B OR C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A OR C; H \<turnstile> A IMP B\<rbrakk> \<Longrightarrow> H \<turnstile> B OR C
[PROOF STEP]
using dsjcnj [of A C B]
[PROOF STATE]
proof (prove)
using this:
A OR C IMP (A IMP B) IMP C OR B \<in> boolean_axioms

goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A OR C; H \<turnstile> A IMP B\<rbrakk> \<Longrightarrow> H \<turnstile> B OR C
[PROOF STEP]
by (metis Bool dsj_commute MP_same)


[STATEMENT]
lemma imp_imp_commute: "H \<turnstile> B IMP (A IMP C) \<Longrightarrow> H \<turnstile> A IMP (B IMP C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B IMP A IMP C \<Longrightarrow> H \<turnstile> A IMP B IMP C
[PROOF STEP]
by (metis dsjAssoc1 dsjAssoc2 dsj_Semicong_1 dsj_commute_imp)


[STATEMENT]
lemma deduction_Diff: assumes "H \<turnstile> B" shows "H - {C} \<turnstile> C IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> B

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

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

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP A
[PROOF STEP]
by (metis Bool imp_triv_I boolean_axioms.Ident nprv.Hyp member_remove remove_def)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP A

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

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

goal (1 subgoal):
 1. H_ - {C} \<turnstile> C IMP H
[PROOF STEP]
by (metis imp_triv_I nprv.Q)
[PROOF STATE]
proof (state)
this:
H_ - {C} \<turnstile> C IMP H

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

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

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP A
[PROOF STEP]
by (metis imp_triv_I nprv.Bool)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP A

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

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

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP A
[PROOF STEP]
by (metis imp_triv_I nprv.eql)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP A

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

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

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP A
[PROOF STEP]
by (metis imp_triv_I nprv.Spec)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP A

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

goal (2 subgoals):
 1. \<And>H A B H'. \<lbrakk>H \<turnstile> A IMP B; H - {C} \<turnstile> C IMP A IMP B; H' \<turnstile> A; H' - {C} \<turnstile> C IMP A\<rbrakk> \<Longrightarrow> H \<union> H' - {C} \<turnstile> C IMP B
 2. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H - {C} \<turnstile> C IMP A IMP B; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
hence "(H-{C}) \<union> (H'-{C}) \<turnstile> imp C B"
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
H' \<turnstile> A
H' - {C} \<turnstile> C IMP A

goal (1 subgoal):
 1. H - {C} \<union> (H' - {C}) \<turnstile> C IMP B
[PROOF STEP]
by (simp add: S)
[PROOF STATE]
proof (state)
this:
H - {C} \<union> (H' - {C}) \<turnstile> C IMP B

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

goal (1 subgoal):
 1. H \<union> H' - {C} \<turnstile> C IMP B
[PROOF STEP]
by (metis Un_Diff)
[PROOF STATE]
proof (state)
this:
H \<union> H' - {C} \<turnstile> C IMP B

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

goal (1 subgoal):
 1. \<And>H A B i. \<lbrakk>H \<turnstile> A IMP B; H - {C} \<turnstile> C IMP A IMP B; atom i \<sharp> B; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
proof (cases "C \<in> H")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C \<in> H

goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
hence "atom i \<sharp> C"
[PROOF STATE]
proof (prove)
using this:
C \<in> H

goal (1 subgoal):
 1. atom i \<sharp> C
[PROOF STEP]
using exiists
[PROOF STATE]
proof (prove)
using this:
C \<in> H
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C

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

goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom i \<sharp> C

goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
have "H - {C} \<turnstile> A IMP C IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H - {C} \<turnstile> A IMP C IMP B
[PROOF STEP]
using exiists
[PROOF STATE]
proof (prove)
using this:
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C

goal (1 subgoal):
 1. H - {C} \<turnstile> A IMP C IMP B
[PROOF STEP]
by (metis imp_imp_commute)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> A IMP C IMP B

goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom i \<sharp> C
H - {C} \<turnstile> A IMP C IMP B
[PROOF STEP]
have "H - {C} \<turnstile> (exi i A) IMP C IMP B"
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> C
H - {C} \<turnstile> A IMP C IMP B

goal (1 subgoal):
 1. H - {C} \<turnstile> exi i A IMP C IMP B
[PROOF STEP]
using exiists
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> C
H - {C} \<turnstile> A IMP C IMP B
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C

goal (1 subgoal):
 1. H - {C} \<turnstile> exi i A IMP C IMP B
[PROOF STEP]
using nprv.eql
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> C
H - {C} \<turnstile> A IMP C IMP B
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C
?A \<in> equality_axioms \<Longrightarrow> ?H \<turnstile> ?A

goal (1 subgoal):
 1. H - {C} \<turnstile> exi i A IMP C IMP B
[PROOF STEP]
by (simp add: nprv.exiists)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> exi i A IMP C IMP B

goal (2 subgoals):
 1. C \<in> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
 2. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H - {C} \<turnstile> exi i A IMP C IMP B

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
by (metis imp_imp_commute)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP exi i A IMP B

goal (1 subgoal):
 1. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<notin> H

goal (1 subgoal):
 1. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
hence "H - {C} = H"
[PROOF STATE]
proof (prove)
using this:
C \<notin> H

goal (1 subgoal):
 1. H - {C} = H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H - {C} = H

goal (1 subgoal):
 1. C \<notin> H \<Longrightarrow> H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H - {C} = H

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
using exiists
[PROOF STATE]
proof (prove)
using this:
H - {C} = H
H \<turnstile> A IMP B
H - {C} \<turnstile> C IMP A IMP B
atom i \<sharp> B
\<forall>C\<in>H. atom i \<sharp> C

goal (1 subgoal):
 1. H - {C} \<turnstile> C IMP exi i A IMP B
[PROOF STEP]
by (metis imp_triv_I nprv.exiists)
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP exi i A IMP B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
H - {C} \<turnstile> C IMP exi i A IMP B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem imp_I [intro!]: "insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B
[PROOF STEP]
by (metis Diff_insert_absorb imp_triv_I deduction_Diff insert_absorb)


[STATEMENT]
lemma anti_deduction: "H \<turnstile> A IMP B \<Longrightarrow> insert A H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IMP B \<Longrightarrow> insert A H \<turnstile> B
[PROOF STEP]
by (metis Assume MP_same thin1)


[STATEMENT]
lemma cut:  "H \<turnstile> A \<Longrightarrow> insert A H' \<turnstile> B \<Longrightarrow> H \<union> H' \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; insert A H' \<turnstile> B\<rbrakk> \<Longrightarrow> H \<union> H' \<turnstile> B
[PROOF STEP]
by (metis MP Un_commute imp_I)


[STATEMENT]
lemma cut_same: "H \<turnstile> A \<Longrightarrow> insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; insert A H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis Un_absorb cut)


[STATEMENT]
lemma cut_thin: "HA \<turnstile> A \<Longrightarrow> insert A HB \<turnstile> B \<Longrightarrow> HA \<union> HB \<subseteq> H \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HA \<turnstile> A; insert A HB \<turnstile> B; HA \<union> HB \<subseteq> H\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis thin cut)


[STATEMENT]
lemma cut0: "{} \<turnstile> A \<Longrightarrow> insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{} \<turnstile> A; insert A H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis cut_same thin0)


[STATEMENT]
lemma cut1: "{A} \<turnstile> B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{A} \<turnstile> B; H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis cut sup_bot_right)


[STATEMENT]
lemma rcut1: "{A} \<turnstile> B \<Longrightarrow> insert B H \<turnstile> C \<Longrightarrow> insert A H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{A} \<turnstile> B; insert B H \<turnstile> C\<rbrakk> \<Longrightarrow> insert A H \<turnstile> C
[PROOF STEP]
by (metis Assume cut1 cut_same rotate2 thin1)


[STATEMENT]
lemma cut2: "\<lbrakk>{A,B} \<turnstile> C; H \<turnstile> A; H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{A, B} \<turnstile> C; H \<turnstile> A; H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> C
[PROOF STEP]
by (metis Un_empty_right Un_insert_right cut cut_same)


[STATEMENT]
lemma rcut2: "{A,B} \<turnstile> C \<Longrightarrow> insert C H \<turnstile> D \<Longrightarrow> H \<turnstile> B \<Longrightarrow> insert A H \<turnstile> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{A, B} \<turnstile> C; insert C H \<turnstile> D; H \<turnstile> B\<rbrakk> \<Longrightarrow> insert A H \<turnstile> D
[PROOF STEP]
by (metis Assume cut2 cut_same insert_commute thin1)


[STATEMENT]
lemma cut4: "\<lbrakk>{A,B,C,D} \<turnstile> E; H \<turnstile> A; H \<turnstile> B; H \<turnstile> C; H \<turnstile> D\<rbrakk> \<Longrightarrow> H \<turnstile> E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{A, B, C, D} \<turnstile> E; H \<turnstile> A; H \<turnstile> B; H \<turnstile> C; H \<turnstile> D\<rbrakk> \<Longrightarrow> H \<turnstile> E
[PROOF STEP]
by (metis MP_same cut3 [of B C D] imp_I)


[STATEMENT]
lemma dsj_I1: "H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B
[PROOF STEP]
by (metis Bool MP_same boolean_axioms.dsjI1)


[STATEMENT]
lemma dsj_I2: "H \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B
[PROOF STEP]
by (metis dsj_commute dsj_I1)


[STATEMENT]
lemma Peirce: "H \<turnstile> (neg A) IMP A \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> neg A IMP A \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
using dsjcnj [of "neg A" A A]  dsjCont [of A]
[PROOF STATE]
proof (prove)
using this:
(A IMP A) IMP (neg A IMP A) IMP A OR A \<in> boolean_axioms
A OR A IMP A \<in> boolean_axioms

goal (1 subgoal):
 1. H \<turnstile> neg A IMP A \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis Bool MP_same boolean_axioms.Ident)


[STATEMENT]
lemma Contra: "insert (neg A) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg A) H \<turnstile> A \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis Peirce imp_I)


[STATEMENT]
lemma imp_neg_I: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A IMP (neg B) \<Longrightarrow> H \<turnstile> neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IMP B; H \<turnstile> A IMP neg B\<rbrakk> \<Longrightarrow> H \<turnstile> neg A
[PROOF STEP]
by (metis dsjcnj [of B "neg A" "neg A"] dsjCont Bool dsj_commute MP_same)


[STATEMENT]
lemma negneg_I: "H \<turnstile> A \<Longrightarrow> H \<turnstile> neg (neg A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A \<Longrightarrow> H \<turnstile> neg (neg A)
[PROOF STEP]
using dsjcnj [of "neg (neg A)" "neg A" "neg (neg A)"]
[PROOF STATE]
proof (prove)
using this:
(neg A IMP neg A) IMP (neg (neg A) IMP neg (neg A)) IMP A IMP neg (neg A) \<in> boolean_axioms

goal (1 subgoal):
 1. H \<turnstile> A \<Longrightarrow> H \<turnstile> neg (neg A)
[PROOF STEP]
by (metis Bool Ident MP_same)


[STATEMENT]
lemma negneg_D: "H \<turnstile> neg (neg A) \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> neg (neg A) \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis dsj_I1 Peirce)


[STATEMENT]
lemma neg_D: "H \<turnstile> neg A \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> neg A; H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis imp_neg_I imp_triv_I negneg_D)


[STATEMENT]
lemma dsj_neg_1: "H \<turnstile> A OR B \<Longrightarrow> H \<turnstile> neg B \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A OR B; H \<turnstile> neg B\<rbrakk> \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis dsj_I1 dsj_Semicong_1 dsj_commute Peirce)


[STATEMENT]
lemma dsj_neg_2: "H \<turnstile> A OR B \<Longrightarrow> H \<turnstile> neg A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A OR B; H \<turnstile> neg A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis dsj_neg_1 dsj_commute)


[STATEMENT]
lemma neg_dsj_I: "H \<turnstile> neg A \<Longrightarrow> H \<turnstile> neg B \<Longrightarrow> H \<turnstile> neg (A OR B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> neg A; H \<turnstile> neg B\<rbrakk> \<Longrightarrow> H \<turnstile> neg (A OR B)
[PROOF STEP]
by (metis Bool dsj_neg_1 MP_same boolean_axioms.Ident dsjAssoc)


[STATEMENT]
lemma cnj_I [intro!]: "H \<turnstile> A \<Longrightarrow> H \<turnstile> B \<Longrightarrow> H \<turnstile> A AND B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> A AND B
[PROOF STEP]
by (metis cnj_def negneg_I neg_dsj_I)


[STATEMENT]
lemma cnj_E1: "H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> A
[PROOF STEP]
by (metis cnj_def Bool dsj_neg_1 negneg_D boolean_axioms.dsjI1)


[STATEMENT]
lemma cnj_E2: "H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis cnj_def Bool dsj_I2 dsj_neg_2 MP_same dsjAssoc Ident)


[STATEMENT]
lemma cnj_commute: "H \<turnstile> B AND A \<Longrightarrow> H \<turnstile> A AND B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B AND A \<Longrightarrow> H \<turnstile> A AND B
[PROOF STEP]
by (metis cnj_E1 cnj_E2 cnj_I)


[STATEMENT]
lemma cnj_E: assumes "insert A (insert B H) \<turnstile> C" shows "insert (A AND B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A AND B) H \<turnstile> C
[PROOF STEP]
apply (rule cut_same [where A=A], metis cnj_E1 Hyp insertI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A (insert (A AND B) H) \<turnstile> C
[PROOF STEP]
by (metis (full_types) AssumeH(2) cnj_E2 assms cut_same [where A=B] insert_commute thin2)


[STATEMENT]
lemma neg_mono: "insert A H \<turnstile> B \<Longrightarrow> insert (neg B) H \<turnstile> neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> B \<Longrightarrow> insert (neg B) H \<turnstile> neg A
[PROOF STEP]
by (rule neg_I0) (metis Hyp neg_D insert_commute insertI1 thin1)


[STATEMENT]
lemma cnj_mono: "insert A H \<turnstile> B \<Longrightarrow> insert C H \<turnstile> D \<Longrightarrow> insert (A AND C) H \<turnstile> B AND D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert A H \<turnstile> B; insert C H \<turnstile> D\<rbrakk> \<Longrightarrow> insert (A AND C) H \<turnstile> B AND D
[PROOF STEP]
by (metis cnj_E1 cnj_E2 cnj_I Hyp Un_absorb2 cut insertI1 subset_insertI)


[STATEMENT]
lemma dsj_mono:
  assumes "insert A H \<turnstile> B" "insert C H \<turnstile> D" shows "insert (A OR C) H \<turnstile> B OR D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
fix A B C H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
have "insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B
[PROOF STEP]
by (metis Bool Hyp MP_same boolean_axioms.dsjcnj insertI1)
[PROOF STATE]
proof (state)
this:
insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
hence "insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B"
[PROOF STATE]
proof (prove)
using this:
insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B

goal (1 subgoal):
 1. insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B
[PROOF STEP]
by (metis MP_same Un_absorb Un_insert_right imp_I thin_Un)
[PROOF STATE]
proof (state)
this:
insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
insert ?Aa2 ?Ha2 \<turnstile> ?Ba2 \<Longrightarrow> insert (?Aa2 OR ?Ca2) ?Ha2 \<turnstile> ?Ca2 OR ?Ba2

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
insert ?Aa2 ?Ha2 \<turnstile> ?Ba2 \<Longrightarrow> insert (?Aa2 OR ?Ca2) ?Ha2 \<turnstile> ?Ca2 OR ?Ba2

goal (1 subgoal):
 1. insert (A OR C) H \<turnstile> B OR D
[PROOF STEP]
by (metis cut_same assms thin2)
[PROOF STATE]
proof (state)
this:
insert (A OR C) H \<turnstile> B OR D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dsj_E:
  assumes A: "insert A H \<turnstile> C" and B: "insert B H \<turnstile> C" shows "insert (A OR B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A OR B) H \<turnstile> C
[PROOF STEP]
by (metis A B dsj_mono negneg_I Peirce)


[STATEMENT]
lemma Contra': "insert A H \<turnstile> neg A \<Longrightarrow> H \<turnstile> neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> neg A \<Longrightarrow> H \<turnstile> neg A
[PROOF STEP]
by (metis Contra neg_mono)


[STATEMENT]
lemma negneg_E [intro!]: "insert A H \<turnstile> B \<Longrightarrow> insert (neg (neg A)) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert A H \<turnstile> B \<Longrightarrow> insert (neg (neg A)) H \<turnstile> B
[PROOF STEP]
by (metis negneg_D neg_mono)


[STATEMENT]
lemma imp_E:
  assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (A IMP B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A IMP B) H \<turnstile> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (A IMP B) H \<turnstile> C
[PROOF STEP]
have "insert (A IMP B) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A IMP B) H \<turnstile> B
[PROOF STEP]
by (metis Hyp A thin1 MP_same insertI1)
[PROOF STATE]
proof (state)
this:
insert (A IMP B) H \<turnstile> B

goal (1 subgoal):
 1. insert (A IMP B) H \<turnstile> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
insert (A IMP B) H \<turnstile> B

goal (1 subgoal):
 1. insert (A IMP B) H \<turnstile> C
[PROOF STEP]
by (metis cut [where B=C] Un_insert_right sup_commute sup_idem B)
[PROOF STATE]
proof (state)
this:
insert (A IMP B) H \<turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_cut:
  assumes "insert C H \<turnstile> A IMP B" "{A} \<turnstile> C"
    shows "H \<turnstile> A IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IMP B
[PROOF STEP]
by (metis Contra dsj_I1 neg_mono assms rcut1)


[STATEMENT]
lemma Iff_I [intro!]: "insert A H \<turnstile> B \<Longrightarrow> insert B H \<turnstile> A \<Longrightarrow> H \<turnstile> A IFF B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert A H \<turnstile> B; insert B H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> A IFF B
[PROOF STEP]
by (metis Iff_def cnj_I imp_I)


[STATEMENT]
lemma Iff_MP_same: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF B; H \<turnstile> A\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis Iff_def cnj_E1 MP_same)


[STATEMENT]
lemma Iff_refl [intro!]: "H \<turnstile> A IFF A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IFF A
[PROOF STEP]
by (metis Hyp Iff_I insertI1)


[STATEMENT]
lemma Iff_sym: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B IFF A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B IFF A
[PROOF STEP]
by (metis Iff_def cnj_commute)


[STATEMENT]
lemma Iff_trans: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B IFF C \<Longrightarrow> H \<turnstile> A IFF C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF B; H \<turnstile> B IFF C\<rbrakk> \<Longrightarrow> H \<turnstile> A IFF C
[PROOF STEP]
unfolding Iff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> (A IMP B) AND (B IMP A); H \<turnstile> (B IMP C) AND (C IMP B)\<rbrakk> \<Longrightarrow> H \<turnstile> (A IMP C) AND (C IMP A)
[PROOF STEP]
by (metis cnj_E1 cnj_E2 cnj_I dsj_Semicong_1 dsj_commute)


[STATEMENT]
lemma Iff_E:
  "insert A (insert B H) \<turnstile> C \<Longrightarrow> insert (neg A) (insert (neg B) H) \<turnstile> C \<Longrightarrow> insert (A IFF B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert A (insert B H) \<turnstile> C; insert (neg A) (insert (neg B) H) \<turnstile> C\<rbrakk> \<Longrightarrow> insert (A IFF B) H \<turnstile> C
[PROOF STEP]
by (simp add: Assume Iff_def anti_deduction cnj_E dsj_EH(2) dsj_I1 insert_commute)


[STATEMENT]
lemma Iff_E1:
  assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (A IFF B) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A IFF B) H \<turnstile> C
[PROOF STEP]
by (metis Iff_def A B cnj_E imp_E insert_commute thin1)


[STATEMENT]
lemma Iff_E2:
  assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (B IFF A) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (B IFF A) H \<turnstile> C
[PROOF STEP]
by (metis Iff_def A B Bool cnj_E2 cnj_mono imp_E boolean_axioms.Ident)


[STATEMENT]
lemma Iff_MP_left: "H \<turnstile> A IFF B \<Longrightarrow> insert A H \<turnstile> C \<Longrightarrow> insert B H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF B; insert A H \<turnstile> C\<rbrakk> \<Longrightarrow> insert B H \<turnstile> C
[PROOF STEP]
by (metis Hyp Iff_E2 cut_same insertI1 insert_commute thin1)


[STATEMENT]
lemma Iff_MP_left': "H \<turnstile> A IFF B \<Longrightarrow> insert B H \<turnstile> C \<Longrightarrow> insert A H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF B; insert B H \<turnstile> C\<rbrakk> \<Longrightarrow> insert A H \<turnstile> C
[PROOF STEP]
by (metis Iff_MP_left Iff_sym)


[STATEMENT]
lemma Swap: "insert (neg B) H \<turnstile> A \<Longrightarrow> insert (neg A) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg B) H \<turnstile> A \<Longrightarrow> insert (neg A) H \<turnstile> B
[PROOF STEP]
by (metis negneg_D neg_mono)


[STATEMENT]
lemma Cases: "insert A H \<turnstile> B \<Longrightarrow> insert (neg A) H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert A H \<turnstile> B; insert (neg A) H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis Contra neg_D neg_mono)


[STATEMENT]
lemma neg_cnj_E: "H \<turnstile> B \<Longrightarrow> insert (neg A) H \<turnstile> C \<Longrightarrow> insert (neg (A AND B)) H \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> B; insert (neg A) H \<turnstile> C\<rbrakk> \<Longrightarrow> insert (neg (A AND B)) H \<turnstile> C
[PROOF STEP]
by (metis cnj_I Swap thin1)


[STATEMENT]
lemma dsj_CI: "insert (neg B) H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg B) H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B
[PROOF STEP]
by (metis Contra dsj_I1 dsj_I2 Swap)


[STATEMENT]
lemma dsj_3I: "insert (neg A) (insert (neg C) H) \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B OR C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (neg A) (insert (neg C) H) \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B OR C
[PROOF STEP]
by (metis dsj_CI dsj_commute insert_commute)


[STATEMENT]
lemma Contrapos1: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> neg B IMP neg A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> neg B IMP neg A
[PROOF STEP]
by (metis Bool MP_same boolean_axioms.dsjcnj boolean_axioms.Ident)


[STATEMENT]
lemma Contrapos2: "H \<turnstile> (neg B) IMP (neg A) \<Longrightarrow> H \<turnstile> A IMP B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> neg B IMP neg A \<Longrightarrow> H \<turnstile> A IMP B
[PROOF STEP]
by (metis Bool MP_same boolean_axioms.dsjcnj boolean_axioms.Ident)


[STATEMENT]
lemma ContraAssumeN [intro]: "B \<in> H \<Longrightarrow> insert (neg B) H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> H \<Longrightarrow> insert (neg B) H \<turnstile> A
[PROOF STEP]
by (metis Hyp Swap thin1)


[STATEMENT]
lemma ContraAssume: "neg B \<in> H \<Longrightarrow> insert B H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg B \<in> H \<Longrightarrow> insert B H \<turnstile> A
[PROOF STEP]
by (metis dsj_I1 Hyp anti_deduction)


[STATEMENT]
lemma ContraProve: "H \<turnstile> B \<Longrightarrow> insert (neg B) H \<turnstile> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> B \<Longrightarrow> insert (neg B) H \<turnstile> A
[PROOF STEP]
by (metis Swap thin1)


[STATEMENT]
lemma dsj_IE1: "insert B H \<turnstile> C \<Longrightarrow> insert (A OR B) H \<turnstile> A OR C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert B H \<turnstile> C \<Longrightarrow> insert (A OR B) H \<turnstile> A OR C
[PROOF STEP]
by (metis Assume dsj_mono)


[STATEMENT]
lemma exi_I: "H \<turnstile> A(i::=x) \<Longrightarrow> H \<turnstile> exi i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A(i::=x) \<Longrightarrow> H \<turnstile> exi i A
[PROOF STEP]
by (metis MP_same Spec special_axioms.intros)


[STATEMENT]
lemma exi_E:
  assumes "insert A H \<turnstile> B" "atom i \<sharp> B" "\<forall>C \<in> H. atom i \<sharp> C"
  shows "insert (exi i A) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (exi i A) H \<turnstile> B
[PROOF STEP]
by (metis exiists imp_I anti_deduction assms)


[STATEMENT]
lemma exi_E_with_renaming:
  assumes "insert ((i \<leftrightarrow> i') \<bullet> A) H \<turnstile> B" "atom i' \<sharp> (A,i,B)" "\<forall>C \<in> H. atom i' \<sharp> C"
  shows "insert (exi i A) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (exi i A) H \<turnstile> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert (exi i A) H \<turnstile> B
[PROOF STEP]
have "exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert ((i \<leftrightarrow> i') \<bullet> A) H \<turnstile> B
atom i' \<sharp> (A, i, B)
\<forall>C\<in>H. atom i' \<sharp> C

goal (1 subgoal):
 1. exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)
[PROOF STEP]
using flip_subst_fmla
[PROOF STATE]
proof (prove)
using this:
insert ((i \<leftrightarrow> i') \<bullet> A) H \<turnstile> B
atom i' \<sharp> (A, i, B)
\<forall>C\<in>H. atom i' \<sharp> C
atom ?y \<sharp> ?\<phi> \<Longrightarrow> (?x \<leftrightarrow> ?y) \<bullet> ?\<phi> = ?\<phi>(?x::=Var ?y)

goal (1 subgoal):
 1. exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)

goal (1 subgoal):
 1. insert (exi i A) H \<turnstile> B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exi i A = exi i' ((i \<leftrightarrow> i') \<bullet> A)

goal (1 subgoal):
 1. insert (exi i A) H \<turnstile> B
[PROOF STEP]
by (metis exi_E assms fresh_Pair)
[PROOF STATE]
proof (state)
this:
insert (exi i A) H \<turnstile> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exi_mono: "insert A H \<turnstile> B \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> insert (exi i A) H \<turnstile> (exi i B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>insert A H \<turnstile> B; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (exi i A) H \<turnstile> exi i B
[PROOF STEP]
by (auto simp add: intro: exi_I [where x="Var i"])


[STATEMENT]
lemma all_I [intro!]: "H \<turnstile> A \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> all i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A; \<forall>C\<in>H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> H \<turnstile> all i A
[PROOF STEP]
by (auto intro: ContraProve neg_I0)


[STATEMENT]
lemma all_D: "H \<turnstile> all i A \<Longrightarrow> H \<turnstile> A(i::=x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> all i A \<Longrightarrow> H \<turnstile> A(i::=x)
[PROOF STEP]
by (metis Assume exi_I negneg_D neg_mono neg cut_same)


[STATEMENT]
lemma all_E: "insert (A(i::=x)) H \<turnstile> B \<Longrightarrow> insert (all i A) H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (A(i::=x)) H \<turnstile> B \<Longrightarrow> insert (all i A) H \<turnstile> B
[PROOF STEP]
by (metis exi_I negneg_D neg_mono neg)


[STATEMENT]
lemma all_E': "H \<turnstile> all i A \<Longrightarrow> insert (A(i::=x)) H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> all i A; insert (A(i::=x)) H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> B
[PROOF STEP]
by (metis all_D cut_same)


[STATEMENT]
lemma neg_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> neg A IFF neg A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> neg A IFF neg A'
[PROOF STEP]
by (metis Iff_def cnj_E1 cnj_E2 cnj_I Contrapos1)


[STATEMENT]
lemma dsj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'
[PROOF STEP]
by (metis cnj_E1 cnj_E2 dsj_mono Iff_I Iff_def anti_deduction)


[STATEMENT]
lemma cnj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A AND B IFF A' AND B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> A AND B IFF A' AND B'
[PROOF STEP]
by (metis cnj_def dsj_cong neg_cong)


[STATEMENT]
lemma imp_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> (A IMP B) IFF (A' IMP B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> (A IMP B) IFF A' IMP B'
[PROOF STEP]
by (metis dsj_cong neg_cong)


[STATEMENT]
lemma Iff_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> (A IFF B) IFF (A' IFF B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>H \<turnstile> A IFF A'; H \<turnstile> B IFF B'\<rbrakk> \<Longrightarrow> H \<turnstile> (A IFF B) IFF A' IFF B'
[PROOF STEP]
by (metis Iff_def cnj_cong imp_cong)