Theory Incompleteness.Coding

chapter‹De Bruijn Syntax, Quotations, Codes, V-Codes›

theory Coding
imports SyntaxN
begin

declare fresh_Nil [iff]

section ‹de Bruijn Indices (locally-nameless version)›

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 ⇒ nat ⇒ name ⇒ 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 ♯ e ⟹ name ∉ set e"
  by (metis List.finite_set fresh_finite_set_at_base fresh_set)

lemma lookup_notin: "x ∉ set e ⟹ lookup e n x = DBVar x"
  by (induct e arbitrary: n) auto

lemma lookup_in:
  "x ∈ set e ⟹ ∃k. lookup e n x = DBInd k ∧ n ≤ k ∧ k < n + length e"
  by (induction e arbitrary: n) force+

lemma lookup_fresh: "x ♯ lookup e n y ⟷ y ∈ set e ∨ x ≠ atom y"
  by (induct arbitrary: n rule: lookup.induct) (auto simp: pure_fresh fresh_at_base)

lemma lookup_eqvt[eqvt]: "(p ∙ lookup xs n x) = lookup (p ∙ xs) (p ∙ n) (p ∙ x)"
  by (induct xs arbitrary: n) (simp_all add: permute_pure)

lemma lookup_inject [iff]: "(lookup e n x = lookup e n y) ⟷ x = y"
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 ⇒ tm ⇒ 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 ♯ trans_tm e t ⟷ i ♯ t ∨ i ∈ atom ` set e"
  by (induct t rule: tm.induct, auto simp: lookup_fresh fresh_at_base)

lemma trans_tm_forget: "atom i ♯ t ⟹ trans_tm [i] t = trans_tm [] t"
  by (induct t rule: tm.induct, auto simp: fresh_Pair)

nominal_function (invariant "λ(xs, _) y. atom ` set xs ♯* y")
  trans_fm :: "name list ⇒ fm ⇒ 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 ♯ e ⟹ 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 (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 ♯ trans_fm e A ⟷ i ♯ A ∨ i ∈ atom ` set e"
  by (nominal_induct A avoiding: e rule: fm.strong_induct, auto simp: fresh_at_base)

abbreviation DBConj :: "dbfm ⇒ dbfm ⇒ dbfm"
  where "DBConj t u ≡ 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) ⟷ t = u"
proof (induct t arbitrary: 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) ⟷ 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' ♯ (e, name)"
    assume "atom name ♯ fm' ∨ 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 ♯ fm'"
      have eq1: "(name ↔ name') ∙ trans_fm (name' # e) fm' = trans_fm (name' # e) fm'"
        by (simp add: flip_fresh_fresh name)
      have eq2: "(name ↔ name') ∙ ([[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 ↔ name') ∙ fm'"]
        by (simp add: flip_fresh_fresh) (metis Abs1_eq(3))
    qed
  qed
qed

lemma trans_fm_perm:
  assumes c: "atom c ♯ (i,j,A,B)"
  and     t: "trans_fm [i] A = trans_fm [j] B"
  shows "(i ↔ c) ∙ A = (j ↔ c) ∙ B"
proof -
  have c_fresh1: "atom c ♯ trans_fm [i] A"
    using c by (auto simp: supp_Pair)
  moreover
  have i_fresh: "atom i ♯ trans_fm [i] A"
    by auto
  moreover
  have c_fresh2: "atom c ♯ trans_fm [j] B"
    using c by (auto simp: supp_Pair)
  moreover
  have j_fresh: "atom j ♯ trans_fm [j] B"
    by auto
  ultimately have "((i ↔ c) ∙ (trans_fm [i] A)) = ((j ↔ c) ∙ trans_fm [j] B)"
    by (simp only: flip_fresh_fresh t)
  then have "trans_fm [c] ((i ↔ c) ∙ A) = trans_fm [c] ((j ↔ c) ∙ B)"
    by simp
  then show "(i ↔ c) ∙ A = (j ↔ c) ∙ B" by simp
qed

section‹Abstraction and Substitution on de Bruijn Formulas›

