diff --git a/thys/Incompleteness/Coding.thy b/thys/Incompleteness/Coding.thy
--- a/thys/Incompleteness/Coding.thy
+++ b/thys/Incompleteness/Coding.thy
@@ -1,860 +1,859 @@
 chapter\<open>De Bruijn Syntax, Quotations, Codes, V-Codes\<close>
 
 theory Coding
 imports SyntaxN
 begin
 
 declare fresh_Nil [iff]
 
 section \<open>de Bruijn Indices (locally-nameless version)\<close>
 
 nominal_datatype dbtm = DBZero | DBVar name | DBInd nat | DBEats dbtm dbtm
 
 nominal_datatype dbfm =
     DBMem dbtm dbtm
   | DBEq dbtm dbtm
   | DBDisj dbfm dbfm
   | DBNeg dbfm
   | DBEx dbfm
 
 declare dbtm.supp [simp]
 declare dbfm.supp [simp]
 
 fun lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> dbtm"
   where
     "lookup [] n x = DBVar x"
   | "lookup (y # ys) n x = (if x = y then DBInd n else (lookup ys (Suc n) x))"
 
 lemma fresh_imp_notin_env: "atom name \<sharp> e \<Longrightarrow> name \<notin> set e"
   by (metis List.finite_set fresh_finite_set_at_base fresh_set)
 
 lemma lookup_notin: "x \<notin> set e \<Longrightarrow> lookup e n x = DBVar x"
   by (induct e arbitrary: n) auto
 
 lemma lookup_in:
   "x \<in> set e \<Longrightarrow> \<exists>k. lookup e n x = DBInd k \<and> n \<le> k \<and> k < n + length e"
-apply (induct e arbitrary: n) 
-apply (auto intro: Suc_leD)
-apply (metis Suc_leD add_Suc_right add_Suc_shift)
-done
+  by (induction e arbitrary: n) force+
 
 lemma lookup_fresh: "x \<sharp> lookup e n y \<longleftrightarrow> y \<in> set e \<or> x \<noteq> atom y"
   by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base)
 
 lemma lookup_eqvt[eqvt]: "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
   by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
 lemma lookup_inject [iff]: "(lookup e n x = lookup e n y) \<longleftrightarrow> x = y"
-apply (induct e n x arbitrary: y rule: lookup.induct, force, simp)
-by (metis Suc_n_not_le_n dbtm.distinct(7) dbtm.eq_iff(3) lookup_in lookup_notin)
+proof (induction e n x arbitrary: y rule: lookup.induct)
+  case (2 y ys n x z)
+  then show ?case
+    by (metis dbtm.distinct(7) dbtm.eq_iff(3) lookup.simps(2) lookup_in lookup_notin not_less_eq_eq)
+qed auto
 
 nominal_function trans_tm :: "name list \<Rightarrow> tm \<Rightarrow> dbtm"
   where
    "trans_tm e Zero = DBZero"
  | "trans_tm e (Var k) = lookup e 0 k"
  | "trans_tm e (Eats t u) = DBEats (trans_tm e t) (trans_tm e u)"
 by (auto simp: eqvt_def trans_tm_graph_aux_def) (metis tm.strong_exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_trans_tm_iff [simp]: "i \<sharp> trans_tm e t \<longleftrightarrow> i \<sharp> t \<or> i \<in> atom ` set e"
   by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base)
 
 lemma trans_tm_forget: "atom i \<sharp> t \<Longrightarrow> trans_tm [i] t = trans_tm [] t"
   by (induct t rule: tm.induct, auto simp: fresh_Pair)
 
 nominal_function (invariant "\<lambda>(xs, _) y. atom ` set xs \<sharp>* y")
   trans_fm :: "name list \<Rightarrow> fm \<Rightarrow> dbfm"
   where
    "trans_fm e (Mem t u) = DBMem (trans_tm e t) (trans_tm e u)"
  | "trans_fm e (Eq t u)  = DBEq (trans_tm e t) (trans_tm e u)"
  | "trans_fm e (Disj A B) = DBDisj (trans_fm e A) (trans_fm e B)"
  | "trans_fm e (Neg A)   = DBNeg (trans_fm e A)"
  | "atom k \<sharp> e \<Longrightarrow> trans_fm e (Ex k A) = DBEx (trans_fm (k#e) A)"
-supply [[simproc del: defined_all]]
-apply(simp add: eqvt_def trans_fm_graph_aux_def)
-apply(erule trans_fm_graph.induct)
-using [[simproc del: alpha_lst]]
-apply(auto simp: fresh_star_def)
-apply(rule_tac y=b and c=a in fm.strong_exhaust)
-apply(auto simp: fresh_star_def)
-apply(erule_tac c=ea in Abs_lst1_fcb2')
-apply (simp_all add: eqvt_at_def)
-apply (simp_all add: fresh_star_Pair perm_supp_eq)
-apply (simp add: fresh_star_def)
-done
+                   supply [[simproc del: defined_all]]
+                   apply(simp add: eqvt_def trans_fm_graph_aux_def)
+                  apply(erule trans_fm_graph.induct)
+  using [[simproc del: alpha_lst]]
+                      apply(auto simp: fresh_star_def)
+   apply (metis fm.strong_exhaust fresh_star_insert)
+  apply(erule Abs_lst1_fcb2')
+     apply (simp_all add: eqvt_at_def)
+    apply (simp_all add: fresh_star_Pair perm_supp_eq)
+  apply (simp add: fresh_star_def)
+  done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_trans_fm [simp]: "i \<sharp> trans_fm e A \<longleftrightarrow> i \<sharp> A \<or> i \<in> atom ` set e"
   by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base)
 
 abbreviation DBConj :: "dbfm \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where "DBConj t u \<equiv> DBNeg (DBDisj (DBNeg t) (DBNeg u))"
 
 lemma trans_fm_Conj [simp]: "trans_fm e (Conj A B) = DBConj (trans_fm e A) (trans_fm e B)"
   by (simp add: Conj_def)
 
 lemma trans_tm_inject [iff]: "(trans_tm e t = trans_tm e u) \<longleftrightarrow> t = u"
 proof (induct t arbitrary: e u rule: tm.induct)
   case Zero show ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
     done
 next
   case (Var i) show ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(1) dbtm.distinct(3) lookup_in lookup_notin)
     apply (metis dbtm.distinct(10) dbtm.distinct(11) lookup_in lookup_notin)
     done
 next
   case (Eats tm1 tm2) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (metis dbtm.distinct(12) dbtm.distinct(9) lookup_in lookup_notin)
     done
 qed
 
 lemma trans_fm_inject [iff]: "(trans_fm e A = trans_fm e B) \<longleftrightarrow> A = B"
 proof (nominal_induct A avoiding: e B rule: fm.strong_induct)
   case (Mem tm1 tm2) thus ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
 next
   case (Eq tm1 tm2) thus ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: fresh_star_def)
 next
   case (Disj fm1 fm2) show ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Disj fresh_star_def)
 next
   case (Neg fm) show ?case
     by (rule fm.strong_exhaust [where y=B and c=e]) (auto simp: Neg fresh_star_def)
 next
   case (Ex name fm)
   thus ?case  using [[simproc del: alpha_lst]]
   proof (cases rule: fm.strong_exhaust [where y=B and c="(e, name)"], simp_all add: fresh_star_def)
     fix name'::name and fm'::fm
     assume name': "atom name' \<sharp> (e, name)"
     assume "atom name \<sharp> fm' \<or> name = name'"
     thus "(trans_fm (name # e) fm = trans_fm (name' # e) fm') = ([[atom name]]lst. fm = [[atom name']]lst. fm')"
          (is "?lhs = ?rhs")
     proof (rule disjE)
       assume "name = name'"
       thus "?lhs = ?rhs"
         by (metis fresh_Pair fresh_at_base(2) name')
     next
       assume name: "atom name \<sharp> fm'"
       have eq1: "(name \<leftrightarrow> name') \<bullet> trans_fm (name' # e) fm' = trans_fm (name' # e) fm'"
         by (simp add: flip_fresh_fresh name)
       have eq2: "(name \<leftrightarrow> name') \<bullet> ([[atom name']]lst. fm') = [[atom name']]lst. fm'"
         by (rule flip_fresh_fresh) (auto simp: Abs_fresh_iff name)
       show "?lhs = ?rhs" using name' eq1 eq2 Ex(1) Ex(3) [of "name#e" "(name \<leftrightarrow> name') \<bullet> fm'"]
         by (simp add: flip_fresh_fresh) (metis Abs1_eq(3))
     qed
   qed
 qed
 
 lemma trans_fm_perm:
   assumes c: "atom c \<sharp> (i,j,A,B)"
   and     t: "trans_fm [i] A = trans_fm [j] B"
   shows "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B"
 proof -
   have c_fresh1: "atom c \<sharp> trans_fm [i] A"
     using c by (auto simp: supp_Pair)
   moreover
   have i_fresh: "atom i \<sharp> trans_fm [i] A"
     by auto
   moreover
   have c_fresh2: "atom c \<sharp> trans_fm [j] B"
     using c by (auto simp: supp_Pair)
   moreover
   have j_fresh: "atom j \<sharp> trans_fm [j] B"
     by auto
   ultimately have "((i \<leftrightarrow> c) \<bullet> (trans_fm [i] A)) = ((j \<leftrightarrow> c) \<bullet> trans_fm [j] B)"
     by (simp only: flip_fresh_fresh t)
   then have "trans_fm [c] ((i \<leftrightarrow> c) \<bullet> A) = trans_fm [c] ((j \<leftrightarrow> c) \<bullet> B)"
     by simp
   then show "(i \<leftrightarrow> c) \<bullet> A = (j \<leftrightarrow> c) \<bullet> B" by simp
 qed
 
 section\<open>Characterising the Well-Formed de Bruijn Formulas\<close>
 
 subsection\<open>Well-Formed Terms\<close>
 
 inductive wf_dbtm :: "dbtm \<Rightarrow> bool"
   where
     Zero:  "wf_dbtm DBZero"
   | Var:   "wf_dbtm (DBVar name)"
   | Eats:  "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbtm (DBEats t1 t2)"
 
 equivariance wf_dbtm
 
 inductive_cases Zero_wf_dbtm [elim!]: "wf_dbtm DBZero"
 inductive_cases Var_wf_dbtm [elim!]:  "wf_dbtm (DBVar name)"
 inductive_cases Ind_wf_dbtm [elim!]:  "wf_dbtm (DBInd i)"
 inductive_cases Eats_wf_dbtm [elim!]: "wf_dbtm (DBEats t1 t2)"
 
 declare wf_dbtm.intros [intro]
 
 lemma wf_dbtm_imp_is_tm:
   assumes "wf_dbtm x"
   shows "\<exists>t::tm. x = trans_tm [] t"
 using assms
 proof (induct rule: wf_dbtm.induct)
   case Zero thus ?case
     by (metis trans_tm.simps(1))
 next
   case (Var i) thus ?case
     by (metis lookup.simps(1) trans_tm.simps(2))
 next
   case (Eats dt1 dt2) thus ?case
     by (metis trans_tm.simps(3))
 qed
 
 lemma wf_dbtm_trans_tm: "wf_dbtm (trans_tm [] t)"
   by (induct t rule: tm.induct) auto
 
 theorem wf_dbtm_iff_is_tm: "wf_dbtm x \<longleftrightarrow> (\<exists>t::tm. x = trans_tm [] t)"
   by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm)
 
 nominal_function abst_dbtm :: "name \<Rightarrow> nat \<Rightarrow> dbtm \<Rightarrow> dbtm"
   where
    "abst_dbtm name i DBZero = DBZero"
  | "abst_dbtm name i (DBVar name') = (if name = name' then DBInd i else DBVar name')"
  | "abst_dbtm name i (DBInd j) = DBInd j"
  | "abst_dbtm name i (DBEats t1 t2) = DBEats (abst_dbtm name i t1) (abst_dbtm name i t2)"
 apply (simp add: eqvt_def abst_dbtm_graph_aux_def, auto)
 apply (metis dbtm.exhaust)
 done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 nominal_function subst_dbtm :: "dbtm \<Rightarrow> name \<Rightarrow> dbtm \<Rightarrow> dbtm"
   where
    "subst_dbtm u i DBZero = DBZero"
  | "subst_dbtm u i (DBVar name) = (if i = name then u else DBVar name)"
  | "subst_dbtm u i (DBInd j) = DBInd j"
  | "subst_dbtm u i (DBEats t1 t2) = DBEats (subst_dbtm u i t1) (subst_dbtm u i t2)"
 by (auto simp: eqvt_def subst_dbtm_graph_aux_def) (metis dbtm.exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_iff_non_subst_dbtm: "subst_dbtm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
   by (induct t rule: dbtm.induct) (auto simp: pure_fresh fresh_at_base(2))
 
 lemma lookup_append: "lookup (e @ [i]) n j = abst_dbtm i (length e + n) (lookup e n j)"
   by (induct e arbitrary: n) (auto simp: fresh_Cons)
 
 lemma trans_tm_abs: "trans_tm (e@[name]) t = abst_dbtm name (length e) (trans_tm e t)"
   by (induct t rule: tm.induct) (auto simp: lookup_notin lookup_append)
 
 subsection\<open>Well-Formed Formulas\<close>
 
 nominal_function abst_dbfm :: "name \<Rightarrow> nat \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where
    "abst_dbfm name i (DBMem t1 t2) = DBMem (abst_dbtm name i t1) (abst_dbtm name i t2)"
  | "abst_dbfm name i (DBEq t1 t2) =  DBEq (abst_dbtm name i t1) (abst_dbtm name i t2)"
  | "abst_dbfm name i (DBDisj A1 A2) = DBDisj (abst_dbfm name i A1) (abst_dbfm name i A2)"
  | "abst_dbfm name i (DBNeg A) = DBNeg (abst_dbfm name i A)"
  | "abst_dbfm name i (DBEx A) = DBEx (abst_dbfm name (i+1) A)"
 apply (simp add: eqvt_def abst_dbfm_graph_aux_def, auto)
 apply (metis dbfm.exhaust)
 done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 nominal_function subst_dbfm :: "dbtm \<Rightarrow> name \<Rightarrow> dbfm \<Rightarrow> dbfm"
   where
    "subst_dbfm u i (DBMem t1 t2) = DBMem (subst_dbtm u i t1) (subst_dbtm u i t2)"
  | "subst_dbfm u i (DBEq t1 t2) =  DBEq (subst_dbtm u i t1) (subst_dbtm u i t2)"
  | "subst_dbfm u i (DBDisj A1 A2) = DBDisj (subst_dbfm u i A1) (subst_dbfm u i A2)"
  | "subst_dbfm u i (DBNeg A) = DBNeg (subst_dbfm u i A)"
  | "subst_dbfm u i (DBEx A) = DBEx (subst_dbfm u i A)"
 by (auto simp: eqvt_def subst_dbfm_graph_aux_def) (metis dbfm.exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma fresh_iff_non_subst_dbfm: "subst_dbfm DBZero i t = t \<longleftrightarrow> atom i \<sharp> t"
   by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm)
 
 
 section\<open>Well formed terms and formulas (de Bruijn representation)\<close>
 
 inductive wf_dbfm :: "dbfm \<Rightarrow> bool"
   where
     Mem:   "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbfm (DBMem t1 t2)"
   | Eq:    "wf_dbtm t1 \<Longrightarrow> wf_dbtm t2 \<Longrightarrow> wf_dbfm (DBEq t1 t2)"
   | Disj:  "wf_dbfm A1 \<Longrightarrow> wf_dbfm A2 \<Longrightarrow> wf_dbfm (DBDisj A1 A2)"
   | Neg:   "wf_dbfm A \<Longrightarrow> wf_dbfm (DBNeg A)"
   | Ex:    "wf_dbfm A \<Longrightarrow> wf_dbfm (DBEx (abst_dbfm name 0 A))"
 
 equivariance wf_dbfm
 
 lemma atom_fresh_abst_dbtm [simp]: "atom i \<sharp> abst_dbtm i n t"
   by (induct t rule: dbtm.induct) (auto simp: pure_fresh)
 
 lemma atom_fresh_abst_dbfm [simp]: "atom i \<sharp> abst_dbfm i n A"
   by (nominal_induct A arbitrary: n rule: dbfm.strong_induct) auto
 
 text\<open>Setting up strong induction: "avoiding" for name. Necessary to allow some proofs to go through\<close>
 nominal_inductive wf_dbfm
   avoids Ex: name
   by (auto simp: fresh_star_def)
 
 inductive_cases Mem_wf_dbfm [elim!]:  "wf_dbfm (DBMem t1 t2)"
 inductive_cases Eq_wf_dbfm [elim!]:   "wf_dbfm (DBEq t1 t2)"
 inductive_cases Disj_wf_dbfm [elim!]: "wf_dbfm (DBDisj A1 A2)"
 inductive_cases Neg_wf_dbfm [elim!]:  "wf_dbfm (DBNeg A)"
 inductive_cases Ex_wf_dbfm [elim!]:   "wf_dbfm (DBEx z)"
 
 declare wf_dbfm.intros [intro]
 
 lemma trans_fm_abs: "trans_fm (e@[name]) A = abst_dbfm name (length e) (trans_fm e A)"
   apply (nominal_induct A avoiding: name e rule: fm.strong_induct)
   apply (auto simp: trans_tm_abs fresh_Cons fresh_append)
   apply (metis One_nat_def Suc_eq_plus1 append_Cons list.size(4))
   done
 
 lemma abst_trans_fm: "abst_dbfm name 0 (trans_fm [] A) = trans_fm [name] A"
   by (metis append_Nil list.size(3) trans_fm_abs)
 
 lemma abst_trans_fm2: "i \<noteq> j \<Longrightarrow> abst_dbfm i (Suc 0) (trans_fm [j] A) = trans_fm [j,i] A"
   using trans_fm_abs [where e="[j]" and name=i]
   by auto
 
 lemma wf_dbfm_imp_is_fm:
   assumes "wf_dbfm x" shows "\<exists>A::fm. x = trans_fm [] A"
 using assms
 proof (induct rule: wf_dbfm.induct)
   case (Mem t1 t2) thus ?case
     by (metis trans_fm.simps(1) wf_dbtm_imp_is_tm)
 next
   case (Eq t1 t2) thus ?case
     by (metis trans_fm.simps(2) wf_dbtm_imp_is_tm)
 next
   case (Disj fm1 fm2) thus ?case
     by (metis trans_fm.simps(3))
 next
   case (Neg fm) thus ?case
     by (metis trans_fm.simps(4))
 next
   case (Ex fm name) thus ?case
     apply auto
     apply (rule_tac x="Ex name A" in exI)
     apply (auto simp: abst_trans_fm)
     done
 qed
 
 lemma wf_dbfm_trans_fm: "wf_dbfm (trans_fm [] A)"
   apply (nominal_induct A rule: fm.strong_induct)
   apply (auto simp: wf_dbtm_trans_tm abst_trans_fm)
   apply (metis abst_trans_fm wf_dbfm.Ex)
   done
 
 lemma wf_dbfm_iff_is_fm: "wf_dbfm x \<longleftrightarrow> (\<exists>A::fm. x = trans_fm [] A)"
   by (metis wf_dbfm_imp_is_fm wf_dbfm_trans_fm)
 
 lemma dbtm_abst_ignore [simp]:
   "abst_dbtm name i (abst_dbtm name j t) = abst_dbtm name j t"
   by (induct t rule: dbtm.induct) auto
 
 lemma abst_dbtm_fresh_ignore [simp]: "atom name \<sharp> u \<Longrightarrow> abst_dbtm name j u = u"
   by (induct u rule: dbtm.induct) auto
 
 lemma dbtm_subst_ignore [simp]:
   "subst_dbtm u name (abst_dbtm name j t) = abst_dbtm name j t"
   by (induct t rule: dbtm.induct) auto
 
 lemma dbtm_abst_swap_subst:
   "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
    subst_dbtm u name (abst_dbtm name' j t) = abst_dbtm name' j (subst_dbtm u name t)"
   by (induct t rule: dbtm.induct) auto
 
 lemma dbfm_abst_swap_subst:
   "name \<noteq> name' \<Longrightarrow> atom name' \<sharp> u \<Longrightarrow>
    subst_dbfm u name (abst_dbfm name' j A) = abst_dbfm name' j (subst_dbfm u name A)"
   by (induct A arbitrary: j rule: dbfm.induct) (auto simp: dbtm_abst_swap_subst)
 
 lemma subst_trans_commute [simp]:
   "atom i \<sharp> e \<Longrightarrow> subst_dbtm (trans_tm e u) i (trans_tm e t) = trans_tm e (subst i u t)"
   apply (induct t rule: tm.induct)
   apply (auto simp: lookup_notin fresh_imp_notin_env)
   apply (metis abst_dbtm_fresh_ignore dbtm_subst_ignore lookup_fresh lookup_notin subst_dbtm.simps(2))
   done
 
 lemma subst_fm_trans_commute [simp]:
   "subst_dbfm (trans_tm [] u) name (trans_fm [] A) = trans_fm [] (A (name::= u))"
   apply (nominal_induct A avoiding: name u rule: fm.strong_induct)
   apply (auto simp: lookup_notin abst_trans_fm [symmetric])
   apply (metis dbfm_abst_swap_subst fresh_at_base(2) fresh_trans_tm_iff)
   done
 
 lemma subst_fm_trans_commute_eq:
   "du = trans_tm [] u \<Longrightarrow> subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))"
   by (metis subst_fm_trans_commute)
 
 
 section\<open>Quotations\<close>
 
 fun htuple :: "nat \<Rightarrow> hf"  where
    "htuple 0 = \<langle>0,0\<rangle>"
  | "htuple (Suc k) = \<langle>0, htuple k\<rangle>"
 
 fun HTuple :: "nat \<Rightarrow> tm"  where
    "HTuple 0 = HPair Zero Zero"
  | "HTuple (Suc k) = HPair Zero (HTuple k)"
 
 lemma eval_tm_HTuple [simp]:  "\<lbrakk>HTuple n\<rbrakk>e = htuple n"
   by (induct n) auto
 
 lemma fresh_HTuple [simp]: "x \<sharp> HTuple n"
   by (induct n) auto
 
 lemma HTuple_eqvt[eqvt]: "(p \<bullet> HTuple n) = HTuple (p \<bullet> n)"
   by (induct n, auto simp: HPair_eqvt permute_pure)
 
 lemma htuple_nonzero [simp]: "htuple k \<noteq> 0"
   by (induct k) auto
 
 lemma htuple_inject [iff]: "htuple i = htuple j \<longleftrightarrow> i=j"
 proof (induct i arbitrary: j)
   case 0 show ?case
     by (cases j) auto
 next
   case (Suc i) show ?case
     by (cases j) (auto simp: Suc)
 qed
 
 subsection \<open>Quotations of de Bruijn terms\<close>
 
 definition nat_of_name :: "name \<Rightarrow> nat"
   where "nat_of_name x = nat_of (atom x)"
 
 lemma nat_of_name_inject [simp]: "nat_of_name n1 = nat_of_name n2 \<longleftrightarrow> n1 = n2"
   by (metis nat_of_name_def atom_components_eq_iff atom_eq_iff sort_of_atom_eq)
 
 definition name_of_nat :: "nat \<Rightarrow> name"
   where "name_of_nat n \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) n)"
 
 lemma nat_of_name_Abs_eq [simp]: "nat_of_name (Abs_name (Atom (Sort ''SyntaxN.name'' []) n)) = n"
   by (auto simp: nat_of_name_def atom_name_def Abs_name_inverse)
 
 lemma nat_of_name_name_eq [simp]: "nat_of_name (name_of_nat n) = n"
   by (simp add: name_of_nat_def)
 
 lemma name_of_nat_nat_of_name [simp]: "name_of_nat (nat_of_name i) = i"
   by (metis nat_of_name_inject nat_of_name_name_eq)
 
 lemma HPair_neq_ORD_OF [simp]: "HPair x y \<noteq> ORD_OF i"
   by (metis Not_Ord_hpair Ord_ord_of eval_tm_HPair eval_tm_ORD_OF)
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function quot_dbtm :: "dbtm \<Rightarrow> tm"
   where
    "quot_dbtm DBZero = Zero"
  | "quot_dbtm (DBVar name) = ORD_OF (Suc (nat_of_name name))"
  | "quot_dbtm (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
  | "quot_dbtm (DBEats t u) = HPair (HTuple 1) (HPair (quot_dbtm t) (quot_dbtm u))"
 by (rule dbtm.exhaust) auto
 
 termination
   by lexicographic_order
 
 lemma quot_dbtm_inject_lemma [simp]: "\<lbrakk>quot_dbtm t\<rbrakk>e = \<lbrakk>quot_dbtm u\<rbrakk>e \<longleftrightarrow> t=u"
 proof (induct t arbitrary: u rule: dbtm.induct)
   case DBZero show ?case
     by (induct u rule: dbtm.induct) auto
 next
   case (DBVar name) show ?case
     by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord')
 next
   case (DBInd k) show ?case
     by (induct u rule: dbtm.induct) (auto simp: hpair_neq_Ord hpair_neq_Ord')
 next
   case (DBEats t1 t2) thus ?case
     by (induct u rule: dbtm.induct) (simp_all add: hpair_neq_Ord)
 qed
 
 lemma quot_dbtm_inject [iff]: "quot_dbtm t = quot_dbtm u \<longleftrightarrow> t=u"
   by (metis quot_dbtm_inject_lemma)
 
 subsection \<open>Quotations of de Bruijn formulas\<close>
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function quot_dbfm :: "dbfm \<Rightarrow> tm"
   where
    "quot_dbfm (DBMem t u) = HPair (HTuple 0) (HPair (quot_dbtm t) (quot_dbtm u))"
  | "quot_dbfm (DBEq t u) = HPair (HTuple 2) (HPair (quot_dbtm t) (quot_dbtm u))"
  | "quot_dbfm (DBDisj A B) = HPair (HTuple 3) (HPair (quot_dbfm A) (quot_dbfm B))"
  | "quot_dbfm (DBNeg A) = HPair (HTuple 4) (quot_dbfm A)"
  | "quot_dbfm (DBEx A) = HPair (HTuple 5) (quot_dbfm A)"
 by (rule_tac y=x in dbfm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma htuple_minus_1: "n > 0 \<Longrightarrow> htuple n = \<langle>0, htuple (n - 1)\<rangle>"
   by (metis Suc_diff_1 htuple.simps(2))
 
 lemma HTuple_minus_1: "n > 0 \<Longrightarrow> HTuple n = HPair Zero (HTuple (n - 1))"
   by (metis Suc_diff_1 HTuple.simps(2))
 
 lemmas HTS = HTuple_minus_1 HTuple.simps \<comment> \<open>for freeness reasoning on codes\<close>
 
 lemma quot_dbfm_inject_lemma [simp]: "\<lbrakk>quot_dbfm A\<rbrakk>e = \<lbrakk>quot_dbfm B\<rbrakk>e \<longleftrightarrow> A=B"
 proof (induct A arbitrary: B rule: dbfm.induct)
   case (DBMem t u) show ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBEq t u) show ?case
     by (induct B rule: dbfm.induct) (auto simp: htuple_minus_1)
 next
   case (DBDisj A B') thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBNeg A) thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 next
   case (DBEx A) thus ?case
     by (induct B rule: dbfm.induct) (simp_all add: htuple_minus_1)
 qed
 
 
 class quot =
   fixes quot :: "'a \<Rightarrow> tm"  ("\<guillemotleft>_\<guillemotright>")
 
 instantiation tm :: quot
 begin
   definition quot_tm :: "tm \<Rightarrow> tm"
     where "quot_tm t = quot_dbtm (trans_tm [] t)"
   
   instance ..
 end
 
 lemma quot_dbtm_fresh [simp]: "s \<sharp> (quot_dbtm t)"
   by (induct t rule: dbtm.induct) auto
 
 lemma quot_tm_fresh [simp]: fixes t::tm shows "s \<sharp> \<guillemotleft>t\<guillemotright>"
   by (simp add: quot_tm_def)
 
 lemma quot_Zero [simp]: "\<guillemotleft>Zero\<guillemotright> = Zero"
   by (simp add: quot_tm_def)
 
 lemma quot_Var: "\<guillemotleft>Var x\<guillemotright> = SUCC (ORD_OF (nat_of_name x))"
   by (simp add: quot_tm_def)
 
 lemma quot_Eats: "\<guillemotleft>Eats x y\<guillemotright> = HPair (HTuple 1) (HPair \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>)"
   by (simp add: quot_tm_def)
 
 text\<open>irrelevance of the environment for quotations, because they are ground terms\<close>
 lemma eval_quot_dbtm_ignore:
     "\<lbrakk>quot_dbtm t\<rbrakk>e = \<lbrakk>quot_dbtm t\<rbrakk>e'"
   by (induct t rule: dbtm.induct) auto
 
 lemma eval_quot_dbfm_ignore:
     "\<lbrakk>quot_dbfm A\<rbrakk>e = \<lbrakk>quot_dbfm A\<rbrakk>e'"
   by (induct A rule: dbfm.induct) (auto intro: eval_quot_dbtm_ignore)
 
 
 instantiation fm :: quot
 begin
   definition quot_fm :: "fm \<Rightarrow> tm"
     where "quot_fm A = quot_dbfm (trans_fm [] A)"
   
   instance ..
 end
 
 lemma quot_dbfm_fresh [simp]: "s \<sharp> (quot_dbfm A)"
   by (induct A rule: dbfm.induct) auto
 
 lemma quot_fm_fresh [simp]: fixes A::fm shows "s \<sharp> \<guillemotleft>A\<guillemotright>"
   by (simp add: quot_fm_def)
 
 lemma quot_fm_permute [simp]: fixes A:: fm shows "p \<bullet> \<guillemotleft>A\<guillemotright> = \<guillemotleft>A\<guillemotright>"
   by (metis fresh_star_def perm_supp_eq quot_fm_fresh)
 
 lemma quot_Mem: "\<guillemotleft>x IN y\<guillemotright> = HPair (HTuple 0) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
   by (simp add: quot_fm_def quot_tm_def)
 
 lemma quot_Eq: "\<guillemotleft>x EQ y\<guillemotright> = HPair (HTuple 2) (HPair (\<guillemotleft>x\<guillemotright>) (\<guillemotleft>y\<guillemotright>))"
   by (simp add: quot_fm_def quot_tm_def)
 
 lemma quot_Disj: "\<guillemotleft>A OR B\<guillemotright> = HPair (HTuple 3) (HPair (\<guillemotleft>A\<guillemotright>) (\<guillemotleft>B\<guillemotright>))"
   by (simp add: quot_fm_def)
 
 lemma quot_Neg: "\<guillemotleft>Neg A\<guillemotright> = HPair (HTuple 4) (\<guillemotleft>A\<guillemotright>)"
   by (simp add: quot_fm_def)
 
 lemma quot_Ex: "\<guillemotleft>Ex i A\<guillemotright> = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))"
   by (simp add: quot_fm_def)
 
 lemma eval_quot_fm_ignore: fixes A:: fm shows "\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e'"
   by (metis eval_quot_dbfm_ignore quot_fm_def)
 
 lemmas quot_simps = quot_Var quot_Eats quot_Eq quot_Mem quot_Disj quot_Neg quot_Ex
 
 section\<open>Definitions Involving Coding\<close>
 
 definition q_Var :: "name \<Rightarrow> hf"
   where "q_Var i \<equiv> succ (ord_of (nat_of_name i))"
 
 definition q_Ind :: "hf \<Rightarrow> hf"
   where "q_Ind k \<equiv>  \<langle>htuple 6, k\<rangle>"
 
 abbreviation Q_Eats :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Eats t u \<equiv> HPair (HTuple (Suc 0)) (HPair t u)"
 
 definition q_Eats :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Eats x y \<equiv> \<langle>htuple 1, x, y\<rangle>"
 
 abbreviation Q_Succ :: "tm \<Rightarrow> tm"
   where "Q_Succ t \<equiv> Q_Eats t t"
 
 definition q_Succ :: "hf \<Rightarrow> hf"
   where "q_Succ x \<equiv> q_Eats x x"
 
 lemma quot_Succ: "\<guillemotleft>SUCC x\<guillemotright> = Q_Succ \<guillemotleft>x\<guillemotright>"
   by (auto simp: SUCC_def quot_Eats)
 
 abbreviation Q_HPair :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_HPair t u \<equiv>
            Q_Eats (Q_Eats Zero (Q_Eats (Q_Eats Zero u) t))
                   (Q_Eats (Q_Eats Zero t) t)"
 
 definition q_HPair :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_HPair x y \<equiv>
            q_Eats (q_Eats 0 (q_Eats (q_Eats 0 y) x))
                   (q_Eats (q_Eats 0 x) x)"
 
 abbreviation Q_Mem :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Mem t u \<equiv> HPair (HTuple 0) (HPair t u)"
 
 definition q_Mem :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Mem x y \<equiv> \<langle>htuple 0, x, y\<rangle>"
 
 abbreviation Q_Eq :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Eq t u \<equiv> HPair (HTuple 2) (HPair t u)"
 
 definition q_Eq :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Eq x y \<equiv> \<langle>htuple 2, x, y\<rangle>"
 
 abbreviation Q_Disj :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Disj t u \<equiv> HPair (HTuple 3) (HPair t u)"
 
 definition q_Disj :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Disj x y \<equiv> \<langle>htuple 3, x, y\<rangle>"
 
 abbreviation Q_Neg :: "tm \<Rightarrow> tm"
   where "Q_Neg t \<equiv> HPair (HTuple 4) t"
 
 definition q_Neg :: "hf \<Rightarrow> hf"
   where "q_Neg x \<equiv> \<langle>htuple 4, x\<rangle>"
 
 abbreviation Q_Conj :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Conj t u \<equiv> Q_Neg (Q_Disj (Q_Neg t) (Q_Neg u))"
 
 definition q_Conj :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Conj t u \<equiv> q_Neg (q_Disj (q_Neg t) (q_Neg u))"
 
 abbreviation Q_Imp :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "Q_Imp t u \<equiv> Q_Disj (Q_Neg t) u"
 
 definition q_Imp :: "hf \<Rightarrow> hf \<Rightarrow> hf"
   where "q_Imp t u \<equiv> q_Disj (q_Neg t) u"
 
 abbreviation Q_Ex :: "tm \<Rightarrow> tm"
   where "Q_Ex t \<equiv> HPair (HTuple 5) t"
 
 definition q_Ex :: "hf \<Rightarrow> hf"
   where "q_Ex x \<equiv> \<langle>htuple 5, x\<rangle>"
 
 abbreviation Q_All :: "tm \<Rightarrow> tm"
   where "Q_All t \<equiv> Q_Neg (Q_Ex (Q_Neg t))"
 
 definition q_All :: "hf \<Rightarrow> hf"
   where "q_All x \<equiv> q_Neg (q_Ex (q_Neg x))"
 
 lemmas q_defs = q_Var_def q_Ind_def q_Eats_def q_HPair_def q_Eq_def q_Mem_def
                 q_Disj_def q_Neg_def q_Conj_def q_Imp_def q_Ex_def q_All_def
 
 lemma q_Eats_iff [iff]: "q_Eats x y = q_Eats x' y' \<longleftrightarrow> x=x' \<and> y=y'"
   by (metis hpair_iff q_Eats_def)
 
 lemma quot_subst_eq: "\<guillemotleft>A(i::=t)\<guillemotright> = quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))"
   by (metis quot_fm_def subst_fm_trans_commute)
 
 lemma Q_Succ_cong: "H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> Q_Succ x EQ Q_Succ x'"
   by (metis HPair_cong Refl)
 
   
 section\<open>Quotations are Injective\<close>
 
 subsection\<open>Terms\<close>
 
 lemma eval_tm_inject [simp]: fixes t::tm shows "\<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk> e = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk> e \<longleftrightarrow> t=u"
 proof (induct t arbitrary: u rule: tm.induct)
   case Zero thus ?case
     by (cases u rule: tm.exhaust) (auto simp: quot_Var quot_Eats)
 next
   case (Var i) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (auto simp: quot_Var quot_Eats)
     done
 next
   case (Eats t1 t2) thus ?case
     apply (cases u rule: tm.exhaust, auto)
     apply (auto simp: quot_Eats quot_Var)
     done
 qed
 
 subsection\<open>Formulas\<close>
 
 lemma eval_fm_inject [simp]: fixes A::fm shows "\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk> e = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk> e \<longleftrightarrow> A=B"
 proof (nominal_induct B arbitrary: A rule: fm.strong_induct)
   case (Mem tm1 tm2) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Eq tm1 tm2) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Neg \<alpha>) thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Disj fm1 fm2)
   thus ?case
     by (cases A rule: fm.exhaust, auto simp: quot_simps htuple_minus_1)
 next
   case (Ex i \<alpha>)
   thus ?case
     apply (induct A arbitrary: i rule: fm.induct)
     apply (auto simp: trans_fm_perm quot_simps htuple_minus_1 Abs1_eq_iff_all)
     by (metis (no_types) Abs1_eq_iff_all(3) dbfm.eq_iff(5) fm.eq_iff(5) fresh_Nil trans_fm.simps(5))
 qed
 
 subsection\<open>The set \<open>\<Gamma>\<close> of Definition 1.1, constant terms used for coding\<close>
 
 inductive coding_tm :: "tm \<Rightarrow> bool"
   where
     Ord:    "\<exists>i. x = ORD_OF i \<Longrightarrow> coding_tm x"
   | HPair:  "coding_tm x \<Longrightarrow> coding_tm y \<Longrightarrow> coding_tm (HPair x y)"
 
 declare coding_tm.intros [intro]
 
 lemma coding_tm_Zero [intro]: "coding_tm Zero"
   by (metis ORD_OF.simps(1) Ord)
 
 lemma coding_tm_HTuple [intro]: "coding_tm (HTuple k)"
   by (induct k, auto)
 
 inductive_simps coding_tm_HPair [simp]: "coding_tm (HPair x y)"
 
 lemma quot_dbtm_coding [simp]: "coding_tm (quot_dbtm t)"
   apply (induct t rule: dbtm.induct, auto)
   apply (metis ORD_OF.simps(2) Ord)
   done
 
 lemma quot_dbfm_coding [simp]: "coding_tm (quot_dbfm fm)"
   by (induct fm rule: dbfm.induct, auto)
 
 lemma quot_fm_coding: fixes A::fm shows "coding_tm \<guillemotleft>A\<guillemotright>"
   by (metis quot_dbfm_coding quot_fm_def)
 
 inductive coding_hf :: "hf \<Rightarrow> bool"
   where
     Ord:    "\<exists>i. x = ord_of i \<Longrightarrow> coding_hf x"
   | HPair:  "coding_hf x \<Longrightarrow> coding_hf y \<Longrightarrow> coding_hf (\<langle>x,y\<rangle>)"
 
 declare coding_hf.intros [intro]
 
 lemma coding_hf_0 [intro]: "coding_hf 0"
   by (metis coding_hf.Ord ord_of.simps(1))
 
 inductive_simps coding_hf_hpair [simp]: "coding_hf (\<langle>x,y\<rangle>)"
 
 lemma coding_tm_hf [simp]: "coding_tm t \<Longrightarrow> coding_hf \<lbrakk>t\<rbrakk>e"
   by (induct t rule: coding_tm.induct) auto
 
   
 section \<open>V-Coding for terms and formulas, for the Second Theorem\<close>
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function vquot_dbtm :: "name set \<Rightarrow> dbtm \<Rightarrow> tm"
   where
    "vquot_dbtm V DBZero = Zero"
  | "vquot_dbtm V (DBVar name) = (if name \<in> V then Var name
                                  else ORD_OF (Suc (nat_of_name name)))"
  | "vquot_dbtm V (DBInd k) = HPair (HTuple 6) (ORD_OF k)"
  | "vquot_dbtm V (DBEats t u) = HPair (HTuple 1) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
 by (auto, rule_tac y=b in dbtm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma fresh_vquot_dbtm [simp]: "i \<sharp> vquot_dbtm V tm \<longleftrightarrow> i \<sharp> tm \<or> i \<notin> atom ` V"
   by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh)
 
 text\<open>Infinite support, so we cannot use nominal primrec.\<close>
 function vquot_dbfm :: "name set \<Rightarrow> dbfm \<Rightarrow> tm"
   where
    "vquot_dbfm V (DBMem t u) = HPair (HTuple 0) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
  | "vquot_dbfm V (DBEq t u) = HPair (HTuple 2) (HPair (vquot_dbtm V t) (vquot_dbtm V u))"
  | "vquot_dbfm V (DBDisj A B) = HPair (HTuple 3) (HPair (vquot_dbfm V A) (vquot_dbfm V B))"
  | "vquot_dbfm V (DBNeg A) = HPair (HTuple 4) (vquot_dbfm V A)"
  | "vquot_dbfm V (DBEx A) = HPair (HTuple 5) (vquot_dbfm V A)"
 by (auto, rule_tac y=b in dbfm.exhaust, auto)
 
 termination
   by lexicographic_order
 
 lemma fresh_vquot_dbfm [simp]: "i \<sharp> vquot_dbfm V fm \<longleftrightarrow> i \<sharp> fm \<or> i \<notin> atom ` V"
   by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1)
 
 class vquot =
   fixes vquot :: "'a \<Rightarrow> name set \<Rightarrow> tm"  ("\<lfloor>_\<rfloor>_"  [0,1000]1000)
 
 instantiation tm :: vquot
 begin
   definition vquot_tm :: "tm \<Rightarrow> name set \<Rightarrow> tm"
     where "vquot_tm t V = vquot_dbtm V (trans_tm [] t)"
   instance ..
 end
 
 lemma vquot_dbtm_empty [simp]: "vquot_dbtm {} t = quot_dbtm t"
   by (induct t rule: dbtm.induct) auto
 
 lemma vquot_tm_empty [simp]: fixes t::tm shows "\<lfloor>t\<rfloor>{} = \<guillemotleft>t\<guillemotright>"
   by (simp add: vquot_tm_def quot_tm_def)
 
 lemma vquot_dbtm_eq: "atom ` V \<inter> supp t = atom ` W \<inter> supp t \<Longrightarrow> vquot_dbtm V t = vquot_dbtm W t"
   by (induct t rule: dbtm.induct) (auto simp: image_iff, blast+)
 
 instantiation fm :: vquot
 begin
   definition vquot_fm :: "fm \<Rightarrow> name set \<Rightarrow> tm"
     where "vquot_fm A V = vquot_dbfm V (trans_fm [] A)"
   instance ..
 end
 
 lemma vquot_fm_fresh [simp]: fixes A::fm shows "i \<sharp> \<lfloor>A\<rfloor>V \<longleftrightarrow> i \<sharp> A \<or> i \<notin> atom ` V"
   by (simp add: vquot_fm_def)
 
 lemma vquot_dbfm_empty [simp]: "vquot_dbfm {} A = quot_dbfm A"
   by (induct A rule: dbfm.induct) auto
 
 lemma vquot_fm_empty [simp]: fixes A::fm shows "\<lfloor>A\<rfloor>{} = \<guillemotleft>A\<guillemotright>"
   by (simp add: vquot_fm_def quot_fm_def)
 
 lemma vquot_dbfm_eq: "atom ` V \<inter> supp A = atom ` W \<inter> supp A \<Longrightarrow> vquot_dbfm V A = vquot_dbfm W A"
   by (induct A rule: dbfm.induct) (auto simp: intro!: vquot_dbtm_eq, blast+)
 
 lemma vquot_fm_insert:
   fixes A::fm shows "atom i \<notin> supp A \<Longrightarrow> \<lfloor>A\<rfloor>(insert i V) = \<lfloor>A\<rfloor>V"
   by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq)
 
 declare HTuple.simps [simp del]
 
 end
