theory LamFun
imports "../Nominal2" Quotient_Option
begin

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  binds x in l

thm lam.distinct
thm lam.induct
thm lam.exhaust
thm lam.fv_defs
thm lam.bn_defs
thm lam.perm_simps
thm lam.eq_iff
thm lam.fv_bn_eqvt
thm lam.size_eqvt
thm lam.size
thm lam_raw.size
thm lam.fresh

primrec match_Var_raw where
  "match_Var_raw (Var_raw x) = Some x"
| "match_Var_raw (App_raw x y) = None"
| "match_Var_raw (Lam_raw n t) = None"

quotient_definition
  "match_Var :: lam \<Rightarrow> name option"
is match_Var_raw

lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
  by (rule, induct_tac a b rule: alpha_lam_raw.induct, simp_all)

lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]

primrec match_App_raw where
  "match_App_raw (Var_raw x) = None"
| "match_App_raw (App_raw x y) = Some (x, y)"
| "match_App_raw (Lam_raw n t) = None"

quotient_definition
  "match_App :: lam \<Rightarrow> (lam \<times> lam) option"
is match_App_raw

lemma [quot_respect]:
  "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw"
  by (intro fun_relI, induct_tac a b rule: alpha_lam_raw.induct, simp_all)

lemmas match_App_simps = match_App_raw.simps[quot_lifted]

definition next_name where
  "next_name (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"

lemma lam_eq: "Lam a t = Lam b s \<longleftrightarrow> (a \<leftrightarrow> b) \<bullet> t = s"
  apply (simp add: lam.eq_iff Abs_eq_iff alphas)
  sorry

lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)"
  by (auto simp add: lam_eq)

definition
  "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then
    (let z = next_name (S, t) in Some (z, THE s. t = Lam z s)) else None)"

lemma match_Lam_simps:
  "match_Lam S (Var n) = None"
  "match_Lam S (App l r) = None"
  "match_Lam S (Lam z s) = (let n = next_name (S, (Lam z s)) in Some (n, (z \<leftrightarrow> n) \<bullet> s))"
  apply (simp_all add: match_Lam_def lam.distinct)
  apply (auto simp add: lam_eq)
  done

lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
by (induct x rule: lam.induct) (simp_all add: match_App_simps)


lemma lam_some: "match_Lam S x = Some (n, t) \<Longrightarrow> x = Lam n t"
  apply (induct x rule: lam.induct)
  apply (simp add: match_Lam_simps)
  apply (simp add: match_Lam_simps)
  apply (simp add: match_Lam_simps Let_def lam_eq)
  apply clarify
  done

function subst where
"subst v s t = (
  case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow>
  case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow>
  case match_Lam (v, s) t of Some (n, s') \<Rightarrow> Lam n (subst v s s') | None \<Rightarrow> undefined)"
print_theorems
thm subst_rel.intros[no_vars]
by pat_completeness auto

termination apply (relation "measure (\<lambda>(_, _, t). size t)")
  apply auto[1]
  apply (case_tac a) apply simp
  apply (frule lam_some) apply (simp add: lam.size)
  apply (case_tac a) apply simp
  apply (frule app_some) apply (simp add: lam.size)
  apply (case_tac a) apply simp
  apply (frule app_some) apply (simp add: lam.size)
done

lemma subst_eqs:
  "subst y s (Var x) = (if x = y then s else (Var x))"
  "subst y s (App l r) = App (subst y s l) (subst y s r)"
  "subst y s (Lam x t) =
    (let n = next_name ((y, s), Lam x t) in Lam n (subst y s ((x \<leftrightarrow> n) \<bullet> t)))"
  apply (subst subst.simps)
  apply (simp only: match_Var_simps option.simps)
  apply (subst subst.simps)
  apply (simp only: match_App_simps option.simps prod.simps match_Var_simps)
  apply (subst subst.simps)
  apply (simp only: match_App_simps option.simps prod.simps match_Var_simps match_Lam_simps Let_def)
  done

lemma subst_eqvt:
  "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"
  proof (induct v s t rule: subst.induct)
    case (1 v s t)
    show ?case proof (cases t rule: lam.exhaust)
      fix n
      assume "t = Var n"
      then show ?thesis by (simp add: match_Var_simps)
    next
      fix l r
      assume "t = App l r"
      then show ?thesis
        apply (simp only: subst_eqs lam.perm_simps)
        apply (subst 1(2)[of "(l, r)" "l" "r"])
        apply (simp add: match_Var_simps)
        apply (simp add: match_App_simps)
        apply (rule refl)
        apply (subst 1(3)[of "(l, r)" "l" "r"])
        apply (simp add: match_Var_simps)
        apply (simp add: match_App_simps)
        apply (rule refl)
        apply (rule refl)
        done
    next
      fix n t'
      assume "t = Lam n t'"
      then show ?thesis
        apply (simp only: subst_eqs lam.perm_simps Let_def)
        apply (subst 1(1))
        apply (simp add: match_Var_simps)
        apply (simp add: match_App_simps)
        apply (simp add: match_Lam_simps Let_def)
        apply (rule refl)
        (* next_name is not equivariant :( *)
        apply (simp only: lam_eq)
        sorry
    qed
  qed

lemma subst_eqvt':
  "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"
  apply (induct t arbitrary: v s rule: lam.induct)
  apply (simp only: subst_eqs lam.perm_simps eqvts)
  apply (simp only: subst_eqs lam.perm_simps)
  apply (simp only: subst_eqs lam.perm_simps Let_def)
  apply (simp only: lam_eq)
  sorry

lemma subst_eq3:
  "atom x \<sharp> (y, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"
  apply (simp only: subst_eqs Let_def)
  apply (simp only: lam_eq)
  (* p # y   p # s   subst_eqvt *)
  (* p \<bullet> -p \<bullet> (subst y s t) = subst y s t *)
  sorry

end