Theory Bumping

(* Title:        Part of the proof of compactness of first-order logic following Harrison's one in
 *               HOL-Light
 * Author:       Sophie Tourret <sophie.tourret at inria.fr>, 2024 *)

theory Bumping
imports 
  FOL_Semantics
  "HOL-Library.Nat_Bijection"
begin

(* Diverges from hol-light version by reusing a nat × nat ⇒ nat encoding available in Isabelle/HOL 
 * /!\ The encoding is not the same (but it serves the same purpose)
 * The hol-light names numpair, numfst and numsnd have been kept to help with the translation *)
abbreviation numpair where
  ‹numpair m n ≡ prod_encode (m,n)›

abbreviation numfst where
  ‹numfst k ≡ fst (prod_decode k)›

abbreviation numsnd where
  ‹numsnd k ≡ snd (prod_decode k)›

(* bumpmod in hol-light *)
definition bump_intrp :: "'m intrp ⇒ 'm intrp" where
  ‹bump_intrp ℳ = Abs_intrp ((dom ℳ), (λk zs. (intrp_fn ℳ) (numsnd k) zs), (intrp_rel ℳ))›

lemma bump_dom [simp]: ‹dom (bump_intrp ℳ) = dom ℳ›
proof -
  have is_struct: ‹struct (dom ℳ)› 
    by (simp add: intrp_is_struct)
  then show ?thesis unfolding bump_intrp_def using dom_Abs_is_fst by blast
qed

lemma bump_intrp_fn [simp]: ‹intrp_fn (bump_intrp ℳ) (numpair 0 f) ts = intrp_fn ℳ f ts›
proof -
  have is_struct: ‹struct (dom ℳ)›
    by (smt (verit, best) intrp_is_struct struct_def)
  then show ?thesis unfolding bump_intrp_def by simp
qed

lemma bump_intrp_rel [simp]: ‹intrp_rel (bump_intrp ℳ) n = intrp_rel ℳ n›
  unfolding bump_intrp_def
  by (smt (verit) intrp_is_struct intrp_rel_Abs_is_snd_snd struct_def)

(* bumpterm in hol-light *)
fun bump_nterm :: "nterm ⇒ nterm" where
  ‹bump_nterm (Var x) = Var x›
| ‹bump_nterm (Fun f ts) = Fun (numpair 0 f) (map bump_nterm ts)›

(* bumpform in hol-light *)
fun bump_form :: "form ⇒ form" where
  ‹bump_form ❙⊥ = ❙⊥›
| ‹bump_form (Atom p ts) = Atom p (map bump_nterm ts)›
| ‹bump_form (φ ❙⟶ ψ) = (bump_form φ) ❙⟶ (bump_form ψ)›
| ‹bump_form (❙∀ x❙. φ) = ❙∀ x❙. (bump_form φ)›


lemma bumpterm: ‹⟦t⟧⇗ℳ,β⇖ = ⟦bump_nterm t⟧⇗bump_intrp ℳ,β⇖›
proof (induct t)
  case (Var x)
  then show ?case
    by simp
next
  case (Fun f ts)
  then have ‹intrp_fn ℳ f [⟦t⟧⇗ℳ,β⇖. t ← ts] =
    intrp_fn ℳ f [⟦bump_nterm t⟧⇗bump_intrp ℳ,β⇖. t ← ts]›
    by (metis (no_types, lifting) map_eq_conv)
  also have ‹... = 
    intrp_fn (bump_intrp ℳ) (numpair 0 f) [⟦bump_nterm t⟧⇗bump_intrp ℳ,β⇖. t ← ts]›
    by (simp add: bump_intrp_fn)
  also have ‹... = 
    intrp_fn (bump_intrp ℳ) (numpair 0 f) [⟦t⟧⇗bump_intrp ℳ,β⇖. t ← (map bump_nterm ts)]›
    using map_eq_conv by fastforce
  ultimately show ?case by auto
qed

