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