equal
deleted
inserted
replaced
59 alpha_gen[simp del]: |
59 alpha_gen[simp del]: |
60 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
60 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
61 |
61 |
62 notation |
62 notation |
63 alpha_gen ("_ \<approx>gen _ _ _ _") |
63 alpha_gen ("_ \<approx>gen _ _ _ _") |
|
64 |
|
65 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
|
66 by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps) |
64 |
67 |
65 lemma alpha_gen_refl: |
68 lemma alpha_gen_refl: |
66 assumes a: "R x x" |
69 assumes a: "R x x" |
67 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
70 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
68 using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm) |
71 using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm) |