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 x "bn e" 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)" 

  evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and

  evals_aux :: "sem \<Rightarrow> sem \<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))" 

| "atom x \<sharp> env \<Longrightarrow> evals env (Lam [x]. t) = L env x t"

| "evals env (App t1 t2) = evals_aux (evals env t1) (evals env t2)"

| "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t"

| "evals_aux (N n) t' = N (A n t')"

apply(simp add: eqvt_def  evals_evals_aux_graph_def)

apply(perm_simp)

apply(simp)

--"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 add: sem_neu_env.fresh)

apply(case_tac b rule: lam.exhaust)

apply(metis)+

apply(case_tac aa rule: sem_neu_env.exhaust(3))

apply(rule_tac y="b" and c="env" in lam.strong_exhaust)

apply(metis)+

apply(simp add: fresh_star_def)

apply(simp)

apply(rule_tac y="b" and c="ECons env name sem" in lam.strong_exhaust)

apply(metis)+

apply(simp add: fresh_star_def)

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 t'a, t)")

apply (subgoal_tac "eqvt_at (\<lambda>(a, b). evals a b) (ECons cenva xa t'a, ta)")

apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenv x t'a, t))")

apply (thin_tac "eqvt_at evals_evals_aux_sumC (Inl (ECons cenva xa t'a, ta))")

apply(erule conjE)+

defer

apply (simp_all add: eqvt_at_def evals_def)[3]

apply(simp add: sem_neu_env.alpha_refl)

apply(erule conjE)+

apply(erule_tac c="(env, enva)" in Abs_lst1_fcb2)

apply(simp add: Abs_fresh_iff)

apply(simp add: fresh_star_def)

apply(perm_simp)

apply(simp add: fresh_star_Pair perm_supp_eq)

apply(perm_simp)

apply(simp add: fresh_star_Pair perm_supp_eq)

sorry

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

lemma [eqvt]:

  shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)"

  and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)"

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:

  fixes env::"env"

  shows "supp (evals env t) \<subseteq> (supp t - set (bn env)) \<union> (fv_bn env)"

  and "supp (evals_aux s v) \<subseteq> (supp s) \<union> (supp v)"

apply(induct env t and s v 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(simp add: supp_at_base)

apply(blast)

apply(simp)

apply(subst sem_neu_env.supp)

apply(simp add: sem_neu_env.supp lam.supp)

apply(auto)[1]

apply(simp add: lam.supp sem_neu_env.supp)

apply(blast)

apply(simp add: sem_neu_env.supp sem_neu_env.bn_defs)

apply(blast)

apply(simp add: sem_neu_env.supp)

done

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 env 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 env 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, env, 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 (env, 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)

thm at_set_avoiding3

using at_set_avoiding3

apply -

apply(drule_tac x="set (atom y # bn env)" in meta_spec)

apply(drule_tac x="(env, enva)" in meta_spec)

apply(drule_tac x="[atom y # bn env]lst. t" in meta_spec)

apply(simp (no_asm_use) add: finite_supp)

apply(drule meta_mp)

apply(rule Abs_fresh_star)

apply(auto)[1]

apply(erule exE)

apply(erule conjE)+

apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)

apply(perm_simp)

apply(simp add: flip_fresh_fresh fresh_Pair)

apply(drule_tac q="(xa \<leftrightarrow> c)" in eqvt_at_perm)

apply(perm_simp)

apply(simp add: flip_fresh_fresh fresh_Pair)

apply(drule sym)

(* HERE *)

apply(rotate_tac 9)

apply(drule sym)

apply(rotate_tac 9)

apply(drule trans)

apply(rule sym)

apply(rule_tac p="p" in supp_perm_eq)

apply(assumption)

apply(simp)

apply(perm_simp)

apply(simp (no_asm_use) add: Abs_eq_iff2 alphas)

apply(erule conjE | erule exE)+

apply(clarify)

apply(rule trans)

apply(rule sym)

apply(rule_tac p="pa" in perm_supp_eq)

defer

apply(rule sym)

apply(rule trans)

apply(rule sym)

apply(rule_tac p="p" in perm_supp_eq)

defer

apply(simp add: atom_eqvt)

apply(drule_tac q="(x \<leftrightarrow> c)" in eqvt_at_perm)

apply(perm_simp)

apply(simp add: flip_fresh_fresh fresh_Pair)

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