lemma bump_intrp_rel_holds: ‹(map (λt. ⟦t⟧⇗ℳ,β⇖) ts ∈ intrp_rel ℳ n) =
  (map ((λt. ⟦t⟧⇗bump_intrp ℳ,β⇖) ∘ bump_nterm) ts ∈ intrp_rel (bump_intrp ℳ) n)›
proof -
  have ‹(λt. ⟦t⟧⇗ℳ,β⇖) = (λt. ⟦t⟧⇗bump_intrp ℳ,β⇖) ∘ bump_nterm›
    using bumpterm by fastforce
  then have ‹map (λt. ⟦t⟧⇗ℳ,β⇖) ts = map ((λt. ⟦t⟧⇗bump_intrp ℳ,β⇖) ∘ bump_nterm) ts›
    by simp
  then show ?thesis
    by (metis bump_intrp_rel)
qed

lemma bumpform: ‹ℳ❙, β ⊨ φ = (bump_intrp ℳ)❙, β ⊨ (bump_form φ)›
proof (induct φ arbitrary: β)
  case Bot
  then show ?case
    unfolding bump_intrp_def by auto
next
  case (Atom x1 x2)
  then show ?case
    using bump_intrp_rel_holds by auto
next
  case (Implies φ1 φ2)
  then show ?case
    unfolding bump_intrp_def by auto
next
  case (Forall x1 φ)
  have ‹(∀a ∈ dom ℳ. (bump_intrp ℳ)❙,β(x1 := a) ⊨ bump_form φ) = 
    (∀a ∈ dom ℳ. ℳ❙,β(x1 := a) ⊨ φ)›
    using Forall by presburger
  then show ?case
    by simp
qed

lemma functions_form_bumpform: ‹(f, m) ∈ functions_form (bump_form φ) ⟹
  ∃k. (f = numpair 0 k) ∧ (k, m) ∈ functions_form φ›
proof (induct φ)
  case (Atom p ts)
  then have ‹∃t∈set ts. (f, m) ∈ functions_term (bump_nterm t)› by simp
  then obtain t where t_in: ‹t ∈ set ts› and fm_in_t: ‹(f, m) ∈ functions_term (bump_nterm t)›
      by blast
  have ‹∃k. f = numpair 0 k ∧ (k, m) ∈ functions_term t›
    using fm_in_t
  proof (induction t)
    case (Var x)
    then show ?case by auto
  next
    case (Fun g us)
    have t_in_disj: ‹functions_term (bump_nterm (Fun g us)) = 
      {((numpair 0 g), length us)} ∪ (⋃ u ∈ set us. functions_term (bump_nterm u))›
      by simp
    then show ?case
    proof (cases "(f, m) = ((numpair 0 g), length us)")
      case True
      then show ?thesis by auto
    next
      case False
      then have ‹(f, m) ∈ (⋃ u ∈ set us. functions_term (bump_nterm u))›
        using t_in_disj
        using Fun.prems by blast
      then show ?thesis
        using Fun(1) by fastforce
    qed
  qed
  then have ‹∃k. f = numpair 0 k ∧ (∃x∈set ts. (k, m) ∈ functions_term x)›
    using t_in by blast
  then show ?case using Atom by simp
qed auto

lemma bumpform_interpretation: ‹is_interpretation (language {φ}) ℳ ⟹
  is_interpretation (language {(bump_form φ)}) (bump_intrp ℳ)›
  unfolding is_interpretation_def language_def
  by (metis bump_dom bump_intrp_fn fst_conv functions_form_bumpform lang_singleton language_def)

(* unbumpterm in hol-light *)
fun unbump_nterm :: "nterm ⇒ nterm" where
  ‹unbump_nterm (Var x) = Var x›
| ‹unbump_nterm (Fun f ts) = Fun (numsnd f) (map unbump_nterm ts)›

(* unbumpform in hol-light *)
fun unbump_form :: "form ⇒ form" where
  ‹unbump_form ❙⊥ = ❙⊥›
