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