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_datatype sem =
  L e::"env" x::"name" l::"lam" binds "bn e" x in l
| N "neu"
and neu = 
  V "name"
| A "neu" "sem"
and env =
  ENil
| ECons "env" "name" "sem"
binder
  bn
where
  "bn ENil = []"
| "bn (ECons env x v) = atom x # bn env" 

nominal_primrec
  evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and
  evals_aux :: "sem \<Rightarrow> lam \<Rightarrow> env \<Rightarrow> sem"
where
  "evals ENil (Var x) = N (V x)"
| "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" 
| "evals env (Lam [x]. t) = L env x t"
| "evals env (App t1 t2) = evals_aux (evals env t1) t2 env"
| "evals_aux (L cenv x t) t2 env = evals (ECons cenv x (evals env t2)) t"
| "evals_aux (N n) t2 env = N (A n (evals env t2))"
apply(subgoal_tac "\<And>p x y. evals_evals_aux_graph x y \<Longrightarrow> evals_evals_aux_graph (p \<bullet> x) (p \<bullet> y)")
apply(simp add: eqvt_def)
apply(simp add: permute_fun_def)
apply(rule allI)
apply(rule ext)
apply(rule ext)
apply(rule iffI)
apply(drule_tac x="p" in meta_spec)
apply(drule_tac x="- p \<bullet> x" in meta_spec)
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
apply(simp add: permute_bool_def)
apply(simp add: permute_bool_def)
apply(erule evals_evals_aux_graph.induct)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(simp)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(simp)
apply(simp)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(simp)
apply(simp)
apply(perm_simp)
apply(rule evals_evals_aux_graph.intros)
apply(simp)
apply (rule TrueI)
--"completeness"
apply(case_tac x)
apply(simp)
apply(case_tac a)
apply(simp)
apply(case_tac aa rule: sem_neu_env.exhaust(3))
apply(simp)
apply(case_tac b rule: lam.exhaust)
apply(metis)+
apply(case_tac b rule: lam.exhaust)
apply(metis)+
apply(simp)
apply(case_tac b)
apply(simp)
apply(case_tac a rule: sem_neu_env.exhaust(1))
apply(metis)+
--"compatibility"
apply(all_trivials)
apply(simp)
apply(simp)
defer
apply(simp)
apply(simp)
apply (simp add: meta_eq_to_obj_eq[OF evals_def, symmetric, unfolded fun_eq_iff])
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenv x (evals enva t2a), t)")
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (enva, t2a)")
apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa (evals enva t2a), ta)")
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x (evals enva t2a), t))")
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (enva, t2a))")
apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa (evals enva t2a), ta))")
apply(erule conjE)+
defer
apply (simp_all add: eqvt_at_def evals_def)[3]
apply(simp)
sorry

(* can probably not proved by a trivial size argument *)
termination sorry

lemma [eqvt]:
  shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"
  and "(p \<bullet> evals_aux v t env) = evals_aux (p \<bullet> v) (p \<bullet> t) (p \<bullet> env)"
sorry

(* fixme: should be a provided lemma *)
lemma fv_bn_finite:
  shows "finite (fv_bn env)"
apply(induct env rule: sem_neu_env.inducts(3))
apply(auto simp add: sem_neu_env.supp finite_supp)
done

lemma test:
  shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"
  and "supp (evals_aux s t env) \<subseteq> ((supp s) - set (bn cenv)) \<union> supp (fn cenv) \<union> supp (evals env t)"
apply(induct rule: evals_evals_aux.induct)
apply(simp add: sem_neu_env.supp lam.supp supp_Nil sem_neu_env.bn_defs)
apply(simp add: sem_neu_env.supp lam.supp supp_Nil supp_Cons sem_neu_env.bn_defs)
apply(rule conjI)
apply(auto)[1]
apply(rule impI)
apply(simp)
apply (metis (no_types) at_base_infinite finite_UNIV)
apply(simp)
apply(subst sem_neu_env.supp)
apply(simp add: sem_neu_env.supp lam.supp)
apply(auto)[1]
apply(simp)
apply(metis)
sorry

nominal_primrec
  reify :: "sem \<Rightarrow> lam" and
  reifyn :: "neu \<Rightarrow> lam"
where
  "atom x \<sharp> (env, y, t) \<Longrightarrow> reify (L env y t) = Lam [x]. (reify (evals (ECons env y (N (V x))) t))"
