src/HOL/Combinatorics/Transposition.thy
author haftmann
Mon, 10 May 2021 19:46:01 +0000
changeset 73664 6e26d06b24b1
parent 73648 1bd3463e30b8
permissions -rw-r--r--
centralized more lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     1
section \<open>Transposition function\<close>
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     2
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     3
theory Transposition
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     4
  imports Main
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     5
begin
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
     6
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
     7
definition transpose :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
     8
  where \<open>transpose a b c = (if c = a then b else if c = b then a else c)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
     9
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    10
lemma transpose_apply_first [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    11
  \<open>transpose a b a = b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    12
  by (simp add: transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    13
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    14
lemma transpose_apply_second [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    15
  \<open>transpose a b b = a\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    16
  by (simp add: transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    17
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    18
lemma transpose_apply_other [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    19
  \<open>transpose a b c = c\<close> if \<open>c \<noteq> a\<close> \<open>c \<noteq> b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    20
  using that by (simp add: transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    21
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    22
lemma transpose_same [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    23
  \<open>transpose a a = id\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    24
  by (simp add: fun_eq_iff transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    25
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    26
lemma transpose_eq_iff:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    27
  \<open>transpose a b c = d \<longleftrightarrow> (c \<noteq> a \<and> c \<noteq> b \<and> d = c) \<or> (c = a \<and> d = b) \<or> (c = b \<and> d = a)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    28
  by (auto simp add: transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    29
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    30
lemma transpose_eq_imp_eq:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    31
  \<open>c = d\<close> if \<open>transpose a b c = transpose a b d\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    32
  using that by (auto simp add: transpose_eq_iff)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    33
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    34
lemma transpose_commute [ac_simps]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    35
  \<open>transpose b a = transpose a b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    36
  by (auto simp add: fun_eq_iff transpose_eq_iff)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    37
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    38
lemma transpose_involutory [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    39
  \<open>transpose a b (transpose a b c) = c\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    40
  by (auto simp add: transpose_eq_iff)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    41
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    42
lemma transpose_comp_involutory [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    43
  \<open>transpose a b \<circ> transpose a b = id\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    44
  by (rule ext) simp
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    45
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    46
lemma transpose_triple:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    47
  \<open>transpose a b (transpose b c (transpose a b d)) = transpose a c d\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    48
  if \<open>a \<noteq> c\<close> and \<open>b \<noteq> c\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    49
  using that by (simp add: transpose_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    50
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    51
lemma transpose_comp_triple:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    52
  \<open>transpose a b \<circ> transpose b c \<circ> transpose a b = transpose a c\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    53
  if \<open>a \<noteq> c\<close> and \<open>b \<noteq> c\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    54
  using that by (simp add: fun_eq_iff transpose_triple)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    55
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    56
lemma transpose_image_eq [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    57
  \<open>transpose a b ` A = A\<close> if \<open>a \<in> A \<longleftrightarrow> b \<in> A\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    58
  using that by (auto simp add: transpose_def [abs_def])
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    59
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    60
lemma inj_on_transpose [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    61
  \<open>inj_on (transpose a b) A\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    62
  by rule (drule transpose_eq_imp_eq)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    63
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    64
lemma inj_transpose:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    65
  \<open>inj (transpose a b)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    66
  by (fact inj_on_transpose)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    67
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    68
lemma surj_transpose:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    69
  \<open>surj (transpose a b)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    70
  by simp
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    71
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    72
lemma bij_betw_transpose_iff [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    73
  \<open>bij_betw (transpose a b) A A\<close> if \<open>a \<in> A \<longleftrightarrow> b \<in> A\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    74
  using that by (auto simp: bij_betw_def)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    75
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    76
lemma bij_transpose [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    77
  \<open>bij (transpose a b)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    78
  by (rule bij_betw_transpose_iff) simp
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    79
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    80
lemma bijection_transpose:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    81
  \<open>bijection (transpose a b)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    82
  by standard (fact bij_transpose)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    83
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    84
lemma inv_transpose_eq [simp]:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    85
  \<open>inv (transpose a b) = transpose a b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    86
  by (rule inv_unique_comp) simp_all
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    87
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    88
lemma transpose_apply_commute:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    89
  \<open>transpose a b (f c) = f (transpose (inv f a) (inv f b) c)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    90
  if \<open>bij f\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    91
proof -
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    92
  from that have \<open>surj f\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    93
    by (rule bij_is_surj)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    94
  with that show ?thesis
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    95
    by (simp add: transpose_def bij_inv_eq_iff surj_f_inv_f)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    96
qed
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    97
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    98
lemma transpose_comp_eq:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
    99
  \<open>transpose a b \<circ> f = f \<circ> transpose (inv f a) (inv f b)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   100
  if \<open>bij f\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   101
  using that by (simp add: fun_eq_iff transpose_apply_commute)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   102
73664
6e26d06b24b1 centralized more lemmas
haftmann
parents: 73648
diff changeset
   103
lemma in_transpose_image_iff:
6e26d06b24b1 centralized more lemmas
haftmann
parents: 73648
diff changeset
   104
  \<open>x \<in> transpose a b ` S \<longleftrightarrow> transpose a b x \<in> S\<close>
6e26d06b24b1 centralized more lemmas
haftmann
parents: 73648
diff changeset
   105
  by (auto intro!: image_eqI)
6e26d06b24b1 centralized more lemmas
haftmann
parents: 73648
diff changeset
   106
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   107
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   108
text \<open>Legacy input alias\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   109
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   110
setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\<open>Fun\<close>))\<close>
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   111
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   112
abbreviation (input) swap :: \<open>'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   113
  where \<open>swap a b f \<equiv> f \<circ> transpose a b\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   114
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   115
lemma swap_def:
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   116
  \<open>Fun.swap a b f = f (a := f b, b:= f a)\<close>
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   117
  by (simp add: fun_eq_iff)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   118
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   119
setup \<open>Context.theory_map (Name_Space.map_naming (Name_Space.parent_path))\<close>
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   120
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   121
lemma swap_apply:
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   122
  "Fun.swap a b f a = f b"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   123
  "Fun.swap a b f b = f a"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   124
  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> Fun.swap a b f c = f c"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   125
  by simp_all
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   126
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   127
lemma swap_self: "Fun.swap a a f = f"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   128
  by simp
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   129
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   130
lemma swap_commute: "Fun.swap a b f = Fun.swap b a f"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   131
  by (simp add: ac_simps)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   132
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   133
lemma swap_nilpotent: "Fun.swap a b (Fun.swap a b f) = f"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   134
  by (simp add: comp_assoc)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   135
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   136
lemma swap_comp_involutory: "Fun.swap a b \<circ> Fun.swap a b = id"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   137
  by (simp add: fun_eq_iff)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   138
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   139
lemma swap_triple:
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   140
  assumes "a \<noteq> c" and "b \<noteq> c"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   141
  shows "Fun.swap a b (Fun.swap b c (Fun.swap a b f)) = Fun.swap a c f"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   142
  using assms transpose_comp_triple [of a c b]
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   143
  by (simp add: comp_assoc)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   144
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   145
lemma comp_swap: "f \<circ> Fun.swap a b g = Fun.swap a b (f \<circ> g)"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   146
  by (simp add: comp_assoc)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   147
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   148
lemma swap_image_eq:
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   149
  assumes "a \<in> A" "b \<in> A"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   150
  shows "Fun.swap a b f ` A = f ` A"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   151
  using assms by (metis image_comp transpose_image_eq)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   152
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   153
lemma inj_on_imp_inj_on_swap: "inj_on f A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> inj_on (Fun.swap a b f) A"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   154
  by (simp add: comp_inj_on)
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   155
  
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   156
lemma inj_on_swap_iff:
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   157
  assumes A: "a \<in> A" "b \<in> A"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   158
  shows "inj_on (Fun.swap a b f) A \<longleftrightarrow> inj_on f A"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   159
  using assms by (metis inj_on_imageI inj_on_imp_inj_on_swap transpose_image_eq)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   160
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   161
lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (Fun.swap a b f)"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   162
  by (meson comp_surj surj_transpose)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   163
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   164
lemma surj_swap_iff: "surj (Fun.swap a b f) \<longleftrightarrow> surj f"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   165
  by (metis fun.set_map surj_transpose)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   166
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   167
lemma bij_betw_swap_iff: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> bij_betw (Fun.swap x y f) A B \<longleftrightarrow> bij_betw f A B"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   168
  by (meson bij_betw_comp_iff bij_betw_transpose_iff)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   169
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   170
lemma bij_swap_iff: "bij (Fun.swap a b f) \<longleftrightarrow> bij f"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   171
  by (simp add: bij_betw_swap_iff)
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   172
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   173
lemma swap_image:
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   174
  \<open>Fun.swap i j f ` A = f ` (A - {i, j}
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   175
    \<union> (if i \<in> A then {j} else {}) \<union> (if j \<in> A then {i} else {}))\<close>
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   176
  by (auto simp add: Fun.swap_def)
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   177
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   178
lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   179
  by simp
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   180
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   181
lemma bij_swap_comp:
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   182
  assumes "bij p"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   183
  shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   184
  using assms by (simp add: transpose_comp_eq) 
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   185
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   186
lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   187
  by (simp add: Fun.swap_def)
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   188
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   189
lemma swap_unfold:
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   190
  \<open>Fun.swap a b p = p \<circ> Fun.swap a b id\<close>
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   191
  by simp
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   192
73648
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   193
lemma swap_id_idempotent: "Fun.swap a b id \<circ> Fun.swap a b id = id"
1bd3463e30b8 more elementary swap
haftmann
parents: 73623
diff changeset
   194
  by simp
73623
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   195
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   196
lemma bij_swap_compose_bij:
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   197
  \<open>bij (Fun.swap a b id \<circ> p)\<close> if \<open>bij p\<close>
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   198
  using that by (rule bij_comp) simp
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   199
5020054b3a16 tuned theory structure
haftmann
parents:
diff changeset
   200
end