diff --git a/thys/Incompleteness/Predicates.thy b/thys/Incompleteness/Predicates.thy
--- a/thys/Incompleteness/Predicates.thy
+++ b/thys/Incompleteness/Predicates.thy
@@ -1,1288 +1,1275 @@
 chapter\<open>Basic Predicates\<close>
 
 theory Predicates
 imports SyntaxN
 begin
 
 section \<open>The Subset Relation\<close>
 
 nominal_function Subset :: "tm \<Rightarrow> tm \<Rightarrow> fm"   (infixr "SUBS" 150)
   where "atom z \<sharp> (t, u) \<Longrightarrow> t SUBS u = All2 z t ((Var z) IN u)"
   by (auto simp: eqvt_def Subset_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 declare Subset.simps [simp del]
 
 lemma Subset_fresh_iff [simp]: "a \<sharp> t SUBS u \<longleftrightarrow> a \<sharp> t \<and> a \<sharp> u"
-apply (rule obtain_fresh [where x="(t, u)"])
-apply (subst Subset.simps, auto)
-done
+  apply (rule obtain_fresh [where x="(t, u)"])
+  apply (subst Subset.simps, auto)
+  done
 
 lemma eval_fm_Subset [simp]: "eval_fm e (Subset t u) \<longleftrightarrow> (\<lbrakk>t\<rbrakk>e \<le> \<lbrakk>u\<rbrakk>e)"
-apply (rule obtain_fresh [where x="(t, u)"])
-apply (subst Subset.simps, auto)
-done
+  apply (rule obtain_fresh [where x="(t, u)"])
+  apply (subst Subset.simps, auto)
+  done
 
 lemma subst_fm_Subset [simp]: "(t SUBS u)(i::=x) = (subst i x t) SUBS (subst i x u)"
 proof -
   obtain j::name where "atom j \<sharp> (i,x,t,u)"
     by (rule obtain_fresh)
   thus ?thesis
     by (auto simp: Subset.simps [of j])
 qed
 
 lemma Subset_I:
   assumes "insert ((Var i) IN t) H \<turnstile> (Var i) IN u" "atom i \<sharp> (t,u)" "\<forall>B \<in> H. atom i \<sharp> B"
   shows "H \<turnstile> t SUBS u"
 by (subst Subset.simps [of i]) (auto simp: assms)
 
 lemma Subset_D:
   assumes major: "H \<turnstile> t SUBS u" and minor: "H \<turnstile> a IN t" shows "H \<turnstile> a IN u"
 proof -
   obtain i::name where i: "atom i \<sharp> (t, u)"
     by (rule obtain_fresh)
   hence "H \<turnstile> (Var i IN t IMP Var i IN u) (i::=a)"
     by (metis Subset.simps major All_D)
   thus ?thesis
     using i  by simp (metis MP_same minor)
 qed
 
 lemma Subset_E: "H \<turnstile> t SUBS u \<Longrightarrow> H \<turnstile> a IN t \<Longrightarrow> insert (a IN u) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
   by (metis Subset_D cut_same)
 
 lemma Subset_cong: "H \<turnstile> t EQ t' \<Longrightarrow> H \<turnstile> u EQ u' \<Longrightarrow> H \<turnstile> t SUBS u IFF t' SUBS u'"
   by (rule P2_cong) auto
 
 lemma Set_MP: "x SUBS y \<in> H \<Longrightarrow> z IN x \<in> H \<Longrightarrow> insert (z IN y) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
   by (metis Assume Subset_D cut_same insert_absorb)
 
 lemma Zero_Subset_I [intro!]: "H \<turnstile> Zero SUBS t"
 proof -
   have "{} \<turnstile> Zero SUBS t"
     by (rule obtain_fresh [where x="(Zero,t)"]) (auto intro: Subset_I)
   thus ?thesis
     by (auto intro: thin)
 qed
 
 lemma Zero_SubsetE: "H \<turnstile> A \<Longrightarrow> insert (Zero SUBS X) H \<turnstile> A"
   by (rule thin1)
 
 lemma Subset_Zero_D:
    assumes "H \<turnstile> t SUBS Zero" shows "H \<turnstile> t EQ Zero"
 proof -
   obtain i::name where i [iff]: "atom i \<sharp> t"
     by (rule obtain_fresh)
   have "{t SUBS Zero} \<turnstile> t EQ Zero"
   proof (rule Eq_Zero_I)
     fix A
     show "{Var i IN t, t SUBS Zero} \<turnstile> A"
       by (metis Hyp Subset_D insertI1 thin1 Mem_Zero_E cut1)
   qed auto
   thus ?thesis
     by (metis assms cut1)
 qed
 
 lemma Subset_refl: "H \<turnstile> t SUBS t"
 proof -
   obtain i::name where "atom i \<sharp> t"
     by (rule obtain_fresh)
   thus ?thesis
     by (metis Assume Subset_I empty_iff fresh_Pair thin0)
 qed
 
 lemma Eats_Subset_Iff: "H \<turnstile> Eats x y SUBS z IFF (x SUBS z) AND (y IN z)"
 proof -
   obtain i::name where i: "atom i \<sharp> (x,y,z)"
     by (rule obtain_fresh)
   have "{} \<turnstile> (Eats x y SUBS z) IFF (x SUBS z AND y IN z)"
   proof (rule Iff_I) 
     show "{Eats x y SUBS z} \<turnstile> x SUBS z AND y IN z"
     proof (rule Conj_I) 
       show "{Eats x y SUBS z} \<turnstile> x SUBS z"
         apply (rule Subset_I [where i=i]) using i
         apply (auto intro: Subset_D Mem_Eats_I1) 
         done
     next
       show "{Eats x y SUBS z} \<turnstile> y IN z"
         by (metis Subset_D Assume Mem_Eats_I2 Refl) 
     qed
   next
     show "{x SUBS z AND y IN z} \<turnstile> Eats x y SUBS z" using i
       by (auto intro!: Subset_I [where i=i] intro: Subset_D Mem_cong [THEN Iff_MP2_same])
   qed
   thus ?thesis
     by (rule thin0) 
 qed
 
 lemma Eats_Subset_I [intro!]: "H \<turnstile> x SUBS z \<Longrightarrow> H \<turnstile> y IN z \<Longrightarrow> H \<turnstile> Eats x y SUBS z"
   by (metis Conj_I Eats_Subset_Iff Iff_MP2_same)
 
 lemma Eats_Subset_E [intro!]:
   "insert (x SUBS z) (insert (y IN z) H) \<turnstile> C \<Longrightarrow> insert (Eats x y SUBS z) H \<turnstile> C"
   by (metis Conj_E Eats_Subset_Iff Iff_MP_left')
 
 text\<open>A surprising proof: a consequence of @{thm Eats_Subset_Iff} and reflexivity!\<close>
 lemma Subset_Eats_I [intro!]: "H \<turnstile> x SUBS Eats x y"
   by (metis Conj_E1 Eats_Subset_Iff Iff_MP_same Subset_refl)
 
 lemma SUCC_Subset_I [intro!]: "H \<turnstile> x SUBS z \<Longrightarrow> H \<turnstile> x IN z \<Longrightarrow> H \<turnstile> SUCC x SUBS z"
   by (metis Eats_Subset_I SUCC_def)
 
 lemma SUCC_Subset_E [intro!]:
   "insert (x SUBS z) (insert (x IN z) H) \<turnstile> C \<Longrightarrow> insert (SUCC x SUBS z) H \<turnstile> C"
   by (metis Eats_Subset_E SUCC_def)
 
 lemma Subset_trans0: "{ a SUBS b, b SUBS c } \<turnstile> a SUBS c"
 proof -
   obtain i::name where [simp]: "atom i \<sharp> (a,b,c)"
     by (rule obtain_fresh)
   show ?thesis
     by (rule Subset_I [of i]) (auto intro: Subset_D)
 qed
 
 lemma Subset_trans: "H \<turnstile> a SUBS b \<Longrightarrow> H \<turnstile> b SUBS c \<Longrightarrow> H \<turnstile> a SUBS c"
   by (metis Subset_trans0 cut2)
 
 lemma Subset_SUCC: "H \<turnstile> a SUBS (SUCC a)"
   by (metis SUCC_def Subset_Eats_I)
 
 lemma All2_Subset_lemma: "atom l \<sharp> (k',k) \<Longrightarrow> {P} \<turnstile> P' \<Longrightarrow> {All2 l k P, k' SUBS k} \<turnstile> All2 l k' P'"
   apply auto
   apply (rule Ex_I [where x = "Var l"])
   apply (auto intro: ContraProve Set_MP cut1)
   done
 
 lemma All2_Subset: "\<lbrakk>H \<turnstile> All2 l k P; H \<turnstile> k' SUBS k; {P} \<turnstile> P'; atom l \<sharp> (k', k)\<rbrakk> \<Longrightarrow> H \<turnstile> All2 l k' P'"
   by (rule cut2 [OF All2_Subset_lemma]) auto
 
 
 section\<open>Extensionality\<close>
 
 lemma Extensionality: "H \<turnstile> x EQ y IFF x SUBS y AND y SUBS x"
 proof -
   obtain i::name and j::name and k::name
     where atoms: "atom i \<sharp> (x,y)"  "atom j \<sharp> (i,x,y)"  "atom k \<sharp> (i,j,y)"
     by (metis obtain_fresh) 
   have "{} \<turnstile> (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)" (is "{} \<turnstile> ?scheme")
   proof (rule Ind [of j])
     show "atom j \<sharp> (i, ?scheme)" using atoms
       by simp 
   next
     show "{} \<turnstile> ?scheme(i::=Zero)" using atoms
     proof auto
       show "{Zero EQ y} \<turnstile> y SUBS Zero"
         by (rule Subset_cong [OF Assume Refl, THEN Iff_MP_same]) (rule Subset_refl)
     next
       show "{Zero SUBS y, y SUBS Zero} \<turnstile> Zero EQ y"
         by (metis AssumeH(2) Subset_Zero_D Sym)
     qed
   next
     show "{} \<turnstile> All i (All j (?scheme IMP ?scheme(i::=Var j) IMP ?scheme(i::=Eats (Var i) (Var j))))"
       using atoms
       apply auto
       apply (metis Subset_cong [OF Refl Assume, THEN Iff_MP_same] Subset_Eats_I)
       apply (metis Mem_cong [OF Refl Assume, THEN Iff_MP_same] Mem_Eats_I2 Refl)
       apply (metis Subset_cong [OF Assume Refl, THEN Iff_MP_same] Subset_refl)
       apply (rule Eq_Eats_I [of _ k, THEN Sym])
       apply (auto intro: Set_MP [where x=y] Subset_D [where t = "Var i"] Disj_I1 Disj_I2)
       apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], auto)
       done
   qed
   hence "{} \<turnstile> (Var i EQ y IFF Var i SUBS y AND y SUBS Var i)(i::=x)" 
     by (metis Subst emptyE)
   thus ?thesis using atoms
     by (simp add: thin0)
 qed
 
 lemma Equality_I: "H \<turnstile> y SUBS x \<Longrightarrow> H \<turnstile> x SUBS y \<Longrightarrow> H \<turnstile> x EQ y"
   by (metis Conj_I Extensionality Iff_MP2_same)
 
 lemma EQ_imp_SUBS: "insert (t EQ u) H \<turnstile> (t SUBS u)"
