1 theory ExLet |
|
2 imports "../NewParser" "../../Attic/Prove" |
|
3 begin |
|
4 |
|
5 text {* example 3 or example 5 from Terms.thy *} |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 nominal_datatype trm = |
|
10 Vr "name" |
|
11 | Ap "trm" "trm" |
|
12 | Lm x::"name" t::"trm" bind_set x in t |
|
13 | Lt a::"lts" t::"trm" bind "bn a" in t |
|
14 (*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*) |
|
15 and lts = |
|
16 Lnil |
|
17 | Lcons "name" "trm" "lts" |
|
18 binder |
|
19 bn |
|
20 where |
|
21 "bn Lnil = []" |
|
22 | "bn (Lcons x t l) = (atom x) # (bn l)" |
|
23 |
|
24 |
|
25 thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros |
|
26 |
|
27 thm trm_lts.fv |
|
28 thm trm_lts.eq_iff |
|
29 thm trm_lts.bn |
|
30 thm trm_lts.perm |
|
31 thm trm_lts.induct[no_vars] |
|
32 thm trm_lts.inducts[no_vars] |
|
33 thm trm_lts.distinct |
|
34 (*thm trm_lts.supp*) |
|
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
|
36 |
|
37 |
|
38 primrec |
|
39 permute_bn_raw |
|
40 where |
|
41 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
|
42 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
|
43 |
|
44 quotient_definition |
|
45 "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
46 is |
|
47 "permute_bn_raw" |
|
48 |
|
49 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
|
50 apply simp |
|
51 apply clarify |
|
52 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
53 apply (rule TrueI)+ |
|
54 apply simp_all |
|
55 apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
56 apply simp_all |
|
57 done |
|
58 |
|
59 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
60 |
|
61 lemma permute_bn_zero: |
|
62 "permute_bn 0 a = a" |
|
63 apply(induct a rule: trm_lts.inducts(2)) |
|
64 apply(rule TrueI)+ |
|
65 apply(simp_all add:permute_bn) |
|
66 done |
|
67 |
|
68 lemma permute_bn_add: |
|
69 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
|
70 oops |
|
71 |
|
72 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
|
73 apply(induct lts rule: trm_lts.inducts(2)) |
|
74 apply(rule TrueI)+ |
|
75 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
|
76 done |
|
77 |
|
78 lemma perm_bn: |
|
79 "p \<bullet> bn l = bn(permute_bn p l)" |
|
80 apply(induct l rule: trm_lts.inducts(2)) |
|
81 apply(rule TrueI)+ |
|
82 apply(simp_all add:permute_bn eqvts) |
|
83 done |
|
84 |
|
85 lemma fv_perm_bn: |
|
86 "fv_bn l = fv_bn (permute_bn p l)" |
|
87 apply(induct l rule: trm_lts.inducts(2)) |
|
88 apply(rule TrueI)+ |
|
89 apply(simp_all add:permute_bn eqvts) |
|
90 done |
|
91 |
|
92 lemma Lt_subst: |
|
93 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
|
94 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
|
95 apply (rule_tac x="q" in exI) |
|
96 apply (simp add: alphas) |
|
97 apply (simp add: perm_bn[symmetric]) |
|
98 apply(rule conjI) |
|
99 apply(drule supp_perm_eq) |
|
100 apply(simp add: abs_eq_iff) |
|
101 apply(simp add: alphas_abs alphas) |
|
102 apply(drule conjunct1) |
|
103 apply (simp add: trm_lts.supp) |
|
104 apply(simp add: supp_abs) |
|
105 apply (simp add: trm_lts.supp) |
|
106 done |
|
107 |
|
108 |
|
109 lemma fin_bn: |
|
110 "finite (set (bn l))" |
|
111 apply(induct l rule: trm_lts.inducts(2)) |
|
112 apply(simp_all add:permute_bn eqvts) |
|
113 done |
|
114 |
|
115 thm trm_lts.inducts[no_vars] |
|
116 |
|
117 lemma |
|
118 fixes t::trm |
|
119 and l::lts |
|
120 and c::"'a::fs" |
|
121 assumes a1: "\<And>name c. P1 c (Vr name)" |
|
122 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
|
123 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
|
124 and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
|
125 and a5: "\<And>c. P2 c Lnil" |
|
126 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
|
127 shows "P1 c t" and "P2 c l" |
|
128 proof - |
|
129 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
|
130 b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
|
131 apply(induct rule: trm_lts.inducts) |
|
132 apply(simp) |
|
133 apply(rule a1) |
|
134 apply(simp) |
|
135 apply(rule a2) |
|
136 apply(simp) |
|
137 apply(simp) |
|
138 apply(simp) |
|
139 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
140 apply(erule exE) |
|
141 apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" |
|
142 and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst) |
|
143 apply(rule supp_perm_eq) |
|
144 apply(simp) |
|
145 apply(simp) |
|
146 apply(rule a3) |
|
147 apply(simp add: atom_eqvt) |
|
148 apply(subst permute_plus[symmetric]) |
|
149 apply(blast) |
|
150 apply(rule at_set_avoiding2_atom) |
|
151 apply(simp add: finite_supp) |
|
152 apply(simp add: finite_supp) |
|
153 apply(simp add: fresh_def) |
|
154 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
155 apply(simp) |
|
156 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
|
157 apply(erule exE) |
|
158 apply(erule conjE) |
|
159 thm Lt_subst |
|
160 apply(subst Lt_subst) |
|
161 apply assumption |
|
162 apply(rule a4) |
|
163 apply(simp add:perm_bn[symmetric]) |
|
164 apply(simp add: eqvts) |
|
165 apply (simp add: fresh_star_def fresh_def) |
|
166 apply(rotate_tac 1) |
|
167 apply(drule_tac x="q + p" in meta_spec) |
|
168 apply(simp) |
|
169 apply(rule at_set_avoiding2) |
|
170 apply(rule fin_bn) |
|
171 apply(simp add: finite_supp) |
|
172 apply(simp add: finite_supp) |
|
173 apply(simp add: fresh_star_def fresh_def supp_abs) |
|
174 apply(simp add: eqvts permute_bn) |
|
175 apply(rule a5) |
|
176 apply(simp add: permute_bn) |
|
177 apply(rule a6) |
|
178 apply simp |
|
179 apply simp |
|
180 done |
|
181 then have a: "P1 c (0 \<bullet> t)" by blast |
|
182 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
183 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
184 qed |
|
185 |
|
186 |
|
187 |
|
188 lemma lets_bla: |
|
189 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
|
190 by (simp add: trm_lts.eq_iff) |
|
191 |
|
192 lemma lets_ok: |
|
193 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
|
194 apply (simp add: trm_lts.eq_iff) |
|
195 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
196 apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) |
|
197 done |
|
198 |
|
199 lemma lets_ok3: |
|
200 "x \<noteq> y \<Longrightarrow> |
|
201 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
202 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
|
203 apply (simp add: alphas trm_lts.eq_iff) |
|
204 done |
|
205 |
|
206 |
|
207 lemma lets_not_ok1: |
|
208 "x \<noteq> y \<Longrightarrow> |
|
209 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
210 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
|
211 apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) |
|
212 done |
|
213 |
|
214 lemma lets_nok: |
|
215 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
216 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
217 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
|
218 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
|
219 done |
|
220 |
|
221 |
|
222 end |
|
223 |
|
224 |
|
225 |
|