nominal_function abst_dbtm :: "name ⇒ nat ⇒ dbtm ⇒ 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 ⇒ name ⇒ dbtm ⇒ dbtm"
  where
   "subst_dbtm u x DBZero = DBZero"
 | "subst_dbtm u x (DBVar name) = (if x = name then u else DBVar name)"
 | "subst_dbtm u x (DBInd j) = DBInd j"
 | "subst_dbtm u x (DBEats t1 t2) = DBEats (subst_dbtm u x t1) (subst_dbtm u x 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 ⟷ atom i ♯ 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‹Well-Formed Formulas›

nominal_function abst_dbfm :: "name ⇒ nat ⇒ dbfm ⇒ 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 ⇒ name ⇒ dbfm ⇒ dbfm"
  where
   "subst_dbfm u x (DBMem t1 t2) = DBMem (subst_dbtm u x t1) (subst_dbtm u x t2)"
 | "subst_dbfm u x (DBEq t1 t2) =  DBEq (subst_dbtm u x t1) (subst_dbtm u x t2)"
 | "subst_dbfm u x (DBDisj A1 A2) = DBDisj (subst_dbfm u x A1) (subst_dbfm u x A2)"
 | "subst_dbfm u x (DBNeg A) = DBNeg (subst_dbfm u x A)"
 | "subst_dbfm u x (DBEx A) = DBEx (subst_dbfm u x 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 ⟷ atom i ♯ t"
  by (induct t rule: dbfm.induct) (auto simp: fresh_iff_non_subst_dbtm)


section‹Well formed terms and formulas (de Bruijn representation)›

subsection‹Well-Formed Terms›

inductive wf_dbtm :: "dbtm ⇒ bool"
  where
    Zero:  "wf_dbtm DBZero"
  | Var:   "wf_dbtm (DBVar name)"
  | Eats:  "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ 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 "∃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 ⟷ (∃t::tm. x = trans_tm [] t)"
  by (metis wf_dbtm_imp_is_tm wf_dbtm_trans_tm)

subsection‹Well-Formed Formulas›

inductive wf_dbfm :: "dbfm ⇒ bool"
  where
    Mem:   "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ wf_dbfm (DBMem t1 t2)"
  | Eq:    "wf_dbtm t1 ⟹ wf_dbtm t2 ⟹ wf_dbfm (DBEq t1 t2)"
  | Disj:  "wf_dbfm A1 ⟹ wf_dbfm A2 ⟹ wf_dbfm (DBDisj A1 A2)"
  | Neg:   "wf_dbfm A ⟹ wf_dbfm (DBNeg A)"
  | Ex:    "wf_dbfm A ⟹ wf_dbfm (DBEx (abst_dbfm name 0 A))"

equivariance wf_dbfm

lemma atom_fresh_abst_dbtm [simp]: "atom i ♯ abst_dbtm i n t"
  by (induct t rule: dbtm.induct) (auto simp: pure_fresh)

lemma atom_fresh_abst_dbfm [simp]: "atom i ♯ abst_dbfm i n A"
  by (nominal_induct A arbitrary: n rule: dbfm.strong_induct) auto

text‹Setting up strong induction: "avoiding" for name. Necessary to allow some proofs to go through›
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)
  by (metis append_Cons length_Cons)

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 ≠ j ⟹ 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 "∃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 ⟷ (∃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 ♯ u ⟹ 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 ≠ name' ⟹ atom name' ♯ u ⟹
   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 ≠ name' ⟹ atom name' ♯ u ⟹
   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 ♯ e ⟹ 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)
  by (metis abst_dbtm_fresh_ignore atom_eq_iff dbtm_subst_ignore lookup_fresh)

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 dbfm_abst_swap_subst simp flip: abst_trans_fm)
  done

lemma subst_fm_trans_commute_eq:
  "du = trans_tm [] u ⟹ subst_dbfm du i (trans_fm [] A) = trans_fm [] (A(i::=u))"
  by (metis subst_fm_trans_commute)


section‹Quotations›

fun htuple :: "nat ⇒ hf"  where
   "htuple 0 = ⟨0,0⟩"
 | "htuple (Suc k) = ⟨0, htuple k⟩"

fun HTuple :: "nat ⇒ tm"  where
   "HTuple 0 = HPair Zero Zero"
 | "HTuple (Suc k) = HPair Zero (HTuple k)"

lemma eval_tm_HTuple [simp]:  "⟦HTuple n⟧e = htuple n"
  by (induct n) auto