-proof -
-  have "{t EQ u} \<turnstile> (t SUBS u)"
-    by (metis Assume Conj_E Extensionality Iff_MP_left')
-thus ?thesis
-  by (metis Assume cut1)
-qed
+  by (meson Assume Iff_MP_same Refl Subset_cong Subset_refl)
 
 lemma EQ_imp_SUBS2: "insert (u EQ t) H \<turnstile> (t SUBS u)"
   by (metis EQ_imp_SUBS Sym_L)
 
 lemma Equality_E: "insert (t SUBS u) (insert (u SUBS t) H) \<turnstile> A \<Longrightarrow> insert (t EQ u) H \<turnstile> A"
   by (metis Conj_E Extensionality Iff_MP_left')
 
 
 section \<open>The Disjointness Relation\<close>
 
 text\<open>The following predicate is defined in order to prove Lemma 2.3, Foundation\<close>
 
 nominal_function Disjoint :: "tm \<Rightarrow> tm \<Rightarrow> fm"
   where "atom z \<sharp> (t, u) \<Longrightarrow> Disjoint t u = All2 z t (Neg ((Var z) IN u))"
   by (auto simp: eqvt_def Disjoint_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 declare Disjoint.simps [simp del]
 
 lemma Disjoint_fresh_iff [simp]: "a \<sharp> Disjoint t u \<longleftrightarrow> a \<sharp> t \<and> a \<sharp> u"
 proof -
   obtain j::name where j: "atom j \<sharp> (a,t,u)"
     by (rule obtain_fresh)
   thus ?thesis
     by (auto simp: Disjoint.simps [of j])
 qed
 
 lemma subst_fm_Disjoint [simp]:
   "(Disjoint t u)(i::=x) = Disjoint (subst i x t) (subst i x u)"
 proof -
   obtain j::name where j: "atom j \<sharp> (i,x,t,u)"
     by (rule obtain_fresh)
   thus ?thesis
     by (auto simp: Disjoint.simps [of j])
 qed
 
 lemma Disjoint_cong: "H \<turnstile> t EQ t' \<Longrightarrow> H \<turnstile> u EQ u' \<Longrightarrow> H \<turnstile> Disjoint t u IFF Disjoint t' u'"
   by (rule P2_cong) auto
 
 lemma Disjoint_I:
   assumes "insert ((Var i) IN t) (insert ((Var i) IN u) H) \<turnstile> Fls"
           "atom i \<sharp> (t,u)" "\<forall>B \<in> H. atom i \<sharp> B"
   shows "H \<turnstile> Disjoint t u"
 by (subst Disjoint.simps [of i]) (auto simp: assms insert_commute)
 
 lemma Disjoint_E:
   assumes major: "H \<turnstile> Disjoint t u" and minor: "H \<turnstile> a IN t" "H \<turnstile> a IN u" shows "H \<turnstile> A"
 proof -
   obtain i::name where i: "atom i \<sharp> (t, u)"
     by (rule obtain_fresh)
   hence "H \<turnstile> (Var i IN t IMP Neg (Var i IN u)) (i::=a)"
     by (metis Disjoint.simps major All_D)
   thus ?thesis using i
     by simp (metis MP_same Neg_D minor)
 qed
 
 lemma Disjoint_commute: "{ Disjoint t u } \<turnstile> Disjoint u t"
 proof -
   obtain i::name where "atom i \<sharp> (t,u)"
     by (rule obtain_fresh)
   thus ?thesis
     by (auto simp: fresh_Pair intro: Disjoint_I Disjoint_E) 
 qed
 
 lemma Disjoint_commute_I: "H \<turnstile> Disjoint t u \<Longrightarrow> H \<turnstile> Disjoint u t"
   by (metis Disjoint_commute cut1)
 
 lemma Disjoint_commute_D: "insert (Disjoint t u) H \<turnstile> A \<Longrightarrow> insert (Disjoint u t) H \<turnstile> A" 
   by (metis Assume Disjoint_commute_I cut_same insert_commute thin1)
 
 lemma Zero_Disjoint_I1 [iff]: "H \<turnstile> Disjoint Zero t"
 proof -
   obtain i::name where i: "atom i \<sharp> t"
     by (rule obtain_fresh)
   hence "{} \<turnstile> Disjoint Zero t"
     by (auto intro: Disjoint_I [of i]) 
   thus ?thesis
     by (metis thin0)
 qed
 
 lemma Zero_Disjoint_I2 [iff]: "H \<turnstile> Disjoint t Zero"
   by (metis Disjoint_commute Zero_Disjoint_I1 cut1)
 
 lemma Disjoint_Eats_D1: "{ Disjoint (Eats x y) z } \<turnstile> Disjoint x z"
 proof -
   obtain i::name where i: "atom i \<sharp> (x,y,z)"
     by (rule obtain_fresh)
   show ?thesis
     apply (rule Disjoint_I [of i])  
     apply (blast intro: Disjoint_E Mem_Eats_I1)
     using i apply auto
     done
 qed
 
 lemma Disjoint_Eats_D2: "{ Disjoint (Eats x y) z } \<turnstile> Neg(y IN z)"
 proof -
   obtain i::name where i: "atom i \<sharp> (x,y,z)"
     by (rule obtain_fresh)
   show ?thesis
     by (force intro: Disjoint_E [THEN rotate2] Mem_Eats_I2)
 qed
 
 lemma Disjoint_Eats_E: 
   "insert (Disjoint x z) (insert (Neg(y IN z)) H) \<turnstile> A \<Longrightarrow> insert (Disjoint (Eats x y) z) H \<turnstile> A"
-  apply (rule cut_same [OF cut1 [OF Disjoint_Eats_D2, OF Assume]])
-  apply (rule cut_same [OF cut1 [OF Disjoint_Eats_D1, OF Hyp]])
-  apply (auto intro: thin)
-  done  
+  by (meson Conj_E Conj_I Disjoint_Eats_D1 Disjoint_Eats_D2 rcut1)
 
 lemma Disjoint_Eats_E2: 
   "insert (Disjoint z x) (insert (Neg(y IN z)) H) \<turnstile> A \<Longrightarrow> insert (Disjoint z (Eats x y)) H \<turnstile> A"
   by (metis Disjoint_Eats_E Disjoint_commute_D)
     
 lemma Disjoint_Eats_Imp: "{ Disjoint x z, Neg(y IN z) } \<turnstile> Disjoint (Eats x y) z"
 proof -
   obtain i::name where"atom i \<sharp> (x,y,z)"
     by (rule obtain_fresh)
   then show ?thesis 
     by (auto intro: Disjoint_I [of i]  Disjoint_E [THEN rotate3] 
                     Mem_cong [OF Assume Refl, THEN Iff_MP_same])
 qed
 
 lemma Disjoint_Eats_I [intro!]: "H \<turnstile> Disjoint x z \<Longrightarrow> insert (y IN z) H \<turnstile> Fls \<Longrightarrow> H \<turnstile> Disjoint (Eats x y) z"
   by (metis Neg_I cut2 [OF Disjoint_Eats_Imp])
 
 lemma Disjoint_Eats_I2 [intro!]: "H \<turnstile> Disjoint z x \<Longrightarrow> insert (y IN z) H \<turnstile> Fls \<Longrightarrow> H \<turnstile> Disjoint z (Eats x y)"
   by (metis Disjoint_Eats_I Disjoint_commute cut1)
 
 
 section \<open>The Foundation Theorem\<close>
 
 lemma Foundation_lemma: 
   assumes i: "atom i \<sharp> z"
   shows "{ All2 i z (Neg (Disjoint (Var i) z)) } \<turnstile> Neg (Var i IN z) AND Disjoint (Var i) z"
 proof -
   obtain j::name  where j: "atom j \<sharp> (z,i)"
     by (metis obtain_fresh) 
   show ?thesis
     apply (rule Ind [of j]) using i j
     apply auto
     apply (rule Ex_I [where x=Zero], auto)
     apply (rule Ex_I [where x="Eats (Var i) (Var j)"], auto)
     apply (metis ContraAssume insertI1 insert_commute)
     apply (metis ContraProve Disjoint_Eats_Imp rotate2 thin1)
     apply (metis Assume Disj_I1 anti_deduction rotate3)
     done
 qed    
 
 theorem Foundation: "atom i \<sharp> z \<Longrightarrow> {} \<turnstile> All2 i z (Neg (Disjoint (Var i) z)) IMP z EQ Zero"
   apply auto 
   apply (rule Eq_Zero_I)
   apply (rule cut_same [where A = "(Neg ((Var i) IN z) AND Disjoint (Var i) z)"])
   apply (rule Foundation_lemma [THEN cut1], auto)
   done
 
 lemma Mem_Neg_refl: "{} \<turnstile> Neg (x IN x)"
 proof -
   obtain i::name where i: "atom i \<sharp> x"
     by (metis obtain_fresh)
   have "{} \<turnstile> Disjoint x (Eats Zero x)" 
     apply (rule cut_same [OF Foundation [where z = "Eats Zero x"]]) using i
     apply auto
     apply (rule cut_same [where A = "Disjoint x (Eats Zero x)"])    
     apply (metis Assume thin1 Disjoint_cong [OF Assume Refl, THEN Iff_MP_same])
     apply (metis Assume AssumeH(4) Disjoint_E Mem_Eats_I2 Refl) 
     done
   thus ?thesis 
     by (metis Disjoint_Eats_D2 Disjoint_commute cut_same)
 qed
 
 lemma Mem_refl_E [intro!]: "insert (x IN x) H \<turnstile> A"
   by (metis Disj_I1 Mem_Neg_refl anti_deduction thin0)
 
 lemma Mem_non_refl: assumes "H \<turnstile> x IN x" shows "H \<turnstile> A"
   by (metis Mem_refl_E assms cut_same)
 
 lemma Mem_Neg_sym: "{ x IN y, y IN x } \<turnstile> Fls"
 proof -
   obtain i::name where i: "atom i \<sharp> (x,y)"
     by (metis obtain_fresh)
   have "{} \<turnstile> Disjoint x (Eats Zero y) OR Disjoint y (Eats Zero x)" 
     apply (rule cut_same [OF Foundation [where i=i and z = "Eats (Eats Zero y) x"]]) using i
     apply (auto intro!: Disjoint_Eats_E2 [THEN rotate2])
     apply (rule Disj_I2, auto)
     apply (metis Assume EQ_imp_SUBS2 Subset_D insert_commute)
     apply (blast intro!: Disj_I1 Disjoint_cong [OF Hyp Refl, THEN Iff_MP_same])
     done
   thus ?thesis
     by (auto intro: cut0 Disjoint_Eats_E2)
 qed
 
 lemma Mem_not_sym: "insert (x IN y) (insert (y IN x) H) \<turnstile> A"
   by (rule cut_thin [OF Mem_Neg_sym]) auto
 
   
 section \<open>The Ordinal Property\<close>
 
 nominal_function OrdP :: "tm \<Rightarrow> fm"
   where "\<lbrakk>atom y \<sharp> (x, z); atom z \<sharp> x\<rbrakk> \<Longrightarrow>
     OrdP x = All2 y x ((Var y) SUBS x AND  All2 z (Var y) ((Var z) SUBS (Var y)))"
   by (auto simp: eqvt_def OrdP_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma
  shows OrdP_fresh_iff [simp]: "a \<sharp> OrdP x \<longleftrightarrow> a \<sharp> x"       (is ?thesis1)
    and eval_fm_OrdP [simp]:  "eval_fm e (OrdP x) \<longleftrightarrow> Ord \<lbrakk>x\<rbrakk>e"  (is ?thesis2)
 proof -
   obtain z::name and y::name where "atom z \<sharp> x" "atom y \<sharp> (x, z)"
     by (metis obtain_fresh)
   thus ?thesis1 ?thesis2
     by (auto simp: OrdP.simps [of y _ z] Ord_def Transset_def)
 qed
 
 lemma subst_fm_OrdP [simp]: "(OrdP t)(i::=x) = OrdP (subst i x t)"
 proof -
   obtain z::name and y::name where "atom z \<sharp> (t,i,x)" "atom y \<sharp> (t,i,x,z)"
     by (metis obtain_fresh)
   thus ?thesis
     by (auto simp: OrdP.simps [of y _ z])
 qed
 
 lemma OrdP_cong: "H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> OrdP x IFF OrdP x'"
   by (rule P1_cong) auto
 
 lemma OrdP_Mem_lemma:
   assumes z: "atom z \<sharp> (k,l)" and l: "insert (OrdP k) H \<turnstile> l IN k"
   shows "insert (OrdP k) H \<turnstile> l SUBS k AND All2 z l (Var z SUBS l)"
 proof -
   obtain y::name where y: "atom y \<sharp> (k,l,z)"
     by (metis obtain_fresh)
   have "insert (OrdP k) H 
         \<turnstile> (Var y IN k IMP (Var y SUBS k AND All2 z (Var y) (Var z SUBS Var y)))(y::=l)"
     by (rule All_D) (simp add: OrdP.simps [of y _ z] y z Assume) 
   also have "... = l IN k IMP (l SUBS k AND All2 z l (Var z SUBS l))" 
     using y z  by simp
   finally show ?thesis
     by (metis MP_same l) 
 qed
 
 lemma OrdP_Mem_E:
   assumes "atom z \<sharp> (k,l)" 
           "insert (OrdP k) H \<turnstile> l IN k"
           "insert (l SUBS k) (insert (All2 z l (Var z SUBS l)) H) \<turnstile> A"
   shows "insert (OrdP k) H \<turnstile> A" 
   apply (rule OrdP_Mem_lemma [THEN cut_same])
   apply (auto simp: insert_commute)
   apply (blast intro: assms thin1)+
   done
 
 lemma OrdP_Mem_imp_Subset:
   assumes k: "H \<turnstile> k IN l" and l: "H \<turnstile> OrdP l" shows "H \<turnstile> k SUBS l"
   apply (rule obtain_fresh [of "(l,k)"])
   apply (rule cut_same [OF l])
   using k  apply (auto intro: OrdP_Mem_E thin1)
   done
 
 lemma SUCC_Subset_Ord_lemma: "{ k' IN k, OrdP k } \<turnstile> SUCC k' SUBS k"
   by auto (metis Assume thin1 OrdP_Mem_imp_Subset)
 
 lemma SUCC_Subset_Ord: "H \<turnstile> k' IN k \<Longrightarrow> H \<turnstile> OrdP k \<Longrightarrow> H \<turnstile> SUCC k' SUBS k"
   by (blast intro!: cut2 [OF SUCC_Subset_Ord_lemma])
 
 lemma OrdP_Trans_lemma: "{ OrdP k, i IN j, j IN k } \<turnstile> i IN k"
 proof -
   obtain m::name where "atom m \<sharp> (i,j,k)"
     by (metis obtain_fresh) 
   thus ?thesis
     by (auto intro: OrdP_Mem_E [of m k j] Subset_D [THEN rotate3])
 qed
 
 lemma OrdP_Trans: "H \<turnstile>  OrdP k \<Longrightarrow> H \<turnstile> i IN j \<Longrightarrow> H \<turnstile> j IN k \<Longrightarrow> H  \<turnstile> i IN k"
   by (blast intro: cut3 [OF OrdP_Trans_lemma])
 
 lemma Ord_IN_Ord0:
   assumes l: "H \<turnstile> l IN k"
   shows "insert (OrdP k) H \<turnstile> OrdP l"
 proof -
   obtain z::name and y::name where z: "atom z \<sharp> (k,l)" and y: "atom y \<sharp> (k,l,z)"
     by (metis obtain_fresh)
   have "{Var y IN l, OrdP k, l IN k} \<turnstile> All2 z (Var y) (Var z SUBS Var y)"  using y z
     apply (simp add: insert_commute [of _ "OrdP k"]) 
     apply (auto intro: OrdP_Mem_E [of z k "Var y"] OrdP_Trans_lemma del: All_I Neg_I)
     done
   hence "{OrdP k, l IN k} \<turnstile> OrdP l" using z y
     apply (auto simp: OrdP.simps [of y l z])
     apply (simp add: insert_commute [of _ "OrdP k"]) 
     apply (rule OrdP_Mem_E [of y k l], simp_all)
     apply (metis Assume thin1)
     apply (rule All_E [where x= "Var y", THEN thin1], simp) 
     apply (metis Assume anti_deduction insert_commute) 
     done
   thus ?thesis
     by (metis (full_types) Assume l cut2 thin1) 
 qed
 
 lemma Ord_IN_Ord: "H \<turnstile> l IN k \<Longrightarrow> H \<turnstile> OrdP k \<Longrightarrow> H \<turnstile> OrdP l"
   by (metis Ord_IN_Ord0 cut_same)
 
 lemma OrdP_I:
   assumes "insert (Var y IN x) H \<turnstile> (Var y) SUBS x"
       and "insert (Var z IN Var y) (insert (Var y IN x) H) \<turnstile> (Var z) SUBS (Var y)"
       and "atom y \<sharp> (x, z)" "\<forall>B \<in> H. atom y \<sharp> B"  "atom z \<sharp> x" "\<forall>B \<in> H. atom z \<sharp> B"
     shows "H \<turnstile> OrdP x"
   using assms by auto
 
 lemma OrdP_Zero [simp]: "H \<turnstile> OrdP Zero"
 proof -
   obtain y::name and z::name where "atom y \<sharp> z"
     by (rule obtain_fresh)
   hence "{} \<turnstile> OrdP Zero"
     by (auto intro: OrdP_I [of y _ _ z])
   thus ?thesis 
     by (metis thin0)
 qed
 
 lemma OrdP_SUCC_I0: "{ OrdP k } \<turnstile> OrdP (SUCC k)"
 proof -
   obtain w::name and y::name and z::name where atoms: "atom w \<sharp> (k,y,z)" "atom y \<sharp> (k,z)" "atom z \<sharp> k"
     by (metis obtain_fresh)
   have 1: "{Var y IN SUCC k, OrdP k} \<turnstile> Var y SUBS SUCC k"
     apply (rule Mem_SUCC_E)
     apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate2]) using atoms
     apply auto
     apply (metis Assume Subset_SUCC Subset_trans)   
     apply (metis EQ_imp_SUBS Subset_SUCC Subset_trans)
     done
   have in_case: "{Var y IN k, Var z IN Var y, OrdP k} \<turnstile> Var z SUBS Var y"
     apply (rule OrdP_Mem_E [of w _ "Var y", THEN rotate3]) using atoms
     apply (auto intro:  All2_E [THEN thin1])
     done
   have "{Var y EQ k, Var z IN k, OrdP k} \<turnstile> Var z SUBS Var y"
     by (metis AssumeH(2) AssumeH(3) EQ_imp_SUBS2 OrdP_Mem_imp_Subset Subset_trans)
   hence eq_case: "{Var y EQ k, Var z IN Var y, OrdP k} \<turnstile> Var z SUBS Var y"
     by (rule cut3) (auto intro: EQ_imp_SUBS [THEN cut1] Subset_D)
   have 2: "{Var z IN Var y, Var y IN SUCC k, OrdP k} \<turnstile> Var z SUBS Var y"
     by (metis rotate2 Mem_SUCC_E in_case eq_case)   
   show ?thesis
-    apply (rule OrdP_I [OF 1 2]) 
-    using atoms apply auto 
-    done
+    using OrdP_I [OF 1 2] atoms
+    by (metis OrdP_fresh_iff SUCC_fresh_iff fresh_Pair singletonD)
 qed
 
 lemma OrdP_SUCC_I: "H \<turnstile> OrdP k \<Longrightarrow> H \<turnstile> OrdP (SUCC k)"
   by (metis OrdP_SUCC_I0 cut1)
 
 lemma Zero_In_OrdP: "{ OrdP x } \<turnstile> x EQ Zero OR Zero IN x"
 proof -
   obtain i::name and j::name
     where i: "atom i \<sharp> x" and j: "atom j \<sharp> (x,i)"
     by (metis obtain_fresh)
   show ?thesis
     apply (rule cut_thin [where HB = "{OrdP x}", OF Foundation [where i=i and z = x]])
     using i j apply auto
     prefer 2 apply (metis Assume Disj_I1)
     apply (rule Disj_I2)
     apply (rule cut_same [where A = "Var i EQ Zero"])
     prefer 2 apply (blast intro: Iff_MP_same [OF Mem_cong [OF Assume Refl]])
     apply (auto intro!: Eq_Zero_I [where i=j] Ex_I [where x="Var i"])
     apply (blast intro: Disjoint_E Subset_D)
     done
 qed
 
 lemma OrdP_HPairE: "insert (OrdP (HPair x y)) H \<turnstile> A"
 proof -
   have "{ OrdP (HPair x y) } \<turnstile> A"
     by (rule cut_same [OF Zero_In_OrdP]) (auto simp: HPair_def)
   thus ?thesis
     by (metis Assume cut1)
 qed
 
 lemmas OrdP_HPairEH = OrdP_HPairE OrdP_HPairE [THEN rotate2] OrdP_HPairE [THEN rotate3] OrdP_HPairE [THEN rotate4] OrdP_HPairE [THEN rotate5] 
                  OrdP_HPairE [THEN rotate6] OrdP_HPairE [THEN rotate7] OrdP_HPairE [THEN rotate8] OrdP_HPairE [THEN rotate9] OrdP_HPairE [THEN rotate10]
 declare OrdP_HPairEH [intro!]
 
 lemma Zero_Eq_HPairE: "insert (Zero EQ HPair x y) H \<turnstile> A"
   by (metis Eats_EQ_Zero_E2 HPair_def)
 
 lemmas Zero_Eq_HPairEH = Zero_Eq_HPairE Zero_Eq_HPairE [THEN rotate2] Zero_Eq_HPairE [THEN rotate3] Zero_Eq_HPairE [THEN rotate4] Zero_Eq_HPairE [THEN rotate5] 
                  Zero_Eq_HPairE [THEN rotate6] Zero_Eq_HPairE [THEN rotate7] Zero_Eq_HPairE [THEN rotate8] Zero_Eq_HPairE [THEN rotate9] Zero_Eq_HPairE [THEN rotate10]
 declare Zero_Eq_HPairEH [intro!]
 
 lemma HPair_Eq_ZeroE: "insert (HPair x y EQ Zero) H \<turnstile> A"
   by (metis Sym_L Zero_Eq_HPairE)
 
 lemmas HPair_Eq_ZeroEH = HPair_Eq_ZeroE HPair_Eq_ZeroE [THEN rotate2] HPair_Eq_ZeroE [THEN rotate3] HPair_Eq_ZeroE [THEN rotate4] HPair_Eq_ZeroE [THEN rotate5] 
                  HPair_Eq_ZeroE [THEN rotate6] HPair_Eq_ZeroE [THEN rotate7] HPair_Eq_ZeroE [THEN rotate8] HPair_Eq_ZeroE [THEN rotate9] HPair_Eq_ZeroE [THEN rotate10]
 declare HPair_Eq_ZeroEH [intro!]
 
 section \<open>Induction on Ordinals\<close>
 
 lemma OrdInd_lemma:
   assumes j: "atom (j::name) \<sharp> (i,A)"
   shows "{ OrdP (Var i) } \<turnstile> (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) IMP A"
 proof -
   obtain l::name and k::name
       where l: "atom l \<sharp> (i,j,A)" and k: "atom k \<sharp> (i,j,l,A)" 
       by (metis obtain_fresh)  
   have "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) } 
         \<turnstile> (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))"
     apply (rule Ind [of k]) 
     using j k l apply auto
     apply (rule All_E [where x="Var l", THEN rotate5], auto)
     apply (metis Assume Disj_I1 anti_deduction thin1)
     apply (rule Ex_I [where x="Var l"], auto)
     apply (rule All_E [where x="Var j", THEN rotate6], auto)
     apply (blast intro: ContraProve Iff_MP_same [OF Mem_cong [OF Refl]])
     apply (metis Assume Ord_IN_Ord0 ContraProve insert_commute)
     apply (metis Assume Neg_D thin1)+
     done
   hence "{ (All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A))) } 
           \<turnstile> (All2 l (Var i) (OrdP (Var l) IMP A(i::= Var l)))(i::= Eats Zero (Var i))"
     by (rule Subst, auto) 
   hence indlem: "{ All i (OrdP (Var i) IMP ((All2 j (Var i) (A(i::= Var j))) IMP A)) } 
              \<turnstile> All2 l (Eats Zero (Var i)) (OrdP (Var l) IMP A(i::=Var l))" 
     using j l by simp 
   show ?thesis
     apply (rule Imp_I)
     apply (rule cut_thin [OF indlem, where HB = "{OrdP (Var i)}"])
     apply (rule All2_Eats_E) using j l
     apply auto 
     done
 qed
 
 lemma OrdInd:
   assumes j: "atom (j::name) \<sharp> (i,A)"
   and x: "H \<turnstile> OrdP (Var i)" and step: "H \<turnstile> All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
   shows "H \<turnstile> A"
   apply (rule cut_thin [OF x, where HB=H])
   apply (rule MP_thin [OF OrdInd_lemma step])
   apply (auto simp: j)
   done
 
 lemma OrdIndH:
   assumes "atom (j::name) \<sharp> (i,A)"
       and "H \<turnstile> All i (OrdP (Var i) IMP (All2 j (Var i) (A(i::= Var j)) IMP A))"
     shows "insert (OrdP (Var i)) H \<turnstile> A"
   by (metis assms thin1 Assume OrdInd)
 
   
 section \<open>Linearity of Ordinals\<close>
 
 lemma OrdP_linear_lemma:
   assumes j: "atom j \<sharp> i"
   shows "{ OrdP (Var i) } \<turnstile> All j (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))"
          (is "_ \<turnstile> ?scheme")
 proof -
   obtain k::name and l::name and m::name
     where k: "atom k \<sharp> (i,j)" and l: "atom l \<sharp> (i,j,k)" and m: "atom m \<sharp> (i,j)"
     by (metis obtain_fresh) 
   show ?thesis
   proof (rule OrdIndH [where i=i and j=k])
     show "atom k \<sharp> (i, ?scheme)"
       using k  by (force simp add: fresh_Pair)  
   next
     show "{} \<turnstile> All i (OrdP (Var i) IMP (All2 k (Var i) (?scheme(i::= Var k)) IMP ?scheme))"
       using j k
       apply simp
       apply (rule All_I Imp_I)+
-      defer 1
-      apply auto [2]
+        defer 1
+        apply auto [2]
       apply (rule OrdIndH [where i=j and j=l]) using l
-      \<comment> \<open>nested induction\<close>
-      apply (force simp add: fresh_Pair)
+        \<comment> \<open>nested induction\<close>
+       apply (force simp add: fresh_Pair)
       apply simp
       apply (rule All_I Imp_I)+
-      prefer 2  apply force
+       prefer 2  apply force
       apply (rule Disj_3I)
       apply (rule Equality_I)
-      \<comment> \<open>Now the opposite inclusion, @{term"Var j SUBS Var i"}\<close>
+        \<comment> \<open>Now the opposite inclusion, @{term"Var j SUBS Var i"}\<close>
+       apply (rule Subset_I [where i=m])
+         apply (rule All2_E [THEN rotate4]) using l m
+           apply auto
+        apply (blast intro: ContraProve [THEN rotate3] OrdP_Trans)
+       apply (blast intro: ContraProve [THEN rotate3] Mem_cong [OF Hyp Refl, THEN Iff_MP2_same])
+        \<comment> \<open>Now the opposite inclusion, @{term"Var i SUBS Var j"}\<close>
       apply (rule Subset_I [where i=m])
-      apply (rule All2_E [THEN rotate4]) using l m
-      apply auto
-      apply (blast intro: ContraProve [THEN rotate3] OrdP_Trans)
-      apply (blast intro: ContraProve [THEN rotate3] Mem_cong [OF Hyp Refl, THEN Iff_MP2_same])
-      \<comment> \<open>Now the opposite inclusion, @{term"Var i SUBS Var j"}\<close>
-      apply (rule Subset_I [where i=m])
-      apply (rule All2_E [THEN rotate6], auto) 
+        apply (rule All2_E [THEN rotate6], auto) 
       apply (rule All_E [where x = "Var j"], auto) 
-      apply (blast intro: ContraProve [THEN rotate4] Mem_cong [OF Hyp Refl, THEN Iff_MP_same])
+       apply (blast intro: ContraProve [THEN rotate4] Mem_cong [OF Hyp Refl, THEN Iff_MP_same])
       apply (blast intro: ContraProve [THEN rotate4] OrdP_Trans)
       done
   qed
 qed
 
 lemma OrdP_linear_imp: "{} \<turnstile> OrdP x IMP OrdP y IMP x IN y OR x EQ y OR y IN x"
 proof -
   obtain i::name and j::name
     where atoms: "atom i \<sharp> (x,y)" "atom j \<sharp> (x,y,i)" 
     by (metis obtain_fresh) 
   have "{ OrdP (Var i) } \<turnstile> (OrdP (Var j) IMP (Var i IN Var j OR Var i EQ Var j OR Var j IN Var i))(j::=y)"
     using atoms  by (metis All_D OrdP_linear_lemma fresh_Pair)
   hence "{} \<turnstile> OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i)"
     using atoms by auto
   hence "{} \<turnstile> (OrdP (Var i) IMP OrdP y IMP (Var i IN y OR Var i EQ y OR y IN Var i))(i::=x)"
     by (metis Subst empty_iff)
   thus ?thesis
     using atoms by auto
 qed
   
 lemma OrdP_linear:
   assumes "H \<turnstile> OrdP x" "H \<turnstile> OrdP y" 
           "insert (x IN y) H \<turnstile> A" "insert (x EQ y) H \<turnstile> A" "insert (y IN x) H \<turnstile> A" 
     shows "H \<turnstile> A"
 proof -
   have "{ OrdP x, OrdP y } \<turnstile> x IN y OR x EQ y OR y IN x"
     by (metis OrdP_linear_imp Imp_Imp_commute anti_deduction)
   thus ?thesis    
     using assms  by (metis cut2 Disj_E cut_same)
 qed
 
 lemma Zero_In_SUCC: "{OrdP k} \<turnstile> Zero IN SUCC k"
   by (rule OrdP_linear [OF OrdP_Zero OrdP_SUCC_I]) (force simp: SUCC_def)+
 
 
 section \<open>The predicate \<open>OrdNotEqP\<close>\<close>
 
 nominal_function OrdNotEqP :: "tm \<Rightarrow> tm \<Rightarrow> fm"  (infixr "NEQ" 150)
   where "OrdNotEqP x y = OrdP x AND OrdP y AND (x IN y OR y IN x)"
   by (auto simp: eqvt_def OrdNotEqP_graph_aux_def)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma OrdNotEqP_fresh_iff [simp]: "a \<sharp> OrdNotEqP x y \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"
   by auto
 
 lemma eval_fm_OrdNotEqP [simp]: "eval_fm e (OrdNotEqP x y) \<longleftrightarrow> Ord \<lbrakk>x\<rbrakk>e \<and> Ord \<lbrakk>y\<rbrakk>e \<and> \<lbrakk>x\<rbrakk>e \<noteq> \<lbrakk>y\<rbrakk>e"
   by (auto simp: hmem_not_refl) (metis Ord_linear)
 
 lemma OrdNotEqP_subst [simp]: "(OrdNotEqP x y)(i::=t) = OrdNotEqP (subst i t x) (subst i t y)"
   by simp
 
 lemma OrdNotEqP_cong: "H \<turnstile> x EQ x' \<Longrightarrow> H \<turnstile> y EQ y' \<Longrightarrow> H \<turnstile> OrdNotEqP x y IFF OrdNotEqP x' y'"
   by (rule P2_cong) auto
 
 lemma OrdNotEqP_self_contra: "{x NEQ x} \<turnstile> Fls"
   by auto
 
 lemma OrdNotEqP_OrdP_E: "insert (OrdP x) (insert (OrdP y) H) \<turnstile> A \<Longrightarrow> insert (x NEQ y) H \<turnstile> A"
   by (auto intro: thin1 rotate2)
 
 lemma OrdNotEqP_I: "insert (x EQ y) H \<turnstile> Fls \<Longrightarrow> H \<turnstile> OrdP x \<Longrightarrow> H \<turnstile> OrdP y \<Longrightarrow> H \<turnstile> x NEQ y"
   by (rule OrdP_linear [of _ x y]) (auto intro: ExFalso thin1 Disj_I1 Disj_I2)
 
 declare OrdNotEqP.simps [simp del]
 
 lemma OrdNotEqP_imp_Neg_Eq: "{x NEQ y} \<turnstile> Neg (x EQ y)"
   by (blast intro: OrdNotEqP_cong [THEN Iff_MP2_same]  OrdNotEqP_self_contra [of x, THEN cut1])
 
 lemma OrdNotEqP_E: "H \<turnstile> x EQ y \<Longrightarrow> insert (x NEQ y) H \<turnstile> A"
   by (metis ContraProve OrdNotEqP_imp_Neg_Eq rcut1)
 
   
 section \<open>Predecessor of an Ordinal\<close>
 
 lemma OrdP_set_max_lemma:
   assumes j: "atom (j::name) \<sharp> i" and k: "atom (k::name) \<sharp> (i,j)"
   shows "{} \<turnstile> (Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP 
               (Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j))))"
 proof -
   obtain l::name where l: "atom l \<sharp> (i,j,k)" 
     by (metis obtain_fresh) 
   show ?thesis
     apply (rule Ind [of l i]) using j k l 
       apply simp_all
      apply (metis Conj_E Refl Swap Imp_I)
     apply (rule All_I Imp_I)+  
       apply simp_all
     apply clarify
     apply (rule thin1)
     apply (rule thin1 [THEN rotate2])
     apply (rule Disj_EH)
      apply (rule Neg_Conj_E)
       apply (auto simp: All2_Eats_E1)   
      apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
       apply (metis Assume Eq_Zero_D rotate3)
      apply (metis Assume EQ_imp_SUBS Neg_D thin1)
     apply (rule Cases [where A = "Var j IN Var l"])