| "reify (N n) = reifyn n"
| "reifyn (V x) = Var x"
| "reifyn (A n d) = App (reifyn n) (reify d)"
apply(subgoal_tac "\<And>p x y. reify_reifyn_graph x y \<Longrightarrow> reify_reifyn_graph (p \<bullet> x) (p \<bullet> y)")
apply(simp add: eqvt_def)
apply(simp add: permute_fun_def)
apply(rule allI)
apply(rule ext)
apply(rule ext)
apply(rule iffI)
apply(drule_tac x="p" in meta_spec)
apply(drule_tac x="- p \<bullet> x" in meta_spec)
apply(drule_tac x="- p \<bullet> xa" in meta_spec)
apply(simp add: permute_bool_def)
apply(simp add: permute_bool_def)
apply(erule reify_reifyn_graph.induct)
apply(perm_simp)
apply(rule reify_reifyn_graph.intros)
apply(rule_tac p="-p" in permute_boolE)
apply(perm_simp add: permute_minus_cancel)
apply(simp)
apply(simp)
apply(perm_simp)
apply(rule reify_reifyn_graph.intros)
apply(simp)
apply(perm_simp)
apply(rule reify_reifyn_graph.intros)
apply(perm_simp)
apply(rule reify_reifyn_graph.intros)
apply(simp)
apply(simp)
apply(rule TrueI)
--"completeness"
apply(case_tac x)
apply(simp)
apply(case_tac a rule: sem_neu_env.exhaust(1))
apply(subgoal_tac "\<exists>x::name. atom x \<sharp> (env, name, lam)")
apply(metis)
apply(rule obtain_fresh)
apply(blast)
apply(blast)
apply(case_tac b rule: sem_neu_env.exhaust(2))
apply(simp)
apply(simp)
apply(metis)
--"compatibility"
apply(all_trivials)
defer
apply(simp)
apply(simp)
apply(simp)
apply(erule conjE)
apply (simp add: meta_eq_to_obj_eq[OF reify_def, symmetric, unfolded fun_eq_iff])
apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva y (N (V x))) t)")
apply (subgoal_tac "eqvt_at (\<lambda>t. reify t) (evals (ECons enva ya (N (V xa))) ta)")
apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva y (N (V x))) t))")
apply (thin_tac "eqvt_at reify_reifyn_sumC (Inl (evals (ECons enva ya (N (V xa))) ta))")
defer
apply (simp_all add: eqvt_at_def reify_def)[2]
apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, enva, y, ya, t, ta)")
prefer 2
apply(rule obtain_fresh)
apply(blast)
apply(erule exE)
apply(rule trans)
apply(rule sym)
apply(rule_tac a="x" and b="c" in flip_fresh_fresh)
apply(simp add: Abs_fresh_iff)
apply(simp add: Abs_fresh_iff fresh_Pair)
apply(auto)[1]
apply(rule fresh_eqvt_at)
back
apply(assumption)
apply(simp add: finite_supp)
apply(rule_tac S="supp (enva, y, x, t)" in supports_fresh)
apply(simp add: supports_def fresh_def[symmetric])
apply(perm_simp)
apply(simp add: swap_fresh_fresh fresh_Pair)
apply(simp add: finite_supp)
apply(simp add: fresh_def[symmetric])
apply(simp add: eqvt_at_def)
apply(simp add: eqvt_at_def[symmetric])
apply(perm_simp)
apply(simp add: flip_fresh_fresh)
apply(rule sym)
apply(rule trans)
apply(rule sym)
apply(rule_tac a="xa" and b="c" in flip_fresh_fresh)
apply(simp add: Abs_fresh_iff)
apply(simp add: Abs_fresh_iff fresh_Pair)
apply(auto)[1]
apply(rule fresh_eqvt_at)
back
apply(assumption)
apply(simp add: finite_supp)
apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
apply(simp add: supports_def fresh_def[symmetric])
apply(perm_simp)
apply(simp add: swap_fresh_fresh fresh_Pair)
apply(simp add: finite_supp)
apply(simp add: fresh_def[symmetric])
apply(simp add: eqvt_at_def)
apply(simp add: eqvt_at_def[symmetric])
apply(perm_simp)
apply(simp add: flip_fresh_fresh)
apply(simp (no_asm) add: Abs1_eq_iff)
apply(rule sym)
apply(erule_tac Abs_lst1_fcb2')
apply(rule fresh_eqvt_at)
back
apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
apply(perm_simp)
apply(simp add: flip_fresh_fresh)
apply(simp add: finite_supp)
apply(rule supports_fresh)
apply(rule_tac S="supp (enva, ya, xa, ta)" in supports_fresh)
apply(simp add: supports_def fresh_def[symmetric])
apply(perm_simp)
apply(simp add: swap_fresh_fresh fresh_Pair)
apply(simp add: finite_supp)
apply(simp add: fresh_def[symmetric])
apply(simp add: eqvt_at_def)
apply(simp add: eqvt_at_def[symmetric])
apply(perm_simp)
apply(rule fresh_eqvt_at)
back
apply(drule_tac q="(c \<leftrightarrow> x)" in eqvt_at_perm)
apply(perm_simp)
apply(simp add: flip_fresh_fresh)
apply(assumption)
apply(simp add: finite_supp)
sorry

termination sorry

definition
  eval :: "lam \<Rightarrow> sem"
where
  "eval t = evals ENil t"

definition
  normalize :: "lam \<Rightarrow> lam"
where
  "normalize t = reify (eval t)"

end