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