-    apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
-    apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
-    apply (rule Ex_I [where x="Var k"], auto)
-    apply (metis Assume Subset_trans OrdP_Mem_imp_Subset thin1)
-    apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
-    apply (metis ContraProve EQ_imp_SUBS rotate3)
-    \<comment> \<open>final case\<close>
+     apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2)
+      apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
+      apply (rule Ex_I [where x="Var k"], auto)
+      apply (metis Assume Subset_trans OrdP_Mem_imp_Subset thin1)
+     apply (rule Ex_I [where x="Var l"], auto intro: Mem_Eats_I2 ContraProve)
+     apply (metis ContraProve EQ_imp_SUBS rotate3)
+      \<comment> \<open>final case\<close>
     apply (rule All2_Eats_E [THEN rotate4], simp_all)
     apply (rule Ex_I [where x="Var j"], auto intro: Mem_Eats_I1)
-    apply (rule All2_E [where x = "Var k", THEN rotate3], auto)
-    apply (rule Ex_I [where x="Var k"], simp)
-    apply (metis Assume NegNeg_I Neg_Disj_I rotate3)
+     apply (rule All2_E [where x = "Var k", THEN rotate3], auto)
+     apply (rule Ex_I [where x="Var k"], simp)
+     apply (metis Assume NegNeg_I Neg_Disj_I rotate3)
     apply (rule cut_same [where A = "OrdP (Var j)"])
-    apply (rule All2_E [where x = "Var j", THEN rotate3], auto)
+     apply (rule All2_E [where x = "Var j", THEN rotate3], auto)
     apply (rule cut_same [where A = "Var l EQ Var j OR Var l IN Var j"])
-    apply (rule OrdP_linear [of _ "Var l" "Var j"], auto intro: Disj_CI)
-    apply (metis Assume ContraProve rotate7)
-    apply (metis ContraProve [THEN rotate4] EQ_imp_SUBS Subset_trans rotate3)
+     apply (rule OrdP_linear [of _ "Var l" "Var j"], auto intro: Disj_CI)
+      apply (metis Assume ContraProve rotate7)
+     apply (metis ContraProve [THEN rotate4] EQ_imp_SUBS Subset_trans rotate3)
     apply (blast intro: ContraProve [THEN rotate4] OrdP_Mem_imp_Subset Iff_MP2_same [OF Mem_cong])
     done
 qed
 
 lemma OrdP_max_imp:
   assumes j: "atom j \<sharp> (x)" and k: "atom k \<sharp> (x,j)"
   shows  "{ OrdP x, Neg (x EQ Zero) } \<turnstile> Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
 proof -
   obtain i::name where i: "atom i \<sharp> (x,j,k)" 
     by (metis obtain_fresh) 
   have "{} \<turnstile> ((Neg (Var i EQ Zero) AND (All2 j (Var i) (OrdP (Var j)))) IMP 
               (Ex j (Var j IN Var i AND (All2 k (Var i) (Var k SUBS Var j)))))(i::=x)"
     apply (rule Subst [OF OrdP_set_max_lemma])
     using i k apply auto
     done
   hence "{ Neg (x EQ Zero) AND (All2 j x (OrdP (Var j))) } 
          \<turnstile> Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
    using i j k by simp (metis anti_deduction)
   hence "{ All2 j x (OrdP (Var j)), Neg (x EQ Zero) } 
              \<turnstile> Ex j (Var j IN x AND (All2 k x (Var k SUBS Var j)))"
     by (rule cut1) (metis Assume Conj_I thin1)
   moreover have "{ OrdP x } \<turnstile> All2 j x (OrdP (Var j))" using j
     by auto (metis Assume Ord_IN_Ord thin1)
   ultimately show ?thesis
    by (metis rcut1)
 qed
 
 declare OrdP.simps [simp del]
 
 
 section \<open>Case Analysis and Zero/SUCC Induction\<close>
 
 lemma OrdP_cases_lemma:
   assumes p: "atom p \<sharp> x" 
   shows  "{ OrdP x, Neg (x EQ Zero) } \<turnstile> Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
 proof -
   obtain j::name and k::name where j: "atom j \<sharp> (x,p)" and k: "atom k \<sharp> (x,j,p)" 
     by (metis obtain_fresh) 
   show ?thesis
     apply (rule cut_same [OF OrdP_max_imp [of j x k]]) 
     using p j k apply auto
     apply (rule Ex_I [where x="Var j"], auto)
      apply (metis Assume Ord_IN_Ord thin1)
     apply (rule cut_same [where A = "OrdP (SUCC (Var j))"])
     apply (metis Assume Ord_IN_Ord0 OrdP_SUCC_I rotate2 thin1)
     apply (rule OrdP_linear [where x = x, OF _ Assume], auto intro!: Mem_SUCC_EH)
     apply (metis Mem_not_sym rotate3) 
     apply (rule Mem_non_refl, blast intro: Mem_cong [OF Assume Refl, THEN Iff_MP2_same])
     apply (force intro: thin1 All2_E [where x = "SUCC (Var j)", THEN rotate4])
     done
 qed
 
 lemma OrdP_cases_disj:
   assumes p: "atom p \<sharp> x" 
   shows  "insert (OrdP x) H \<turnstile> x EQ Zero OR Ex p (OrdP (Var p) AND x EQ SUCC (Var p))"
   by (metis Disj_CI Assume cut2 [OF OrdP_cases_lemma [OF p]] Swap thin1)
 
 lemma OrdP_cases_E:
   "\<lbrakk>insert (x EQ Zero) H \<turnstile> A;
     insert (x EQ SUCC (Var k)) (insert (OrdP (Var k)) H) \<turnstile> A; 
     atom k \<sharp> (x,A);   \<forall>C \<in> H. atom k \<sharp> C\<rbrakk>
    \<Longrightarrow> insert (OrdP x) H \<turnstile> A"
   by (rule cut_same [OF OrdP_cases_disj [of k]]) (auto simp: insert_commute intro: thin1)
 
 lemma OrdInd2_lemma:
   "{ OrdP (Var i), A(i::= Zero), (All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))) } \<turnstile> A"
 proof -
   obtain j::name and k::name  where atoms: "atom j \<sharp> (i,A)" "atom k \<sharp> (i,j,A)" 
     by (metis obtain_fresh) 
   show ?thesis
