72 apply assumption |
72 apply assumption |
73 apply (simp add: alpha_eqvt) |
73 apply (simp add: alpha_eqvt) |
74 sorry |
74 sorry |
75 |
75 |
76 |
76 |
77 (* |
77 |
78 abbreviation "WBind \<equiv> WBind_raw" |
78 abbreviation "WBind \<equiv> WBind_raw" |
79 abbreviation "WP \<equiv> WP_raw" |
79 abbreviation "WP \<equiv> WP_raw" |
80 abbreviation "WV \<equiv> WV_raw" |
80 abbreviation "WV \<equiv> WV_raw" |
81 |
81 |
82 lemma test: |
82 lemma test: |
83 assumes a: "distinct [x, y, z]" |
83 assumes a: "distinct [x, y, z]" |
84 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
84 shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
85 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
85 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
86 apply(rule_tac alpha_weird.intros) |
86 apply(rule_tac alpha_weird_raw.intros) |
87 unfolding alpha_gen |
87 unfolding alpha_gen |
88 using a |
88 using a |
|
89 apply(auto) |
|
90 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
91 apply(auto) |
|
92 apply(simp add: fresh_star_def flip_def fresh_def supp_swap) |
|
93 apply(rule alpha_weird_raw.intros) |
|
94 apply(simp add: alpha_weird_raw.intros(2)) |
|
95 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
96 apply(rule_tac x="0" in exI) |
|
97 apply(simp add: fresh_star_def) |
|
98 apply(auto) |
|
99 apply(rule alpha_weird_raw.intros) |
|
100 apply(simp add: alpha_weird_raw.intros(2)) |
|
101 apply(simp add: flip_def supp_swap supp_perm) |
|
102 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
89 apply(simp) |
103 apply(simp) |
90 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
91 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
92 apply(simp add: fresh_star_def) |
|
93 apply(simp add: flip_def) |
|
94 apply(auto) |
104 apply(auto) |
95 prefer 2 |
105 apply(simp add: flip_def fresh_def supp_swap) |
96 apply(rule alpha_weird.intros) |
106 apply(rule alpha_weird_raw.intros) |
97 apply(simp add: alpha_weird.intros(2)) |
107 apply(simp add: alpha_weird_raw.intros(2)) |
98 prefer 2 |
108 done |
99 apply(rule alpha_weird.intros) |
|
100 apply(simp add: alpha_weird.intros(2)) |
|
101 apply(simp) |
|
102 apply(rule alpha_weird.intros) |
|
103 apply(simp) |
|
104 apply(simp add: alpha_gen) |
|
105 using a |
|
106 apply(simp) |
|
107 *) |
|
108 |
109 |
109 text {* example 1 *} |
110 text {* example 1 *} |
110 |
111 |
111 (* ML {* set show_hyps *} *) |
112 (* ML {* set show_hyps *} *) |
112 |
113 |