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