theory Lambda+ −
imports "../Nominal2" + −
begin+ −
+ −
atom_decl name+ −
+ −
nominal_datatype lam =+ −
Var "name"+ −
| App "lam" "lam"+ −
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)+ −
+ −
lemma Abs1_eq_fdest:+ −
fixes x y :: "'a :: at_base"+ −
and S T :: "'b :: fs"+ −
assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"+ −
and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"+ −
and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"+ −
and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"+ −
and "sort_of (atom x) = sort_of (atom y)"+ −
shows "f x T = f y S"+ −
using assms apply -+ −
apply (subst (asm) Abs1_eq_iff')+ −
apply simp_all+ −
apply (elim conjE disjE)+ −
apply simp+ −
apply(rule trans)+ −
apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])+ −
apply(rule fresh_star_supp_conv)+ −
apply(simp add: supp_swap fresh_star_def)+ −
apply(simp add: swap_commute)+ −
done+ −
+ −
lemma fresh_fun_eqvt_app3:+ −
assumes a: "eqvt f"+ −
and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"+ −
shows "a \<sharp> f x y z"+ −
using fresh_fun_eqvt_app[OF a b(1)] a b+ −
by (metis fresh_fun_app)+ −
+ −
lemma fresh_fun_eqvt_app4:+ −
assumes a: "eqvt f"+ −
and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"+ −
shows "a \<sharp> f x y z w"+ −
using fresh_fun_eqvt_app[OF a b(1)] a b+ −
by (metis fresh_fun_app)+ −
+ −
nominal_primrec+ −
f+ −
where+ −
"f f1 f2 f3 (Var x) l = f1 x l"+ −
| "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l"+ −
| "(\<And>t l r. atom x \<sharp> r \<Longrightarrow> atom x \<sharp> f3 x t r l) \<Longrightarrow> (eqvt f1 \<and> eqvt f2 \<and> eqvt f3) \<Longrightarrow> atom x \<sharp> (f1,f2,f3,l) \<Longrightarrow> (f f1 f2 f3 (Lam [x].t) l) = f3 x t (f f1 f2 f3 t (x # l)) l"+ −
apply (simp add: eqvt_def f_graph_def)+ −
apply (rule, perm_simp, rule)+ −
apply(case_tac x)+ −
apply(rule_tac y="d" and c="z" in lam.strong_exhaust)+ −
apply(auto simp add: fresh_star_def)+ −
apply(blast)+ −
apply blast+ −
defer+ −
apply(simp add: fresh_Pair_elim)+ −
apply(erule Abs1_eq_fdest)+ −
defer+ −
apply simp_all+ −
apply (rule_tac f="f3a" in fresh_fun_eqvt_app4)+ −
apply assumption+ −
apply (simp add: fresh_at_base)+ −
apply assumption+ −
apply (erule fresh_eqvt_at)+ −
apply (simp add: supp_Pair supp_fun_eqvt finite_supp)+ −
apply (simp add: fresh_Pair)+ −
apply (simp add: fresh_Cons)+ −
apply (simp add: fresh_Cons fresh_at_base)+ −
apply (assumption)+ −
apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3a x y r l) = f3a (p \<bullet> x) (p \<bullet> y) (p \<bullet> r) (p \<bullet> l)")+ −
apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")+ −
apply (simp add: eqvt_at_def eqvt_def)+ −
apply (simp add: swap_fresh_fresh)+ −
apply (simp add: permute_fun_app_eq)+ −
apply (simp add: eqvt_def)+ −
prefer 2+ −
apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)")+ −
apply simp+ −
--"I believe this holds by induction on the graph..."+ −
unfolding f_sumC_def+ −
apply (rule_tac y="t" in lam.exhaust)+ −
apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)")+ −
apply simp+ −
defer+ −
apply (rule THE_default1_equality)+ −
apply simp+ −
defer+ −
apply simp+ −
apply (rule_tac ?f1.0="f1a" in f_graph.intros(1))+ −
sorry (*this could be defined? *)+ −
+ −
termination+ −
by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size)+ −
+ −
section {* Locally Nameless Terms *}+ −
+ −
nominal_datatype ln = + −
LNBnd nat+ −
| LNVar name+ −
| LNApp ln ln+ −
| LNLam ln+ −
+ −
fun+ −
lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" + −
where+ −
"lookup [] n x = LNVar x"+ −
| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"+ −
+ −
lemma [eqvt]:+ −
shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"+ −
by (induct xs arbitrary: n) (simp_all add: permute_pure)+ −
+ −
definition+ −
trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"+ −
where+ −
"trans t l = f (%x l. lookup l 0 x) (%t1 t2 r1 r2 l. LNApp r1 r2) (%n t r l. LNLam r) t l"+ −
+ −
lemma+ −
"trans (Var x) xs = lookup xs 0 x"+ −
"trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"+ −
"atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"+ −
apply (simp_all add: trans_def)+ −
apply (subst f.simps)+ −
apply (simp add: ln.fresh)+ −
apply (simp add: eqvt_def)+ −
apply auto+ −
apply (perm_simp, rule)+ −
apply (perm_simp, rule)+ −
apply (perm_simp, rule)+ −
apply (auto simp add: fresh_Pair)[1]+ −
apply (simp_all add: fresh_def supp_def permute_fun_def)[3]+ −
apply (simp add: eqvts permute_pure)+ −
done+ −
+ −