src/HOL/Nominal/Nominal.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 66453 cc19f7ca2ed6
child 67443 3abf6a722518
permissions -rw-r--r--
tuned: each session has at most one defining entry;
     1 theory Nominal 
     2 imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"
     3 keywords
     4   "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
     5   "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
     6   "avoids"
     7 begin
     8 
     9 declare [[typedef_overloaded]]
    10 
    11 
    12 section \<open>Permutations\<close>
    13 (*======================*)
    14 
    15 type_synonym 
    16   'x prm = "('x \<times> 'x) list"
    17 
    18 (* polymorphic constants for permutation and swapping *)
    19 consts 
    20   perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
    21   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
    22 
    23 (* a "private" copy of the option type used in the abstraction function *)
    24 datatype 'a noption = nSome 'a | nNone
    25 
    26 datatype_compat noption
    27 
    28 (* a "private" copy of the product type used in the nominal induct method *)
    29 datatype ('a, 'b) nprod = nPair 'a 'b
    30 
    31 datatype_compat nprod
    32 
    33 (* an auxiliary constant for the decision procedure involving *) 
    34 (* permutations (to avoid loops when using perm-compositions)  *)
    35 definition
    36   "perm_aux pi x = pi\<bullet>x"
    37 
    38 (* overloaded permutation operations *)
    39 overloading
    40   perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
    41   perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
    42   perm_set    \<equiv> "perm :: 'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set"           (unchecked)
    43   perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
    44   perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"    (unchecked)
    45   perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
    46   perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
    47   perm_char   \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char"           (unchecked)
    48   perm_nat    \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat"             (unchecked)
    49   perm_int    \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int"             (unchecked)
    50 
    51   perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"   (unchecked)
    52   perm_nprod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
    53 begin
    54 
    55 definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    56   "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
    57 
    58 definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    59   "perm_bool pi b = b"
    60 
    61 definition perm_set :: "'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    62   "perm_set pi X = {pi \<bullet> x | x. x \<in> X}"
    63 
    64 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    65   "perm_unit pi () = ()"
    66   
    67 primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
    68   "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
    69 
    70 primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    71   nil_eqvt:  "perm_list pi []     = []"
    72 | cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    73 
    74 primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where
    75   some_eqvt:  "perm_option pi (Some x) = Some (pi\<bullet>x)"
    76 | none_eqvt:  "perm_option pi None     = None"
    77 
    78 definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
    79   "perm_char pi c = c"
    80 
    81 definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
    82   "perm_nat pi i = i"
    83 
    84 definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
    85   "perm_int pi i = i"
    86 
    87 primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
    88   nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
    89 | nnone_eqvt:  "perm_noption pi nNone     = nNone"
    90 
    91 primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
    92   "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
    93 
    94 end
    95 
    96 (* permutations on booleans *)
    97 lemmas perm_bool = perm_bool_def
    98 
    99 lemma true_eqvt [simp]:
   100   "pi \<bullet> True \<longleftrightarrow> True"
   101   by (simp add: perm_bool_def)
   102 
   103 lemma false_eqvt [simp]:
   104   "pi \<bullet> False \<longleftrightarrow> False"
   105   by (simp add: perm_bool_def)
   106 
   107 lemma perm_boolI:
   108   assumes a: "P"
   109   shows "pi\<bullet>P"
   110   using a by (simp add: perm_bool)
   111 
   112 lemma perm_boolE:
   113   assumes a: "pi\<bullet>P"
   114   shows "P"
   115   using a by (simp add: perm_bool)
   116 
   117 lemma if_eqvt:
   118   fixes pi::"'a prm"
   119   shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
   120   by (simp add: perm_fun_def)
   121 
   122 lemma imp_eqvt:
   123   shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
   124   by (simp add: perm_bool)
   125 
   126 lemma conj_eqvt:
   127   shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
   128   by (simp add: perm_bool)
   129 
   130 lemma disj_eqvt:
   131   shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"
   132   by (simp add: perm_bool)
   133 
   134 lemma neg_eqvt:
   135   shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
   136   by (simp add: perm_bool)
   137 
   138 (* permutation on sets *)
   139 lemma empty_eqvt:
   140   shows "pi\<bullet>{} = {}"
   141   by (simp add: perm_set_def)
   142 
   143 lemma union_eqvt:
   144   shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   145   by (auto simp add: perm_set_def)
   146 
   147 lemma insert_eqvt:
   148   shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
   149   by (auto simp add: perm_set_def)
   150 
   151 (* permutations on products *)
   152 lemma fst_eqvt:
   153   "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
   154  by (cases x) simp
   155 
   156 lemma snd_eqvt:
   157   "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
   158  by (cases x) simp
   159 
   160 (* permutation on lists *)
   161 lemma append_eqvt:
   162   fixes pi :: "'x prm"
   163   and   l1 :: "'a list"
   164   and   l2 :: "'a list"
   165   shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
   166   by (induct l1) auto
   167 
   168 lemma rev_eqvt:
   169   fixes pi :: "'x prm"
   170   and   l  :: "'a list"
   171   shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
   172   by (induct l) (simp_all add: append_eqvt)
   173 
   174 lemma set_eqvt:
   175   fixes pi :: "'x prm"
   176   and   xs :: "'a list"
   177   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
   178 by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
   179 
   180 (* permutation on characters and strings *)
   181 lemma perm_string:
   182   fixes s::"string"
   183   shows "pi\<bullet>s = s"
   184   by (induct s)(auto simp add: perm_char_def)
   185 
   186 
   187 section \<open>permutation equality\<close>
   188 (*==============================*)
   189 
   190 definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where
   191   "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)"
   192 
   193 section \<open>Support, Freshness and Supports\<close>
   194 (*========================================*)
   195 definition supp :: "'a \<Rightarrow> ('x set)" where  
   196    "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   197 
   198 definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where
   199    "a \<sharp> x \<longleftrightarrow> a \<notin> supp x"
   200 
   201 definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where
   202    "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))"
   203 
   204 (* lemmas about supp *)
   205 lemma supp_fresh_iff: 
   206   fixes x :: "'a"
   207   shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
   208   by (simp add: fresh_def)
   209 
   210 lemma supp_unit:
   211   shows "supp () = {}"
   212   by (simp add: supp_def)
   213 
   214 lemma supp_set_empty:
   215   shows "supp {} = {}"
   216   by (force simp add: supp_def empty_eqvt)
   217 
   218 lemma supp_prod: 
   219   fixes x :: "'a"
   220   and   y :: "'b"
   221   shows "(supp (x,y)) = (supp x)\<union>(supp y)"
   222   by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
   223 
   224 lemma supp_nprod: 
   225   fixes x :: "'a"
   226   and   y :: "'b"
   227   shows "(supp (nPair x y)) = (supp x)\<union>(supp y)"
   228   by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
   229 
   230 lemma supp_list_nil:
   231   shows "supp [] = {}"
   232   by (simp add: supp_def)
   233 
   234 lemma supp_list_cons:
   235   fixes x  :: "'a"
   236   and   xs :: "'a list"
   237   shows "supp (x#xs) = (supp x)\<union>(supp xs)"
   238   by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
   239 
   240 lemma supp_list_append:
   241   fixes xs :: "'a list"
   242   and   ys :: "'a list"
   243   shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
   244   by (induct xs) (auto simp add: supp_list_nil supp_list_cons)
   245 
   246 lemma supp_list_rev:
   247   fixes xs :: "'a list"
   248   shows "supp (rev xs) = (supp xs)"
   249   by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
   250 
   251 lemma supp_bool:
   252   fixes x  :: "bool"
   253   shows "supp x = {}"
   254   by (cases "x") (simp_all add: supp_def)
   255 
   256 lemma supp_some:
   257   fixes x :: "'a"
   258   shows "supp (Some x) = (supp x)"
   259   by (simp add: supp_def)
   260 
   261 lemma supp_none:
   262   fixes x :: "'a"
   263   shows "supp (None) = {}"
   264   by (simp add: supp_def)
   265 
   266 lemma supp_int:
   267   fixes i::"int"
   268   shows "supp (i) = {}"
   269   by (simp add: supp_def perm_int_def)
   270 
   271 lemma supp_nat:
   272   fixes n::"nat"
   273   shows "(supp n) = {}"
   274   by (simp add: supp_def perm_nat_def)
   275 
   276 lemma supp_char:
   277   fixes c::"char"
   278   shows "(supp c) = {}"
   279   by (simp add: supp_def perm_char_def)
   280   
   281 lemma supp_string:
   282   fixes s::"string"
   283   shows "(supp s) = {}"
   284   by (simp add: supp_def perm_string)
   285 
   286 (* lemmas about freshness *)
   287 lemma fresh_set_empty:
   288   shows "a\<sharp>{}"
   289   by (simp add: fresh_def supp_set_empty)
   290 
   291 lemma fresh_unit:
   292   shows "a\<sharp>()"
   293   by (simp add: fresh_def supp_unit)
   294 
   295 lemma fresh_prod:
   296   fixes a :: "'x"
   297   and   x :: "'a"
   298   and   y :: "'b"
   299   shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
   300   by (simp add: fresh_def supp_prod)
   301 
   302 lemma fresh_list_nil:
   303   fixes a :: "'x"
   304   shows "a\<sharp>[]"
   305   by (simp add: fresh_def supp_list_nil) 
   306 
   307 lemma fresh_list_cons:
   308   fixes a :: "'x"
   309   and   x :: "'a"
   310   and   xs :: "'a list"
   311   shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
   312   by (simp add: fresh_def supp_list_cons)
   313 
   314 lemma fresh_list_append:
   315   fixes a :: "'x"
   316   and   xs :: "'a list"
   317   and   ys :: "'a list"
   318   shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
   319   by (simp add: fresh_def supp_list_append)
   320 
   321 lemma fresh_list_rev:
   322   fixes a :: "'x"
   323   and   xs :: "'a list"
   324   shows "a\<sharp>(rev xs) = a\<sharp>xs"
   325   by (simp add: fresh_def supp_list_rev)
   326 
   327 lemma fresh_none:
   328   fixes a :: "'x"
   329   shows "a\<sharp>None"
   330   by (simp add: fresh_def supp_none)
   331 
   332 lemma fresh_some:
   333   fixes a :: "'x"
   334   and   x :: "'a"
   335   shows "a\<sharp>(Some x) = a\<sharp>x"
   336   by (simp add: fresh_def supp_some)
   337 
   338 lemma fresh_int:
   339   fixes a :: "'x"
   340   and   i :: "int"
   341   shows "a\<sharp>i"
   342   by (simp add: fresh_def supp_int)
   343 
   344 lemma fresh_nat:
   345   fixes a :: "'x"
   346   and   n :: "nat"
   347   shows "a\<sharp>n"
   348   by (simp add: fresh_def supp_nat)
   349 
   350 lemma fresh_char:
   351   fixes a :: "'x"
   352   and   c :: "char"
   353   shows "a\<sharp>c"
   354   by (simp add: fresh_def supp_char)
   355 
   356 lemma fresh_string:
   357   fixes a :: "'x"
   358   and   s :: "string"
   359   shows "a\<sharp>s"
   360   by (simp add: fresh_def supp_string)
   361 
   362 lemma fresh_bool:
   363   fixes a :: "'x"
   364   and   b :: "bool"
   365   shows "a\<sharp>b"
   366   by (simp add: fresh_def supp_bool)
   367 
   368 text \<open>Normalization of freshness results; cf.\ \<open>nominal_induct\<close>\<close>
   369 lemma fresh_unit_elim: 
   370   shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
   371   by (simp add: fresh_def supp_unit)
   372 
   373 lemma fresh_prod_elim: 
   374   shows "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
   375   by rule (simp_all add: fresh_prod)
   376 
   377 (* this rule needs to be added before the fresh_prodD is *)
   378 (* added to the simplifier with mksimps                  *) 
   379 lemma [simp]:
   380   shows "a\<sharp>x1 \<Longrightarrow> a\<sharp>x2 \<Longrightarrow> a\<sharp>(x1,x2)"
   381   by (simp add: fresh_prod)
   382 
   383 lemma fresh_prodD:
   384   shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x"
   385   and   "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
   386   by (simp_all add: fresh_prod)
   387 
   388 ML \<open>
   389   val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
   390 \<close>
   391 declaration \<open>fn _ =>
   392   Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
   393 \<close>
   394 
   395 section \<open>Abstract Properties for Permutations and  Atoms\<close>
   396 (*=========================================================*)
   397 
   398 (* properties for being a permutation type *)
   399 definition
   400   "pt TYPE('a) TYPE('x) \<equiv> 
   401      (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
   402      (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
   403      (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
   404 
   405 (* properties for being an atom type *)
   406 definition
   407   "at TYPE('x) \<equiv> 
   408      (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
   409      (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 
   410      (\<forall>(a::'x) (b::'x) (c::'x). swap (a,b) c = (if a=c then b else (if b=c then a else c))) \<and> 
   411      (infinite (UNIV::'x set))"
   412 
   413 (* property of two atom-types being disjoint *)
   414 definition
   415   "disjoint TYPE('x) TYPE('y) \<equiv> 
   416        (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 
   417        (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
   418 
   419 (* composition property of two permutation on a type 'a *)
   420 definition
   421   "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
   422       (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 
   423 
   424 (* property of having finite support *)
   425 definition
   426   "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
   427 
   428 section \<open>Lemmas about the atom-type properties\<close>
   429 (*==============================================*)
   430 
   431 lemma at1: 
   432   fixes x::"'x"
   433   assumes a: "at TYPE('x)"
   434   shows "([]::'x prm)\<bullet>x = x"
   435   using a by (simp add: at_def)
   436 
   437 lemma at2: 
   438   fixes a ::"'x"
   439   and   b ::"'x"
   440   and   x ::"'x"
   441   and   pi::"'x prm"
   442   assumes a: "at TYPE('x)"
   443   shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
   444   using a by (simp only: at_def)
   445 
   446 lemma at3: 
   447   fixes a ::"'x"
   448   and   b ::"'x"
   449   and   c ::"'x"
   450   assumes a: "at TYPE('x)"
   451   shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
   452   using a by (simp only: at_def)
   453 
   454 (* rules to calculate simple permutations *)
   455 lemmas at_calc = at2 at1 at3
   456 
   457 lemma at_swap_simps:
   458   fixes a ::"'x"
   459   and   b ::"'x"
   460   assumes a: "at TYPE('x)"
   461   shows "[(a,b)]\<bullet>a = b"
   462   and   "[(a,b)]\<bullet>b = a"
   463   and   "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c"
   464   using a by (simp_all add: at_calc)
   465 
   466 lemma at4: 
   467   assumes a: "at TYPE('x)"
   468   shows "infinite (UNIV::'x set)"
   469   using a by (simp add: at_def)
   470 
   471 lemma at_append:
   472   fixes pi1 :: "'x prm"
   473   and   pi2 :: "'x prm"
   474   and   c   :: "'x"
   475   assumes at: "at TYPE('x)" 
   476   shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
   477 proof (induct pi1)
   478   case Nil show ?case by (simp add: at1[OF at])
   479 next
   480   case (Cons x xs)
   481   have "(xs@pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)" by fact
   482   also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
   483   ultimately show ?case by (cases "x", simp add:  at2[OF at])
   484 qed
   485  
   486 lemma at_swap:
   487   fixes a :: "'x"
   488   and   b :: "'x"
   489   and   c :: "'x"
   490   assumes at: "at TYPE('x)" 
   491   shows "swap (a,b) (swap (a,b) c) = c"
   492   by (auto simp add: at3[OF at])
   493 
   494 lemma at_rev_pi:
   495   fixes pi :: "'x prm"
   496   and   c  :: "'x"
   497   assumes at: "at TYPE('x)"
   498   shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
   499 proof(induct pi)
   500   case Nil show ?case by (simp add: at1[OF at])
   501 next
   502   case (Cons x xs) thus ?case 
   503     by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
   504 qed
   505 
   506 lemma at_pi_rev:
   507   fixes pi :: "'x prm"
   508   and   x  :: "'x"
   509   assumes at: "at TYPE('x)"
   510   shows "pi\<bullet>((rev pi)\<bullet>x) = x"
   511   by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
   512 
   513 lemma at_bij1: 
   514   fixes pi :: "'x prm"
   515   and   x  :: "'x"
   516   and   y  :: "'x"
   517   assumes at: "at TYPE('x)"
   518   and     a:  "(pi\<bullet>x) = y"
   519   shows   "x=(rev pi)\<bullet>y"
   520 proof -
   521   from a have "y=(pi\<bullet>x)" by (rule sym)
   522   thus ?thesis by (simp only: at_rev_pi[OF at])
   523 qed
   524 
   525 lemma at_bij2: 
   526   fixes pi :: "'x prm"
   527   and   x  :: "'x"
   528   and   y  :: "'x"
   529   assumes at: "at TYPE('x)"
   530   and     a:  "((rev pi)\<bullet>x) = y"
   531   shows   "x=pi\<bullet>y"
   532 proof -
   533   from a have "y=((rev pi)\<bullet>x)" by (rule sym)
   534   thus ?thesis by (simp only: at_pi_rev[OF at])
   535 qed
   536 
   537 lemma at_bij:
   538   fixes pi :: "'x prm"
   539   and   x  :: "'x"
   540   and   y  :: "'x"
   541   assumes at: "at TYPE('x)"
   542   shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
   543 proof 
   544   assume "pi\<bullet>x = pi\<bullet>y" 
   545   hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
   546   thus "x=y" by (simp only: at_rev_pi[OF at])
   547 next
   548   assume "x=y"
   549   thus "pi\<bullet>x = pi\<bullet>y" by simp
   550 qed
   551 
   552 lemma at_supp:
   553   fixes x :: "'x"
   554   assumes at: "at TYPE('x)"
   555   shows "supp x = {x}"
   556 by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at])
   557 
   558 lemma at_fresh:
   559   fixes a :: "'x"
   560   and   b :: "'x"
   561   assumes at: "at TYPE('x)"
   562   shows "(a\<sharp>b) = (a\<noteq>b)" 
   563   by (simp add: at_supp[OF at] fresh_def)
   564 
   565 lemma at_prm_fresh1:
   566   fixes c :: "'x"
   567   and   pi:: "'x prm"
   568   assumes at: "at TYPE('x)"
   569   and     a: "c\<sharp>pi" 
   570   shows "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b"
   571 using a by (induct pi) (auto simp add: fresh_list_cons fresh_prod at_fresh[OF at])
   572 
   573 lemma at_prm_fresh2:
   574   fixes c :: "'x"
   575   and   pi:: "'x prm"
   576   assumes at: "at TYPE('x)"
   577   and     a: "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b" 
   578   shows "pi\<bullet>c = c"
   579 using a  by(induct pi) (auto simp add: at1[OF at] at2[OF at] at3[OF at])
   580 
   581 lemma at_prm_fresh:
   582   fixes c :: "'x"
   583   and   pi:: "'x prm"
   584   assumes at: "at TYPE('x)"
   585   and     a: "c\<sharp>pi" 
   586   shows "pi\<bullet>c = c"
   587 by (rule at_prm_fresh2[OF at], rule at_prm_fresh1[OF at, OF a])
   588 
   589 lemma at_prm_rev_eq:
   590   fixes pi1 :: "'x prm"
   591   and   pi2 :: "'x prm"
   592   assumes at: "at TYPE('x)"
   593   shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
   594 proof (simp add: prm_eq_def, auto)
   595   fix x
   596   assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   597   hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
   598   hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
   599   hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
   600   thus "pi1\<bullet>x  =  pi2\<bullet>x" by simp
   601 next
   602   fix x
   603   assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
   604   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
   605   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
   606   hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
   607   thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
   608 qed
   609 
   610 lemma at_prm_eq_append:
   611   fixes pi1 :: "'x prm"
   612   and   pi2 :: "'x prm"
   613   and   pi3 :: "'x prm"
   614   assumes at: "at TYPE('x)"
   615   and     a: "pi1 \<triangleq> pi2"
   616   shows "(pi3@pi1) \<triangleq> (pi3@pi2)"
   617 using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at])
   618 
   619 lemma at_prm_eq_append':
   620   fixes pi1 :: "'x prm"
   621   and   pi2 :: "'x prm"
   622   and   pi3 :: "'x prm"
   623   assumes at: "at TYPE('x)"
   624   and     a: "pi1 \<triangleq> pi2"
   625   shows "(pi1@pi3) \<triangleq> (pi2@pi3)"
   626 using a by (simp add: prm_eq_def at_append[OF at])
   627 
   628 lemma at_prm_eq_trans:
   629   fixes pi1 :: "'x prm"
   630   and   pi2 :: "'x prm"
   631   and   pi3 :: "'x prm"
   632   assumes a1: "pi1 \<triangleq> pi2"
   633   and     a2: "pi2 \<triangleq> pi3"  
   634   shows "pi1 \<triangleq> pi3"
   635 using a1 a2 by (auto simp add: prm_eq_def)
   636   
   637 lemma at_prm_eq_refl:
   638   fixes pi :: "'x prm"
   639   shows "pi \<triangleq> pi"
   640 by (simp add: prm_eq_def)
   641 
   642 lemma at_prm_rev_eq1:
   643   fixes pi1 :: "'x prm"
   644   and   pi2 :: "'x prm"
   645   assumes at: "at TYPE('x)"
   646   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   647   by (simp add: at_prm_rev_eq[OF at])
   648 
   649 lemma at_ds1:
   650   fixes a  :: "'x"
   651   assumes at: "at TYPE('x)"
   652   shows "[(a,a)] \<triangleq> []"
   653   by (force simp add: prm_eq_def at_calc[OF at])
   654 
   655 lemma at_ds2: 
   656   fixes pi :: "'x prm"
   657   and   a  :: "'x"
   658   and   b  :: "'x"
   659   assumes at: "at TYPE('x)"
   660   shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])"
   661   by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
   662       at_rev_pi[OF at] at_calc[OF at])
   663 
   664 lemma at_ds3: 
   665   fixes a  :: "'x"
   666   and   b  :: "'x"
   667   and   c  :: "'x"
   668   assumes at: "at TYPE('x)"
   669   and     a:  "distinct [a,b,c]"
   670   shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]"
   671   using a by (force simp add: prm_eq_def at_calc[OF at])
   672 
   673 lemma at_ds4: 
   674   fixes a  :: "'x"
   675   and   b  :: "'x"
   676   and   pi  :: "'x prm"
   677   assumes at: "at TYPE('x)"
   678   shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)"
   679   by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
   680       at_pi_rev[OF at] at_rev_pi[OF at])
   681 
   682 lemma at_ds5: 
   683   fixes a  :: "'x"
   684   and   b  :: "'x"
   685   assumes at: "at TYPE('x)"
   686   shows "[(a,b)] \<triangleq> [(b,a)]"
   687   by (force simp add: prm_eq_def at_calc[OF at])
   688 
   689 lemma at_ds5': 
   690   fixes a  :: "'x"
   691   and   b  :: "'x"
   692   assumes at: "at TYPE('x)"
   693   shows "[(a,b),(b,a)] \<triangleq> []"
   694   by (force simp add: prm_eq_def at_calc[OF at])
   695 
   696 lemma at_ds6: 
   697   fixes a  :: "'x"
   698   and   b  :: "'x"
   699   and   c  :: "'x"
   700   assumes at: "at TYPE('x)"
   701   and     a: "distinct [a,b,c]"
   702   shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]"
   703   using a by (force simp add: prm_eq_def at_calc[OF at])
   704 
   705 lemma at_ds7:
   706   fixes pi :: "'x prm"
   707   assumes at: "at TYPE('x)"
   708   shows "((rev pi)@pi) \<triangleq> []"
   709   by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
   710 
   711 lemma at_ds8_aux:
   712   fixes pi :: "'x prm"
   713   and   a  :: "'x"
   714   and   b  :: "'x"
   715   and   c  :: "'x"
   716   assumes at: "at TYPE('x)"
   717   shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
   718   by (force simp add: at_calc[OF at] at_bij[OF at])
   719 
   720 lemma at_ds8: 
   721   fixes pi1 :: "'x prm"
   722   and   pi2 :: "'x prm"
   723   and   a  :: "'x"
   724   and   b  :: "'x"
   725   assumes at: "at TYPE('x)"
   726   shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)"
   727 apply(induct_tac pi2)
   728 apply(simp add: prm_eq_def)
   729 apply(auto simp add: prm_eq_def)
   730 apply(simp add: at2[OF at])
   731 apply(drule_tac x="aa" in spec)
   732 apply(drule sym)
   733 apply(simp)
   734 apply(simp add: at_append[OF at])
   735 apply(simp add: at2[OF at])
   736 apply(simp add: at_ds8_aux[OF at])
   737 done
   738 
   739 lemma at_ds9: 
   740   fixes pi1 :: "'x prm"
   741   and   pi2 :: "'x prm"
   742   and   a  :: "'x"
   743   and   b  :: "'x"
   744   assumes at: "at TYPE('x)"
   745   shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
   746 apply(induct_tac pi2)
   747 apply(simp add: prm_eq_def)
   748 apply(auto simp add: prm_eq_def)
   749 apply(simp add: at_append[OF at])
   750 apply(simp add: at2[OF at] at1[OF at])
   751 apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
   752 apply(drule sym)
   753 apply(simp)
   754 apply(simp add: at_ds8_aux[OF at])
   755 apply(simp add: at_rev_pi[OF at])
   756 done
   757 
   758 lemma at_ds10:
   759   fixes pi :: "'x prm"
   760   and   a  :: "'x"
   761   and   b  :: "'x"
   762   assumes at: "at TYPE('x)"
   763   and     a:  "b\<sharp>(rev pi)"
   764   shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])"
   765 using a
   766 apply -
   767 apply(rule at_prm_eq_trans)
   768 apply(rule at_ds2[OF at])
   769 apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
   770 apply(rule at_prm_eq_refl)
   771 done
   772 
   773 \<comment>"there always exists an atom that is not being in a finite set"
   774 lemma ex_in_inf:
   775   fixes   A::"'x set"
   776   assumes at: "at TYPE('x)"
   777   and     fs: "finite A"
   778   obtains c::"'x" where "c\<notin>A"
   779 proof -
   780   from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
   781     by (simp add: Diff_infinite_finite)
   782   hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
   783   then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
   784   then have "c\<notin>A" by simp
   785   then show ?thesis ..
   786 qed
   787 
   788 text \<open>there always exists a fresh name for an object with finite support\<close>
   789 lemma at_exists_fresh': 
   790   fixes  x :: "'a"
   791   assumes at: "at TYPE('x)"
   792   and     fs: "finite ((supp x)::'x set)"
   793   shows "\<exists>c::'x. c\<sharp>x"
   794   by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs])
   795 
   796 lemma at_exists_fresh: 
   797   fixes  x :: "'a"
   798   assumes at: "at TYPE('x)"
   799   and     fs: "finite ((supp x)::'x set)"
   800   obtains c::"'x" where  "c\<sharp>x"
   801   by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
   802 
   803 lemma at_finite_select: 
   804   fixes S::"'a set"
   805   assumes a: "at TYPE('a)"
   806   and     b: "finite S" 
   807   shows "\<exists>x. x \<notin> S" 
   808   using a b
   809   apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
   810   apply(simp add: at_def)
   811   apply(subgoal_tac "UNIV - S \<noteq> {}")
   812   apply(simp only: ex_in_conv [symmetric])
   813   apply(blast)
   814   apply(rule notI)
   815   apply(simp)
   816   done
   817 
   818 lemma at_different:
   819   assumes at: "at TYPE('x)"
   820   shows "\<exists>(b::'x). a\<noteq>b"
   821 proof -
   822   have "infinite (UNIV::'x set)" by (rule at4[OF at])
   823   hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
   824   have "(UNIV-{a}) \<noteq> ({}::'x set)" 
   825   proof (rule_tac ccontr, drule_tac notnotD)
   826     assume "UNIV-{a} = ({}::'x set)"
   827     with inf2 have "infinite ({}::'x set)" by simp
   828     then show "False" by auto
   829   qed
   830   hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
   831   then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast
   832   from mem2 have "a\<noteq>b" by blast
   833   then show "\<exists>(b::'x). a\<noteq>b" by blast
   834 qed
   835 
   836 \<comment>"the at-props imply the pt-props"
   837 lemma at_pt_inst:
   838   assumes at: "at TYPE('x)"
   839   shows "pt TYPE('x) TYPE('x)"
   840 apply(auto simp only: pt_def)
   841 apply(simp only: at1[OF at])
   842 apply(simp only: at_append[OF at]) 
   843 apply(simp only: prm_eq_def)
   844 done
   845 
   846 section \<open>finite support properties\<close>
   847 (*===================================*)
   848 
   849 lemma fs1:
   850   fixes x :: "'a"
   851   assumes a: "fs TYPE('a) TYPE('x)"
   852   shows "finite ((supp x)::'x set)"
   853   using a by (simp add: fs_def)
   854 
   855 lemma fs_at_inst:
   856   fixes a :: "'x"
   857   assumes at: "at TYPE('x)"
   858   shows "fs TYPE('x) TYPE('x)"
   859 apply(simp add: fs_def) 
   860 apply(simp add: at_supp[OF at])
   861 done
   862 
   863 lemma fs_unit_inst:
   864   shows "fs TYPE(unit) TYPE('x)"
   865 apply(simp add: fs_def)
   866 apply(simp add: supp_unit)
   867 done
   868 
   869 lemma fs_prod_inst:
   870   assumes fsa: "fs TYPE('a) TYPE('x)"
   871   and     fsb: "fs TYPE('b) TYPE('x)"
   872   shows "fs TYPE('a\<times>'b) TYPE('x)"
   873 apply(unfold fs_def)
   874 apply(auto simp add: supp_prod)
   875 apply(rule fs1[OF fsa])
   876 apply(rule fs1[OF fsb])
   877 done
   878 
   879 lemma fs_nprod_inst:
   880   assumes fsa: "fs TYPE('a) TYPE('x)"
   881   and     fsb: "fs TYPE('b) TYPE('x)"
   882   shows "fs TYPE(('a,'b) nprod) TYPE('x)"
   883 apply(unfold fs_def, rule allI)
   884 apply(case_tac x)
   885 apply(auto simp add: supp_nprod)
   886 apply(rule fs1[OF fsa])
   887 apply(rule fs1[OF fsb])
   888 done
   889 
   890 lemma fs_list_inst:
   891   assumes fs: "fs TYPE('a) TYPE('x)"
   892   shows "fs TYPE('a list) TYPE('x)"
   893 apply(simp add: fs_def, rule allI)
   894 apply(induct_tac x)
   895 apply(simp add: supp_list_nil)
   896 apply(simp add: supp_list_cons)
   897 apply(rule fs1[OF fs])
   898 done
   899 
   900 lemma fs_option_inst:
   901   assumes fs: "fs TYPE('a) TYPE('x)"
   902   shows "fs TYPE('a option) TYPE('x)"
   903 apply(simp add: fs_def, rule allI)
   904 apply(case_tac x)
   905 apply(simp add: supp_none)
   906 apply(simp add: supp_some)
   907 apply(rule fs1[OF fs])
   908 done
   909 
   910 section \<open>Lemmas about the permutation properties\<close>
   911 (*=================================================*)
   912 
   913 lemma pt1:
   914   fixes x::"'a"
   915   assumes a: "pt TYPE('a) TYPE('x)"
   916   shows "([]::'x prm)\<bullet>x = x"
   917   using a by (simp add: pt_def)
   918 
   919 lemma pt2: 
   920   fixes pi1::"'x prm"
   921   and   pi2::"'x prm"
   922   and   x  ::"'a"
   923   assumes a: "pt TYPE('a) TYPE('x)"
   924   shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
   925   using a by (simp add: pt_def)
   926 
   927 lemma pt3:
   928   fixes pi1::"'x prm"
   929   and   pi2::"'x prm"
   930   and   x  ::"'a"
   931   assumes a: "pt TYPE('a) TYPE('x)"
   932   shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
   933   using a by (simp add: pt_def)
   934 
   935 lemma pt3_rev:
   936   fixes pi1::"'x prm"
   937   and   pi2::"'x prm"
   938   and   x  ::"'a"
   939   assumes pt: "pt TYPE('a) TYPE('x)"
   940   and     at: "at TYPE('x)"
   941   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   942   by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
   943 
   944 section \<open>composition properties\<close>
   945 (* ============================== *)
   946 lemma cp1:
   947   fixes pi1::"'x prm"
   948   and   pi2::"'y prm"
   949   and   x  ::"'a"
   950   assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   951   shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
   952   using cp by (simp add: cp_def)
   953 
   954 lemma cp_pt_inst:
   955   assumes pt: "pt TYPE('a) TYPE('x)"
   956   and     at: "at TYPE('x)"
   957   shows "cp TYPE('a) TYPE('x) TYPE('x)"
   958 apply(auto simp add: cp_def pt2[OF pt,symmetric])
   959 apply(rule pt3[OF pt])
   960 apply(rule at_ds8[OF at])
   961 done
   962 
   963 section \<open>disjointness properties\<close>
   964 (*=================================*)
   965 lemma dj_perm_forget:
   966   fixes pi::"'y prm"
   967   and   x ::"'x"
   968   assumes dj: "disjoint TYPE('x) TYPE('y)"
   969   shows "pi\<bullet>x=x" 
   970   using dj by (simp_all add: disjoint_def)
   971 
   972 lemma dj_perm_set_forget:
   973   fixes pi::"'y prm"
   974   and   x ::"'x set"
   975   assumes dj: "disjoint TYPE('x) TYPE('y)"
   976   shows "pi\<bullet>x=x" 
   977   using dj by (simp_all add: perm_set_def disjoint_def)
   978 
   979 lemma dj_perm_perm_forget:
   980   fixes pi1::"'x prm"
   981   and   pi2::"'y prm"
   982   assumes dj: "disjoint TYPE('x) TYPE('y)"
   983   shows "pi2\<bullet>pi1=pi1"
   984   using dj by (induct pi1, auto simp add: disjoint_def)
   985 
   986 lemma dj_cp:
   987   fixes pi1::"'x prm"
   988   and   pi2::"'y prm"
   989   and   x  ::"'a"
   990   assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   991   and     dj: "disjoint TYPE('y) TYPE('x)"
   992   shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
   993   by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
   994 
   995 lemma dj_supp:
   996   fixes a::"'x"
   997   assumes dj: "disjoint TYPE('x) TYPE('y)"
   998   shows "(supp a) = ({}::'y set)"
   999 apply(simp add: supp_def dj_perm_forget[OF dj])
  1000 done
  1001 
  1002 lemma at_fresh_ineq:
  1003   fixes a :: "'x"
  1004   and   b :: "'y"
  1005   assumes dj: "disjoint TYPE('y) TYPE('x)"
  1006   shows "a\<sharp>b" 
  1007   by (simp add: fresh_def dj_supp[OF dj])
  1008 
  1009 section \<open>permutation type instances\<close>
  1010 (* ===================================*)
  1011 
  1012 lemma pt_fun_inst:
  1013   assumes pta: "pt TYPE('a) TYPE('x)"
  1014   and     ptb: "pt TYPE('b) TYPE('x)"
  1015   and     at:  "at TYPE('x)"
  1016   shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
  1017 apply(auto simp only: pt_def)
  1018 apply(simp_all add: perm_fun_def)
  1019 apply(simp add: pt1[OF pta] pt1[OF ptb])
  1020 apply(simp add: pt2[OF pta] pt2[OF ptb])
  1021 apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*)
  1022 apply(simp add: pt3[OF pta] pt3[OF ptb])
  1023 (*A*)
  1024 apply(simp add: at_prm_rev_eq[OF at])
  1025 done
  1026 
  1027 lemma pt_bool_inst:
  1028   shows  "pt TYPE(bool) TYPE('x)"
  1029   by (simp add: pt_def perm_bool_def)
  1030 
  1031 lemma pt_set_inst:
  1032   assumes pt: "pt TYPE('a) TYPE('x)"
  1033   shows  "pt TYPE('a set) TYPE('x)"
  1034 apply(simp add: pt_def)
  1035 apply(simp_all add: perm_set_def)
  1036 apply(simp add: pt1[OF pt])
  1037 apply(force simp add: pt2[OF pt] pt3[OF pt])
  1038 done
  1039 
  1040 lemma pt_unit_inst:
  1041   shows "pt TYPE(unit) TYPE('x)"
  1042   by (simp add: pt_def)
  1043 
  1044 lemma pt_prod_inst:
  1045   assumes pta: "pt TYPE('a) TYPE('x)"
  1046   and     ptb: "pt TYPE('b) TYPE('x)"
  1047   shows  "pt TYPE('a \<times> 'b) TYPE('x)"
  1048   apply(auto simp add: pt_def)
  1049   apply(rule pt1[OF pta])
  1050   apply(rule pt1[OF ptb])
  1051   apply(rule pt2[OF pta])
  1052   apply(rule pt2[OF ptb])
  1053   apply(rule pt3[OF pta],assumption)
  1054   apply(rule pt3[OF ptb],assumption)
  1055   done
  1056 
  1057 lemma pt_list_nil: 
  1058   fixes xs :: "'a list"
  1059   assumes pt: "pt TYPE('a) TYPE ('x)"
  1060   shows "([]::'x prm)\<bullet>xs = xs" 
  1061 apply(induct_tac xs)
  1062 apply(simp_all add: pt1[OF pt])
  1063 done
  1064 
  1065 lemma pt_list_append: 
  1066   fixes pi1 :: "'x prm"
  1067   and   pi2 :: "'x prm"
  1068   and   xs  :: "'a list"
  1069   assumes pt: "pt TYPE('a) TYPE ('x)"
  1070   shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
  1071 apply(induct_tac xs)
  1072 apply(simp_all add: pt2[OF pt])
  1073 done
  1074 
  1075 lemma pt_list_prm_eq: 
  1076   fixes pi1 :: "'x prm"
  1077   and   pi2 :: "'x prm"
  1078   and   xs  :: "'a list"
  1079   assumes pt: "pt TYPE('a) TYPE ('x)"
  1080   shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
  1081 apply(induct_tac xs)
  1082 apply(simp_all add: prm_eq_def pt3[OF pt])
  1083 done
  1084 
  1085 lemma pt_list_inst:
  1086   assumes pt: "pt TYPE('a) TYPE('x)"
  1087   shows  "pt TYPE('a list) TYPE('x)"
  1088 apply(auto simp only: pt_def)
  1089 apply(rule pt_list_nil[OF pt])
  1090 apply(rule pt_list_append[OF pt])
  1091 apply(rule pt_list_prm_eq[OF pt],assumption)
  1092 done
  1093 
  1094 lemma pt_option_inst:
  1095   assumes pta: "pt TYPE('a) TYPE('x)"
  1096   shows  "pt TYPE('a option) TYPE('x)"
  1097 apply(auto simp only: pt_def)
  1098 apply(case_tac "x")
  1099 apply(simp_all add: pt1[OF pta])
  1100 apply(case_tac "x")
  1101 apply(simp_all add: pt2[OF pta])
  1102 apply(case_tac "x")
  1103 apply(simp_all add: pt3[OF pta])
  1104 done
  1105 
  1106 lemma pt_noption_inst:
  1107   assumes pta: "pt TYPE('a) TYPE('x)"
  1108   shows  "pt TYPE('a noption) TYPE('x)"
  1109 apply(auto simp only: pt_def)
  1110 apply(case_tac "x")
  1111 apply(simp_all add: pt1[OF pta])
  1112 apply(case_tac "x")
  1113 apply(simp_all add: pt2[OF pta])
  1114 apply(case_tac "x")
  1115 apply(simp_all add: pt3[OF pta])
  1116 done
  1117 
  1118 lemma pt_nprod_inst:
  1119   assumes pta: "pt TYPE('a) TYPE('x)"
  1120   and     ptb: "pt TYPE('b) TYPE('x)"
  1121   shows  "pt TYPE(('a,'b) nprod) TYPE('x)"
  1122   apply(auto simp add: pt_def)
  1123   apply(case_tac x)
  1124   apply(simp add: pt1[OF pta] pt1[OF ptb])
  1125   apply(case_tac x)
  1126   apply(simp add: pt2[OF pta] pt2[OF ptb])
  1127   apply(case_tac x)
  1128   apply(simp add: pt3[OF pta] pt3[OF ptb])
  1129   done
  1130 
  1131 section \<open>further lemmas for permutation types\<close>
  1132 (*==============================================*)
  1133 
  1134 lemma pt_rev_pi:
  1135   fixes pi :: "'x prm"
  1136   and   x  :: "'a"
  1137   assumes pt: "pt TYPE('a) TYPE('x)"
  1138   and     at: "at TYPE('x)"
  1139   shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
  1140 proof -
  1141   have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at])
  1142   hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
  1143   thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
  1144 qed
  1145 
  1146 lemma pt_pi_rev:
  1147   fixes pi :: "'x prm"
  1148   and   x  :: "'a"
  1149   assumes pt: "pt TYPE('a) TYPE('x)"
  1150   and     at: "at TYPE('x)"
  1151   shows "pi\<bullet>((rev pi)\<bullet>x) = x"
  1152   by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
  1153 
  1154 lemma pt_bij1: 
  1155   fixes pi :: "'x prm"
  1156   and   x  :: "'a"
  1157   and   y  :: "'a"
  1158   assumes pt: "pt TYPE('a) TYPE('x)"
  1159   and     at: "at TYPE('x)"
  1160   and     a:  "(pi\<bullet>x) = y"
  1161   shows   "x=(rev pi)\<bullet>y"
  1162 proof -
  1163   from a have "y=(pi\<bullet>x)" by (rule sym)
  1164   thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
  1165 qed
  1166 
  1167 lemma pt_bij2: 
  1168   fixes pi :: "'x prm"
  1169   and   x  :: "'a"
  1170   and   y  :: "'a"
  1171   assumes pt: "pt TYPE('a) TYPE('x)"
  1172   and     at: "at TYPE('x)"
  1173   and     a:  "x = (rev pi)\<bullet>y"
  1174   shows   "(pi\<bullet>x)=y"
  1175   using a by (simp add: pt_pi_rev[OF pt, OF at])
  1176 
  1177 lemma pt_bij:
  1178   fixes pi :: "'x prm"
  1179   and   x  :: "'a"
  1180   and   y  :: "'a"
  1181   assumes pt: "pt TYPE('a) TYPE('x)"
  1182   and     at: "at TYPE('x)"
  1183   shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
  1184 proof 
  1185   assume "pi\<bullet>x = pi\<bullet>y" 
  1186   hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 
  1187   thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
  1188 next
  1189   assume "x=y"
  1190   thus "pi\<bullet>x = pi\<bullet>y" by simp
  1191 qed
  1192 
  1193 lemma pt_eq_eqvt:
  1194   fixes pi :: "'x prm"
  1195   and   x  :: "'a"
  1196   and   y  :: "'a"
  1197   assumes pt: "pt TYPE('a) TYPE('x)"
  1198   and     at: "at TYPE('x)"
  1199   shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
  1200   using pt at
  1201   by (auto simp add: pt_bij perm_bool)
  1202 
  1203 lemma pt_bij3:
  1204   fixes pi :: "'x prm"
  1205   and   x  :: "'a"
  1206   and   y  :: "'a"
  1207   assumes a:  "x=y"
  1208   shows "(pi\<bullet>x = pi\<bullet>y)"
  1209   using a by simp 
  1210 
  1211 lemma pt_bij4:
  1212   fixes pi :: "'x prm"
  1213   and   x  :: "'a"
  1214   and   y  :: "'a"
  1215   assumes pt: "pt TYPE('a) TYPE('x)"
  1216   and     at: "at TYPE('x)"
  1217   and     a:  "pi\<bullet>x = pi\<bullet>y"
  1218   shows "x = y"
  1219   using a by (simp add: pt_bij[OF pt, OF at])
  1220 
  1221 lemma pt_swap_bij:
  1222   fixes a  :: "'x"
  1223   and   b  :: "'x"
  1224   and   x  :: "'a"
  1225   assumes pt: "pt TYPE('a) TYPE('x)"
  1226   and     at: "at TYPE('x)"
  1227   shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
  1228   by (rule pt_bij2[OF pt, OF at], simp)
  1229 
  1230 lemma pt_swap_bij':
  1231   fixes a  :: "'x"
  1232   and   b  :: "'x"
  1233   and   x  :: "'a"
  1234   assumes pt: "pt TYPE('a) TYPE('x)"
  1235   and     at: "at TYPE('x)"
  1236   shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x"
  1237 apply(simp add: pt2[OF pt,symmetric])
  1238 apply(rule trans)
  1239 apply(rule pt3[OF pt])
  1240 apply(rule at_ds5'[OF at])
  1241 apply(rule pt1[OF pt])
  1242 done
  1243 
  1244 lemma pt_swap_bij'':
  1245   fixes a  :: "'x"
  1246   and   x  :: "'a"
  1247   assumes pt: "pt TYPE('a) TYPE('x)"
  1248   and     at: "at TYPE('x)"
  1249   shows "[(a,a)]\<bullet>x = x"
  1250 apply(rule trans)
  1251 apply(rule pt3[OF pt])
  1252 apply(rule at_ds1[OF at])
  1253 apply(rule pt1[OF pt])
  1254 done
  1255 
  1256 lemma supp_singleton:
  1257   shows "supp {x} = supp x"
  1258   by (force simp add: supp_def perm_set_def)
  1259 
  1260 lemma fresh_singleton:
  1261   shows "a\<sharp>{x} = a\<sharp>x"
  1262   by (simp add: fresh_def supp_singleton)
  1263 
  1264 lemma pt_set_bij1:
  1265   fixes pi :: "'x prm"
  1266   and   x  :: "'a"
  1267   and   X  :: "'a set"
  1268   assumes pt: "pt TYPE('a) TYPE('x)"
  1269   and     at: "at TYPE('x)"
  1270   shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
  1271   by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  1272 
  1273 lemma pt_set_bij1a:
  1274   fixes pi :: "'x prm"
  1275   and   x  :: "'a"
  1276   and   X  :: "'a set"
  1277   assumes pt: "pt TYPE('a) TYPE('x)"
  1278   and     at: "at TYPE('x)"
  1279   shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
  1280   by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  1281 
  1282 lemma pt_set_bij:
  1283   fixes pi :: "'x prm"
  1284   and   x  :: "'a"
  1285   and   X  :: "'a set"
  1286   assumes pt: "pt TYPE('a) TYPE('x)"
  1287   and     at: "at TYPE('x)"
  1288   shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
  1289   by (simp add: perm_set_def pt_bij[OF pt, OF at])
  1290 
  1291 lemma pt_in_eqvt:
  1292   fixes pi :: "'x prm"
  1293   and   x  :: "'a"
  1294   and   X  :: "'a set"
  1295   assumes pt: "pt TYPE('a) TYPE('x)"
  1296   and     at: "at TYPE('x)"
  1297   shows "pi\<bullet>(x\<in>X)=((pi\<bullet>x)\<in>(pi\<bullet>X))"
  1298 using assms
  1299 by (auto simp add:  pt_set_bij perm_bool)
  1300 
  1301 lemma pt_set_bij2:
  1302   fixes pi :: "'x prm"
  1303   and   x  :: "'a"
  1304   and   X  :: "'a set"
  1305   assumes pt: "pt TYPE('a) TYPE('x)"
  1306   and     at: "at TYPE('x)"
  1307   and     a:  "x\<in>X"
  1308   shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
  1309   using a by (simp add: pt_set_bij[OF pt, OF at])
  1310 
  1311 lemma pt_set_bij2a:
  1312   fixes pi :: "'x prm"
  1313   and   x  :: "'a"
  1314   and   X  :: "'a set"
  1315   assumes pt: "pt TYPE('a) TYPE('x)"
  1316   and     at: "at TYPE('x)"
  1317   and     a:  "x\<in>((rev pi)\<bullet>X)"
  1318   shows "(pi\<bullet>x)\<in>X"
  1319   using a by (simp add: pt_set_bij1[OF pt, OF at])
  1320 
  1321 (* FIXME: is this lemma needed anywhere? *)
  1322 lemma pt_set_bij3:
  1323   fixes pi :: "'x prm"
  1324   and   x  :: "'a"
  1325   and   X  :: "'a set"
  1326   shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
  1327 by (simp add: perm_bool)
  1328 
  1329 lemma pt_subseteq_eqvt:
  1330   fixes pi :: "'x prm"
  1331   and   Y  :: "'a set"
  1332   and   X  :: "'a set"
  1333   assumes pt: "pt TYPE('a) TYPE('x)"
  1334   and     at: "at TYPE('x)"
  1335   shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
  1336 by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
  1337 
  1338 lemma pt_set_diff_eqvt:
  1339   fixes X::"'a set"
  1340   and   Y::"'a set"
  1341   and   pi::"'x prm"
  1342   assumes pt: "pt TYPE('a) TYPE('x)"
  1343   and     at: "at TYPE('x)"
  1344   shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
  1345   by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
  1346 
  1347 lemma pt_Collect_eqvt:
  1348   fixes pi::"'x prm"
  1349   assumes pt: "pt TYPE('a) TYPE('x)"
  1350   and     at: "at TYPE('x)"
  1351   shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
  1352 apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
  1353 apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  1354 apply(simp add: pt_pi_rev[OF pt, OF at])
  1355 done
  1356 
  1357 \<comment> "some helper lemmas for the pt_perm_supp_ineq lemma"
  1358 lemma Collect_permI: 
  1359   fixes pi :: "'x prm"
  1360   and   x  :: "'a"
  1361   assumes a: "\<forall>x. (P1 x = P2 x)" 
  1362   shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}"
  1363   using a by force
  1364 
  1365 lemma Infinite_cong:
  1366   assumes a: "X = Y"
  1367   shows "infinite X = infinite Y"
  1368   using a by (simp)
  1369 
  1370 lemma pt_set_eq_ineq:
  1371   fixes pi :: "'y prm"
  1372   assumes pt: "pt TYPE('x) TYPE('y)"
  1373   and     at: "at TYPE('y)"
  1374   shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}"
  1375   by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  1376 
  1377 lemma pt_inject_on_ineq:
  1378   fixes X  :: "'y set"
  1379   and   pi :: "'x prm"
  1380   assumes pt: "pt TYPE('y) TYPE('x)"
  1381   and     at: "at TYPE('x)"
  1382   shows "inj_on (perm pi) X"
  1383 proof (unfold inj_on_def, intro strip)
  1384   fix x::"'y" and y::"'y"
  1385   assume "pi\<bullet>x = pi\<bullet>y"
  1386   thus "x=y" by (simp add: pt_bij[OF pt, OF at])
  1387 qed
  1388 
  1389 lemma pt_set_finite_ineq: 
  1390   fixes X  :: "'x set"
  1391   and   pi :: "'y prm"
  1392   assumes pt: "pt TYPE('x) TYPE('y)"
  1393   and     at: "at TYPE('y)"
  1394   shows "finite (pi\<bullet>X) = finite X"
  1395 proof -
  1396   have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
  1397   show ?thesis
  1398   proof (rule iffI)
  1399     assume "finite (pi\<bullet>X)"
  1400     hence "finite (perm pi ` X)" using image by (simp)
  1401     thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
  1402   next
  1403     assume "finite X"
  1404     hence "finite (perm pi ` X)" by (rule finite_imageI)
  1405     thus "finite (pi\<bullet>X)" using image by (simp)
  1406   qed
  1407 qed
  1408 
  1409 lemma pt_set_infinite_ineq: 
  1410   fixes X  :: "'x set"
  1411   and   pi :: "'y prm"
  1412   assumes pt: "pt TYPE('x) TYPE('y)"
  1413   and     at: "at TYPE('y)"
  1414   shows "infinite (pi\<bullet>X) = infinite X"
  1415 using pt at by (simp add: pt_set_finite_ineq)
  1416 
  1417 lemma pt_perm_supp_ineq:
  1418   fixes  pi  :: "'x prm"
  1419   and    x   :: "'a"
  1420   assumes pta: "pt TYPE('a) TYPE('x)"
  1421   and     ptb: "pt TYPE('y) TYPE('x)"
  1422   and     at:  "at TYPE('x)"
  1423   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1424   shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
  1425 proof -
  1426   have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
  1427   also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
  1428   proof (rule Collect_permI, rule allI, rule iffI)
  1429     fix a
  1430     assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
  1431     hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1432     thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
  1433   next
  1434     fix a
  1435     assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
  1436     hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
  1437     thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
  1438       by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1439   qed
  1440   also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 
  1441     by (simp add: pt_set_eq_ineq[OF ptb, OF at])
  1442   also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1443     by (simp add: pt_bij[OF pta, OF at])
  1444   also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1445   proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
  1446     fix a::"'y" and b::"'y"
  1447     have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
  1448       by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
  1449     thus "(pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq>  pi\<bullet>x) = ([(a,b)]\<bullet>(pi\<bullet>x) \<noteq> pi\<bullet>x)" by simp
  1450   qed
  1451   finally show "?LHS = ?RHS" by (simp add: supp_def) 
  1452 qed
  1453 
  1454 lemma pt_perm_supp:
  1455   fixes  pi  :: "'x prm"
  1456   and    x   :: "'a"
  1457   assumes pt: "pt TYPE('a) TYPE('x)"
  1458   and     at: "at TYPE('x)"
  1459   shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
  1460 apply(rule pt_perm_supp_ineq)
  1461 apply(rule pt)
  1462 apply(rule at_pt_inst)
  1463 apply(rule at)+
  1464 apply(rule cp_pt_inst)
  1465 apply(rule pt)
  1466 apply(rule at)
  1467 done
  1468 
  1469 lemma pt_supp_finite_pi:
  1470   fixes  pi  :: "'x prm"
  1471   and    x   :: "'a"
  1472   assumes pt: "pt TYPE('a) TYPE('x)"
  1473   and     at: "at TYPE('x)"
  1474   and     f: "finite ((supp x)::'x set)"
  1475   shows "finite ((supp (pi\<bullet>x))::'x set)"
  1476 apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
  1477 apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
  1478 apply(rule f)
  1479 done
  1480 
  1481 lemma pt_fresh_left_ineq:  
  1482   fixes  pi :: "'x prm"
  1483   and     x :: "'a"
  1484   and     a :: "'y"
  1485   assumes pta: "pt TYPE('a) TYPE('x)"
  1486   and     ptb: "pt TYPE('y) TYPE('x)"
  1487   and     at:  "at TYPE('x)"
  1488   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1489   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1490 apply(simp add: fresh_def)
  1491 apply(simp add: pt_set_bij1[OF ptb, OF at])
  1492 apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1493 done
  1494 
  1495 lemma pt_fresh_right_ineq:  
  1496   fixes  pi :: "'x prm"
  1497   and     x :: "'a"
  1498   and     a :: "'y"
  1499   assumes pta: "pt TYPE('a) TYPE('x)"
  1500   and     ptb: "pt TYPE('y) TYPE('x)"
  1501   and     at:  "at TYPE('x)"
  1502   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1503   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1504 apply(simp add: fresh_def)
  1505 apply(simp add: pt_set_bij1[OF ptb, OF at])
  1506 apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1507 done
  1508 
  1509 lemma pt_fresh_bij_ineq:
  1510   fixes  pi :: "'x prm"
  1511   and     x :: "'a"
  1512   and     a :: "'y"
  1513   assumes pta: "pt TYPE('a) TYPE('x)"
  1514   and     ptb: "pt TYPE('y) TYPE('x)"
  1515   and     at:  "at TYPE('x)"
  1516   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1517   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1518 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  1519 apply(simp add: pt_rev_pi[OF ptb, OF at])
  1520 done
  1521 
  1522 lemma pt_fresh_left:  
  1523   fixes  pi :: "'x prm"
  1524   and     x :: "'a"
  1525   and     a :: "'x"
  1526   assumes pt: "pt TYPE('a) TYPE('x)"
  1527   and     at: "at TYPE('x)"
  1528   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1529 apply(rule pt_fresh_left_ineq)
  1530 apply(rule pt)
  1531 apply(rule at_pt_inst)
  1532 apply(rule at)+
  1533 apply(rule cp_pt_inst)
  1534 apply(rule pt)
  1535 apply(rule at)
  1536 done
  1537 
  1538 lemma pt_fresh_right:  
  1539   fixes  pi :: "'x prm"
  1540   and     x :: "'a"
  1541   and     a :: "'x"
  1542   assumes pt: "pt TYPE('a) TYPE('x)"
  1543   and     at: "at TYPE('x)"
  1544   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1545 apply(rule pt_fresh_right_ineq)
  1546 apply(rule pt)
  1547 apply(rule at_pt_inst)
  1548 apply(rule at)+
  1549 apply(rule cp_pt_inst)
  1550 apply(rule pt)
  1551 apply(rule at)
  1552 done
  1553 
  1554 lemma pt_fresh_bij:
  1555   fixes  pi :: "'x prm"
  1556   and     x :: "'a"
  1557   and     a :: "'x"
  1558   assumes pt: "pt TYPE('a) TYPE('x)"
  1559   and     at: "at TYPE('x)"
  1560   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1561 apply(rule pt_fresh_bij_ineq)
  1562 apply(rule pt)
  1563 apply(rule at_pt_inst)
  1564 apply(rule at)+
  1565 apply(rule cp_pt_inst)
  1566 apply(rule pt)
  1567 apply(rule at)
  1568 done
  1569 
  1570 lemma pt_fresh_bij1:
  1571   fixes  pi :: "'x prm"
  1572   and     x :: "'a"
  1573   and     a :: "'x"
  1574   assumes pt: "pt TYPE('a) TYPE('x)"
  1575   and     at: "at TYPE('x)"
  1576   and     a:  "a\<sharp>x"
  1577   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
  1578 using a by (simp add: pt_fresh_bij[OF pt, OF at])
  1579 
  1580 lemma pt_fresh_bij2:
  1581   fixes  pi :: "'x prm"
  1582   and     x :: "'a"
  1583   and     a :: "'x"
  1584   assumes pt: "pt TYPE('a) TYPE('x)"
  1585   and     at: "at TYPE('x)"
  1586   and     a:  "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
  1587   shows  "a\<sharp>x"
  1588 using a by (simp add: pt_fresh_bij[OF pt, OF at])
  1589 
  1590 lemma pt_fresh_eqvt:
  1591   fixes  pi :: "'x prm"
  1592   and     x :: "'a"
  1593   and     a :: "'x"
  1594   assumes pt: "pt TYPE('a) TYPE('x)"
  1595   and     at: "at TYPE('x)"
  1596   shows "pi\<bullet>(a\<sharp>x) = (pi\<bullet>a)\<sharp>(pi\<bullet>x)"
  1597   by (simp add: perm_bool pt_fresh_bij[OF pt, OF at])
  1598 
  1599 lemma pt_perm_fresh1:
  1600   fixes a :: "'x"
  1601   and   b :: "'x"
  1602   and   x :: "'a"
  1603   assumes pt: "pt TYPE('a) TYPE('x)"
  1604   and     at: "at TYPE ('x)"
  1605   and     a1: "\<not>(a\<sharp>x)"
  1606   and     a2: "b\<sharp>x"
  1607   shows "[(a,b)]\<bullet>x \<noteq> x"
  1608 proof
  1609   assume neg: "[(a,b)]\<bullet>x = x"
  1610   from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 
  1611   from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 
  1612   from a1' a2' have a3: "a\<noteq>b" by force
  1613   from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
  1614     by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
  1615   hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_calc[OF at])
  1616   hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
  1617   with a2' neg show False by simp
  1618 qed
  1619 
  1620 (* the next two lemmas are needed in the proof *)
  1621 (* of the structural induction principle       *)
  1622 lemma pt_fresh_aux:
  1623   fixes a::"'x"
  1624   and   b::"'x"
  1625   and   c::"'x"
  1626   and   x::"'a"
  1627   assumes pt: "pt TYPE('a) TYPE('x)"
  1628   and     at: "at TYPE ('x)"
  1629   assumes a1: "c\<noteq>a" and  a2: "a\<sharp>x" and a3: "c\<sharp>x"
  1630   shows "c\<sharp>([(a,b)]\<bullet>x)"
  1631 using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
  1632 
  1633 lemma pt_fresh_perm_app:
  1634   fixes pi :: "'x prm" 
  1635   and   a  :: "'x"
  1636   and   x  :: "'y"
  1637   assumes pt: "pt TYPE('y) TYPE('x)"
  1638   and     at: "at TYPE('x)"
  1639   and     h1: "a\<sharp>pi"
  1640   and     h2: "a\<sharp>x"
  1641   shows "a\<sharp>(pi\<bullet>x)"
  1642 using assms
  1643 proof -
  1644   have "a\<sharp>(rev pi)"using h1 by (simp add: fresh_list_rev)
  1645   then have "(rev pi)\<bullet>a = a" by (simp add: at_prm_fresh[OF at])
  1646   then have "((rev pi)\<bullet>a)\<sharp>x" using h2 by simp
  1647   thus "a\<sharp>(pi\<bullet>x)"  by (simp add: pt_fresh_right[OF pt, OF at])
  1648 qed
  1649 
  1650 lemma pt_fresh_perm_app_ineq:
  1651   fixes pi::"'x prm"
  1652   and   c::"'y"
  1653   and   x::"'a"
  1654   assumes pta: "pt TYPE('a) TYPE('x)"
  1655   and     ptb: "pt TYPE('y) TYPE('x)"
  1656   and     at:  "at TYPE('x)"
  1657   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1658   and     dj:  "disjoint TYPE('y) TYPE('x)"
  1659   assumes a: "c\<sharp>x"
  1660   shows "c\<sharp>(pi\<bullet>x)"
  1661 using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])
  1662 
  1663 lemma pt_fresh_eqvt_ineq:
  1664   fixes pi::"'x prm"
  1665   and   c::"'y"
  1666   and   x::"'a"
  1667   assumes pta: "pt TYPE('a) TYPE('x)"
  1668   and     ptb: "pt TYPE('y) TYPE('x)"
  1669   and     at:  "at TYPE('x)"
  1670   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1671   and     dj:  "disjoint TYPE('y) TYPE('x)"
  1672   shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)"
  1673 by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
  1674 
  1675 \<comment>"the co-set of a finite set is infinte"
  1676 lemma finite_infinite:
  1677   assumes a: "finite {b::'x. P b}"
  1678   and     b: "infinite (UNIV::'x set)"        
  1679   shows "infinite {b. \<not>P b}"
  1680 proof -
  1681   from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite)
  1682   moreover 
  1683   have "{b::'x. \<not>P b} = UNIV - {b::'x. P b}" by auto
  1684   ultimately show "infinite {b::'x. \<not>P b}" by simp
  1685 qed 
  1686 
  1687 lemma pt_fresh_fresh:
  1688   fixes   x :: "'a"
  1689   and     a :: "'x"
  1690   and     b :: "'x"
  1691   assumes pt: "pt TYPE('a) TYPE('x)"
  1692   and     at: "at TYPE ('x)"
  1693   and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
  1694   shows "[(a,b)]\<bullet>x=x"
  1695 proof (cases "a=b")
  1696   assume "a=b"
  1697   hence "[(a,b)] \<triangleq> []" by (simp add: at_ds1[OF at])
  1698   hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
  1699   thus ?thesis by (simp only: pt1[OF pt])
  1700 next
  1701   assume c2: "a\<noteq>b"
  1702   from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1703   from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1704   from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 
  1705     by (force simp only: Collect_disj_eq)
  1706   have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 
  1707     by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
  1708   hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
  1709     by (force dest: Diff_infinite_finite)
  1710   hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
  1711     by (metis finite_set set_empty2)
  1712   hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
  1713   then obtain c 
  1714     where eq1: "[(a,c)]\<bullet>x = x" 
  1715       and eq2: "[(b,c)]\<bullet>x = x" 
  1716       and ineq: "a\<noteq>c \<and> b\<noteq>c"
  1717     by (force)
  1718   hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
  1719   hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
  1720   from c2 ineq have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" by (simp add: at_ds3[OF at])
  1721   hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
  1722   thus ?thesis using eq3 by simp
  1723 qed
  1724 
  1725 lemma pt_pi_fresh_fresh:
  1726   fixes   x :: "'a"
  1727   and     pi :: "'x prm"
  1728   assumes pt: "pt TYPE('a) TYPE('x)"
  1729   and     at: "at TYPE ('x)"
  1730   and     a:  "\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x" 
  1731   shows "pi\<bullet>x=x"
  1732 using a
  1733 proof (induct pi)
  1734   case Nil
  1735   show "([]::'x prm)\<bullet>x = x" by (rule pt1[OF pt])
  1736 next
  1737   case (Cons ab pi)
  1738   have a: "\<forall>(a,b)\<in>set (ab#pi). a\<sharp>x \<and> b\<sharp>x" by fact
  1739   have ih: "(\<forall>(a,b)\<in>set pi. a\<sharp>x \<and> b\<sharp>x) \<Longrightarrow> pi\<bullet>x=x" by fact
  1740   obtain a b where e: "ab=(a,b)" by (cases ab) (auto)
  1741   from a have a': "a\<sharp>x" "b\<sharp>x" using e by auto
  1742   have "(ab#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x" using e by simp
  1743   also have "\<dots> = [(a,b)]\<bullet>(pi\<bullet>x)" by (simp only: pt2[OF pt])
  1744   also have "\<dots> = [(a,b)]\<bullet>x" using ih a by simp
  1745   also have "\<dots> = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at])
  1746   finally show "(ab#pi)\<bullet>x = x" by simp
  1747 qed
  1748 
  1749 lemma pt_perm_compose:
  1750   fixes pi1 :: "'x prm"
  1751   and   pi2 :: "'x prm"
  1752   and   x  :: "'a"
  1753   assumes pt: "pt TYPE('a) TYPE('x)"
  1754   and     at: "at TYPE('x)"
  1755   shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
  1756 proof -
  1757   have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8 [OF at])
  1758   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
  1759   thus ?thesis by (simp add: pt2[OF pt])
  1760 qed
  1761 
  1762 lemma pt_perm_compose':
  1763   fixes pi1 :: "'x prm"
  1764   and   pi2 :: "'x prm"
  1765   and   x  :: "'a"
  1766   assumes pt: "pt TYPE('a) TYPE('x)"
  1767   and     at: "at TYPE('x)"
  1768   shows "(pi2\<bullet>pi1)\<bullet>x = pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x))" 
  1769 proof -
  1770   have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>((rev pi2)\<bullet>x))"
  1771     by (rule pt_perm_compose[OF pt, OF at])
  1772   also have "\<dots> = (pi2\<bullet>pi1)\<bullet>x" by (simp add: pt_pi_rev[OF pt, OF at])
  1773   finally have "pi2\<bullet>(pi1\<bullet>((rev pi2)\<bullet>x)) = (pi2\<bullet>pi1)\<bullet>x" by simp
  1774   thus ?thesis by simp
  1775 qed
  1776 
  1777 lemma pt_perm_compose_rev:
  1778   fixes pi1 :: "'x prm"
  1779   and   pi2 :: "'x prm"
  1780   and   x  :: "'a"
  1781   assumes pt: "pt TYPE('a) TYPE('x)"
  1782   and     at: "at TYPE('x)"
  1783   shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
  1784 proof -
  1785   have "((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
  1786   hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
  1787   thus ?thesis by (simp add: pt2[OF pt])
  1788 qed
  1789 
  1790 section \<open>equivariance for some connectives\<close>
  1791 lemma pt_all_eqvt:
  1792   fixes  pi :: "'x prm"
  1793   and     x :: "'a"
  1794   assumes pt: "pt TYPE('a) TYPE('x)"
  1795   and     at: "at TYPE('x)"
  1796   shows "pi\<bullet>(\<forall>(x::'a). P x) = (\<forall>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
  1797 apply(auto simp add: perm_bool perm_fun_def)
  1798 apply(drule_tac x="pi\<bullet>x" in spec)
  1799 apply(simp add: pt_rev_pi[OF pt, OF at])
  1800 done
  1801 
  1802 lemma pt_ex_eqvt:
  1803   fixes  pi :: "'x prm"
  1804   and     x :: "'a"
  1805   assumes pt: "pt TYPE('a) TYPE('x)"
  1806   and     at: "at TYPE('x)"
  1807   shows "pi\<bullet>(\<exists>(x::'a). P x) = (\<exists>(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
  1808 apply(auto simp add: perm_bool perm_fun_def)
  1809 apply(rule_tac x="pi\<bullet>x" in exI) 
  1810 apply(simp add: pt_rev_pi[OF pt, OF at])
  1811 done
  1812 
  1813 lemma pt_ex1_eqvt:
  1814   fixes  pi :: "'x prm"
  1815   and     x :: "'a"
  1816   assumes pt: "pt TYPE('a) TYPE('x)"
  1817   and     at: "at TYPE('x)"
  1818   shows  "(pi\<bullet>(\<exists>!x. P (x::'a))) = (\<exists>!x. pi\<bullet>(P (rev pi\<bullet>x)))"
  1819 unfolding Ex1_def
  1820 by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] 
  1821               imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at])
  1822 
  1823 lemma pt_the_eqvt:
  1824   fixes  pi :: "'x prm"
  1825   assumes pt: "pt TYPE('a) TYPE('x)"
  1826   and     at: "at TYPE('x)"
  1827   and     unique: "\<exists>!x. P x"
  1828   shows "pi\<bullet>(THE(x::'a). P x) = (THE(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
  1829   apply(rule the1_equality [symmetric])
  1830   apply(simp add: pt_ex1_eqvt[OF pt at,symmetric])
  1831   apply(simp add: perm_bool unique)
  1832   apply(simp add: perm_bool pt_rev_pi [OF pt at])
  1833   apply(rule theI'[OF unique])
  1834   done
  1835 
  1836 section \<open>facts about supports\<close>
  1837 (*==============================*)
  1838 
  1839 lemma supports_subset:
  1840   fixes x  :: "'a"
  1841   and   S1 :: "'x set"
  1842   and   S2 :: "'x set"
  1843   assumes  a: "S1 supports x"
  1844   and      b: "S1 \<subseteq> S2"
  1845   shows "S2 supports x"
  1846   using a b
  1847   by (force simp add: supports_def)
  1848 
  1849 lemma supp_is_subset:
  1850   fixes S :: "'x set"
  1851   and   x :: "'a"
  1852   assumes a1: "S supports x"
  1853   and     a2: "finite S"
  1854   shows "(supp x)\<subseteq>S"
  1855 proof (rule ccontr)
  1856   assume "\<not>(supp x \<subseteq> S)"
  1857   hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
  1858   then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
  1859   from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold supports_def, force)
  1860   hence "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by force
  1861   with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
  1862   hence "a\<notin>(supp x)" by (unfold supp_def, auto)
  1863   with b1 show False by simp
  1864 qed
  1865 
  1866 lemma supp_supports:
  1867   fixes x :: "'a"
  1868   assumes  pt: "pt TYPE('a) TYPE('x)"
  1869   and      at: "at TYPE ('x)"
  1870   shows "((supp x)::'x set) supports x"
  1871 proof (unfold supports_def, intro strip)
  1872   fix a b
  1873   assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
  1874   hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
  1875   thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
  1876 qed
  1877 
  1878 lemma supports_finite:
  1879   fixes S :: "'x set"
  1880   and   x :: "'a"
  1881   assumes a1: "S supports x"
  1882   and     a2: "finite S"
  1883   shows "finite ((supp x)::'x set)"
  1884 proof -
  1885   have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1886   thus ?thesis using a2 by (simp add: finite_subset)
  1887 qed
  1888   
  1889 lemma supp_is_inter:
  1890   fixes  x :: "'a"
  1891   assumes  pt: "pt TYPE('a) TYPE('x)"
  1892   and      at: "at TYPE ('x)"
  1893   and      fs: "fs TYPE('a) TYPE('x)"
  1894   shows "((supp x)::'x set) = (\<Inter>{S. finite S \<and> S supports x})"
  1895 proof (rule equalityI)
  1896   show "((supp x)::'x set) \<subseteq> (\<Inter>{S. finite S \<and> S supports x})"
  1897   proof (clarify)
  1898     fix S c
  1899     assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
  1900     hence  "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 
  1901     with b show "c\<in>S" by force
  1902   qed
  1903 next
  1904   show "(\<Inter>{S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
  1905   proof (clarify, simp)
  1906     fix c
  1907     assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
  1908     have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1909     with d fs1[OF fs] show "c\<in>supp x" by force
  1910   qed
  1911 qed
  1912     
  1913 lemma supp_is_least_supports:
  1914   fixes S :: "'x set"
  1915   and   x :: "'a"
  1916   assumes  pt: "pt TYPE('a) TYPE('x)"
  1917   and      at: "at TYPE ('x)"
  1918   and      a1: "S supports x"
  1919   and      a2: "finite S"
  1920   and      a3: "\<forall>S'. (S' supports x) \<longrightarrow> S\<subseteq>S'"
  1921   shows "S = (supp x)"
  1922 proof (rule equalityI)
  1923   show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1924 next
  1925   have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1926   with a3 show "S\<subseteq>supp x" by force
  1927 qed
  1928 
  1929 lemma supports_set:
  1930   fixes S :: "'x set"
  1931   and   X :: "'a set"
  1932   assumes  pt: "pt TYPE('a) TYPE('x)"
  1933   and      at: "at TYPE ('x)"
  1934   and      a: "\<forall>x\<in>X. (\<forall>(a::'x) (b::'x). a\<notin>S\<and>b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x)\<in>X)"
  1935   shows  "S supports X"
  1936 using a
  1937 apply(auto simp add: supports_def)
  1938 apply(simp add: pt_set_bij1a[OF pt, OF at])
  1939 apply(force simp add: pt_swap_bij[OF pt, OF at])
  1940 apply(simp add: pt_set_bij1a[OF pt, OF at])
  1941 done
  1942 
  1943 lemma supports_fresh:
  1944   fixes S :: "'x set"
  1945   and   a :: "'x"
  1946   and   x :: "'a"
  1947   assumes a1: "S supports x"
  1948   and     a2: "finite S"
  1949   and     a3: "a\<notin>S"
  1950   shows "a\<sharp>x"
  1951 proof (simp add: fresh_def)
  1952   have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1953   thus "a\<notin>(supp x)" using a3 by force
  1954 qed
  1955 
  1956 lemma at_fin_set_supports:
  1957   fixes X::"'x set"
  1958   assumes at: "at TYPE('x)"
  1959   shows "X supports X"
  1960 proof -
  1961   have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X"
  1962     by (auto simp add: perm_set_def at_calc[OF at])
  1963   then show ?thesis by (simp add: supports_def)
  1964 qed
  1965 
  1966 lemma infinite_Collection:
  1967   assumes a1:"infinite X"
  1968   and     a2:"\<forall>b\<in>X. P(b)"
  1969   shows "infinite {b\<in>X. P(b)}"
  1970   using a1 a2 
  1971   apply auto
  1972   apply (subgoal_tac "infinite (X - {b\<in>X. P b})")
  1973   apply (simp add: set_diff_eq)
  1974   apply (simp add: Diff_infinite_finite)
  1975   done
  1976 
  1977 lemma at_fin_set_supp:
  1978   fixes X::"'x set" 
  1979   assumes at: "at TYPE('x)"
  1980   and     fs: "finite X"
  1981   shows "(supp X) = X"
  1982 proof (rule subset_antisym)
  1983   show "(supp X) \<subseteq> X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset)
  1984 next
  1985   have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
  1986   { fix a::"'x"
  1987     assume asm: "a\<in>X"
  1988     hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X"
  1989       by (auto simp add: perm_set_def at_calc[OF at])
  1990     with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection)
  1991     hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto)
  1992     hence "a\<in>(supp X)" by (simp add: supp_def)
  1993   }
  1994   then show "X\<subseteq>(supp X)" by blast
  1995 qed
  1996 
  1997 lemma at_fin_set_fresh:
  1998   fixes X::"'x set" 
  1999   assumes at: "at TYPE('x)"
  2000   and     fs: "finite X"
  2001   shows "(x \<sharp> X) = (x \<notin> X)"
  2002   by (simp add: at_fin_set_supp fresh_def at fs)
  2003 
  2004 
  2005 section \<open>Permutations acting on Functions\<close>
  2006 (*==========================================*)
  2007 
  2008 lemma pt_fun_app_eq:
  2009   fixes f  :: "'a\<Rightarrow>'b"
  2010   and   x  :: "'a"
  2011   and   pi :: "'x prm"
  2012   assumes pt: "pt TYPE('a) TYPE('x)"
  2013   and     at: "at TYPE('x)"
  2014   shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)"
  2015   by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
  2016 
  2017 
  2018 \<comment>"sometimes pt_fun_app_eq does too much; this lemma 'corrects it'"
  2019 lemma pt_perm:
  2020   fixes x  :: "'a"
  2021   and   pi1 :: "'x prm"
  2022   and   pi2 :: "'x prm"
  2023   assumes pt: "pt TYPE('a) TYPE('x)"
  2024   and     at: "at TYPE ('x)"
  2025   shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 
  2026   by (simp add: pt_fun_app_eq[OF pt, OF at])
  2027 
  2028 
  2029 lemma pt_fun_eq:
  2030   fixes f  :: "'a\<Rightarrow>'b"
  2031   and   pi :: "'x prm"
  2032   assumes pt: "pt TYPE('a) TYPE('x)"
  2033   and     at: "at TYPE('x)"
  2034   shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS")
  2035 proof
  2036   assume a: "?LHS"
  2037   show "?RHS"
  2038   proof
  2039     fix x
  2040     have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
  2041     also have "\<dots> = f (pi\<bullet>x)" using a by simp
  2042     finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp
  2043   qed
  2044 next
  2045   assume b: "?RHS"
  2046   show "?LHS"
  2047   proof (rule ccontr)
  2048     assume "(pi\<bullet>f) \<noteq> f"
  2049     hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: fun_eq_iff)
  2050     then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
  2051     from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
  2052     hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" 
  2053       by (simp add: pt_fun_app_eq[OF pt, OF at])
  2054     hence "(pi\<bullet>f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])
  2055     with b1 show "False" by simp
  2056   qed
  2057 qed
  2058 
  2059 \<comment> "two helper lemmas for the equivariance of functions"
  2060 lemma pt_swap_eq_aux:
  2061   fixes   y :: "'a"
  2062   and    pi :: "'x prm"
  2063   assumes pt: "pt TYPE('a) TYPE('x)"
  2064   and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
  2065   shows "pi\<bullet>y = y"
  2066 proof(induct pi)
  2067   case Nil show ?case by (simp add: pt1[OF pt])
  2068 next
  2069   case (Cons x xs)
  2070   have ih: "xs\<bullet>y = y" by fact
  2071   obtain a b where p: "x=(a,b)" by force
  2072   have "((a,b)#xs)\<bullet>y = ([(a,b)]@xs)\<bullet>y" by simp
  2073   also have "\<dots> = [(a,b)]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
  2074   finally show ?case using a ih p by simp
  2075 qed
  2076 
  2077 lemma pt_swap_eq:
  2078   fixes   y :: "'a"
  2079   assumes pt: "pt TYPE('a) TYPE('x)"
  2080   shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)"
  2081   by (force intro: pt_swap_eq_aux[OF pt])
  2082 
  2083 lemma pt_eqvt_fun1a:
  2084   fixes f     :: "'a\<Rightarrow>'b"
  2085   assumes pta: "pt TYPE('a) TYPE('x)"
  2086   and     ptb: "pt TYPE('b) TYPE('x)"
  2087   and     at:  "at TYPE('x)"
  2088   and     a:   "((supp f)::'x set)={}"
  2089   shows "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  2090 proof (intro strip)
  2091   fix pi
  2092   have "\<forall>a b. a\<notin>((supp f)::'x set) \<and> b\<notin>((supp f)::'x set) \<longrightarrow> (([(a,b)]\<bullet>f) = f)" 
  2093     by (intro strip, fold fresh_def, 
  2094       simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at])
  2095   with a have "\<forall>(a::'x) (b::'x). ([(a,b)]\<bullet>f) = f" by force
  2096   hence "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  2097     by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]])
  2098   thus "(pi::'x prm)\<bullet>f = f" by simp
  2099 qed
  2100 
  2101 lemma pt_eqvt_fun1b:
  2102   fixes f     :: "'a\<Rightarrow>'b"
  2103   assumes a: "\<forall>(pi::'x prm). pi\<bullet>f = f"
  2104   shows "((supp f)::'x set)={}"
  2105 using a by (simp add: supp_def)
  2106 
  2107 lemma pt_eqvt_fun1:
  2108   fixes f     :: "'a\<Rightarrow>'b"
  2109   assumes pta: "pt TYPE('a) TYPE('x)"
  2110   and     ptb: "pt TYPE('b) TYPE('x)"
  2111   and     at: "at TYPE('x)"
  2112   shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS")
  2113 by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)
  2114 
  2115 lemma pt_eqvt_fun2a:
  2116   fixes f     :: "'a\<Rightarrow>'b"
  2117   assumes pta: "pt TYPE('a) TYPE('x)"
  2118   and     ptb: "pt TYPE('b) TYPE('x)"
  2119   and     at: "at TYPE('x)"
  2120   assumes a: "((supp f)::'x set)={}"
  2121   shows "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)" 
  2122 proof (intro strip)
  2123   fix pi x
  2124   from a have b: "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) 
  2125   have "(pi::'x prm)\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 
  2126   with b show "(pi::'x prm)\<bullet>(f x) = f (pi\<bullet>x)" by force 
  2127 qed
  2128 
  2129 lemma pt_eqvt_fun2b:
  2130   fixes f     :: "'a\<Rightarrow>'b"
  2131   assumes pt1: "pt TYPE('a) TYPE('x)"
  2132   and     pt2: "pt TYPE('b) TYPE('x)"
  2133   and     at: "at TYPE('x)"
  2134   assumes a: "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)"
  2135   shows "((supp f)::'x set)={}"
  2136 proof -
  2137   from a have "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric])
  2138   thus ?thesis by (simp add: supp_def)
  2139 qed
  2140 
  2141 lemma pt_eqvt_fun2:
  2142   fixes f     :: "'a\<Rightarrow>'b"
  2143   assumes pta: "pt TYPE('a) TYPE('x)"
  2144   and     ptb: "pt TYPE('b) TYPE('x)"
  2145   and     at: "at TYPE('x)"
  2146   shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))" 
  2147 by (rule iffI, 
  2148     simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], 
  2149     simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])
  2150 
  2151 lemma pt_supp_fun_subset:
  2152   fixes f :: "'a\<Rightarrow>'b"
  2153   assumes pta: "pt TYPE('a) TYPE('x)"
  2154   and     ptb: "pt TYPE('b) TYPE('x)"
  2155   and     at: "at TYPE('x)" 
  2156   and     f1: "finite ((supp f)::'x set)"
  2157   and     f2: "finite ((supp x)::'x set)"
  2158   shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
  2159 proof -
  2160   have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
  2161   proof (simp add: supports_def, fold fresh_def, auto)
  2162     fix a::"'x" and b::"'x"
  2163     assume "a\<sharp>f" and "b\<sharp>f"
  2164     hence a1: "[(a,b)]\<bullet>f = f" 
  2165       by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at])
  2166     assume "a\<sharp>x" and "b\<sharp>x"
  2167     hence a2: "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pta, OF at])
  2168     from a1 a2 show "[(a,b)]\<bullet>(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
  2169   qed
  2170   from f1 f2 have "finite ((supp f)\<union>((supp x)::'x set))" by force
  2171   with s1 show ?thesis by (rule supp_is_subset)
  2172 qed
  2173       
  2174 lemma pt_empty_supp_fun_subset:
  2175   fixes f :: "'a\<Rightarrow>'b"
  2176   assumes pta: "pt TYPE('a) TYPE('x)"
  2177   and     ptb: "pt TYPE('b) TYPE('x)"
  2178   and     at:  "at TYPE('x)" 
  2179   and     e:   "(supp f)=({}::'x set)"
  2180   shows "supp (f x) \<subseteq> ((supp x)::'x set)"
  2181 proof (unfold supp_def, auto)
  2182   fix a::"'x"
  2183   assume a1: "finite {b. [(a, b)]\<bullet>x \<noteq> x}"
  2184   assume "infinite {b. [(a, b)]\<bullet>(f x) \<noteq> f x}"
  2185   hence a2: "infinite {b. f ([(a, b)]\<bullet>x) \<noteq> f x}" using e
  2186     by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at])
  2187   have a3: "{b. f ([(a,b)]\<bullet>x) \<noteq> f x}\<subseteq>{b. [(a,b)]\<bullet>x \<noteq> x}" by force
  2188   from a1 a2 a3 show False by (force dest: finite_subset)
  2189 qed
  2190 
  2191 section \<open>Facts about the support of finite sets of finitely supported things\<close>
  2192 (*=============================================================================*)
  2193 
  2194 definition X_to_Un_supp :: "('a set) \<Rightarrow> 'x set" where
  2195   "X_to_Un_supp X \<equiv> \<Union>x\<in>X. ((supp x)::'x set)"
  2196 
  2197 lemma UNION_f_eqvt:
  2198   fixes X::"('a set)"
  2199   and   f::"'a \<Rightarrow> 'x set"
  2200   and   pi::"'x prm"
  2201   assumes pt: "pt TYPE('a) TYPE('x)"
  2202   and     at: "at TYPE('x)"
  2203   shows "pi\<bullet>(\<Union>x\<in>X. f x) = (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
  2204 proof -
  2205   have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
  2206   show ?thesis
  2207   proof (rule equalityI)
  2208     show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
  2209       apply(auto simp add: perm_set_def)
  2210       apply(rule_tac x="pi\<bullet>xb" in exI)
  2211       apply(rule conjI)
  2212       apply(rule_tac x="xb" in exI)
  2213       apply(simp)
  2214       apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xb) = pi\<bullet>(f xb)")(*A*)
  2215       apply(simp)
  2216       apply(rule pt_set_bij2[OF pt_x, OF at])
  2217       apply(assumption)
  2218       (*A*)
  2219       apply(rule sym)
  2220       apply(rule pt_fun_app_eq[OF pt, OF at])
  2221       done
  2222   next
  2223     show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
  2224       apply(auto simp add: perm_set_def)
  2225       apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  2226       apply(rule conjI)
  2227       apply(simp add: pt_pi_rev[OF pt_x, OF at])
  2228       apply(rule_tac x="xb" in bexI)
  2229       apply(simp add: pt_set_bij1[OF pt_x, OF at])
  2230       apply(simp add: pt_fun_app_eq[OF pt, OF at])
  2231       apply(assumption)
  2232       done
  2233   qed
  2234 qed
  2235 
  2236 lemma X_to_Un_supp_eqvt:
  2237   fixes X::"('a set)"
  2238   and   pi::"'x prm"
  2239   assumes pt: "pt TYPE('a) TYPE('x)"
  2240   and     at: "at TYPE('x)"
  2241   shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
  2242   apply(simp add: X_to_Un_supp_def)
  2243   apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
  2244   apply(simp add: pt_perm_supp[OF pt, OF at])
  2245   apply(simp add: pt_pi_rev[OF pt, OF at])
  2246   done
  2247 
  2248 lemma Union_supports_set:
  2249   fixes X::"('a set)"
  2250   assumes pt: "pt TYPE('a) TYPE('x)"
  2251   and     at: "at TYPE('x)"
  2252   shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
  2253   apply(simp add: supports_def fresh_def[symmetric])
  2254   apply(rule allI)+
  2255   apply(rule impI)
  2256   apply(erule conjE)
  2257   apply(simp add: perm_set_def)
  2258   apply(auto)
  2259   apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
  2260   apply(simp)
  2261   apply(rule pt_fresh_fresh[OF pt, OF at])
  2262   apply(force)
  2263   apply(force)
  2264   apply(rule_tac x="x" in exI)
  2265   apply(simp)
  2266   apply(rule sym)
  2267   apply(rule pt_fresh_fresh[OF pt, OF at])
  2268   apply(force)+
  2269   done
  2270 
  2271 lemma Union_of_fin_supp_sets:
  2272   fixes X::"('a set)"
  2273   assumes fs: "fs TYPE('a) TYPE('x)" 
  2274   and     fi: "finite X"   
  2275   shows "finite (\<Union>x\<in>X. ((supp x)::'x set))"
  2276 using fi by (induct, auto simp add: fs1[OF fs])
  2277 
  2278 lemma Union_included_in_supp:
  2279   fixes X::"('a set)"
  2280   assumes pt: "pt TYPE('a) TYPE('x)"
  2281   and     at: "at TYPE('x)"
  2282   and     fs: "fs TYPE('a) TYPE('x)" 
  2283   and     fi: "finite X"
  2284   shows "(\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> supp X"
  2285 proof -
  2286   have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
  2287     apply(rule pt_empty_supp_fun_subset)
  2288     apply(force intro: pt_set_inst at_pt_inst pt at)+
  2289     apply(rule pt_eqvt_fun2b)
  2290     apply(force intro: pt_set_inst at_pt_inst pt at)+
  2291     apply(rule allI)+
  2292     apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
  2293     done
  2294   hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
  2295   moreover
  2296   have "supp (\<Union>x\<in>X. ((supp x)::'x set)) = (\<Union>x\<in>X. ((supp x)::'x set))"
  2297     apply(rule at_fin_set_supp[OF at])
  2298     apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
  2299     done
  2300   ultimately show ?thesis by force
  2301 qed
  2302 
  2303 lemma supp_of_fin_sets:
  2304   fixes X::"('a set)"
  2305   assumes pt: "pt TYPE('a) TYPE('x)"
  2306   and     at: "at TYPE('x)"
  2307   and     fs: "fs TYPE('a) TYPE('x)" 
  2308   and     fi: "finite X"
  2309   shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))"
  2310 apply(rule equalityI)
  2311 apply(rule supp_is_subset)
  2312 apply(rule Union_supports_set[OF pt, OF at])
  2313 apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
  2314 apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi])
  2315 done
  2316 
  2317 lemma supp_fin_union:
  2318   fixes X::"('a set)"
  2319   and   Y::"('a set)"
  2320   assumes pt: "pt TYPE('a) TYPE('x)"
  2321   and     at: "at TYPE('x)"
  2322   and     fs: "fs TYPE('a) TYPE('x)" 
  2323   and     f1: "finite X"
  2324   and     f2: "finite Y"
  2325   shows "(supp (X\<union>Y)) = (supp X)\<union>((supp Y)::'x set)"
  2326 using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs])
  2327 
  2328 lemma supp_fin_insert:
  2329   fixes X::"('a set)"
  2330   and   x::"'a"
  2331   assumes pt: "pt TYPE('a) TYPE('x)"
  2332   and     at: "at TYPE('x)"
  2333   and     fs: "fs TYPE('a) TYPE('x)" 
  2334   and     f:  "finite X"
  2335   shows "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
  2336 proof -
  2337   have "(supp (insert x X)) = ((supp ({x}\<union>(X::'a set)))::'x set)" by simp
  2338   also have "\<dots> = (supp {x})\<union>(supp X)"
  2339     by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
  2340   finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 
  2341     by (simp add: supp_singleton)
  2342 qed
  2343 
  2344 lemma fresh_fin_union:
  2345   fixes X::"('a set)"
  2346   and   Y::"('a set)"
  2347   and   a::"'x"
  2348   assumes pt: "pt TYPE('a) TYPE('x)"
  2349   and     at: "at TYPE('x)"
  2350   and     fs: "fs TYPE('a) TYPE('x)" 
  2351   and     f1: "finite X"
  2352   and     f2: "finite Y"
  2353   shows "a\<sharp>(X\<union>Y) = (a\<sharp>X \<and> a\<sharp>Y)"
  2354 apply(simp add: fresh_def)
  2355 apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2])
  2356 done
  2357 
  2358 lemma fresh_fin_insert:
  2359   fixes X::"('a set)"
  2360   and   x::"'a"
  2361   and   a::"'x"
  2362   assumes pt: "pt TYPE('a) TYPE('x)"
  2363   and     at: "at TYPE('x)"
  2364   and     fs: "fs TYPE('a) TYPE('x)" 
  2365   and     f:  "finite X"
  2366   shows "a\<sharp>(insert x X) = (a\<sharp>x \<and> a\<sharp>X)"
  2367 apply(simp add: fresh_def)
  2368 apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f])
  2369 done
  2370 
  2371 lemma fresh_fin_insert1:
  2372   fixes X::"('a set)"
  2373   and   x::"'a"
  2374   and   a::"'x"
  2375   assumes pt: "pt TYPE('a) TYPE('x)"
  2376   and     at: "at TYPE('x)"
  2377   and     fs: "fs TYPE('a) TYPE('x)" 
  2378   and     f:  "finite X"
  2379   and     a1:  "a\<sharp>x"
  2380   and     a2:  "a\<sharp>X"
  2381   shows "a\<sharp>(insert x X)"
  2382   using a1 a2
  2383   by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
  2384 
  2385 lemma pt_list_set_supp:
  2386   fixes xs :: "'a list"
  2387   assumes pt: "pt TYPE('a) TYPE('x)"
  2388   and     at: "at TYPE('x)"
  2389   and     fs: "fs TYPE('a) TYPE('x)"
  2390   shows "supp (set xs) = ((supp xs)::'x set)"
  2391 proof -
  2392   have "supp (set xs) = (\<Union>x\<in>(set xs). ((supp x)::'x set))"
  2393     by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set)
  2394   also have "(\<Union>x\<in>(set xs). ((supp x)::'x set)) = (supp xs)"
  2395   proof(induct xs)
  2396     case Nil show ?case by (simp add: supp_list_nil)
  2397   next
  2398     case (Cons h t) thus ?case by (simp add: supp_list_cons)
  2399   qed
  2400   finally show ?thesis by simp
  2401 qed
  2402     
  2403 lemma pt_list_set_fresh:
  2404   fixes a :: "'x"
  2405   and   xs :: "'a list"
  2406   assumes pt: "pt TYPE('a) TYPE('x)"
  2407   and     at: "at TYPE('x)"
  2408   and     fs: "fs TYPE('a) TYPE('x)"
  2409   shows "a\<sharp>(set xs) = a\<sharp>xs"
  2410 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
  2411 
  2412 
  2413 section \<open>generalisation of freshness to lists and sets of atoms\<close>
  2414 (*================================================================*)
  2415  
  2416 consts
  2417   fresh_star :: "'b \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp>* _" [100,100] 100)
  2418 
  2419 overloading fresh_star_set \<equiv> "fresh_star :: 'b set \<Rightarrow> 'a \<Rightarrow> bool"
  2420 begin
  2421   definition fresh_star_set: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>xs. x\<sharp>(c::'a)"
  2422 end
  2423 
  2424 overloading frsh_star_list \<equiv> "fresh_star :: 'b list \<Rightarrow> 'a \<Rightarrow> bool"
  2425 begin
  2426   definition fresh_star_list: "xs\<sharp>*c \<equiv> \<forall>x::'b\<in>set xs. x\<sharp>(c::'a)"
  2427 end
  2428 
  2429 lemmas fresh_star_def = fresh_star_list fresh_star_set
  2430 
  2431 lemma fresh_star_prod_set:
  2432   fixes xs::"'a set"
  2433   shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
  2434 by (auto simp add: fresh_star_def fresh_prod)
  2435 
  2436 lemma fresh_star_prod_list:
  2437   fixes xs::"'a list"
  2438   shows "xs\<sharp>*(a,b) = (xs\<sharp>*a \<and> xs\<sharp>*b)"
  2439   by (auto simp add: fresh_star_def fresh_prod)
  2440 
  2441 lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
  2442 
  2443 lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
  2444   by (simp add: fresh_star_def)
  2445 
  2446 lemma fresh_star_Un_elim:
  2447   "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
  2448   apply rule
  2449   apply (simp_all add: fresh_star_def)
  2450   apply (erule meta_mp)
  2451   apply blast
  2452   done
  2453 
  2454 lemma fresh_star_insert_elim:
  2455   "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
  2456   by rule (simp_all add: fresh_star_def)
  2457 
  2458 lemma fresh_star_empty_elim:
  2459   "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
  2460   by (simp add: fresh_star_def)
  2461 
  2462 text \<open>Normalization of freshness results; see \ \<open>nominal_induct\<close>\<close>
  2463 
  2464 lemma fresh_star_unit_elim: 
  2465   shows "((a::'a set)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
  2466   and "((b::'a list)\<sharp>*() \<Longrightarrow> PROP C) \<equiv> PROP C"
  2467   by (simp_all add: fresh_star_def fresh_def supp_unit)
  2468 
  2469 lemma fresh_star_prod_elim: 
  2470   shows "((a::'a set)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>*x \<Longrightarrow> a\<sharp>*y \<Longrightarrow> PROP C)"
  2471   and "((b::'a list)\<sharp>*(x,y) \<Longrightarrow> PROP C) \<equiv> (b\<sharp>*x \<Longrightarrow> b\<sharp>*y \<Longrightarrow> PROP C)"
  2472   by (rule, simp_all add: fresh_star_prod)+
  2473 
  2474 
  2475 lemma pt_fresh_star_bij_ineq:
  2476   fixes  pi :: "'x prm"
  2477   and     x :: "'a"
  2478   and     a :: "'y set"
  2479   and     b :: "'y list"
  2480   assumes pta: "pt TYPE('a) TYPE('x)"
  2481   and     ptb: "pt TYPE('y) TYPE('x)"
  2482   and     at:  "at TYPE('x)"
  2483   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2484   shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
  2485   and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
  2486 apply(unfold fresh_star_def)
  2487 apply(auto)
  2488 apply(drule_tac x="pi\<bullet>xa" in bspec)
  2489 apply(erule pt_set_bij2[OF ptb, OF at])
  2490 apply(simp add: fresh_star_def pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
  2491 apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
  2492 apply(simp add: pt_set_bij1[OF ptb, OF at])
  2493 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  2494 apply(drule_tac x="pi\<bullet>xa" in bspec)
  2495 apply(simp add: pt_set_bij1[OF ptb, OF at])
  2496 apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
  2497 apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
  2498 apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
  2499 apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
  2500 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  2501 done
  2502 
  2503 lemma pt_fresh_star_bij:
  2504   fixes  pi :: "'x prm"
  2505   and     x :: "'a"
  2506   and     a :: "'x set"
  2507   and     b :: "'x list"
  2508   assumes pt: "pt TYPE('a) TYPE('x)"
  2509   and     at: "at TYPE('x)"
  2510   shows "(pi\<bullet>a)\<sharp>*(pi\<bullet>x) = a\<sharp>*x"
  2511   and   "(pi\<bullet>b)\<sharp>*(pi\<bullet>x) = b\<sharp>*x"
  2512 apply(rule pt_fresh_star_bij_ineq(1))
  2513 apply(rule pt)
  2514 apply(rule at_pt_inst)
  2515 apply(rule at)+
  2516 apply(rule cp_pt_inst)
  2517 apply(rule pt)
  2518 apply(rule at)
  2519 apply(rule pt_fresh_star_bij_ineq(2))
  2520 apply(rule pt)
  2521 apply(rule at_pt_inst)
  2522 apply(rule at)+
  2523 apply(rule cp_pt_inst)
  2524 apply(rule pt)
  2525 apply(rule at)
  2526 done
  2527 
  2528 lemma pt_fresh_star_eqvt:
  2529   fixes  pi :: "'x prm"
  2530   and     x :: "'a"
  2531   and     a :: "'x set"
  2532   and     b :: "'x list"
  2533   assumes pt: "pt TYPE('a) TYPE('x)"
  2534   and     at: "at TYPE('x)"
  2535   shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
  2536   and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
  2537   by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])
  2538 
  2539 lemma pt_fresh_star_eqvt_ineq:
  2540   fixes pi::"'x prm"
  2541   and   a::"'y set"
  2542   and   b::"'y list"
  2543   and   x::"'a"
  2544   assumes pta: "pt TYPE('a) TYPE('x)"
  2545   and     ptb: "pt TYPE('y) TYPE('x)"
  2546   and     at:  "at TYPE('x)"
  2547   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2548   and     dj:  "disjoint TYPE('y) TYPE('x)"
  2549   shows "pi\<bullet>(a\<sharp>*x) = (pi\<bullet>a)\<sharp>*(pi\<bullet>x)"
  2550   and   "pi\<bullet>(b\<sharp>*x) = (pi\<bullet>b)\<sharp>*(pi\<bullet>x)"
  2551   by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
  2552 
  2553 lemma pt_freshs_freshs:
  2554   assumes pt: "pt TYPE('a) TYPE('x)"
  2555   and at: "at TYPE ('x)"
  2556   and pi: "set (pi::'x prm) \<subseteq> Xs \<times> Ys"
  2557   and Xs: "Xs \<sharp>* (x::'a)"
  2558   and Ys: "Ys \<sharp>* x"
  2559   shows "pi\<bullet>x = x"
  2560   using pi
  2561 proof (induct pi)
  2562   case Nil
  2563   show ?case by (simp add: pt1 [OF pt])
  2564 next
  2565   case (Cons p pi)
  2566   obtain a b where p: "p = (a, b)" by (cases p)
  2567   with Cons Xs Ys have "a \<sharp> x" "b \<sharp> x"
  2568     by (simp_all add: fresh_star_def)
  2569   with Cons p show ?case
  2570     by (simp add: pt_fresh_fresh [OF pt at]
  2571       pt2 [OF pt, of "[(a, b)]" pi, simplified])
  2572 qed
  2573 
  2574 lemma pt_fresh_star_pi: 
  2575   fixes x::"'a"
  2576   and   pi::"'x prm"
  2577   assumes pt: "pt TYPE('a) TYPE('x)"
  2578   and     at: "at TYPE('x)"
  2579   and     a: "((supp x)::'x set)\<sharp>* pi"
  2580   shows "pi\<bullet>x = x"
  2581 using a
  2582 apply(induct pi)
  2583 apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
  2584 apply(subgoal_tac "((a,b)#pi)\<bullet>x = ([(a,b)]@pi)\<bullet>x")
  2585 apply(simp only: pt2[OF pt])
  2586 apply(rule pt_fresh_fresh[OF pt at])
  2587 apply(simp add: fresh_def at_supp[OF at])
  2588 apply(blast)
  2589 apply(simp add: fresh_def at_supp[OF at])
  2590 apply(blast)
  2591 apply(simp add: pt2[OF pt])
  2592 done
  2593 
  2594 section \<open>Infrastructure lemmas for strong rule inductions\<close>
  2595 (*==========================================================*)
  2596 
  2597 text \<open>
  2598   For every set of atoms, there is another set of atoms
  2599   avoiding a finitely supported c and there is a permutation
  2600   which 'translates' between both sets.
  2601 \<close>
  2602 
  2603 lemma at_set_avoiding_aux:
  2604   fixes Xs::"'a set"
  2605   and   As::"'a set"
  2606   assumes at: "at TYPE('a)"
  2607   and     b: "Xs \<subseteq> As"
  2608   and     c: "finite As"
  2609   and     d: "finite ((supp c)::'a set)"
  2610   shows "\<exists>(pi::'a prm). (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
  2611 proof -
  2612   from b c have "finite Xs" by (simp add: finite_subset)
  2613   then show ?thesis using b 
  2614   proof (induct)
  2615     case empty
  2616     have "({}::'a set)\<sharp>*c" by (simp add: fresh_star_def)
  2617     moreover
  2618     have "({}::'a set) \<inter> As = {}" by simp
  2619     moreover
  2620     have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
  2621     ultimately show ?case by (simp add: empty_eqvt)
  2622   next
  2623     case (insert x Xs)
  2624     then have ih: "\<exists>pi. (pi\<bullet>Xs)\<sharp>*c \<and> (pi\<bullet>Xs) \<inter> As = {} \<and> set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by simp
  2625     then obtain pi where a1: "(pi\<bullet>Xs)\<sharp>*c" and a2: "(pi\<bullet>Xs) \<inter> As = {}" and 
  2626       a4: "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)" by blast
  2627     have b: "x\<notin>Xs" by fact
  2628     have d1: "finite As" by fact
  2629     have d2: "finite Xs" by fact
  2630     have d3: "({x} \<union> Xs) \<subseteq> As" using insert(4) by simp
  2631     from d d1 d2
  2632     obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)" 
  2633       apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"])
  2634       apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
  2635         pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at]] at])
  2636       done
  2637     have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def)
  2638     moreover
  2639     have "({y}\<union>(pi\<bullet>Xs))\<inter>As = {}" using a2 d1 fr 
  2640       by (simp add: fresh_prod at_fin_set_fresh[OF at])
  2641     moreover
  2642     have "pi\<bullet>x=x" using a4 b a2 d3 
  2643       by (rule_tac at_prm_fresh2[OF at]) (auto)
  2644     then have "set ((pi\<bullet>x,y)#pi) \<subseteq> ({x} \<union> Xs) \<times> ({y}\<union>(pi\<bullet>Xs))" using a4 by auto
  2645     moreover
  2646     have "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)"
  2647     proof -
  2648       have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
  2649       proof -
  2650         have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2 
  2651           by (simp add: pt_fresh_bij [OF pt_set_inst [OF at_pt_inst [OF at]], OF at]
  2652             at_fin_set_fresh [OF at])
  2653         moreover
  2654         have "y\<sharp>(pi\<bullet>Xs)" using fr by simp
  2655         ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
  2656           by (simp add: pt_fresh_fresh[OF pt_set_inst
  2657             [OF at_pt_inst[OF at]], OF at])
  2658       qed
  2659       have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
  2660         by (simp add: pt2[symmetric, OF pt_set_inst [OF at_pt_inst[OF at]]])
  2661       also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
  2662         by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
  2663       finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp
  2664     qed
  2665     ultimately 
  2666     show ?case by (rule_tac x="(pi\<bullet>x,y)#pi" in exI) (auto)
  2667   qed
  2668 qed
  2669 
  2670 lemma at_set_avoiding:
  2671   fixes Xs::"'a set"
  2672   assumes at: "at TYPE('a)"
  2673   and     a: "finite Xs"
  2674   and     b: "finite ((supp c)::'a set)"
  2675   obtains pi::"'a prm" where "(pi\<bullet>Xs)\<sharp>*c" and "set pi \<subseteq> Xs \<times> (pi\<bullet>Xs)"
  2676 using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"]
  2677 by (blast)
  2678 
  2679 section \<open>composition instances\<close>
  2680 (* ============================= *)
  2681 
  2682 lemma cp_list_inst:
  2683   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2684   shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
  2685 using c1
  2686 apply(simp add: cp_def)
  2687 apply(auto)
  2688 apply(induct_tac x)
  2689 apply(auto)
  2690 done
  2691 
  2692 lemma cp_set_inst:
  2693   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2694   shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
  2695 using c1
  2696 apply(simp add: cp_def)
  2697 apply(auto)
  2698 apply(auto simp add: perm_set_def)
  2699 apply(rule_tac x="pi2\<bullet>xc" in exI)
  2700 apply(auto)
  2701 done
  2702 
  2703 lemma cp_option_inst:
  2704   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2705   shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
  2706 using c1
  2707 apply(simp add: cp_def)
  2708 apply(auto)
  2709 apply(case_tac x)
  2710 apply(auto)
  2711 done
  2712 
  2713 lemma cp_noption_inst:
  2714   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2715   shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
  2716 using c1
  2717 apply(simp add: cp_def)
  2718 apply(auto)
  2719 apply(case_tac x)
  2720 apply(auto)
  2721 done
  2722 
  2723 lemma cp_unit_inst:
  2724   shows "cp TYPE (unit) TYPE('x) TYPE('y)"
  2725 apply(simp add: cp_def)
  2726 done
  2727 
  2728 lemma cp_bool_inst:
  2729   shows "cp TYPE (bool) TYPE('x) TYPE('y)"
  2730 apply(simp add: cp_def)
  2731 apply(rule allI)+
  2732 apply(induct_tac x)
  2733 apply(simp_all)
  2734 done
  2735 
  2736 lemma cp_prod_inst:
  2737   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2738   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  2739   shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
  2740 using c1 c2
  2741 apply(simp add: cp_def)
  2742 done
  2743 
  2744 lemma cp_fun_inst:
  2745   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2746   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  2747   and     pt: "pt TYPE ('y) TYPE('x)"
  2748   and     at: "at TYPE ('x)"
  2749   shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
  2750 using c1 c2
  2751 apply(auto simp add: cp_def perm_fun_def fun_eq_iff)
  2752 apply(simp add: rev_eqvt[symmetric])
  2753 apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
  2754 done
  2755 
  2756 
  2757 section \<open>Andy's freshness lemma\<close>
  2758 (*================================*)
  2759 
  2760 lemma freshness_lemma:
  2761   fixes h :: "'x\<Rightarrow>'a"
  2762   assumes pta: "pt TYPE('a) TYPE('x)"
  2763   and     at:  "at TYPE('x)" 
  2764   and     f1:  "finite ((supp h)::'x set)"
  2765   and     a: "\<exists>a::'x. a\<sharp>(h,h a)"
  2766   shows  "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr"
  2767 proof -
  2768   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  2769   have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  2770   from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by (force simp add: fresh_prod)
  2771   show ?thesis
  2772   proof
  2773     let ?fr = "h (a0::'x)"
  2774     show "\<forall>(a::'x). (a\<sharp>h \<longrightarrow> ((h a) = ?fr))" 
  2775     proof (intro strip)
  2776       fix a
  2777       assume a3: "(a::'x)\<sharp>h"
  2778       show "h (a::'x) = h a0"
  2779       proof (cases "a=a0")
  2780         case True thus "h (a::'x) = h a0" by simp
  2781       next
  2782         case False 
  2783         assume "a\<noteq>a0"
  2784         hence c1: "a\<notin>((supp a0)::'x set)" by  (simp add: fresh_def[symmetric] at_fresh[OF at])
  2785         have c2: "a\<notin>((supp h)::'x set)" using a3 by (simp add: fresh_def)
  2786         from c1 c2 have c3: "a\<notin>((supp h)\<union>((supp a0)::'x set))" by force
  2787         have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at])
  2788         from f1 f2 have "((supp (h a0))::'x set)\<subseteq>((supp h)\<union>(supp a0))"
  2789           by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at])
  2790         hence "a\<notin>((supp (h a0))::'x set)" using c3 by force
  2791         hence "a\<sharp>(h a0)" by (simp add: fresh_def) 
  2792         with a2 have d1: "[(a0,a)]\<bullet>(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at])
  2793         from a1 a3 have d2: "[(a0,a)]\<bullet>h = h" by (rule pt_fresh_fresh[OF ptc, OF at])
  2794         from d1 have "h a0 = [(a0,a)]\<bullet>(h a0)" by simp
  2795         also have "\<dots>= ([(a0,a)]\<bullet>h)([(a0,a)]\<bullet>a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2796         also have "\<dots> = h ([(a0,a)]\<bullet>a0)" using d2 by simp
  2797         also have "\<dots> = h a" by (simp add: at_calc[OF at])
  2798         finally show "h a = h a0" by simp
  2799       qed
  2800     qed
  2801   qed
  2802 qed
  2803 
  2804 lemma freshness_lemma_unique:
  2805   fixes h :: "'x\<Rightarrow>'a"
  2806   assumes pt: "pt TYPE('a) TYPE('x)"
  2807   and     at: "at TYPE('x)" 
  2808   and     f1: "finite ((supp h)::'x set)"
  2809   and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
  2810   shows  "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
  2811 proof (rule ex_ex1I)
  2812   from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
  2813 next
  2814   fix fr1 fr2
  2815   assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1"
  2816   assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2"
  2817   from a obtain a where "(a::'x)\<sharp>h" by (force simp add: fresh_prod) 
  2818   with b1 b2 have "h a = fr1 \<and> h a = fr2" by force
  2819   thus "fr1 = fr2" by force
  2820 qed
  2821 
  2822 \<comment> "packaging the freshness lemma into a function"
  2823 definition fresh_fun :: "('x\<Rightarrow>'a)\<Rightarrow>'a" where
  2824   "fresh_fun (h) \<equiv> THE fr. (\<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr)"
  2825 
  2826 lemma fresh_fun_app:
  2827   fixes h :: "'x\<Rightarrow>'a"
  2828   and   a :: "'x"
  2829   assumes pt: "pt TYPE('a) TYPE('x)"
  2830   and     at: "at TYPE('x)" 
  2831   and     f1: "finite ((supp h)::'x set)"
  2832   and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
  2833   and     b: "a\<sharp>h"
  2834   shows "(fresh_fun h) = (h a)"
  2835 proof (unfold fresh_fun_def, rule the_equality)
  2836   show "\<forall>(a'::'x). a'\<sharp>h \<longrightarrow> h a' = h a"
  2837   proof (intro strip)
  2838     fix a'::"'x"
  2839     assume c: "a'\<sharp>h"
  2840     from pt at f1 a have "\<exists>(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" by (rule freshness_lemma)
  2841     with b c show "h a' = h a" by force
  2842   qed
  2843 next
  2844   fix fr::"'a"
  2845   assume "\<forall>a. a\<sharp>h \<longrightarrow> h a = fr"
  2846   with b show "fr = h a" by force
  2847 qed
  2848 
  2849 lemma fresh_fun_app':
  2850   fixes h :: "'x\<Rightarrow>'a"
  2851   and   a :: "'x"
  2852   assumes pt: "pt TYPE('a) TYPE('x)"
  2853   and     at: "at TYPE('x)" 
  2854   and     f1: "finite ((supp h)::'x set)"
  2855   and     a: "a\<sharp>h" "a\<sharp>h a"
  2856   shows "(fresh_fun h) = (h a)"
  2857 apply(rule fresh_fun_app[OF pt, OF at, OF f1])
  2858 apply(auto simp add: fresh_prod intro: a)
  2859 done
  2860 
  2861 lemma fresh_fun_equiv_ineq:
  2862   fixes h :: "'y\<Rightarrow>'a"
  2863   and   pi:: "'x prm"
  2864   assumes pta: "pt TYPE('a) TYPE('x)"
  2865   and     ptb: "pt TYPE('y) TYPE('x)"
  2866   and     ptb':"pt TYPE('a) TYPE('y)"
  2867   and     at:  "at TYPE('x)" 
  2868   and     at': "at TYPE('y)"
  2869   and     cpa: "cp TYPE('a) TYPE('x) TYPE('y)"
  2870   and     cpb: "cp TYPE('y) TYPE('x) TYPE('y)"
  2871   and     f1: "finite ((supp h)::'y set)"
  2872   and     a1: "\<exists>(a::'y). a\<sharp>(h,h a)"
  2873   shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
  2874 proof -
  2875   have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 
  2876   have ptc: "pt TYPE('y\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  2877   have cpc: "cp TYPE('y\<Rightarrow>'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at])
  2878   have f2: "finite ((supp (pi\<bullet>h))::'y set)"
  2879   proof -
  2880     from f1 have "finite (pi\<bullet>((supp h)::'y set))"
  2881       by (simp add: pt_set_finite_ineq[OF ptb, OF at])
  2882     thus ?thesis
  2883       by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc])
  2884   qed
  2885   from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force
  2886   hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod)
  2887   have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1
  2888   by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc])
  2889   have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
  2890   proof -
  2891     from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))"
  2892       by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa])
  2893     thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2894   qed
  2895   have a2: "\<exists>(a::'y). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod)
  2896   have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1])
  2897   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 
  2898     by (simp add: fresh_fun_app[OF ptb', OF at', OF f2])
  2899   show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2900 qed
  2901 
  2902 lemma fresh_fun_equiv:
  2903   fixes h :: "'x\<Rightarrow>'a"
  2904   and   pi:: "'x prm"
  2905   assumes pta: "pt TYPE('a) TYPE('x)"
  2906   and     at:  "at TYPE('x)" 
  2907   and     f1:  "finite ((supp h)::'x set)"
  2908   and     a1: "\<exists>(a::'x). a\<sharp>(h,h a)"
  2909   shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
  2910 proof -
  2911   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  2912   have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  2913   have f2: "finite ((supp (pi\<bullet>h))::'x set)"
  2914   proof -
  2915     from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
  2916     thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
  2917   qed
  2918   from a1 obtain a' where c0: "a'\<sharp>(h,h a')" by force
  2919   hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by (simp_all add: fresh_prod)
  2920   have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
  2921   have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
  2922   proof -
  2923     from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
  2924     thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2925   qed
  2926   have a2: "\<exists>(a::'x). a\<sharp>(pi\<bullet>h,(pi\<bullet>h) a)" using c3 c4 by (force simp add: fresh_prod)
  2927   have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
  2928   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
  2929   show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2930 qed
  2931 
  2932 lemma fresh_fun_supports:
  2933   fixes h :: "'x\<Rightarrow>'a"
  2934   assumes pt: "pt TYPE('a) TYPE('x)"
  2935   and     at: "at TYPE('x)" 
  2936   and     f1: "finite ((supp h)::'x set)"
  2937   and     a: "\<exists>(a::'x). a\<sharp>(h,h a)"
  2938   shows "((supp h)::'x set) supports (fresh_fun h)"
  2939   apply(simp add: supports_def fresh_def[symmetric])
  2940   apply(auto)
  2941   apply(simp add: fresh_fun_equiv[OF pt, OF at, OF f1, OF a])
  2942   apply(simp add: pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
  2943   done
  2944   
  2945 section \<open>Abstraction function\<close>
  2946 (*==============================*)
  2947 
  2948 lemma pt_abs_fun_inst:
  2949   assumes pt: "pt TYPE('a) TYPE('x)"
  2950   and     at: "at TYPE('x)"
  2951   shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)"
  2952   by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
  2953 
  2954 definition abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100) where 
  2955   "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
  2956 
  2957 (* FIXME: should be called perm_if and placed close to the definition of permutations on bools *)
  2958 lemma abs_fun_if: 
  2959   fixes pi :: "'x prm"
  2960   and   x  :: "'a"
  2961   and   y  :: "'a"
  2962   and   c  :: "bool"
  2963   shows "pi\<bullet>(if c then x else y) = (if c then (pi\<bullet>x) else (pi\<bullet>y))"   
  2964   by force
  2965 
  2966 lemma abs_fun_pi_ineq:
  2967   fixes a  :: "'y"
  2968   and   x  :: "'a"
  2969   and   pi :: "'x prm"
  2970   assumes pta: "pt TYPE('a) TYPE('x)"
  2971   and     ptb: "pt TYPE('y) TYPE('x)"
  2972   and     at:  "at TYPE('x)"
  2973   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2974   shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  2975   apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
  2976   apply(simp only: fun_eq_iff)
  2977   apply(rule allI)
  2978   apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
  2979   apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
  2980   apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
  2981   apply(simp)
  2982 (*C*)
  2983   apply(simp add: cp1[OF cp])
  2984   apply(simp add: pt_pi_rev[OF ptb, OF at])
  2985 (*B*)
  2986   apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  2987 (*A*)
  2988   apply(rule iffI)
  2989   apply(rule pt_bij2[OF ptb, OF at, THEN sym])
  2990   apply(simp)
  2991   apply(rule pt_bij2[OF ptb, OF at])
  2992   apply(simp)
  2993 done
  2994 
  2995 lemma abs_fun_pi:
  2996   fixes a  :: "'x"
  2997   and   x  :: "'a"
  2998   and   pi :: "'x prm"
  2999   assumes pt: "pt TYPE('a) TYPE('x)"
  3000   and     at: "at TYPE('x)"
  3001   shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  3002 apply(rule abs_fun_pi_ineq)
  3003 apply(rule pt)
  3004 apply(rule at_pt_inst)
  3005 apply(rule at)+
  3006 apply(rule cp_pt_inst)
  3007 apply(rule pt)
  3008 apply(rule at)
  3009 done
  3010 
  3011 lemma abs_fun_eq1: 
  3012   fixes x  :: "'a"
  3013   and   y  :: "'a"
  3014   and   a  :: "'x"
  3015   shows "([a].x = [a].y) = (x = y)"
  3016 apply(auto simp add: abs_fun_def)
  3017 apply(auto simp add: fun_eq_iff)
  3018 apply(drule_tac x="a" in spec)
  3019 apply(simp)
  3020 done
  3021 
  3022 lemma abs_fun_eq2:
  3023   fixes x  :: "'a"
  3024   and   y  :: "'a"
  3025   and   a  :: "'x"
  3026   and   b  :: "'x"
  3027   assumes pt: "pt TYPE('a) TYPE('x)"
  3028       and at: "at TYPE('x)"
  3029       and a1: "a\<noteq>b" 
  3030       and a2: "[a].x = [b].y" 
  3031   shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
  3032 proof -
  3033   from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: fun_eq_iff)
  3034   hence "([a].x) a = ([b].y) a" by simp
  3035   hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def)
  3036   show "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
  3037   proof (cases "a\<sharp>y")
  3038     assume a4: "a\<sharp>y"
  3039     hence "x=[(b,a)]\<bullet>y" using a3 a1 by (simp add: abs_fun_def)
  3040     moreover
  3041     have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
  3042     ultimately show ?thesis using a4 by simp
  3043   next
  3044     assume "\<not>a\<sharp>y"
  3045     hence "nSome(x) = nNone" using a1 a3 by (simp add: abs_fun_def)
  3046     hence False by simp
  3047     thus ?thesis by simp
  3048   qed
  3049 qed
  3050 
  3051 lemma abs_fun_eq3: 
  3052   fixes x  :: "'a"
  3053   and   y  :: "'a"
  3054   and   a   :: "'x"
  3055   and   b   :: "'x"
  3056   assumes pt: "pt TYPE('a) TYPE('x)"
  3057       and at: "at TYPE('x)"
  3058       and a1: "a\<noteq>b" 
  3059       and a2: "x=[(a,b)]\<bullet>y" 
  3060       and a3: "a\<sharp>y" 
  3061   shows "[a].x =[b].y"
  3062 proof -
  3063   show ?thesis 
  3064   proof (simp only: abs_fun_def fun_eq_iff, intro strip)
  3065     fix c::"'x"
  3066     let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone"
  3067     and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone"
  3068     show "?LHS=?RHS"
  3069     proof -
  3070       have "(c=a) \<or> (c=b) \<or> (c\<noteq>a \<and> c\<noteq>b)" by blast
  3071       moreover  \<comment>"case c=a"
  3072       { have "nSome(x) = nSome([(a,b)]\<bullet>y)" using a2 by simp
  3073         also have "\<dots> = nSome([(b,a)]\<bullet>y)" by (simp, rule pt3[OF pt], rule at_ds5[OF at])
  3074         finally have "nSome(x) = nSome([(b,a)]\<bullet>y)" by simp
  3075         moreover
  3076         assume "c=a"
  3077         ultimately have "?LHS=?RHS" using a1 a3 by simp
  3078       }
  3079       moreover  \<comment> "case c=b"
  3080       { have a4: "y=[(a,b)]\<bullet>x" using a2 by (simp only: pt_swap_bij[OF pt, OF at])
  3081         hence "a\<sharp>([(a,b)]\<bullet>x)" using a3 by simp
  3082         hence "b\<sharp>x" by (simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
  3083         moreover
  3084         assume "c=b"
  3085         ultimately have "?LHS=?RHS" using a1 a4 by simp
  3086       }
  3087       moreover  \<comment> "case c\<noteq>a \<and> c\<noteq>b"
  3088       { assume a5: "c\<noteq>a \<and> c\<noteq>b"
  3089         moreover 
  3090         have "c\<sharp>x = c\<sharp>y" using a2 a5 by (force simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
  3091         moreover 
  3092         have "c\<sharp>y \<longrightarrow> [(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 
  3093         proof (intro strip)
  3094           assume a6: "c\<sharp>y"
  3095           have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at])
  3096           hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>y)) = [(a,b)]\<bullet>y" 
  3097             by (simp add: pt2[OF pt, symmetric] pt3[OF pt])
  3098           hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = [(a,b)]\<bullet>y" using a3 a6 
  3099             by (simp add: pt_fresh_fresh[OF pt, OF at])
  3100           hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = x" using a2 by simp
  3101           hence "[(b,c)]\<bullet>y = [(a,c)]\<bullet>x" by (drule_tac pt_bij1[OF pt, OF at], simp)
  3102           thus "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y" by simp
  3103         qed
  3104         ultimately have "?LHS=?RHS" by simp
  3105       }
  3106       ultimately show "?LHS = ?RHS" by blast
  3107     qed
  3108   qed
  3109 qed
  3110         
  3111 (* alpha equivalence *)
  3112 lemma abs_fun_eq: 
  3113   fixes x  :: "'a"
  3114   and   y  :: "'a"
  3115   and   a  :: "'x"
  3116   and   b  :: "'x"
  3117   assumes pt: "pt TYPE('a) TYPE('x)"
  3118       and at: "at TYPE('x)"
  3119   shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y))"
  3120 proof (rule iffI)
  3121   assume b: "[a].x = [b].y"
  3122   show "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  3123   proof (cases "a=b")
  3124     case True with b show ?thesis by (simp add: abs_fun_eq1)
  3125   next
  3126     case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at])
  3127   qed
  3128 next
  3129   assume "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  3130   thus "[a].x = [b].y"
  3131   proof
  3132     assume "a=b \<and> x=y" thus ?thesis by simp
  3133   next
  3134     assume "a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 
  3135     thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at])
  3136   qed
  3137 qed
  3138 
  3139 (* symmetric version of alpha-equivalence *)
  3140 lemma abs_fun_eq': 
  3141   fixes x  :: "'a"
  3142   and   y  :: "'a"
  3143   and   a  :: "'x"
  3144   and   b  :: "'x"
  3145   assumes pt: "pt TYPE('a) TYPE('x)"
  3146       and at: "at TYPE('x)"
  3147   shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> [(b,a)]\<bullet>x=y \<and> b\<sharp>x))"
  3148 by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij'[OF pt, OF at] 
  3149                    pt_fresh_left[OF pt, OF at] 
  3150                    at_calc[OF at])
  3151 
  3152 (* alpha_equivalence with a fresh name *)
  3153 lemma abs_fun_fresh: 
  3154   fixes x :: "'a"
  3155   and   y :: "'a"
  3156   and   c :: "'x"
  3157   and   a :: "'x"
  3158   and   b :: "'x"
  3159   assumes pt: "pt TYPE('a) TYPE('x)"
  3160       and at: "at TYPE('x)"
  3161       and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 
  3162   shows "([a].x = [b].y) = ([(a,c)]\<bullet>x = [(b,c)]\<bullet>y)"
  3163 proof (rule iffI)
  3164   assume eq0: "[a].x = [b].y"
  3165   show "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y"
  3166   proof (cases "a=b")
  3167     case True then show ?thesis using eq0 by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at])
  3168   next
  3169     case False 
  3170     have ineq: "a\<noteq>b" by fact
  3171     with eq0 have eq: "x=[(a,b)]\<bullet>y" and fr': "a\<sharp>y" by (simp_all add: abs_fun_eq[OF pt, OF at])
  3172     from eq have "[(a,c)]\<bullet>x = [(a,c)]\<bullet>[(a,b)]\<bullet>y" by (simp add: pt_bij[OF pt, OF at])
  3173     also have "\<dots> = ([(a,c)]\<bullet>[(a,b)])\<bullet>([(a,c)]\<bullet>y)" by (rule pt_perm_compose[OF pt, OF at])
  3174     also have "\<dots> = [(c,b)]\<bullet>y" using ineq fr fr' 
  3175       by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at])
  3176     also have "\<dots> = [(b,c)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
  3177     finally show ?thesis by simp
  3178   qed
  3179 next
  3180   assume eq: "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y"
  3181   thus "[a].x = [b].y"
  3182   proof (cases "a=b")
  3183     case True then show ?thesis using eq by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at])
  3184   next
  3185     case False
  3186     have ineq: "a\<noteq>b" by fact
  3187     from fr have "([(a,c)]\<bullet>c)\<sharp>([(a,c)]\<bullet>x)" by (simp add: pt_fresh_bij[OF pt, OF at])
  3188     hence "a\<sharp>([(b,c)]\<bullet>y)" using eq fr by (simp add: at_calc[OF at])
  3189     hence fr0: "a\<sharp>y" using ineq fr by (simp add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
  3190     from eq have "x = (rev [(a,c)])\<bullet>([(b,c)]\<bullet>y)" by (rule pt_bij1[OF pt, OF at])
  3191     also have "\<dots> = [(a,c)]\<bullet>([(b,c)]\<bullet>y)" by simp
  3192     also have "\<dots> = ([(a,c)]\<bullet>[(b,c)])\<bullet>([(a,c)]\<bullet>y)" by (rule pt_perm_compose[OF pt, OF at])
  3193     also have "\<dots> = [(b,a)]\<bullet>y" using ineq fr fr0  
  3194       by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at])
  3195     also have "\<dots> = [(a,b)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
  3196     finally show ?thesis using ineq fr0 by (simp add: abs_fun_eq[OF pt, OF at])
  3197   qed
  3198 qed
  3199 
  3200 lemma abs_fun_fresh': 
  3201   fixes x :: "'a"
  3202   and   y :: "'a"
  3203   and   c :: "'x"
  3204   and   a :: "'x"
  3205   and   b :: "'x"
  3206   assumes pt: "pt TYPE('a) TYPE('x)"
  3207       and at: "at TYPE('x)"
  3208       and as: "[a].x = [b].y"
  3209       and fr: "c\<noteq>a" "c\<noteq>b" "c\<sharp>x" "c\<sharp>y" 
  3210   shows "x = [(a,c)]\<bullet>[(b,c)]\<bullet>y"
  3211 using as fr
  3212 apply(drule_tac sym)
  3213 apply(simp add: abs_fun_fresh[OF pt, OF at] pt_swap_bij[OF pt, OF at])
  3214 done
  3215 
  3216 lemma abs_fun_supp_approx:
  3217   fixes x :: "'a"
  3218   and   a :: "'x"
  3219   assumes pt: "pt TYPE('a) TYPE('x)"
  3220   and     at: "at TYPE('x)"
  3221   shows "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))"
  3222 proof 
  3223   fix c
  3224   assume "c\<in>((supp ([a].x))::'x set)"
  3225   hence "infinite {b. [(c,b)]\<bullet>([a].x) \<noteq> [a].x}" by (simp add: supp_def)
  3226   hence "infinite {b. [([(c,b)]\<bullet>a)].([(c,b)]\<bullet>x) \<noteq> [a].x}" by (simp add: abs_fun_pi[OF pt, OF at])
  3227   moreover
  3228   have "{b. [([(c,b)]\<bullet>a)].([(c,b)]\<bullet>x) \<noteq> [a].x} \<subseteq> {b. ([(c,b)]\<bullet>x,[(c,b)]\<bullet>a) \<noteq> (x, a)}" by force
  3229   ultimately have "infinite {b. ([(c,b)]\<bullet>x,[(c,b)]\<bullet>a) \<noteq> (x, a)}" by (simp add: infinite_super)
  3230   thus "c\<in>(supp (x,a))" by (simp add: supp_def)
  3231 qed
  3232 
  3233 lemma abs_fun_finite_supp:
  3234   fixes x :: "'a"
  3235   and   a :: "'x"
  3236   assumes pt: "pt TYPE('a) TYPE('x)"
  3237   and     at: "at TYPE('x)"
  3238   and     f:  "finite ((supp x)::'x set)"
  3239   shows "finite ((supp ([a].x))::'x set)"
  3240 proof -
  3241   from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at])
  3242   moreover
  3243   have "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at])
  3244   ultimately show ?thesis by (simp add: finite_subset)
  3245 qed
  3246 
  3247 lemma fresh_abs_funI1:
  3248   fixes  x :: "'a"
  3249   and    a :: "'x"
  3250   and    b :: "'x"
  3251   assumes pt:  "pt TYPE('a) TYPE('x)"
  3252   and     at:   "at TYPE('x)"
  3253   and f:  "finite ((supp x)::'x set)"
  3254   and a1: "b\<sharp>x" 
  3255   and a2: "a\<noteq>b"
  3256   shows "b\<sharp>([a].x)"
  3257   proof -
  3258     have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 
  3259     proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
  3260       show "finite ((supp ([a].x))::'x set)" using f
  3261         by (simp add: abs_fun_finite_supp[OF pt, OF at])        
  3262     qed
  3263     then obtain c where fr1: "c\<noteq>b"
  3264                   and   fr2: "c\<noteq>a"
  3265                   and   fr3: "c\<sharp>x"
  3266                   and   fr4: "c\<sharp>([a].x)"
  3267                   by (force simp add: fresh_prod at_fresh[OF at])
  3268     have e: "[(c,b)]\<bullet>([a].x) = [a].([(c,b)]\<bullet>x)" using a2 fr1 fr2 
  3269       by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  3270     from fr4 have "([(c,b)]\<bullet>c)\<sharp> ([(c,b)]\<bullet>([a].x))"
  3271       by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  3272     hence "b\<sharp>([a].([(c,b)]\<bullet>x))" using fr1 fr2 e  
  3273       by (simp add: at_calc[OF at])
  3274     thus ?thesis using a1 fr3 
  3275       by (simp add: pt_fresh_fresh[OF pt, OF at])
  3276 qed
  3277 
  3278 lemma fresh_abs_funE:
  3279   fixes a :: "'x"
  3280   and   b :: "'x"
  3281   and   x :: "'a"
  3282   assumes pt:  "pt TYPE('a) TYPE('x)"
  3283   and     at:  "at TYPE('x)"
  3284   and     f:  "finite ((supp x)::'x set)"
  3285   and     a1: "b\<sharp>([a].x)" 
  3286   and     a2: "b\<noteq>a" 
  3287   shows "b\<sharp>x"
  3288 proof -
  3289   have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
  3290   proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
  3291     show "finite ((supp ([a].x))::'x set)" using f
  3292       by (simp add: abs_fun_finite_supp[OF pt, OF at])  
  3293   qed
  3294   then obtain c where fr1: "b\<noteq>c"
  3295                 and   fr2: "c\<noteq>a"
  3296                 and   fr3: "c\<sharp>x"
  3297                 and   fr4: "c\<sharp>([a].x)" by (force simp add: fresh_prod at_fresh[OF at])
  3298   have "[a].x = [(b,c)]\<bullet>([a].x)" using a1 fr4 
  3299     by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  3300   hence "[a].x = [a].([(b,c)]\<bullet>x)" using fr2 a2 
  3301     by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  3302   hence b: "([(b,c)]\<bullet>x) = x" by (simp add: abs_fun_eq1)
  3303   from fr3 have "([(b,c)]\<bullet>c)\<sharp>([(b,c)]\<bullet>x)" 
  3304     by (simp add: pt_fresh_bij[OF pt, OF at]) 
  3305   thus ?thesis using b fr1 by (simp add: at_calc[OF at])
  3306 qed
  3307 
  3308 lemma fresh_abs_funI2:
  3309   fixes a :: "'x"
  3310   and   x :: "'a"
  3311   assumes pt: "pt TYPE('a) TYPE('x)"
  3312   and     at: "at TYPE('x)"
  3313   and     f: "finite ((supp x)::'x set)"
  3314   shows "a\<sharp>([a].x)"
  3315 proof -
  3316   have "\<exists>c::'x. c\<sharp>(a,x)"
  3317     by  (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 
  3318   then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 
  3319                 and   fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
  3320   have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
  3321   hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))" using fr1  
  3322     by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  3323   hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))" using fr1_sym 
  3324     by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  3325   have "[c].([(c,a)]\<bullet>x) = ([a].x)" using fr1_sym fr2 
  3326     by (simp add: abs_fun_eq[OF pt, OF at])
  3327   thus ?thesis using a by simp
  3328 qed
  3329 
  3330 lemma fresh_abs_fun_iff: 
  3331   fixes a :: "'x"
  3332   and   b :: "'x"
  3333   and   x :: "'a"
  3334   assumes pt: "pt TYPE('a) TYPE('x)"
  3335   and     at: "at TYPE('x)"
  3336   and     f: "finite ((supp x)::'x set)"
  3337   shows "(b\<sharp>([a].x)) = (b=a \<or> b\<sharp>x)" 
  3338   by (auto  dest: fresh_abs_funE[OF pt, OF at,OF f] 
  3339            intro: fresh_abs_funI1[OF pt, OF at,OF f] 
  3340                   fresh_abs_funI2[OF pt, OF at,OF f])
  3341 
  3342 lemma abs_fun_supp: 
  3343   fixes a :: "'x"
  3344   and   x :: "'a"
  3345   assumes pt: "pt TYPE('a) TYPE('x)"
  3346   and     at: "at TYPE('x)"
  3347   and     f: "finite ((supp x)::'x set)"
  3348   shows "supp ([a].x) = (supp x)-{a}"
  3349  by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f])
  3350 
  3351 (* maybe needs to be better stated as supp intersection supp *)
  3352 lemma abs_fun_supp_ineq: 
  3353   fixes a :: "'y"
  3354   and   x :: "'a"
  3355   assumes pta: "pt TYPE('a) TYPE('x)"
  3356   and     ptb: "pt TYPE('y) TYPE('x)"
  3357   and     at:  "at TYPE('x)"
  3358   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  3359   and     dj:  "disjoint TYPE('y) TYPE('x)"
  3360   shows "((supp ([a].x))::'x set) = (supp x)"
  3361 apply(auto simp add: supp_def)
  3362 apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp])
  3363 apply(auto simp add: dj_perm_forget[OF dj])
  3364 apply(auto simp add: abs_fun_eq1) 
  3365 done
  3366 
  3367 lemma fresh_abs_fun_iff_ineq: 
  3368   fixes a :: "'y"
  3369   and   b :: "'x"
  3370   and   x :: "'a"
  3371   assumes pta: "pt TYPE('a) TYPE('x)"
  3372   and     ptb: "pt TYPE('y) TYPE('x)"
  3373   and     at:  "at TYPE('x)"
  3374   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  3375   and     dj:  "disjoint TYPE('y) TYPE('x)"
  3376   shows "b\<sharp>([a].x) = b\<sharp>x" 
  3377   by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj])
  3378 
  3379 section \<open>abstraction type for the parsing in nominal datatype\<close>
  3380 (*==============================================================*)
  3381 
  3382 inductive_set ABS_set :: "('x\<Rightarrow>('a noption)) set"
  3383   where
  3384   ABS_in: "(abs_fun a x)\<in>ABS_set"
  3385 
  3386 definition "ABS = ABS_set"
  3387 
  3388 typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
  3389     "ABS::('x\<Rightarrow>('a noption)) set"
  3390   morphisms Rep_ABS Abs_ABS
  3391   unfolding ABS_def
  3392 proof 
  3393   fix x::"'a" and a::"'x"
  3394   show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
  3395 qed
  3396 
  3397 
  3398 section \<open>lemmas for deciding permutation equations\<close>
  3399 (*===================================================*)
  3400 
  3401 lemma perm_aux_fold:
  3402   shows "perm_aux pi x = pi\<bullet>x" by (simp only: perm_aux_def)
  3403 
  3404 lemma pt_perm_compose_aux:
  3405   fixes pi1 :: "'x prm"
  3406   and   pi2 :: "'x prm"
  3407   and   x  :: "'a"
  3408   assumes pt: "pt TYPE('a) TYPE('x)"
  3409   and     at: "at TYPE('x)"
  3410   shows "pi2\<bullet>(pi1\<bullet>x) = perm_aux (pi2\<bullet>pi1) (pi2\<bullet>x)" 
  3411 proof -
  3412   have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8[OF at])
  3413   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
  3414   thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
  3415 qed  
  3416 
  3417 lemma cp1_aux:
  3418   fixes pi1::"'x prm"
  3419   and   pi2::"'y prm"
  3420   and   x  ::"'a"
  3421   assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  3422   shows "pi1\<bullet>(pi2\<bullet>x) = perm_aux (pi1\<bullet>pi2) (pi1\<bullet>x)"
  3423   using cp by (simp add: cp_def perm_aux_def)
  3424 
  3425 lemma perm_eq_app:
  3426   fixes f  :: "'a\<Rightarrow>'b"
  3427   and   x  :: "'a"
  3428   and   pi :: "'x prm"
  3429   assumes pt: "pt TYPE('a) TYPE('x)"
  3430   and     at: "at TYPE('x)"
  3431   shows "(pi\<bullet>(f x)=y) = ((pi\<bullet>f)(pi\<bullet>x)=y)"
  3432   by (simp add: pt_fun_app_eq[OF pt, OF at])
  3433 
  3434 lemma perm_eq_lam:
  3435   fixes f  :: "'a\<Rightarrow>'b"
  3436   and   x  :: "'a"
  3437   and   pi :: "'x prm"
  3438   shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
  3439   by (simp add: perm_fun_def)
  3440 
  3441 section \<open>test\<close>
  3442 lemma at_prm_eq_compose:
  3443   fixes pi1 :: "'x prm"
  3444   and   pi2 :: "'x prm"
  3445   and   pi3 :: "'x prm"
  3446   assumes at: "at TYPE('x)"
  3447   and     a: "pi1 \<triangleq> pi2"
  3448   shows "(pi3\<bullet>pi1) \<triangleq> (pi3\<bullet>pi2)"
  3449 proof -
  3450   have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at])
  3451   have pt_prm: "pt TYPE('x prm) TYPE('x)" 
  3452     by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]])  
  3453   from a show ?thesis
  3454     apply -
  3455     apply(auto simp add: prm_eq_def)
  3456     apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at])
  3457     apply(rule trans)
  3458     apply(rule pt_perm_compose[OF pt, OF at])
  3459     apply(simp add: pt_rev_pi[OF pt_prm, OF at])
  3460     apply(rule sym)
  3461     apply(rule trans)
  3462     apply(rule pt_perm_compose[OF pt, OF at])
  3463     apply(simp add: pt_rev_pi[OF pt_prm, OF at])
  3464     done
  3465 qed
  3466 
  3467 (************************)
  3468 (* Various eqvt-lemmas  *)
  3469 
  3470 lemma Zero_nat_eqvt:
  3471   shows "pi\<bullet>(0::nat) = 0" 
  3472 by (auto simp add: perm_nat_def)
  3473 
  3474 lemma One_nat_eqvt:
  3475   shows "pi\<bullet>(1::nat) = 1"
  3476 by (simp add: perm_nat_def)
  3477 
  3478 lemma Suc_eqvt:
  3479   shows "pi\<bullet>(Suc x) = Suc (pi\<bullet>x)" 
  3480 by (auto simp add: perm_nat_def)
  3481 
  3482 lemma numeral_nat_eqvt: 
  3483  shows "pi\<bullet>((numeral n)::nat) = numeral n" 
  3484 by (simp add: perm_nat_def perm_int_def)
  3485 
  3486 lemma max_nat_eqvt:
  3487   fixes x::"nat"
  3488   shows "pi\<bullet>(max x y) = max (pi\<bullet>x) (pi\<bullet>y)" 
  3489 by (simp add:perm_nat_def) 
  3490 
  3491 lemma min_nat_eqvt:
  3492   fixes x::"nat"
  3493   shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 
  3494 by (simp add:perm_nat_def) 
  3495 
  3496 lemma plus_nat_eqvt:
  3497   fixes x::"nat"
  3498   shows "pi\<bullet>(x + y) = (pi\<bullet>x) + (pi\<bullet>y)" 
  3499 by (simp add:perm_nat_def) 
  3500 
  3501 lemma minus_nat_eqvt:
  3502   fixes x::"nat"
  3503   shows "pi\<bullet>(x - y) = (pi\<bullet>x) - (pi\<bullet>y)" 
  3504 by (simp add:perm_nat_def) 
  3505 
  3506 lemma mult_nat_eqvt:
  3507   fixes x::"nat"
  3508   shows "pi\<bullet>(x * y) = (pi\<bullet>x) * (pi\<bullet>y)" 
  3509 by (simp add:perm_nat_def) 
  3510 
  3511 lemma div_nat_eqvt:
  3512   fixes x::"nat"
  3513   shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 
  3514 by (simp add:perm_nat_def) 
  3515 
  3516 lemma Zero_int_eqvt:
  3517   shows "pi\<bullet>(0::int) = 0" 
  3518 by (auto simp add: perm_int_def)
  3519 
  3520 lemma One_int_eqvt:
  3521   shows "pi\<bullet>(1::int) = 1"
  3522 by (simp add: perm_int_def)
  3523 
  3524 lemma numeral_int_eqvt: 
  3525  shows "pi\<bullet>((numeral n)::int) = numeral n" 
  3526 by (simp add: perm_int_def perm_int_def)
  3527 
  3528 lemma neg_numeral_int_eqvt:
  3529  shows "pi\<bullet>((- numeral n)::int) = - numeral n"
  3530 by (simp add: perm_int_def perm_int_def)
  3531 
  3532 lemma max_int_eqvt:
  3533   fixes x::"int"
  3534   shows "pi\<bullet>(max (x::int) y) = max (pi\<bullet>x) (pi\<bullet>y)" 
  3535 by (simp add:perm_int_def) 
  3536 
  3537 lemma min_int_eqvt:
  3538   fixes x::"int"
  3539   shows "pi\<bullet>(min x y) = min (pi\<bullet>x) (pi\<bullet>y)" 
  3540 by (simp add:perm_int_def) 
  3541 
  3542 lemma plus_int_eqvt:
  3543   fixes x::"int"
  3544   shows "pi\<bullet>(x + y) = (pi\<bullet>x) + (pi\<bullet>y)" 
  3545 by (simp add:perm_int_def) 
  3546 
  3547 lemma minus_int_eqvt:
  3548   fixes x::"int"
  3549   shows "pi\<bullet>(x - y) = (pi\<bullet>x) - (pi\<bullet>y)" 
  3550 by (simp add:perm_int_def) 
  3551 
  3552 lemma mult_int_eqvt:
  3553   fixes x::"int"
  3554   shows "pi\<bullet>(x * y) = (pi\<bullet>x) * (pi\<bullet>y)" 
  3555 by (simp add:perm_int_def) 
  3556 
  3557 lemma div_int_eqvt:
  3558   fixes x::"int"
  3559   shows "pi\<bullet>(x div y) = (pi\<bullet>x) div (pi\<bullet>y)" 
  3560 by (simp add:perm_int_def) 
  3561 
  3562 (*******************************************************)
  3563 (* Setup of the theorem attributes eqvt and eqvt_force *)
  3564 ML_file "nominal_thmdecls.ML"
  3565 setup "NominalThmDecls.setup"
  3566 
  3567 lemmas [eqvt] = 
  3568   (* connectives *)
  3569   if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
  3570   true_eqvt false_eqvt
  3571   imp_eqvt [folded HOL.induct_implies_def]
  3572   
  3573   (* datatypes *)
  3574   perm_unit.simps
  3575   perm_list.simps append_eqvt
  3576   perm_prod.simps
  3577   fst_eqvt snd_eqvt
  3578   perm_option.simps
  3579 
  3580   (* nats *)
  3581   Suc_eqvt Zero_nat_eqvt One_nat_eqvt min_nat_eqvt max_nat_eqvt
  3582   plus_nat_eqvt minus_nat_eqvt mult_nat_eqvt div_nat_eqvt
  3583   
  3584   (* ints *)
  3585   Zero_int_eqvt One_int_eqvt min_int_eqvt max_int_eqvt
  3586   plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
  3587   
  3588   (* sets *)
  3589   union_eqvt empty_eqvt insert_eqvt set_eqvt
  3590   
  3591  
  3592 (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
  3593 (* usual form of an eqvt-lemma, but they are needed for analysing       *)
  3594 (* permutations on nats and ints *)
  3595 lemmas [eqvt_force] = numeral_nat_eqvt numeral_int_eqvt neg_numeral_int_eqvt
  3596 
  3597 (***************************************)
  3598 (* setup for the individial atom-kinds *)
  3599 (* and nominal datatypes               *)
  3600 ML_file "nominal_atoms.ML"
  3601 
  3602 (************************************************************)
  3603 (* various tactics for analysing permutations, supports etc *)
  3604 ML_file "nominal_permeq.ML"
  3605 
  3606 method_setup perm_simp =
  3607   \<open>NominalPermeq.perm_simp_meth\<close>
  3608   \<open>simp rules and simprocs for analysing permutations\<close>
  3609 
  3610 method_setup perm_simp_debug =
  3611   \<open>NominalPermeq.perm_simp_meth_debug\<close>
  3612   \<open>simp rules and simprocs for analysing permutations including debugging facilities\<close>
  3613 
  3614 method_setup perm_extend_simp =
  3615   \<open>NominalPermeq.perm_extend_simp_meth\<close>
  3616   \<open>tactic for deciding equalities involving permutations\<close>
  3617 
  3618 method_setup perm_extend_simp_debug =
  3619   \<open>NominalPermeq.perm_extend_simp_meth_debug\<close>
  3620   \<open>tactic for deciding equalities involving permutations including debugging facilities\<close>
  3621 
  3622 method_setup supports_simp =
  3623   \<open>NominalPermeq.supports_meth\<close>
  3624   \<open>tactic for deciding whether something supports something else\<close>
  3625 
  3626 method_setup supports_simp_debug =
  3627   \<open>NominalPermeq.supports_meth_debug\<close>
  3628   \<open>tactic for deciding whether something supports something else including debugging facilities\<close>
  3629 
  3630 method_setup finite_guess =
  3631   \<open>NominalPermeq.finite_guess_meth\<close>
  3632   \<open>tactic for deciding whether something has finite support\<close>
  3633 
  3634 method_setup finite_guess_debug =
  3635   \<open>NominalPermeq.finite_guess_meth_debug\<close>
  3636   \<open>tactic for deciding whether something has finite support including debugging facilities\<close>
  3637 
  3638 method_setup fresh_guess =
  3639   \<open>NominalPermeq.fresh_guess_meth\<close>
  3640   \<open>tactic for deciding whether an atom is fresh for something\<close>
  3641 
  3642 method_setup fresh_guess_debug =
  3643   \<open>NominalPermeq.fresh_guess_meth_debug\<close>
  3644   \<open>tactic for deciding whether an atom is fresh for something including debugging facilities\<close>
  3645 
  3646 (*****************************************************************)
  3647 (* tactics for generating fresh names and simplifying fresh_funs *)
  3648 ML_file "nominal_fresh_fun.ML"
  3649 
  3650 method_setup generate_fresh = \<open>
  3651   Args.type_name {proper = true, strict = true} >>
  3652     (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s))
  3653 \<close> "generate a name fresh for all the variables in the goal"
  3654 
  3655 method_setup fresh_fun_simp = \<open>
  3656   Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >>
  3657     (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))
  3658 \<close> "delete one inner occurrence of fresh_fun"
  3659 
  3660 
  3661 (************************************************)
  3662 (* main file for constructing nominal datatypes *)
  3663 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
  3664   using assms ..
  3665 
  3666 ML_file "nominal_datatype.ML"
  3667 
  3668 (******************************************************)
  3669 (* primitive recursive functions on nominal datatypes *)
  3670 ML_file "nominal_primrec.ML"
  3671 
  3672 (****************************************************)
  3673 (* inductive definition involving nominal datatypes *)
  3674 ML_file "nominal_inductive.ML"
  3675 ML_file "nominal_inductive2.ML"
  3676 
  3677 (*****************************************)
  3678 (* setup for induction principles method *)
  3679 ML_file "nominal_induct.ML"
  3680 method_setup nominal_induct =
  3681   \<open>NominalInduct.nominal_induct_method\<close>
  3682   \<open>nominal induction\<close>
  3683 
  3684 end