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