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