1 theory Let |
1 theory Let |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 3 or example 5 from Terms.thy *} |
|
6 |
|
7 atom_decl name |
5 atom_decl name |
8 |
|
9 declare [[STEPS = 29]] |
|
10 |
6 |
11 nominal_datatype trm = |
7 nominal_datatype trm = |
12 Var "name" |
8 Var "name" |
13 | App "trm" "trm" |
9 | App "trm" "trm" |
14 | Lam x::"name" t::"trm" bind x in t |
10 | Lam x::"name" t::"trm" bind x in t |
15 | Let a::"lts" t::"trm" bind "bn a" in t |
11 | Let as::"assn" t::"trm" bind "bn as" in t |
16 and lts = |
12 and assn = |
17 Lnil |
13 ANil |
18 | Lcons "name" "trm" "lts" |
14 | ACons "name" "trm" "assn" |
19 binder |
15 binder |
20 bn |
16 bn |
21 where |
17 where |
22 "bn Lnil = []" |
18 "bn ANil = []" |
23 | "bn (Lcons x t l) = (atom x) # (bn l)" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
|
20 |
|
21 thm trm_assn.fv_defs |
|
22 thm trm_assn.eq_iff trm_assn.bn_defs |
|
23 thm trm_assn.bn_defs |
|
24 thm trm_assn.perm_simps |
|
25 thm trm_assn.induct[no_vars] |
|
26 thm trm_assn.inducts[no_vars] |
|
27 thm trm_assn.distinct |
|
28 thm trm_assn.supp |
|
29 thm trm_assn.fv_defs[simplified trm_assn.supp(1-2)] |
|
30 |
|
31 |
|
32 |
|
33 lemma fv_supp: |
|
34 shows "fv_trm = supp" |
|
35 and "fv_assn = supp" |
|
36 apply(rule ext) |
|
37 apply(rule trm_assn.supp) |
|
38 apply(rule ext) |
|
39 apply(rule trm_assn.supp) |
|
40 done |
|
41 |
|
42 lemmas eq_iffs = trm_assn.eq_iff[folded fv_supp[symmetric], folded Abs_eq_iff] |
|
43 |
|
44 lemmas supps = trm_assn.fv_defs[simplified trm_assn.supp(1-2)] |
|
45 |
|
46 lemma supp_fresh_eq: |
|
47 assumes "supp x = supp y" |
|
48 shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y" |
|
49 using assms |
|
50 by (simp add: fresh_def) |
|
51 |
|
52 lemma supp_not_in: |
|
53 assumes "x = y" |
|
54 shows "a \<notin> x \<longleftrightarrow> a \<notin> y" |
|
55 using assms |
|
56 by (simp add: fresh_def) |
|
57 |
|
58 lemmas freshs = |
|
59 supps(1)[THEN supp_not_in, folded fresh_def] |
|
60 supps(2)[THEN supp_not_in, simplified, folded fresh_def] |
|
61 supps(3)[THEN supp_not_in, folded fresh_def] |
|
62 supps(4)[THEN supp_not_in, folded fresh_def] |
|
63 supps(5)[THEN supp_not_in, simplified, folded fresh_def] |
|
64 supps(6)[THEN supp_not_in, simplified, folded fresh_def] |
|
65 |
|
66 lemma fin_bn: |
|
67 shows "finite (set (bn l))" |
|
68 apply(induct l rule: trm_assn.inducts(2)) |
|
69 apply(simp_all) |
|
70 done |
|
71 |
|
72 |
|
73 inductive |
|
74 test_trm :: "trm \<Rightarrow> bool" |
|
75 and test_assn :: "assn \<Rightarrow> bool" |
|
76 where |
|
77 "test_trm (Var x)" |
|
78 | "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)" |
|
79 | "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)" |
|
80 | "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)" |
|
81 | "test_assn ANil" |
|
82 | "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)" |
|
83 |
|
84 declare trm_assn.fv_bn_eqvt[eqvt] |
|
85 equivariance test_trm |
|
86 |
|
87 (* |
|
88 lemma |
|
89 fixes p::"perm" |
|
90 shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)" |
|
91 apply(induct t and as arbitrary: p and p rule: trm_assn.inducts) |
|
92 apply(simp) |
|
93 apply(rule test_trm_test_assn.intros) |
|
94 apply(simp) |
|
95 apply(rule test_trm_test_assn.intros) |
|
96 apply(assumption) |
|
97 apply(assumption) |
|
98 apply(simp) |
|
99 apply(rule test_trm_test_assn.intros) |
|
100 apply(assumption) |
|
101 apply(simp add: freshs fresh_star_def) |
|
102 apply(simp) |
|
103 defer |
|
104 apply(simp) |
|
105 apply(rule test_trm_test_assn.intros) |
|
106 apply(simp) |
|
107 apply(rule test_trm_test_assn.intros) |
|
108 apply(assumption) |
|
109 apply(assumption) |
|
110 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
|
111 apply(rule eq_iffs(4)[THEN iffD2]) |
|
112 defer |
|
113 apply(rule test_trm_test_assn.intros) |
|
114 prefer 3 |
|
115 thm freshs |
|
116 --"HERE" |
|
117 |
|
118 thm supps |
|
119 apply(rule test_trm_test_assn.intros) |
|
120 apply(assumption) |
|
121 |
|
122 apply(assumption) |
|
123 |
|
124 |
|
125 |
|
126 lemma |
|
127 fixes t::trm |
|
128 and as::assn |
|
129 and c::"'a::fs" |
|
130 assumes a1: "\<And>x c. P1 c (Var x)" |
|
131 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
|
132 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
|
133 and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)" |
|
134 and a5: "\<And>c. P2 c ANil" |
|
135 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
|
136 shows "P1 c t" and "P2 c as" |
|
137 proof - |
|
138 have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" |
|
139 and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)" |
|
140 apply(induct rule: trm_assn.inducts) |
|
141 apply(simp) |
|
142 apply(rule a1) |
|
143 apply(simp) |
|
144 apply(rule a2) |
|
145 apply(assumption) |
|
146 apply(assumption) |
|
147 -- "lam case" |
|
148 apply(simp) |
|
149 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
150 apply(erule exE) |
|
151 apply(erule conjE) |
|
152 apply(drule supp_perm_eq[symmetric]) |
|
153 apply(simp) |
|
154 apply(thin_tac "?X = ?Y") |
|
155 apply(rule a3) |
|
156 apply(simp add: atom_eqvt permute_set_eq) |
|
157 apply(simp only: permute_plus[symmetric]) |
|
158 apply(rule at_set_avoiding2) |
|
159 apply(simp add: finite_supp) |
|
160 apply(simp add: finite_supp) |
|
161 apply(simp add: finite_supp) |
|
162 apply(simp add: freshs fresh_star_def) |
|
163 --"let case" |
|
164 apply(simp) |
|
165 thm trm_assn.eq_iff |
|
166 thm eq_iffs |
|
167 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q") |
|
168 apply(erule exE) |
|
169 apply(erule conjE) |
|
170 prefer 2 |
|
171 apply(rule at_set_avoiding2) |
|
172 apply(rule fin_bn) |
|
173 apply(simp add: finite_supp) |
|
174 apply(simp add: finite_supp) |
|
175 apply(simp add: abs_fresh) |
|
176 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
|
177 prefer 2 |
|
178 apply(rule a4) |
|
179 prefer 4 |
|
180 apply(simp add: eq_iffs) |
|
181 apply(rule conjI) |
|
182 prefer 2 |
|
183 apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) |
|
184 apply(subst permute_plus[symmetric]) |
|
185 apply(blast) |
|
186 prefer 2 |
|
187 apply(simp add: eq_iffs) |
|
188 thm eq_iffs |
|
189 apply(subst permute_plus[symmetric]) |
|
190 apply(blast) |
|
191 apply(simp add: supps) |
|
192 apply(simp add: fresh_star_def freshs) |
|
193 apply(drule supp_perm_eq[symmetric]) |
|
194 apply(simp) |
|
195 apply(simp add: eq_iffs) |
|
196 apply(simp) |
|
197 apply(thin_tac "?X = ?Y") |
|
198 apply(rule a4) |
|
199 apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) |
|
200 apply(subst permute_plus[symmetric]) |
|
201 apply(blast) |
|
202 apply(subst permute_plus[symmetric]) |
|
203 apply(blast) |
|
204 apply(simp add: supps) |
|
205 thm at_set_avoiding2 |
|
206 --"HERE" |
|
207 apply(rule at_set_avoiding2) |
|
208 apply(rule fin_bn) |
|
209 apply(simp add: finite_supp) |
|
210 apply(simp add: finite_supp) |
|
211 apply(simp add: fresh_star_def freshs) |
|
212 apply(rule ballI) |
|
213 apply(simp add: eqvts permute_bn) |
|
214 apply(rule a5) |
|
215 apply(simp add: permute_bn) |
|
216 apply(rule a6) |
|
217 apply simp |
|
218 apply simp |
|
219 done |
|
220 then have a: "P1 c (0 \<bullet> t)" by blast |
|
221 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
222 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
223 qed |
|
224 *) |
24 |
225 |
25 text {* *} |
226 text {* *} |
26 |
227 |
27 (* |
228 (* |
28 |
|
29 thm trm_lts.fv |
|
30 thm trm_lts.eq_iff |
|
31 thm trm_lts.bn |
|
32 thm trm_lts.perm |
|
33 thm trm_lts.induct[no_vars] |
|
34 thm trm_lts.inducts[no_vars] |
|
35 thm trm_lts.distinct |
|
36 thm trm_lts.supp |
|
37 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
|
38 |
|
39 |
229 |
40 primrec |
230 primrec |
41 permute_bn_raw |
231 permute_bn_raw |
42 where |
232 where |
43 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
233 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |