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