52 (auto simp add: le_fun_def le_bool_def alphas) |
52 (auto simp add: le_fun_def le_bool_def alphas) |
53 |
53 |
54 fun |
54 fun |
55 alpha_abs |
55 alpha_abs |
56 where |
56 where |
|
57 [simp del]: |
57 "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
58 "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
58 |
59 |
59 fun |
60 fun |
60 alpha_abs_lst |
61 alpha_abs_lst |
61 where |
62 where |
|
63 [simp del]: |
62 "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))" |
64 "alpha_abs_lst (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))" |
63 |
65 |
64 fun |
66 fun |
65 alpha_abs_res |
67 alpha_abs_res |
66 where |
68 where |
|
69 [simp del]: |
67 "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))" |
70 "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))" |
68 |
71 |
69 notation |
72 notation |
70 alpha_abs ("_ \<approx>abs _") and |
73 alpha_abs (infix "\<approx>abs" 50) and |
71 alpha_abs_lst ("_ \<approx>abs'_lst _") and |
74 alpha_abs_lst (infix "\<approx>abs'_lst" 50) and |
72 alpha_abs_res ("_ \<approx>abs'_res _") |
75 alpha_abs_res (infix "\<approx>abs'_res" 50) |
73 |
76 |
74 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps |
77 lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps |
75 |
78 |
76 lemma alphas_abs_refl: |
79 lemma alphas_abs_refl: |
77 shows "(bs, x) \<approx>abs (bs, x)" |
80 shows "(bs, x) \<approx>abs (bs, x)" |
206 |
209 |
207 lemma abs_eq_iff: |
210 lemma abs_eq_iff: |
208 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
211 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
209 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
212 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
210 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
213 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
211 apply(simp_all) |
214 apply(simp_all add: alphas_abs) |
212 apply(lifting alphas_abs) |
215 apply(lifting alphas_abs) |
213 done |
216 done |
214 |
217 |
215 instantiation abs_gen :: (pt) pt |
218 instantiation abs_gen :: (pt) pt |
216 begin |
219 begin |