2812
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 1
theory Lambda
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 2
imports "../Nominal2"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 3
begin
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 4
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 5
atom_decl name
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 6
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 7
nominal_datatype lam =
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 8
Var "name"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 9
| App "lam" "lam"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 10
| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 11
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 12
lemma Abs1_eq_fdest:
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 13
fixes x y :: "'a :: at_base"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 14
and S T :: "'b :: fs"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 15
assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 16
and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 17
and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 18
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"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 19
and "sort_of (atom x) = sort_of (atom y)"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 20
shows "f x T = f y S"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 21
using assms apply -
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 22
apply (subst (asm) Abs1_eq_iff')
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 23
apply simp_all
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 24
apply (elim conjE disjE)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 25
apply simp
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 26
apply(rule trans)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 27
apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 28
apply(rule fresh_star_supp_conv)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 29
apply(simp add: supp_swap fresh_star_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 30
apply(simp add: swap_commute)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 31
done
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 32
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 33
lemma fresh_fun_eqvt_app3:
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 34
assumes a: "eqvt f"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 35
and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 36
shows "a \<sharp> f x y z"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 37
using fresh_fun_eqvt_app[OF a b(1)] a b
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 38
by (metis fresh_fun_app)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 39
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 40
lemma fresh_fun_eqvt_app4:
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 41
assumes a: "eqvt f"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 42
and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" "a \<sharp> w"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 43
shows "a \<sharp> f x y z w"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 44
using fresh_fun_eqvt_app[OF a b(1)] a b
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 45
by (metis fresh_fun_app)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 46
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 47
nominal_primrec
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 48
f
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 49
where
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 50
"f f1 f2 f3 (Var x) l = f1 x l"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 51
| "f f1 f2 f3 (App t1 t2) l = f2 t1 t2 (f f1 f2 f3 t1 l) (f f1 f2 f3 t2 l) l"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 52
| "(\<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"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 53
apply (simp add: eqvt_def f_graph_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 54
apply (rule, perm_simp, rule)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 55
apply(case_tac x)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 56
apply(rule_tac y="d" and c="z" in lam.strong_exhaust)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 57
apply(auto simp add: fresh_star_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 58
apply(blast)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 59
apply blast
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 60
defer
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 61
apply(simp add: fresh_Pair_elim)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 62
apply(erule Abs1_eq_fdest)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 63
defer
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 64
apply simp_all
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 65
apply (rule_tac f="f3a" in fresh_fun_eqvt_app4)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 66
apply assumption
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 67
apply (simp add: fresh_at_base)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 68
apply assumption
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 69
apply (erule fresh_eqvt_at)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 70
apply (simp add: supp_Pair supp_fun_eqvt finite_supp)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 71
apply (simp add: fresh_Pair)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 72
apply (simp add: fresh_Cons)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 73
apply (simp add: fresh_Cons fresh_at_base)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 74
apply (assumption)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 75
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)")
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 76
apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> la = la")
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 77
apply (simp add: eqvt_at_def eqvt_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 78
apply (simp add: swap_fresh_fresh)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 79
apply (simp add: permute_fun_app_eq)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 80
apply (simp add: eqvt_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 81
prefer 2
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 82
apply (subgoal_tac "atom x \<sharp> f_sumC (f1a, f2a, f3a, t, x # la)")
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 83
apply simp
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 84
--"I believe this holds by induction on the graph..."
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 85
unfolding f_sumC_def
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 86
apply (rule_tac y="t" in lam.exhaust)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 87
apply (subgoal_tac "THE_default undefined (f_graph (f1a, f2a, f3a, t, x # la)) = f1a name (x # la)")
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 88
apply simp
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 89
defer
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 90
apply (rule THE_default1_equality)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 91
apply simp
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 92
defer
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 93
apply simp
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 94
apply (rule_tac ?f1.0="f1a" in f_graph.intros(1))
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 95
sorry (*this could be defined? *)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 96
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 97
termination
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 98
by (relation "measure (\<lambda>(_,_,_,x,_). size x)") (auto simp add: lam.size)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 99
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 100
section {* Locally Nameless Terms *}
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 101
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 102
nominal_datatype ln =
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 103
LNBnd nat
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 104
| LNVar name
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 105
| LNApp ln ln
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 106
| LNLam ln
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 107
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 108
fun
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 109
lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 110
where
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 111
"lookup [] n x = LNVar x"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 112
| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 113
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 114
lemma [eqvt]:
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 115
shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 116
by (induct xs arbitrary: n) (simp_all add: permute_pure)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 117
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 118
definition
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 119
trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 120
where
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 121
"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"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 122
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 123
lemma
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 124
"trans (Var x) xs = lookup xs 0 x"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 125
"trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 126
"atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))"
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 127
apply (simp_all add: trans_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 128
apply (subst f.simps)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 129
apply (simp add: ln.fresh)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 130
apply (simp add: eqvt_def)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 131
apply auto
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 132
apply (perm_simp, rule)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 133
apply (perm_simp, rule)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 134
apply (perm_simp, rule)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 135
apply (auto simp add: fresh_Pair)[1]
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 136
apply (simp_all add: fresh_def supp_def permute_fun_def)[3]
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 137
apply (simp add: eqvts permute_pure)
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 138
done
1135a14927bb
F for lambda used to define translation to locally nameless
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
+ − 139