-  apply (rule OrdIndH [where i=i and j=j]) 
-  using atoms  apply auto
-  apply (rule OrdP_cases_E [where k=k, THEN rotate3])
-  apply (rule ContraProve [THEN rotate2]) using Var_Eq_imp_subst_Iff
-  apply (metis Assume AssumeH(3) Iff_MP_same) 
-  apply (rule Ex_I [where x="Var k"], simp)
-  apply (rule Neg_Imp_I, blast)
-  apply (rule cut_same [where A = "A(i::=Var k)"])
-  apply (rule All2_E [where x = "Var k", THEN rotate5])
-  apply (auto intro: Mem_SUCC_I2 Mem_cong [OF Refl, THEN Iff_MP2_same])
-  apply (rule ContraProve [THEN rotate5])
-  by (metis Assume Iff_MP_left' Var_Eq_subst_Iff thin1)
+    apply (rule OrdIndH [where i=i and j=j]) 
+    using atoms  apply auto
+    apply (rule OrdP_cases_E [where k=k, THEN rotate3])
+       apply (rule ContraProve [THEN rotate2]) using Var_Eq_imp_subst_Iff
+       apply (metis Assume AssumeH(3) Iff_MP_same) 
+      apply (rule Ex_I [where x="Var k"], simp)
+      apply (rule Neg_Imp_I, blast)
+      apply (rule cut_same [where A = "A(i::=Var k)"])
+       apply (rule All2_E [where x = "Var k", THEN rotate5])
+         apply (auto intro: Mem_SUCC_I2 Mem_cong [OF Refl, THEN Iff_MP2_same])
+    apply (rule ContraProve [THEN rotate5])
+    by (metis Assume Iff_MP_left' Var_Eq_subst_Iff thin1)
 qed
 
 lemma OrdInd2:
   assumes "H \<turnstile> OrdP (Var i)"
       and "H \<turnstile> A(i::= Zero)"
       and "H \<turnstile> All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
     shows "H \<turnstile> A"
   by (metis cut3 [OF OrdInd2_lemma] assms)
 
 lemma OrdInd2H:
   assumes "H \<turnstile> A(i::= Zero)"
       and "H \<turnstile> All i (OrdP (Var i) IMP A IMP (A(i::= SUCC (Var i))))"
     shows "insert (OrdP (Var i)) H \<turnstile> A"
   by (metis assms thin1 Assume OrdInd2)
 
 
 section \<open>The predicate \<open>HFun_Sigma\<close>\<close>
 
 text\<open>To characterise the concept of a function using only bounded universal quantifiers.\<close>
 
 text\<open>See the note after the proof of Lemma 2.3.\<close>
 
 definition hfun_sigma where
  "hfun_sigma r \<equiv> \<forall>z \<^bold>\<in> r. \<forall>z' \<^bold>\<in> r. \<exists>x y x' y'. z = \<langle>x,y\<rangle> \<and> z' = \<langle>x',y'\<rangle> \<and> (x=x' \<longrightarrow> y=y')"
 
 definition hfun_sigma_ord where
  "hfun_sigma_ord r \<equiv> \<forall>z \<^bold>\<in> r. \<forall>z' \<^bold>\<in> r. \<exists>x y x' y'. z = \<langle>x,y\<rangle> \<and> z' = \<langle>x',y'\<rangle> \<and> Ord x \<and> Ord x' \<and> (x=x' \<longrightarrow> y=y')"
 
 nominal_function HFun_Sigma :: "tm \<Rightarrow> fm"
   where "\<lbrakk>atom z \<sharp> (r,z',x,y,x',y'); atom z' \<sharp> (r,x,y,x',y'); 
           atom x \<sharp> (r,y,x',y'); atom y \<sharp> (r,x',y'); atom x' \<sharp> (r,y'); atom y' \<sharp> (r) \<rbrakk> \<Longrightarrow>
     HFun_Sigma r = 
          All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
              (Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
               AND OrdP (Var x) AND OrdP (Var x') AND 
               ((Var x EQ Var x') IMP (Var y EQ Var y'))))))))"
 by (auto simp: eqvt_def HFun_Sigma_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma
   shows HFun_Sigma_fresh_iff [simp]: "a \<sharp> HFun_Sigma r \<longleftrightarrow> a \<sharp> r" (is ?thesis1)
     and eval_fm_HFun_Sigma [simp]:
          "eval_fm e (HFun_Sigma r) \<longleftrightarrow> hfun_sigma_ord \<lbrakk>r\<rbrakk>e" (is ?thesis2)
 proof -
   obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
     where "atom z \<sharp> (r,z',x,y,x',y')"  "atom z' \<sharp> (r,x,y,x',y')"
           "atom x \<sharp> (r,y,x',y')"  "atom y \<sharp> (r,x',y')" 
           "atom x' \<sharp> (r,y')"  "atom y' \<sharp> (r)"
     by (metis obtain_fresh) 
   thus ?thesis1 ?thesis2
     by (auto simp: HBall_def hfun_sigma_ord_def, metis+)
 qed
 
 lemma HFun_Sigma_subst [simp]: "(HFun_Sigma r)(i::=t) = HFun_Sigma (subst i t r)"
 proof -
   obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
     where "atom z \<sharp> (r,t,i,z',x,y,x',y')" "atom z' \<sharp> (r,t,i,x,y,x',y')"
           "atom x \<sharp> (r,t,i,y,x',y')" "atom y \<sharp> (r,t,i,x',y')" 
           "atom x' \<sharp> (r,t,i,y')" "atom y' \<sharp> (r,t,i)"
     by (metis obtain_fresh) 
   thus ?thesis 
     by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
 qed
 
 lemma HFun_Sigma_Zero: "H \<turnstile> HFun_Sigma Zero"
 proof -
   obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
     where "atom z'' \<sharp> (z,z',x,y,x',y')" "atom z \<sharp> (z',x,y,x',y')" "atom z' \<sharp> (x,y,x',y')"
       "atom x \<sharp> (y,x',y')" "atom y \<sharp> (x',y')" "atom x' \<sharp> y'" 
     by (metis obtain_fresh) 
   hence "{} \<turnstile> HFun_Sigma Zero"
     by (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
   thus ?thesis
     by (metis thin0)
 qed
 
 lemma Subset_HFun_Sigma: "{HFun_Sigma s, s' SUBS s} \<turnstile> HFun_Sigma s'"
 proof -
   obtain x::name and y::name and z::name and x'::name and y'::name and z'::name and z''::name
     where "atom z'' \<sharp> (z,z',x,y,x',y',s,s')" 
       "atom z \<sharp> (z',x,y,x',y',s,s')" "atom z' \<sharp> (x,y,x',y',s,s')"
       "atom x \<sharp> (y,x',y',s,s')" "atom y \<sharp> (x',y',s,s')" 
       "atom x' \<sharp> (y',s,s')" "atom y' \<sharp> (s,s')" 
     by (metis obtain_fresh) 
   thus ?thesis
     apply (auto simp: HFun_Sigma.simps [of z _ z' x y x' y'])
     apply (rule Ex_I [where x="Var z"], auto)
     apply (blast intro: Subset_D ContraProve)
     apply (rule All_E [where x="Var z'"], auto intro: Subset_D ContraProve)
     done
 qed
 
 text\<open>Captures the property of being a relation, using fewer variables than the full definition\<close>
 lemma HFun_Sigma_Mem_imp_HPair:
   assumes "H \<turnstile> HFun_Sigma r" "H \<turnstile> a IN r"
       and xy: "atom x \<sharp> (y,a,r)" "atom y \<sharp> (a,r)"
     shows "H \<turnstile> (Ex x (Ex y (a EQ HPair (Var x) (Var y))))"  (is "_ \<turnstile> ?concl")
 proof -
   obtain x'::name and y'::name and z::name and z'::name
     where atoms: "atom z \<sharp> (z',x',y',x,y,a,r)" "atom z' \<sharp> (x',y',x,y,a,r)"
                  "atom x' \<sharp> (y',x,y,a,r)" "atom y' \<sharp> (x,y,a,r)" 
     by (metis obtain_fresh) 
   hence "{HFun_Sigma r, a IN r} \<turnstile> ?concl" using xy
     apply (auto simp: HFun_Sigma.simps [of z r z' x y x' y'])
     apply (rule All_E [where x=a], auto)
     apply (rule All_E [where x=a], simp)
     apply (rule Imp_E, blast)
-    apply (rule Ex_EH Conj_EH)+
-    apply simp_all
+    apply (rule Ex_EH Conj_EH)+ apply simp_all
     apply (rule Ex_I [where x="Var x"], simp)
     apply (rule Ex_I [where x="Var y"], auto)
     done
   thus ?thesis
     by (rule cut2) (rule assms)+ 
 qed
 
     
 section \<open>The predicate \<open>HDomain_Incl\<close>\<close>
 
 text \<open>This is an internal version of @{term "\<forall>x \<^bold>\<in> d. \<exists>y z. z \<^bold>\<in> r \<and> z = \<langle>x,y\<rangle>"}.\<close>
 
 nominal_function HDomain_Incl :: "tm \<Rightarrow> tm \<Rightarrow> fm"
   where "\<lbrakk>atom x \<sharp> (r,d,y,z); atom y \<sharp> (r,d,z); atom z \<sharp> (r,d)\<rbrakk> \<Longrightarrow>
     HDomain_Incl r d = All2 x d (Ex y (Ex z (Var z IN r AND Var z EQ HPair (Var x) (Var y))))"
   by (auto simp: eqvt_def HDomain_Incl_graph_aux_def flip_fresh_fresh) (metis obtain_fresh)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma
   shows HDomain_Incl_fresh_iff [simp]:
       "a \<sharp> HDomain_Incl r d \<longleftrightarrow> a \<sharp> r \<and> a \<sharp> d" (is ?thesis1)
   and   eval_fm_HDomain_Incl [simp]:
       "eval_fm e (HDomain_Incl r d) \<longleftrightarrow> \<lbrakk>d\<rbrakk>e \<le> hdomain \<lbrakk>r\<rbrakk>e" (is ?thesis2)
 proof -
   obtain x::name and y::name and z::name 
     where "atom x \<sharp> (r,d,y,z)" "atom y \<sharp> (r,d,z)" "atom z \<sharp> (r,d)"
     by (metis obtain_fresh) 
   thus ?thesis1 ?thesis2
     by (auto simp: HDomain_Incl.simps [of x _ _ y z] hdomain_def)
 qed
 
 lemma HDomain_Incl_subst [simp]:
       "(HDomain_Incl r d)(i::=t) = HDomain_Incl (subst i t r) (subst i t d)"
 proof -
   obtain x::name and y::name and z::name 
     where "atom x \<sharp> (r,d,y,z,t,i)"  "atom y \<sharp> (r,d,z,t,i)" "atom z \<sharp> (r,d,t,i)"
     by (metis obtain_fresh) 
   thus ?thesis
     by (auto simp: HDomain_Incl.simps [of x _ _ y z])
 qed
 
 lemma HDomain_Incl_Subset_lemma: "{ HDomain_Incl r k, k' SUBS k } \<turnstile> HDomain_Incl r k'"
 proof -
   obtain x::name and y::name and z::name 
     where "atom x \<sharp> (r,k,k',y,z)" "atom y \<sharp> (r,k,k',z)" "atom z \<sharp> (r,k,k')"
     by (metis obtain_fresh) 
   thus ?thesis
     apply (simp add: HDomain_Incl.simps [of x _ _ y z], auto)
     apply (rule Ex_I [where x = "Var x"], auto intro: ContraProve Subset_D)
     done
 qed
 
 lemma HDomain_Incl_Subset: "H \<turnstile> HDomain_Incl r k \<Longrightarrow> H \<turnstile> k' SUBS k \<Longrightarrow> H \<turnstile> HDomain_Incl r k'"
   by (metis HDomain_Incl_Subset_lemma cut2)
 
 lemma HDomain_Incl_Mem_Ord: "H \<turnstile> HDomain_Incl r k \<Longrightarrow> H \<turnstile> k' IN k \<Longrightarrow> H \<turnstile> OrdP k \<Longrightarrow> H \<turnstile> HDomain_Incl r k'"
   by (metis HDomain_Incl_Subset OrdP_Mem_imp_Subset)
 
 lemma HDomain_Incl_Zero [simp]: "H \<turnstile> HDomain_Incl r Zero"
 proof -
   obtain x::name and y::name and z::name 
     where "atom x \<sharp> (r,y,z)" "atom y \<sharp> (r,z)" "atom z \<sharp> r"
     by (metis obtain_fresh) 
   hence "{} \<turnstile> HDomain_Incl r Zero"
     by (auto simp: HDomain_Incl.simps [of x _ _ y z])
   thus ?thesis
     by (metis thin0)
 qed
 
 lemma HDomain_Incl_Eats: "{ HDomain_Incl r d } \<turnstile> HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
 proof -
   obtain x::name and y::name and z::name 
     where x: "atom x \<sharp> (r,d,d',y,z)" and y: "atom y \<sharp> (r,d,d',z)" and z: "atom z \<sharp> (r,d,d')"
     by (metis obtain_fresh) 
   thus ?thesis
     apply (auto simp: HDomain_Incl.simps [of x _ _ y z] intro!: Mem_SUCC_EH)
     apply (rule Ex_I [where x = "Var x"], auto)
     apply (rule Ex_I [where x = "Var y"], auto)
     apply (rule Ex_I [where x = "Var z"], auto intro: Mem_Eats_I1)
     apply (rule rotate2 [OF Swap])
     apply (rule Ex_I [where x = d'], auto)
     apply (rule Ex_I [where x = "HPair d d'"], auto intro: Mem_Eats_I2 HPair_cong Sym)
     done
 qed
 
 lemma HDomain_Incl_Eats_I: "H \<turnstile> HDomain_Incl r d \<Longrightarrow> H \<turnstile> HDomain_Incl (Eats r (HPair d d')) (SUCC d)"
   by (metis HDomain_Incl_Eats cut1)
 
 
 section \<open>@{term HPair} is Provably Injective\<close>
 
 lemma Doubleton_E:
   assumes "insert (a EQ c) (insert (b EQ d) H) \<turnstile> A"
           "insert (a EQ d) (insert (b EQ c) H) \<turnstile> A"
     shows    "insert ((Eats (Eats Zero b) a) EQ (Eats (Eats Zero d) c)) H \<turnstile> A"
 apply (rule Equality_E) using assms
 apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
 apply (rule_tac [!] rotate3) 
 apply (auto intro!: Zero_SubsetE rotate2 [of "a IN b"])
 apply (metis Sym_L insert_commute thin1)+
 done
   
 lemma HFST: "{HPair a b EQ HPair c d} \<turnstile> a EQ c"
   unfolding HPair_def  by (metis Assume Doubleton_E thin1)
 
 lemma b_EQ_d_1: "{a EQ c, a EQ d, b EQ c} \<turnstile> b EQ d"
   by (metis Assume thin1 Sym Trans)
 
 lemma HSND: "{HPair a b EQ HPair c d} \<turnstile> b EQ d"
   unfolding HPair_def
   by (metis  AssumeH(2) Doubleton_E b_EQ_d_1 rotate3 thin2) 
 
 lemma HPair_E [intro!]:
   assumes "insert (a EQ c) (insert (b EQ d) H) \<turnstile> A"
     shows "insert (HPair a b EQ HPair c d) H \<turnstile> A"
   by (metis Conj_E [OF assms] Conj_I [OF HFST HSND] rcut1)
 
 declare HPair_E [THEN rotate2, intro!]
 declare HPair_E [THEN rotate3, intro!]
 declare HPair_E [THEN rotate4, intro!]
 declare HPair_E [THEN rotate5, intro!]
 declare HPair_E [THEN rotate6, intro!]
 declare HPair_E [THEN rotate7, intro!]
 declare HPair_E [THEN rotate8, intro!]
 
 lemma HFun_Sigma_E:
   assumes r: "H \<turnstile> HFun_Sigma r"
       and b: "H \<turnstile> HPair a b IN r"
       and b': "H \<turnstile> HPair a b' IN r"
     shows "H \<turnstile> b EQ b'"
 proof -
   obtain x::name and y::name and z::name and x'::name and y'::name and z'::name
     where atoms: "atom z \<sharp> (r,a,b,b',z',x,y,x',y')"  "atom z' \<sharp> (r,a,b,b',x,y,x',y')"
        "atom x \<sharp> (r,a,b,b',y,x',y')"  "atom y \<sharp> (r,a,b,b',x',y')" 
        "atom x' \<sharp> (r,a,b,b',y')"  "atom y' \<sharp> (r,a,b,b')"
     by (metis obtain_fresh) 
   hence d1: "H \<turnstile> All2 z r (All2 z' r (Ex x (Ex y (Ex x' (Ex y'
                   (Var z EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
                    AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))))" 
       using r HFun_Sigma.simps [of z r z' x y x' y']
     by simp 
   have d2: "H \<turnstile> All2 z' r (Ex x (Ex y (Ex x' (Ex y'
              (HPair a b EQ HPair (Var x) (Var y) AND Var z' EQ HPair (Var x') (Var y')
                    AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))))" 
     using All_D [where x = "HPair a b", OF d1]  atoms
     by simp (metis MP_same b)              
   have d4: "H \<turnstile> Ex x (Ex y (Ex x' (Ex y'
              (HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
                AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y'))))))"
     using All_D [where x = "HPair a b'", OF d2]  atoms
     by simp (metis MP_same b')              
   have d': "{ Ex x (Ex y (Ex x' (Ex y'
              (HPair a b EQ HPair (Var x) (Var y) AND HPair a b' EQ HPair (Var x') (Var y')
               AND OrdP (Var x) AND OrdP (Var x') AND ((Var x EQ Var x') IMP (Var y EQ Var y')))))) } \<turnstile> b EQ b'" 
      using atoms
      by (auto intro: ContraProve Trans Sym)
   thus ?thesis 
     by (rule cut_thin [OF d4], auto)
 qed
 
 
 section \<open>@{term SUCC} is Provably Injective\<close>
 
 lemma SUCC_SUBS_lemma: "{SUCC x SUBS SUCC y} \<turnstile> x SUBS y"
   apply (rule obtain_fresh [where x="(x,y)"]) 
   apply (auto simp: SUCC_def)
   prefer 2  apply (metis Assume Conj_E1 Extensionality Iff_MP_same)
   apply (auto intro!: Subset_I)
   apply (blast intro: Set_MP cut_same [OF Mem_cong [OF Refl Assume, THEN Iff_MP2_same]] 
             Mem_not_sym thin2)
   done
 
 lemma SUCC_SUBS: "insert (SUCC x SUBS SUCC y) H \<turnstile> x SUBS y"
   by (metis Assume SUCC_SUBS_lemma cut1)
 
 lemma SUCC_inject: "insert (SUCC x EQ SUCC y) H \<turnstile> x EQ y"
   by (metis Equality_I EQ_imp_SUBS SUCC_SUBS Sym_L cut1)
 
 lemma SUCC_inject_E [intro!]: "insert (x EQ y) H \<turnstile> A \<Longrightarrow> insert (SUCC x EQ SUCC y) H \<turnstile> A"
   by (metis SUCC_inject cut_same insert_commute thin1)
 
 declare SUCC_inject_E [THEN rotate2, intro!]
 declare SUCC_inject_E [THEN rotate3, intro!]
 declare SUCC_inject_E [THEN rotate4, intro!]
 declare SUCC_inject_E [THEN rotate5, intro!]
 declare SUCC_inject_E [THEN rotate6, intro!]
 declare SUCC_inject_E [THEN rotate7, intro!]
 declare SUCC_inject_E [THEN rotate8, intro!]
 
 lemma OrdP_IN_SUCC_lemma: "{OrdP x, y IN x} \<turnstile> SUCC y IN SUCC x"
   apply (rule OrdP_linear [of _ "SUCC x" "SUCC y"])
-  apply (auto intro!: Mem_SUCC_EH  intro: OrdP_SUCC_I Ord_IN_Ord0)
-  apply (metis Hyp Mem_SUCC_I1 Mem_not_sym cut_same insertCI)
-  apply (metis Assume EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D thin1) 
+      apply (auto intro!: Mem_SUCC_EH  intro: OrdP_SUCC_I Ord_IN_Ord0)
+    apply (metis Hyp Mem_SUCC_I1 Mem_not_sym cut_same insertCI)
+   apply (metis Assume EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D thin1) 
   apply (blast intro: cut_same [OF Mem_cong [THEN Iff_MP2_same]])
   done
 
 lemma OrdP_IN_SUCC: "H \<turnstile> OrdP x \<Longrightarrow> H \<turnstile> y IN x \<Longrightarrow> H \<turnstile> SUCC y IN SUCC x"
   by (rule cut2 [OF OrdP_IN_SUCC_lemma])
 
 lemma OrdP_IN_SUCC_D_lemma: "{OrdP x, SUCC y IN SUCC x} \<turnstile> y IN x"
   apply (rule OrdP_linear [of _ "x" "y"], auto)
-  apply (metis Assume AssumeH(2) Mem_SUCC_Refl OrdP_SUCC_I Ord_IN_Ord)
-  apply (rule Mem_SUCC_E [THEN rotate3])
-  apply (blast intro: Mem_SUCC_Refl OrdP_Trans) 
-  apply (metis AssumeH(2) EQ_imp_SUBS Mem_SUCC_I1 Mem_non_refl Subset_D)
-  apply (metis EQ_imp_SUBS Mem_SUCC_I2 Mem_SUCC_EH(2) Mem_SUCC_I1 Refl SUCC_Subset_Ord_lemma Subset_D thin1)  
-  done
+    apply (metis Assume AssumeH(2) Mem_SUCC_Refl OrdP_SUCC_I Ord_IN_Ord)
+   apply (metis Assume EQ_imp_SUBS Mem_Eats_EH(2) Mem_SUCC_Refl OrdP_Mem_imp_Subset SUCC_def Subset_D thin1)
+  by (meson Assume EQ_imp_SUBS Mem_SUCC_E Mem_SUCC_Refl OrdP_Mem_imp_Subset Subset_D rotate3)
 
 lemma OrdP_IN_SUCC_D: "H \<turnstile> OrdP x \<Longrightarrow> H \<turnstile> SUCC y IN SUCC x \<Longrightarrow> H \<turnstile> y IN x"
   by (rule cut2 [OF OrdP_IN_SUCC_D_lemma])
 
 lemma OrdP_IN_SUCC_Iff: "H \<turnstile> OrdP y \<Longrightarrow> H \<turnstile> SUCC x IN SUCC y IFF x IN y" 
   by (metis Assume Iff_I OrdP_IN_SUCC OrdP_IN_SUCC_D thin1)
 
 
 section \<open>The predicate \<open>LstSeqP\<close>\<close>
 
 lemma hfun_sigma_ord_iff: "hfun_sigma_ord s \<longleftrightarrow> OrdDom s \<and> hfun_sigma s"
   by (auto simp: hfun_sigma_ord_def OrdDom_def hfun_sigma_def HBall_def, metis+)
 
 lemma hfun_sigma_iff: "hfun_sigma r \<longleftrightarrow> hfunction r \<and> hrelation r"
   by (auto simp add: HBall_def hfun_sigma_def hfunction_def hrelation_def is_hpair_def, metis+)
 
 lemma Seq_iff: "Seq r d \<longleftrightarrow> d \<le> hdomain r \<and> hfun_sigma r"
   by (auto simp: Seq_def hfun_sigma_iff)
 
 lemma LstSeq_iff: "LstSeq s k y \<longleftrightarrow> succ k \<le> hdomain s \<and> \<langle>k,y\<rangle> \<^bold>\<in> s \<and> hfun_sigma_ord s"
   by (auto simp: OrdDom_def LstSeq_def Seq_iff hfun_sigma_ord_iff)
 
 nominal_function LstSeqP :: "tm \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> fm"
   where
     "LstSeqP s k y = OrdP k AND HDomain_Incl s (SUCC k) AND HFun_Sigma s AND HPair k y IN s"
   by (auto simp: eqvt_def LstSeqP_graph_aux_def)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma
  shows LstSeqP_fresh_iff [simp]:
       "a \<sharp> LstSeqP s k y \<longleftrightarrow> a \<sharp> s \<and> a \<sharp> k \<and> a \<sharp> y"         (is ?thesis1)
    and eval_fm_LstSeqP [simp]: 
       "eval_fm e (LstSeqP s k y) \<longleftrightarrow> LstSeq \<lbrakk>s\<rbrakk>e \<lbrakk>k\<rbrakk>e \<lbrakk>y\<rbrakk>e"  (is ?thesis2)
 proof -
   show ?thesis1 ?thesis2
     by (auto simp: LstSeq_iff OrdDom_def hfun_sigma_ord_iff)
 qed
 
 lemma LstSeqP_subst [simp]:
   "(LstSeqP s k y)(i::=t) = LstSeqP (subst i t s) (subst i t k) (subst i t y)" 
   by (auto simp: fresh_Pair fresh_at_base)
 
 lemma LstSeqP_E: 
   assumes "insert (HDomain_Incl s (SUCC k)) 
             (insert (OrdP k) (insert (HFun_Sigma s)
               (insert (HPair k y IN s) H))) \<turnstile> B" 
     shows "insert (LstSeqP s k y) H \<turnstile> B" 
   using assms by (auto simp: insert_commute)
 
 declare LstSeqP.simps [simp del]
 
 lemma LstSeqP_cong:
   assumes "H \<turnstile> s EQ s'" "H \<turnstile> k EQ k'" "H \<turnstile> y EQ y'" 
   shows "H \<turnstile> LstSeqP s k y IFF LstSeqP s' k' y'"
   by (rule P3_cong [OF _ assms], auto)
 
 lemma LstSeqP_OrdP: "H \<turnstile> LstSeqP r k y \<Longrightarrow> H \<turnstile> OrdP k"
   by (metis Conj_E1 LstSeqP.simps)
 
 lemma LstSeqP_Mem_lemma: "{ LstSeqP r k y, HPair k' z IN r, k' IN k } \<turnstile> LstSeqP r k' z"
   by (auto simp: LstSeqP.simps intro: Ord_IN_Ord OrdP_SUCC_I OrdP_IN_SUCC HDomain_Incl_Mem_Ord)
 
 lemma LstSeqP_Mem: "H \<turnstile> LstSeqP r k y \<Longrightarrow> H \<turnstile> HPair k' z IN r \<Longrightarrow> H \<turnstile> k' IN k \<Longrightarrow> H \<turnstile> LstSeqP r k' z"
   by (rule cut3 [OF LstSeqP_Mem_lemma])
 
 lemma LstSeqP_imp_Mem: "H \<turnstile> LstSeqP s k y \<Longrightarrow> H \<turnstile> HPair k y IN s"
   by (auto simp: LstSeqP.simps) (metis Conj_E2)
 
 lemma LstSeqP_SUCC: "H \<turnstile> LstSeqP r (SUCC d) y \<Longrightarrow> H \<turnstile> HPair d z IN r \<Longrightarrow> H \<turnstile> LstSeqP r d z"
   by (metis LstSeqP_Mem Mem_SUCC_I2 Refl)
 
 lemma LstSeqP_EQ: "\<lbrakk>H \<turnstile> LstSeqP s k y; H \<turnstile> HPair k y' IN s\<rbrakk> \<Longrightarrow> H \<turnstile> y EQ y'" 
   by (metis AssumeH(2) HFun_Sigma_E LstSeqP_E cut1 insert_commute)
 
 end
diff --git a/thys/Incompleteness/SyntaxN.thy b/thys/Incompleteness/SyntaxN.thy
--- a/thys/Incompleteness/SyntaxN.thy
+++ b/thys/Incompleteness/SyntaxN.thy
@@ -1,1594 +1,1577 @@
 chapter\<open>Syntax of Terms and Formulas using Nominal Logic\<close>
 
 theory SyntaxN
 imports Nominal2.Nominal2 HereditarilyFinite.OrdArith
 begin
 
 section\<open>Terms and Formulas\<close>
 
 subsection\<open>Hf is a pure permutation type\<close>
 
 instantiation hf :: pt
 begin
   definition "p \<bullet> (s::hf) = s"
   instance
     by standard (simp_all add: permute_hf_def)
 end
 
 instance hf :: pure
   proof qed (rule permute_hf_def)
 
 atom_decl name
 
 declare fresh_set_empty [simp]
 
 lemma supp_name [simp]: fixes i::name shows "supp i = {atom i}"
   by (rule supp_at_base)
 
 subsection\<open>The datatypes\<close>
 
 nominal_datatype tm = Zero | Var name | Eats tm tm
 
 nominal_datatype fm =
     Mem tm tm    (infixr "IN" 150)
   | Eq tm tm     (infixr "EQ" 150)
   | Disj fm fm   (infixr "OR" 130)
   | Neg fm
   | Ex x::name f::fm binds x in f
 
 text \<open>Mem, Eq are atomic formulas; Disj, Neg, Ex are non-atomic\<close>
 
 declare tm.supp [simp] fm.supp [simp]
 
 subsection\<open>Substitution\<close>
 
 nominal_function subst :: "name \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm"
   where
    "subst i x Zero       = Zero"
  | "subst i x (Var k)    = (if i=k then x else Var k)"
  | "subst i x (Eats t u) = Eats (subst i x t) (subst i x u)"
 by (auto simp: eqvt_def subst_graph_aux_def) (metis tm.strong_exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 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))"
   by (induct t rule: tm.induct) (auto simp: fresh_at_base)
 
 lemma forget_subst_tm [simp]: "atom a \<sharp> tm \<Longrightarrow> subst a x tm = tm"
   by (induct tm rule: tm.induct) (simp_all add: fresh_at_base)
 
 lemma subst_tm_id [simp]: "subst a (Var a) tm = tm"
   by (induct tm rule: tm.induct) simp_all
 
 lemma subst_tm_commute [simp]:
   "atom j \<sharp> tm \<Longrightarrow> subst j u (subst i t tm) = subst i (subst j u t) tm"
   by (induct tm rule: tm.induct) (auto simp: fresh_Pair)
 
 lemma subst_tm_commute2 [simp]:
   "atom j \<sharp> t \<Longrightarrow> atom i \<sharp> u \<Longrightarrow> i \<noteq> j \<Longrightarrow> subst j u (subst i t tm) = subst i t (subst j u tm)"
   by (induct tm rule: tm.induct) auto
 
 lemma repeat_subst_tm [simp]: "subst i u (subst i t tm) = subst i (subst i u t) tm"
   by (induct tm rule: tm.induct) auto
 
 nominal_function  subst_fm :: "fm \<Rightarrow> name \<Rightarrow> tm \<Rightarrow> fm" ("_'(_::=_')" [1000, 0, 0] 200)
   where
     Mem:  "(Mem t u)(i::=x)  = Mem (subst i x t) (subst i x u)"
   | Eq:   "(Eq t u)(i::=x)   = Eq  (subst i x t) (subst i x u)"
   | Disj: "(Disj A B)(i::=x) = Disj (A(i::=x)) (B(i::=x))"
   | Neg:  "(Neg A)(i::=x)    = Neg  (A(i::=x))"
   | Ex:   "atom j \<sharp> (i, x) \<Longrightarrow> (Ex j A)(i::=x) = Ex j (A(i::=x))"
 apply (simp add: eqvt_def subst_fm_graph_aux_def)
 apply auto [16]
 apply (rule_tac y=a and c="(aa, b)" in fm.strong_exhaust)
 apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
 apply (metis flip_at_base_simps(3) flip_fresh_fresh)
 done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma size_subst_fm [simp]: "size (A(i::=x)) = size A"
   by (nominal_induct A avoiding: i x rule: fm.strong_induct) auto
 
 lemma forget_subst_fm [simp]: "atom a \<sharp> A \<Longrightarrow> A(a::=x) = A"
   by (nominal_induct A avoiding: a x rule: fm.strong_induct) (auto simp: fresh_at_base)
 
 lemma subst_fm_id [simp]: "A(a::=Var a) = A"
   by (nominal_induct A avoiding: a rule: fm.strong_induct) (auto simp: fresh_at_base)
 
 lemma fresh_subst_fm_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))"
   by (nominal_induct A avoiding: i x rule: fm.strong_induct) (auto simp: fresh_at_base)
 
 lemma subst_fm_commute [simp]:
   "atom j \<sharp> A \<Longrightarrow> (A(i::=t))(j::=u) = A(i ::= subst j u t)"
   by (nominal_induct A avoiding: i j t u rule: fm.strong_induct) (auto simp: fresh_at_base)
 
 lemma repeat_subst_fm [simp]: "(A(i::=t))(i::=u) = A(i ::= subst i u t)"
   by (nominal_induct A avoiding: i t u rule: fm.strong_induct) auto
 
 lemma subst_fm_Ex_with_renaming:
   "atom i' \<sharp> (A, i, j, t) \<Longrightarrow> (Ex i A)(j ::= t) = Ex i' (((i \<leftrightarrow> i') \<bullet> A)(j ::= t))"
   by (rule subst [of "Ex i' ((i \<leftrightarrow> i') \<bullet> A)" "Ex i A"])
      (auto simp: Abs1_eq_iff flip_def swap_commute)
 
 text \<open>the simplifier cannot apply the rule above, because
 it introduces a new variable at the right hand side.\<close>
 
 simproc_setup subst_fm_renaming ("(Ex i A)(j ::= t)") = \<open>fn _ => fn ctxt => fn ctrm =>
   let
      val _ $ (_ $ i $ A) $ j $ t = Thm.term_of ctrm
 
      val atoms = Simplifier.prems_of ctxt
       |> map_filter (fn thm => case Thm.prop_of thm of
            _ $ (Const (@{const_name fresh}, _) $ atm $ _) => SOME (atm) | _ => NONE)
       |> distinct ((=))
 
      fun get_thm atm =
        let
          val goal = HOLogic.mk_Trueprop (mk_fresh atm (HOLogic.mk_tuple [A, i, j, t]))
        in
          SOME ((Goal.prove ctxt [] [] goal (K (asm_full_simp_tac ctxt 1)))
            RS @{thm subst_fm_Ex_with_renaming} RS eq_reflection)
          handle ERROR _ => NONE
        end
   in
     get_first get_thm atoms
   end
 \<close>
 
 subsection\<open>Semantics\<close>
 
 definition e0 :: "(name, hf) finfun"    \<comment> \<open>the null environment\<close>
   where "e0 \<equiv> finfun_const 0"
 
 nominal_function eval_tm :: "(name, hf) finfun \<Rightarrow> tm \<Rightarrow> hf"
   where
    "eval_tm e Zero = 0"
  | "eval_tm e (Var k) = finfun_apply e k"
  | "eval_tm e (Eats t u) = eval_tm e t \<triangleleft> eval_tm e u"
 by (auto simp: eqvt_def eval_tm_graph_aux_def) (metis tm.strong_exhaust)
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 syntax
   "_EvalTm" :: "tm \<Rightarrow> (name, hf) finfun \<Rightarrow> hf"      ("\<lbrakk>_\<rbrakk>_" [0,1000]1000)
 
 translations
   "\<lbrakk>tm\<rbrakk>e"    == "CONST eval_tm e tm"
 
 nominal_function eval_fm :: "(name, hf) finfun \<Rightarrow> fm \<Rightarrow> bool"
   where
    "eval_fm e (t IN u) \<longleftrightarrow> \<lbrakk>t\<rbrakk>e \<^bold>\<in> \<lbrakk>u\<rbrakk>e"
  | "eval_fm e (t EQ u) \<longleftrightarrow> \<lbrakk>t\<rbrakk>e = \<lbrakk>u\<rbrakk>e"
  | "eval_fm e (A OR B) \<longleftrightarrow> eval_fm e A \<or> eval_fm e B"
  | "eval_fm e (Neg A) \<longleftrightarrow> (~ eval_fm e A)"
  | "atom k \<sharp> e \<Longrightarrow> eval_fm e (Ex k A) \<longleftrightarrow> (\<exists>x. eval_fm (finfun_update e k x) A)"
-supply [[simproc del: defined_all]]
-apply(simp add: eqvt_def eval_fm_graph_aux_def)
-apply(auto del: iffI)[16]
-apply(rule_tac y=b and c="(a)" in fm.strong_exhaust)
-apply(auto simp: fresh_star_def)[5]
-using [[simproc del: alpha_lst]] apply clarsimp
-apply(erule_tac c="(ea)" in Abs_lst1_fcb2')
-apply(rule pure_fresh)
-apply(simp add: fresh_star_def)
-apply (simp_all add: eqvt_at_def)
-apply (simp_all add: perm_supp_eq)
-done
+                   supply [[simproc del: defined_all]]
+                   apply(simp add: eqvt_def eval_fm_graph_aux_def)
+                  apply(auto del: iffI)[16]
+   apply (metis fm.strong_exhaust fresh_star_insert)
+  using [[simproc del: alpha_lst]] apply clarsimp
+  apply(erule Abs_lst1_fcb2')
+     apply(rule pure_fresh)
+    apply(simp add: fresh_star_def)
+   apply (simp_all add: eqvt_at_def)
+   apply (simp_all add: perm_supp_eq)
+  done
 
 nominal_termination (eqvt)
   by lexicographic_order
 
 lemma eval_tm_rename:
   assumes "atom k' \<sharp> t"
   shows "\<lbrakk>t\<rbrakk>(finfun_update e k x) = \<lbrakk>(k' \<leftrightarrow> k) \<bullet> t\<rbrakk>(finfun_update e k' x)"
 using assms
 by (induct t rule: tm.induct) (auto simp: permute_flip_at)
 
 lemma eval_fm_rename:
   assumes "atom k' \<sharp> A"
   shows "eval_fm (finfun_update e k x) A = eval_fm (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A)"
-using assms
-apply (nominal_induct A avoiding: e k k' x rule: fm.strong_induct)
-apply (simp_all add: eval_tm_rename[symmetric], metis)
-apply (simp add: fresh_finfun_update fresh_at_base finfun_update_twist)
-done
+  using assms
+proof (nominal_induct A avoiding: e k k' x rule: fm.strong_induct)
+  case Ex
+  then show ?case
+    by (simp add: fresh_finfun_update fresh_at_base) (metis finfun_update_twist)
+qed (simp_all add: eval_tm_rename[symmetric], metis)
 
 lemma better_ex_eval_fm[simp]:
   "eval_fm e (Ex k A) \<longleftrightarrow> (\<exists>x. eval_fm (finfun_update e k x) A)"
 proof -
   obtain k'::name where k': "atom k' \<sharp> (k, e, A)"
     by (rule obtain_fresh)
   then have eq: "Ex k' ((k' \<leftrightarrow> k) \<bullet> A) = Ex k A"
     by (simp add: Abs1_eq_iff flip_def)
   have "eval_fm e (Ex k' ((k' \<leftrightarrow> k) \<bullet> A)) = (\<exists>x. eval_fm (finfun_update e k' x) ((k' \<leftrightarrow> k) \<bullet> A))"
     using k' by simp
   also have "... = (\<exists>x. eval_fm (finfun_update e k x) A)"
     by (metis eval_fm_rename k' fresh_Pair)
   finally show ?thesis
     by (metis eq)
 qed
 
 lemma forget_eval_tm [simp]: "atom i \<sharp> t \<Longrightarrow>  \<lbrakk>t\<rbrakk>(finfun_update e i x) = \<lbrakk>t\<rbrakk>e"
   by (induct t rule: tm.induct) (simp_all add: fresh_at_base)
 
 lemma forget_eval_fm [simp]:
    "atom k \<sharp> A \<Longrightarrow> eval_fm (finfun_update e k x) A = eval_fm e A"
   by (nominal_induct A avoiding: k e rule: fm.strong_induct)
      (simp_all add: fresh_at_base finfun_update_twist)
 
 lemma eval_subst_tm: "\<lbrakk>subst i t u\<rbrakk>e = \<lbrakk>u\<rbrakk>(finfun_update e i \<lbrakk>t\<rbrakk>e)"
   by (induct u rule: tm.induct) (auto)
 
 lemma eval_subst_fm: "eval_fm e (fm(i::= t)) = eval_fm (finfun_update e i \<lbrakk>t\<rbrakk>e) fm"
   by (nominal_induct fm avoiding: i t e rule: fm.strong_induct)
      (simp_all add: eval_subst_tm finfun_update_twist fresh_at_base)
 
 subsection\<open>Derived syntax\<close>
 
 subsubsection\<open>Ordered pairs\<close>
 
 definition HPair :: "tm \<Rightarrow> tm \<Rightarrow> tm"
   where "HPair a b = Eats (Eats Zero (Eats (Eats Zero b) a)) (Eats (Eats Zero a) a)"
 
 lemma HPair_eqvt [eqvt]: "(p \<bullet> HPair a b) = HPair (p \<bullet> a) (p \<bullet> b)"
   by (auto simp: HPair_def)
 
 lemma fresh_HPair [simp]: "x \<sharp> HPair a b \<longleftrightarrow> (x \<sharp> a \<and> x \<sharp> b)"
   by (auto simp: HPair_def)
 
 lemma HPair_injective_iff [iff]: "HPair a b = HPair a' b' \<longleftrightarrow> (a = a' \<and> b = b')"
   by (auto simp: HPair_def)
 
 lemma subst_tm_HPair [simp]: "subst i x (HPair a b) = HPair (subst i x a) (subst i x b)"
   by (auto simp: HPair_def)
 
 lemma eval_tm_HPair [simp]: "\<lbrakk>HPair a b\<rbrakk>e = hpair \<lbrakk>a\<rbrakk>e \<lbrakk>b\<rbrakk>e"
   by (auto simp: HPair_def hpair_def)
 
 subsubsection\<open>Ordinals\<close>
 
 definition
   SUCC  :: "tm \<Rightarrow> tm"  where
     "SUCC x \<equiv> Eats x x"
 
 fun ORD_OF :: "nat \<Rightarrow> tm"
   where
    "ORD_OF 0 = Zero"
  | "ORD_OF (Suc k) = SUCC (ORD_OF k)"
 
 lemma eval_tm_SUCC [simp]: "\<lbrakk>SUCC t\<rbrakk>e = succ \<lbrakk>t\<rbrakk>e"
   by (simp add: SUCC_def succ_def)
 
 lemma SUCC_fresh_iff [simp]: "a \<sharp> SUCC t \<longleftrightarrow> a \<sharp> t"
   by (simp add: SUCC_def)
 
 lemma SUCC_eqvt [eqvt]: "(p \<bullet> SUCC a) = SUCC (p \<bullet> a)"
   by (simp add: SUCC_def)
 
 lemma SUCC_subst [simp]: "subst i t (SUCC k) = SUCC (subst i t k)"
   by (simp add: SUCC_def)
 
 lemma eval_tm_ORD_OF [simp]: "\<lbrakk>ORD_OF n\<rbrakk>e = ord_of n"
   by (induct n) auto
 
 lemma ORD_OF_fresh [simp]: "a \<sharp> ORD_OF n"
   by (induct n) (auto simp: SUCC_def)
 
 lemma ORD_OF_eqvt [eqvt]: "(p \<bullet> ORD_OF n) = ORD_OF (p \<bullet> n)"
   by (induct n) (auto simp: permute_pure SUCC_eqvt)
 
 subsection\<open>Derived logical connectives\<close>
 
 abbreviation Imp :: "fm \<Rightarrow> fm \<Rightarrow> fm"   (infixr "IMP" 125)
   where "Imp A B \<equiv> Disj (Neg A) B"
 
 abbreviation All :: "name \<Rightarrow> fm \<Rightarrow> fm"
   where "All i A \<equiv> Neg (Ex i (Neg A))"
 
 abbreviation All2 :: "name \<Rightarrow> tm \<Rightarrow> fm \<Rightarrow> fm" \<comment> \<open>bounded universal quantifier, for Sigma formulas\<close>
   where "All2 i t A \<equiv> All i ((Var i IN t) IMP A)"
 
 subsubsection\<open>Conjunction\<close>
 
 definition Conj :: "fm \<Rightarrow> fm \<Rightarrow> fm"   (infixr "AND" 135)
   where "Conj A B \<equiv> Neg (Disj (Neg A) (Neg B))"
 
 lemma Conj_eqvt [eqvt]: "p \<bullet> (A AND B) = (p \<bullet> A) AND (p \<bullet> B)"
   by (simp add: Conj_def)
 
 lemma fresh_Conj [simp]: "a \<sharp> A AND B \<longleftrightarrow> (a \<sharp> A \<and> a \<sharp> B)"
   by (auto simp: Conj_def)
 
 lemma supp_Conj [simp]: "supp (A AND B) = supp A \<union> supp B"
   by (auto simp: Conj_def)
 
 lemma size_Conj [simp]: "size (A AND B) = size A + size B + 4"
   by (simp add: Conj_def)
 
 lemma Conj_injective_iff [iff]: "(A AND B) = (A' AND B') \<longleftrightarrow> (A = A' \<and> B = B')"
   by (auto simp: Conj_def)
 
 lemma subst_fm_Conj [simp]: "(A AND B)(i::=x) = (A(i::=x)) AND (B(i::=x))"
   by (auto simp: Conj_def)
 
 lemma eval_fm_Conj [simp]: "eval_fm e (Conj A B) \<longleftrightarrow> (eval_fm e A \<and> eval_fm e B)"
   by (auto simp: Conj_def)
 
 subsubsection\<open>If and only if\<close>
 
 definition Iff :: "fm \<Rightarrow> fm \<Rightarrow> fm"   (infixr "IFF" 125)
   where "Iff A B = Conj (Imp A B) (Imp B A)"
 
 lemma Iff_eqvt [eqvt]: "p \<bullet> (A IFF B) = (p \<bullet> A) IFF (p \<bullet> B)"
   by (simp add: Iff_def)
 
 lemma fresh_Iff [simp]: "a \<sharp> A IFF B \<longleftrightarrow> (a \<sharp> A \<and> a \<sharp> B)"
   by (auto simp: Conj_def Iff_def)
 
 lemma size_Iff [simp]: "size (A IFF B) = 2*(size A + size B) + 8"
   by (simp add: Iff_def)
 
 lemma Iff_injective_iff [iff]: "(A IFF B) = (A' IFF B') \<longleftrightarrow> (A = A' \<and> B = B')"
   by (auto simp: Iff_def)
 
 lemma subst_fm_Iff [simp]: "(A IFF B)(i::=x) = (A(i::=x)) IFF (B(i::=x))"
   by (auto simp: Iff_def)
 
 lemma eval_fm_Iff [simp]: "eval_fm e (Iff A B) \<longleftrightarrow> (eval_fm e A  \<longleftrightarrow>  eval_fm e B)"
   by (auto simp: Iff_def)
 
 
 section\<open>Axioms and Theorems\<close>
 
 subsection\<open>Logical axioms\<close>
 
 inductive_set boolean_axioms :: "fm set"
   where
     Ident:     "A IMP A \<in> boolean_axioms"
   | DisjI1:    "A IMP (A OR B) \<in> boolean_axioms"
   | DisjCont:  "(A OR A) IMP A \<in> boolean_axioms"
   | DisjAssoc: "(A OR (B OR C)) IMP ((A OR B) OR C) \<in> boolean_axioms"
   | DisjConj:  "(C OR A) IMP (((Neg C) OR B) IMP (A OR B)) \<in> boolean_axioms"
 
 lemma boolean_axioms_hold: "A \<in> boolean_axioms \<Longrightarrow> eval_fm e A"
   by (induct rule: boolean_axioms.induct, auto)
 
 inductive_set special_axioms :: "fm set" where
   I: "A(i::=x) IMP (Ex i A) \<in> special_axioms"
 
 lemma special_axioms_hold: "A \<in> special_axioms \<Longrightarrow> eval_fm e A"
   by (induct rule: special_axioms.induct, auto) (metis eval_subst_fm)
 
 inductive_set induction_axioms :: "fm set" where
   ind:
   "atom (j::name) \<sharp> (i,A)
    \<Longrightarrow> A(i::=Zero) IMP ((All i (All j (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j))))))
       IMP (All i A))
     \<in> induction_axioms"
 
 lemma twist_forget_eval_fm [simp]:
    "atom j \<sharp> (i, A)
     \<Longrightarrow> eval_fm (finfun_update (finfun_update (finfun_update e i x) j y) i z) A =
         eval_fm (finfun_update e i z) A"
   by (metis finfun_update_twice finfun_update_twist forget_eval_fm fresh_Pair)
 
 lemma induction_axioms_hold: "A \<in> induction_axioms \<Longrightarrow> eval_fm e A"
   by (induction rule: induction_axioms.induct) (auto simp: eval_subst_fm intro: hf_induct_ax)
 
 subsection \<open>Concrete variables\<close>
 
 declare Abs_name_inject[simp]
 
 abbreviation
   "X0 \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) 0)"
 
 abbreviation
   "X1 \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) (Suc 0))"
    \<comment> \<open>We prefer @{term "Suc 0"} because simplification will transform 1 to that form anyway.\<close>
 
 abbreviation
   "X2 \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) 2)"
 
 abbreviation
   "X3 \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) 3)"
 
 abbreviation
   "X4 \<equiv> Abs_name (Atom (Sort ''SyntaxN.name'' []) 4)"
 
 
 subsection\<open>The HF axioms\<close>
 
 definition HF1 :: fm where  \<comment> \<open>the axiom @{term"z=0 \<longleftrightarrow> (\<forall>x. \<not> x \<^bold>\<in> z)"}\<close>
   "HF1 = (Var X0 EQ Zero) IFF (All X1 (Neg (Var X1 IN Var X0)))"
 
 lemma HF1_holds: "eval_fm e HF1"
   by (auto simp: HF1_def)
 
 
 definition HF2 :: fm where  \<comment> \<open>the axiom @{term"z = x \<triangleleft> y \<longleftrightarrow> (\<forall>u. u \<^bold>\<in> z \<longleftrightarrow> u \<^bold>\<in> x | u=y)"}\<close>
   "HF2 \<equiv> Var X0 EQ Eats (Var X1) (Var X2) IFF
           All X3 (Var X3 IN Var X0 IFF Var X3 IN Var X1 OR Var X3 EQ Var X2)"
 
 lemma HF2_holds: "eval_fm e HF2"
   by (auto simp: HF2_def)
 
 definition HF_axioms where "HF_axioms = {HF1, HF2}"
 
 lemma HF_axioms_hold: "A \<in> HF_axioms \<Longrightarrow> eval_fm e A"
   by (auto simp: HF_axioms_def HF1_holds HF2_holds)
 
 subsection\<open>Equality axioms\<close>
 
 definition refl_ax :: fm where
   "refl_ax = Var X1 EQ Var X1"
 
 lemma refl_ax_holds: "eval_fm e refl_ax"
   by (auto simp: refl_ax_def)
 
 definition eq_cong_ax :: fm where
   "eq_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP
                 ((Var X1 EQ Var X3) IMP (Var X2 EQ Var X4))"
 
 lemma eq_cong_ax_holds: "eval_fm e eq_cong_ax"
   by (auto simp: Conj_def eq_cong_ax_def)
 
 definition mem_cong_ax :: fm where
   "mem_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP
                  ((Var X1 IN Var X3) IMP (Var X2 IN Var X4))"
 
 lemma mem_cong_ax_holds: "eval_fm e mem_cong_ax"
   by (auto simp: Conj_def mem_cong_ax_def)
 
 definition eats_cong_ax :: fm where
   "eats_cong_ax = ((Var X1 EQ Var X2) AND (Var X3 EQ Var X4)) IMP
                   ((Eats (Var X1) (Var X3)) EQ (Eats (Var X2) (Var X4)))"
 
 lemma eats_cong_ax_holds: "eval_fm e eats_cong_ax"
   by (auto simp: Conj_def eats_cong_ax_def)
 
 definition equality_axioms :: "fm set" where
   "equality_axioms = {refl_ax, eq_cong_ax, mem_cong_ax, eats_cong_ax}"
 
 lemma equality_axioms_hold: "A \<in> equality_axioms \<Longrightarrow> eval_fm e A"
   by (auto simp: equality_axioms_def refl_ax_holds eq_cong_ax_holds mem_cong_ax_holds eats_cong_ax_holds)
 
 subsection\<open>The proof system\<close>
 
 text\<open>This arbitrary additional axiom generalises the statements of the incompleteness theorems
   and other results to any formal system stronger than the HF theory. The additional axiom
   could be the conjunction of any finite number of assertions. Any more general extension
   must be a form that can be formalised for the proof predicate.\<close>
 consts  extra_axiom :: fm
 
 specification (extra_axiom)
   extra_axiom_holds:  "eval_fm e extra_axiom"
   by (rule exI [where x = "Zero IN Eats Zero Zero"], auto)
 
 inductive hfthm :: "fm set \<Rightarrow> fm \<Rightarrow> bool" (infixl "\<turnstile>" 55)
   where
     Hyp:    "A \<in> H \<Longrightarrow> H \<turnstile> A"
   | Extra:  "H \<turnstile> extra_axiom"
   | Bool:   "A \<in> boolean_axioms \<Longrightarrow> H \<turnstile> A"
   | Eq:     "A \<in> equality_axioms \<Longrightarrow> H \<turnstile> A"
   | Spec:   "A \<in> special_axioms \<Longrightarrow> H \<turnstile> A"
   | HF:     "A \<in> HF_axioms \<Longrightarrow> H \<turnstile> A"
   | Ind:    "A \<in> induction_axioms \<Longrightarrow> H \<turnstile> A"
   | MP:     "H \<turnstile> A IMP B \<Longrightarrow> H' \<turnstile> A \<Longrightarrow> H \<union> H' \<turnstile> B"
   | Exists: "H \<turnstile> A IMP B \<Longrightarrow> atom i \<sharp> B \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (Ex i A) IMP B"
 
 text\<open>Soundness theorem!\<close>
 theorem hfthm_sound: assumes "H \<turnstile> A" shows "(\<forall>B\<in>H. eval_fm e B) \<Longrightarrow> eval_fm e A"
 using assms
 proof (induct arbitrary: e)
-  case (Hyp A H) thus ?case
-    by auto
-next
   case (Extra H) thus ?case
     by (metis extra_axiom_holds)
 next
   case (Bool A H) thus ?case
     by (metis boolean_axioms_hold)
 next
   case (Eq A H) thus ?case
     by (metis equality_axioms_hold)
 next
   case (Spec A H) thus ?case
     by (metis special_axioms_hold)
 next
   case (HF A H) thus ?case
     by (metis HF_axioms_hold)
 next
   case (Ind A H) thus ?case
     by (metis induction_axioms_hold)
 next
-  case (MP H A B H') thus ?case
-    by auto
-next
   case (Exists H A B i e) thus ?case
     by auto (metis forget_eval_fm)
-qed
+qed auto
 
 subsection\<open>Derived rules of inference\<close>
 
 lemma contraction: "insert A (insert A H) \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B"
   by (metis insert_absorb2)
 
 lemma thin_Un: "H \<turnstile> A \<Longrightarrow> H \<union> H' \<turnstile> A"
   by (metis Bool MP boolean_axioms.Ident sup_commute)
 
 lemma thin: "H \<turnstile> A \<Longrightarrow> H \<subseteq> H' \<Longrightarrow> H' \<turnstile> A"
   by (metis Un_absorb1 thin_Un)
 
 lemma thin0: "{} \<turnstile> A \<Longrightarrow> H \<turnstile> A"
   by (metis sup_bot_left thin_Un)
 
 lemma thin1: "H \<turnstile> B \<Longrightarrow> insert A H \<turnstile> B"
   by (metis subset_insertI thin)
 
 lemma thin2: "insert A1 H \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B"
   by (blast intro: thin)
 
 lemma thin3: "insert A1 (insert A2 H) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 H)) \<turnstile> B"
   by (blast intro: thin)
 
 lemma thin4:
   "insert A1 (insert A2 (insert A3 H)) \<turnstile> B
    \<Longrightarrow> insert A1 (insert A2 (insert A3 (insert A4 H))) \<turnstile> B"
   by (blast intro: thin)
 
 lemma rotate2: "insert A2 (insert A1 H) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 H) \<turnstile> B"
   by (blast intro: thin)
 
 lemma rotate3: "insert A3 (insert A1 (insert A2 H)) \<turnstile> B \<Longrightarrow> insert A1 (insert A2 (insert A3 H)) \<turnstile> B"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 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"
   by (blast intro: thin)
 
 lemma MP_same: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
   by (metis MP Un_absorb)
 
 lemma MP_thin: "HA \<turnstile> A IMP B \<Longrightarrow> HB \<turnstile> A \<Longrightarrow> HA \<union> HB \<subseteq> H \<Longrightarrow> H \<turnstile> B"
   by (metis MP_same le_sup_iff thin)
 
 lemma MP_null: "{} \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
   by (metis MP_same thin0)
 
 lemma Disj_commute: "H \<turnstile> B OR A \<Longrightarrow> H \<turnstile> A OR B"
   using DisjConj [of B A B] Ident [of B]
 by (metis Bool MP_same)
 
 lemma S: assumes  "H \<turnstile> A IMP (B IMP C)" "H' \<turnstile> A IMP B" shows "H \<union> H' \<turnstile> A IMP C"
 proof -
   have "H' \<union> H \<turnstile> (Neg A) OR (C OR (Neg A))"
     by (metis Bool MP MP_same boolean_axioms.DisjConj Disj_commute DisjAssoc assms)
   thus ?thesis
     by (metis Bool Disj_commute Un_commute MP_same DisjAssoc DisjCont DisjI1)
 qed
 
 lemma Assume: "insert A H \<turnstile> A"
   by (metis Hyp insertI1)
 
 lemmas AssumeH = Assume Assume [THEN rotate2] Assume [THEN rotate3] Assume [THEN rotate4] Assume [THEN rotate5]
                  Assume [THEN rotate6] Assume [THEN rotate7] Assume [THEN rotate8] Assume [THEN rotate9] Assume [THEN rotate10]
                  Assume [THEN rotate11] Assume [THEN rotate12]
 declare AssumeH [intro!]
 
 lemma Imp_triv_I: "H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B"
   by (metis Bool Disj_commute MP_same boolean_axioms.DisjI1)
 
 lemma DisjAssoc1: "H \<turnstile> A OR (B OR C) \<Longrightarrow> H \<turnstile> (A OR B) OR C"
   by (metis Bool MP_same boolean_axioms.DisjAssoc)
 
 lemma DisjAssoc2: "H \<turnstile> (A OR B) OR C \<Longrightarrow> H \<turnstile> A OR (B OR C)"
   by (metis DisjAssoc1 Disj_commute)
 
 lemma Disj_commute_Imp: "H \<turnstile> (B OR A) IMP (A OR B)"
   using DisjConj [of B A B] Ident [of B]
   by (metis Bool DisjAssoc2 Disj_commute MP_same)
 
 lemma Disj_Semicong_1: "H \<turnstile> A OR C \<Longrightarrow> H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> B OR C"
   using DisjConj [of A C B]
   by (metis Bool Disj_commute MP_same)
 
 lemma Imp_Imp_commute: "H \<turnstile> B IMP (A IMP C) \<Longrightarrow> H \<turnstile> A IMP (B IMP C)"
   by (metis DisjAssoc1 DisjAssoc2 Disj_Semicong_1 Disj_commute_Imp)
 
 
 subsection\<open>The Deduction Theorem\<close>
 
 lemma deduction_Diff: assumes "H \<turnstile> B" shows "H - {C} \<turnstile> C IMP B"
 using assms
 proof (induct)
   case (Hyp A H) thus ?case
     by (metis Bool Imp_triv_I boolean_axioms.Ident hfthm.Hyp member_remove remove_def)
 next
   case (Extra H) thus ?case
     by (metis Imp_triv_I hfthm.Extra)
 next
   case (Bool A H) thus ?case
     by (metis Imp_triv_I hfthm.Bool)
 next
   case (Eq A H) thus ?case
     by (metis Imp_triv_I hfthm.Eq)
 next
   case (Spec A H) thus ?case
     by (metis Imp_triv_I hfthm.Spec)
 next
   case (HF A H) thus ?case
     by (metis Imp_triv_I hfthm.HF)
 next
   case (Ind A H) thus ?case
     by (metis Imp_triv_I hfthm.Ind)
 next
   case (MP H A B H')
   hence "(H-{C}) \<union> (H'-{C}) \<turnstile> Imp C B"
     by (simp add: S)
   thus ?case
     by (metis Un_Diff)
 next
   case (Exists H A B i) show ?case
   proof (cases "C \<in> H")
     case True
     hence "atom i \<sharp> C" using Exists by auto
     moreover have "H - {C} \<turnstile> A IMP C IMP B" using Exists
       by (metis Imp_Imp_commute)
     ultimately have "H - {C} \<turnstile> (Ex i A) IMP C IMP B" using Exists
-      by (metis fm.fresh(3) fm.fresh(4) hfthm.Exists member_remove remove_def)
+      using hfthm.Exists by force
     thus ?thesis
       by (metis Imp_Imp_commute)
   next
     case False
     hence "H - {C} = H" by auto
     thus ?thesis using Exists
       by (metis Imp_triv_I hfthm.Exists)
   qed
 qed
 
 theorem Imp_I [intro!]: "insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> A IMP B"
   by (metis Diff_insert_absorb Imp_triv_I deduction_Diff insert_absorb)
 
 lemma anti_deduction: "H \<turnstile> A IMP B \<Longrightarrow> insert A H \<turnstile> B"
    by (metis Assume MP_same thin1)
 
 subsection\<open>Cut rules\<close>
 
 lemma cut:  "H \<turnstile> A \<Longrightarrow> insert A H' \<turnstile> B \<Longrightarrow> H \<union> H' \<turnstile> B"
   by (metis MP Un_commute Imp_I)
 
 lemma cut_same: "H \<turnstile> A \<Longrightarrow> insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
   by (metis Un_absorb cut)
 
 lemma cut_thin: "HA \<turnstile> A \<Longrightarrow> insert A HB \<turnstile> B \<Longrightarrow> HA \<union> HB \<subseteq> H \<Longrightarrow> H \<turnstile> B"
   by (metis thin cut)
 
 lemma cut0: "{} \<turnstile> A \<Longrightarrow> insert A H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
   by (metis cut_same thin0)
 
 lemma cut1: "{A} \<turnstile> B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
   by (metis cut sup_bot_right)
 
 lemma rcut1: "{A} \<turnstile> B \<Longrightarrow> insert B H \<turnstile> C \<Longrightarrow> insert A H \<turnstile> C"
   by (metis Assume cut1 cut_same rotate2 thin1)
 
 lemma cut2: "\<lbrakk>{A,B} \<turnstile> C; H \<turnstile> A; H \<turnstile> B\<rbrakk> \<Longrightarrow> H \<turnstile> C"
   by (metis Un_empty_right Un_insert_right cut cut_same)
 
 lemma rcut2: "{A,B} \<turnstile> C \<Longrightarrow> insert C H \<turnstile> D \<Longrightarrow> H \<turnstile> B \<Longrightarrow> insert A H \<turnstile> D"
   by (metis Assume cut2 cut_same insert_commute thin1)
 
 lemma cut3: "\<lbrakk>{A,B,C} \<turnstile> D; H \<turnstile> A; H \<turnstile> B; H \<turnstile> C\<rbrakk> \<Longrightarrow> H \<turnstile> D"
   by (metis MP_same cut2 Imp_I)
 
 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"
   by (metis MP_same cut3 [of B C D] Imp_I)
 
 
 section\<open>Miscellaneous logical rules\<close>
 
 lemma Disj_I1: "H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B"
   by (metis Bool MP_same boolean_axioms.DisjI1)
 
 lemma Disj_I2: "H \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B"
   by (metis Disj_commute Disj_I1)
 
 lemma Peirce: "H \<turnstile> (Neg A) IMP A \<Longrightarrow> H \<turnstile> A"
   using DisjConj [of "Neg A" A A]  DisjCont [of A]
   by (metis Bool MP_same boolean_axioms.Ident)
 
 lemma Contra: "insert (Neg A) H \<turnstile> A \<Longrightarrow> H \<turnstile> A"
   by (metis Peirce Imp_I)
 
 lemma Imp_Neg_I: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> A IMP (Neg B) \<Longrightarrow> H \<turnstile> Neg A"
   by (metis DisjConj [of B "Neg A" "Neg A"] DisjCont Bool Disj_commute MP_same)
 
 lemma NegNeg_I: "H \<turnstile> A \<Longrightarrow> H \<turnstile> Neg (Neg A)"
   using DisjConj [of "Neg (Neg A)" "Neg A" "Neg (Neg A)"]
   by (metis Bool Ident MP_same)
 
 lemma NegNeg_D: "H \<turnstile> Neg (Neg A) \<Longrightarrow> H \<turnstile> A"
   by (metis Disj_I1 Peirce)
 
 lemma Neg_D: "H \<turnstile> Neg A \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
   by (metis Imp_Neg_I Imp_triv_I NegNeg_D)
 
 lemma Disj_Neg_1: "H \<turnstile> A OR B \<Longrightarrow> H \<turnstile> Neg B \<Longrightarrow> H \<turnstile> A"
   by (metis Disj_I1 Disj_Semicong_1 Disj_commute Peirce)
 
 lemma Disj_Neg_2: "H \<turnstile> A OR B \<Longrightarrow> H \<turnstile> Neg A \<Longrightarrow> H \<turnstile> B"
   by (metis Disj_Neg_1 Disj_commute)
 
 lemma Neg_Disj_I: "H \<turnstile> Neg A \<Longrightarrow> H \<turnstile> Neg B \<Longrightarrow> H \<turnstile> Neg (A OR B)"
 by (metis Bool Disj_Neg_1 MP_same boolean_axioms.Ident DisjAssoc)
 
 lemma Conj_I [intro!]: "H \<turnstile> A \<Longrightarrow> H \<turnstile> B \<Longrightarrow> H \<turnstile> A AND B"
   by (metis Conj_def NegNeg_I Neg_Disj_I)
 
 lemma Conj_E1: "H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> A"
   by (metis Conj_def Bool Disj_Neg_1 NegNeg_D boolean_axioms.DisjI1)
 
 lemma Conj_E2: "H \<turnstile> A AND B \<Longrightarrow> H \<turnstile> B"
   by (metis Conj_def Bool Disj_I2 Disj_Neg_2 MP_same DisjAssoc Ident)
 
 lemma Conj_commute: "H \<turnstile> B AND A \<Longrightarrow> H \<turnstile> A AND B"
   by (metis Conj_E1 Conj_E2 Conj_I)
 
 lemma Conj_E: assumes "insert A (insert B H) \<turnstile> C" shows "insert (A AND B) H \<turnstile> C"
 apply (rule cut_same [where A=A], metis Conj_E1 Hyp insertI1)
 by (metis (full_types) AssumeH(2) Conj_E2 assms cut_same [where A=B] insert_commute thin2)
 
 lemmas Conj_EH = Conj_E Conj_E [THEN rotate2] Conj_E [THEN rotate3] Conj_E [THEN rotate4] Conj_E [THEN rotate5]
                  Conj_E [THEN rotate6] Conj_E [THEN rotate7] Conj_E [THEN rotate8] Conj_E [THEN rotate9] Conj_E [THEN rotate10]
 declare Conj_EH [intro!]
 
 lemma Neg_I0: assumes "(\<And>B. atom i \<sharp> B \<Longrightarrow> insert A H \<turnstile> B)" shows "H \<turnstile> Neg A"
   by (rule Imp_Neg_I [where B = "Zero IN Zero"]) (auto simp: assms)
 
 lemma Neg_mono: "insert A H \<turnstile> B \<Longrightarrow> insert (Neg B) H \<turnstile> Neg A"
   by (rule Neg_I0) (metis Hyp Neg_D insert_commute insertI1 thin1)
 
 lemma Conj_mono: "insert A H \<turnstile> B \<Longrightarrow> insert C H \<turnstile> D \<Longrightarrow> insert (A AND C) H \<turnstile> B AND D"
   by (metis Conj_E1 Conj_E2 Conj_I Hyp Un_absorb2 cut insertI1 subset_insertI)
 
 lemma Disj_mono:
   assumes "insert A H \<turnstile> B" "insert C H \<turnstile> D" shows "insert (A OR C) H \<turnstile> B OR D"
 proof -
   { fix A B C H
     have "insert (A OR C) H \<turnstile> (A IMP B) IMP C OR B"
       by (metis Bool Hyp MP_same boolean_axioms.DisjConj insertI1)
     hence "insert A H \<turnstile> B \<Longrightarrow> insert (A OR C) H \<turnstile> C OR B"
       by (metis MP_same Un_absorb Un_insert_right Imp_I thin_Un)
   }
   thus ?thesis
     by (metis cut_same assms thin2)
 qed
 
 lemma Disj_E:
   assumes A: "insert A H \<turnstile> C" and B: "insert B H \<turnstile> C" shows "insert (A OR B) H \<turnstile> C"
   by (metis A B Disj_mono NegNeg_I Peirce)
 
 lemmas Disj_EH = Disj_E Disj_E [THEN rotate2] Disj_E [THEN rotate3] Disj_E [THEN rotate4] Disj_E [THEN rotate5]
                  Disj_E [THEN rotate6] Disj_E [THEN rotate7] Disj_E [THEN rotate8] Disj_E [THEN rotate9] Disj_E [THEN rotate10]
 declare Disj_EH [intro!]
 
 lemma Contra': "insert A H \<turnstile> Neg A \<Longrightarrow> H \<turnstile> Neg A"
   by (metis Contra Neg_mono)
 
 lemma NegNeg_E [intro!]: "insert A H \<turnstile> B \<Longrightarrow> insert (Neg (Neg A)) H \<turnstile> B"
   by (metis NegNeg_D Neg_mono)
 
 declare NegNeg_E [THEN rotate2, intro!]
 declare NegNeg_E [THEN rotate3, intro!]
 declare NegNeg_E [THEN rotate4, intro!]
 declare NegNeg_E [THEN rotate5, intro!]
 declare NegNeg_E [THEN rotate6, intro!]
 declare NegNeg_E [THEN rotate7, intro!]
 declare NegNeg_E [THEN rotate8, intro!]
 
 lemma Imp_E:
   assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (A IMP B) H \<turnstile> C"
 proof -
   have "insert (A IMP B) H \<turnstile> B"
     by (metis Hyp A thin1 MP_same insertI1)
   thus ?thesis
     by (metis cut [where B=C] Un_insert_right sup_commute sup_idem B)
 qed
 
 lemma Imp_cut:
   assumes "insert C H \<turnstile> A IMP B" "{A} \<turnstile> C"
     shows "H \<turnstile> A IMP B"
   by (metis Contra Disj_I1 Neg_mono assms rcut1)
 
 lemma Iff_I [intro!]: "insert A H \<turnstile> B \<Longrightarrow> insert B H \<turnstile> A \<Longrightarrow> H \<turnstile> A IFF B"
   by (metis Iff_def Conj_I Imp_I)
 
 lemma Iff_MP_same: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> A \<Longrightarrow> H \<turnstile> B"
   by (metis Iff_def Conj_E1 MP_same)
 
 lemma Iff_MP2_same: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B \<Longrightarrow> H \<turnstile> A"
   by (metis Iff_def Conj_E2 MP_same)
 
 lemma Iff_refl [intro!]: "H \<turnstile> A IFF A"
   by (metis Hyp Iff_I insertI1)
 
 lemma Iff_sym: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B IFF A"
   by (metis Iff_def Conj_commute)
 
 lemma Iff_trans: "H \<turnstile> A IFF B \<Longrightarrow> H \<turnstile> B IFF C \<Longrightarrow> H \<turnstile> A IFF C"
   unfolding Iff_def
   by (metis Conj_E1 Conj_E2 Conj_I Disj_Semicong_1 Disj_commute)
 
 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"
-  apply (auto simp: Iff_def insert_commute)
-  apply (metis Disj_I1 Hyp anti_deduction insertCI)
-  apply (metis Assume Disj_I1 anti_deduction)
-  done
+  by (smt (verit) AssumeH(2) Conj_E Disj_E Iff_def Neg_D rotate2)
 
 lemma Iff_E1:
   assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (A IFF B) H \<turnstile> C"
   by (metis Iff_def A B Conj_E Imp_E insert_commute thin1)
 
 lemma Iff_E2:
   assumes A: "H \<turnstile> A" and B: "insert B H \<turnstile> C" shows "insert (B IFF A) H \<turnstile> C"
   by (metis Iff_def A B Bool Conj_E2 Conj_mono Imp_E boolean_axioms.Ident)
 
 lemma Iff_MP_left: "H \<turnstile> A IFF B \<Longrightarrow> insert A H \<turnstile> C \<Longrightarrow> insert B H \<turnstile> C"
   by (metis Hyp Iff_E2 cut_same insertI1 insert_commute thin1)
 
 lemma Iff_MP_left': "H \<turnstile> A IFF B \<Longrightarrow> insert B H \<turnstile> C \<Longrightarrow> insert A H \<turnstile> C"
   by (metis Iff_MP_left Iff_sym)
 
 lemma Swap: "insert (Neg B) H \<turnstile> A \<Longrightarrow> insert (Neg A) H \<turnstile> B"
   by (metis NegNeg_D Neg_mono)
 
 lemma Cases: "insert A H \<turnstile> B \<Longrightarrow> insert (Neg A) H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
   by (metis Contra Neg_D Neg_mono)
 
 lemma Neg_Conj_E: "H \<turnstile> B \<Longrightarrow> insert (Neg A) H \<turnstile> C \<Longrightarrow> insert (Neg (A AND B)) H \<turnstile> C"
   by (metis Conj_I Swap thin1)
 
 lemma Disj_CI: "insert (Neg B) H \<turnstile> A \<Longrightarrow> H \<turnstile> A OR B"
   by (metis Contra Disj_I1 Disj_I2 Swap)
 
 lemma Disj_3I: "insert (Neg A) (insert (Neg C) H) \<turnstile> B \<Longrightarrow> H \<turnstile> A OR B OR C"
   by (metis Disj_CI Disj_commute insert_commute)
 
 lemma Contrapos1: "H \<turnstile> A IMP B \<Longrightarrow> H \<turnstile> Neg B IMP Neg A"
   by (metis Bool MP_same boolean_axioms.DisjConj boolean_axioms.Ident)
 
 lemma Contrapos2: "H \<turnstile> (Neg B) IMP (Neg A) \<Longrightarrow> H \<turnstile> A IMP B"
   by (metis Bool MP_same boolean_axioms.DisjConj boolean_axioms.Ident)
 
 lemma ContraAssumeN [intro]: "B \<in> H \<Longrightarrow> insert (Neg B) H \<turnstile> A"
   by (metis Hyp Swap thin1)
 
 lemma ContraAssume: "Neg B \<in> H \<Longrightarrow> insert B H \<turnstile> A"
   by (metis Disj_I1 Hyp anti_deduction)
 
 lemma ContraProve: "H \<turnstile> B \<Longrightarrow> insert (Neg B) H \<turnstile> A"
   by (metis Swap thin1)
 
 lemma Disj_IE1: "insert B H \<turnstile> C \<Longrightarrow> insert (A OR B) H \<turnstile> A OR C"
   by (metis Assume Disj_mono)
 
 lemmas Disj_IE1H = Disj_IE1 Disj_IE1 [THEN rotate2] Disj_IE1 [THEN rotate3] Disj_IE1 [THEN rotate4] Disj_IE1 [THEN rotate5]
                  Disj_IE1 [THEN rotate6] Disj_IE1 [THEN rotate7] Disj_IE1 [THEN rotate8]
 declare Disj_IE1H [intro!]
 
 subsection\<open>Quantifier reasoning\<close>
 
 lemma Ex_I: "H \<turnstile> A(i::=x) \<Longrightarrow> H \<turnstile> Ex i A"
   by (metis MP_same Spec special_axioms.intros)
 
 lemma Ex_E:
   assumes "insert A H \<turnstile> B" "atom i \<sharp> B" "\<forall>C \<in> H. atom i \<sharp> C"
   shows "insert (Ex i A) H \<turnstile> B"
   by (metis Exists Imp_I anti_deduction assms)
 
 lemma Ex_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 (Ex i A) H \<turnstile> B"
 proof -
   have "Ex i A = Ex i' ((i \<leftrightarrow> i') \<bullet> A)" using assms
-    apply (auto simp: Abs1_eq_iff fresh_Pair)
-    apply (metis flip_at_simps(2) fresh_at_base_permute_iff)+
-    done
+    using fresh_permute_left by (fastforce simp add: Abs1_eq_iff fresh_Pair)
   thus ?thesis
     by (metis Ex_E assms fresh_Pair)
 qed
 
 lemmas Ex_EH = Ex_E Ex_E [THEN rotate2] Ex_E [THEN rotate3] Ex_E [THEN rotate4] Ex_E [THEN rotate5]
                  Ex_E [THEN rotate6] Ex_E [THEN rotate7] Ex_E [THEN rotate8] Ex_E [THEN rotate9] Ex_E [THEN rotate10]
 declare Ex_EH [intro!]
 
 lemma Ex_mono: "insert A H \<turnstile> B \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> insert (Ex i A) H \<turnstile> (Ex i B)"
   by (auto simp add: intro: Ex_I [where x="Var i"])
 
 lemma All_I [intro!]: "H \<turnstile> A \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> All i A"
   by (auto intro: ContraProve Neg_I0)
 
 lemma All_D: "H \<turnstile> All i A \<Longrightarrow> H \<turnstile> A(i::=x)"
   by (metis Assume Ex_I NegNeg_D Neg_mono SyntaxN.Neg cut_same)
 
 lemma All_E: "insert (A(i::=x)) H \<turnstile> B \<Longrightarrow> insert (All i A) H \<turnstile> B"
   by (metis Ex_I NegNeg_D Neg_mono SyntaxN.Neg)
 
 lemma All_E': "H \<turnstile> All i A \<Longrightarrow> insert (A(i::=x)) H \<turnstile> B \<Longrightarrow> H \<turnstile> B"
   by (metis All_D cut_same)
 
 lemma All2_E: "\<lbrakk>atom i \<sharp> t; H \<turnstile> x IN t; insert (A(i::=x)) H \<turnstile> B\<rbrakk> \<Longrightarrow> insert (All2 i t A) H \<turnstile> B"
   apply (rule All_E [where x=x], auto)
   by (metis Swap thin1)
 
 lemma All2_E': "\<lbrakk>H \<turnstile> All2 i t A; H \<turnstile> x IN t; insert (A(i::=x)) H \<turnstile> B; atom i \<sharp> t\<rbrakk> \<Longrightarrow> H \<turnstile> B"
   by (metis All2_E cut_same)
 
 
 subsection\<open>Congruence rules\<close>
 
 lemma Neg_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> Neg A IFF Neg A'"
   by (metis Iff_def Conj_E1 Conj_E2 Conj_I Contrapos1)
 
 lemma Disj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A OR B IFF A' OR B'"
   by (metis Conj_E1 Conj_E2 Disj_mono Iff_I Iff_def anti_deduction)
 
 lemma Conj_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> A AND B IFF A' AND B'"
   by (metis Conj_def Disj_cong Neg_cong)
 
 lemma Imp_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> (A IMP B) IFF (A' IMP B')"
   by (metis Disj_cong Neg_cong)
 
 lemma Iff_cong: "H \<turnstile> A IFF A' \<Longrightarrow> H \<turnstile> B IFF B' \<Longrightarrow> H \<turnstile> (A IFF B) IFF (A' IFF B')"
   by (metis Iff_def Conj_cong Imp_cong)
 
 lemma Ex_cong: "H \<turnstile> A IFF A' \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (Ex i A) IFF (Ex i A')"
-  apply (rule Iff_I)
-   apply (metis Ex_mono Hyp Iff_MP_same Un_absorb Un_insert_right insertI1 thin_Un)
-  apply (metis Ex_mono Hyp Iff_MP2_same Un_absorb Un_insert_right insertI1 thin_Un)
-  done
+  by (meson Assume Ex_mono Iff_I Iff_MP_left Iff_MP_left')
 
 lemma All_cong: "H \<turnstile> A IFF A' \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (All i A) IFF (All i A')"
   by (metis Ex_cong Neg_cong)
 
 lemma Subst: "H \<turnstile> A \<Longrightarrow> \<forall>B \<in> H. atom i \<sharp> B \<Longrightarrow> H \<turnstile> A (i::=x)"
   by (metis All_D All_I)
 
 
 section\<open>Equality reasoning\<close>
 
 subsection\<open>The congruence property for @{term Eq}, and other basic properties of equality\<close>
 
 lemma Eq_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (t EQ u IMP t' EQ u')"
 proof -
   obtain v2::name and v3::name and v4::name
     where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
       and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
       and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
     by (metis obtain_fresh)
   have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)"
     by (rule Eq) (simp add: eq_cong_ax_def equality_axioms_def)
   hence "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var X2 EQ Var X4)"
     by (drule_tac i=X1 and x="Var X1" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (Var X1 EQ Var X3 IMP Var v2 EQ Var X4)"
     by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var X4)"
     using v2
     by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (Var X1 EQ Var v3 IMP Var v2 EQ Var v4)"
     using v2 v3
     by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
   hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP Var v2 EQ Var v4)"
     using v2 v3 v4
     by (drule_tac i=X1 and x=t in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (t EQ Var v3 IMP t' EQ Var v4)"
     using v2 v3 v4
     by (drule_tac i=v2 and x="t'" in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (t EQ u IMP t' EQ Var v4)"
     using v3 v4
     by (drule_tac i=v3 and x=u in Subst) simp_all
   thus ?thesis
     using v4
     by (drule_tac i=v4 and x="u'" in Subst) simp_all
 qed
 
 lemma Refl [iff]: "H \<turnstile> t EQ t"
 proof -
   have "{} \<turnstile> Var X1 EQ Var X1"
     by (rule Eq) (simp add: equality_axioms_def refl_ax_def)
   hence "{} \<turnstile> t EQ t"
     by (drule_tac i=X1 and x=t in Subst) simp_all
   thus ?thesis
     by (metis empty_subsetI thin)
 qed
 
 text\<open>Apparently necessary in order to prove the congruence property.\<close>
 lemma Sym: assumes "H \<turnstile> t EQ u" shows "H \<turnstile> u EQ t"
 proof -
   have "{} \<turnstile>  (t EQ u AND t EQ t) IMP (t EQ t IMP u EQ t)"
     by (rule Eq_cong1)
    moreover have "{t EQ u} \<turnstile> t EQ u AND t EQ t"
     by (metis Assume Conj_I Refl)
   ultimately have "{t EQ u} \<turnstile> u EQ t"
     by (metis MP_same MP Refl sup_bot_left)
   thus "H \<turnstile> u EQ t" by (metis assms cut1)
 qed
 
 lemma Sym_L: "insert (t EQ u) H \<turnstile> A \<Longrightarrow> insert (u EQ t) H \<turnstile> A"
   by (metis Assume Sym Un_empty_left Un_insert_left cut)
 
 lemma Trans: assumes "H \<turnstile> x EQ y" "H \<turnstile> y EQ z" shows "H \<turnstile> x EQ z"
 proof -
   have "\<And>H. H \<turnstile> (x EQ x AND y EQ z) IMP (x EQ y IMP x EQ z)"
     by (metis Eq_cong1 bot_least thin)
   moreover have "{x EQ y, y EQ z} \<turnstile> x EQ x AND y EQ z"
     by (metis Assume Conj_I Refl thin1)
   ultimately have "{x EQ y, y EQ z} \<turnstile> x EQ z"
     by (metis Hyp MP_same insertI1)
   thus ?thesis
     by (metis assms cut2)
 qed
 
 lemma Eq_cong:
   assumes "H \<turnstile> t EQ t'" "H \<turnstile> u EQ u'" shows "H \<turnstile> t EQ u IFF t' EQ u'"
 proof -
   { fix t t' u u'
     assume  "H \<turnstile> t EQ t'" "H \<turnstile> u EQ u'"
     moreover have "{t EQ t', u EQ u'} \<turnstile> t EQ u IMP t' EQ u'" using Eq_cong1
       by (metis Assume Conj_I MP_null insert_commute)
     ultimately have "H \<turnstile> t EQ u IMP t' EQ u'"
       by (metis cut2)
   }
   thus ?thesis
     by (metis Iff_def Conj_I assms Sym)
 qed
 
 lemma Eq_Trans_E: "H \<turnstile> x EQ u \<Longrightarrow> insert (t EQ u) H \<turnstile> A \<Longrightarrow> insert (x EQ t) H \<turnstile> A"
   by (metis Assume Sym_L Trans cut_same thin1 thin2)
 
 subsection\<open>The congruence property for @{term Mem}\<close>
 
 lemma Mem_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (t IN u IMP t' IN u')"
 proof -
   obtain v2::name and v3::name and v4::name
     where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
       and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
       and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
     by (metis obtain_fresh)
   have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Var X1 IN Var X3 IMP Var X2 IN Var X4)"
     by (metis mem_cong_ax_def equality_axioms_def insert_iff Eq)
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (Var X1 IN Var X3 IMP Var v2 IN Var X4)"
     by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (Var X1 IN Var v3 IMP Var v2 IN Var X4)"
     using v2
     by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (Var X1 IN Var v3 IMP Var v2 IN Var v4)"
     using v2 v3
     by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
   hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (t IN Var v3 IMP Var v2 IN Var v4)"
     using v2 v3 v4
     by (drule_tac i=X1 and x=t in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (t IN Var v3 IMP t' IN Var v4)"
     using v2 v3 v4
     by (drule_tac i=v2 and x=t' in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (t IN u IMP t' IN Var v4)"
     using v3 v4
     by (drule_tac i=v3 and x=u in Subst) simp_all
   thus ?thesis
     using v4
     by (drule_tac i=v4 and x=u' in Subst) simp_all
 qed
 
 lemma Mem_cong:
   assumes "H \<turnstile> t EQ t'" "H \<turnstile> u EQ u'" shows "H \<turnstile> t IN u IFF t' IN u'"
 proof -
   { fix t t' u u'
     have cong: "{t EQ t', u EQ u'} \<turnstile> t IN u IMP t' IN u'"
       by (metis AssumeH(2) Conj_I MP_null Mem_cong1 insert_commute)
   }
   thus ?thesis
     by (metis Iff_def Conj_I cut2 assms Sym)
 qed
 
 subsection\<open>The congruence properties for @{term Eats} and @{term HPair}\<close>
 
 lemma Eats_cong1: "{} \<turnstile> (t EQ t' AND u EQ u') IMP (Eats t u EQ Eats t' u')"
 proof -
   obtain v2::name and v3::name and v4::name
     where v2: "atom v2 \<sharp> (t,X1,X3,X4)"
       and v3: "atom v3 \<sharp> (t,t',X1,v2,X4)"
       and v4: "atom v4 \<sharp> (t,t',u,X1,v2,v3)"
     by (metis obtain_fresh)
   have "{} \<turnstile> (Var X1 EQ Var X2 AND Var X3 EQ Var X4) IMP (Eats (Var X1) (Var X3) EQ Eats (Var X2) (Var X4))"
     by (metis eats_cong_ax_def equality_axioms_def insert_iff Eq)
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var X3 EQ Var X4) IMP (Eats (Var X1) (Var X3) EQ Eats (Var v2) (Var X4))"
     by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var X4) IMP (Eats (Var X1) (Var v3) EQ Eats (Var v2) (Var X4))"
     using v2
     by (drule_tac i=X3 and x="Var v3" in Subst) simp_all
   hence "{} \<turnstile> (Var X1 EQ Var v2 AND Var v3 EQ Var v4) IMP (Eats (Var X1) (Var v3) EQ Eats (Var v2) (Var v4))"
     using v2 v3
     by (drule_tac i=X4 and x="Var v4" in Subst) simp_all
   hence "{} \<turnstile> (t EQ Var v2 AND Var v3 EQ Var v4) IMP (Eats t (Var v3) EQ Eats (Var v2) (Var v4))"
     using v2 v3 v4
     by (drule_tac i=X1 and x=t in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND Var v3 EQ Var v4) IMP (Eats t (Var v3) EQ Eats t' (Var v4))"
     using v2 v3 v4
     by (drule_tac i=v2 and x=t' in Subst) simp_all
   hence "{} \<turnstile> (t EQ t' AND u EQ Var v4) IMP (Eats t u EQ Eats t' (Var v4))"
     using v3 v4
     by (drule_tac i=v3 and x=u in Subst) simp_all
   thus ?thesis
     using v4
     by (drule_tac i=v4 and x=u' in Subst) simp_all
 qed
 
 lemma Eats_cong: "\<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> Eats t u EQ Eats t' u'"
   by (metis Conj_I anti_deduction Eats_cong1 cut1)
 
 lemma HPair_cong: "\<lbrakk>H \<turnstile> t EQ t'; H \<turnstile> u EQ u'\<rbrakk> \<Longrightarrow> H \<turnstile> HPair t u EQ HPair t' u'"
   by (metis HPair_def Eats_cong Refl)
 
 lemma SUCC_cong: "H \<turnstile> t EQ t' \<Longrightarrow> H \<turnstile> SUCC t EQ SUCC t'"
   by (metis Eats_cong SUCC_def)
 
 subsection\<open>Substitution for Equalities\<close>
 
 lemma Eq_subst_tm_Iff: "{t EQ u} \<turnstile> subst i t tm EQ subst i u tm"
   by (induct tm rule: tm.induct) (auto simp: Eats_cong)
 
 lemma Eq_subst_fm_Iff: "insert (t EQ u) H \<turnstile> A(i::=t) IFF A(i::=u)"
 proof -
   have "{ t EQ u } \<turnstile> A(i::=t) IFF A(i::=u)"
     by (nominal_induct A avoiding: i t u rule: fm.strong_induct)
        (auto simp: Disj_cong Neg_cong Ex_cong Mem_cong Eq_cong Eq_subst_tm_Iff)
   thus ?thesis
     by (metis Assume cut1)
 qed
 
 lemma Var_Eq_subst_Iff: "insert (Var i EQ t) H \<turnstile> A(i::=t) IFF A"
   by (metis Eq_subst_fm_Iff Iff_sym subst_fm_id)
 
 lemma Var_Eq_imp_subst_Iff: "H \<turnstile> Var i EQ t \<Longrightarrow> H \<turnstile> A(i::=t) IFF A"
   by (metis Var_Eq_subst_Iff cut_same)
 
 subsection\<open>Congruence Rules for Predicates\<close>
 
 lemma P1_cong:
   fixes tms :: "tm list"
   assumes "\<And>i t x. atom i \<sharp> tms \<Longrightarrow> (P t)(i::=x) = P (subst i x t)" and "H \<turnstile> x EQ x'"
   shows "H \<turnstile> P x IFF P x'"
 proof -
   obtain i::name where i: "atom i \<sharp> tms"
     by (metis obtain_fresh)
   have "insert (x EQ x') H  \<turnstile> (P (Var i))(i::=x) IFF (P(Var i))(i::=x')"
     by (rule Eq_subst_fm_Iff)
   thus ?thesis using assms i
     by (metis cut_same subst.simps(2))
 qed
 
 lemma P2_cong:
   fixes tms :: "tm list"
   assumes sub: "\<And>i t u x. atom i \<sharp> tms \<Longrightarrow> (P t u)(i::=x) = P (subst i x t) (subst i x u)"
       and eq:  "H \<turnstile> x EQ x'" "H \<turnstile> y EQ y'"
   shows "H \<turnstile> P x y IFF P x' y'"
 proof -
   have yy': "{ y EQ y' } \<turnstile> P x' y IFF P x' y'"
     by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub)
   have "{ x EQ x' } \<turnstile> P x y IFF P x' y"
     by (rule P1_cong [where tms="[y,x']@tms"]) (auto simp: fresh_Cons sub)
   hence "{x EQ x', y EQ y'} \<turnstile> P x y IFF P x' y'"
     by (metis Assume Iff_trans cut1 rotate2 yy')
   thus ?thesis
     by (metis cut2 eq)
  qed
 
 lemma P3_cong:
   fixes tms :: "tm list"
   assumes sub: "\<And>i t u v x. atom i \<sharp> tms \<Longrightarrow>
                    (P t u v)(i::=x) = P (subst i x t) (subst i x u) (subst i x v)"
       and eq:  "H \<turnstile> x EQ x'" "H \<turnstile> y EQ y'" "H \<turnstile> z EQ z'"
   shows "H \<turnstile> P x y z IFF P x' y' z'"
 proof -
   obtain i::name where i: "atom i \<sharp> (z,z',y,y',x,x')"
     by (metis obtain_fresh)
   have tl: "{ y EQ y', z EQ z' } \<turnstile> P x' y z IFF P x' y' z'"
     by (rule P2_cong [where tms="[z,z',y,y',x,x']@tms"]) (auto simp: fresh_Cons sub)
   have hd: "{ x EQ x' } \<turnstile> P x y z IFF P x' y z"
     by (rule P1_cong [where tms="[z,y,x']@tms"]) (auto simp: fresh_Cons sub)
   have "{x EQ x', y EQ y', z EQ z'} \<turnstile> P x y z IFF P x' y' z'"
     by (metis Assume thin1 hd [THEN cut1] tl Iff_trans)
   thus ?thesis
     by (rule cut3) (rule eq)+
 qed
 
 lemma P4_cong:
   fixes tms :: "tm list"
   assumes sub: "\<And>i t1 t2 t3 t4 x. atom i \<sharp> tms \<Longrightarrow>
                  (P t1 t2 t3 t4)(i::=x) = P (subst i x t1) (subst i x t2) (subst i x t3) (subst i x t4)"
       and eq:  "H \<turnstile> x1 EQ x1'" "H \<turnstile> x2 EQ x2'" "H \<turnstile> x3 EQ x3'" "H \<turnstile> x4 EQ x4'"
   shows "H \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'"
 proof -
   obtain i::name where i: "atom i \<sharp> (x4,x4',x3,x3',x2,x2',x1,x1')"
     by (metis obtain_fresh)
   have tl: "{ x2 EQ x2', x3 EQ x3', x4 EQ x4' } \<turnstile> P x1' x2 x3 x4 IFF P x1' x2' x3' x4'"
     by (rule P3_cong [where tms="[x4,x4',x3,x3',x2,x2',x1,x1']@tms"]) (auto simp: fresh_Cons sub)
   have hd: "{ x1 EQ x1' } \<turnstile> P x1 x2 x3 x4 IFF P x1' x2 x3 x4"
     by (auto simp: fresh_Cons sub intro!: P1_cong [where tms="[x4,x3,x2,x1']@tms"])
   have "{x1 EQ x1', x2 EQ x2', x3 EQ x3', x4 EQ x4'} \<turnstile> P x1 x2 x3 x4 IFF P x1' x2' x3' x4'"
     by (metis Assume thin1 hd [THEN cut1] tl Iff_trans)
   thus ?thesis
     by (rule cut4) (rule eq)+
 qed
 
 
 section\<open>Zero and Falsity\<close>
 
 lemma Mem_Zero_iff:
   assumes "atom i \<sharp> t" shows "H \<turnstile> (t EQ Zero) IFF (All i (Neg ((Var i) IN t)))"
 proof -
   obtain i'::name where i': "atom i' \<sharp> (t, X0, X1, i)"
     by (rule obtain_fresh)
   have "{} \<turnstile> ((Var X0) EQ Zero) IFF (All X1 (Neg ((Var X1) IN (Var X0))))"
     by (simp add: HF HF_axioms_def HF1_def)
   then have "{} \<turnstile> (((Var X0) EQ Zero) IFF (All X1 (Neg ((Var X1) IN (Var X0)))))(X0 ::= t)"
      by (rule Subst) simp
   hence "{} \<turnstile> (t EQ Zero) IFF (All i' (Neg ((Var i') IN t)))" using i'
     by simp
   also have "... = (FRESH i'. (t EQ Zero) IFF (All i' (Neg ((Var i') IN t))))"
     using i' by simp
   also have "... = (t EQ Zero) IFF (All i (Neg ((Var i) IN t)))"
     using assms by simp
   finally show ?thesis
     by (metis empty_subsetI thin)
 qed
 
 lemma Mem_Zero_E [intro!]: "insert (x IN Zero) H \<turnstile> A"
 proof -
   obtain i::name where "atom i \<sharp> Zero"
     by (rule obtain_fresh)
   hence "{} \<turnstile> All i (Neg ((Var i) IN Zero))"
     by (metis Mem_Zero_iff Iff_MP_same Refl)
   hence "{} \<turnstile> Neg (x IN Zero)"
     by (drule_tac x=x in All_D) simp
   thus ?thesis
     by (metis Contrapos2 Hyp Imp_triv_I MP_same empty_subsetI insertI1 thin)
 qed
 
 declare Mem_Zero_E [THEN rotate2, intro!]
 declare Mem_Zero_E [THEN rotate3, intro!]
 declare Mem_Zero_E [THEN rotate4, intro!]
 declare Mem_Zero_E [THEN rotate5, intro!]
 declare Mem_Zero_E [THEN rotate6, intro!]
 declare Mem_Zero_E [THEN rotate7, intro!]
 declare Mem_Zero_E [THEN rotate8, intro!]
 
 
 subsection\<open>The Formula @{term Fls}; Consistency of the Calculus\<close>
 
 definition Fls  where "Fls \<equiv> Zero IN Zero"
 
 lemma Fls_eqvt [eqvt]: "(p \<bullet> Fls) = Fls"
   by (simp add: Fls_def)
 
 lemma Fls_fresh [simp]: "a \<sharp> Fls"
   by (simp add: Fls_def)
 
 lemma Neg_I [intro!]: "insert A H \<turnstile> Fls \<Longrightarrow> H \<turnstile> Neg A"
   unfolding Fls_def
   by (rule Neg_I0) (metis Mem_Zero_E cut_same)
 
 lemma Neg_E [intro!]: "H \<turnstile> A \<Longrightarrow> insert (Neg A) H \<turnstile> Fls"
   by (rule ContraProve)
 
 declare Neg_E [THEN rotate2, intro!]
 declare Neg_E [THEN rotate3, intro!]
 declare Neg_E [THEN rotate4, intro!]
 declare Neg_E [THEN rotate5, intro!]
 declare Neg_E [THEN rotate6, intro!]
 declare Neg_E [THEN rotate7, intro!]
 declare Neg_E [THEN rotate8, intro!]
 
 text\<open>We need these because Neg (A IMP B) doesn't have to be syntactically a conjunction.\<close>
 lemma Neg_Imp_I [intro!]: "H \<turnstile> A \<Longrightarrow> insert B H \<turnstile> Fls \<Longrightarrow> H \<turnstile> Neg (A IMP B)"
   by (metis NegNeg_I Neg_Disj_I Neg_I)
 
 lemma Neg_Imp_E [intro!]: "insert (Neg B) (insert A H) \<turnstile> C \<Longrightarrow> insert (Neg (A IMP B)) H \<turnstile> C"
-apply (rule cut_same [where A=A])
- apply (metis Assume Disj_I1 NegNeg_D Neg_mono)
-apply (metis Swap Imp_I rotate2 thin1)
-done
+  using Imp_I Swap rotate2 by metis
 
 declare Neg_Imp_E [THEN rotate2, intro!]
 declare Neg_Imp_E [THEN rotate3, intro!]
 declare Neg_Imp_E [THEN rotate4, intro!]
 declare Neg_Imp_E [THEN rotate5, intro!]
 declare Neg_Imp_E [THEN rotate6, intro!]
 declare Neg_Imp_E [THEN rotate7, intro!]
 declare Neg_Imp_E [THEN rotate8, intro!]
 
 lemma Fls_E [intro!]: "insert Fls H \<turnstile> A"
   by (metis Mem_Zero_E Fls_def)
 
 declare Fls_E [THEN rotate2, intro!]
 declare Fls_E [THEN rotate3, intro!]
 declare Fls_E [THEN rotate4, intro!]
 declare Fls_E [THEN rotate5, intro!]
 declare Fls_E [THEN rotate6, intro!]
 declare Fls_E [THEN rotate7, intro!]
 declare Fls_E [THEN rotate8, intro!]
 
 lemma truth_provable: "H \<turnstile> (Neg Fls)"
   by (metis Fls_E Neg_I)
 
 lemma ExFalso: "H \<turnstile> Fls \<Longrightarrow> H \<turnstile> A"
   by (metis Neg_D truth_provable)
 
 text\<open>Thanks to Andrei Popescu for pointing out that consistency was provable here.\<close>
 proposition consistent: "\<not> {} \<turnstile> Fls"
   by (meson empty_iff eval_fm.simps(4) hfthm_sound truth_provable)
 
 
 subsection\<open>More properties of @{term Zero}\<close>
 
 lemma Eq_Zero_D:
   assumes "H \<turnstile> t EQ Zero" "H \<turnstile> u IN t" shows "H \<turnstile> A"
 proof -
   obtain i::name where  i: "atom i \<sharp> t"
     by (rule obtain_fresh)
   with assms have an: "H \<turnstile> (All i (Neg ((Var i) IN t)))"
     by (metis Iff_MP_same Mem_Zero_iff)
   have "H \<turnstile> Neg (u IN t)" using All_D [OF an, of u] i
     by simp
   thus ?thesis using assms
     by (metis Neg_D)
 qed
 
 lemma Eq_Zero_thm:
   assumes "atom i \<sharp> t" shows "{All i (Neg ((Var i) IN t))} \<turnstile> t EQ Zero"
 by (metis Assume Iff_MP2_same Mem_Zero_iff assms)
 
 lemma Eq_Zero_I:
   assumes insi: "insert ((Var i) IN t) H \<turnstile> Fls" and i1: "atom i \<sharp> t" and i2: "\<forall>B \<in> H. atom i \<sharp> B"
   shows "H \<turnstile> t EQ Zero"
 proof -
   have "H \<turnstile> All i (Neg ((Var i) IN t))"
     by (metis All_I Neg_I i2 insi)
   thus ?thesis
-    by (metis cut_same  cut [OF Eq_Zero_thm [OF i1] Hyp] insertCI insert_is_Un)
+    using Eq_Zero_thm cut1 i1 by blast
 qed
 
 subsection\<open>Basic properties of @{term Eats}\<close>
 
 lemma Eq_Eats_iff:
   assumes "atom i \<sharp> (z,t,u)"
   shows "H \<turnstile> (z EQ Eats t u) IFF (All i (Var i IN z IFF Var i IN t OR Var i EQ u))"
 proof -
   obtain v1::name and v2::name and i'::name
     where v1: "atom v1 \<sharp> (z,X0,X2,X3)"
       and v2: "atom v2 \<sharp> (t,z,X0,v1,X3)"
       and i': "atom i' \<sharp> (t,u,z,X0,v1,v2,X3)"
     by (metis obtain_fresh)
   have "{} \<turnstile> ((Var X0) EQ (Eats (Var X1) (Var X2))) IFF
              (All X3 (Var X3 IN Var X0 IFF Var X3 IN Var X1 OR Var X3 EQ Var X2))"
     by (simp add: HF HF_axioms_def HF2_def)
   hence "{} \<turnstile> ((Var X0) EQ (Eats (Var X1) (Var X2))) IFF
               (All X3 (Var X3 IN Var X0 IFF Var X3 IN Var X1 OR Var X3 EQ Var X2))"
     by (drule_tac i=X0 and x="Var X0" in Subst) simp_all
   hence "{} \<turnstile> ((Var X0) EQ (Eats (Var v1) (Var X2))) IFF
                  (All X3 (Var X3 IN Var X0 IFF Var X3 IN Var v1 OR Var X3 EQ Var X2))"
     using v1 by (drule_tac i=X1 and x="Var v1" in Subst) simp_all
   hence "{} \<turnstile> ((Var X0) EQ (Eats (Var v1) (Var v2))) IFF
                  (All X3 (Var X3 IN Var X0 IFF Var X3 IN Var v1 OR Var X3 EQ Var v2))"
     using v1 v2 by (drule_tac i=X2 and x="Var v2" in Subst) simp_all
   hence "{} \<turnstile> (((Var X0) EQ (Eats (Var v1) (Var v2))) IFF
              (All X3 (Var X3 IN Var X0 IFF Var X3 IN Var v1 OR Var X3 EQ Var v2)))(X0 ::= z)"
      by (rule Subst) simp
   hence "{} \<turnstile> ((z EQ (Eats (Var v1) (Var v2))) IFF
               (All i' (Var i' IN z IFF Var i' IN Var v1 OR Var i' EQ Var v2)))"
     using v1 v2 i' by (simp add: Conj_def Iff_def)
   hence "{} \<turnstile> (z EQ (Eats t (Var v2))) IFF
                  (All i' (Var i' IN z IFF Var i' IN t OR Var i' EQ Var v2))"
     using v1 v2 i' by (drule_tac i=v1 and x=t in Subst) simp_all
   hence "{} \<turnstile> (z EQ Eats t u) IFF
                  (All i' (Var i' IN z IFF Var i' IN t OR Var i' EQ u))"
     using v1 v2 i' by (drule_tac i=v2 and x=u in Subst) simp_all
   also have "... = (FRESH i'. (z EQ Eats t u) IFF (All i' (Var i' IN z IFF Var i' IN t OR Var i' EQ u)))"
     using i' by simp
   also have "... = (z EQ Eats t u) IFF (All i (Var i IN z IFF Var i IN t OR Var i EQ u))"
     using assms i' by simp
   finally show ?thesis
     by (rule thin0)
 qed
 
 lemma Eq_Eats_I:
   "H \<turnstile> All i (Var i IN z IFF Var i IN t OR Var i EQ u) \<Longrightarrow> atom i \<sharp> (z,t,u) \<Longrightarrow> H \<turnstile> z EQ Eats t u"
   by (metis Iff_MP2_same Eq_Eats_iff)
 
 lemma Mem_Eats_Iff:
   "H \<turnstile> x IN (Eats t u) IFF x IN t OR x EQ u"
 proof -
   obtain i::name where "atom i \<sharp> (Eats t u, t, u)"
     by (rule obtain_fresh)
   thus ?thesis
     using Iff_MP_same [OF Eq_Eats_iff, THEN All_D]
     by auto
 qed
 
 lemma Mem_Eats_I1: "H \<turnstile> u IN t \<Longrightarrow> H \<turnstile> u IN Eats t z"
   by (metis Disj_I1 Iff_MP2_same Mem_Eats_Iff)
 
 lemma Mem_Eats_I2: "H \<turnstile> u EQ z \<Longrightarrow> H \<turnstile> u IN Eats t z"
   by (metis Disj_I2 Iff_MP2_same Mem_Eats_Iff)
 
 lemma Mem_Eats_E:
   assumes A: "insert (u IN t) H \<turnstile> C" and B: "insert (u EQ z) H \<turnstile> C"
     shows "insert (u IN Eats t z) H \<turnstile> C"
-  by (rule Mem_Eats_Iff [of _ u t z, THEN Iff_MP_left']) (metis A B Disj_E)
+  by (meson A B Disj_E Iff_MP_left' Mem_Eats_Iff)
 
 lemmas Mem_Eats_EH = Mem_Eats_E Mem_Eats_E [THEN rotate2] Mem_Eats_E [THEN rotate3] Mem_Eats_E [THEN rotate4] Mem_Eats_E [THEN rotate5]
                  Mem_Eats_E [THEN rotate6] Mem_Eats_E [THEN rotate7] Mem_Eats_E [THEN rotate8]
 declare Mem_Eats_EH [intro!]
 
 lemma Mem_SUCC_I1: "H \<turnstile> u IN t \<Longrightarrow> H \<turnstile> u IN SUCC t"
   by (metis Mem_Eats_I1 SUCC_def)
 
 lemma Mem_SUCC_I2: "H \<turnstile> u EQ t \<Longrightarrow> H \<turnstile> u IN SUCC t"
   by (metis Mem_Eats_I2 SUCC_def)
 
 lemma Mem_SUCC_Refl [simp]: "H \<turnstile> k IN SUCC k"
   by (metis Mem_SUCC_I2 Refl)
 
 lemma Mem_SUCC_E:
   assumes "insert (u IN t) H \<turnstile> C" "insert (u EQ t) H \<turnstile> C" shows "insert (u IN SUCC t) H \<turnstile> C"
   by (metis assms Mem_Eats_E SUCC_def)
 
 lemmas Mem_SUCC_EH = Mem_SUCC_E Mem_SUCC_E [THEN rotate2] Mem_SUCC_E [THEN rotate3] Mem_SUCC_E [THEN rotate4] Mem_SUCC_E [THEN rotate5]
                  Mem_SUCC_E [THEN rotate6] Mem_SUCC_E [THEN rotate7] Mem_SUCC_E [THEN rotate8]
 
 lemma Eats_EQ_Zero_E: "insert (Eats t u EQ Zero) H \<turnstile> A"
   by (metis Assume Eq_Zero_D Mem_Eats_I2 Refl)
 
 lemmas Eats_EQ_Zero_EH = Eats_EQ_Zero_E Eats_EQ_Zero_E [THEN rotate2] Eats_EQ_Zero_E [THEN rotate3] Eats_EQ_Zero_E [THEN rotate4] Eats_EQ_Zero_E [THEN rotate5]
                  Eats_EQ_Zero_E [THEN rotate6] Eats_EQ_Zero_E [THEN rotate7] Eats_EQ_Zero_E [THEN rotate8]
 declare Eats_EQ_Zero_EH [intro!]
 
 lemma Eats_EQ_Zero_E2: "insert (Zero EQ Eats t u) H \<turnstile> A"
   by (metis Eats_EQ_Zero_E Sym_L)
 
 lemmas Eats_EQ_Zero_E2H = Eats_EQ_Zero_E2 Eats_EQ_Zero_E2 [THEN rotate2] Eats_EQ_Zero_E2 [THEN rotate3] Eats_EQ_Zero_E2 [THEN rotate4] Eats_EQ_Zero_E2 [THEN rotate5]
                  Eats_EQ_Zero_E2 [THEN rotate6] Eats_EQ_Zero_E2 [THEN rotate7] Eats_EQ_Zero_E2 [THEN rotate8]
 declare Eats_EQ_Zero_E2H [intro!]
 
 
 section\<open>Bounded Quantification involving @{term Eats}\<close>
 
 lemma All2_cong: "H \<turnstile> t EQ t' \<Longrightarrow> H \<turnstile> A IFF A' \<Longrightarrow> \<forall>C \<in> H. atom i \<sharp> C \<Longrightarrow> H \<turnstile> (All2 i t A) IFF (All2 i t' A')"
   by (metis All_cong Imp_cong Mem_cong Refl)
 
 lemma All2_Zero_E [intro!]: "H  \<turnstile> B \<Longrightarrow> insert (All2 i Zero A) H \<turnstile> B"
   by (rule thin1)
 
 lemma All2_Eats_I_D:
   "atom i \<sharp> (t,u) \<Longrightarrow> { All2 i t A, A(i::=u)} \<turnstile> (All2 i (Eats t u) A)"
     apply (auto, auto intro!: Ex_I [where x="Var i"])
     apply (metis Assume thin1 Var_Eq_subst_Iff [THEN Iff_MP_same])
     done
 
 lemma All2_Eats_I:
   "\<lbrakk>atom i \<sharp> (t,u); H \<turnstile> All2 i t A; H \<turnstile> A(i::=u)\<rbrakk> \<Longrightarrow> H \<turnstile> (All2 i (Eats t u) A)"
   by (rule cut2 [OF All2_Eats_I_D], auto)
 
 lemma All2_Eats_E1:
   "\<lbrakk>atom i \<sharp> (t,u); \<forall>C \<in> H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (All2 i (Eats t u) A) H \<turnstile> All2 i t A"
   by auto (metis Assume Ex_I Imp_E Mem_Eats_I1 Neg_mono subst_fm_id)
 
 lemma All2_Eats_E2:
   "\<lbrakk>atom i \<sharp> (t,u); \<forall>C \<in> H. atom i \<sharp> C\<rbrakk> \<Longrightarrow> insert (All2 i (Eats t u) A) H \<turnstile> A(i::=u)"
   by (rule All_E [where x=u]) (auto intro: ContraProve Mem_Eats_I2)
 
 lemma All2_Eats_E:
   assumes i: "atom i \<sharp> (t,u)"
       and B: "insert (All2 i t A) (insert (A(i::=u)) H) \<turnstile> B"
     shows "insert (All2 i (Eats t u) A) H \<turnstile> B"
   using i
   apply (rule cut_thin [OF All2_Eats_E2, where HB = "insert (All2 i (Eats t u) A) H"], auto)
   apply (rule cut_thin [OF All2_Eats_E1 B], auto)
   done
 
 lemma All2_SUCC_I:
   "atom i \<sharp> t \<Longrightarrow> H \<turnstile> All2 i t A \<Longrightarrow> H \<turnstile> A(i::=t) \<Longrightarrow> H \<turnstile> (All2 i (SUCC t) A)"
   by (simp add: SUCC_def All2_Eats_I)
 
 lemma All2_SUCC_E:
   assumes "atom i \<sharp> t"
       and "insert (All2 i t A) (insert (A(i::=t)) H) \<turnstile> B"
     shows "insert (All2 i (SUCC t) A) H \<turnstile> B"
   by (simp add: SUCC_def All2_Eats_E assms)
 
 lemma All2_SUCC_E':
   assumes "H \<turnstile> u EQ SUCC t"
       and "atom i \<sharp> t" "\<forall>C \<in> H. atom i \<sharp> C"
       and "insert (All2 i t A) (insert (A(i::=t)) H) \<turnstile> B"
     shows "insert (All2 i u A) H \<turnstile> B"
   by (metis All2_SUCC_E Iff_MP_left' Iff_refl All2_cong assms)
 
 section\<open>Induction\<close>
 
 lemma Ind:
   assumes j: "atom (j::name) \<sharp> (i,A)"
   and prems: "H \<turnstile> A(i::=Zero)" "H \<turnstile> All i (All j (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))))"
   shows "H \<turnstile> A"
 proof -
   have  "{A(i::=Zero), All i (All j (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))))} \<turnstile> All i A"
     by (metis j hfthm.Ind ind anti_deduction insert_commute)
   hence "H \<turnstile> (All i A)"
     by (metis cut2 prems)
   thus ?thesis
     by (metis All_E' Assume subst_fm_id)
 qed
 
 end