lemma fresh_HTuple [simp]: "x ♯ HTuple n"
  by (induct n) auto

lemma HTuple_eqvt[eqvt]: "(p ∙ HTuple n) = HTuple (p ∙ n)"
  by (induct n, auto simp: HPair_eqvt permute_pure)

lemma htuple_nonzero [simp]: "htuple k ≠ 0"
  by (induct k) auto

lemma htuple_inject [iff]: "htuple i = htuple j ⟷ 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 ‹Quotations of de Bruijn terms›

definition nat_of_name :: "name ⇒ nat"
  where "nat_of_name x = nat_of (atom x)"

lemma nat_of_name_inject [simp]: "nat_of_name n1 = nat_of_name n2 ⟷ n1 = n2"
  by (metis nat_of_name_def atom_components_eq_iff atom_eq_iff sort_of_atom_eq)

definition name_of_nat :: "nat ⇒ name"
  where "name_of_nat n ≡ 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 ≠ ORD_OF i"
  by (metis Not_Ord_hpair Ord_ord_of eval_tm_HPair eval_tm_ORD_OF)

text‹Infinite support, so we cannot use nominal primrec.›
function quot_dbtm :: "dbtm ⇒ 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]: "⟦quot_dbtm t⟧e = ⟦quot_dbtm u⟧e ⟷ 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 ⟷ t=u"
  by (metis quot_dbtm_inject_lemma)

subsection ‹Quotations of de Bruijn formulas›

text‹Infinite support, so we cannot use nominal primrec.›
function quot_dbfm :: "dbfm ⇒ 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 ⟹ htuple n = ⟨0, htuple (n - 1)⟩"
  by (metis Suc_diff_1 htuple.simps(2))

lemma HTuple_minus_1: "n > 0 ⟹ HTuple n = HPair Zero (HTuple (n - 1))"
  by (metis Suc_diff_1 HTuple.simps(2))

lemmas HTS = HTuple_minus_1 HTuple.simps ― ‹for freeness reasoning on codes›

lemma quot_dbfm_inject_lemma [simp]: "⟦quot_dbfm A⟧e = ⟦quot_dbfm B⟧e ⟷ 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 ⇒ tm"  (‹«_»›)

instantiation tm :: quot
begin
  definition quot_tm :: "tm ⇒ tm"
    where "quot_tm t = quot_dbtm (trans_tm [] t)"
  
  instance ..
end

lemma quot_dbtm_fresh [simp]: "s ♯ (quot_dbtm t)"
  by (induct t rule: dbtm.induct) auto

lemma quot_tm_fresh [simp]: fixes t::tm shows "s ♯ «t»"
  by (simp add: quot_tm_def)

lemma quot_Zero [simp]: "«Zero» = Zero"
  by (simp add: quot_tm_def)

lemma quot_Var: "«Var x» = SUCC (ORD_OF (nat_of_name x))"
  by (simp add: quot_tm_def)

lemma quot_Eats: "«Eats x y» = HPair (HTuple 1) (HPair «x» «y»)"
  by (simp add: quot_tm_def)

text‹irrelevance of the environment for quotations, because they are ground terms›
lemma eval_quot_dbtm_ignore:
    "⟦quot_dbtm t⟧e = ⟦quot_dbtm t⟧e'"
  by (induct t rule: dbtm.induct) auto

lemma eval_quot_dbfm_ignore:
    "⟦quot_dbfm A⟧e = ⟦quot_dbfm A⟧e'"
  by (induct A rule: dbfm.induct) (auto intro: eval_quot_dbtm_ignore)


instantiation fm :: quot
begin
  definition quot_fm :: "fm ⇒ tm"
    where "quot_fm A = quot_dbfm (trans_fm [] A)"
  
  instance ..
end

lemma quot_dbfm_fresh [simp]: "s ♯ (quot_dbfm A)"
  by (induct A rule: dbfm.induct) auto

lemma quot_fm_fresh [simp]: fixes A::fm shows "s ♯ «A»"
  by (simp add: quot_fm_def)

lemma quot_fm_permute [simp]: fixes A:: fm shows "p ∙ «A» = «A»"
  by (metis fresh_star_def perm_supp_eq quot_fm_fresh)

