more simp rules for Fun.swap
authorhaftmann
Wed Apr 16 21:51:41 2014 +0200 (2014-04-16)
changeset 566088e3c848008fa
parent 56607 ab7c656215f2
child 56609 5ac67041ccf8
more simp rules for Fun.swap
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Permutations.thy
     1.1 --- a/src/HOL/Fun.thy	Wed Apr 16 18:28:13 2014 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Apr 16 21:51:41 2014 +0200
     1.3 @@ -641,17 +641,31 @@
     1.4  
     1.5  subsection {* @{text swap} *}
     1.6  
     1.7 -definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
     1.8 +definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
     1.9 +where
    1.10    "swap a b f = f (a := f b, b:= f a)"
    1.11  
    1.12 -lemma swap_self [simp]: "swap a a f = f"
    1.13 -by (simp add: swap_def)
    1.14 +lemma swap_apply [simp]:
    1.15 +  "swap a b f a = f b"
    1.16 +  "swap a b f b = f a"
    1.17 +  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> swap a b f c = f c"
    1.18 +  by (simp_all add: swap_def)
    1.19 +
    1.20 +lemma swap_self [simp]:
    1.21 +  "swap a a f = f"
    1.22 +  by (simp add: swap_def)
    1.23  
    1.24 -lemma swap_commute: "swap a b f = swap b a f"
    1.25 -by (rule ext, simp add: fun_upd_def swap_def)
    1.26 +lemma swap_commute:
    1.27 +  "swap a b f = swap b a f"
    1.28 +  by (simp add: fun_upd_def swap_def fun_eq_iff)
    1.29  
    1.30 -lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
    1.31 -by (rule ext, simp add: fun_upd_def swap_def)
    1.32 +lemma swap_nilpotent [simp]:
    1.33 +  "swap a b (swap a b f) = f"
    1.34 +  by (rule ext, simp add: fun_upd_def swap_def)
    1.35 +
    1.36 +lemma swap_comp_involutory [simp]:
    1.37 +  "swap a b \<circ> swap a b = id"
    1.38 +  by (rule ext) simp
    1.39  
    1.40  lemma swap_triple:
    1.41    assumes "a \<noteq> c" and "b \<noteq> c"
    1.42 @@ -659,7 +673,7 @@
    1.43    using assms by (simp add: fun_eq_iff swap_def)
    1.44  
    1.45  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    1.46 -by (rule ext, simp add: fun_upd_def swap_def)
    1.47 +  by (rule ext, simp add: fun_upd_def swap_def)
    1.48  
    1.49  lemma swap_image_eq [simp]:
    1.50    assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
    1.51 @@ -701,6 +715,7 @@
    1.52  
    1.53  hide_const (open) swap
    1.54  
    1.55 +
    1.56  subsection {* Inversion of injective functions *}
    1.57  
    1.58  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Apr 16 18:28:13 2014 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Apr 16 21:51:41 2014 +0200
     2.3 @@ -409,6 +409,13 @@
     2.4    by auto
     2.5  qed
     2.6  
     2.7 +lemma inv_unique_comp:
     2.8 +  assumes fg: "f \<circ> g = id"
     2.9 +    and gf: "g \<circ> f = id"
    2.10 +  shows "inv f = g"
    2.11 +  using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
    2.12 +
    2.13 +
    2.14  subsection {* The Cantor-Bernstein Theorem *}
    2.15  
    2.16  lemma Cantor_Bernstein_aux:
     3.1 --- a/src/HOL/Library/Permutations.thy	Wed Apr 16 18:28:13 2014 +0200
     3.2 +++ b/src/HOL/Library/Permutations.thy	Wed Apr 16 21:51:41 2014 +0200
     3.3 @@ -10,28 +10,16 @@
     3.4  
     3.5  subsection {* Transpositions *}
     3.6  
     3.7 -lemma swap_id_refl: "Fun.swap a a id = id"
     3.8 -  by (fact swap_self)
     3.9 -
    3.10 -lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
    3.11 -  by (fact swap_commute)
    3.12 -
    3.13 -lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
    3.14 -  by (fact swap_commute)
    3.15 -
    3.16 -lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
    3.17 +lemma swap_id_idempotent [simp]:
    3.18 +  "Fun.swap a b id \<circ> Fun.swap a b id = id"
    3.19    by (rule ext, auto simp add: Fun.swap_def)
    3.20  
    3.21 -lemma inv_unique_comp:
    3.22 -  assumes fg: "f \<circ> g = id"
    3.23 -    and gf: "g \<circ> f = id"
    3.24 -  shows "inv f = g"
    3.25 -  using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
    3.26 -
    3.27 -lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
    3.28 +lemma inv_swap_id:
    3.29 +  "inv (Fun.swap a b id) = Fun.swap a b id"
    3.30    by (rule inv_unique_comp) simp_all
    3.31  
    3.32 -lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    3.33 +lemma swap_id_eq:
    3.34 +  "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
    3.35    by (simp add: Fun.swap_def)
    3.36  
    3.37  
    3.38 @@ -439,7 +427,7 @@
    3.39      apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
    3.40      apply (simp_all only: swap_commute)
    3.41      apply (case_tac "a = c \<and> b = d")
    3.42 -    apply (clarsimp simp only: swapid_sym swap_id_idempotent)
    3.43 +    apply (clarsimp simp only: swap_commute swap_id_idempotent)
    3.44      apply (case_tac "a = c \<and> b \<noteq> d")
    3.45      apply (rule disjI2)
    3.46      apply (rule_tac x="b" in exI)