25 bn |
25 bn |
26 where |
26 where |
27 "bn ENil = []" |
27 "bn ENil = []" |
28 | "bn (ECons env x v) = (atom x) # (bn env)" |
28 | "bn (ECons env x v) = (atom x) # (bn env)" |
29 |
29 |
30 |
30 nominal_primrec (invariant "\<lambda>x y. case x of Inl (x1, y1) \<Rightarrow> |
31 nominal_primrec |
31 supp y \<subseteq> (supp y1 - set (bn x1)) \<union> (fv_bn x1) | Inr (x2, y2) \<Rightarrow> supp y \<subseteq> supp x2 \<union> supp y2") |
32 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
32 evals :: "env \<Rightarrow> lam \<Rightarrow> sem" and |
33 evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem" |
33 evals_aux :: "sem \<Rightarrow> sem \<Rightarrow> sem" |
34 where |
34 where |
35 "evals ENil (Var x) = N (V x)" |
35 "evals ENil (Var x) = N (V x)" |
36 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
36 | "evals (ECons tail y v) (Var x) = (if x = y then v else evals tail (Var x))" |
39 | "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t" |
39 | "evals_aux (L cenv x t) t' = evals (ECons cenv x t') t" |
40 | "evals_aux (N n) t' = N (A n t')" |
40 | "evals_aux (N n) t' = N (A n t')" |
41 apply(simp add: eqvt_def evals_evals_aux_graph_def) |
41 apply(simp add: eqvt_def evals_evals_aux_graph_def) |
42 apply(perm_simp) |
42 apply(perm_simp) |
43 apply(simp) |
43 apply(simp) |
44 apply (rule TrueI) |
44 apply(erule evals_evals_aux_graph.induct) |
|
45 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
|
46 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
|
47 apply(rule conjI) |
|
48 apply(rule impI) |
|
49 apply(blast) |
|
50 apply(rule impI) |
|
51 apply(simp add: supp_at_base) |
|
52 apply(blast) |
|
53 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
|
54 apply(blast) |
|
55 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
|
56 apply(blast) |
|
57 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
|
58 apply(blast) |
|
59 apply(simp add: sem_neu_env.supp lam.supp sem_neu_env.bn_defs) |
45 --"completeness" |
60 --"completeness" |
46 apply(case_tac x) |
61 apply(case_tac x) |
47 apply(simp) |
62 apply(simp) |
48 apply(case_tac a) |
63 apply(case_tac a) |
49 apply(simp) |
64 apply(simp) |
86 apply(simp add: fresh_star_def) |
101 apply(simp add: fresh_star_def) |
87 apply(perm_simp) |
102 apply(perm_simp) |
88 apply(simp add: fresh_star_Pair perm_supp_eq) |
103 apply(simp add: fresh_star_Pair perm_supp_eq) |
89 apply(perm_simp) |
104 apply(perm_simp) |
90 apply(simp add: fresh_star_Pair perm_supp_eq) |
105 apply(simp add: fresh_star_Pair perm_supp_eq) |
91 thm Abs_lst1_fcb2' |
106 apply(simp add: sem_neu_env.bn_defs sem_neu_env.supp) |
|
107 using at_set_avoiding3 |
|
108 apply - |
|
109 apply(drule_tac x="set (atom x # bn cenv)" in meta_spec) |
|
110 apply(drule_tac x="(cenv, cenva, x, xa, t, ta, t'a)" in meta_spec) |
|
111 apply(drule_tac x="[atom x # bn cenv]lst. t" in meta_spec) |
|
112 apply(simp (no_asm_use) add: finite_supp Abs_fresh_star_iff) |
|
113 apply(drule meta_mp) |
|
114 apply(simp add: fresh_star_def) |
|
115 apply(erule exE) |
|
116 apply(erule conjE)+ |
|
117 thm Abs_fresh_star_iff |
|
118 |
|
119 |
|
120 apply(subgoal_tac "\<exists>c::name. atom c \<sharp> (x, xa, cenv, cenva, t, ta, t'a)") |
|
121 prefer 2 |
|
122 apply(rule obtain_fresh) |
|
123 apply(blast) |
|
124 apply(erule exE) |
|
125 apply(drule trans) |
|
126 apply(rule sym) |
|
127 apply(rule_tac a="xa" and b="c" in flip_fresh_fresh) |
|
128 apply(simp add: Abs_fresh_iff) |
|
129 apply(simp add: Abs_fresh_iff fresh_Pair fresh_at_base) |
|
130 apply(perm_simp) |
|
131 apply(simp) |
|
132 apply(rotate_tac 4) |
|
133 apply(drule sym) |
|
134 apply(rotate_tac 5) |
|
135 apply(drule trans) |
|
136 apply(rule sym) |
|
137 apply(rule_tac a="x" and b="c" in flip_fresh_fresh) |
|
138 apply(simp add: Abs_fresh_iff) |
|
139 apply(simp add: Abs_fresh_iff fresh_Pair fresh_at_base) |
|
140 apply(perm_simp) |
|
141 apply(simp) |
|
142 (* HERE *) |
|
143 apply(auto)[1] |
|
144 apply(rule fresh_eqvt_at) |
|
145 back |
|
146 apply(assumption) |
|
147 apply(simp add: finite_supp) |
|
148 apply(rule_tac S="supp (env, y, x, t)" in supports_fresh) |
|
149 apply(simp add: supports_def fresh_def[symmetric]) |
|
150 apply(perm_simp) |
|
151 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
152 apply(simp add: finite_supp) |
|
153 apply(simp add: fresh_def[symmetric]) |
|
154 apply(simp add: eqvt_at_def) |
|
155 apply(simp add: eqvt_at_def[symmetric]) |
|
156 apply(perm_simp) |
|
157 apply(simp add: flip_fresh_fresh) |
|
158 apply(rule sym) |
|
159 apply(rule trans) |
|
160 |
92 sorry |
161 sorry |
93 |
162 |
94 (* can probably not proved by a trivial size argument *) |
163 (* can probably not proved by a trivial size argument *) |
95 termination sorry |
164 termination apply(lexicographic_order) |
|
165 |
|
166 sorry |
96 |
167 |
97 lemma [eqvt]: |
168 lemma [eqvt]: |
98 shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)" |
169 shows "(p \<bullet> evals env t) = evals (p \<bullet> env) (p \<bullet> t)" |
99 and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)" |
170 and "(p \<bullet> evals_aux v s) = evals_aux (p \<bullet> v) (p \<bullet> s)" |
100 sorry |
171 sorry |