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