35 thm trm_assn.exhaust |
48 thm trm_assn.exhaust |
36 thm trm_assn.strong_exhaust |
49 thm trm_assn.strong_exhaust |
37 thm trm_assn.perm_bn_simps |
50 thm trm_assn.perm_bn_simps |
38 |
51 |
39 thm alpha_bn_raw.cases |
52 thm alpha_bn_raw.cases |
40 |
53 thm trm_assn.alpha_refl |
|
54 thm trm_assn.alpha_sym |
|
55 thm trm_assn.alpha_trans |
41 |
56 |
42 lemmas alpha_bn_cases[consumes 1] = alpha_bn_raw.cases[quot_lifted] |
57 lemmas alpha_bn_cases[consumes 1] = alpha_bn_raw.cases[quot_lifted] |
43 |
58 |
44 lemma alpha_bn_refl: "alpha_bn x x" |
59 lemma alpha_bn_refl: "alpha_bn x x" |
45 by (induct x rule: trm_assn.inducts(2)) |
60 by(rule trm_assn.alpha_refl) |
46 (rule TrueI, auto simp add: trm_assn.eq_iff) |
61 |
47 lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x" |
62 lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x" |
48 apply(erule alpha_bn_cases) |
63 by (rule trm_assn.alpha_sym) |
49 apply(auto) |
|
50 done |
|
51 |
64 |
52 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
65 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
53 sorry |
66 using trm_assn.alpha_trans by metis |
54 |
67 |
55 lemma k: "A \<Longrightarrow> A \<and> A" by blast |
68 lemma k: "A \<Longrightarrow> A \<and> A" by blast |
56 |
69 |
57 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
70 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
58 by (simp add: permute_pure) |
71 by (simp add: permute_pure) |
131 apply(erule_tac c="()" in Abs_lst_fcb2) |
144 apply(erule_tac c="()" in Abs_lst_fcb2) |
132 apply(simp_all add: pure_fresh fresh_star_def)[3] |
145 apply(simp_all add: pure_fresh fresh_star_def)[3] |
133 apply(simp_all add: eqvt_at_def) |
146 apply(simp_all add: eqvt_at_def) |
134 done |
147 done |
135 |
148 |
|
149 (* assn-function prevents automatic discharge |
|
150 termination by lexicographic_order |
|
151 *) |
136 |
152 |
137 nominal_primrec |
153 nominal_primrec |
138 subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
154 subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::= _]" [90, 90, 90] 90) |
139 where |
155 where |
140 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
156 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
164 |
180 |
165 section {* direct definitions --- problems *} |
181 section {* direct definitions --- problems *} |
166 |
182 |
167 lemma cheat: "P" sorry |
183 lemma cheat: "P" sorry |
168 |
184 |
169 nominal_primrec (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y") |
185 nominal_primrec |
|
186 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y") |
170 height_trm2 :: "trm \<Rightarrow> nat" |
187 height_trm2 :: "trm \<Rightarrow> nat" |
171 and height_assn2 :: "assn \<Rightarrow> nat" |
188 and height_assn2 :: "assn \<Rightarrow> nat" |
172 where |
189 where |
173 "height_trm2 (Var x) = 1" |
190 "height_trm2 (Var x) = 1" |
174 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
191 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
175 | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" |
192 | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" |
176 | "height_assn2 (Assn x t) = (height_trm2 t)" |
193 | "height_assn2 (Assn x t) = (height_trm2 t)" |
177 thm height_trm2_height_assn2_graph.intros |
194 thm height_trm2_height_assn2_graph.intros[no_vars] |
178 thm height_trm2_height_assn2_graph_def |
195 thm height_trm2_height_assn2_graph_def |
179 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
196 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
180 apply (rule, perm_simp, rule) |
197 apply (rule, perm_simp, rule) |
181 apply(erule height_trm2_height_assn2_graph.induct) |
198 apply(erule height_trm2_height_assn2_graph.induct) |
182 -- "invariant" |
199 -- "invariant" |
297 apply(simp) |
314 apply(simp) |
298 done |
315 done |
299 |
316 |
300 |
317 |
301 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
318 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
302 subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm= _]" [90, 90, 90] 90) and |
319 subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_ [_ ::trm2= _]" [90, 90, 90] 90) and |
303 subst_assn :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn= _]" [90, 90, 90] 90) |
320 subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn" ("_ [_ ::assn2= _]" [90, 90, 90] 90) |
304 where |
321 where |
305 "(Var x)[y ::trm= s] = (if x = y then s else (Var x))" |
322 "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))" |
306 | "(App t1 t2)[y ::trm= s] = App (t1[y ::trm= s]) (t2[y ::trm= s])" |
323 | "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])" |
307 | "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm= s] = Let (ast[y ::assn= s]) (t[y ::trm= s])" |
324 | "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])" |
308 | "(Assn x t)[y ::assn= s] = Assn x (t[y ::trm= s])" |
325 | "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])" |
309 apply(subgoal_tac "\<And>p x r. subst_trm_subst_assn_graph x r \<Longrightarrow> subst_trm_subst_assn_graph (p \<bullet> x) (p \<bullet> r)") |
326 apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)") |
310 apply(simp add: eqvt_def) |
327 apply(simp add: eqvt_def) |
311 apply(rule allI) |
328 apply(rule allI) |
312 apply(simp add: permute_fun_def permute_bool_def) |
329 apply(simp add: permute_fun_def permute_bool_def) |
313 apply(rule ext) |
330 apply(rule ext) |
314 apply(rule ext) |
331 apply(rule ext) |
334 apply(case_tac b) |
351 apply(case_tac b) |
335 apply(simp) |
352 apply(simp) |
336 apply(rule_tac y="a" in trm_assn.exhaust(2)) |
353 apply(rule_tac y="a" in trm_assn.exhaust(2)) |
337 apply(simp) |
354 apply(simp) |
338 apply(blast) |
355 apply(blast) |
339 apply(simp_all)[7] |
356 --"compatibility" |
|
357 apply(all_trivials) |
|
358 apply(simp) |
|
359 apply(simp) |
340 prefer 2 |
360 prefer 2 |
341 apply(simp) |
361 apply(simp) |
342 prefer 2 |
362 thm Inl_inject |
343 apply(simp) |
363 apply(drule Inl_inject) |
344 apply(simp) |
364 apply(rule arg_cong) |
345 apply (simp only: meta_eq_to_obj_eq[OF subst_trm_def, symmetric, unfolded fun_eq_iff]) |
365 back |
346 apply (simp only: meta_eq_to_obj_eq[OF subst_assn_def, symmetric, unfolded fun_eq_iff]) |
366 apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff]) |
347 apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn ast ya sa) ast") |
367 apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff]) |
348 apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn asta ya sa) asta") |
368 apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn2 ast ya sa) ast") |
349 apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm t ya sa) t") |
369 apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn2 asta ya sa) asta") |
350 apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm ta ya sa) ta") |
370 apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm2 t ya sa) t") |
351 apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (ast, ya, sa))") |
371 apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm2 ta ya sa) ta") |
352 apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (asta, ya, sa))") |
372 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))") |
353 apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (t, ya, sa))") |
373 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))") |
354 apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (ta, ya, sa))") |
374 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))") |
355 defer |
375 apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))") |
|
376 defer |
|
377 apply(simp add: Abs_eq_iff alphas) |
|
378 apply(clarify) |
|
379 apply(rule eqvt_at_perm) |
|
380 apply(simp) |
|
381 apply(simp add: subst_trm2_def) |
|
382 apply(simp add: eqvt_at_def) |
356 defer |
383 defer |
357 defer |
384 defer |
358 defer |
385 defer |
359 defer |
386 defer |
360 defer |
387 defer |
361 apply(rule conjI) |
388 apply(rule conjI) |
362 apply (subgoal_tac "subst_assn ast ya sa= subst_assn asta ya sa") |
389 apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa") |
363 apply (subgoal_tac "subst_trm t ya sa = subst_trm ta ya sa") |
390 apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa") |
364 apply(simp) |
391 apply(simp) |
365 apply(erule_tac conjE)+ |
392 apply(erule_tac conjE)+ |
366 apply(erule alpha_bn_cases) |
393 apply(erule alpha_bn_cases) |
367 apply(simp add: trm_assn.bn_defs) |
394 apply(simp add: trm_assn.bn_defs) |
368 apply(rotate_tac 7) |
395 apply(rotate_tac 7) |