theory Scratch imports
  Main
begin

datatype 'a trm = Var 'a | Fn 'a "('a trm list)"
type_synonym 'a subst = "('a \<times> 'a trm) list"

abbreviation (input) eq where "eq x \<equiv> \<lambda>y. x = y"

fun assoc :: "'a \<Rightarrow> 'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" where
  "assoc v d [] = d"
  | "assoc v d ((u, t) # xs) = (if (v = u) then t else assoc v d xs)"

primrec apply_subst_list :: "('a trm) list \<Rightarrow> 'a subst \<Rightarrow> ('a trm) list"  and
        apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60) where
  "apply_subst_list [] s = []"
| "apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)"
| "(Var v) \<triangleleft> s = assoc v (Var v) s"
| "(Fn f xs) \<triangleleft> s = (Fn f (apply_subst_list xs s))"


primrec occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" and
        occ_list :: "'a trm \<Rightarrow> 'a trm list \<Rightarrow> bool" where
  "occ u (Var v)     = False"
| "occ u (Fn f xs)   = (if (list_ex (eq u) xs) then True else (occ_list u xs))"
| "occ_list u []     = False"
| "occ_list u (x#xs) = (if occ u x then True else occ_list u xs)"

lemma subst_no_occ:
  shows "\<not> occ (Var v) t \<Longrightarrow> Var v \<noteq> t \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
    and "\<not> occ_list (Var v) ts \<Longrightarrow> (\<And>u. u \<in> set ts \<Longrightarrow> Var v \<noteq> u) \<Longrightarrow> apply_subst_list ts [(v,s)] = ts"
proof (induct rule: trm.inducts)
  case Var then show ?case by simp
next
  case Nil_trm then show ?case by simp
next
  case Cons_trm then show ?case by (simp split: split_if_asm)
next
  case Fn then show ?case apply (auto simp: list_ex_iff split: split_if_asm)