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