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