# HG changeset patch # User haftmann # Date 1397677901 -7200 # Node ID 8e3c848008fa1cb03072898b04e30dcd6fcf815d # Parent ab7c656215f2dceae27532927600f34a356ea40b more simp rules for Fun.swap diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Fun.thy --- a/src/HOL/Fun.thy Wed Apr 16 18:28:13 2014 +0200 +++ b/src/HOL/Fun.thy Wed Apr 16 21:51:41 2014 +0200 @@ -641,17 +641,31 @@ subsection {* @{text swap} *} -definition swap :: "'a \ 'a \ ('a \ 'b) \ ('a \ 'b)" where +definition swap :: "'a \ 'a \ ('a \ 'b) \ ('a \ 'b)" +where "swap a b f = f (a := f b, b:= f a)" -lemma swap_self [simp]: "swap a a f = f" -by (simp add: swap_def) +lemma swap_apply [simp]: + "swap a b f a = f b" + "swap a b f b = f a" + "c \ a \ c \ b \ swap a b f c = f c" + by (simp_all add: swap_def) + +lemma swap_self [simp]: + "swap a a f = f" + by (simp add: swap_def) -lemma swap_commute: "swap a b f = swap b a f" -by (rule ext, simp add: fun_upd_def swap_def) +lemma swap_commute: + "swap a b f = swap b a f" + by (simp add: fun_upd_def swap_def fun_eq_iff) -lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" -by (rule ext, simp add: fun_upd_def swap_def) +lemma swap_nilpotent [simp]: + "swap a b (swap a b f) = f" + by (rule ext, simp add: fun_upd_def swap_def) + +lemma swap_comp_involutory [simp]: + "swap a b \ swap a b = id" + by (rule ext) simp lemma swap_triple: assumes "a \ c" and "b \ c" @@ -659,7 +673,7 @@ using assms by (simp add: fun_eq_iff swap_def) lemma comp_swap: "f \ swap a b g = swap a b (f \ g)" -by (rule ext, simp add: fun_upd_def swap_def) + by (rule ext, simp add: fun_upd_def swap_def) lemma swap_image_eq [simp]: assumes "a \ A" "b \ A" shows "swap a b f ` A = f ` A" @@ -701,6 +715,7 @@ hide_const (open) swap + subsection {* Inversion of injective functions *} definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Apr 16 18:28:13 2014 +0200 +++ b/src/HOL/Hilbert_Choice.thy Wed Apr 16 21:51:41 2014 +0200 @@ -409,6 +409,13 @@ by auto qed +lemma inv_unique_comp: + assumes fg: "f \ g = id" + and gf: "g \ f = id" + shows "inv f = g" + using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) + + subsection {* The Cantor-Bernstein Theorem *} lemma Cantor_Bernstein_aux: diff -r ab7c656215f2 -r 8e3c848008fa src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Wed Apr 16 18:28:13 2014 +0200 +++ b/src/HOL/Library/Permutations.thy Wed Apr 16 21:51:41 2014 +0200 @@ -10,28 +10,16 @@ subsection {* Transpositions *} -lemma swap_id_refl: "Fun.swap a a id = id" - by (fact swap_self) - -lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" - by (fact swap_commute) - -lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" - by (fact swap_commute) - -lemma swap_id_idempotent[simp]: "Fun.swap a b id \ Fun.swap a b id = id" +lemma swap_id_idempotent [simp]: + "Fun.swap a b id \ Fun.swap a b id = id" by (rule ext, auto simp add: Fun.swap_def) -lemma inv_unique_comp: - assumes fg: "f \ g = id" - and gf: "g \ f = id" - shows "inv f = g" - using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) - -lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" +lemma inv_swap_id: + "inv (Fun.swap a b id) = Fun.swap a b id" by (rule inv_unique_comp) simp_all -lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" +lemma swap_id_eq: + "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" by (simp add: Fun.swap_def) @@ -439,7 +427,7 @@ apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) apply (simp_all only: swap_commute) apply (case_tac "a = c \ b = d") - apply (clarsimp simp only: swapid_sym swap_id_idempotent) + apply (clarsimp simp only: swap_commute swap_id_idempotent) apply (case_tac "a = c \ b \ d") apply (rule disjI2) apply (rule_tac x="b" in exI)