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