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