Theory Polymorphic_Term

theory Polymorphic_Term
  imports 
    IsaFoR_Nonground_Term
    Polymorphic_Ground_Term
begin


section ‹Polymorphic terms›

datatype ('f, poly_term_vars: 'v, 'tyf, poly_term_type_vars: 'tyv) poly_term =
  PVar (the_PVar: 'v) |
  PFun
    (fun_sym: 'f) (type_args: "('tyf, 'tyv) term list")
    (args: "('f, 'v, 'tyf, 'tyv) poly_term list")
where
  "args (PVar _) = []"

type_synonym ('f, 'v, 'tyf, 'tyv) poly_subst = 
  "('v ⇒ ('f, 'v, 'tyf, 'tyv) poly_term) × ('tyv ⇒ ('tyf, 'tyv) term)"

primrec poly_term_subst ::
  "('f, 'v, 'tyf, 'tyv) poly_term ⇒
   ('f, 'v, 'tyf, 'tyv) poly_subst ⇒
   ('f, 'v, 'tyf, 'tyv) poly_term" (infixl ‹⋅p› 67) where
  "PVar x ⋅p σ = fst σ x"
| "PFun f αs ts ⋅p σ = PFun f (map (λα. α ⋅ snd σ) αs) (map (λt. t ⋅p σ) ts)"

definition compose_subst (infixl ‹⊙› 70) where
  "σ ⊙ σ' ≡ (λx. PVar x ⋅p σ ⋅p σ', snd σ ∘⇩s snd σ')"

fun update_subst :: 
  "('f, 'v, 'tyf, 'tyv) poly_subst ⇒
   'v ⇒
   ('f, 'v, 'tyf, 'tyv) poly_term ⇒
   ('f, 'v, 'tyf, 'tyv) poly_subst" (‹_⟦_ := _⟧› [1000, 0, 50] 70) where
  "update_subst (σ, σ') x update = (σ(x:=update), σ')"

abbreviation id_subst where
  "id_subst ≡ (PVar, Var)"

abbreviation apply_subst (infixl "⋅v" 69) where
  "apply_subst x σ ≡ PVar x ⋅p σ"

abbreviation poly_term_is_ground where
  "poly_term_is_ground t ≡ poly_term_vars t = {} ∧ poly_term_type_vars t = {}"

fun poly_to_ground ::  "('f, 'v, 'tyf, 'tyv) poly_term ⇒ ('f, 'tyf) poly_gterm" where
  "poly_to_ground (PFun f αs ts) = PGFun f (map term.to_ground αs) (map poly_to_ground ts)"

fun poly_from_ground :: "('f, 'tyf) poly_gterm ⇒ ('f, 'v, 'tyf, 'tyv) poly_term" where
  "poly_from_ground (PGFun f αs ts) = PFun f (map term.from_ground αs) (map poly_from_ground ts)"

abbreviation is_PVar where
 "is_PVar t ≡ ∃x. t = PVar x"

abbreviation is_PFun where
  "is_PFun t ≡ ¬is_PVar t"

lemma is_PFunE [elim]:
  "is_PFun t ⟹ (⋀f αs ts. t = PFun f αs ts ⟹ P) ⟹ P"
  by (cases t) auto

lemma subst_id_subst [simp]: "t ⋅p id_subst = t"
  by (induction t) (auto simp: list.map_ident_strong)

lemma subst_two: "t ⋅p σ ⋅p σ' = t ⋅p (λx. fst σ x ⋅p σ', snd σ ∘⇩s snd σ')"
  by (induction t) auto

lemma poly_term_subst_eq_conv:
  "t ⋅p (σ, σ') = t ⋅p (τ, τ') ⟷
    (∀x ∈ poly_term_vars t. σ x = τ x) ∧ (∀x ∈ poly_term_type_vars t. σ' x = τ' x)"
  by (induction t) (auto simp: term_subst_eq_conv)

lemma obtain_PFun_not_in_finite_set:
  fixes T :: "('f, 'v, 'tyf, 'tyv) poly_term set" 
  assumes "finite T"
  shows "∃t. t ∉ T ∧ is_PFun t"
proof -

  define arg_lengths where
    "arg_lengths ≡ length ` poly_term.args ` {t ∈ T. is_PFun t}"

  then have "finite arg_lengths"
    using assms
    unfolding arg_lengths_def
    by auto

  then obtain n where n: "∀n' ∈ arg_lengths. n' < n"
    using finite_nat_set_iff_bounded
    by auto

  define t :: "('f, 'v, 'tyf, 'tyv) poly_term" where
    "t = PFun (SOME f. True) [] (replicate n (PFun (SOME f. True) [] []))"

  show ?thesis
  proof (intro exI conjI)
    show "t ∉ T"
      using n
      unfolding t_def arg_lengths_def
      by auto
  next
    show "is_PFun t"
      unfolding t_def
      by simp
  qed
qed

lemma poly_term_type_vars_subst_update:
  fixes t
  assumes "poly_term_type_vars u = {}"
  shows "poly_term_type_vars (t ⋅p σ⟦x := u⟧) ⊆ poly_term_type_vars (t ⋅p σ)"
  using assms
proof (induction t)
  case (PVar x)
  then show ?case
    by (cases σ) auto
next
  case (PFun f αs ts)
  then show ?case
    by (cases σ) fastforce
qed


subsection ‹Substitution interpretations›

global_interpretation poly_term: base_substitution where
  subst = "(⋅p)" and vars = poly_term_vars and id_subst = id_subst and
  comp_subst = "(⊙)" and apply_subst = "(⋅v)" and is_ground = poly_term_is_ground
proof unfold_locales
  fix t and σ⇩1 σ⇩2 :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "t ⋅p σ⇩1 ⊙ σ⇩2 = t ⋅p σ⇩1 ⋅p σ⇩2"
    unfolding compose_subst_def
    by (induction t) auto
next
  fix σ⇩1 σ⇩2 σ⇩3 :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "σ⇩1 ⊙ σ⇩2 ⊙ σ⇩3 = σ⇩1 ⊙ (σ⇩2 ⊙ σ⇩3)"
    unfolding compose_subst_def
    by (simp add: subst_two term.comp_subst.left.assoc)
next
  fix t :: "('f, 'v, 'tyf, 'tyv) poly_term"
  assume "poly_term_is_ground t"  
  
  then show "∀σ. t ⋅p σ = t"
  proof (induction t)
    case (PVar x)

    then show ?case
      by simp
  next
    case (PFun f αs ts)

    moreover have "⋀σ. map (λα. α ⋅ σ) αs = αs"
      using PFun(2)
      by (induction αs) auto

    moreover have "⋀σ σ'. map (λt. t ⋅p (σ, σ')) ts = ts"
      using PFun
      by (induction ts) auto

    ultimately show ?case
      by simp
  qed
next
  fix t and σ⇩1 σ⇩2 :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "t ⋅p σ⇩1 ⊙ σ⇩2 = t ⋅p σ⇩1 ⋅p σ⇩2"
    unfolding compose_subst_def
    by (induction t) auto
next
  fix t and σ :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "poly_term_vars (t ⋅p σ) = ⋃ (poly_term_vars ` (λx. PVar x ⋅p σ) ` poly_term_vars t)"
    by (induction t) auto
next
  fix t and γ :: "('f, 'v, 'tyf, 'tyv) poly_subst"
  assume "poly_term_is_ground (t ⋅p γ)"

  then show "∀x∈poly_term_vars t. poly_term_is_ground (x ⋅v γ)"
    by (induction t) auto
qed (auto simp: compose_subst_def)

global_interpretation poly_term: subst_update where
  subst = "(⋅p)" and vars = poly_term_vars and id_subst = id_subst and
  is_ground = poly_term_is_ground and apply_subst = "(⋅v)" and 
  comp_subst = "(⊙)" and subst_update = update_subst
proof unfold_locales
  fix x update and σ :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "x ⋅v σ⟦x := update⟧ = update"
    by (cases σ) simp
next
  fix σ :: "('f, 'v, 'tyf, 'tyv) poly_subst" and x y :: 'v and update

  assume "x ≠ y"

  then show "x ⋅v σ⟦y := update⟧ = x ⋅v σ"
    by (cases σ) simp
next
  fix x update σ and t :: "('f, 'v, 'tyf, 'tyv) poly_term"

  assume "x ∉ poly_term_vars t"

  then show "t ⋅p σ⟦x := update⟧ = t ⋅p σ"
    by (cases σ, induction t) simp_all
next
  fix σ :: "('f, 'v, 'tyf, 'tyv) poly_subst" and x
  
  show "σ⟦x := x ⋅v σ⟧ = σ"
    by (cases σ) simp
next
  fix σ :: "('f, 'v, 'tyf, 'tyv) poly_subst" and x t t'

  show "(σ⟦x := t⟧)⟦x := t'⟧ = σ⟦x := t'⟧"
    by (cases σ) simp
qed

global_interpretation poly_term: finite_variables where
  subst = "(⋅p)" and vars = poly_term_vars and id_subst = id_subst and
  is_ground = poly_term_is_ground and apply_subst = "(⋅v)" and 
  comp_subst = "(⊙)"
  by unfold_locales simp

(* TODO: Do without infinite when Unification exists *)
global_interpretation poly_term: base_variables_in_base_imgu where
  subst = "(⋅p)" and id_subst = id_subst and is_ground = poly_term_is_ground and
  vars = "poly_term_vars :: ('f, 'v, 'tyf, 'tyv) poly_term ⇒ 'v :: infinite set" and
  apply_subst = "(⋅v)" and comp_subst = "(⊙)" and subst_update = update_subst
proof unfold_locales

  show "infinite (UNIV :: 'v set)"
    using infinite_UNIV 
    by simp
next
  fix t and σ :: "('f, 'v, 'tyf, 'tyv) poly_subst"

  show "∃x. t ⋅p σ = x ⋅v id_subst ⟹ ∃x. t = x ⋅v id_subst"
    by (cases t) auto
qed

(* TODO: get rid of infinite *)
global_interpretation poly_term: nonground_term where
  term_subst = "(⋅p)" and id_subst = id_subst and
  term_vars = "poly_term_vars :: ('f, 'v, 'tyf, 'tyv) poly_term ⇒ 'v :: infinite set" and
  term_is_ground = poly_term_is_ground and apply_subst = "(⋅v)" and comp_subst = "(⊙)" and
  subst_update = update_subst and term_from_ground = poly_from_ground and
  term_to_ground = poly_to_ground
proof unfold_locales                                       
  fix t :: "('f, 'v, 'tyf, 'tyv) poly_term"

  show "poly_term_is_ground t ⟷ (∀σ. t ⋅p σ = t)"
  proof (induction t)
    case (PVar x)

    then show ?case
      by auto
  next
    case (PFun f αs ts)

    show ?case 
    proof (rule iffI)
      assume "poly_term_is_ground (PFun f αs ts)"

      then show " ∀σ. PFun f αs ts ⋅p σ = PFun f αs ts"
        using poly_term.subst_ident_if_ground
        by blast
    next
      assume subst_ident: "∀σ. PFun f αs ts ⋅p σ = PFun f αs ts"

     {
        fix t
        assume "t ∈ set ts"

        moreover then have "∀σ. t ⋅p σ = t"
          using subst_ident map_eq_conv 
          by fastforce

        ultimately have "poly_term_is_ground t"
          using PFun
          by presburger
      }

      moreover {
        fix α

        assume "α ∈ set αs"

        moreover then have "∀σ. α ⋅ σ = α"
          using subst_ident map_eq_conv
          by (metis (no_types, lifting) list.map_ident poly_term.inject(2)
              poly_term_subst.simps(2) prod.collapse prod.simps(1))

        ultimately have "term.is_ground α"
          by (meson term.all_subst_ident_iff_ground)
      }

      ultimately show "poly_term_is_ground (PFun f αs ts)"
        by auto
    qed
  qed
next

  {
    fix t :: "('f, 'v, 'tyf, 'tyv) poly_term"
    assume t_is_ground: "poly_term_is_ground t"

    have "∃g. poly_from_ground g = t"
    proof(intro exI)

      from t_is_ground
      show "poly_from_ground (poly_to_ground t) = t"
        by (induction t) (simp_all add: map_idI)
    qed
  }

  moreover have "poly_term_is_ground (poly_from_ground t)" for t :: "('f, 'tyf) poly_gterm"
    by (induction t) simp

  ultimately show
    "{t :: ('f, 'v, 'tyf, 'tyv) poly_term. poly_term_is_ground t} = range poly_from_ground"
    by fast
next
  fix t⇩G :: "('f, 'tyf) poly_gterm"


  show "poly_to_ground (poly_from_ground t⇩G) = t⇩G"
    by (induction t⇩G) (auto simp: map_idI)
next
  fix t :: "('f, 'v, 'tyf, 'tyv) poly_term" and ts :: "('f, 'v, 'tyf, 'tyv) poly_term set"

  assume "finite ts" "¬poly_term_is_ground t"

  then show "∃σ. t ⋅p σ ≠ t ∧ t ⋅p σ ∉ ts"
  proof(induction t arbitrary: ts)
    case (PVar x)

    obtain t' where t': "t' ∉ ts" "is_PFun t'"
      using PVar.prems(1)
      by (metis PVar.prems(1) obtain_PFun_not_in_finite_set)

    define σ :: "('f, 'v, 'tyf, 'tyv) poly_subst" where "σ ≡ (λx. t', Var)"

    have "PVar x ⋅p σ ≠ PVar x"
      using t'
      unfolding σ_def
      by auto

    moreover have "PVar x ⋅p σ ∉ ts"
      using t'
      unfolding σ_def
      by simp

    ultimately show ?case
      using PVar
      by blast
  next
    case (PFun f αs args)

    show ?case
    proof (cases "∃a ∈ set args. ¬poly_term_is_ground a")
      case True

      obtain a where a: "a ∈ set args" and a_vars: "¬poly_term_is_ground a"
        using True
        by auto

      then obtain σ where
        σ: "a ⋅p σ ≠ a" and
        a_σ_not_in_args: "a ⋅p σ ∉ ⋃ (set ` poly_term.args ` ts)"
        by (metis PFun.IH PFun.prems(1) List.finite_set finite_UN finite_imageI)

      then have "PFun f αs args ⋅p σ ≠ PFun f αs args"
        using a map_eq_conv
        by fastforce

      moreover have "PFun f αs args ⋅p σ ∉ ts"
        using a a_σ_not_in_args
        by auto

      ultimately show ?thesis
        by blast
    next
      case False

      then obtain α where α: "α ∈ set αs" and α_vars: "¬term.is_ground α"
        using PFun(3)
        by auto

      then obtain σ where
        σ: "α ⋅ σ ≠ α" and
        α_σ_not_in_args: "α ⋅ σ ∉ ⋃ (set ` poly_term.type_args ` ts)"
        by (metis PFun.prems(1) UN_simps(10) finite_UN list.set_finite term.exists_non_ident_subst)

      then have "PFun f αs args ⋅p (PVar, σ) ≠ PFun f αs args"
        using α map_eq_conv
        by fastforce

      moreover have "PFun f αs args ⋅p (PVar, σ) ∉ ts"
        using α α_σ_not_in_args
        by auto

      ultimately show ?thesis
        by blast
    qed    
  qed
next
  fix ρ :: "('f, 'v, 'tyf, 'tyv) poly_subst" and t

  assume ρ: "poly_term.is_renaming ρ"

  then show "inj (λx. x ⋅v ρ) ∧ (∀x. ∃x'. x ⋅v ρ = x' ⋅v id_subst)"
    unfolding poly_term.is_renaming_def inj_def
    by (metis poly_term.exhaust poly_term.inject(1) poly_term.simps(4) poly_term.subst_comp_subst 
        poly_term_subst.simps(2) subst_id_subst)

  then have x': "⋀x. ∃x'. x ⋅v ρ = x' ⋅v id_subst"
    by auto

  show "poly_term_vars (t ⋅p ρ) = poly_term.rename ρ ` poly_term_vars t"
  proof (induction t)
    case (PVar x)

    have "x ⋅v ρ = PVar (poly_term.rename ρ x)"
      using x'[of x]
      unfolding poly_term.rename_def[OF ρ]
      by auto

    then show ?case
      by simp
  next
    case (PFun f αs ts)
    then show ?case
      by auto
  qed
next
  fix u t :: "('f, 'v, 'tyf, 'tyv) poly_term" and γ x
  assume "poly_term_is_ground u" "poly_term_is_ground (t ⋅p γ)" "x ∈ poly_term_vars t"

  then show "poly_term_is_ground (t ⋅p γ⟦x := u⟧)"
  proof (induction t)
    case (PVar y)

    then show ?case 
      by (cases γ) auto
  next
    case (PFun f αs ts)

    have "poly_term_type_vars (PFun f αs ts ⋅p γ⟦x := u⟧) = {}"
      using PFun.prems PFun.IH
      by (cases γ) (metis poly_term_type_vars_subst_update  subset_empty)        
    
    then show ?case
      using PFun(2, 3)
      by (cases γ) (auto simp: poly_term.base_vars_subst)
  qed
next

  show "∃t. poly_term_is_ground t"
    by (rule exI[of _ "PFun (SOME f. True) [] []"]) simp
next

  let ?upd = "λ(x, b) σ. σ⟦x := b⟧"

  have snd_fold: "snd (fold ?upd us σ) = snd σ" for us and σ :: "('f,'v,'tyf,'tyv) poly_subst"
  proof (induction us arbitrary: σ)
    case Nil
    then show ?case by simp
  next
    case (Cons a us)

    show ?case
      using Cons
      by (cases a, cases σ) auto
  qed

  fix us us' :: "('v × ('f, 'v, 'tyf, 'tyv) poly_term) list"

  assume "⋀x. x ⋅v fold ?upd us id_subst ⊙ fold ?upd us' id_subst = x ⋅v id_subst"

  then have "fst (fold ?upd us id_subst ⊙ fold ?upd us' id_subst) = PVar"
    unfolding compose_subst_def
    by auto

  moreover have "snd (fold ?upd us id_subst ⊙ fold ?upd us' id_subst) = Var"
    by (simp add: compose_subst_def snd_fold)

  ultimately show "fold ?upd us id_subst ⊙ fold ?upd us' id_subst = id_subst"
    unfolding compose_subst_def
    by auto
qed


subsection ‹Generic term interpretations›

interpretation poly_term: term_interpretation where
  subterms = args and fun_sym = fun_sym and extra = type_args and is_var = poly_term.is_Var and
  Fun = PFun and size = size
proof unfold_locales
  fix t' t :: "('f, 'v, 'tyf, 'tyv) poly_term"
  assume "t' ∈ set (poly_term.args t)"

  then show "size t' < size t"
    by (induction t) (auto simp: elem_size_size_list_size less_Suc_eq trans_less_add2)
next
  fix t :: "('f, 'v :: infinite, 'tyf, 'tyv) poly_term"

  show "¬ poly_term.is_Var t ⟷ (∃f e ts. t = PFun f e ts)"
  proof (induction t)
    case (PVar x)
    then show ?case 
      by (metis poly_term.set_intros(3) poly_term.distinct(1) fst_conv all_not_in_conv
          poly_term_subst.simps(1))
  next
    case (PFun f αs ts)
    then show ?case 
      by simp
  qed
qed fastforce+


end