2 imports "../Parser" |
2 imports "../Parser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype lm = |
7 nominal_datatype lam = |
8 Vr "name" |
8 Var "name" |
9 | Ap "lm" "lm" |
9 | App "lam" "lam" |
10 | Lm x::"name" l::"lm" bind x in l |
10 | Lam x::"name" l::"lam" bind x in l |
11 |
11 |
12 lemmas supp_fn' = lm.fv[simplified lm.supp] |
12 lemmas supp_fn' = lam.fv[simplified lam.supp] |
|
13 |
|
14 section {* Strong Induction Principles*} |
13 |
15 |
14 (* |
16 (* |
15 Old way of establishing strong induction |
17 Old way of establishing strong induction |
16 principles by chosing a fresh name. |
18 principles by chosing a fresh name. |
17 *) |
19 *) |
18 lemma |
20 lemma |
19 fixes c::"'a::fs" |
21 fixes c::"'a::fs" |
20 assumes a1: "\<And>name c. P c (Vr name)" |
22 assumes a1: "\<And>name c. P c (Var name)" |
21 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
23 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
22 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
24 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
23 shows "P c lm" |
25 shows "P c lam" |
24 proof - |
26 proof - |
25 have "\<And>p. P c (p \<bullet> lm)" |
27 have "\<And>p. P c (p \<bullet> lam)" |
26 apply(induct lm arbitrary: c rule: lm.induct) |
28 apply(induct lam arbitrary: c rule: lam.induct) |
27 apply(simp only: lm.perm) |
29 apply(simp only: lam.perm) |
28 apply(rule a1) |
30 apply(rule a1) |
29 apply(simp only: lm.perm) |
31 apply(simp only: lam.perm) |
30 apply(rule a2) |
32 apply(rule a2) |
31 apply(assumption) |
33 apply(assumption) |
32 apply(assumption) |
34 apply(assumption) |
33 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lm (p \<bullet> name) (p \<bullet> lm))") |
35 apply(subgoal_tac "\<exists>new::name. (atom new) \<sharp> (c, Lam (p \<bullet> name) (p \<bullet> lam))") |
34 defer |
36 defer |
35 apply(simp add: fresh_def) |
37 apply(simp add: fresh_def) |
36 apply(rule_tac X="supp (c, Lm (p \<bullet> name) (p \<bullet> lm))" in obtain_at_base) |
38 apply(rule_tac X="supp (c, Lam (p \<bullet> name) (p \<bullet> lam))" in obtain_at_base) |
37 apply(simp add: supp_Pair finite_supp) |
39 apply(simp add: supp_Pair finite_supp) |
38 apply(blast) |
40 apply(blast) |
39 apply(erule exE) |
41 apply(erule exE) |
40 apply(rule_tac t="p \<bullet> Lm name lm" and |
42 apply(rule_tac t="p \<bullet> Lam name lam" and |
41 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst) |
43 s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lam name lam" in subst) |
42 apply(simp del: lm.perm) |
44 apply(simp del: lam.perm) |
43 apply(subst lm.perm) |
45 apply(subst lam.perm) |
44 apply(subst (2) lm.perm) |
46 apply(subst (2) lam.perm) |
45 apply(rule flip_fresh_fresh) |
47 apply(rule flip_fresh_fresh) |
46 apply(simp add: fresh_def) |
48 apply(simp add: fresh_def) |
47 apply(simp only: supp_fn') |
49 apply(simp only: supp_fn') |
48 apply(simp) |
50 apply(simp) |
49 apply(simp add: fresh_Pair) |
51 apply(simp add: fresh_Pair) |
51 apply(rule a3) |
53 apply(rule a3) |
52 apply(simp add: fresh_Pair) |
54 apply(simp add: fresh_Pair) |
53 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
55 apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec) |
54 apply(simp) |
56 apply(simp) |
55 done |
57 done |
56 then have "P c (0 \<bullet> lm)" by blast |
58 then have "P c (0 \<bullet> lam)" by blast |
57 then show "P c lm" by simp |
59 then show "P c lam" by simp |
58 qed |
60 qed |
59 |
61 |
60 (* |
62 (* |
61 New way of establishing strong induction |
63 New way of establishing strong induction |
62 principles by using a appropriate permutation. |
64 principles by using a appropriate permutation. |
63 *) |
65 *) |
64 lemma |
66 lemma |
65 fixes c::"'a::fs" |
67 fixes c::"'a::fs" |
66 assumes a1: "\<And>name c. P c (Vr name)" |
68 assumes a1: "\<And>name c. P c (Var name)" |
67 and a2: "\<And>lm1 lm2 c. \<lbrakk>\<And>d. P d lm1; \<And>d. P d lm2\<rbrakk> \<Longrightarrow> P c (Ap lm1 lm2)" |
69 and a2: "\<And>lam1 lam2 c. \<lbrakk>\<And>d. P d lam1; \<And>d. P d lam2\<rbrakk> \<Longrightarrow> P c (App lam1 lam2)" |
68 and a3: "\<And>name lm c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lm\<rbrakk> \<Longrightarrow> P c (Lm name lm)" |
70 and a3: "\<And>name lam c. \<lbrakk>atom name \<sharp> c; \<And>d. P d lam\<rbrakk> \<Longrightarrow> P c (Lam name lam)" |
69 shows "P c lm" |
71 shows "P c lam" |
70 proof - |
72 proof - |
71 have "\<And>p. P c (p \<bullet> lm)" |
73 have "\<And>p. P c (p \<bullet> lam)" |
72 apply(induct lm arbitrary: c rule: lm.induct) |
74 apply(induct lam arbitrary: c rule: lam.induct) |
73 apply(simp only: lm.perm) |
75 apply(simp only: lam.perm) |
74 apply(rule a1) |
76 apply(rule a1) |
75 apply(simp only: lm.perm) |
77 apply(simp only: lam.perm) |
76 apply(rule a2) |
78 apply(rule a2) |
77 apply(assumption) |
79 apply(assumption) |
78 apply(assumption) |
80 apply(assumption) |
79 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lm name lm) \<sharp>* q") |
81 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom name}) \<sharp>* c \<and> supp (p \<bullet> Lam name lam) \<sharp>* q") |
80 apply(erule exE) |
82 apply(erule exE) |
81 apply(rule_tac t="p \<bullet> Lm name lm" and |
83 apply(rule_tac t="p \<bullet> Lam name lam" and |
82 s="q \<bullet> p \<bullet> Lm name lm" in subst) |
84 s="q \<bullet> p \<bullet> Lam name lam" in subst) |
83 defer |
85 defer |
84 apply(simp add: lm.perm) |
86 apply(simp add: lam.perm) |
85 apply(rule a3) |
87 apply(rule a3) |
86 apply(simp add: eqvts fresh_star_def) |
88 apply(simp add: eqvts fresh_star_def) |
87 apply(drule_tac x="q + p" in meta_spec) |
89 apply(drule_tac x="q + p" in meta_spec) |
88 apply(simp) |
90 apply(simp) |
89 apply(rule at_set_avoiding2) |
91 apply(rule at_set_avoiding2) |
90 apply(simp add: finite_supp) |
92 apply(simp add: finite_supp) |
91 apply(simp add: finite_supp) |
93 apply(simp add: finite_supp) |
92 apply(simp add: finite_supp) |
94 apply(simp add: finite_supp) |
93 apply(simp only: lm.perm atom_eqvt) |
95 apply(simp only: lam.perm atom_eqvt) |
94 apply(simp add: fresh_star_def fresh_def supp_fn') |
96 apply(simp add: fresh_star_def fresh_def supp_fn') |
95 apply(rule supp_perm_eq) |
97 apply(rule supp_perm_eq) |
96 apply(simp) |
98 apply(simp) |
97 done |
99 done |
98 then have "P c (0 \<bullet> lm)" by blast |
100 then have "P c (0 \<bullet> lam)" by blast |
99 then show "P c lm" by simp |
101 then show "P c lam" by simp |
100 qed |
102 qed |
101 |
103 |
|
104 section {* size function *} |
|
105 |
|
106 lemma size_eqvt_raw: |
|
107 fixes t::"lam_raw" |
|
108 shows "size (pi \<bullet> t) = size t" |
|
109 apply (induct rule: lam_raw.inducts) |
|
110 apply simp_all |
|
111 done |
|
112 |
|
113 instantiation lam :: size |
|
114 begin |
|
115 |
|
116 quotient_definition |
|
117 "size_lam :: lam \<Rightarrow> nat" |
|
118 is |
|
119 "size :: lam_raw \<Rightarrow> nat" |
|
120 |
|
121 lemma size_rsp: |
|
122 "alpha_lam_raw x y \<Longrightarrow> size x = size y" |
|
123 apply (induct rule: alpha_lam_raw.inducts) |
|
124 apply (simp_all only: lam_raw.size) |
|
125 apply (simp_all only: alphas) |
|
126 apply clarify |
|
127 apply (simp_all only: size_eqvt_raw) |
|
128 done |
|
129 |
|
130 lemma [quot_respect]: |
|
131 "(alpha_lam_raw ===> op =) size size" |
|
132 by (simp_all add: size_rsp) |
|
133 |
|
134 lemma [quot_preserve]: |
|
135 "(rep_lam ---> id) size = size" |
|
136 by (simp_all add: size_lam_def) |
|
137 |
|
138 instance |
|
139 by default |
|
140 |
102 end |
141 end |
103 |
142 |
104 |
143 lemmas size_lam[simp] = |
105 |
144 lam_raw.size(4)[quot_lifted] |
|
145 lam_raw.size(5)[quot_lifted] |
|
146 lam_raw.size(6)[quot_lifted] |
|
147 |
|
148 (* is this needed? *) |
|
149 lemma [measure_function]: |
|
150 "is_measure (size::lam\<Rightarrow>nat)" |
|
151 by (rule is_measure_trivial) |
|
152 |
|
153 section {* Matching *} |
|
154 |
|
155 definition |
|
156 MATCH :: "('c::pt \<Rightarrow> (bool * 'a::pt * 'b::pt)) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
|
157 where |
|
158 "MATCH M d x \<equiv> if (\<exists>!r. \<exists>q. M q = (True, x, r)) then (THE r. \<exists>q. M q = (True, x, r)) else d" |
|
159 |
|
160 (* |
|
161 lemma MATCH_eqvt: |
|
162 shows "p \<bullet> (MATCH M d x) = MATCH (p \<bullet> M) (p \<bullet> d) (p \<bullet> x)" |
|
163 unfolding MATCH_def |
|
164 apply(perm_simp the_eqvt) |
|
165 apply (tactic {* Nominal_Permeq.eqvt_tac @{context} 1 *}) |
|
166 apply(simp) |
|
167 thm eqvts_raw |
|
168 apply(subst if_eqvt) |
|
169 apply(subst ex1_eqvt) |
|
170 apply(subst permute_fun_def) |
|
171 apply(subst ex_eqvt) |
|
172 apply(subst permute_fun_def) |
|
173 apply(subst eq_eqvt) |
|
174 apply(subst permute_fun_app_eq[where f="M"]) |
|
175 apply(simp only: permute_minus_cancel) |
|
176 apply(subst permute_prod.simps) |
|
177 apply(subst permute_prod.simps) |
|
178 apply(simp only: permute_minus_cancel) |
|
179 apply(simp only: permute_bool_def) |
|
180 apply(simp) |
|
181 apply(subst ex1_eqvt) |
|
182 apply(subst permute_fun_def) |
|
183 apply(subst ex_eqvt) |
|
184 apply(subst permute_fun_def) |
|
185 apply(subst eq_eqvt) |
|
186 |
|
187 apply(simp only: eqvts) |
|
188 apply(simp) |
|
189 apply(subgoal_tac "(p \<bullet> (\<exists>!r. \<exists>q. M q = (True, x, r))) = (\<exists>!r. \<exists>q. (p \<bullet> M) q = (True, p \<bullet> x, r))") |
|
190 apply(drule sym) |
|
191 apply(simp) |
|
192 apply(rule impI) |
|
193 apply(simp add: perm_bool) |
|
194 apply(rule trans) |
|
195 apply(rule pt_the_eqvt[OF pta at]) |
|
196 apply(assumption) |
|
197 apply(simp add: pt_ex_eqvt[OF pt at]) |
|
198 apply(simp add: pt_eq_eqvt[OF ptb at]) |
|
199 apply(rule cheat) |
|
200 apply(rule trans) |
|
201 apply(rule pt_ex1_eqvt) |
|
202 apply(rule pta) |
|
203 apply(rule at) |
|
204 apply(simp add: pt_ex_eqvt[OF pt at]) |
|
205 apply(simp add: pt_eq_eqvt[OF ptb at]) |
|
206 apply(subst pt_pi_rev[OF pta at]) |
|
207 apply(subst pt_fun_app_eq[OF pt at]) |
|
208 apply(subst pt_pi_rev[OF pt at]) |
|
209 apply(simp) |
|
210 done |
|
211 |
|
212 lemma MATCH_cng: |
|
213 assumes a: "M1 = M2" "d1 = d2" |
|
214 shows "MATCH M1 d1 x = MATCH M2 d2 x" |
|
215 using a by simp |
|
216 |
|
217 lemma MATCH_eq: |
|
218 assumes a: "t = l x" "G x" "\<And>x'. t = l x' \<Longrightarrow> G x' \<Longrightarrow> r x' = r x" |
|
219 shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = r x" |
|
220 using a |
|
221 unfolding MATCH_def |
|
222 apply(subst if_P) |
|
223 apply(rule_tac a="r x" in ex1I) |
|
224 apply(rule_tac x="x" in exI) |
|
225 apply(blast) |
|
226 apply(erule exE) |
|
227 apply(drule_tac x="q" in meta_spec) |
|
228 apply(auto)[1] |
|
229 apply(rule the_equality) |
|
230 apply(blast) |
|
231 apply(erule exE) |
|
232 apply(drule_tac x="q" in meta_spec) |
|
233 apply(auto)[1] |
|
234 done |
|
235 |
|
236 lemma MATCH_eq2: |
|
237 assumes a: "t = l x1 x2" "G x1 x2" "\<And>x1' x2'. t = l x1' x2' \<Longrightarrow> G x1' x2' \<Longrightarrow> r x1' x2' = r x1 x2" |
|
238 shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = r x1 x2" |
|
239 sorry |
|
240 |
|
241 lemma MATCH_neq: |
|
242 assumes a: "\<And>x. t = l x \<Longrightarrow> G x \<Longrightarrow> False" |
|
243 shows "MATCH (\<lambda>x. (G x, l x, r x)) d t = d" |
|
244 using a |
|
245 unfolding MATCH_def |
|
246 apply(subst if_not_P) |
|
247 apply(blast) |
|
248 apply(rule refl) |
|
249 done |
|
250 |
|
251 lemma MATCH_neq2: |
|
252 assumes a: "\<And>x1 x2. t = l x1 x2 \<Longrightarrow> G x1 x2 \<Longrightarrow> False" |
|
253 shows "MATCH (\<lambda>(x1,x2). (G x1 x2, l x1 x2, r x1 x2)) d t = d" |
|
254 using a |
|
255 unfolding MATCH_def |
|
256 apply(subst if_not_P) |
|
257 apply(auto) |
|
258 done |
|
259 *) |
|
260 |
|
261 end |
|
262 |
|
263 |
|
264 |