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