equal
deleted
inserted
replaced
13 |
13 |
14 (* ------------------------------------------------------------------------- *) |
14 (* ------------------------------------------------------------------------- *) |
15 (* Transpositions. *) |
15 (* Transpositions. *) |
16 (* ------------------------------------------------------------------------- *) |
16 (* ------------------------------------------------------------------------- *) |
17 |
17 |
18 declare swap_self[simp] |
|
19 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" |
18 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" |
20 by (auto simp add: expand_fun_eq swap_def fun_upd_def) |
19 by (auto simp add: expand_fun_eq swap_def fun_upd_def) |
21 lemma swap_id_refl: "Fun.swap a a id = id" by simp |
20 lemma swap_id_refl: "Fun.swap a a id = id" by simp |
22 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" |
21 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" |
23 by (rule ext, simp add: swap_def) |
22 by (rule ext, simp add: swap_def) |