equal
deleted
inserted
replaced
465 by (rule ext, simp add: fun_upd_def swap_def) |
465 by (rule ext, simp add: fun_upd_def swap_def) |
466 |
466 |
467 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" |
467 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" |
468 by (rule ext, simp add: fun_upd_def swap_def) |
468 by (rule ext, simp add: fun_upd_def swap_def) |
469 |
469 |
|
470 lemma swap_triple: |
|
471 assumes "a \<noteq> c" and "b \<noteq> c" |
|
472 shows "swap a b (swap b c (swap a b f)) = swap a c f" |
|
473 using assms by (simp add: expand_fun_eq swap_def) |
|
474 |
470 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)" |
475 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)" |
471 by (rule ext, simp add: fun_upd_def swap_def) |
476 by (rule ext, simp add: fun_upd_def swap_def) |
472 |
477 |
473 lemma inj_on_imp_inj_on_swap: |
478 lemma inj_on_imp_inj_on_swap: |
474 "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A" |
479 "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A" |