1 (* General executable permutations *)

     2 

     3 theory GPerm

     4 imports

     5   "~~/src/HOL/Library/Quotient_Syntax"

     6   "~~/src/HOL/Library/Product_ord"

     7   "~~/src/HOL/Library/List_lexord"

     8 begin

     9 

    10 definition perm_apply where

    11   "perm_apply l e = (case [a\<leftarrow>l . fst a = e] of [] \<Rightarrow> e | x # xa \<Rightarrow> snd x)"

    12 

    13 lemma perm_apply_simps[simp]:

    14   "perm_apply (h # t) e = (if fst h = e then snd h else perm_apply t e)"

    15   "perm_apply [] e = e"

    16   by (auto simp add: perm_apply_def)

    17 

    18 definition valid_perm where

    19   "valid_perm p \<longleftrightarrow> distinct (map fst p) \<and> fst ` set p = snd ` set p"

    20 

    21 lemma valid_perm_zero[simp]:

    22   "valid_perm []"

    23   by (simp add: valid_perm_def)

    24 

    25 lemma length_eq_card_distinct:

    26   "length l = card (set l) \<longleftrightarrow> distinct l"

    27   using card_distinct distinct_card by force

    28 

    29 lemma len_set_eq_distinct:

    30   assumes "length l = length m" "set l = set m"

    31   shows "distinct l = distinct m"

    32   using assms

    33   by (simp add: length_eq_card_distinct[symmetric])

    34 

    35 lemma valid_perm_distinct_snd: "valid_perm a \<Longrightarrow> distinct (map snd a)"

    36   by (metis valid_perm_def image_set length_map len_set_eq_distinct)

    37 

    38 definition

    39   perm_eq :: "('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> bool" (infix "\<approx>" 50)

    40 where

    41   "x \<approx> y \<longleftrightarrow> valid_perm x \<and> valid_perm y \<and> (perm_apply x = perm_apply y)"

    42 

    43 lemma perm_eq_sym[sym]:

    44   "x \<approx> y \<Longrightarrow> y \<approx> x"

    45   by (auto simp add: perm_eq_def)

    46 

    47 lemma perm_eq_equivp:

    48   "part_equivp perm_eq"

    49   by (auto intro!: part_equivpI sympI transpI exI[of _ "[]"] simp add: perm_eq_def)

    50 

    51 quotient_type

    52   'a gperm = "('a \<times> 'a) list" / partial: "perm_eq"

    53   by (rule perm_eq_equivp)

    54 

    55 definition perm_add_raw where

    56   "perm_add_raw p q = map (map_pair id (perm_apply p)) q @ [a\<leftarrow>p. fst a \<notin> fst ` set q]"

    57 

    58 lemma perm_apply_del[simp]:

    59   "e \<noteq> b \<Longrightarrow> perm_apply [a\<leftarrow>l. fst a \<noteq> b] e = perm_apply l e"

    60   "e \<noteq> b \<Longrightarrow> e \<noteq> c \<Longrightarrow> perm_apply [a\<leftarrow>l . fst a \<noteq> b \<and> fst a \<noteq> c] e = perm_apply l e"

    61   by (induct l) auto

    62 

    63 lemma perm_apply_appendl:

    64   "perm_apply a e = perm_apply b e \<Longrightarrow> perm_apply (c @ a) e = perm_apply (c @ b) e"

    65   by (induct c) auto

    66 

    67 lemma perm_apply_filterP:

    68   "b \<noteq> e \<Longrightarrow> perm_apply [a\<leftarrow>l . fst a \<noteq> b \<and> P a] e = perm_apply [a\<leftarrow>l . P a] e"

    69   by (induct l) auto

    70 

    71 lemma perm_add_apply:

    72   shows "perm_apply (perm_add_raw p q) e = perm_apply p (perm_apply q e)"

    73   by (rule sym, induct q)

    74      (auto simp add: perm_add_raw_def perm_apply_filterP intro!: perm_apply_appendl)

    75 

    76 definition swap_pair where

    77   "swap_pair a = (snd a, fst a)"

    78 

    79 definition uminus_perm_raw where

    80   [simp]: "uminus_perm_raw = map swap_pair"

    81 

    82 lemma map_fst_minus_perm[simp]:

    83   "map fst (uminus_perm_raw x) = map snd x"

    84   "map snd (uminus_perm_raw x) = map fst x"

    85   by (induct x) (auto simp add: swap_pair_def)

    86 

    87 lemma fst_snd_set_minus_perm[simp]:

    88   "fst ` set (uminus_perm_raw x) = snd ` set x"

    89   "snd ` set (uminus_perm_raw x) = fst ` set x"

    90   by (induct x) (auto simp add: swap_pair_def)

    91 

    92 lemma fst_snd_swap_pair[simp]:

    93   "fst (swap_pair x) = snd x"

    94   "snd (swap_pair x) = fst x"

    95   by (auto simp add: swap_pair_def)

    96 

    97 lemma fst_snd_swap_pair_set[simp]:

    98   "fst ` swap_pair ` set l = snd ` set l"

    99   "snd ` swap_pair ` set l = fst ` set l"

   100   by (induct l) (auto simp add: swap_pair_def)

   101 

   102 lemma valid_perm_minus[simp]:

   103   assumes "valid_perm x"

   104   shows "valid_perm (map swap_pair x)"

   105   using assms unfolding valid_perm_def

   106   by (simp add: valid_perm_distinct_snd[OF assms] o_def)

   107 

   108 lemma swap_pair_id[simp]:

   109   "swap_pair (swap_pair x) = x"

   110   unfolding swap_pair_def by simp

   111 

   112 lemma perm_apply_minus_minus[simp]:

   113   "perm_apply (uminus_perm_raw (uminus_perm_raw x)) = perm_apply x"

   114   by (simp add: o_def)

   115 

   116 lemma filter_eq_nil:

   117   "[a\<leftarrow>a. fst a = e] = [] \<longleftrightarrow> e \<notin> fst ` set a"

   118   "[a\<leftarrow>a. snd a = e] = [] \<longleftrightarrow> e \<notin> snd ` set a"

   119   by (induct a) auto

   120 

   121 lemma filter_rev_eq_nil: "[a\<leftarrow>map swap_pair a. fst a = e] = [] \<longleftrightarrow> e \<notin> snd ` set a"

   122   by (induct a) (auto simp add: swap_pair_def)

   123 

   124 lemma filter_fst_eq:

   125   "[a\<leftarrow>a . fst a = e] = (l, r) # list \<Longrightarrow> l = e"

   126   "[a\<leftarrow>a . snd a = e] = (l, r) # list \<Longrightarrow> r = e"

   127   by (drule filter_eq_ConsD, auto)+

   128 

   129 lemma filter_map_swap_pair:

   130   "[a\<leftarrow>map swap_pair a. fst a = e] = map swap_pair [a\<leftarrow>a. snd a = e]"

   131   by (induct a) auto

   132 

   133 lemma forget_tl:

   134   "[a\<leftarrow>l . P a] = a # b \<Longrightarrow> a \<in> set l"

   135   by (metis Cons_eq_filter_iff in_set_conv_decomp)

   136 

   137 lemma valid_perm_lookup_fst_eq_snd:

   138   "[a\<leftarrow>l . fst a = f] = (f, s) # l1 \<Longrightarrow> [a\<leftarrow>l . snd a = s] = (f2, s) # l2 \<Longrightarrow> valid_perm l \<Longrightarrow> f2 = f"

   139   apply (drule forget_tl valid_perm_distinct_snd)+

   140   apply (case_tac "f2 = f")

   141   apply (auto simp add: in_set_conv_nth swap_pair_def)

   142   apply (case_tac "i = ia")

   143   apply auto

   144   by (metis length_map nth_eq_iff_index_eq nth_map snd_conv)

   145 

   146 lemma valid_perm_add_minus: "valid_perm a \<Longrightarrow> perm_apply (map swap_pair a) (perm_apply a e) = e"

   147   apply (auto simp add: filter_map_swap_pair filter_eq_nil filter_rev_eq_nil perm_apply_def split: list.split)

   148   apply (metis filter_eq_nil(2) neq_Nil_conv valid_perm_def)

   149   apply (metis hd.simps hd_in_set image_eqI list.simps(2) member_project project_set snd_conv)

   150   apply (frule filter_fst_eq(1))

   151   apply (frule filter_fst_eq(2))

   152   apply (auto simp add: swap_pair_def)

   153   apply (erule valid_perm_lookup_fst_eq_snd)

   154   apply assumption+

   155   done

   156 

   157 lemma perm_apply_minus: "valid_perm x \<Longrightarrow> perm_apply (map swap_pair x) a = b \<longleftrightarrow> perm_apply x b = a"

   158   using valid_perm_add_minus[symmetric] valid_perm_minus

   159   by (metis uminus_perm_raw_def)

   160 

   161 lemma uminus_perm_raw_rsp[simp]:

   162   "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"

   163   by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)

   164 

   165 lemma [quot_respect]:

   166   "(op \<approx> ===> op \<approx>) uminus_perm_raw uminus_perm_raw"

   167   by (auto intro!: fun_relI simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)

   168 

   169 lemma fst_snd_map_pair[simp]:

   170   "fst ` map_pair f g ` set l = f ` fst ` set l"

   171   "snd ` map_pair f g ` set l = g ` snd ` set l"

   172   by (induct l) auto

   173 

   174 lemma fst_diff[simp]:

   175   shows "fst ` {xa \<in> set x. fst xa \<notin> fst ` set y} = fst ` set x - fst ` set y"

   176   by auto

   177 

   178 lemma pair_perm_apply:

   179   "distinct (map fst x) \<Longrightarrow> (a, b) \<in> set x \<Longrightarrow> perm_apply x a = b"

   180   by (induct x) (auto, metis fst_conv image_eqI)

   181 

   182 lemma valid_perm_apply:

   183   "valid_perm x \<Longrightarrow> (a, b) \<in> set x \<Longrightarrow> perm_apply x a = b"

   184   unfolding valid_perm_def using pair_perm_apply by auto

   185 

   186 lemma in_perm_apply:

   187   "valid_perm x \<Longrightarrow> (a, b) \<in> set x \<Longrightarrow> a \<in> c \<Longrightarrow> b \<in> perm_apply x ` c"

   188   by (metis imageI valid_perm_apply)

   189 

   190 lemma snd_set_not_in_perm_apply[simp]:

   191   assumes "valid_perm x"

   192   shows "snd ` {xa \<in> set x. fst xa \<notin> fst ` set y} = perm_apply x ` (fst ` set x - fst ` set y)"

   193 proof auto

   194   fix a b

   195   assume a: "(a, b) \<in> set x" " a \<notin> fst ` set y"

   196   then have "a \<in> fst ` set x - fst ` set y"

   197     by simp (metis fst_conv image_eqI)

   198   with a show "b \<in> perm_apply x ` (fst ` set x - fst ` set y)"

   199     by (simp add: in_perm_apply assms)

   200 next

   201   fix a b

   202   assume a: "a \<notin> fst ` set y" "(a, b) \<in> set x"

   203   then have "perm_apply x a = b"

   204     by (simp add: valid_perm_apply assms)

   205   with a show "perm_apply x a \<in> snd ` {xa \<in> set x. fst xa \<notin> fst ` set y}"

   206     by (metis (lifting) CollectI fst_conv image_eqI snd_conv)

   207 qed

   208 

   209 lemma perm_apply_set:

   210   "valid_perm x \<Longrightarrow> perm_apply x ` fst ` set x = fst ` set x"

   211   by (auto simp add: valid_perm_def)

   212      (metis (hide_lams, no_types) image_iff pair_perm_apply snd_eqD surjective_pairing)+

   213 

   214 lemma perm_apply_outset: "a \<notin> fst ` set x \<Longrightarrow> perm_apply x a = a"

   215   by (induct x) auto

   216 

   217 lemma perm_apply_subset: "valid_perm x \<Longrightarrow> fst ` set x \<subseteq> s \<Longrightarrow> perm_apply x ` s = s"

   218   apply auto

   219   apply (case_tac [!] "xa \<in> fst ` set x")

   220   apply (metis imageI perm_apply_set subsetD)

   221   apply (metis perm_apply_outset)

   222   apply (metis image_mono perm_apply_set subsetD)

   223   by (metis imageI perm_apply_outset)

   224 

   225 lemma valid_perm_add_raw[simp]:

   226   assumes "valid_perm x" "valid_perm y"

   227   shows "valid_perm (perm_add_raw x y)"

   228   using assms

   229   apply (simp (no_asm) add: valid_perm_def)

   230   apply (intro conjI)

   231   apply (auto simp add: perm_add_raw_def valid_perm_def fst_def[symmetric])[1]

   232   apply (simp add: distinct_map inj_on_def)

   233   apply (metis imageI snd_conv)

   234   apply (simp add: perm_add_raw_def image_Un)

   235   apply (simp add: image_Un[symmetric])

   236   apply (auto simp add: perm_apply_subset valid_perm_def)

   237   done

   238 

   239 lemma perm_add_raw_rsp[simp]:

   240   "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"

   241   by (simp add: fun_eq_iff perm_add_apply perm_eq_def)

   242 

   243 lemma [quot_respect]:

   244   "(op \<approx> ===> op \<approx> ===> op \<approx>) perm_add_raw perm_add_raw"

   245   by (auto intro!: fun_relI simp add: perm_add_raw_rsp)

   246 

   247 lemma [simp]:

   248   "a \<approx> a \<longleftrightarrow> valid_perm a"

   249   by (simp_all add: perm_eq_def)

   250 

   251 lemma [quot_respect]: "[] \<approx> []"

   252   by auto

   253 

   254 lemmas [simp] = in_respects

   255 

   256 instantiation gperm :: (type) group_add

   257 begin

   258 

   259 quotient_definition "0 :: 'a gperm" is "[] :: ('a \<times> 'a) list"

   260 

   261 quotient_definition "uminus :: 'a gperm \<Rightarrow> 'a gperm" is

   262   "uminus_perm_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"

   263 

   264 quotient_definition "(op +) :: 'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is

   265   "perm_add_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"

   266 

   267 definition

   268   minus_perm_def: "(p1::'a gperm) - p2 = p1 + - p2"

   269 

   270 instance

   271   apply default

   272   unfolding minus_perm_def

   273   by (partiality_descending, simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+

   274 

   275 end

   276 

   277 definition "mk_perm_raw l = (if valid_perm l then l else [])"

   278 

   279 quotient_definition "mk_perm :: ('a \<times> 'a) list \<Rightarrow> 'a gperm"

   280   is "mk_perm_raw"

   281 

   282 definition "dest_perm_raw p = sort [x\<leftarrow>p. fst x \<noteq> snd x]"

   283 

   284 quotient_definition "dest_perm :: ('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"

   285   is "dest_perm_raw"

   286 

   287 lemma [quot_respect]: "(op = ===> op \<approx>) mk_perm_raw mk_perm_raw"

   288   by (auto intro!: fun_relI simp add: mk_perm_raw_def)

   289 

   290 lemma distinct_fst_distinct[simp]: "distinct (map fst x) \<Longrightarrow> distinct x"

   291   by (induct x) auto

   292 

   293 lemma perm_apply_in_set:

   294   "a \<noteq> b \<Longrightarrow> perm_apply y a = b \<Longrightarrow> (a, b) \<in> set y"

   295   by (induct y) (auto split: if_splits)

   296 

   297 lemma perm_eq_not_eq_same:

   298   "x \<approx> y \<Longrightarrow> {xa \<in> set x. fst xa \<noteq> snd xa} = {x \<in> set y. fst x \<noteq> snd x}"

   299   unfolding perm_eq_def set_eq_iff

   300   apply auto

   301   apply (subgoal_tac "perm_apply x a = b")

   302   apply (simp add: perm_apply_in_set)

   303   apply (erule valid_perm_apply)

   304   apply simp

   305   apply (subgoal_tac "perm_apply y a = b")

   306   apply (simp add: perm_apply_in_set)

   307   apply (erule valid_perm_apply)

   308   apply simp

   309   done

   310 

   311 lemma [simp]: "distinct (map fst (sort x)) = distinct (map fst x)"

   312   by (rule len_set_eq_distinct) simp_all

   313 

   314 lemma valid_perm_sort[simp]:

   315   "valid_perm x \<Longrightarrow> valid_perm (sort x)"

   316   unfolding valid_perm_def by simp

   317 

   318 lemma same_not_in_dpr:

   319   "valid_perm x \<Longrightarrow> (b, b) \<in> set x \<Longrightarrow> b \<notin> fst ` set (dest_perm_raw x)"

   320   unfolding dest_perm_raw_def valid_perm_def

   321   by auto (metis pair_perm_apply)

   322 

   323 lemma in_set_in_dpr:

   324   "valid_perm x \<Longrightarrow> a \<noteq> b \<Longrightarrow> (a, b) \<in> set x \<longleftrightarrow> (a, b) \<in> set (dest_perm_raw x)"

   325   unfolding dest_perm_raw_def valid_perm_def

   326   by simp

   327 

   328 lemma in_set_in_dpr2:

   329   "a \<noteq> b \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) \<Longrightarrow> valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (a, b) \<in> set x \<longleftrightarrow> (a, b) \<in> set y"

   330   using in_set_in_dpr by metis

   331 

   332 lemma in_set_in_dpr3:

   333   "(dest_perm_raw x = dest_perm_raw y) \<Longrightarrow> valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> perm_apply x a = perm_apply y a"

   334   by (metis in_set_in_dpr2 pair_perm_apply perm_apply_in_set valid_perm_def)

   335 

   336 lemma dest_perm_raw_eq[simp]:

   337   "valid_perm x \<Longrightarrow> valid_perm y \<Longrightarrow> (dest_perm_raw x = dest_perm_raw y) = (x \<approx> y)"

   338   apply (auto simp add: perm_eq_def)

   339   apply (metis in_set_in_dpr3 fun_eq_iff)

   340   unfolding dest_perm_raw_def

   341   by (rule sorted_distinct_set_unique)

   342      (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified])

   343 

   344 lemma [quot_respect]:

   345   "(op \<approx> ===> op =) dest_perm_raw dest_perm_raw"

   346   by (auto intro!: fun_relI simp add: perm_eq_def)

   347 

   348 lemma dest_perm_mk_perm[simp]:

   349   "dest_perm (mk_perm xs) = sort [x\<leftarrow>mk_perm_raw xs. fst x \<noteq> snd x]"

   350   by (partiality_descending)

   351      (simp add: dest_perm_raw_def)

   352 

   353 lemma valid_perm_filter_id[simp]:

   354   "valid_perm p \<Longrightarrow> valid_perm [x\<leftarrow>p. fst x \<noteq> snd x]"

   355 proof (simp (no_asm) add: valid_perm_def, intro conjI)

   356   show "valid_perm p \<Longrightarrow> distinct (map fst [x\<Colon>'a \<times> 'a\<leftarrow>p . fst x \<noteq> snd x])"

   357     by (auto simp add: distinct_map inj_on_def valid_perm_def)

   358   assume a: "valid_perm p"

   359   then show "fst ` {x\<Colon>'a \<times> 'a \<in> set p. fst x \<noteq> snd x} = snd ` {x\<Colon>'a \<times> 'a \<in> set p. fst x \<noteq> snd x}"

   360     apply -

   361     apply (frule valid_perm_distinct_snd)

   362     apply (simp add: valid_perm_def)

   363     apply auto

   364     apply (subgoal_tac "a \<in> snd ` set p")

   365     apply auto

   366     apply (subgoal_tac "(aa, ba) \<in> {x \<in> set p. fst x \<noteq> snd x}")

   367     apply (metis (lifting) image_eqI snd_conv)

   368     apply (metis (lifting, mono_tags) fst_conv mem_Collect_eq snd_conv pair_perm_apply)

   369     apply (metis fst_conv imageI)

   370     apply (drule sym)

   371     apply (subgoal_tac "b \<in> fst ` set p")

   372     apply auto

   373     apply (subgoal_tac "(aa, ba) \<in> {x \<in> set p. fst x \<noteq> snd x}")

   374     apply (metis (lifting) image_eqI fst_conv)

   375     apply simp

   376     apply (metis valid_perm_add_minus valid_perm_apply valid_perm_def)

   377     apply (metis snd_conv imageI)

   378     done

   379 qed

   380 

   381 lemma valid_perm_dest_pair_raw[simp]:

   382   assumes "valid_perm x"

   383   shows "valid_perm (dest_perm_raw x)"

   384   using valid_perm_filter_id valid_perm_sort assms

   385   unfolding dest_perm_raw_def

   386   by simp

   387 

   388 lemma dest_perm_raw_repeat[simp]:

   389   "dest_perm_raw (dest_perm_raw p) = dest_perm_raw p"

   390   unfolding dest_perm_raw_def

   391   by simp (rule sorted_sort_id[OF sorted_sort])

   392 

   393 lemma valid_dest_perm_raw_eq[simp]:

   394   "valid_perm p \<Longrightarrow> dest_perm_raw p \<approx> p"

   395   "valid_perm p \<Longrightarrow> p \<approx> dest_perm_raw p"

   396   by (simp_all add: dest_perm_raw_eq[symmetric])

   397 

   398 lemma mk_perm_dest_perm[code abstype]:

   399   "mk_perm (dest_perm p) = p"

   400   by (partiality_descending)

   401      (auto simp add: mk_perm_raw_def)

   402 

   403 instantiation gperm :: (linorder) equal begin

   404 

   405 definition equal_gperm_def: "equal_gperm a b \<longleftrightarrow> dest_perm a = dest_perm b"

   406 

   407 instance

   408   apply default

   409   unfolding equal_gperm_def

   410   by partiality_descending simp

   411 

   412 end

   413 

   414 lemma [code abstract]:

   415   "dest_perm 0 = []"

   416   by (partiality_descending) (simp add: dest_perm_raw_def)

   417 

   418 lemma [code abstract]:

   419   "dest_perm (-a) = dest_perm_raw (uminus_perm_raw (dest_perm a))"

   420   by (partiality_descending) (auto)

   421 

   422 lemma [code abstract]:

   423   "dest_perm (a + b) = dest_perm_raw (perm_add_raw (dest_perm a) (dest_perm b))"

   424   by (partiality_descending) auto

   425 

   426 quotient_definition "gpermute :: 'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"

   427 is perm_apply

   428 

   429 lemma [quot_respect]: "(op \<approx> ===> op =) perm_apply perm_apply"

   430   by (auto intro!: fun_relI simp add: perm_eq_def)

   431 

   432 lemma gpermute_zero[simp]:

   433   "gpermute 0 x = x"

   434   by descending simp

   435 

   436 lemma gpermute_add[simp]:

   437   "gpermute (p + q) x = gpermute p (gpermute q x)"

   438   by descending (simp add: perm_add_apply)

   439 

   440 definition [simp]:"swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"

   441 

   442 lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) swap_raw swap_raw"

   443   by (auto intro!: fun_relI simp add: valid_perm_def)

   444 

   445 quotient_definition "gswap :: 'a \<Rightarrow> 'a \<Rightarrow> 'a gperm"

   446 is swap_raw

   447 

   448 lemma [code abstract]:

   449   "dest_perm (gswap a b) = (if (a, b) \<le> (b, a) then swap_raw a b else swap_raw b a)"

   450   by (partiality_descending) (auto simp add: dest_perm_raw_def)

   451 

   452 lemma swap_self [simp]:

   453   "gswap a a = 0"

   454   by (partiality_descending, auto)

   455 

   456 lemma [simp]: "a \<noteq> b \<Longrightarrow> valid_perm [(a, b), (b, a)]"

   457   unfolding valid_perm_def by auto

   458 

   459 lemma swap_cancel [simp]:

   460   "gswap a b + gswap a b = 0"

   461   "gswap a b + gswap b a = 0"

   462   by (descending, auto simp add: perm_eq_def perm_add_apply)+

   463 

   464 lemma minus_swap [simp]:

   465   "- gswap a b = gswap a b"

   466   by (partiality_descending, auto simp add: perm_eq_def)

   467 

   468 lemma swap_commute:

   469   "gswap a b = gswap b a"

   470   by (partiality_descending, auto simp add: perm_eq_def)

   471 

   472 lemma swap_triple:

   473   assumes "a \<noteq> b" "c \<noteq> b"

   474   shows "gswap a c + gswap b c + gswap a c = gswap a b"

   475   using assms

   476   by descending (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)

   477 

   478 lemma gpermute_gswap[simp]:

   479   "b \<noteq> a \<Longrightarrow> gpermute (gswap a b) b = a"

   480   "a \<noteq> b \<Longrightarrow> gpermute (gswap a b) a = b"

   481   "c \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> gpermute (gswap a b) c = c"

   482   by (descending, auto)+

   483 

   484 lemma gperm_eq:

   485   "(p = q) = (\<forall>a. gpermute p a = gpermute q a)"

   486   by (partiality_descending) (auto simp add: perm_eq_def)

   487 

   488 lemma finite_gpermute_neq:

   489   "finite {a. gpermute p a \<noteq> a}"

   490   apply descending

   491   apply (rule_tac B="fst ` set p" in finite_subset)

   492   apply auto

   493   by (metis perm_apply_outset)

   494 

   495 end