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