1 theory Abs

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product"

     3 begin

     4 

     5 (* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *)

     6 lemma ball_image: 

     7   shows "(\<forall>x \<in> p \<bullet> S. P x) = (\<forall>x \<in> S. P (p \<bullet> x))"

     8 apply(auto)

     9 apply(drule_tac x="p \<bullet> x" in bspec)

    10 apply(simp add: mem_permute_iff)

    11 apply(simp)

    12 apply(drule_tac x="(- p) \<bullet> x" in bspec)

    13 apply(rule_tac p1="p" in mem_permute_iff[THEN iffD1])

    14 apply(simp)

    15 apply(simp)

    16 done

    17 

    18 lemma fresh_star_plus:

    19   fixes p q::perm

    20   shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"

    21   unfolding fresh_star_def

    22   by (simp add: fresh_plus_perm)

    23 

    24 lemma fresh_star_permute_iff:

    25   shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"

    26 apply(simp add: fresh_star_def)

    27 apply(simp add: ball_image)

    28 apply(simp add: fresh_permute_iff)

    29 done

    30 

    31 fun

    32   alpha_gen 

    33 where

    34   alpha_gen[simp del]:

    35   "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y"

    36 

    37 notation

    38   alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100)

    39 

    40 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"

    41   by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)

    42 

    43 lemma alpha_gen_refl:

    44   assumes a: "R x x"

    45   shows "(bs, x) \<approx>gen R f 0 (bs, x)"

    46   using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm)

    47 

    48 lemma alpha_gen_sym:

    49   assumes a: "(bs, x) \<approx>gen R f p (cs, y)"

    50   and     b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"

    51   shows "(cs, y) \<approx>gen R f (- p) (bs, x)"

    52   using a b by (simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm)

    53 

    54 lemma alpha_gen_trans:

    55   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"

    56   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"

    57   and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"

    58   shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"

    59   using a b c using supp_plus_perm

    60   apply(simp add: alpha_gen fresh_star_def fresh_def)

    61   apply(blast)

    62   done

    63 

    64 lemma alpha_gen_eqvt:

    65   assumes a: "(bs, x) \<approx>gen R f q (cs, y)"

    66   and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"

    67   and     c: "p \<bullet> (f x) = f (p \<bullet> x)"

    68   and     d: "p \<bullet> (f y) = f (p \<bullet> y)"

    69   shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"

    70   using a b

    71   apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])

    72   apply(simp add: permute_eqvt[symmetric])

    73   apply(simp add: fresh_star_permute_iff)

    74   apply(clarsimp)

    75   done

    76 

    77 lemma alpha_gen_compose_sym:

    78   fixes pi

    79   assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"

    80   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"

    81   shows "(ab, s) \<approx>gen R f (- pi) (aa, t)"

    82   using b apply -

    83   apply(simp add: alpha_gen.simps)

    84   apply(erule conjE)+

    85   apply(rule conjI)

    86   apply(simp add: fresh_star_def fresh_minus_perm)

    87   apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")

    88   apply simp

    89   apply(rule a)

    90   apply assumption

    91   done

    92 

    93 lemma alpha_gen_compose_trans:

    94   fixes pi pia

    95   assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)"

    96   and c: "(ab, ta) \<approx>gen R f pia (ac, sa)"

    97   and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"

    98   shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)"

    99   using b c apply -

   100   apply(simp add: alpha_gen.simps)

   101   apply(erule conjE)+

   102   apply(simp add: fresh_star_plus)

   103   apply(drule_tac x="- pia \<bullet> sa" in spec)

   104   apply(drule mp)

   105   apply(rotate_tac 4)

   106   apply(drule_tac pi="- pia" in a)

   107   apply(simp)

   108   apply(rotate_tac 6)

   109   apply(drule_tac pi="pia" in a)

   110   apply(simp)

   111   done

   112 

   113 lemma alpha_gen_compose_eqvt:

   114   fixes  pia

   115   assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"

   116   and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"

   117   and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"

   118   shows  "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)"

   119   using b

   120   apply -

   121   apply(simp add: alpha_gen.simps)

   122   apply(erule conjE)+

   123   apply(rule conjI)

   124   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

   125   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])

   126   apply(rule conjI)

   127   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

   128   apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric])

   129   apply(subst permute_eqvt[symmetric])

   130   apply(simp)

   131   done

   132 

   133 fun

   134   alpha_abs 

   135 where

   136   "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"

   137 

   138 notation

   139   alpha_abs ("_ \<approx>abs _")

   140 

   141 lemma alpha_abs_swap:

   142   assumes a1: "a \<notin> (supp x) - bs"

   143   and     a2: "b \<notin> (supp x) - bs"

   144   shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"

   145   apply(simp)

   146   apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)

   147   apply(simp add: alpha_gen)

   148   apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])

   149   apply(simp add: swap_set_not_in[OF a1 a2])

   150   apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")

   151   using a1 a2

   152   apply(simp add: fresh_star_def fresh_def)

   153   apply(blast)

   154   apply(simp add: supp_swap)

   155   done

   156 

   157 fun

   158   supp_abs_fun

   159 where

   160   "supp_abs_fun (bs, x) = (supp x) - bs"

   161 

   162 lemma supp_abs_fun_lemma:

   163   assumes a: "x \<approx>abs y" 

   164   shows "supp_abs_fun x = supp_abs_fun y"

   165   using a

   166   apply(induct rule: alpha_abs.induct)

   167   apply(simp add: alpha_gen)

   168   done

   169   

   170 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs"

   171   apply(rule equivpI)

   172   unfolding reflp_def symp_def transp_def

   173   apply(simp_all)

   174   (* refl *)

   175   apply(clarify)

   176   apply(rule exI)

   177   apply(rule alpha_gen_refl)

   178   apply(simp)

   179   (* symm *)

   180   apply(clarify)

   181   apply(rule exI)

   182   apply(rule alpha_gen_sym)

   183   apply(assumption)

   184   apply(clarsimp)

   185   (* trans *)

   186   apply(clarify)

   187   apply(rule exI)

   188   apply(rule alpha_gen_trans)

   189   apply(assumption)

   190   apply(assumption)

   191   apply(simp)

   192   done

   193 

   194 quotient_definition

   195   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"

   196 is

   197   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"

   198 

   199 lemma [quot_respect]:

   200   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"

   201   apply(clarsimp)

   202   apply(rule exI)

   203   apply(rule alpha_gen_refl)

   204   apply(simp)

   205   done

   206 

   207 lemma [quot_respect]:

   208   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"

   209   apply(clarsimp)

   210   apply(rule exI)

   211   apply(rule alpha_gen_eqvt)

   212   apply(assumption)

   213   apply(simp_all add: supp_eqvt)

   214   done

   215 

   216 lemma [quot_respect]:

   217   shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun"

   218   apply(simp add: supp_abs_fun_lemma)

   219   done

   220 

   221 lemma abs_induct:

   222   "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"

   223   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])

   224   done

   225 

   226 (* TEST case *)

   227 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]

   228 thm abs_induct abs_induct2

   229 

   230 instantiation abs :: (pt) pt

   231 begin

   232 

   233 quotient_definition

   234   "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"

   235 is

   236   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"

   237 

   238 lemma permute_ABS [simp]:

   239   fixes x::"'a::pt"  (* ??? has to be 'a \<dots> 'b does not work *)

   240   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"

   241   by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])

   242 

   243 instance

   244   apply(default)

   245   apply(induct_tac [!] x rule: abs_induct)

   246   apply(simp_all)

   247   done

   248 

   249 end

   250 

   251 quotient_definition

   252   "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"

   253 is

   254   "supp_abs_fun"

   255 

   256 lemma supp_Abs_fun_simp:

   257   shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"

   258   by (lifting supp_abs_fun.simps(1))

   259 

   260 lemma supp_Abs_fun_eqvt [eqvt]:

   261   shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"

   262   apply(induct_tac x rule: abs_induct)

   263   apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)

   264   done

   265 

   266 lemma supp_Abs_fun_fresh:

   267   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"

   268   apply(rule fresh_fun_eqvt_app)

   269   apply(simp add: eqvts_raw)

   270   apply(simp)

   271   done

   272 

   273 lemma Abs_swap:

   274   assumes a1: "a \<notin> (supp x) - bs"

   275   and     a2: "b \<notin> (supp x) - bs"

   276   shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"

   277   using a1 a2 by (lifting alpha_abs_swap)

   278 

   279 lemma Abs_supports:

   280   shows "((supp x) - as) supports (Abs as x)"

   281   unfolding supports_def

   282   apply(clarify)

   283   apply(simp (no_asm))

   284   apply(subst Abs_swap[symmetric])

   285   apply(simp_all)

   286   done

   287 

   288 lemma supp_Abs_subset1:

   289   fixes x::"'a::fs"

   290   shows "(supp x) - as \<subseteq> supp (Abs as x)"

   291   apply(simp add: supp_conv_fresh)

   292   apply(auto)

   293   apply(drule_tac supp_Abs_fun_fresh)

   294   apply(simp only: supp_Abs_fun_simp)

   295   apply(simp add: fresh_def)

   296   apply(simp add: supp_finite_atom_set finite_supp)

   297   done

   298 

   299 lemma supp_Abs_subset2:

   300   fixes x::"'a::fs"

   301   shows "supp (Abs as x) \<subseteq> (supp x) - as"

   302   apply(rule supp_is_subset)

   303   apply(rule Abs_supports)

   304   apply(simp add: finite_supp)

   305   done

   306 

   307 lemma supp_Abs:

   308   fixes x::"'a::fs"

   309   shows "supp (Abs as x) = (supp x) - as"

   310   apply(rule_tac subset_antisym)

   311   apply(rule supp_Abs_subset2)

   312   apply(rule supp_Abs_subset1)

   313   done

   314 

   315 instance abs :: (fs) fs

   316   apply(default)

   317   apply(induct_tac x rule: abs_induct)

   318   apply(simp add: supp_Abs)

   319   apply(simp add: finite_supp)

   320   done

   321 

   322 lemma Abs_fresh_iff:

   323   fixes x::"'a::fs"

   324   shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"

   325   apply(simp add: fresh_def)

   326   apply(simp add: supp_Abs)

   327   apply(auto)

   328   done

   329 

   330 lemma Abs_eq_iff:

   331   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"

   332   by (lifting alpha_abs.simps(1))

   333 

   334 

   335 

   336 (* 

   337   below is a construction site for showing that in the

   338   single-binder case, the old and new alpha equivalence 

   339   coincide

   340 *)

   341 

   342 fun

   343   alpha1

   344 where

   345   "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   346 

   347 notation 

   348   alpha1 ("_ \<approx>abs1 _")

   349 

   350 fun

   351   alpha2

   352 where

   353   "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"

   354 

   355 notation 

   356   alpha2 ("_ \<approx>abs2 _")

   357 

   358 

   359 

   360 lemma qq:

   361   fixes S::"atom set"

   362   assumes a: "supp p \<inter> S = {}"

   363   shows "p \<bullet> S = S"

   364 using a

   365 apply(simp add: supp_perm permute_set_eq)

   366 apply(auto)

   367 apply(simp only: disjoint_iff_not_equal)

   368 apply(simp)

   369 apply (metis permute_atom_def_raw)

   370 apply(rule_tac x="(- p) \<bullet> x" in exI)

   371 apply(simp)

   372 apply(simp only: disjoint_iff_not_equal)

   373 apply(simp)

   374 apply(metis permute_minus_cancel)

   375 done

   376 

   377 lemma

   378   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"

   379   shows "({a}, x) \<approx>abs ({b}, y)"

   380 using a

   381 apply(simp)

   382 apply(erule disjE)

   383 apply(simp)

   384 apply(rule exI)

   385 apply(rule alpha_gen_refl)

   386 apply(simp)

   387 apply(rule_tac x="(a \<rightleftharpoons> b)" in  exI)

   388 apply(simp add: alpha_gen)

   389 apply(simp add: fresh_def)

   390 apply(rule conjI)

   391 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])

   392 apply(rule trans)

   393 apply(simp add: Diff_eqvt supp_eqvt)

   394 apply(subst swap_set_not_in)

   395 back

   396 apply(simp)

   397 apply(simp)

   398 apply(simp add: permute_set_eq)

   399 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])

   400 apply(simp add: permute_self)

   401 apply(simp add: Diff_eqvt supp_eqvt)

   402 apply(simp add: permute_set_eq)

   403 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")

   404 apply(simp add: fresh_star_def fresh_def)

   405 apply(blast)

   406 apply(simp add: supp_swap)

   407 done

   408 

   409 lemma perm_zero:

   410   assumes a: "\<forall>x::atom. p \<bullet> x = x"

   411   shows "p = 0"

   412 using a

   413 by (simp add: expand_perm_eq)

   414 

   415 fun

   416   add_perm 

   417 where

   418   "add_perm [] = 0"

   419 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"

   420 

   421 fun

   422   elem_perm

   423 where

   424   "elem_perm [] = {}"

   425 | "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"

   426 

   427 

   428 lemma add_perm_apend:

   429   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"

   430 apply(induct xs arbitrary: ys)

   431 apply(auto simp add: add_assoc)

   432 done

   433 

   434 lemma perm_list_exists:

   435   fixes p::perm

   436   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   437 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)

   438 apply(rename_tac p)

   439 apply(case_tac "supp p = {}")

   440 apply(simp)

   441 apply(simp add: supp_perm)

   442 apply(drule perm_zero)

   443 apply(simp)

   444 apply(rule_tac x="[]" in exI)

   445 apply(simp add: supp_Nil)

   446 apply(subgoal_tac "\<exists>x. x \<in> supp p")

   447 defer

   448 apply(auto)[1]

   449 apply(erule exE)

   450 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)

   451 apply(drule mp)

   452 defer

   453 apply(erule exE)

   454 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)

   455 apply(simp add: add_perm_apend)

   456 apply(erule conjE)

   457 apply(drule sym)

   458 apply(simp)

   459 apply(simp add: expand_perm_eq)

   460 apply(simp add: supp_append)

   461 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)

   462 apply(rule conjI)

   463 prefer 2

   464 apply(auto)[1]

   465 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))

   466 defer

   467 apply(rule psubset_card_mono)

   468 apply(simp add: finite_supp)

   469 apply(rule psubsetI)

   470 defer

   471 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")

   472 apply(blast)

   473 apply(simp add: supp_perm)

   474 defer

   475 apply(auto simp add: supp_perm)[1]

   476 apply(case_tac "x = xa")

   477 apply(simp)

   478 apply(case_tac "((- p) \<bullet> x) = xa")

   479 apply(simp)

   480 apply(case_tac "sort_of xa = sort_of x")

   481 apply(simp)

   482 apply(auto)[1]

   483 apply(simp)

   484 apply(simp)

   485 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")

   486 apply(blast)

   487 apply(auto simp add: supp_perm)[1]

   488 apply(case_tac "x = xa")

   489 apply(simp)

   490 apply(case_tac "((- p) \<bullet> x) = xa")

   491 apply(simp)

   492 apply(case_tac "sort_of xa = sort_of x")

   493 apply(simp)

   494 apply(auto)[1]

   495 apply(simp)

   496 apply(simp)

   497 done

   498 

   499 lemma tt0:

   500   fixes p::perm

   501   shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"

   502 apply(auto simp add: fresh_star_def supp_perm fresh_def)

   503 done

   504 

   505 lemma uu0:

   506   shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"

   507 apply(induct xs rule: add_perm.induct)

   508 apply(simp)

   509 apply(simp add: swap_fresh_fresh)

   510 done

   511 

   512 lemma yy0:

   513   fixes xs::"(atom \<times> atom) list"

   514   shows "supp xs = elem_perm xs"

   515 apply(induct xs rule: elem_perm.induct)

   516 apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)

   517 done

   518 

   519 lemma tt1:

   520   shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"

   521 apply(drule tt0)

   522 apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")

   523 prefer 2

   524 apply(rule perm_list_exists)

   525 apply(erule exE)

   526 apply(simp only: yy0)

   527 apply(rule uu0)

   528 apply(auto)

   529 done

   530 

   531 

   532 lemma perm_induct_test:

   533   fixes P :: "perm => bool"

   534   assumes fin: "finite (supp p)" 

   535   assumes zero: "P 0"

   536   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"

   537   assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   538   shows "P p"

   539 using fin

   540 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)

   541 apply(simp add: supp_perm)

   542 apply(drule perm_zero)

   543 apply(simp add: zero)

   544 apply(rotate_tac 3)

   545 oops

   546 lemma tt:

   547   "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"

   548 oops

   549 

   550 lemma yy:

   551   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"

   552   shows "S1 = S2"

   553 using assms

   554 apply (metis insert_Diff_single insert_absorb)

   555 done

   556 

   557 lemma permute_boolI:

   558   fixes P::"bool"

   559   shows "p \<bullet> P \<Longrightarrow> P"

   560 apply(simp add: permute_bool_def)

   561 done

   562 

   563 lemma permute_boolE:

   564   fixes P::"bool"

   565   shows "P \<Longrightarrow> p \<bullet> P"

   566 apply(simp add: permute_bool_def)

   567 done

   568 

   569 lemma fresh_star_eqvt:

   570   shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"

   571 apply(simp add: permute_bool_def)

   572 apply(auto simp add: fresh_star_def)

   573 apply(drule_tac x="(- p) \<bullet> xa" in bspec)

   574 apply(rule_tac p="p" in permute_boolI)

   575 apply(simp add: mem_eqvt)

   576 apply(rule_tac p="- p" in permute_boolI)

   577 apply(simp add: fresh_eqvt)

   578 apply(drule_tac x="p \<bullet> xa" in bspec)

   579 apply(rule_tac p="- p" in permute_boolI)

   580 apply(simp add: mem_eqvt)

   581 apply(rule_tac p="p" in permute_boolI)

   582 apply(simp add: fresh_eqvt)

   583 done

   584 

   585 lemma kk:

   586   assumes a: "p \<bullet> x = y"

   587   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"

   588 using a

   589 apply(auto)

   590 apply(rule_tac p="- p" in permute_boolI)

   591 apply(simp add: mem_eqvt supp_eqvt)

   592 done

   593 

   594 lemma ww:

   595   assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"

   596   shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"

   597 apply(subgoal_tac "(supp x) supports x")

   598 apply(simp add: supports_def)

   599 using assms

   600 apply -

   601 apply(drule_tac x="a" in spec)

   602 defer

   603 apply(rule supp_supports)

   604 apply(auto)

   605 apply(rotate_tac 1)

   606 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)

   607 apply(simp add: mem_eqvt supp_eqvt)

   608 done

   609 

   610 lemma zz:

   611   assumes "p \<bullet> x \<noteq> p \<bullet> y"

   612   shows "x \<noteq> y"

   613 using assms

   614 apply(auto)

   615 done

   616 

   617 lemma alpha_abs_sym:

   618   assumes a: "({a}, x) \<approx>abs ({b}, y)"

   619   shows "({b}, y) \<approx>abs ({a}, x)"

   620 using a

   621 apply(simp)

   622 apply(erule exE)

   623 apply(rule_tac x="- p" in exI)

   624 apply(simp add: alpha_gen)

   625 apply(simp add: fresh_star_def fresh_minus_perm)

   626 apply (metis permute_minus_cancel(2))

   627 done

   628 

   629 lemma alpha_abs_trans:

   630   assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"

   631   assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"

   632   shows "({a1}, x1) \<approx>abs ({a3}, x3)"

   633 using a b

   634 apply(simp)

   635 apply(erule exE)+

   636 apply(rule_tac x="pa + p" in exI)

   637 apply(simp add: alpha_gen)

   638 apply(simp add: fresh_star_def fresh_plus_perm)

   639 done

   640 

   641 lemma alpha_equal:

   642   assumes a: "({a}, x) \<approx>abs ({a}, y)" 

   643   shows "(a, x) \<approx>abs1 (a, y)"

   644 using a

   645 apply(simp)

   646 apply(erule exE)

   647 apply(simp add: alpha_gen)

   648 apply(erule conjE)+

   649 apply(case_tac "a \<notin> supp x")

   650 apply(simp)

   651 apply(subgoal_tac "supp x \<sharp>* p")

   652 apply(drule tt1)

   653 apply(simp)

   654 apply(simp)

   655 apply(simp)

   656 apply(case_tac "a \<notin> supp y")

   657 apply(simp)

   658 apply(drule tt1)

   659 apply(clarify)

   660 apply(simp (no_asm_use))

   661 apply(simp)

   662 apply(simp)

   663 apply(drule yy)

   664 apply(simp)

   665 apply(simp)

   666 apply(simp)

   667 apply(case_tac "a \<sharp> p")

   668 apply(subgoal_tac "supp y \<sharp>* p")

   669 apply(drule tt1)

   670 apply(clarify)

   671 apply(simp (no_asm_use))

   672 apply(metis)

   673 apply(auto simp add: fresh_star_def)[1]

   674 apply(frule_tac kk)

   675 apply(drule_tac x="a" in bspec)

   676 apply(simp)

   677 apply(simp add: fresh_def)

   678 apply(simp add: supp_perm)

   679 apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")

   680 apply(simp add: fresh_def supp_perm)

   681 apply(simp add: fresh_star_def)

   682 done

   683 

   684 lemma alpha_unequal:

   685   assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"

   686   shows "(a, x) \<approx>abs1 (b, y)"

   687 using a

   688 apply -

   689 apply(subgoal_tac "a \<notin> supp x - {a}")

   690 apply(subgoal_tac "b \<notin> supp x - {a}")

   691 defer

   692 apply(simp add: alpha_gen)

   693 apply(simp)

   694 apply(drule_tac alpha_abs_swap)

   695 apply(assumption)

   696 apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)

   697 apply(drule alpha_abs_sym)

   698 apply(rotate_tac 4)

   699 apply(drule_tac alpha_abs_trans)

   700 apply(assumption)

   701 apply(drule alpha_equal)

   702 apply(simp)

   703 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)

   704 apply(simp add: fresh_eqvt)

   705 apply(simp add: fresh_def)

   706 done

   707 

   708 lemma alpha_new_old:

   709   assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" 

   710   shows "(a, x) \<approx>abs1 (b, y)"

   711 using a

   712 apply(case_tac "a=b")

   713 apply(simp only: alpha_equal)

   714 apply(drule alpha_unequal)

   715 apply(simp)

   716 apply(simp)

   717 apply(simp)

   718 done

   719 

   720 fun

   721   distinct_perms 

   722 where

   723   "distinct_perms [] = True"

   724 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"

   725 

   726 (* support of concrete atom sets *)

   727 

   728 lemma atom_eqvt_raw:

   729   fixes p::"perm"

   730   shows "(p \<bullet> atom) = atom"

   731 by (simp add: expand_fun_eq permute_fun_def atom_eqvt)

   732 

   733 lemma atom_image_cong:

   734   shows "(atom ` X = atom ` Y) = (X = Y)"

   735 apply(rule inj_image_eq_iff)

   736 apply(simp add: inj_on_def)

   737 done

   738 

   739 lemma supp_atom_image:

   740   fixes as::"'a::at_base set"

   741   shows "supp (atom ` as) = supp as"

   742 apply(simp add: supp_def)

   743 apply(simp add: image_eqvt)

   744 apply(simp add: atom_eqvt_raw)

   745 apply(simp add: atom_image_cong)

   746 done

   747 

   748 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"

   749   apply (simp add: fresh_def)

   750   apply (simp add: supp_atom_image)

   751   apply (fold fresh_def)

   752   apply (simp add: swap_fresh_fresh)

   753   done

   754 

   755 

   756 end

   757