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