| ‹unbump_form (Atom p ts) = Atom p (map unbump_nterm ts)›
| ‹unbump_form (φ ❙⟶ ψ) = (unbump_form φ) ❙⟶ (unbump_form ψ)›
| ‹unbump_form (❙∀ x❙. φ) = ❙∀ x❙. (unbump_form φ)›

lemma unbumpterm [simp]: "unbump_nterm (bump_nterm t) = t"
  by (induct t) (simp add: list.map_ident_strong)+

lemma unbumpform [simp]: ‹unbump_form (bump_form φ) = φ›
  by (induct φ) (simp add: list.map_ident_strong)+

(* unbumpmod in hol-light *)
definition unbump_intrp :: "'m intrp ⇒ 'm intrp" where
  ‹unbump_intrp ℳ = Abs_intrp (dom ℳ, (λk zs. (intrp_fn ℳ) (numpair 0 k) zs), (intrp_rel ℳ))›

(* UNBUMPMOD_TERM in hol-light *)
lemma unbump_term_intrp: ‹⟦bump_nterm t⟧⇗ℳ,β⇖ = ⟦t⟧⇗unbump_intrp ℳ,β⇖›
proof (induct t)
  case (Fun f ts)
  then show ?case 
    unfolding unbump_intrp_def
    by (smt (verit, best) bump_nterm.simps(2) concat_map eval.simps(2) intrp_fn_Abs_is_fst_snd 
        intrp_is_struct list.map_cong0 struct_def)
qed simp

(*  UNBUMPMOD in hol-light *)
lemma unbump_holds: ‹(ℳ❙,β ⊨ bump_form φ) = (unbump_intrp ℳ❙,β ⊨ φ)›
proof (induct φ arbitrary: β)
  case Bot
  then show ?case
    by auto
next
  case (Atom p ts)
  then show ?case
    unfolding unbump_intrp_def using bump_intrp_def bumpform dom_Abs_is_fst functions_form_bumpform
        holds_indep_intrp_if intrp_fn_Abs_is_fst_snd intrp_is_struct intrp_rel_Abs_is_snd_snd
        struct_def
    by (smt (verit, ccfv_SIG) prod_encode_inverse snd_conv)
next
  case (Implies φ1 φ2)
  then show ?case
    by auto
next
  case (Forall x φ)
  then show ?case
    by (smt (verit, best) bump_form.simps(4) dom_Abs_is_fst holds.simps(4) intrp_is_struct 
        struct_def unbump_intrp_def)
qed

abbreviation numlist where
  ‹numlist ns ≡ list_encode ns›

fun num_of_term :: "nterm ⇒ nat" where
  ‹num_of_term (Var x) = numpair 0 x›
| ‹num_of_term (Fun f ts) = numpair 1 (numpair f (numlist (map num_of_term ts)))›

(* to move in AFP theory First-Order Terms.Term *)
lemma term_induct2:
  "(⋀x y. P (Var x) (Var y))
    ⟹ (⋀x g us. P (Var x) (Fun g us))
    ⟹ (⋀f ts y. P (Fun f ts) (Var y)) 
    ⟹ (⋀f ts g us. (⋀p q. p ∈ set ts ⟹ q ∈ set us ⟹ P p q) ⟹ P (Fun f ts) (Fun g us))
    ⟹ P t1 t2"
proof (induction t2 arbitrary: t1)
  case (Var y)
  then show ?case by (metis is_FunE is_VarE)
next
  case (Fun g us)
  then have ‹p ∈ set ts ⟹ q ∈ set us ⟹ P p q› for ts p q
    by blast
  then show ?case
    using Fun by (metis is_FunE is_VarE)
qed
(************************************************)