lemma quot_Mem: "«x IN y» = HPair (HTuple 0) (HPair («x») («y»))"
  by (simp add: quot_fm_def quot_tm_def)

lemma quot_Eq: "«x EQ y» = HPair (HTuple 2) (HPair («x») («y»))"
  by (simp add: quot_fm_def quot_tm_def)

lemma quot_Disj: "«A OR B» = HPair (HTuple 3) (HPair («A») («B»))"
  by (simp add: quot_fm_def)

lemma quot_Neg: "«Neg A» = HPair (HTuple 4) («A»)"
  by (simp add: quot_fm_def)

lemma quot_Ex: "«Ex i A» = HPair (HTuple 5) (quot_dbfm (trans_fm [i] A))"
  by (simp add: quot_fm_def)

lemma eval_quot_fm_ignore: fixes A:: fm shows "⟦«A»⟧e = ⟦«A»⟧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‹Definitions Involving Coding›

definition q_Var :: "name ⇒ hf"
  where "q_Var i ≡ succ (ord_of (nat_of_name i))"

definition q_Ind :: "hf ⇒ hf"
  where "q_Ind k ≡  ⟨htuple 6, k⟩"

abbreviation Q_Eats :: "tm ⇒ tm ⇒ tm"
  where "Q_Eats t u ≡ HPair (HTuple (Suc 0)) (HPair t u)"

definition q_Eats :: "hf ⇒ hf ⇒ hf"
  where "q_Eats x y ≡ ⟨htuple 1, x, y⟩"

abbreviation Q_Succ :: "tm ⇒ tm"
  where "Q_Succ t ≡ Q_Eats t t"

definition q_Succ :: "hf ⇒ hf"
  where "q_Succ x ≡ q_Eats x x"

lemma quot_Succ: "«SUCC x» = Q_Succ «x»"
  by (auto simp: SUCC_def quot_Eats)

abbreviation Q_HPair :: "tm ⇒ tm ⇒ tm"
  where "Q_HPair t u ≡
           Q_Eats (Q_Eats Zero (Q_Eats (Q_Eats Zero u) t))
                  (Q_Eats (Q_Eats Zero t) t)"

definition q_HPair :: "hf ⇒ hf ⇒ hf"
  where "q_HPair x y ≡
           q_Eats (q_Eats 0 (q_Eats (q_Eats 0 y) x))
                  (q_Eats (q_Eats 0 x) x)"

abbreviation Q_Mem :: "tm ⇒ tm ⇒ tm"
  where "Q_Mem t u ≡ HPair (HTuple 0) (HPair t u)"

definition q_Mem :: "hf ⇒ hf ⇒ hf"
  where "q_Mem x y ≡ ⟨htuple 0, x, y⟩"

abbreviation Q_Eq :: "tm ⇒ tm ⇒ tm"
  where "Q_Eq t u ≡ HPair (HTuple 2) (HPair t u)"

definition q_Eq :: "hf ⇒ hf ⇒ hf"
  where "q_Eq x y ≡ ⟨htuple 2, x, y⟩"

abbreviation Q_Disj :: "tm ⇒ tm ⇒ tm"
  where "Q_Disj t u ≡ HPair (HTuple 3) (HPair t u)"

definition q_Disj :: "hf ⇒ hf ⇒ hf"
  where "q_Disj x y ≡ ⟨htuple 3, x, y⟩"

abbreviation Q_Neg :: "tm ⇒ tm"
  where "Q_Neg t ≡ HPair (HTuple 4) t"

definition q_Neg :: "hf ⇒ hf"
  where "q_Neg x ≡ ⟨htuple 4, x⟩"

abbreviation Q_Conj :: "tm ⇒ tm ⇒ tm"
  where "Q_Conj t u ≡ Q_Neg (Q_Disj (Q_Neg t) (Q_Neg u))"

definition q_Conj :: "hf ⇒ hf ⇒ hf"
  where "q_Conj t u ≡ q_Neg (q_Disj (q_Neg t) (q_Neg u))"

abbreviation Q_Imp :: "tm ⇒ tm ⇒ tm"
  where "Q_Imp t u ≡ Q_Disj (Q_Neg t) u"

definition q_Imp :: "hf ⇒ hf ⇒ hf"
  where "q_Imp t u ≡ q_Disj (q_Neg t) u"

