theory Lambda imports "../Nominal2" begin

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)

nominal_primrec lam2_rec where
  "lam2_rec faa fll xs (Var n) (Var m) = ((n, m) \<in> set xs)"
| "lam2_rec faa fll xs (Var n) (App l r) = False"
| "lam2_rec faa fll xs (Var n) (Lam [x]. t) = False"
| "lam2_rec faa fll xs (App l r) (Var n) = False"
| "lam2_rec faa fll xs (App l1 r1) (App l2 r2) = faa l1 r1 l2 r2"
| "lam2_rec faa fll xs (App l r) (Lam [x]. t) = False"
| "lam2_rec faa fll xs (Lam [x]. t) (Var n) = False"
| "lam2_rec faa fll xs (Lam [x]. t) (App l1 r1) = False"
| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
     (\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
        \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
     lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = fll x t y s"
| "(atom x \<sharp> (xs, Lam [y]. s) \<and> atom y \<sharp> (x, xs, Lam [x]. t) \<and>
     \<not>(\<forall>x' y' t' s'. atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow> atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow> Lam [x]. t = Lam [x']. t' \<longrightarrow> Lam [y]. s = Lam [y']. s'
        \<longrightarrow> fll x t y s = fll x' t' y' s')) \<Longrightarrow>
     lam2_rec faa fll xs (Lam [x]. t) (Lam [y]. s) = False"
  apply (simp add: eqvt_def lam2_rec_graph_def)
  apply (rule, perm_simp, rule, rule)
  defer
  apply (simp_all)[53]
  apply clarify
  apply metis
  apply simp
  apply (case_tac x)
  apply (rule_tac y="d" and c="(c, e)" in lam.strong_exhaust)
  apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
  apply simp_all[3]
  apply (metis, metis, metis)
  apply (rule_tac y="e" and c="(c, d)" in lam.strong_exhaust)
  apply simp_all[3]
  apply (metis, metis, metis)
  apply (rule_tac y="e" and c="(name, c, d)" in lam.strong_exhaust)
  apply simp_all[2]
  apply (metis, metis)
  apply (thin_tac "\<And>faa fll xs n m. x = (faa, fll, xs, Var n, Var m) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs n l r. x = (faa, fll, xs, Var n, App l r) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs n xa t. x = (faa, fll, xs, Var n, Lam [xa]. t) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l1 r1 l2 r2. x = (faa, fll, xs, App l1 r1, App l2 r2) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l r n. x = (faa, fll, xs, App l r, Var n) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs l r xa t. x = (faa, fll, xs, App l r, Lam [xa]. t) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs xa t n. x = (faa, fll, xs, Lam [xa]. t, Var n) \<Longrightarrow> P")
  apply (thin_tac "\<And>faa fll xs xa t l1 r1. x = (faa, fll, xs, Lam [xa]. t, App l1 r1) \<Longrightarrow> P")
  apply (drule_tac x="name" in meta_spec)+
  apply (drule_tac x="c" in meta_spec)+
  apply (drule_tac x="namea" in meta_spec)+
  apply (drule_tac x="lama" in meta_spec)
  apply (drule_tac x="lama" in meta_spec)
  apply (drule_tac x="lam" in meta_spec)+
  apply (drule_tac x="b" in meta_spec)+
  apply (drule_tac x="a" in meta_spec)+
  apply (case_tac "
(\<forall>x' y' t' s'.
             atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s')
  ")
  apply clarify
  apply (simp add: fresh_star_def)
  apply (thin_tac "\<lbrakk>atom name \<sharp> (c, Lam [namea]. lama) \<and>
         atom namea \<sharp> (name, c, Lam [name]. lam) \<and>
         (\<forall>x' y' t' s'.
             atom x' \<sharp> (c, Lam [y']. s') \<longrightarrow>
             atom y' \<sharp> (x', c, Lam [x']. t') \<longrightarrow>
             Lam [name]. lam = Lam [x']. t' \<longrightarrow>
             Lam [namea]. lama = Lam [y']. s' \<longrightarrow> b name lam namea lama = b x' t' y' s');
         x = (a, b, c, Lam [name]. lam, Lam [namea]. lama)\<rbrakk>
        \<Longrightarrow> P")
  apply (simp add: fresh_star_def)
  done

termination (eqvt) by lexicographic_order

lemma lam_rec2_cong[fundef_cong]:
  "(\<And>s1 s2 s3 s4. l = App s1 s2 \<Longrightarrow> l2 = App s3 s4  \<Longrightarrow> faa s1 s2 s3 s4 = faa' s1 s2 s3 s4) \<Longrightarrow>
   (\<And>n t n' t'. l = Lam [n]. t \<Longrightarrow> l2 = Lam [n']. t' \<Longrightarrow> fll n t n' t' = fll' n t n' t') \<Longrightarrow>
  lam2_rec faa fll xs l l2 = lam2_rec faa' fll' xs l l2"
  apply (rule_tac y="l" and c="(xs, l2)" in lam.strong_exhaust)
  apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
  apply (rule_tac y="l2" and c="(xs, l)" in lam.strong_exhaust) apply auto[3]
  apply (rule_tac y="l2" and c="(name, xs, l)" in lam.strong_exhaust)
  apply auto[2]
  apply clarify
  apply (case_tac "(\<forall>x' y' t' s'.
              atom x' \<sharp> (xs, Lam [y']. s') \<longrightarrow>
              atom y' \<sharp> (x', xs, Lam [x']. t') \<longrightarrow>
              Lam [name]. lam = Lam [x']. t' \<longrightarrow>
              Lam [namea]. lama = Lam [y']. s' \<longrightarrow>
              fll name lam namea lama = fll x' t' y' s')")
  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
  apply (subst lam2_rec.simps) apply (simp add: fresh_star_def)
  using Abs1_eq_iff lam.eq_iff apply metis
  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
  apply (subst lam2_rec.simps(10)) apply (simp add: fresh_star_def)
  apply rule
  done

nominal_primrec aux :: "lam \<Rightarrow> lam \<Rightarrow> (name \<times> name) list \<Rightarrow> bool"
  where
[simp del]: "aux l r xs = lam2_rec
  (%t1 t2 t3 t4. (aux t1 t3 xs) \<and> (aux t2 t4 xs))
  (%x t y s. aux t s ((x, y) # xs)) xs l r"
  unfolding eqvt_def aux_graph_def
  apply (rule, perm_simp, rule, rule)
  by pat_completeness auto

termination (eqvt)
  by (relation "measure (\<lambda>(l, r, xs). size l + size r)") simp_all

lemma aux_simps:
  "aux (Var x) (Var y) xs = ((x, y) \<in> set xs)"
  "aux (App t1 t2) (App s1 s2) xs = (aux t1 s1 xs \<and> aux t2 s2 xs)"
  "aux (Var x) (App t1 t2) xs = False"
  "aux (Var x) (Lam [y].t) xs = False"
  "aux (App t1 t2) (Var x) xs = False"
  "aux (App t1 t2) (Lam [x].t) xs = False"
  "aux (Lam [x].t) (Var y) xs = False"
  "aux (Lam [x].t) (App t1 t2) xs = False"
  "\<lbrakk>atom x \<sharp> (s, xs); atom y \<sharp> (x, t, xs)\<rbrakk> \<Longrightarrow> aux (Lam [x].t) (Lam [y].s) xs = aux t s ((x, y) # xs)"
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps, simp)
  apply (subst aux.simps)
  apply (subst lam2_rec.simps)
  prefer 2 apply rule
  apply (rule, simp add: lam.fresh)
  apply (rule, simp add: lam.fresh)
  apply (intro allI impI)
  apply (rule_tac x="(x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
  apply (rule_tac x="(a, x, x', y, y', t, t', s, s', xs)" and ?'a="name" in obtain_fresh)
  apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
  apply (rule_tac s="(atom x \<rightleftharpoons> atom a) \<bullet> aux t s ((x, y) # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
  apply (rename_tac b)
  apply (rule_tac s="aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) ((atom y \<rightleftharpoons> atom b) \<bullet> s) ((a, b) # xs)" in trans)
  apply (rule_tac s="(atom y \<rightleftharpoons> atom b) \<bullet> aux ((atom x \<rightleftharpoons> atom a) \<bullet> t) s ((a, y) # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim)
  apply (subst permute_eqvt)
  apply (simp add: eqvts swap_fresh_fresh)
  apply (rule sym)
  apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
  apply (rule_tac s="(atom x' \<rightleftharpoons> atom a) \<bullet> aux t' s' ((x', y') # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
  apply (rule_tac s="aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') ((atom y' \<rightleftharpoons> atom b) \<bullet> s') ((a, b) # xs)" in trans)
  apply (rule_tac s="(atom y' \<rightleftharpoons> atom b) \<bullet> aux ((atom x' \<rightleftharpoons> atom a) \<bullet> t') s' ((a, y') # xs)" in trans)
  apply (rule permute_pure[symmetric])
  apply (simp add: eqvts swap_fresh_fresh)
  apply (simp add: lam.fresh fresh_at_base fresh_Pair_elim swap_fresh_fresh)
  apply (subst permute_eqvt)
  apply (simp add: eqvts swap_fresh_fresh)
  apply (subgoal_tac "(atom x' \<rightleftharpoons> atom a) \<bullet> t' = (atom x \<rightleftharpoons> atom a) \<bullet> t")
  apply (subgoal_tac "(atom y' \<rightleftharpoons> atom b) \<bullet> s' = (atom y \<rightleftharpoons> atom b) \<bullet> s")
  apply simp
  apply (subgoal_tac "Lam [y]. s = Lam [b]. ((atom y \<rightleftharpoons> atom b) \<bullet> s)")
  apply (subgoal_tac "Lam [y']. s' = Lam [b]. ((atom y' \<rightleftharpoons> atom b) \<bullet> s')")
  apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (subgoal_tac "Lam [x]. t = Lam [a]. ((atom x \<rightleftharpoons> atom a) \<bullet> t)")
  apply (subgoal_tac "Lam [x']. t' = Lam [a]. ((atom x' \<rightleftharpoons> atom a) \<bullet> t')")
  apply (auto simp add: fresh_Pair_elim Abs1_eq_iff)[1]
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  apply (rule sym)
  apply (simp add: Abs1_eq_iff fresh_Pair_elim fresh_at_base swap_commute)
  done

end