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 |
16 |
17 (* |
17 |
18 abbreviation "WBind \<equiv> WBind_raw" |
18 abbreviation "WBind \<equiv> WBind_raw" |
19 abbreviation "WP \<equiv> WP_raw" |
19 abbreviation "WP \<equiv> WP_raw" |
20 abbreviation "WV \<equiv> WV_raw" |
20 abbreviation "WV \<equiv> WV_raw" |
21 |
21 |
22 lemma test: |
22 lemma test: |
23 assumes a: "distinct [x, y, z]" |
23 assumes a: "distinct [x, y, z]" |
24 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
24 shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
25 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
25 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
26 apply(rule_tac alpha_weird.intros) |
26 apply(rule_tac alpha_weird_raw.intros) |
27 unfolding alpha_gen |
27 unfolding alpha_gen |
28 using a |
28 using a |
|
29 apply(auto) |
|
30 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
31 apply(auto) |
|
32 apply(simp add: fresh_star_def flip_def fresh_def supp_swap) |
|
33 apply(rule alpha_weird_raw.intros) |
|
34 apply(simp add: alpha_weird_raw.intros(2)) |
|
35 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
36 apply(rule_tac x="0" in exI) |
|
37 apply(simp add: fresh_star_def) |
|
38 apply(auto) |
|
39 apply(rule alpha_weird_raw.intros) |
|
40 apply(simp add: alpha_weird_raw.intros(2)) |
|
41 apply(simp add: flip_def supp_swap supp_perm) |
|
42 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
29 apply(simp) |
43 apply(simp) |
30 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
31 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
32 apply(simp add: fresh_star_def) |
|
33 apply(simp add: flip_def) |
|
34 apply(auto) |
44 apply(auto) |
35 prefer 2 |
45 apply(simp add: flip_def fresh_def supp_swap) |
36 apply(rule alpha_weird.intros) |
46 apply(rule alpha_weird_raw.intros) |
37 apply(simp add: alpha_weird.intros(2)) |
47 apply(simp add: alpha_weird_raw.intros(2)) |
38 prefer 2 |
48 done |
39 apply(rule alpha_weird.intros) |
|
40 apply(simp add: alpha_weird.intros(2)) |
|
41 apply(simp) |
|
42 apply(rule alpha_weird.intros) |
|
43 apply(simp) |
|
44 apply(simp add: alpha_gen) |
|
45 using a |
|
46 apply(simp) |
|
47 *) |
|
48 |
49 |
49 text {* example 1 *} |
50 text {* example 1 *} |
50 |
51 |
51 (* ML {* set show_hyps *} *) |
52 (* ML {* set show_hyps *} *) |
52 |
53 |