11 | WP "weird" "weird" |
11 | WP "weird" "weird" |
12 |
12 |
13 thm permute_weird_raw.simps[no_vars] |
13 thm permute_weird_raw.simps[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
16 |
|
17 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)" |
|
18 apply (erule alpha_weird_raw.induct) |
|
19 defer |
|
20 apply (simp add: alpha_weird_raw.intros) |
|
21 apply (simp add: alpha_weird_raw.intros) |
|
22 apply (simp only: permute_weird_raw.simps) |
|
23 apply (rule alpha_weird_raw.intros) |
|
24 apply (erule exi[of _ _ "p"]) |
|
25 apply (erule exi[of _ _ "p"]) |
|
26 apply (erule exi[of _ _ "p"]) |
|
27 apply (erule exi[of _ _ "p"]) |
|
28 apply (erule conjE)+ |
|
29 apply (rule conjI) |
|
30 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) |
|
31 apply (simp add: eqvts) |
|
32 apply (simp add: eqvts) |
|
33 apply (rule conjI) |
|
34 defer |
|
35 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) |
|
36 apply (simp add: eqvts) |
|
37 apply (simp add: eqvts) |
|
38 apply (rule conjI) |
|
39 defer |
|
40 apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt) |
|
41 apply(simp add: alpha_gen.simps) |
|
42 apply(erule conjE)+ |
|
43 apply(rule conjI) |
|
44 apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) |
|
45 apply (simp add: eqvts) |
|
46 apply(rule conjI) |
|
47 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
|
48 apply (simp add: eqvts add_perm_eqvt) |
|
49 apply (simp add: permute_eqvt[symmetric]) |
|
50 done |
|
51 |
|
52 |
16 |
53 (* |
17 (* |
54 abbreviation "WBind \<equiv> WBind_raw" |
18 abbreviation "WBind \<equiv> WBind_raw" |
55 abbreviation "WP \<equiv> WP_raw" |
19 abbreviation "WP \<equiv> WP_raw" |
56 abbreviation "WV \<equiv> WV_raw" |
20 abbreviation "WV \<equiv> WV_raw" |