Beta: equ and equ2 are not the same relations, equ2 seems not to be beta-eta equality.
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 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)+ −
+ −
lemma the_default_pty:+ −
assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"+ −
and unique: "\<exists>!y. G x y"+ −
and pty: "\<And>x y. G x y \<Longrightarrow> P x y"+ −
shows "P x (f x)"+ −
apply(subst f_def)+ −
apply (rule ex1E[OF unique])+ −
apply (subst THE_default1_equality[OF unique])+ −
apply assumption+ −
apply (rule pty)+ −
apply assumption+ −
done+ −
+ −
lemma Abs_lst1_fcb2:+ −
fixes a b :: "'a :: at"+ −
and S T :: "'b :: fs"+ −
and c::"'c::fs"+ −
assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"+ −
and fcb: "\<And>a T. atom a \<sharp> f a T c"+ −
and fresh: "{atom a, atom b} \<sharp>* c"+ −
and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"+ −
and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"+ −
shows "f a T c = f b S c"+ −
proof -+ −
have fin1: "finite (supp (f a T c))"+ −
apply(rule_tac S="supp (a, T, c)" in supports_finite)+ −
apply(simp add: supports_def)+ −
apply(simp add: fresh_def[symmetric])+ −
apply(clarify)+ −
apply(subst perm1)+ −
apply(simp add: supp_swap fresh_star_def)+ −
apply(simp add: swap_fresh_fresh fresh_Pair)+ −
apply(simp add: finite_supp)+ −
done+ −
have fin2: "finite (supp (f b S c))"+ −
apply(rule_tac S="supp (b, S, c)" in supports_finite)+ −
apply(simp add: supports_def)+ −
apply(simp add: fresh_def[symmetric])+ −
apply(clarify)+ −
apply(subst perm2)+ −
apply(simp add: supp_swap fresh_star_def)+ −
apply(simp add: swap_fresh_fresh fresh_Pair)+ −
apply(simp add: finite_supp)+ −
done+ −
obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" + −
using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"]+ −
apply(auto simp add: finite_supp supp_Pair fin1 fin2)+ −
done+ −
have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" + −
apply(simp (no_asm_use) only: flip_def)+ −
apply(subst swap_fresh_fresh)+ −
apply(simp add: Abs_fresh_iff)+ −
using fr+ −
apply(simp add: Abs_fresh_iff)+ −
apply(subst swap_fresh_fresh)+ −
apply(simp add: Abs_fresh_iff)+ −
using fr+ −
apply(simp add: Abs_fresh_iff)+ −
apply(rule e)+ −
done+ −
then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)"+ −
apply (simp add: swap_atom flip_def)+ −
done+ −
then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S"+ −
by (simp add: Abs1_eq_iff)+ −
have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"+ −
unfolding flip_def+ −
apply(rule sym)+ −
apply(rule swap_fresh_fresh)+ −
using fcb[where a="a"] + −
apply(simp)+ −
using fr+ −
apply(simp add: fresh_Pair)+ −
done+ −
also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"+ −
unfolding flip_def+ −
apply(subst perm1)+ −
using fresh fr+ −
apply(simp add: supp_swap fresh_star_def fresh_Pair)+ −
apply(simp)+ −
done+ −
also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp+ −
also have "... = (b \<leftrightarrow> d) \<bullet> f b S c"+ −
unfolding flip_def+ −
apply(subst perm2)+ −
using fresh fr+ −
apply(simp add: supp_swap fresh_star_def fresh_Pair)+ −
apply(simp)+ −
done+ −
also have "... = f b S c" + −
apply(rule flip_fresh_fresh)+ −
using fcb[where a="b"] + −
apply(simp)+ −
using fr+ −
apply(simp add: fresh_Pair)+ −
done+ −
finally show ?thesis by simp+ −
qed+ −
+ −
locale test =+ −
fixes f1::"name \<Rightarrow> name list \<Rightarrow> ('a::pt)"+ −
and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"+ −
and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> name list \<Rightarrow> ('a::pt)"+ −
assumes fs: "finite (supp (f1, f2, f3))"+ −
and eq: "eqvt f1" "eqvt f2" "eqvt f3"+ −
and fcb1: "\<And>l n. atom ` set l \<sharp>* f1 n l"+ −
and fcb2: "\<And>l t1 t2 r1 r2. atom ` set l \<sharp>* (r1, r2) \<Longrightarrow> atom ` set l \<sharp>* f2 t1 t2 r1 r2 l"+ −
and fcb3: "\<And>t l r. atom ` set (x # l) \<sharp>* r \<Longrightarrow> atom ` set (x # l) \<sharp>* f3 x t r l"+ −
begin+ −
+ −
nominal_primrec (invariant "\<lambda>(x, l) y. atom ` set l \<sharp>* y")+ −
f+ −
where+ −
"f (Var x) l = f1 x l"+ −
| "f (App t1 t2) l = f2 t1 t2 (f t1 l) (f t2 l) l"+ −
| "atom x \<sharp> l \<Longrightarrow> (f (Lam [x].t) l) = f3 x t (f t (x # l)) l"+ −
apply (simp add: eqvt_def f_graph_def)+ −
apply (rule, perm_simp)+ −
apply (simp only: eq[unfolded eqvt_def])+ −
apply (erule f_graph.induct)+ −
apply (simp add: fcb1)+ −
apply (simp add: fcb2 fresh_star_Pair)+ −
apply simp+ −
apply (subgoal_tac "atom ` set (xa # l) \<sharp>* f3 xa t (f_sum (t, xa # l)) l")+ −
apply (simp add: fresh_star_def)+ −
apply (rule fcb3)+ −
apply (simp add: fresh_star_def fresh_def)+ −
apply simp_all+ −
apply(case_tac x)+ −
apply(rule_tac y="a" and c="b" in lam.strong_exhaust)+ −
apply(auto simp add: fresh_star_def)+ −
apply(erule_tac Abs_lst1_fcb2)+ −
--"?"+ −
apply (subgoal_tac "atom ` set (a # la) \<sharp>* f3 a T (f_sumC (T, a # la)) la")+ −
apply (simp add: fresh_star_def)+ −
apply (rule fcb3)+ −
apply (simp add: fresh_star_def)+ −
apply (rule fresh_fun_eqvt_app4[OF eq(3)])+ −
apply (simp add: fresh_at_base)+ −
apply assumption+ −
apply (erule fresh_eqvt_at)+ −
apply (simp add: finite_supp)+ −
apply (simp add: fresh_Pair fresh_Cons fresh_at_base)+ −
apply assumption+ −
apply (subgoal_tac "\<And>p y r l. p \<bullet> (f3 x y r l) = f3 (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)+ −
apply (simp add: swap_fresh_fresh)+ −
apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def])+ −
apply simp+ −
done+ −
+ −
termination+ −
by (relation "measure (\<lambda>(x,_). size x)") (auto simp add: lam.size)+ −
+ −
end+ −
+ −
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 lookup_eqvt[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)+ −
+ −
lemma fresh_at_list: "atom x \<sharp> xs \<longleftrightarrow> x \<notin> set xs"+ −
unfolding fresh_def supp_set[symmetric]+ −
apply (induct xs)+ −
apply (simp add: supp_set_empty)+ −
apply simp+ −
apply auto+ −
apply (simp_all add: insert_absorb UnI2 finite_set supp_of_finite_insert supp_at_base)+ −
done+ −
+ −
interpretation trans: test+ −
"%x l. lookup l 0 x"+ −
"%t1 t2 r1 r2 l. LNApp r1 r2"+ −
"%n t r l. LNLam r"+ −
apply default+ −
apply (auto simp add: pure_fresh supp_Pair)+ −
apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure lookup_eqvt)[3]+ −
apply (simp_all add: eqvt_def permute_fun_def permute_pure lookup_eqvt)+ −
apply (simp add: fresh_star_def)+ −
apply (rule_tac x="0 :: nat" in spec)+ −
apply (induct_tac l)+ −
apply (simp add: ln.fresh pure_fresh)+ −
apply (auto simp add: ln.fresh pure_fresh)[1]+ −
apply (case_tac "a \<in> set list")+ −
apply simp+ −
apply (rule_tac f="lookup" in fresh_fun_eqvt_app3)+ −
unfolding eqvt_def+ −
apply rule+ −
using eqvts_raw(35)+ −
apply auto[1]+ −
apply (simp add: fresh_at_list)+ −
apply (simp add: pure_fresh)+ −
apply (simp add: fresh_at_base)+ −
apply (simp add: fresh_star_Pair fresh_star_def ln.fresh)+ −
apply (simp add: fresh_star_def ln.fresh)+ −
done+ −
+ −
thm trans.f.simps+ −
+ −
lemma lam_strong_exhaust2:+ −
"\<lbrakk>\<And>name. y = Var name \<Longrightarrow> P; + −
\<And>lam1 lam2. y = App lam1 lam2 \<Longrightarrow> P;+ −
\<And>name lam. \<lbrakk>{atom name} \<sharp>* c; y = Lam [name]. lam\<rbrakk> \<Longrightarrow> P;+ −
finite (supp c)\<rbrakk>+ −
\<Longrightarrow> P"+ −
sorry+ −
+ −
nominal_primrec+ −
g+ −
where+ −
"(~finite (supp (g1, g2, g3))) \<Longrightarrow> g g1 g2 g3 t = t"+ −
| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (Var x) = g1 x"+ −
| "finite (supp (g1, g2, g3)) \<Longrightarrow> g g1 g2 g3 (App t1 t2) = g2 t1 t2 (g g1 g2 g3 t1) (g g1 g2 g3 t2)"+ −
| "finite (supp (g1, g2, g3)) \<Longrightarrow> atom x \<sharp> (g1,g2,g3) \<Longrightarrow> (g g1 g2 g3 (Lam [x].t)) = g3 x t (g g1 g2 g3 t)"+ −
apply (simp add: eqvt_def g_graph_def)+ −
apply (rule, perm_simp, rule)+ −
apply simp_all+ −
apply (case_tac x)+ −
apply (case_tac "finite (supp (a, b, c))")+ −
prefer 2+ −
apply simp+ −
apply(rule_tac y="d" and c="(a,b,c)" in lam_strong_exhaust2)+ −
apply auto+ −
apply blast+ −
apply (simp add: Abs1_eq_iff fresh_star_def)+ −
sorry+ −
+ −
termination+ −
by (relation "measure (\<lambda>(_,_,_,t). size t)") (simp_all add: lam.size)+ −
+ −
end+ −