abbreviation Q_Ex :: "tm ⇒ tm"
  where "Q_Ex t ≡ HPair (HTuple 5) t"

definition q_Ex :: "hf ⇒ hf"
  where "q_Ex x ≡ ⟨htuple 5, x⟩"

abbreviation Q_All :: "tm ⇒ tm"
  where "Q_All t ≡ Q_Neg (Q_Ex (Q_Neg t))"

definition q_All :: "hf ⇒ hf"
  where "q_All x ≡ 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' ⟷ x=x' ∧ y=y'"
  by (metis hpair_iff q_Eats_def)

lemma quot_subst_eq: "«A(i::=t)» = 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 ⊢ x EQ x' ⟹ H ⊢ Q_Succ x EQ Q_Succ x'"
  by (metis HPair_cong Refl)

  
section‹Quotations are Injective›

subsection‹Terms›

lemma eval_tm_inject [simp]: fixes t::tm shows "⟦«t»⟧ e = ⟦«u»⟧ e ⟷ 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‹Formulas›

lemma eval_fm_inject [simp]: fixes A::fm shows "⟦«A»⟧ e = ⟦«B»⟧ e ⟷ 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 α) 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 α)
  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‹The set ‹Γ› of Definition 1.1, constant terms used for coding›

inductive coding_tm :: "tm ⇒ bool"
  where
    Ord:    "∃i. x = ORD_OF i ⟹ coding_tm x"
  | HPair:  "coding_tm x ⟹ coding_tm y ⟹ 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 «A»"
  by (metis quot_dbfm_coding quot_fm_def)

inductive coding_hf :: "hf ⇒ bool"
  where
    Ord:    "∃i. x = ord_of i ⟹ coding_hf x"
  | HPair:  "coding_hf x ⟹ coding_hf y ⟹ coding_hf (⟨x,y⟩)"

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 (⟨x,y⟩)"

lemma coding_tm_hf [simp]: "coding_tm t ⟹ coding_hf ⟦t⟧e"
  by (induct t rule: coding_tm.induct) auto

  
section ‹V-Coding for terms and formulas, for the Second Theorem›

text‹Infinite support, so we cannot use nominal primrec.›
function vquot_dbtm :: "name set ⇒ dbtm ⇒ tm"
  where
   "vquot_dbtm V DBZero = Zero"
 | "vquot_dbtm V (DBVar name) = (if name ∈ 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 ♯ vquot_dbtm V tm ⟷ i ♯ tm ∨ i ∉ atom ` V"
  by (induct tm rule: dbtm.induct) (auto simp: fresh_at_base pure_fresh)

text‹Infinite support, so we cannot use nominal primrec.›
function vquot_dbfm :: "name set ⇒ dbfm ⇒ 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 ♯ vquot_dbfm V fm ⟷ i ♯ fm ∨ i ∉ atom ` V"
  by (induct fm rule: dbfm.induct) (auto simp: HPair_def HTuple_minus_1)

class vquot =
  fixes vquot :: "'a ⇒ name set ⇒ tm"  (‹⌊_⌋_›  [0,1000]1000)

instantiation tm :: vquot
begin
  definition vquot_tm :: "tm ⇒ name set ⇒ 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 "⌊t⌋{} = «t»"
  by (simp add: vquot_tm_def quot_tm_def)

lemma vquot_dbtm_eq: "atom ` V ∩ supp t = atom ` W ∩ supp t ⟹ 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 ⇒ name set ⇒ tm"
    where "vquot_fm A V = vquot_dbfm V (trans_fm [] A)"
  instance ..
end

lemma vquot_fm_fresh [simp]: fixes A::fm shows "i ♯ ⌊A⌋V ⟷ i ♯ A ∨ i ∉ 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 "⌊A⌋{} = «A»"
  by (simp add: vquot_fm_def quot_fm_def)

lemma vquot_dbfm_eq: "atom ` V ∩ supp A = atom ` W ∩ supp A ⟹ 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 ∉ supp A ⟹ ⌊A⌋(insert i V) = ⌊A⌋V"
  by (auto simp: vquot_fm_def supp_conv_fresh intro: vquot_dbfm_eq)

declare HTuple.simps [simp del]

end