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