lemma num_of_term_inj: ‹num_of_term s = num_of_term t ⟷ s = t›
proof (induction s t rule: term_induct2)
  case (4 f ts g us)
  have ‹(Fun f ts = Fun g us) ⟹ num_of_term (Fun f ts) = num_of_term (Fun g us)›
    by auto
  moreover {
    assume ‹num_of_term (Fun f ts) = num_of_term (Fun g us)›
    then have ‹numpair f (numlist (map num_of_term ts)) = numpair g (numlist (map num_of_term us))›
      by auto
    then have fun_eq: ‹f = g› and nl_eq: ‹numlist (map num_of_term ts) = (numlist (map num_of_term us))›
      by auto
    then have "map num_of_term ts = map num_of_term us"
      using list_encode_eq by blast
    then have args_eq: ‹ts = us›
      using 4 by (metis list.inj_map_strong)
    have ‹Fun f ts = Fun g us›
      using fun_eq args_eq by simp
  }
  ultimately show ?case by auto
qed auto

fun num_of_form :: "form ⇒ nat" where
  ‹num_of_form ❙⊥ = numpair 0 0›
| ‹num_of_form (Atom p ts) = numpair 1 (numpair p (numlist (map num_of_term ts)))›
| ‹num_of_form (φ ❙⟶ ψ) = numpair 2 (numpair (num_of_form φ) (num_of_form ψ))›
| ‹num_of_form (❙∀x❙. φ) = numpair 3 (numpair x (num_of_form φ))›

lemma numlist_num_of_term: ‹numlist (map num_of_term ts) = (numlist (map num_of_term us)) ≡ ts = us›
  by (smt (verit) list.inj_map_strong list_encode_eq num_of_term_inj)

lemma num_of_form_inj: ‹num_of_form φ = num_of_form ψ ⟷ φ = ψ›
proof 
  show ‹num_of_form φ = num_of_form ψ ⟹ φ = ψ›
  proof (induct φ arbitrary: ψ rule: num_of_form.induct)
    case 1
    then show ?case
      using num_of_form.elims num_of_form.simps(1)  zero_neq_numeral zero_neq_one
      by (metis prod.sel(1) prod_encode_inverse)
  next
    case (2 p ts)
    then show ?case
    proof (cases ψ)
      case Bot
      then show ?thesis
        using "2" num_of_term_inj by fastforce
    next
      case (Atom q us)
      then show ?thesis
        using "2" by (simp add: numlist_num_of_term)
    next
      case (Implies ψ1 ψ2)
      then show ?thesis
        using "2" by simp
    next
      case (Forall y ψ1)
      then have ‹∃k. num_of_form ψ = numpair 3 k› 
        by auto
      moreover have ‹∃k'. num_of_form (Atom p ts) = numpair 1 k'›
        by auto
      ultimately show ?thesis using "2" by force
    qed
  next
    case (3 φ1 φ2)
    then show ?case
      by (smt (verit, best) One_nat_def Pair_inject Suc_eq_numeral form.distinct(11) 
          form.distinct(7) form.sel(3) form.sel(4) nat.simps(3) num_of_form.elims numeral_3_eq_3
          numerals(2) prod_encode_eq)
  next
    case (4 x φ1)
    then show ?case
      by (smt (verit, ccfv_SIG) One_nat_def Zero_neq_Suc num_of_form.elims num_of_form.simps(4)
          numeral_3_eq_3 numerals(2) old.nat.inject old.prod.inject prod_encode_eq)
  qed
qed auto

consts term_of_num :: "nat ⇒ nterm"
specification (term_of_num) ‹∀n. term_of_num n = (THE t. num_of_term t = n)›
  using num_of_term_inj by force

(* TERM_OF_NUM in hol-light *)
lemma term_of_num_of_term [simp]: ‹term_of_num(num_of_term t) = t›
  using num_of_term_inj HOL.nitpick_choice_spec by auto

consts form_of_num :: "nat ⇒ form"
specification (form_of_num) ‹∀n. form_of_num n = (THE φ. num_of_form φ = n)›
  using num_of_form_inj by force

(* FORM_OF_NUM in hol-light *)
lemma form_of_num_of_form [simp]: ‹form_of_num (num_of_form φ) = φ›
  using num_of_form_inj HOL.nitpick_choice_spec by auto

end