src/HOL/Nominal/Nominal.thy
author urbanc
Thu Jan 05 12:09:26 2006 +0100 (2006-01-05)
changeset 18579 002d371401f5
parent 18578 68420ce82a0b
child 18600 20ad06db427b
permissions -rw-r--r--
changed the name of the type "nOption" to "noption".
     1 (* $Id$ *)
     2 
     3 theory nominal 
     4 imports Main
     5 uses
     6   ("nominal_atoms.ML")
     7   ("nominal_package.ML")
     8   ("nominal_induct.ML") 
     9   ("nominal_permeq.ML")
    10 begin 
    11 
    12 ML {* reset NameSpace.unique_names; *}
    13 
    14 section {* Permutations *}
    15 (*======================*)
    16 
    17 types 
    18   'x prm = "('x \<times> 'x) list"
    19 
    20 (* polymorphic operations for permutation and swapping*)
    21 consts 
    22   perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
    23   swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
    24 
    25 (* permutation on sets *)
    26 defs (overloaded)
    27   perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
    28 
    29 lemma perm_union:
    30   shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)"
    31   by (auto simp add: perm_set_def)
    32 
    33 (* permutation on units and products *)
    34 primrec (perm_unit)
    35   "pi\<bullet>()    = ()"
    36 
    37 primrec (perm_prod)
    38   "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
    39 
    40 lemma perm_fst:
    41   "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
    42  by (cases x, simp)
    43 
    44 lemma perm_snd:
    45   "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
    46  by (cases x, simp)
    47 
    48 (* permutation on lists *)
    49 primrec (perm_list)
    50   perm_nil_def:  "pi\<bullet>[]     = []"
    51   perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
    52 
    53 lemma perm_append:
    54   fixes pi :: "'x prm"
    55   and   l1 :: "'a list"
    56   and   l2 :: "'a list"
    57   shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
    58   by (induct l1, auto)
    59 
    60 lemma perm_rev:
    61   fixes pi :: "'x prm"
    62   and   l  :: "'a list"
    63   shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
    64   by (induct l, simp_all add: perm_append)
    65 
    66 (* permutation on functions *)
    67 defs (overloaded)
    68   perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
    69 
    70 (* permutation on bools *)
    71 primrec (perm_bool)
    72   perm_true_def:  "pi\<bullet>True  = True"
    73   perm_false_def: "pi\<bullet>False = False"
    74 
    75 lemma perm_bool:
    76   shows "pi\<bullet>(b::bool) = b"
    77   by (cases "b", auto)
    78 
    79 (* permutation on options *)
    80 primrec (perm_option)
    81   perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
    82   perm_none_def:  "pi\<bullet>None    = None"
    83 
    84 (* a "private" copy of the option type used in the abstraction function *)
    85 datatype 'a noption = nSome 'a | nNone
    86 
    87 primrec (perm_noption)
    88   perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
    89   perm_Nnone_def:  "pi\<bullet>nNone    = nNone"
    90 
    91 (* permutation on characters (used in strings) *)
    92 defs (overloaded)
    93   perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
    94 
    95 (* permutation on ints *)
    96 defs (overloaded)
    97   perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"
    98 
    99 (* permutation on nats *)
   100 defs (overloaded)
   101   perm_nat_def:    "pi\<bullet>(i::nat) \<equiv> i"
   102 
   103 section {* permutation equality *}
   104 (*==============================*)
   105 
   106 constdefs
   107   prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<triangleq> _ " [80,80] 80)
   108   "pi1 \<triangleq> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
   109 
   110 section {* Support, Freshness and Supports*}
   111 (*========================================*)
   112 constdefs
   113    supp :: "'a \<Rightarrow> ('x set)"  
   114    "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
   115 
   116    fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80)
   117    "a \<sharp> x \<equiv> a \<notin> supp x"
   118 
   119    supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
   120    "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
   121 
   122 lemma supp_fresh_iff: 
   123   fixes x :: "'a"
   124   shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
   125 apply(simp add: fresh_def)
   126 done
   127 
   128 lemma supp_unit:
   129   shows "supp () = {}"
   130   by (simp add: supp_def)
   131 
   132 lemma supp_set_empty:
   133   shows "supp {} = {}"
   134   by (force simp add: supp_def perm_set_def)
   135 
   136 lemma supp_singleton:
   137   shows "supp {x} = supp x"
   138   by (force simp add: supp_def perm_set_def)
   139 
   140 lemma supp_prod: 
   141   fixes x :: "'a"
   142   and   y :: "'b"
   143   shows "(supp (x,y)) = (supp x)\<union>(supp y)"
   144   by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
   145 
   146 lemma supp_list_nil:
   147   shows "supp [] = {}"
   148 apply(simp add: supp_def)
   149 done
   150 
   151 lemma supp_list_cons:
   152   fixes x  :: "'a"
   153   and   xs :: "'a list"
   154   shows "supp (x#xs) = (supp x)\<union>(supp xs)"
   155 apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
   156 done
   157 
   158 lemma supp_list_append:
   159   fixes xs :: "'a list"
   160   and   ys :: "'a list"
   161   shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
   162   by (induct xs, auto simp add: supp_list_nil supp_list_cons)
   163 
   164 lemma supp_list_rev:
   165   fixes xs :: "'a list"
   166   shows "supp (rev xs) = (supp xs)"
   167   by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
   168 
   169 lemma supp_bool:
   170   fixes x  :: "bool"
   171   shows "supp (x) = {}"
   172   apply(case_tac "x")
   173   apply(simp_all add: supp_def)
   174 done
   175 
   176 lemma supp_some:
   177   fixes x :: "'a"
   178   shows "supp (Some x) = (supp x)"
   179   apply(simp add: supp_def)
   180   done
   181 
   182 lemma supp_none:
   183   fixes x :: "'a"
   184   shows "supp (None) = {}"
   185   apply(simp add: supp_def)
   186   done
   187 
   188 lemma supp_int:
   189   fixes i::"int"
   190   shows "supp (i) = {}"
   191   apply(simp add: supp_def perm_int_def)
   192   done
   193 
   194 lemma fresh_set_empty:
   195   shows "a\<sharp>{}"
   196   by (simp add: fresh_def supp_set_empty)
   197 
   198 lemma fresh_singleton:
   199   shows "a\<sharp>{x} = a\<sharp>x"
   200   by (simp add: fresh_def supp_singleton)
   201 
   202 lemma fresh_prod:
   203   fixes a :: "'x"
   204   and   x :: "'a"
   205   and   y :: "'b"
   206   shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
   207   by (simp add: fresh_def supp_prod)
   208 
   209 lemma fresh_list_nil:
   210   fixes a :: "'x"
   211   shows "a\<sharp>[]"
   212   by (simp add: fresh_def supp_list_nil) 
   213 
   214 lemma fresh_list_cons:
   215   fixes a :: "'x"
   216   and   x :: "'a"
   217   and   xs :: "'a list"
   218   shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
   219   by (simp add: fresh_def supp_list_cons)
   220 
   221 lemma fresh_list_append:
   222   fixes a :: "'x"
   223   and   xs :: "'a list"
   224   and   ys :: "'a list"
   225   shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
   226   by (simp add: fresh_def supp_list_append)
   227 
   228 lemma fresh_list_rev:
   229   fixes a :: "'x"
   230   and   xs :: "'a list"
   231   shows "a\<sharp>(rev xs) = a\<sharp>xs"
   232   by (simp add: fresh_def supp_list_rev)
   233 
   234 lemma fresh_none:
   235   fixes a :: "'x"
   236   shows "a\<sharp>None"
   237   apply(simp add: fresh_def supp_none)
   238   done
   239 
   240 lemma fresh_some:
   241   fixes a :: "'x"
   242   and   x :: "'a"
   243   shows "a\<sharp>(Some x) = a\<sharp>x"
   244   apply(simp add: fresh_def supp_some)
   245   done
   246 
   247 
   248 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
   249 
   250 lemma fresh_unit_elim: "(a\<sharp>() \<Longrightarrow> PROP C) == PROP C"
   251   by (simp add: fresh_def supp_unit)
   252 
   253 lemma fresh_prod_elim: "(a\<sharp>(x,y) \<Longrightarrow> PROP C) == (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
   254   by rule (simp_all add: fresh_prod)
   255 
   256 
   257 section {* Abstract Properties for Permutations and  Atoms *}
   258 (*=========================================================*)
   259 
   260 (* properties for being a permutation type *)
   261 constdefs 
   262   "pt TYPE('a) TYPE('x) \<equiv> 
   263      (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
   264      (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
   265      (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
   266 
   267 (* properties for being an atom type *)
   268 constdefs 
   269   "at TYPE('x) \<equiv> 
   270      (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
   271      (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 
   272      (\<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> 
   273      (infinite (UNIV::'x set))"
   274 
   275 (* property of two atom-types being disjoint *)
   276 constdefs
   277   "disjoint TYPE('x) TYPE('y) \<equiv> 
   278        (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 
   279        (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
   280 
   281 (* composition property of two permutation on a type 'a *)
   282 constdefs
   283   "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
   284       (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 
   285 
   286 (* property of having finite support *)
   287 constdefs 
   288   "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
   289 
   290 section {* Lemmas about the atom-type properties*}
   291 (*==============================================*)
   292 
   293 lemma at1: 
   294   fixes x::"'x"
   295   assumes a: "at TYPE('x)"
   296   shows "([]::'x prm)\<bullet>x = x"
   297   using a by (simp add: at_def)
   298 
   299 lemma at2: 
   300   fixes a ::"'x"
   301   and   b ::"'x"
   302   and   x ::"'x"
   303   and   pi::"'x prm"
   304   assumes a: "at TYPE('x)"
   305   shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
   306   using a by (simp only: at_def)
   307 
   308 lemma at3: 
   309   fixes a ::"'x"
   310   and   b ::"'x"
   311   and   c ::"'x"
   312   assumes a: "at TYPE('x)"
   313   shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
   314   using a by (simp only: at_def)
   315 
   316 (* rules to calculate simple premutations *)
   317 lemmas at_calc = at2 at1 at3
   318 
   319 lemma at4: 
   320   assumes a: "at TYPE('x)"
   321   shows "infinite (UNIV::'x set)"
   322   using a by (simp add: at_def)
   323 
   324 lemma at_append:
   325   fixes pi1 :: "'x prm"
   326   and   pi2 :: "'x prm"
   327   and   c   :: "'x"
   328   assumes at: "at TYPE('x)" 
   329   shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
   330 proof (induct pi1)
   331   case Nil show ?case by (simp add: at1[OF at])
   332 next
   333   case (Cons x xs)
   334   have "(xs@pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)" by fact
   335   also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
   336   ultimately show ?case by (cases "x", simp add:  at2[OF at])
   337 qed
   338  
   339 lemma at_swap:
   340   fixes a :: "'x"
   341   and   b :: "'x"
   342   and   c :: "'x"
   343   assumes at: "at TYPE('x)" 
   344   shows "swap (a,b) (swap (a,b) c) = c"
   345   by (auto simp add: at3[OF at])
   346 
   347 lemma at_rev_pi:
   348   fixes pi :: "'x prm"
   349   and   c  :: "'x"
   350   assumes at: "at TYPE('x)"
   351   shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
   352 proof(induct pi)
   353   case Nil show ?case by (simp add: at1[OF at])
   354 next
   355   case (Cons x xs) thus ?case 
   356     by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
   357 qed
   358 
   359 lemma at_pi_rev:
   360   fixes pi :: "'x prm"
   361   and   x  :: "'x"
   362   assumes at: "at TYPE('x)"
   363   shows "pi\<bullet>((rev pi)\<bullet>x) = x"
   364   by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
   365 
   366 lemma at_bij1: 
   367   fixes pi :: "'x prm"
   368   and   x  :: "'x"
   369   and   y  :: "'x"
   370   assumes at: "at TYPE('x)"
   371   and     a:  "(pi\<bullet>x) = y"
   372   shows   "x=(rev pi)\<bullet>y"
   373 proof -
   374   from a have "y=(pi\<bullet>x)" by (rule sym)
   375   thus ?thesis by (simp only: at_rev_pi[OF at])
   376 qed
   377 
   378 lemma at_bij2: 
   379   fixes pi :: "'x prm"
   380   and   x  :: "'x"
   381   and   y  :: "'x"
   382   assumes at: "at TYPE('x)"
   383   and     a:  "((rev pi)\<bullet>x) = y"
   384   shows   "x=pi\<bullet>y"
   385 proof -
   386   from a have "y=((rev pi)\<bullet>x)" by (rule sym)
   387   thus ?thesis by (simp only: at_pi_rev[OF at])
   388 qed
   389 
   390 lemma at_bij:
   391   fixes pi :: "'x prm"
   392   and   x  :: "'x"
   393   and   y  :: "'x"
   394   assumes at: "at TYPE('x)"
   395   shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
   396 proof 
   397   assume "pi\<bullet>x = pi\<bullet>y" 
   398   hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
   399   thus "x=y" by (simp only: at_rev_pi[OF at])
   400 next
   401   assume "x=y"
   402   thus "pi\<bullet>x = pi\<bullet>y" by simp
   403 qed
   404 
   405 lemma at_supp:
   406   fixes x :: "'x"
   407   assumes at: "at TYPE('x)"
   408   shows "supp x = {x}"
   409 proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
   410   assume f: "finite {b::'x. b \<noteq> x}"
   411   have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
   412   have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
   413   from f a1 a2 show False by force
   414 qed
   415 
   416 lemma at_fresh:
   417   fixes a :: "'x"
   418   and   b :: "'x"
   419   assumes at: "at TYPE('x)"
   420   shows "(a\<sharp>b) = (a\<noteq>b)" 
   421   by (simp add: at_supp[OF at] fresh_def)
   422 
   423 lemma at_prm_fresh[rule_format]:
   424   fixes c :: "'x"
   425   and   pi:: "'x prm"
   426   assumes at: "at TYPE('x)"
   427   shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
   428 apply(induct pi)
   429 apply(simp add: at1[OF at]) 
   430 apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
   431 done
   432 
   433 lemma at_prm_rev_eq:
   434   fixes pi1 :: "'x prm"
   435   and   pi2 :: "'x prm"
   436   assumes at: "at TYPE('x)"
   437   shows a: "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
   438 proof (simp add: prm_eq_def, auto)
   439   fix x
   440   assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   441   hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
   442   hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
   443   hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
   444   thus "pi1\<bullet>x  =  pi2\<bullet>x" by simp
   445 next
   446   fix x
   447   assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
   448   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
   449   hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
   450   hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
   451   thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
   452 qed
   453   
   454 lemma at_prm_rev_eq1:
   455   fixes pi1 :: "'x prm"
   456   and   pi2 :: "'x prm"
   457   assumes at: "at TYPE('x)"
   458   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
   459   by (simp add: at_prm_rev_eq[OF at])
   460 
   461 lemma at_ds1:
   462   fixes a  :: "'x"
   463   assumes at: "at TYPE('x)"
   464   shows "[(a,a)] \<triangleq> []"
   465   by (force simp add: prm_eq_def at_calc[OF at])
   466 
   467 lemma at_ds2: 
   468   fixes pi :: "'x prm"
   469   and   a  :: "'x"
   470   and   b  :: "'x"
   471   assumes at: "at TYPE('x)"
   472   shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<triangleq> ([(a,b)]@pi)"
   473   by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
   474       at_rev_pi[OF at] at_calc[OF at])
   475 
   476 lemma at_ds3: 
   477   fixes a  :: "'x"
   478   and   b  :: "'x"
   479   and   c  :: "'x"
   480   assumes at: "at TYPE('x)"
   481   and     a:  "distinct [a,b,c]"
   482   shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]"
   483   using a by (force simp add: prm_eq_def at_calc[OF at])
   484 
   485 lemma at_ds4: 
   486   fixes a  :: "'x"
   487   and   b  :: "'x"
   488   and   pi  :: "'x prm"
   489   assumes at: "at TYPE('x)"
   490   shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)"
   491   by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
   492       at_pi_rev[OF at] at_rev_pi[OF at])
   493 
   494 lemma at_ds5: 
   495   fixes a  :: "'x"
   496   and   b  :: "'x"
   497   assumes at: "at TYPE('x)"
   498   shows "[(a,b)] \<triangleq> [(b,a)]"
   499   by (force simp add: prm_eq_def at_calc[OF at])
   500 
   501 lemma at_ds6: 
   502   fixes a  :: "'x"
   503   and   b  :: "'x"
   504   and   c  :: "'x"
   505   assumes at: "at TYPE('x)"
   506   and     a: "distinct [a,b,c]"
   507   shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]"
   508   using a by (force simp add: prm_eq_def at_calc[OF at])
   509 
   510 lemma at_ds7:
   511   fixes pi :: "'x prm"
   512   assumes at: "at TYPE('x)"
   513   shows "((rev pi)@pi) \<triangleq> []"
   514   by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
   515 
   516 lemma at_ds8_aux:
   517   fixes pi :: "'x prm"
   518   and   a  :: "'x"
   519   and   b  :: "'x"
   520   and   c  :: "'x"
   521   assumes at: "at TYPE('x)"
   522   shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
   523   by (force simp add: at_calc[OF at] at_bij[OF at])
   524 
   525 lemma at_ds8: 
   526   fixes pi1 :: "'x prm"
   527   and   pi2 :: "'x prm"
   528   and   a  :: "'x"
   529   and   b  :: "'x"
   530   assumes at: "at TYPE('x)"
   531   shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)"
   532 apply(induct_tac pi2)
   533 apply(simp add: prm_eq_def)
   534 apply(auto simp add: prm_eq_def)
   535 apply(simp add: at2[OF at])
   536 apply(drule_tac x="aa" in spec)
   537 apply(drule sym)
   538 apply(simp)
   539 apply(simp add: at_append[OF at])
   540 apply(simp add: at2[OF at])
   541 apply(simp add: at_ds8_aux[OF at])
   542 done
   543 
   544 lemma at_ds9: 
   545   fixes pi1 :: "'x prm"
   546   and   pi2 :: "'x prm"
   547   and   a  :: "'x"
   548   and   b  :: "'x"
   549   assumes at: "at TYPE('x)"
   550   shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
   551 apply(induct_tac pi2)
   552 apply(simp add: prm_eq_def)
   553 apply(auto simp add: prm_eq_def)
   554 apply(simp add: at_append[OF at])
   555 apply(simp add: at2[OF at] at1[OF at])
   556 apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
   557 apply(drule sym)
   558 apply(simp)
   559 apply(simp add: at_ds8_aux[OF at])
   560 apply(simp add: at_rev_pi[OF at])
   561 done
   562 
   563 --"there always exists an atom not being in a finite set"
   564 lemma ex_in_inf:
   565   fixes   A::"'x set"
   566   assumes at: "at TYPE('x)"
   567   and     fs: "finite A"
   568   shows "\<exists>c::'x. c\<notin>A"
   569 proof -
   570   from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
   571     by (simp add: Diff_infinite_finite)
   572   hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
   573   hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
   574   thus "\<exists>c::'x. c\<notin>A" by force
   575 qed
   576 
   577 --"there always exists a fresh name for an object with finite support"
   578 lemma at_exists_fresh: 
   579   fixes  x :: "'a"
   580   assumes at: "at TYPE('x)"
   581   and     fs: "finite ((supp x)::'x set)"
   582   shows "\<exists>c::'x. c\<sharp>x"
   583   by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
   584 
   585 --"the at-props imply the pt-props"
   586 lemma at_pt_inst:
   587   assumes at: "at TYPE('x)"
   588   shows "pt TYPE('x) TYPE('x)"
   589 apply(auto simp only: pt_def)
   590 apply(simp only: at1[OF at])
   591 apply(simp only: at_append[OF at]) 
   592 apply(simp only: prm_eq_def)
   593 done
   594 
   595 section {* finite support properties *}
   596 (*===================================*)
   597 
   598 lemma fs1:
   599   fixes x :: "'a"
   600   assumes a: "fs TYPE('a) TYPE('x)"
   601   shows "finite ((supp x)::'x set)"
   602   using a by (simp add: fs_def)
   603 
   604 lemma fs_at_inst:
   605   fixes a :: "'x"
   606   assumes at: "at TYPE('x)"
   607   shows "fs TYPE('x) TYPE('x)"
   608 apply(simp add: fs_def) 
   609 apply(simp add: at_supp[OF at])
   610 done
   611 
   612 lemma fs_unit_inst:
   613   shows "fs TYPE(unit) TYPE('x)"
   614 apply(simp add: fs_def)
   615 apply(simp add: supp_unit)
   616 done
   617 
   618 lemma fs_prod_inst:
   619   assumes fsa: "fs TYPE('a) TYPE('x)"
   620   and     fsb: "fs TYPE('b) TYPE('x)"
   621   shows "fs TYPE('a\<times>'b) TYPE('x)"
   622 apply(unfold fs_def)
   623 apply(auto simp add: supp_prod)
   624 apply(rule fs1[OF fsa])
   625 apply(rule fs1[OF fsb])
   626 done
   627 
   628 lemma fs_list_inst:
   629   assumes fs: "fs TYPE('a) TYPE('x)"
   630   shows "fs TYPE('a list) TYPE('x)"
   631 apply(simp add: fs_def, rule allI)
   632 apply(induct_tac x)
   633 apply(simp add: supp_list_nil)
   634 apply(simp add: supp_list_cons)
   635 apply(rule fs1[OF fs])
   636 done
   637 
   638 lemma fs_option_inst:
   639   assumes fs: "fs TYPE('a) TYPE('x)"
   640   shows "fs TYPE('a option) TYPE('x)"
   641 apply(simp add: fs_def, rule allI)
   642 apply(case_tac x)
   643 apply(simp add: supp_none)
   644 apply(simp add: supp_some)
   645 apply(rule fs1[OF fs])
   646 done
   647 
   648 section {* Lemmas about the permutation properties *}
   649 (*=================================================*)
   650 
   651 lemma pt1:
   652   fixes x::"'a"
   653   assumes a: "pt TYPE('a) TYPE('x)"
   654   shows "([]::'x prm)\<bullet>x = x"
   655   using a by (simp add: pt_def)
   656 
   657 lemma pt2: 
   658   fixes pi1::"'x prm"
   659   and   pi2::"'x prm"
   660   and   x  ::"'a"
   661   assumes a: "pt TYPE('a) TYPE('x)"
   662   shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
   663   using a by (simp add: pt_def)
   664 
   665 lemma pt3:
   666   fixes pi1::"'x prm"
   667   and   pi2::"'x prm"
   668   and   x  ::"'a"
   669   assumes a: "pt TYPE('a) TYPE('x)"
   670   shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
   671   using a by (simp add: pt_def)
   672 
   673 lemma pt3_rev:
   674   fixes pi1::"'x prm"
   675   and   pi2::"'x prm"
   676   and   x  ::"'a"
   677   assumes pt: "pt TYPE('a) TYPE('x)"
   678   and     at: "at TYPE('x)"
   679   shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
   680   by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
   681 
   682 section {* composition properties *}
   683 (* ============================== *)
   684 lemma cp1:
   685   fixes pi1::"'x prm"
   686   and   pi2::"'y prm"
   687   and   x  ::"'a"
   688   assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
   689   shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
   690   using cp by (simp add: cp_def)
   691 
   692 lemma cp_pt_inst:
   693   assumes pt: "pt TYPE('a) TYPE('x)"
   694   and     at: "at TYPE('x)"
   695   shows "cp TYPE('a) TYPE('x) TYPE('x)"
   696 apply(auto simp add: cp_def pt2[OF pt,symmetric])
   697 apply(rule pt3[OF pt])
   698 apply(rule at_ds8[OF at])
   699 done
   700 
   701 section {* permutation type instances *}
   702 (* ===================================*)
   703 
   704 lemma pt_set_inst:
   705   assumes pt: "pt TYPE('a) TYPE('x)"
   706   shows  "pt TYPE('a set) TYPE('x)"
   707 apply(simp add: pt_def)
   708 apply(simp_all add: perm_set_def)
   709 apply(simp add: pt1[OF pt])
   710 apply(force simp add: pt2[OF pt] pt3[OF pt])
   711 done
   712 
   713 lemma pt_list_nil: 
   714   fixes xs :: "'a list"
   715   assumes pt: "pt TYPE('a) TYPE ('x)"
   716   shows "([]::'x prm)\<bullet>xs = xs" 
   717 apply(induct_tac xs)
   718 apply(simp_all add: pt1[OF pt])
   719 done
   720 
   721 lemma pt_list_append: 
   722   fixes pi1 :: "'x prm"
   723   and   pi2 :: "'x prm"
   724   and   xs  :: "'a list"
   725   assumes pt: "pt TYPE('a) TYPE ('x)"
   726   shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
   727 apply(induct_tac xs)
   728 apply(simp_all add: pt2[OF pt])
   729 done
   730 
   731 lemma pt_list_prm_eq: 
   732   fixes pi1 :: "'x prm"
   733   and   pi2 :: "'x prm"
   734   and   xs  :: "'a list"
   735   assumes pt: "pt TYPE('a) TYPE ('x)"
   736   shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
   737 apply(induct_tac xs)
   738 apply(simp_all add: prm_eq_def pt3[OF pt])
   739 done
   740 
   741 lemma pt_list_inst:
   742   assumes pt: "pt TYPE('a) TYPE('x)"
   743   shows  "pt TYPE('a list) TYPE('x)"
   744 apply(auto simp only: pt_def)
   745 apply(rule pt_list_nil[OF pt])
   746 apply(rule pt_list_append[OF pt])
   747 apply(rule pt_list_prm_eq[OF pt],assumption)
   748 done
   749 
   750 lemma pt_unit_inst:
   751   shows  "pt TYPE(unit) TYPE('x)"
   752   by (simp add: pt_def)
   753 
   754 lemma pt_prod_inst:
   755   assumes pta: "pt TYPE('a) TYPE('x)"
   756   and     ptb: "pt TYPE('b) TYPE('x)"
   757   shows  "pt TYPE('a \<times> 'b) TYPE('x)"
   758   apply(auto simp add: pt_def)
   759   apply(rule pt1[OF pta])
   760   apply(rule pt1[OF ptb])
   761   apply(rule pt2[OF pta])
   762   apply(rule pt2[OF ptb])
   763   apply(rule pt3[OF pta],assumption)
   764   apply(rule pt3[OF ptb],assumption)
   765   done
   766 
   767 lemma pt_fun_inst:
   768   assumes pta: "pt TYPE('a) TYPE('x)"
   769   and     ptb: "pt TYPE('b) TYPE('x)"
   770   and     at:  "at TYPE('x)"
   771   shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
   772 apply(auto simp only: pt_def)
   773 apply(simp_all add: perm_fun_def)
   774 apply(simp add: pt1[OF pta] pt1[OF ptb])
   775 apply(simp add: pt2[OF pta] pt2[OF ptb])
   776 apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*)
   777 apply(simp add: pt3[OF pta] pt3[OF ptb])
   778 (*A*)
   779 apply(simp add: at_prm_rev_eq[OF at])
   780 done
   781 
   782 lemma pt_option_inst:
   783   assumes pta: "pt TYPE('a) TYPE('x)"
   784   shows  "pt TYPE('a option) TYPE('x)"
   785 apply(auto simp only: pt_def)
   786 apply(case_tac "x")
   787 apply(simp_all add: pt1[OF pta])
   788 apply(case_tac "x")
   789 apply(simp_all add: pt2[OF pta])
   790 apply(case_tac "x")
   791 apply(simp_all add: pt3[OF pta])
   792 done
   793 
   794 lemma pt_noption_inst:
   795   assumes pta: "pt TYPE('a) TYPE('x)"
   796   shows  "pt TYPE('a noption) TYPE('x)"
   797 apply(auto simp only: pt_def)
   798 apply(case_tac "x")
   799 apply(simp_all add: pt1[OF pta])
   800 apply(case_tac "x")
   801 apply(simp_all add: pt2[OF pta])
   802 apply(case_tac "x")
   803 apply(simp_all add: pt3[OF pta])
   804 done
   805 
   806 section {* further lemmas for permutation types *}
   807 (*==============================================*)
   808 
   809 lemma pt_rev_pi:
   810   fixes pi :: "'x prm"
   811   and   x  :: "'a"
   812   assumes pt: "pt TYPE('a) TYPE('x)"
   813   and     at: "at TYPE('x)"
   814   shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
   815 proof -
   816   have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at])
   817   hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
   818   thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
   819 qed
   820 
   821 lemma pt_pi_rev:
   822   fixes pi :: "'x prm"
   823   and   x  :: "'a"
   824   assumes pt: "pt TYPE('a) TYPE('x)"
   825   and     at: "at TYPE('x)"
   826   shows "pi\<bullet>((rev pi)\<bullet>x) = x"
   827   by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
   828 
   829 lemma pt_bij1: 
   830   fixes pi :: "'x prm"
   831   and   x  :: "'a"
   832   and   y  :: "'a"
   833   assumes pt: "pt TYPE('a) TYPE('x)"
   834   and     at: "at TYPE('x)"
   835   and     a:  "(pi\<bullet>x) = y"
   836   shows   "x=(rev pi)\<bullet>y"
   837 proof -
   838   from a have "y=(pi\<bullet>x)" by (rule sym)
   839   thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
   840 qed
   841 
   842 lemma pt_bij2: 
   843   fixes pi :: "'x prm"
   844   and   x  :: "'a"
   845   and   y  :: "'a"
   846   assumes pt: "pt TYPE('a) TYPE('x)"
   847   and     at: "at TYPE('x)"
   848   and     a:  "x = (rev pi)\<bullet>y"
   849   shows   "(pi\<bullet>x)=y"
   850   using a by (simp add: pt_pi_rev[OF pt, OF at])
   851 
   852 lemma pt_bij:
   853   fixes pi :: "'x prm"
   854   and   x  :: "'a"
   855   and   y  :: "'a"
   856   assumes pt: "pt TYPE('a) TYPE('x)"
   857   and     at: "at TYPE('x)"
   858   shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
   859 proof 
   860   assume "pi\<bullet>x = pi\<bullet>y" 
   861   hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 
   862   thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
   863 next
   864   assume "x=y"
   865   thus "pi\<bullet>x = pi\<bullet>y" by simp
   866 qed
   867 
   868 lemma pt_bij3:
   869   fixes pi :: "'x prm"
   870   and   x  :: "'a"
   871   and   y  :: "'a"
   872   assumes a:  "x=y"
   873   shows "(pi\<bullet>x = pi\<bullet>y)"
   874 using a by simp 
   875 
   876 lemma pt_bij4:
   877   fixes pi :: "'x prm"
   878   and   x  :: "'a"
   879   and   y  :: "'a"
   880   assumes pt: "pt TYPE('a) TYPE('x)"
   881   and     at: "at TYPE('x)"
   882   and     a:  "pi\<bullet>x = pi\<bullet>y"
   883   shows "x = y"
   884 using a by (simp add: pt_bij[OF pt, OF at])
   885 
   886 lemma pt_swap_bij:
   887   fixes a  :: "'x"
   888   and   b  :: "'x"
   889   and   x  :: "'a"
   890   assumes pt: "pt TYPE('a) TYPE('x)"
   891   and     at: "at TYPE('x)"
   892   shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
   893   by (rule pt_bij2[OF pt, OF at], simp)
   894 
   895 lemma pt_set_bij1:
   896   fixes pi :: "'x prm"
   897   and   x  :: "'a"
   898   and   X  :: "'a set"
   899   assumes pt: "pt TYPE('a) TYPE('x)"
   900   and     at: "at TYPE('x)"
   901   shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
   902   by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   903 
   904 lemma pt_set_bij1a:
   905   fixes pi :: "'x prm"
   906   and   x  :: "'a"
   907   and   X  :: "'a set"
   908   assumes pt: "pt TYPE('a) TYPE('x)"
   909   and     at: "at TYPE('x)"
   910   shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
   911   by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   912 
   913 lemma pt_set_bij:
   914   fixes pi :: "'x prm"
   915   and   x  :: "'a"
   916   and   X  :: "'a set"
   917   assumes pt: "pt TYPE('a) TYPE('x)"
   918   and     at: "at TYPE('x)"
   919   shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
   920   by (simp add: perm_set_def pt_bij[OF pt, OF at])
   921 
   922 lemma pt_set_bij2:
   923   fixes pi :: "'x prm"
   924   and   x  :: "'a"
   925   and   X  :: "'a set"
   926   assumes pt: "pt TYPE('a) TYPE('x)"
   927   and     at: "at TYPE('x)"
   928   and     a:  "x\<in>X"
   929   shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
   930   using a by (simp add: pt_set_bij[OF pt, OF at])
   931 
   932 lemma pt_set_bij2a:
   933   fixes pi :: "'x prm"
   934   and   x  :: "'a"
   935   and   X  :: "'a set"
   936   assumes pt: "pt TYPE('a) TYPE('x)"
   937   and     at: "at TYPE('x)"
   938   and     a:  "x\<in>((rev pi)\<bullet>X)"
   939   shows "(pi\<bullet>x)\<in>X"
   940   using a by (simp add: pt_set_bij1[OF pt, OF at])
   941 
   942 lemma pt_set_bij3:
   943   fixes pi :: "'x prm"
   944   and   x  :: "'a"
   945   and   X  :: "'a set"
   946   assumes pt: "pt TYPE('a) TYPE('x)"
   947   and     at: "at TYPE('x)"
   948   shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
   949 apply(case_tac "x\<in>X = True")
   950 apply(auto)
   951 done
   952 
   953 lemma pt_subseteq_eqvt:
   954   fixes pi :: "'x prm"
   955   and   Y  :: "'a set"
   956   and   X  :: "'a set"
   957   assumes pt: "pt TYPE('a) TYPE('x)"
   958   and     at: "at TYPE('x)"
   959   shows "((pi\<bullet>X)\<subseteq>(pi\<bullet>Y)) = (X\<subseteq>Y)"
   960 proof (auto)
   961   fix x::"'a"
   962   assume a: "(pi\<bullet>X)\<subseteq>(pi\<bullet>Y)"
   963   and    "x\<in>X"
   964   hence  "(pi\<bullet>x)\<in>(pi\<bullet>X)" by (simp add: pt_set_bij[OF pt, OF at])
   965   with a have "(pi\<bullet>x)\<in>(pi\<bullet>Y)" by force
   966   thus "x\<in>Y" by (simp add: pt_set_bij[OF pt, OF at])
   967 next
   968   fix x::"'a"
   969   assume a: "X\<subseteq>Y"
   970   and    "x\<in>(pi\<bullet>X)"
   971   thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
   972 qed
   973 
   974 -- "some helper lemmas for the pt_perm_supp_ineq lemma"
   975 lemma Collect_permI: 
   976   fixes pi :: "'x prm"
   977   and   x  :: "'a"
   978   assumes a: "\<forall>x. (P1 x = P2 x)" 
   979   shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}"
   980   using a by force
   981 
   982 lemma Infinite_cong:
   983   assumes a: "X = Y"
   984   shows "infinite X = infinite Y"
   985   using a by (simp)
   986 
   987 lemma pt_set_eq_ineq:
   988   fixes pi :: "'y prm"
   989   assumes pt: "pt TYPE('x) TYPE('y)"
   990   and     at: "at TYPE('y)"
   991   shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}"
   992   by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
   993 
   994 lemma pt_inject_on_ineq:
   995   fixes X  :: "'y set"
   996   and   pi :: "'x prm"
   997   assumes pt: "pt TYPE('y) TYPE('x)"
   998   and     at: "at TYPE('x)"
   999   shows "inj_on (perm pi) X"
  1000 proof (unfold inj_on_def, intro strip)
  1001   fix x::"'y" and y::"'y"
  1002   assume "pi\<bullet>x = pi\<bullet>y"
  1003   thus "x=y" by (simp add: pt_bij[OF pt, OF at])
  1004 qed
  1005 
  1006 lemma pt_set_finite_ineq: 
  1007   fixes X  :: "'x set"
  1008   and   pi :: "'y prm"
  1009   assumes pt: "pt TYPE('x) TYPE('y)"
  1010   and     at: "at TYPE('y)"
  1011   shows "finite (pi\<bullet>X) = finite X"
  1012 proof -
  1013   have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
  1014   show ?thesis
  1015   proof (rule iffI)
  1016     assume "finite (pi\<bullet>X)"
  1017     hence "finite (perm pi ` X)" using image by (simp)
  1018     thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
  1019   next
  1020     assume "finite X"
  1021     hence "finite (perm pi ` X)" by (rule finite_imageI)
  1022     thus "finite (pi\<bullet>X)" using image by (simp)
  1023   qed
  1024 qed
  1025 
  1026 lemma pt_set_infinite_ineq: 
  1027   fixes X  :: "'x set"
  1028   and   pi :: "'y prm"
  1029   assumes pt: "pt TYPE('x) TYPE('y)"
  1030   and     at: "at TYPE('y)"
  1031   shows "infinite (pi\<bullet>X) = infinite X"
  1032 using pt at by (simp add: pt_set_finite_ineq)
  1033 
  1034 lemma pt_perm_supp_ineq:
  1035   fixes  pi  :: "'x prm"
  1036   and    x   :: "'a"
  1037   assumes pta: "pt TYPE('a) TYPE('x)"
  1038   and     ptb: "pt TYPE('y) TYPE('x)"
  1039   and     at:  "at TYPE('x)"
  1040   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1041   shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
  1042 proof -
  1043   have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
  1044   also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
  1045   proof (rule Collect_permI, rule allI, rule iffI)
  1046     fix a
  1047     assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
  1048     hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1049     thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
  1050   next
  1051     fix a
  1052     assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
  1053     hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
  1054     thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
  1055       by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  1056   qed
  1057   also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 
  1058     by (simp add: pt_set_eq_ineq[OF ptb, OF at])
  1059   also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1060     by (simp add: pt_bij[OF pta, OF at])
  1061   also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  1062   proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
  1063     fix a::"'y" and b::"'y"
  1064     have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
  1065       by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
  1066     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
  1067   qed
  1068   finally show "?LHS = ?RHS" by (simp add: supp_def) 
  1069 qed
  1070 
  1071 lemma pt_perm_supp:
  1072   fixes  pi  :: "'x prm"
  1073   and    x   :: "'a"
  1074   assumes pt: "pt TYPE('a) TYPE('x)"
  1075   and     at: "at TYPE('x)"
  1076   shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
  1077 apply(rule pt_perm_supp_ineq)
  1078 apply(rule pt)
  1079 apply(rule at_pt_inst)
  1080 apply(rule at)+
  1081 apply(rule cp_pt_inst)
  1082 apply(rule pt)
  1083 apply(rule at)
  1084 done
  1085 
  1086 lemma pt_supp_finite_pi:
  1087   fixes  pi  :: "'x prm"
  1088   and    x   :: "'a"
  1089   assumes pt: "pt TYPE('a) TYPE('x)"
  1090   and     at: "at TYPE('x)"
  1091   and     f: "finite ((supp x)::'x set)"
  1092   shows "finite ((supp (pi\<bullet>x))::'x set)"
  1093 apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
  1094 apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
  1095 apply(rule f)
  1096 done
  1097 
  1098 lemma pt_fresh_left_ineq:  
  1099   fixes  pi :: "'x prm"
  1100   and     x :: "'a"
  1101   and     a :: "'y"
  1102   assumes pta: "pt TYPE('a) TYPE('x)"
  1103   and     ptb: "pt TYPE('y) TYPE('x)"
  1104   and     at:  "at TYPE('x)"
  1105   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1106   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1107 apply(simp add: fresh_def)
  1108 apply(simp add: pt_set_bij1[OF ptb, OF at])
  1109 apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1110 done
  1111 
  1112 lemma pt_fresh_right_ineq:  
  1113   fixes  pi :: "'x prm"
  1114   and     x :: "'a"
  1115   and     a :: "'y"
  1116   assumes pta: "pt TYPE('a) TYPE('x)"
  1117   and     ptb: "pt TYPE('y) TYPE('x)"
  1118   and     at:  "at TYPE('x)"
  1119   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1120   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1121 apply(simp add: fresh_def)
  1122 apply(simp add: pt_set_bij1[OF ptb, OF at])
  1123 apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
  1124 done
  1125 
  1126 lemma pt_fresh_bij_ineq:
  1127   fixes  pi :: "'x prm"
  1128   and     x :: "'a"
  1129   and     a :: "'y"
  1130   assumes pta: "pt TYPE('a) TYPE('x)"
  1131   and     ptb: "pt TYPE('y) TYPE('x)"
  1132   and     at:  "at TYPE('x)"
  1133   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  1134   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1135 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  1136 apply(simp add: pt_rev_pi[OF ptb, OF at])
  1137 done
  1138 
  1139 lemma pt_fresh_left:  
  1140   fixes  pi :: "'x prm"
  1141   and     x :: "'a"
  1142   and     a :: "'x"
  1143   assumes pt: "pt TYPE('a) TYPE('x)"
  1144   and     at: "at TYPE('x)"
  1145   shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
  1146 apply(rule pt_fresh_left_ineq)
  1147 apply(rule pt)
  1148 apply(rule at_pt_inst)
  1149 apply(rule at)+
  1150 apply(rule cp_pt_inst)
  1151 apply(rule pt)
  1152 apply(rule at)
  1153 done
  1154 
  1155 lemma pt_fresh_right:  
  1156   fixes  pi :: "'x prm"
  1157   and     x :: "'a"
  1158   and     a :: "'x"
  1159   assumes pt: "pt TYPE('a) TYPE('x)"
  1160   and     at: "at TYPE('x)"
  1161   shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
  1162 apply(rule pt_fresh_right_ineq)
  1163 apply(rule pt)
  1164 apply(rule at_pt_inst)
  1165 apply(rule at)+
  1166 apply(rule cp_pt_inst)
  1167 apply(rule pt)
  1168 apply(rule at)
  1169 done
  1170 
  1171 lemma pt_fresh_bij:
  1172   fixes  pi :: "'x prm"
  1173   and     x :: "'a"
  1174   and     a :: "'x"
  1175   assumes pt: "pt TYPE('a) TYPE('x)"
  1176   and     at: "at TYPE('x)"
  1177   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
  1178 apply(rule pt_fresh_bij_ineq)
  1179 apply(rule pt)
  1180 apply(rule at_pt_inst)
  1181 apply(rule at)+
  1182 apply(rule cp_pt_inst)
  1183 apply(rule pt)
  1184 apply(rule at)
  1185 done
  1186 
  1187 lemma pt_fresh_bij1:
  1188   fixes  pi :: "'x prm"
  1189   and     x :: "'a"
  1190   and     a :: "'x"
  1191   assumes pt: "pt TYPE('a) TYPE('x)"
  1192   and     at: "at TYPE('x)"
  1193   and     a:  "a\<sharp>x"
  1194   shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
  1195 using a by (simp add: pt_fresh_bij[OF pt, OF at])
  1196 
  1197 lemma pt_perm_fresh1:
  1198   fixes a :: "'x"
  1199   and   b :: "'x"
  1200   and   x :: "'a"
  1201   assumes pt: "pt TYPE('a) TYPE('x)"
  1202   and     at: "at TYPE ('x)"
  1203   and     a1: "\<not>(a\<sharp>x)"
  1204   and     a2: "b\<sharp>x"
  1205   shows "[(a,b)]\<bullet>x \<noteq> x"
  1206 proof
  1207   assume neg: "[(a,b)]\<bullet>x = x"
  1208   from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 
  1209   from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 
  1210   from a1' a2' have a3: "a\<noteq>b" by force
  1211   from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
  1212     by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
  1213   hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
  1214   hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
  1215   with a2' neg show False by simp
  1216 qed
  1217 
  1218 -- "three helper lemmas for the perm_fresh_fresh-lemma"
  1219 lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
  1220   by (auto)
  1221 
  1222 lemma infinite_or_neg_infinite:
  1223   assumes h:"infinite (UNIV::'a set)"
  1224   shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
  1225 proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
  1226   assume j:"finite {b::'a. P b}"
  1227   have "infinite ((UNIV::'a set) - {b::'a. P b})"
  1228     using Diff_infinite_finite[OF j h] by auto
  1229   thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
  1230 next
  1231   assume j:"infinite {b::'a. P b}"
  1232   thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
  1233 qed
  1234 
  1235 --"the co-set of a finite set is infinte"
  1236 lemma finite_infinite:
  1237   assumes a: "finite {b::'x. P b}"
  1238   and     b: "infinite (UNIV::'x set)"        
  1239   shows "infinite {b. \<not>P b}"
  1240   using a and infinite_or_neg_infinite[OF b] by simp
  1241 
  1242 lemma pt_fresh_fresh:
  1243   fixes   x :: "'a"
  1244   and     a :: "'x"
  1245   and     b :: "'x"
  1246   assumes pt: "pt TYPE('a) TYPE('x)"
  1247   and     at: "at TYPE ('x)"
  1248   and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
  1249   shows "[(a,b)]\<bullet>x=x"
  1250 proof (cases "a=b")
  1251   assume c1: "a=b"
  1252   have "[(a,a)] \<triangleq> []" by (rule at_ds1[OF at])
  1253   hence "[(a,b)] \<triangleq> []" using c1 by simp
  1254   hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
  1255   thus ?thesis by (simp only: pt1[OF pt])
  1256 next
  1257   assume c2: "a\<noteq>b"
  1258   from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1259   from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  1260   from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 
  1261     by (force simp only: Collect_disj_eq)
  1262   have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 
  1263     by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
  1264   hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
  1265     by (force dest: Diff_infinite_finite)
  1266   hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}" 
  1267     by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
  1268   hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
  1269   then obtain c 
  1270     where eq1: "[(a,c)]\<bullet>x = x" 
  1271       and eq2: "[(b,c)]\<bullet>x = x" 
  1272       and ineq: "a\<noteq>c \<and> b\<noteq>c"
  1273     by (force)
  1274   hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
  1275   hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
  1276   from c2 ineq have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" by (simp add: at_ds3[OF at])
  1277   hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
  1278   thus ?thesis using eq3 by simp
  1279 qed
  1280 
  1281 lemma pt_perm_compose:
  1282   fixes pi1 :: "'x prm"
  1283   and   pi2 :: "'x prm"
  1284   and   x  :: "'a"
  1285   assumes pt: "pt TYPE('a) TYPE('x)"
  1286   and     at: "at TYPE('x)"
  1287   shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
  1288 proof -
  1289   have "(pi2@pi1) \<triangleq> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
  1290   hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
  1291   thus ?thesis by (simp add: pt2[OF pt])
  1292 qed
  1293 
  1294 lemma pt_perm_compose_rev:
  1295   fixes pi1 :: "'x prm"
  1296   and   pi2 :: "'x prm"
  1297   and   x  :: "'a"
  1298   assumes pt: "pt TYPE('a) TYPE('x)"
  1299   and     at: "at TYPE('x)"
  1300   shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
  1301 proof -
  1302   have "((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
  1303   hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
  1304   thus ?thesis by (simp add: pt2[OF pt])
  1305 qed
  1306 
  1307 section {* facts about supports *}
  1308 (*==============================*)
  1309 
  1310 lemma supports_subset:
  1311   fixes x  :: "'a"
  1312   and   S1 :: "'x set"
  1313   and   S2 :: "'x set"
  1314   assumes  a: "S1 supports x"
  1315   and      b: "S1 \<subseteq> S2"
  1316   shows "S2 supports x"
  1317   using a b
  1318   by (force simp add: "op supports_def")
  1319 
  1320 lemma supp_is_subset:
  1321   fixes S :: "'x set"
  1322   and   x :: "'a"
  1323   assumes a1: "S supports x"
  1324   and     a2: "finite S"
  1325   shows "(supp x)\<subseteq>S"
  1326 proof (rule ccontr)
  1327   assume "\<not>(supp x \<subseteq> S)"
  1328   hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
  1329   then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
  1330   from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
  1331   with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
  1332   with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
  1333   hence "a\<notin>(supp x)" by (unfold supp_def, auto)
  1334   with b1 show False by simp
  1335 qed
  1336 
  1337 lemma supp_supports:
  1338   fixes x :: "'a"
  1339   assumes  pt: "pt TYPE('a) TYPE('x)"
  1340   and      at: "at TYPE ('x)"
  1341   shows "((supp x)::'x set) supports x"
  1342 proof (unfold "op supports_def", intro strip)
  1343   fix a b
  1344   assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
  1345   hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
  1346   thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
  1347 qed
  1348 
  1349 lemma supports_finite:
  1350   fixes S :: "'x set"
  1351   and   x :: "'a"
  1352   assumes a1: "S supports x"
  1353   and     a2: "finite S"
  1354   shows "finite ((supp x)::'x set)"
  1355 proof -
  1356   have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1357   thus ?thesis using a2 by (simp add: finite_subset)
  1358 qed
  1359   
  1360 lemma supp_is_inter:
  1361   fixes  x :: "'a"
  1362   assumes  pt: "pt TYPE('a) TYPE('x)"
  1363   and      at: "at TYPE ('x)"
  1364   and      fs: "fs TYPE('a) TYPE('x)"
  1365   shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
  1366 proof (rule equalityI)
  1367   show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
  1368   proof (clarify)
  1369     fix S c
  1370     assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
  1371     hence  "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 
  1372     with b show "c\<in>S" by force
  1373   qed
  1374 next
  1375   show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
  1376   proof (clarify, simp)
  1377     fix c
  1378     assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
  1379     have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1380     with d fs1[OF fs] show "c\<in>supp x" by force
  1381   qed
  1382 qed
  1383     
  1384 lemma supp_is_least_supports:
  1385   fixes S :: "'x set"
  1386   and   x :: "'a"
  1387   assumes  pt: "pt TYPE('a) TYPE('x)"
  1388   and      at: "at TYPE ('x)"
  1389   and      a1: "S supports x"
  1390   and      a2: "finite S"
  1391   and      a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
  1392   shows "S = (supp x)"
  1393 proof (rule equalityI)
  1394   show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1395 next
  1396   have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  1397   have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1398   hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
  1399   with s1 a3 show "S\<subseteq>supp x" by force
  1400 qed
  1401 
  1402 lemma supports_set:
  1403   fixes S :: "'x set"
  1404   and   X :: "'a set"
  1405   assumes  pt: "pt TYPE('a) TYPE('x)"
  1406   and      at: "at TYPE ('x)"
  1407   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)"
  1408   shows  "S supports X"
  1409 using a
  1410 apply(auto simp add: "op supports_def")
  1411 apply(simp add: pt_set_bij1a[OF pt, OF at])
  1412 apply(force simp add: pt_swap_bij[OF pt, OF at])
  1413 apply(simp add: pt_set_bij1a[OF pt, OF at])
  1414 done
  1415 
  1416 lemma supports_fresh:
  1417   fixes S :: "'x set"
  1418   and   a :: "'x"
  1419   and   x :: "'a"
  1420   assumes a1: "S supports x"
  1421   and     a2: "finite S"
  1422   and     a3: "a\<notin>S"
  1423   shows "a\<sharp>x"
  1424 proof (simp add: fresh_def)
  1425   have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  1426   thus "a\<notin>(supp x)" using a3 by force
  1427 qed
  1428 
  1429 lemma at_fin_set_supports:
  1430   fixes X::"'x set"
  1431   assumes at: "at TYPE('x)"
  1432   shows "X supports X"
  1433 proof (simp add: "op supports_def", intro strip)
  1434   fix a b
  1435   assume "a\<notin>X \<and> b\<notin>X"
  1436   thus "[(a,b)]\<bullet>X = X" by (force simp add: perm_set_def at_calc[OF at])
  1437 qed
  1438 
  1439 lemma at_fin_set_supp:
  1440   fixes X::"'x set"
  1441   assumes at: "at TYPE('x)"
  1442   and     fs: "finite X"
  1443   shows "(supp X) = X"
  1444 proof -
  1445   have pt_set: "pt TYPE('x set) TYPE('x)" 
  1446     by (rule pt_set_inst[OF at_pt_inst[OF at]])
  1447   have X_supports_X: "X supports X" by (rule at_fin_set_supports[OF at])
  1448   show ?thesis using  pt_set at X_supports_X fs
  1449   proof (rule supp_is_least_supports[symmetric])
  1450     show "\<forall>S'. finite S' \<and> S' supports X \<longrightarrow> X \<subseteq> S'"
  1451     proof (auto)
  1452       fix S'::"'x set" and x::"'x"
  1453       assume f: "finite S'"
  1454       and    s: "S' supports X"
  1455       and    e1: "x\<in>X"
  1456       show "x\<in>S'"
  1457       proof (rule ccontr)
  1458 	assume e2: "x\<notin>S'"
  1459 	have "\<exists>b. b\<notin>(X\<union>S')" by (force intro: ex_in_inf[OF at] simp only: fs f)
  1460 	then obtain b where b1: "b\<notin>X" and b2: "b\<notin>S'" by (auto)
  1461 	from s e2 b2 have c1: "[(x,b)]\<bullet>X=X" by (simp add: "op supports_def")
  1462 	from e1 b1 have c2: "[(x,b)]\<bullet>X\<noteq>X" by (force simp add: perm_set_def at_calc[OF at])
  1463 	show "False" using c1 c2 by simp
  1464       qed
  1465     qed
  1466   qed
  1467 qed
  1468 
  1469 section {* Permutations acting on Functions *}
  1470 (*==========================================*)
  1471 
  1472 lemma pt_fun_app_eq:
  1473   fixes f  :: "'a\<Rightarrow>'b"
  1474   and   x  :: "'a"
  1475   and   pi :: "'x prm"
  1476   assumes pt: "pt TYPE('a) TYPE('x)"
  1477   and     at: "at TYPE('x)"
  1478   shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)"
  1479   by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
  1480 
  1481 
  1482 --"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
  1483 lemma pt_perm:
  1484   fixes x  :: "'a"
  1485   and   pi1 :: "'x prm"
  1486   and   pi2 :: "'x prm"
  1487   assumes pt: "pt TYPE('a) TYPE('x)"
  1488   and     at: "at TYPE ('x)"
  1489   shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 
  1490   by (simp add: pt_fun_app_eq[OF pt, OF at])
  1491 
  1492 
  1493 lemma pt_fun_eq:
  1494   fixes f  :: "'a\<Rightarrow>'b"
  1495   and   pi :: "'x prm"
  1496   assumes pt: "pt TYPE('a) TYPE('x)"
  1497   and     at: "at TYPE('x)"
  1498   shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS")
  1499 proof
  1500   assume a: "?LHS"
  1501   show "?RHS"
  1502   proof
  1503     fix x
  1504     have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
  1505     also have "\<dots> = f (pi\<bullet>x)" using a by simp
  1506     finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp
  1507   qed
  1508 next
  1509   assume b: "?RHS"
  1510   show "?LHS"
  1511   proof (rule ccontr)
  1512     assume "(pi\<bullet>f) \<noteq> f"
  1513     hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
  1514     then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
  1515     from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
  1516     hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" 
  1517       by (simp add: pt_fun_app_eq[OF pt, OF at])
  1518     hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
  1519     with b1 show "False" by simp
  1520   qed
  1521 qed
  1522 
  1523 -- "two helper lemmas for the equivariance of functions"
  1524 lemma pt_swap_eq_aux:
  1525   fixes   y :: "'a"
  1526   and    pi :: "'x prm"
  1527   assumes pt: "pt TYPE('a) TYPE('x)"
  1528   and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
  1529   shows "pi\<bullet>y = y"
  1530 proof(induct pi)
  1531     case Nil show ?case by (simp add: pt1[OF pt])
  1532   next
  1533     case (Cons x xs)
  1534     have "\<exists>a b. x=(a,b)" by force
  1535     then obtain a b where p: "x=(a,b)" by force
  1536     assume i: "xs\<bullet>y = y"
  1537     have "x#xs = [x]@xs" by simp
  1538     hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
  1539     hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
  1540     thus ?case using a i p by force
  1541   qed
  1542 
  1543 lemma pt_swap_eq:
  1544   fixes   y :: "'a"
  1545   assumes pt: "pt TYPE('a) TYPE('x)"
  1546   shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)"
  1547   by (force intro: pt_swap_eq_aux[OF pt])
  1548 
  1549 lemma pt_eqvt_fun1a:
  1550   fixes f     :: "'a\<Rightarrow>'b"
  1551   assumes pta: "pt TYPE('a) TYPE('x)"
  1552   and     ptb: "pt TYPE('b) TYPE('x)"
  1553   and     at:  "at TYPE('x)"
  1554   and     a:   "((supp f)::'x set)={}"
  1555   shows "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  1556 proof (intro strip)
  1557   fix pi
  1558   have "\<forall>a b. a\<notin>((supp f)::'x set) \<and> b\<notin>((supp f)::'x set) \<longrightarrow> (([(a,b)]\<bullet>f) = f)" 
  1559     by (intro strip, fold fresh_def, 
  1560       simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at])
  1561   with a have "\<forall>(a::'x) (b::'x). ([(a,b)]\<bullet>f) = f" by force
  1562   hence "\<forall>(pi::'x prm). pi\<bullet>f = f" 
  1563     by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]])
  1564   thus "(pi::'x prm)\<bullet>f = f" by simp
  1565 qed
  1566 
  1567 lemma pt_eqvt_fun1b:
  1568   fixes f     :: "'a\<Rightarrow>'b"
  1569   assumes a: "\<forall>(pi::'x prm). pi\<bullet>f = f"
  1570   shows "((supp f)::'x set)={}"
  1571 using a by (simp add: supp_def)
  1572 
  1573 lemma pt_eqvt_fun1:
  1574   fixes f     :: "'a\<Rightarrow>'b"
  1575   assumes pta: "pt TYPE('a) TYPE('x)"
  1576   and     ptb: "pt TYPE('b) TYPE('x)"
  1577   and     at: "at TYPE('x)"
  1578   shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm). pi\<bullet>f = f)" (is "?LHS = ?RHS")
  1579 by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)
  1580 
  1581 lemma pt_eqvt_fun2a:
  1582   fixes f     :: "'a\<Rightarrow>'b"
  1583   assumes pta: "pt TYPE('a) TYPE('x)"
  1584   and     ptb: "pt TYPE('b) TYPE('x)"
  1585   and     at: "at TYPE('x)"
  1586   assumes a: "((supp f)::'x set)={}"
  1587   shows "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)" 
  1588 proof (intro strip)
  1589   fix pi x
  1590   from a have b: "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) 
  1591   have "(pi::'x prm)\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 
  1592   with b show "(pi::'x prm)\<bullet>(f x) = f (pi\<bullet>x)" by force 
  1593 qed
  1594 
  1595 lemma pt_eqvt_fun2b:
  1596   fixes f     :: "'a\<Rightarrow>'b"
  1597   assumes pt1: "pt TYPE('a) TYPE('x)"
  1598   and     pt2: "pt TYPE('b) TYPE('x)"
  1599   and     at: "at TYPE('x)"
  1600   assumes a: "\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x)"
  1601   shows "((supp f)::'x set)={}"
  1602 proof -
  1603   from a have "\<forall>(pi::'x prm). pi\<bullet>f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric])
  1604   thus ?thesis by (simp add: supp_def)
  1605 qed
  1606 
  1607 lemma pt_eqvt_fun2:
  1608   fixes f     :: "'a\<Rightarrow>'b"
  1609   assumes pta: "pt TYPE('a) TYPE('x)"
  1610   and     ptb: "pt TYPE('b) TYPE('x)"
  1611   and     at: "at TYPE('x)"
  1612   shows "(((supp f)::'x set)={}) = (\<forall>(pi::'x prm) (x::'a). pi\<bullet>(f x) = f(pi\<bullet>x))" 
  1613 by (rule iffI, 
  1614     simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], 
  1615     simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])
  1616 
  1617 lemma pt_supp_fun_subset:
  1618   fixes f :: "'a\<Rightarrow>'b"
  1619   assumes pta: "pt TYPE('a) TYPE('x)"
  1620   and     ptb: "pt TYPE('b) TYPE('x)"
  1621   and     at: "at TYPE('x)" 
  1622   and     f1: "finite ((supp f)::'x set)"
  1623   and     f2: "finite ((supp x)::'x set)"
  1624   shows "supp (f x) \<subseteq> (((supp f)\<union>(supp x))::'x set)"
  1625 proof -
  1626   have s1: "((supp f)\<union>((supp x)::'x set)) supports (f x)"
  1627   proof (simp add: "op supports_def", fold fresh_def, auto)
  1628     fix a::"'x" and b::"'x"
  1629     assume "a\<sharp>f" and "b\<sharp>f"
  1630     hence a1: "[(a,b)]\<bullet>f = f" 
  1631       by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at])
  1632     assume "a\<sharp>x" and "b\<sharp>x"
  1633     hence a2: "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pta, OF at])
  1634     from a1 a2 show "[(a,b)]\<bullet>(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
  1635   qed
  1636   from f1 f2 have "finite ((supp f)\<union>((supp x)::'x set))" by force
  1637   with s1 show ?thesis by (rule supp_is_subset)
  1638 qed
  1639       
  1640 lemma pt_empty_supp_fun_subset:
  1641   fixes f :: "'a\<Rightarrow>'b"
  1642   assumes pta: "pt TYPE('a) TYPE('x)"
  1643   and     ptb: "pt TYPE('b) TYPE('x)"
  1644   and     at:  "at TYPE('x)" 
  1645   and     e:   "(supp f)=({}::'x set)"
  1646   shows "supp (f x) \<subseteq> ((supp x)::'x set)"
  1647 proof (unfold supp_def, auto)
  1648   fix a::"'x"
  1649   assume a1: "finite {b. [(a, b)]\<bullet>x \<noteq> x}"
  1650   assume "infinite {b. [(a, b)]\<bullet>(f x) \<noteq> f x}"
  1651   hence a2: "infinite {b. f ([(a, b)]\<bullet>x) \<noteq> f x}" using e
  1652     by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at])
  1653   have a3: "{b. f ([(a,b)]\<bullet>x) \<noteq> f x}\<subseteq>{b. [(a,b)]\<bullet>x \<noteq> x}" by force
  1654   from a1 a2 a3 show False by (force dest: finite_subset)
  1655 qed
  1656 
  1657 section {* Facts about the support of finite sets of finitely supported things *}
  1658 (*=============================================================================*)
  1659 
  1660 constdefs
  1661   X_to_Un_supp :: "('a set) \<Rightarrow> 'x set"
  1662   "X_to_Un_supp X \<equiv> \<Union>x\<in>X. ((supp x)::'x set)"
  1663 
  1664 lemma UNION_f_eqvt:
  1665   fixes X::"('a set)"
  1666   and   f::"'a \<Rightarrow> 'x set"
  1667   and   pi::"'x prm"
  1668   assumes pt: "pt TYPE('a) TYPE('x)"
  1669   and     at: "at TYPE('x)"
  1670   shows "pi\<bullet>(\<Union>x\<in>X. f x) = (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
  1671 proof -
  1672   have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
  1673   show ?thesis
  1674   proof (rule equalityI)
  1675     case goal1
  1676     show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
  1677       apply(auto simp add: perm_set_def)
  1678       apply(rule_tac x="pi\<bullet>xa" in exI)
  1679       apply(rule conjI)
  1680       apply(rule_tac x="xa" in exI)
  1681       apply(simp)
  1682       apply(subgoal_tac "(pi\<bullet>f) (pi\<bullet>xa) = pi\<bullet>(f xa)")(*A*)
  1683       apply(simp)
  1684       apply(rule pt_set_bij2[OF pt_x, OF at])
  1685       apply(assumption)
  1686       (*A*)
  1687       apply(rule sym)
  1688       apply(rule pt_fun_app_eq[OF pt, OF at])
  1689       done
  1690   next
  1691     case goal2
  1692     show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
  1693       apply(auto simp add: perm_set_def)
  1694       apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  1695       apply(rule conjI)
  1696       apply(simp add: pt_pi_rev[OF pt_x, OF at])
  1697       apply(rule_tac x="a" in bexI)
  1698       apply(simp add: pt_set_bij1[OF pt_x, OF at])
  1699       apply(simp add: pt_fun_app_eq[OF pt, OF at])
  1700       apply(assumption)
  1701       done
  1702   qed
  1703 qed
  1704 
  1705 lemma X_to_Un_supp_eqvt:
  1706   fixes X::"('a set)"
  1707   and   pi::"'x prm"
  1708   assumes pt: "pt TYPE('a) TYPE('x)"
  1709   and     at: "at TYPE('x)"
  1710   shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
  1711   apply(simp add: X_to_Un_supp_def)
  1712   apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
  1713   apply(simp add: pt_perm_supp[OF pt, OF at])
  1714   apply(simp add: pt_pi_rev[OF pt, OF at])
  1715   done
  1716 
  1717 lemma Union_supports_set:
  1718   fixes X::"('a set)"
  1719   assumes pt: "pt TYPE('a) TYPE('x)"
  1720   and     at: "at TYPE('x)"
  1721   shows "(\<Union>x\<in>X. ((supp x)::'x set)) supports X"
  1722   apply(simp add: "op supports_def" fresh_def[symmetric])
  1723   apply(rule allI)+
  1724   apply(rule impI)
  1725   apply(erule conjE)
  1726   apply(simp add: perm_set_def)
  1727   apply(auto)
  1728   apply(subgoal_tac "[(a,b)]\<bullet>aa = aa")(*A*)
  1729   apply(simp)
  1730   apply(rule pt_fresh_fresh[OF pt, OF at])
  1731   apply(force)
  1732   apply(force)
  1733   apply(rule_tac x="x" in exI)
  1734   apply(simp)
  1735   apply(rule sym)
  1736   apply(rule pt_fresh_fresh[OF pt, OF at])
  1737   apply(force)+
  1738   done
  1739 
  1740 lemma Union_of_fin_supp_sets:
  1741   fixes X::"('a set)"
  1742   assumes fs: "fs TYPE('a) TYPE('x)" 
  1743   and     fi: "finite X"   
  1744   shows "finite (\<Union>x\<in>X. ((supp x)::'x set))"
  1745 using fi by (induct, auto simp add: fs1[OF fs])
  1746 
  1747 lemma Union_included_in_supp:
  1748   fixes X::"('a set)"
  1749   assumes pt: "pt TYPE('a) TYPE('x)"
  1750   and     at: "at TYPE('x)"
  1751   and     fs: "fs TYPE('a) TYPE('x)" 
  1752   and     fi: "finite X"
  1753   shows "(\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> supp X"
  1754 proof -
  1755   have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
  1756     apply(rule pt_empty_supp_fun_subset)
  1757     apply(force intro: pt_set_inst at_pt_inst pt at)+
  1758     apply(rule pt_eqvt_fun2b)
  1759     apply(force intro: pt_set_inst at_pt_inst pt at)+
  1760     apply(rule allI)+
  1761     apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
  1762     done
  1763   hence "supp (\<Union>x\<in>X. ((supp x)::'x set)) \<subseteq> ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
  1764   moreover
  1765   have "supp (\<Union>x\<in>X. ((supp x)::'x set)) = (\<Union>x\<in>X. ((supp x)::'x set))"
  1766     apply(rule at_fin_set_supp[OF at])
  1767     apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
  1768     done
  1769   ultimately show ?thesis by force
  1770 qed
  1771 
  1772 lemma supp_of_fin_sets:
  1773   fixes X::"('a set)"
  1774   assumes pt: "pt TYPE('a) TYPE('x)"
  1775   and     at: "at TYPE('x)"
  1776   and     fs: "fs TYPE('a) TYPE('x)" 
  1777   and     fi: "finite X"
  1778   shows "(supp X) = (\<Union>x\<in>X. ((supp x)::'x set))"
  1779 apply(rule equalityI)
  1780 apply(rule supp_is_subset)
  1781 apply(rule Union_supports_set[OF pt, OF at])
  1782 apply(rule Union_of_fin_supp_sets[OF fs, OF fi])
  1783 apply(rule Union_included_in_supp[OF pt, OF at, OF fs, OF fi])
  1784 done
  1785 
  1786 lemma supp_fin_union:
  1787   fixes X::"('a set)"
  1788   and   Y::"('a set)"
  1789   assumes pt: "pt TYPE('a) TYPE('x)"
  1790   and     at: "at TYPE('x)"
  1791   and     fs: "fs TYPE('a) TYPE('x)" 
  1792   and     f1: "finite X"
  1793   and     f2: "finite Y"
  1794   shows "(supp (X\<union>Y)) = (supp X)\<union>((supp Y)::'x set)"
  1795 using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs])
  1796 
  1797 lemma supp_fin_insert:
  1798   fixes X::"('a set)"
  1799   and   x::"'a"
  1800   assumes pt: "pt TYPE('a) TYPE('x)"
  1801   and     at: "at TYPE('x)"
  1802   and     fs: "fs TYPE('a) TYPE('x)" 
  1803   and     f:  "finite X"
  1804   shows "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
  1805 proof -
  1806   have "(supp (insert x X)) = ((supp ({x}\<union>(X::'a set)))::'x set)" by simp
  1807   also have "\<dots> = (supp {x})\<union>(supp X)"
  1808     by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
  1809   finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 
  1810     by (simp add: supp_singleton)
  1811 qed
  1812 
  1813 lemma fresh_fin_union:
  1814   fixes X::"('a set)"
  1815   and   Y::"('a set)"
  1816   and   a::"'x"
  1817   assumes pt: "pt TYPE('a) TYPE('x)"
  1818   and     at: "at TYPE('x)"
  1819   and     fs: "fs TYPE('a) TYPE('x)" 
  1820   and     f1: "finite X"
  1821   and     f2: "finite Y"
  1822   shows "a\<sharp>(X\<union>Y) = (a\<sharp>X \<and> a\<sharp>Y)"
  1823 apply(simp add: fresh_def)
  1824 apply(simp add: supp_fin_union[OF pt, OF at, OF fs, OF f1, OF f2])
  1825 done
  1826 
  1827 lemma fresh_fin_insert:
  1828   fixes X::"('a set)"
  1829   and   x::"'a"
  1830   and   a::"'x"
  1831   assumes pt: "pt TYPE('a) TYPE('x)"
  1832   and     at: "at TYPE('x)"
  1833   and     fs: "fs TYPE('a) TYPE('x)" 
  1834   and     f:  "finite X"
  1835   shows "a\<sharp>(insert x X) = (a\<sharp>x \<and> a\<sharp>X)"
  1836 apply(simp add: fresh_def)
  1837 apply(simp add: supp_fin_insert[OF pt, OF at, OF fs, OF f])
  1838 done
  1839 
  1840 lemma fresh_fin_insert1:
  1841   fixes X::"('a set)"
  1842   and   x::"'a"
  1843   and   a::"'x"
  1844   assumes pt: "pt TYPE('a) TYPE('x)"
  1845   and     at: "at TYPE('x)"
  1846   and     fs: "fs TYPE('a) TYPE('x)" 
  1847   and     f:  "finite X"
  1848   and     a1:  "a\<sharp>x"
  1849   and     a2:  "a\<sharp>X"
  1850   shows "a\<sharp>(insert x X)"
  1851 using a1 a2
  1852 apply(simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])
  1853 done
  1854 
  1855 lemma pt_list_set_pi:
  1856   fixes pi :: "'x prm"
  1857   and   xs :: "'a list"
  1858   assumes pt: "pt TYPE('a) TYPE('x)"
  1859   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
  1860 by (induct xs, auto simp add: perm_set_def pt1[OF pt])
  1861 
  1862 lemma pt_list_set_supp:
  1863   fixes xs :: "'a list"
  1864   assumes pt: "pt TYPE('a) TYPE('x)"
  1865   and     at: "at TYPE('x)"
  1866   and     fs: "fs TYPE('a) TYPE('x)"
  1867   shows "supp (set xs) = ((supp xs)::'x set)"
  1868 proof -
  1869   have "supp (set xs) = (\<Union>x\<in>(set xs). ((supp x)::'x set))"
  1870     by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set)
  1871   also have "(\<Union>x\<in>(set xs). ((supp x)::'x set)) = (supp xs)"
  1872   proof(induct xs)
  1873     case Nil show ?case by (simp add: supp_list_nil)
  1874   next
  1875     case (Cons h t) thus ?case by (simp add: supp_list_cons)
  1876   qed
  1877   finally show ?thesis by simp
  1878 qed
  1879     
  1880 lemma pt_list_set_fresh:
  1881   fixes a :: "'x"
  1882   and   xs :: "'a list"
  1883   assumes pt: "pt TYPE('a) TYPE('x)"
  1884   and     at: "at TYPE('x)"
  1885   and     fs: "fs TYPE('a) TYPE('x)"
  1886   and     a: "a\<sharp>xs"
  1887   shows "a\<sharp>(set xs) = a\<sharp>xs"
  1888 by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])
  1889  
  1890 section {* Andy's freshness lemma *}
  1891 (*================================*)
  1892 
  1893 lemma freshness_lemma:
  1894   fixes h :: "'x\<Rightarrow>'a"
  1895   assumes pta: "pt TYPE('a) TYPE('x)"
  1896   and     at:  "at TYPE('x)" 
  1897   and     f1:  "finite ((supp h)::'x set)"
  1898   and     a: "\<exists>a::'x. (a\<sharp>h \<and> a\<sharp>(h a))"
  1899   shows  "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> (h a) = fr"
  1900 proof -
  1901   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  1902   have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  1903   from a obtain a0 where a1: "a0\<sharp>h" and a2: "a0\<sharp>(h a0)" by force
  1904   show ?thesis
  1905   proof
  1906     let ?fr = "h (a0::'x)"
  1907     show "\<forall>(a::'x). (a\<sharp>h \<longrightarrow> ((h a) = ?fr))" 
  1908     proof (intro strip)
  1909       fix a
  1910       assume a3: "(a::'x)\<sharp>h"
  1911       show "h (a::'x) = h a0"
  1912       proof (cases "a=a0")
  1913 	case True thus "h (a::'x) = h a0" by simp
  1914       next
  1915 	case False 
  1916 	assume "a\<noteq>a0"
  1917 	hence c1: "a\<notin>((supp a0)::'x set)" by  (simp add: fresh_def[symmetric] at_fresh[OF at])
  1918 	have c2: "a\<notin>((supp h)::'x set)" using a3 by (simp add: fresh_def)
  1919 	from c1 c2 have c3: "a\<notin>((supp h)\<union>((supp a0)::'x set))" by force
  1920 	have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at])
  1921 	from f1 f2 have "((supp (h a0))::'x set)\<subseteq>((supp h)\<union>(supp a0))"
  1922 	  by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at])
  1923 	hence "a\<notin>((supp (h a0))::'x set)" using c3 by force
  1924 	hence "a\<sharp>(h a0)" by (simp add: fresh_def) 
  1925 	with a2 have d1: "[(a0,a)]\<bullet>(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at])
  1926 	from a1 a3 have d2: "[(a0,a)]\<bullet>h = h" by (rule pt_fresh_fresh[OF ptc, OF at])
  1927 	from d1 have "h a0 = [(a0,a)]\<bullet>(h a0)" by simp
  1928 	also have "\<dots>= ([(a0,a)]\<bullet>h)([(a0,a)]\<bullet>a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at])
  1929 	also have "\<dots> = h ([(a0,a)]\<bullet>a0)" using d2 by simp
  1930 	also have "\<dots> = h a" by (simp add: at_calc[OF at])
  1931 	finally show "h a = h a0" by simp
  1932       qed
  1933     qed
  1934   qed
  1935 qed
  1936 	    
  1937 lemma freshness_lemma_unique:
  1938   fixes h :: "'x\<Rightarrow>'a"
  1939   assumes pt: "pt TYPE('a) TYPE('x)"
  1940   and     at: "at TYPE('x)" 
  1941   and     f1: "finite ((supp h)::'x set)"
  1942   and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1943   shows  "\<exists>!(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr"
  1944 proof
  1945   from pt at f1 a show "\<exists>fr::'a. \<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr" by (simp add: freshness_lemma)
  1946 next
  1947   fix fr1 fr2
  1948   assume b1: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr1"
  1949   assume b2: "\<forall>a::'x. a\<sharp>h \<longrightarrow> h a = fr2"
  1950   from a obtain a where "(a::'x)\<sharp>h" by force 
  1951   with b1 b2 have "h a = fr1 \<and> h a = fr2" by force
  1952   thus "fr1 = fr2" by force
  1953 qed
  1954 
  1955 -- "packaging the freshness lemma into a function"
  1956 constdefs
  1957   fresh_fun :: "('x\<Rightarrow>'a)\<Rightarrow>'a"
  1958   "fresh_fun (h) \<equiv> THE fr. (\<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr)"
  1959 
  1960 lemma fresh_fun_app:
  1961   fixes h :: "'x\<Rightarrow>'a"
  1962   and   a :: "'x"
  1963   assumes pt: "pt TYPE('a) TYPE('x)"
  1964   and     at: "at TYPE('x)" 
  1965   and     f1: "finite ((supp h)::'x set)"
  1966   and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1967   and     b: "a\<sharp>h"
  1968   shows "(fresh_fun h) = (h a)"
  1969 proof (unfold fresh_fun_def, rule the_equality)
  1970   show "\<forall>(a'::'x). a'\<sharp>h \<longrightarrow> h a' = h a"
  1971   proof (intro strip)
  1972     fix a'::"'x"
  1973     assume c: "a'\<sharp>h"
  1974     from pt at f1 a have "\<exists>(fr::'a). \<forall>(a::'x). a\<sharp>h \<longrightarrow> (h a) = fr" by (rule freshness_lemma)
  1975     with b c show "h a' = h a" by force
  1976   qed
  1977 next
  1978   fix fr::"'a"
  1979   assume "\<forall>a. a\<sharp>h \<longrightarrow> h a = fr"
  1980   with b show "fr = h a" by force
  1981 qed
  1982 
  1983 
  1984 lemma fresh_fun_supports:
  1985   fixes h :: "'x\<Rightarrow>'a"
  1986   assumes pt: "pt TYPE('a) TYPE('x)"
  1987   and     at: "at TYPE('x)" 
  1988   and     f1: "finite ((supp h)::'x set)"
  1989   and     a: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  1990   shows "((supp h)::'x set) supports (fresh_fun h)"
  1991   apply(simp add: "op supports_def")
  1992   apply(fold fresh_def)
  1993   apply(auto)
  1994   apply(subgoal_tac "\<exists>(a''::'x). a''\<sharp>(h,a,b)")(*A*)
  1995   apply(erule exE)
  1996   apply(simp add: fresh_prod)
  1997   apply(auto)
  1998   apply(rotate_tac 2)
  1999   apply(drule fresh_fun_app[OF pt, OF at, OF f1, OF a])
  2000   apply(simp add: at_fresh[OF at])
  2001   apply(simp add: pt_fun_app_eq[OF at_pt_inst[OF at], OF at])
  2002   apply(auto simp add: at_calc[OF at])
  2003   apply(subgoal_tac "[(a, b)]\<bullet>h = h")(*B*)
  2004   apply(simp)
  2005   (*B*)
  2006   apply(rule pt_fresh_fresh[OF pt_fun_inst[OF at_pt_inst[OF at], OF pt], OF at, OF at])
  2007   apply(assumption)+
  2008   (*A*)
  2009   apply(rule at_exists_fresh[OF at])
  2010   apply(simp add: supp_prod)
  2011   apply(simp add: f1 at_supp[OF at])
  2012   done
  2013 
  2014 lemma fresh_fun_equiv:
  2015   fixes h :: "'x\<Rightarrow>'a"
  2016   and   pi:: "'x prm"
  2017   assumes pta: "pt TYPE('a) TYPE('x)"
  2018   and     at:  "at TYPE('x)" 
  2019   and     f1:  "finite ((supp h)::'x set)"
  2020   and     a1: "\<exists>(a::'x). (a\<sharp>h \<and> a\<sharp>(h a))"
  2021   shows "pi\<bullet>(fresh_fun h) = fresh_fun(pi\<bullet>h)" (is "?LHS = ?RHS")
  2022 proof -
  2023   have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  2024   have ptc: "pt TYPE('x\<Rightarrow>'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  2025   have f2: "finite ((supp (pi\<bullet>h))::'x set)"
  2026   proof -
  2027     from f1 have "finite (pi\<bullet>((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
  2028     thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
  2029   qed
  2030   from a1 obtain a' where c0: "a'\<sharp>h \<and> a'\<sharp>(h a')" by force
  2031   hence c1: "a'\<sharp>h" and c2: "a'\<sharp>(h a')" by simp_all
  2032   have c3: "(pi\<bullet>a')\<sharp>(pi\<bullet>h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
  2033   have c4: "(pi\<bullet>a')\<sharp>(pi\<bullet>h) (pi\<bullet>a')"
  2034   proof -
  2035     from c2 have "(pi\<bullet>a')\<sharp>(pi\<bullet>(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
  2036     thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2037   qed
  2038   have a2: "\<exists>(a::'x). (a\<sharp>(pi\<bullet>h) \<and> a\<sharp>((pi\<bullet>h) a))" using c3 c4 by force
  2039   have d1: "?LHS = pi\<bullet>(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
  2040   have d2: "?RHS = (pi\<bullet>h) (pi\<bullet>a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
  2041   show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
  2042 qed
  2043   
  2044 section {* disjointness properties *}
  2045 (*=================================*)
  2046 lemma dj_perm_forget:
  2047   fixes pi::"'y prm"
  2048   and   x ::"'x"
  2049   assumes dj: "disjoint TYPE('x) TYPE('y)"
  2050   shows "pi\<bullet>x=x"
  2051   using dj by (simp add: disjoint_def)
  2052 
  2053 lemma dj_perm_perm_forget:
  2054   fixes pi1::"'x prm"
  2055   and   pi2::"'y prm"
  2056   assumes dj: "disjoint TYPE('x) TYPE('y)"
  2057   shows "pi2\<bullet>pi1=pi1"
  2058   using dj by (induct pi1, auto simp add: disjoint_def)
  2059 
  2060 lemma dj_cp:
  2061   fixes pi1::"'x prm"
  2062   and   pi2::"'y prm"
  2063   and   x  ::"'a"
  2064   assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2065   and     dj: "disjoint TYPE('y) TYPE('x)"
  2066   shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
  2067   by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
  2068 
  2069 lemma dj_supp:
  2070   fixes a::"'x"
  2071   assumes dj: "disjoint TYPE('x) TYPE('y)"
  2072   shows "(supp a) = ({}::'y set)"
  2073 apply(simp add: supp_def dj_perm_forget[OF dj])
  2074 done
  2075 
  2076 
  2077 section {* composition instances *}
  2078 (* ============================= *)
  2079 
  2080 lemma cp_list_inst:
  2081   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2082   shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
  2083 using c1
  2084 apply(simp add: cp_def)
  2085 apply(auto)
  2086 apply(induct_tac x)
  2087 apply(auto)
  2088 done
  2089 
  2090 lemma cp_set_inst:
  2091   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2092   shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
  2093 using c1
  2094 apply(simp add: cp_def)
  2095 apply(auto)
  2096 apply(auto simp add: perm_set_def)
  2097 apply(rule_tac x="pi2\<bullet>aa" in exI)
  2098 apply(auto)
  2099 done
  2100 
  2101 lemma cp_option_inst:
  2102   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2103   shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
  2104 using c1
  2105 apply(simp add: cp_def)
  2106 apply(auto)
  2107 apply(case_tac x)
  2108 apply(auto)
  2109 done
  2110 
  2111 lemma cp_noption_inst:
  2112   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2113   shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
  2114 using c1
  2115 apply(simp add: cp_def)
  2116 apply(auto)
  2117 apply(case_tac x)
  2118 apply(auto)
  2119 done
  2120 
  2121 lemma cp_unit_inst:
  2122   shows "cp TYPE (unit) TYPE('x) TYPE('y)"
  2123 apply(simp add: cp_def)
  2124 done
  2125 
  2126 lemma cp_bool_inst:
  2127   shows "cp TYPE (bool) TYPE('x) TYPE('y)"
  2128 apply(simp add: cp_def)
  2129 apply(rule allI)+
  2130 apply(induct_tac x)
  2131 apply(simp_all)
  2132 done
  2133 
  2134 lemma cp_prod_inst:
  2135   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2136   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  2137   shows "cp TYPE ('a\<times>'b) TYPE('x) TYPE('y)"
  2138 using c1 c2
  2139 apply(simp add: cp_def)
  2140 done
  2141 
  2142 lemma cp_fun_inst:
  2143   assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  2144   and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  2145   and     pt: "pt TYPE ('y) TYPE('x)"
  2146   and     at: "at TYPE ('x)"
  2147   shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
  2148 using c1 c2
  2149 apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
  2150 apply(simp add: perm_rev[symmetric])
  2151 apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
  2152 done
  2153 
  2154 
  2155 section {* Abstraction function *}
  2156 (*==============================*)
  2157 
  2158 lemma pt_abs_fun_inst:
  2159   assumes pt: "pt TYPE('a) TYPE('x)"
  2160   and     at: "at TYPE('x)"
  2161   shows "pt TYPE('x\<Rightarrow>('a noption)) TYPE('x)"
  2162   by (rule pt_fun_inst[OF at_pt_inst[OF at],OF pt_noption_inst[OF pt],OF at])
  2163 
  2164 constdefs
  2165   abs_fun :: "'x\<Rightarrow>'a\<Rightarrow>('x\<Rightarrow>('a noption))" ("[_]._" [100,100] 100)
  2166   "[a].x \<equiv> (\<lambda>b. (if b=a then nSome(x) else (if b\<sharp>x then nSome([(a,b)]\<bullet>x) else nNone)))"
  2167 
  2168 lemma abs_fun_if: 
  2169   fixes pi :: "'x prm"
  2170   and   x  :: "'a"
  2171   and   y  :: "'a"
  2172   and   c  :: "bool"
  2173   shows "pi\<bullet>(if c then x else y) = (if c then (pi\<bullet>x) else (pi\<bullet>y))"   
  2174   by force
  2175 
  2176 lemma abs_fun_pi_ineq:
  2177   fixes a  :: "'y"
  2178   and   x  :: "'a"
  2179   and   pi :: "'x prm"
  2180   assumes pta: "pt TYPE('a) TYPE('x)"
  2181   and     ptb: "pt TYPE('y) TYPE('x)"
  2182   and     at:  "at TYPE('x)"
  2183   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2184   shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  2185   apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
  2186   apply(simp only: expand_fun_eq)
  2187   apply(rule allI)
  2188   apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
  2189   apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
  2190   apply(subgoal_tac "pi\<bullet>([(a,(rev pi)\<bullet>xa)]\<bullet>x) = [(pi\<bullet>a,xa)]\<bullet>(pi\<bullet>x)")(*C*)
  2191   apply(simp)
  2192 (*C*)
  2193   apply(simp add: cp1[OF cp])
  2194   apply(simp add: pt_pi_rev[OF ptb, OF at])
  2195 (*B*)
  2196   apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  2197 (*A*)
  2198   apply(rule iffI)
  2199   apply(rule pt_bij2[OF ptb, OF at, THEN sym])
  2200   apply(simp)
  2201   apply(rule pt_bij2[OF ptb, OF at])
  2202   apply(simp)
  2203 done
  2204 
  2205 lemma abs_fun_pi:
  2206   fixes a  :: "'x"
  2207   and   x  :: "'a"
  2208   and   pi :: "'x prm"
  2209   assumes pt: "pt TYPE('a) TYPE('x)"
  2210   and     at: "at TYPE('x)"
  2211   shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
  2212 apply(rule abs_fun_pi_ineq)
  2213 apply(rule pt)
  2214 apply(rule at_pt_inst)
  2215 apply(rule at)+
  2216 apply(rule cp_pt_inst)
  2217 apply(rule pt)
  2218 apply(rule at)
  2219 done
  2220 
  2221 lemma abs_fun_eq1: 
  2222   fixes x  :: "'a"
  2223   and   y  :: "'a"
  2224   and   a  :: "'x"
  2225   shows "([a].x = [a].y) = (x = y)"
  2226 apply(auto simp add: abs_fun_def)
  2227 apply(auto simp add: expand_fun_eq)
  2228 apply(drule_tac x="a" in spec)
  2229 apply(simp)
  2230 done
  2231 
  2232 lemma abs_fun_eq2:
  2233   fixes x  :: "'a"
  2234   and   y  :: "'a"
  2235   and   a  :: "'x"
  2236   and   b  :: "'x"
  2237   assumes pt: "pt TYPE('a) TYPE('x)"
  2238       and at: "at TYPE('x)"
  2239       and a1: "a\<noteq>b" 
  2240       and a2: "[a].x = [b].y" 
  2241   shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
  2242 proof -
  2243   from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq)
  2244   hence "([a].x) a = ([b].y) a" by simp
  2245   hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def)
  2246   show "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
  2247   proof (cases "a\<sharp>y")
  2248     assume a4: "a\<sharp>y"
  2249     hence "x=[(b,a)]\<bullet>y" using a3 a1 by (simp add: abs_fun_def)
  2250     moreover
  2251     have "[(a,b)]\<bullet>y = [(b,a)]\<bullet>y" by (rule pt3[OF pt], rule at_ds5[OF at])
  2252     ultimately show ?thesis using a4 by simp
  2253   next
  2254     assume "\<not>a\<sharp>y"
  2255     hence "nSome(x) = nNone" using a1 a3 by (simp add: abs_fun_def)
  2256     hence False by simp
  2257     thus ?thesis by simp
  2258   qed
  2259 qed
  2260 
  2261 lemma abs_fun_eq3: 
  2262   fixes x  :: "'a"
  2263   and   y  :: "'a"
  2264   and   a   :: "'x"
  2265   and   b   :: "'x"
  2266   assumes pt: "pt TYPE('a) TYPE('x)"
  2267       and at: "at TYPE('x)"
  2268       and a1: "a\<noteq>b" 
  2269       and a2: "x=[(a,b)]\<bullet>y" 
  2270       and a3: "a\<sharp>y" 
  2271   shows "[a].x =[b].y"
  2272 proof -
  2273   show ?thesis 
  2274   proof (simp only: abs_fun_def expand_fun_eq, intro strip)
  2275     fix c::"'x"
  2276     let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone"
  2277     and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone"
  2278     show "?LHS=?RHS"
  2279     proof -
  2280       have "(c=a) \<or> (c=b) \<or> (c\<noteq>a \<and> c\<noteq>b)" by blast
  2281       moreover  --"case c=a"
  2282       { have "nSome(x) = nSome([(a,b)]\<bullet>y)" using a2 by simp
  2283 	also have "\<dots> = nSome([(b,a)]\<bullet>y)" by (simp, rule pt3[OF pt], rule at_ds5[OF at])
  2284 	finally have "nSome(x) = nSome([(b,a)]\<bullet>y)" by simp
  2285 	moreover
  2286 	assume "c=a"
  2287 	ultimately have "?LHS=?RHS" using a1 a3 by simp
  2288       }
  2289       moreover  -- "case c=b"
  2290       { have a4: "y=[(a,b)]\<bullet>x" using a2 by (simp only: pt_swap_bij[OF pt, OF at])
  2291 	hence "a\<sharp>([(a,b)]\<bullet>x)" using a3 by simp
  2292 	hence "b\<sharp>x" by (simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
  2293 	moreover
  2294 	assume "c=b"
  2295 	ultimately have "?LHS=?RHS" using a1 a4 by simp
  2296       }
  2297       moreover  -- "case c\<noteq>a \<and> c\<noteq>b"
  2298       { assume a5: "c\<noteq>a \<and> c\<noteq>b"
  2299 	moreover 
  2300 	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])
  2301 	moreover 
  2302 	have "c\<sharp>y \<longrightarrow> [(a,c)]\<bullet>x = [(b,c)]\<bullet>y" 
  2303 	proof (intro strip)
  2304 	  assume a6: "c\<sharp>y"
  2305 	  have "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at])
  2306 	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>y)) = [(a,b)]\<bullet>y" 
  2307 	    by (simp add: pt2[OF pt, symmetric] pt3[OF pt])
  2308  	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = [(a,b)]\<bullet>y" using a3 a6 
  2309 	    by (simp add: pt_fresh_fresh[OF pt, OF at])
  2310 	  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>y) = x" using a2 by simp
  2311 	  hence "[(b,c)]\<bullet>y = [(a,c)]\<bullet>x" by (drule_tac pt_bij1[OF pt, OF at], simp)
  2312 	  thus "[(a,c)]\<bullet>x = [(b,c)]\<bullet>y" by simp
  2313 	qed
  2314 	ultimately have "?LHS=?RHS" by simp
  2315       }
  2316       ultimately show "?LHS = ?RHS" by blast
  2317     qed
  2318   qed
  2319 qed
  2320 	
  2321 lemma abs_fun_eq: 
  2322   fixes x  :: "'a"
  2323   and   y  :: "'a"
  2324   and   a  :: "'x"
  2325   and   b  :: "'x"
  2326   assumes pt: "pt TYPE('a) TYPE('x)"
  2327       and at: "at TYPE('x)"
  2328   shows "([a].x = [b].y) = ((a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y))"
  2329 proof (rule iffI)
  2330   assume b: "[a].x = [b].y"
  2331   show "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  2332   proof (cases "a=b")
  2333     case True with b show ?thesis by (simp add: abs_fun_eq1)
  2334   next
  2335     case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at])
  2336   qed
  2337 next
  2338   assume "(a=b \<and> x=y)\<or>(a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y)"
  2339   thus "[a].x = [b].y"
  2340   proof
  2341     assume "a=b \<and> x=y" thus ?thesis by simp
  2342   next
  2343     assume "a\<noteq>b \<and> x=[(a,b)]\<bullet>y \<and> a\<sharp>y" 
  2344     thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at])
  2345   qed
  2346 qed
  2347 
  2348 lemma abs_fun_supp_approx:
  2349   fixes x :: "'a"
  2350   and   a :: "'x"
  2351   assumes pt: "pt TYPE('a) TYPE('x)"
  2352   and     at: "at TYPE('x)"
  2353   shows "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))"
  2354 proof 
  2355   fix c
  2356   assume "c\<in>((supp ([a].x))::'x set)"
  2357   hence "infinite {b. [(c,b)]\<bullet>([a].x) \<noteq> [a].x}" by (simp add: supp_def)
  2358   hence "infinite {b. [([(c,b)]\<bullet>a)].([(c,b)]\<bullet>x) \<noteq> [a].x}" by (simp add: abs_fun_pi[OF pt, OF at])
  2359   moreover
  2360   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
  2361   ultimately have "infinite {b. ([(c,b)]\<bullet>x,[(c,b)]\<bullet>a) \<noteq> (x, a)}" by (simp add: infinite_super)
  2362   thus "c\<in>(supp (x,a))" by (simp add: supp_def)
  2363 qed
  2364 
  2365 lemma abs_fun_finite_supp:
  2366   fixes x :: "'a"
  2367   and   a :: "'x"
  2368   assumes pt: "pt TYPE('a) TYPE('x)"
  2369   and     at: "at TYPE('x)"
  2370   and     f:  "finite ((supp x)::'x set)"
  2371   shows "finite ((supp ([a].x))::'x set)"
  2372 proof -
  2373   from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at])
  2374   moreover
  2375   have "((supp ([a].x))::'x set) \<subseteq> (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at])
  2376   ultimately show ?thesis by (simp add: finite_subset)
  2377 qed
  2378 
  2379 lemma fresh_abs_funI1:
  2380   fixes  x :: "'a"
  2381   and    a :: "'x"
  2382   and    b :: "'x"
  2383   assumes pt:  "pt TYPE('a) TYPE('x)"
  2384   and     at:   "at TYPE('x)"
  2385   and f:  "finite ((supp x)::'x set)"
  2386   and a1: "b\<sharp>x" 
  2387   and a2: "a\<noteq>b"
  2388   shows "b\<sharp>([a].x)"
  2389   proof -
  2390     have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)" 
  2391     proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
  2392       show "finite ((supp ([a].x))::'x set)" using f
  2393 	by (simp add: abs_fun_finite_supp[OF pt, OF at])	
  2394     qed
  2395     then obtain c where fr1: "c\<noteq>b"
  2396                   and   fr2: "c\<noteq>a"
  2397                   and   fr3: "c\<sharp>x"
  2398                   and   fr4: "c\<sharp>([a].x)"
  2399                   by (force simp add: fresh_prod at_fresh[OF at])
  2400     have e: "[(c,b)]\<bullet>([a].x) = [a].([(c,b)]\<bullet>x)" using a2 fr1 fr2 
  2401       by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  2402     from fr4 have "([(c,b)]\<bullet>c)\<sharp> ([(c,b)]\<bullet>([a].x))"
  2403       by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  2404     hence "b\<sharp>([a].([(c,b)]\<bullet>x))" using fr1 fr2 e  
  2405       by (simp add: at_calc[OF at])
  2406     thus ?thesis using a1 fr3 
  2407       by (simp add: pt_fresh_fresh[OF pt, OF at])
  2408 qed
  2409 
  2410 lemma fresh_abs_funE:
  2411   fixes a :: "'x"
  2412   and   b :: "'x"
  2413   and   x :: "'a"
  2414   assumes pt:  "pt TYPE('a) TYPE('x)"
  2415   and     at:  "at TYPE('x)"
  2416   and     f:  "finite ((supp x)::'x set)"
  2417   and     a1: "b\<sharp>([a].x)" 
  2418   and     a2: "b\<noteq>a" 
  2419   shows "b\<sharp>x"
  2420 proof -
  2421   have "\<exists>c::'x. c\<sharp>(b,a,x,[a].x)"
  2422   proof (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f)
  2423     show "finite ((supp ([a].x))::'x set)" using f
  2424       by (simp add: abs_fun_finite_supp[OF pt, OF at])	
  2425   qed
  2426   then obtain c where fr1: "b\<noteq>c"
  2427                 and   fr2: "c\<noteq>a"
  2428                 and   fr3: "c\<sharp>x"
  2429                 and   fr4: "c\<sharp>([a].x)" by (force simp add: fresh_prod at_fresh[OF at])
  2430   have "[a].x = [(b,c)]\<bullet>([a].x)" using a1 fr4 
  2431     by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  2432   hence "[a].x = [a].([(b,c)]\<bullet>x)" using fr2 a2 
  2433     by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  2434   hence b: "([(b,c)]\<bullet>x) = x" by (simp add: abs_fun_eq1)
  2435   from fr3 have "([(b,c)]\<bullet>c)\<sharp>([(b,c)]\<bullet>x)" 
  2436     by (simp add: pt_fresh_bij[OF pt, OF at]) 
  2437   thus ?thesis using b fr1 by (simp add: at_calc[OF at])
  2438 qed
  2439 
  2440 lemma fresh_abs_funI2:
  2441   fixes a :: "'x"
  2442   and   x :: "'a"
  2443   assumes pt: "pt TYPE('a) TYPE('x)"
  2444   and     at: "at TYPE('x)"
  2445   and     f: "finite ((supp x)::'x set)"
  2446   shows "a\<sharp>([a].x)"
  2447 proof -
  2448   have "\<exists>c::'x. c\<sharp>(a,x)"
  2449     by  (rule at_exists_fresh[OF at], auto simp add: supp_prod at_supp[OF at] f) 
  2450   then obtain c where fr1: "a\<noteq>c" and fr1_sym: "c\<noteq>a" 
  2451                 and   fr2: "c\<sharp>x" by (force simp add: fresh_prod at_fresh[OF at])
  2452   have "c\<sharp>([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
  2453   hence "([(c,a)]\<bullet>c)\<sharp>([(c,a)]\<bullet>([a].x))" using fr1  
  2454     by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  2455   hence a: "a\<sharp>([c].([(c,a)]\<bullet>x))" using fr1_sym 
  2456     by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  2457   have "[c].([(c,a)]\<bullet>x) = ([a].x)" using fr1_sym fr2 
  2458     by (simp add: abs_fun_eq[OF pt, OF at])
  2459   thus ?thesis using a by simp
  2460 qed
  2461 
  2462 lemma fresh_abs_fun_iff: 
  2463   fixes a :: "'x"
  2464   and   b :: "'x"
  2465   and   x :: "'a"
  2466   assumes pt: "pt TYPE('a) TYPE('x)"
  2467   and     at: "at TYPE('x)"
  2468   and     f: "finite ((supp x)::'x set)"
  2469   shows "(b\<sharp>([a].x)) = (b=a \<or> b\<sharp>x)" 
  2470   by (auto  dest: fresh_abs_funE[OF pt, OF at,OF f] 
  2471            intro: fresh_abs_funI1[OF pt, OF at,OF f] 
  2472                   fresh_abs_funI2[OF pt, OF at,OF f])
  2473 
  2474 lemma abs_fun_supp: 
  2475   fixes a :: "'x"
  2476   and   x :: "'a"
  2477   assumes pt: "pt TYPE('a) TYPE('x)"
  2478   and     at: "at TYPE('x)"
  2479   and     f: "finite ((supp x)::'x set)"
  2480   shows "supp ([a].x) = (supp x)-{a}"
  2481  by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f])
  2482 
  2483 (* maybe needs to be better stated as supp intersection supp *)
  2484 lemma abs_fun_supp_ineq: 
  2485   fixes a :: "'y"
  2486   and   x :: "'a"
  2487   assumes pta: "pt TYPE('a) TYPE('x)"
  2488   and     ptb: "pt TYPE('y) TYPE('x)"
  2489   and     at:  "at TYPE('x)"
  2490   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2491   and     dj:  "disjoint TYPE('y) TYPE('x)"
  2492   shows "((supp ([a].x))::'x set) = (supp x)"
  2493 apply(auto simp add: supp_def)
  2494 apply(auto simp add: abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp])
  2495 apply(auto simp add: dj_perm_forget[OF dj])
  2496 apply(auto simp add: abs_fun_eq1) 
  2497 done
  2498 
  2499 lemma fresh_abs_fun_iff_ineq: 
  2500   fixes a :: "'y"
  2501   and   b :: "'x"
  2502   and   x :: "'a"
  2503   assumes pta: "pt TYPE('a) TYPE('x)"
  2504   and     ptb: "pt TYPE('y) TYPE('x)"
  2505   and     at:  "at TYPE('x)"
  2506   and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  2507   and     dj:  "disjoint TYPE('y) TYPE('x)"
  2508   shows "b\<sharp>([a].x) = b\<sharp>x" 
  2509   by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj])
  2510 
  2511 section {* abstraction type for the parsing in nominal datatype *}
  2512 (*==============================================================*)
  2513 consts
  2514   "ABS_set" :: "('x\<Rightarrow>('a noption)) set"
  2515 inductive ABS_set
  2516   intros
  2517   ABS_in: "(abs_fun a x)\<in>ABS_set"
  2518 
  2519 typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
  2520 proof 
  2521   fix x::"'a" and a::"'x"
  2522   show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
  2523 qed
  2524 
  2525 syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
  2526 
  2527 
  2528 section {* lemmas for deciding permutation equations *}
  2529 (*===================================================*)
  2530 
  2531 lemma perm_eq_app:
  2532   fixes f  :: "'a\<Rightarrow>'b"
  2533   and   x  :: "'a"
  2534   and   pi :: "'x prm"
  2535   assumes pt: "pt TYPE('a) TYPE('x)"
  2536   and     at: "at TYPE('x)"
  2537   shows "(pi\<bullet>(f x)=y) = ((pi\<bullet>f)(pi\<bullet>x)=y)"
  2538   by (simp add: pt_fun_app_eq[OF pt, OF at])
  2539 
  2540 lemma perm_eq_lam:
  2541   fixes f  :: "'a\<Rightarrow>'b"
  2542   and   x  :: "'a"
  2543   and   pi :: "'x prm"
  2544   shows "((pi\<bullet>(\<lambda>x. f x))=y) = ((\<lambda>x. (pi\<bullet>(f ((rev pi)\<bullet>x))))=y)"
  2545   by (simp add: perm_fun_def)
  2546 
  2547 
  2548 (***************************************)
  2549 (* setup for the individial atom-kinds *)
  2550 (* and nominal datatypes               *)
  2551 use "nominal_atoms.ML"
  2552 use "nominal_package.ML"
  2553 setup "NominalAtoms.setup"
  2554 
  2555 (*****************************************)
  2556 (* setup for induction principles method *)
  2557 
  2558 use "nominal_induct.ML";
  2559 method_setup nominal_induct =
  2560   {* NominalInduct.nominal_induct_method *}
  2561   {* nominal induction *}
  2562 
  2563 (*******************************)
  2564 (* permutation equality tactic *)
  2565 use "nominal_permeq.ML";
  2566 
  2567 method_setup perm_simp =
  2568   {* perm_eq_meth *}
  2569   {* tactic for deciding equalities involving permutations *}
  2570 
  2571 method_setup perm_simp_debug =
  2572   {* perm_eq_meth_debug *}
  2573   {* tactic for deciding equalities involving permutations including debuging facilities *}
  2574 
  2575 method_setup supports_simp =
  2576   {* supports_meth *}
  2577   {* tactic for deciding whether something supports semthing else *}
  2578 
  2579 method_setup supports_simp_debug =
  2580   {* supports_meth_debug *}
  2581   {* tactic for deciding equalities involving permutations including debuging facilities *}
  2582 
  2583 end