src/HOL/Nominal/Nominal.thy
author berghofe
Mon, 17 Oct 2005 12:30:57 +0200
changeset 17870 c35381811d5c
child 17871 67ffbfcd6fef
permissions -rw-r--r--
Initial revision.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     1
(* $Id$ *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     2
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     3
theory nominal 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     4
imports Main
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     5
  uses ("nominal_package.ML") ("nominal_induct.ML") ("nominal_permeq.ML")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     6
begin 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     7
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     8
ML {* reset NameSpace.unique_names; *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
     9
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    10
section {* Permutations *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    11
(*======================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    12
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    13
types 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    14
  'x prm = "('x \<times> 'x) list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    15
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    16
(* polymorphic operations for permutation and swapping*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    17
consts 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    18
  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     ("_ \<bullet> _" [80,80] 80)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    19
  swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    20
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    21
(* permutation on sets *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    22
defs (overloaded)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    23
  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    24
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    25
(* permutation on units and products *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    26
primrec (perm_unit)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    27
  "pi\<bullet>()    = ()"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    28
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    29
primrec (perm_prod)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    30
  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    31
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    32
lemma perm_fst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    33
  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    34
 by (cases x, simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    35
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    36
lemma perm_snd:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    37
  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    38
 by (cases x, simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    39
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    40
(* permutation on lists *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    41
primrec (perm_list)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    42
  perm_nil_def:  "pi\<bullet>[]     = []"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    43
  perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    44
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    45
lemma perm_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    46
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    47
  and   l1 :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    48
  and   l2 :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    49
  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    50
  by (induct l1, auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    51
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    52
lemma perm_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    53
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    54
  and   l  :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    55
  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    56
  by (induct l, simp_all add: perm_append)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    57
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    58
(* permutation on functions *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    59
defs (overloaded)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    60
  perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    61
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    62
(* permutation on bools *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    63
primrec (perm_bool)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    64
  perm_true_def:  "pi\<bullet>True  = True"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    65
  perm_false_def: "pi\<bullet>False = False"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    66
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    67
(* permutation on options *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    68
primrec (perm_option)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    69
  perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    70
  perm_none_def:  "pi\<bullet>None    = None"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    71
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    72
(* a "private" copy of the option type used in the abstraction function *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    73
datatype 'a nOption = nSome 'a | nNone
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    74
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    75
primrec (perm_noption)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    76
  perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    77
  perm_Nnone_def:  "pi\<bullet>nNone    = nNone"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    78
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    79
(* permutation on characters (used in strings) *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    80
defs (overloaded)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    81
  perm_char_def: "pi\<bullet>(s::char) \<equiv> s"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    82
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    83
(* permutation on ints *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    84
defs (overloaded)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    85
  perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    86
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    87
(* permutation on nats *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    88
defs (overloaded)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    89
  perm_nat_def:    "pi\<bullet>(i::nat) \<equiv> i"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    90
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    91
section {* permutation equality *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    92
(*==============================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    93
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    94
constdefs
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    95
  prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<sim> _ " [80,80] 80)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    96
  "pi1 \<sim> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    97
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    98
section {* Support, Freshness and Supports*}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    99
(*========================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   100
constdefs
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   101
   supp :: "'a \<Rightarrow> ('x set)"  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   102
   "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   103
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   104
   fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (" _ \<sharp> _" [80,80] 80)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   105
   "a \<sharp> x \<equiv> a \<notin> supp x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   106
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   107
   supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   108
   "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   109
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   110
lemma supp_fresh_iff: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   111
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   112
  shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   113
apply(simp add: fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   114
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   115
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   116
lemma supp_unit:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   117
  shows "supp () = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   118
  by (simp add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   119
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   120
lemma supp_prod: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   121
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   122
  and   y :: "'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   123
  shows "(supp (x,y)) = (supp x)\<union>(supp y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   124
  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   125
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   126
lemma supp_list_nil:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   127
  shows "supp [] = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   128
apply(simp add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   129
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   130
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   131
lemma supp_list_cons:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   132
  fixes x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   133
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   134
  shows "supp (x#xs) = (supp x)\<union>(supp xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   135
apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   136
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   137
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   138
lemma supp_list_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   139
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   140
  and   ys :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   141
  shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   142
  by (induct xs, auto simp add: supp_list_nil supp_list_cons)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   143
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   144
lemma supp_list_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   145
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   146
  shows "supp (rev xs) = (supp xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   147
  by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   148
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   149
lemma supp_bool:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   150
  fixes x  :: "bool"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   151
  shows "supp (x) = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   152
  apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   153
  apply(simp_all add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   154
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   155
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   156
lemma supp_some:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   157
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   158
  shows "supp (Some x) = (supp x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   159
  apply(simp add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   160
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   161
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   162
lemma supp_none:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   163
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   164
  shows "supp (None) = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   165
  apply(simp add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   166
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   167
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   168
lemma supp_int:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   169
  fixes i::"int"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   170
  shows "supp (i) = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   171
  apply(simp add: supp_def perm_int_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   172
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   173
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   174
lemma fresh_prod:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   175
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   176
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   177
  and   y :: "'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   178
  shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   179
  by (simp add: fresh_def supp_prod)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   180
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   181
lemma fresh_list_nil:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   182
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   183
  shows "a\<sharp>([]::'a list)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   184
  by (simp add: fresh_def supp_list_nil) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   185
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   186
lemma fresh_list_cons:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   187
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   188
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   189
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   190
  shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   191
  by (simp add: fresh_def supp_list_cons)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   192
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   193
lemma fresh_list_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   194
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   195
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   196
  and   ys :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   197
  shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   198
  by (simp add: fresh_def supp_list_append)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   199
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   200
lemma fresh_list_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   201
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   202
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   203
  shows "a\<sharp>(rev xs) = a\<sharp>xs"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   204
  by (simp add: fresh_def supp_list_rev)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   205
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   206
lemma fresh_none:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   207
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   208
  shows "a\<sharp>None"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   209
  apply(simp add: fresh_def supp_none)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   210
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   211
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   212
lemma fresh_some:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   213
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   214
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   215
  shows "a\<sharp>(Some x) = a\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   216
  apply(simp add: fresh_def supp_some)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   217
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   218
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   219
section {* Abstract Properties for Permutations and  Atoms *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   220
(*=========================================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   221
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   222
(* properties for being a permutation type *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   223
constdefs 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   224
  "pt TYPE('a) TYPE('x) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   225
     (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   226
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   227
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<sim> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   228
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   229
(* properties for being an atom type *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   230
constdefs 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   231
  "at TYPE('x) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   232
     (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   233
     (\<forall>(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\<bullet>x = swap (a,b) (pi\<bullet>x)) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   234
     (\<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> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   235
     (infinite (UNIV::'x set))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   236
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   237
(* property of two atom-types being disjoint *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   238
constdefs
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   239
  "disjoint TYPE('x) TYPE('y) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   240
       (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   241
       (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   242
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   243
(* composition property of two permutation on a type 'a *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   244
constdefs
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   245
  "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   246
      (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   247
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   248
(* property of having finite support *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   249
constdefs 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   250
  "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   251
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   252
section {* Lemmas about the atom-type properties*}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   253
(*==============================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   254
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   255
lemma at1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   256
  fixes x::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   257
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   258
  shows "([]::'x prm)\<bullet>x = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   259
  using a by (simp add: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   260
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   261
lemma at2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   262
  fixes a ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   263
  and   b ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   264
  and   x ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   265
  and   pi::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   266
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   267
  shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   268
  using a by (simp only: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   269
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   270
lemma at3: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   271
  fixes a ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   272
  and   b ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   273
  and   c ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   274
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   275
  shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   276
  using a by (simp only: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   277
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   278
(* rules to calculate simple premutations *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   279
lemmas at_calc = at2 at1 at3
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   280
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   281
lemma at4: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   282
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   283
  shows "infinite (UNIV::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   284
  using a by (simp add: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   285
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   286
lemma at_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   287
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   288
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   289
  and   c   :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   290
  assumes at: "at TYPE('x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   291
  shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   292
proof (induct pi1)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   293
  case Nil show ?case by (simp add: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   294
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   295
  case (Cons x xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   296
  assume i: "(xs @ pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   297
  have "(x#xs)@pi2 = x#(xs@pi2)" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   298
  thus ?case using i by (cases "x", simp add:  at2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   299
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   300
 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   301
lemma at_swap:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   302
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   303
  and   b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   304
  and   c :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   305
  assumes at: "at TYPE('x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   306
  shows "swap (a,b) (swap (a,b) c) = c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   307
  by (auto simp add: at3[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   308
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   309
lemma at_rev_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   310
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   311
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   312
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   313
  shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   314
proof(induct pi)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   315
  case Nil show ?case by (simp add: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   316
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   317
  case (Cons x xs) thus ?case 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   318
    by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   319
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   320
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   321
lemma at_pi_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   322
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   323
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   324
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   325
  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   326
  by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   327
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   328
lemma at_bij1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   329
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   330
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   331
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   332
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   333
  and     a:  "(pi\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   334
  shows   "x=(rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   335
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   336
  from a have "y=(pi\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   337
  thus ?thesis by (simp only: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   338
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   339
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   340
lemma at_bij2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   341
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   342
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   343
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   344
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   345
  and     a:  "((rev pi)\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   346
  shows   "x=pi\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   347
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   348
  from a have "y=((rev pi)\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   349
  thus ?thesis by (simp only: at_pi_rev[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   350
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   351
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   352
lemma at_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   353
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   354
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   355
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   356
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   357
  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   358
proof 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   359
  assume "pi\<bullet>x = pi\<bullet>y" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   360
  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   361
  thus "x=y" by (simp only: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   362
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   363
  assume "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   364
  thus "pi\<bullet>x = pi\<bullet>y" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   365
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   366
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   367
lemma at_supp:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   368
  fixes x :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   369
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   370
  shows "supp x = {x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   371
proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   372
  assume f: "finite {b::'x. b \<noteq> x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   373
  have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   374
  have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   375
  from f a1 a2 show False by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   376
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   377
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   378
lemma at_fresh:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   379
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   380
  and   b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   381
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   382
  shows "(a\<sharp>b) = (a\<noteq>b)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   383
  by (simp add: at_supp[OF at] fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   384
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   385
lemma at_prm_fresh[rule_format]:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   386
  fixes c :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   387
  and   pi:: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   388
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   389
  shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   390
apply(induct pi)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   391
apply(simp add: at1[OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   392
apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   393
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   394
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   395
lemma at_prm_rev_eq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   396
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   397
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   398
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   399
  shows a: "((rev pi1) \<sim> (rev pi2)) = (pi1 \<sim> pi2)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   400
proof (simp add: prm_eq_def, auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   401
  fix x
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   402
  assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   403
  hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   404
  hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   405
  hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   406
  thus "pi1 \<bullet> x  =  pi2 \<bullet> x" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   407
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   408
  fix x
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   409
  assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   410
  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   411
  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   412
  hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   413
  thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   414
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   415
  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   416
lemma at_prm_rev_eq1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   417
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   418
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   419
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   420
  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1) \<sim> (rev pi2)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   421
  by (simp add: at_prm_rev_eq[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   422
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   423
lemma at_ds1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   424
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   425
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   426
  shows "[(a,a)] \<sim> []"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   427
  by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   428
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   429
lemma at_ds2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   430
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   431
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   432
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   433
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   434
  shows "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<sim> ([(a,b)]@pi)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   435
  by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   436
      at_rev_pi[OF at] at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   437
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   438
lemma at_ds3: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   439
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   440
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   441
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   442
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   443
  and     a:  "distinct [a,b,c]"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   444
  shows "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   445
  using a by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   446
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   447
lemma at_ds4: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   448
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   449
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   450
  and   pi  :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   451
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   452
  shows "(pi@[(a,(rev pi)\<bullet>b)]) \<sim> ([(pi\<bullet>a,b)]@pi)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   453
  by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   454
      at_pi_rev[OF at] at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   455
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   456
lemma at_ds5: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   457
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   458
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   459
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   460
  shows "[(a,b)] \<sim> [(b,a)]"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   461
  by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   462
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   463
lemma at_ds6: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   464
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   465
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   466
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   467
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   468
  and     a: "distinct [a,b,c]"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   469
  shows "[(a,c),(a,b)] \<sim> [(b,c),(a,c)]"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   470
  using a by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   471
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   472
lemma at_ds7:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   473
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   474
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   475
  shows "((rev pi)@pi) \<sim> []"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   476
  by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   477
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   478
lemma at_ds8_aux:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   479
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   480
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   481
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   482
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   483
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   484
  shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   485
  by (force simp add: at_calc[OF at] at_bij[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   486
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   487
lemma at_ds8: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   488
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   489
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   490
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   491
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   492
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   493
  shows "(pi1@pi2) \<sim> ((pi1\<bullet>pi2)@pi1)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   494
apply(induct_tac pi2)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   495
apply(simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   496
apply(auto simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   497
apply(simp add: at2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   498
apply(drule_tac x="aa" in spec)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   499
apply(drule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   500
apply(simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   501
apply(simp add: at_append[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   502
apply(simp add: at2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   503
apply(simp add: at_ds8_aux[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   504
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   505
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   506
lemma at_ds9: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   507
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   508
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   509
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   510
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   511
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   512
  shows " ((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   513
apply(induct_tac pi2)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   514
apply(simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   515
apply(auto simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   516
apply(simp add: at_append[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   517
apply(simp add: at2[OF at] at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   518
apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   519
apply(drule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   520
apply(simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   521
apply(simp add: at_ds8_aux[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   522
apply(simp add: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   523
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   524
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   525
--"there always exists an atom not being in a finite set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   526
lemma ex_in_inf:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   527
  fixes   A::"'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   528
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   529
  and     fs: "finite A"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   530
  shows "\<exists>c::'x. c\<notin>A"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   531
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   532
  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   533
    by (simp add: Diff_infinite_finite)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   534
  hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   535
  hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   536
  thus "\<exists>c::'x. c\<notin>A" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   537
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   538
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   539
--"there always exists a fresh name for an object with finite support"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   540
lemma at_exists_fresh: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   541
  fixes  x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   542
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   543
  and     fs: "finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   544
  shows "\<exists>c::'x. c\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   545
  by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   546
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   547
--"the at-props imply the pt-props"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   548
lemma at_pt_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   549
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   550
  shows "pt TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   551
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   552
apply(simp only: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   553
apply(simp only: at_append[OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   554
apply(simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   555
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   556
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   557
section {* finite support properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   558
(*===================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   559
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   560
lemma fs1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   561
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   562
  assumes a: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   563
  shows "finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   564
  using a by (simp add: fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   565
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   566
lemma fs_at_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   567
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   568
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   569
  shows "fs TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   570
apply(simp add: fs_def) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   571
apply(simp add: at_supp[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   572
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   573
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   574
lemma fs_unit_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   575
  shows "fs TYPE(unit) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   576
apply(simp add: fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   577
apply(simp add: supp_unit)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   578
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   579
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   580
lemma fs_prod_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   581
  assumes fsa: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   582
  and     fsb: "fs TYPE('b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   583
  shows "fs TYPE('a\<times>'b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   584
apply(unfold fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   585
apply(auto simp add: supp_prod)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   586
apply(rule fs1[OF fsa])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   587
apply(rule fs1[OF fsb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   588
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   589
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   590
lemma fs_list_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   591
  assumes fs: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   592
  shows "fs TYPE('a list) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   593
apply(simp add: fs_def, rule allI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   594
apply(induct_tac x)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   595
apply(simp add: supp_list_nil)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   596
apply(simp add: supp_list_cons)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   597
apply(rule fs1[OF fs])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   598
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   599
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   600
lemma fs_bool_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   601
  shows "fs TYPE(bool) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   602
apply(simp add: fs_def, rule allI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   603
apply(simp add: supp_bool)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   604
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   605
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   606
lemma fs_int_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   607
  shows "fs TYPE(int) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   608
apply(simp add: fs_def, rule allI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   609
apply(simp add: supp_int)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   610
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   611
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   612
section {* Lemmas about the permutation properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   613
(*=================================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   614
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   615
lemma pt1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   616
  fixes x::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   617
  assumes a: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   618
  shows "([]::'x prm)\<bullet>x = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   619
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   620
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   621
lemma pt2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   622
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   623
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   624
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   625
  assumes a: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   626
  shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   627
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   628
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   629
lemma pt3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   630
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   631
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   632
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   633
  assumes a: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   634
  shows "pi1 \<sim> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   635
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   636
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   637
lemma pt3_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   638
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   639
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   640
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   641
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   642
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   643
  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   644
  by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   645
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   646
section {* composition properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   647
(* ============================== *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   648
lemma cp1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   649
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   650
  and   pi2::"'y prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   651
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   652
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   653
  shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   654
  using cp by (simp add: cp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   655
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   656
lemma cp_pt_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   657
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   658
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   659
  shows "cp TYPE('a) TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   660
apply(auto simp add: cp_def pt2[OF pt,symmetric])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   661
apply(rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   662
apply(rule at_ds8[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   663
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   664
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   665
section {* permutation type instances *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   666
(* ===================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   667
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   668
lemma pt_set_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   669
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   670
  shows  "pt TYPE('a set) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   671
apply(simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   672
apply(simp_all add: perm_set_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   673
apply(simp add: pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   674
apply(force simp add: pt2[OF pt] pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   675
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   676
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   677
lemma pt_list_nil: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   678
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   679
  assumes pt: "pt TYPE('a) TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   680
  shows "([]::'x prm)\<bullet>xs = xs" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   681
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   682
apply(simp_all add: pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   683
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   684
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   685
lemma pt_list_append: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   686
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   687
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   688
  and   xs  :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   689
  assumes pt: "pt TYPE('a) TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   690
  shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   691
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   692
apply(simp_all add: pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   693
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   694
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   695
lemma pt_list_prm_eq: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   696
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   697
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   698
  and   xs  :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   699
  assumes pt: "pt TYPE('a) TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   700
  shows "pi1 \<sim> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   701
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   702
apply(simp_all add: prm_eq_def pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   703
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   704
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   705
lemma pt_list_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   706
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   707
  shows  "pt TYPE('a list) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   708
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   709
apply(rule pt_list_nil[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   710
apply(rule pt_list_append[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   711
apply(rule pt_list_prm_eq[OF pt],assumption)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   712
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   713
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   714
lemma pt_unit_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   715
  shows  "pt TYPE(unit) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   716
  by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   717
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   718
lemma pt_prod_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   719
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   720
  and     ptb: "pt TYPE('b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   721
  shows  "pt TYPE('a \<times> 'b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   722
  apply(auto simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   723
  apply(rule pt1[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   724
  apply(rule pt1[OF ptb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   725
  apply(rule pt2[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   726
  apply(rule pt2[OF ptb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   727
  apply(rule pt3[OF pta],assumption)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   728
  apply(rule pt3[OF ptb],assumption)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   729
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   730
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   731
lemma pt_fun_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   732
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   733
  and     ptb: "pt TYPE('b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   734
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   735
  shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   736
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   737
apply(simp_all add: perm_fun_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   738
apply(simp add: pt1[OF pta] pt1[OF ptb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   739
apply(simp add: pt2[OF pta] pt2[OF ptb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   740
apply(subgoal_tac "(rev pi1) \<sim> (rev pi2)")(*A*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   741
apply(simp add: pt3[OF pta] pt3[OF ptb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   742
(*A*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   743
apply(simp add: at_prm_rev_eq[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   744
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   745
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   746
lemma pt_option_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   747
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   748
  shows  "pt TYPE('a option) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   749
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   750
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   751
apply(simp_all add: pt1[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   752
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   753
apply(simp_all add: pt2[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   754
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   755
apply(simp_all add: pt3[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   756
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   757
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   758
lemma pt_noption_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   759
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   760
  shows  "pt TYPE('a nOption) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   761
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   762
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   763
apply(simp_all add: pt1[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   764
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   765
apply(simp_all add: pt2[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   766
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   767
apply(simp_all add: pt3[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   768
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   769
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   770
lemma pt_bool_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   771
  shows  "pt TYPE(bool) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   772
  apply(auto simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   773
  apply(case_tac "x=True", simp add: perm_bool_def, simp add: perm_bool_def)+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   774
  done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   775
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   776
lemma pt_prm_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   777
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   778
  shows  "pt TYPE('x prm) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   779
apply(rule pt_list_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   780
apply(rule pt_prod_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   781
apply(rule at_pt_inst[OF at])+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   782
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   783
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   784
section {* further lemmas for permutation types *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   785
(*==============================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   786
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   787
lemma pt_rev_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   788
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   789
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   790
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   791
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   792
  shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   793
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   794
  have "((rev pi)@pi) \<sim> ([]::'x prm)" by (simp add: at_ds7[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   795
  hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   796
  thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   797
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   798
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   799
lemma pt_pi_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   800
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   801
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   802
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   803
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   804
  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   805
  by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   806
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   807
lemma pt_bij1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   808
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   809
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   810
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   811
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   812
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   813
  and     a:  "(pi\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   814
  shows   "x=(rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   815
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   816
  from a have "y=(pi\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   817
  thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   818
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   819
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   820
lemma pt_bij2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   821
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   822
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   823
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   824
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   825
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   826
  and     a:  "x = (rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   827
  shows   "(pi\<bullet>x)=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   828
  using a by (simp add: pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   829
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   830
lemma pt_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   831
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   832
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   833
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   834
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   835
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   836
  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   837
proof 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   838
  assume "pi\<bullet>x = pi\<bullet>y" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   839
  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   840
  thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   841
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   842
  assume "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   843
  thus "pi\<bullet>x = pi\<bullet>y" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   844
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   845
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   846
lemma pt_bij3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   847
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   848
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   849
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   850
  assumes a:  "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   851
  shows "(pi\<bullet>x = pi\<bullet>y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   852
using a by simp 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   853
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   854
lemma pt_bij4:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   855
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   856
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   857
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   858
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   859
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   860
  and     a:  "pi\<bullet>x = pi\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   861
  shows "x = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   862
using a by (simp add: pt_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   863
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   864
lemma pt_swap_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   865
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   866
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   867
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   868
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   869
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   870
  shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   871
  by (rule pt_bij2[OF pt, OF at], simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   872
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   873
lemma pt_set_bij1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   874
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   875
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   876
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   877
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   878
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   879
  shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   880
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   881
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   882
lemma pt_set_bij1a:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   883
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   884
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   885
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   886
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   887
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   888
  shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   889
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   890
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   891
lemma pt_set_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   892
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   893
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   894
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   895
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   896
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   897
  shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   898
  by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   899
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   900
lemma pt_set_bij2:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   901
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   902
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   903
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   904
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   905
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   906
  and     a:  "x\<in>X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   907
  shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   908
  using a by (simp add: pt_set_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   909
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   910
lemma pt_set_bij3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   911
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   912
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   913
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   914
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   915
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   916
  shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   917
apply(case_tac "x\<in>X = True")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   918
apply(auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   919
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   920
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   921
lemma pt_list_set_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   922
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   923
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   924
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   925
  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   926
by (induct xs, auto simp add: perm_set_def pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   927
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   928
-- "some helper lemmas for the pt_perm_supp_ineq lemma"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   929
lemma Collect_permI: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   930
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   931
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   932
  assumes a: "\<forall>x. (P1 x = P2 x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   933
  shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>x| x. P2 x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   934
  using a by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   935
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   936
lemma Infinite_cong:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   937
  assumes a: "X = Y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   938
  shows "infinite X = infinite Y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   939
  using a by (simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   940
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   941
lemma pt_set_eq_ineq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   942
  fixes pi :: "'y prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   943
  assumes pt: "pt TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   944
  and     at: "at TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   945
  shows "{pi\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>x)}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   946
  by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   947
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   948
lemma pt_inject_on_ineq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   949
  fixes X  :: "'y set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   950
  and   pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   951
  assumes pt: "pt TYPE('y) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   952
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   953
  shows "inj_on (perm pi) X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   954
proof (unfold inj_on_def, intro strip)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   955
  fix x::"'y" and y::"'y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   956
  assume "pi\<bullet>x = pi\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   957
  thus "x=y" by (simp add: pt_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   958
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   959
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   960
lemma pt_set_finite_ineq: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   961
  fixes X  :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   962
  and   pi :: "'y prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   963
  assumes pt: "pt TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   964
  and     at: "at TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   965
  shows "finite (pi\<bullet>X) = finite X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   966
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   967
  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   968
  show ?thesis
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   969
  proof (rule iffI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   970
    assume "finite (pi\<bullet>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   971
    hence "finite (perm pi ` X)" using image by (simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   972
    thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   973
  next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   974
    assume "finite X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   975
    hence "finite (perm pi ` X)" by (rule finite_imageI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   976
    thus "finite (pi\<bullet>X)" using image by (simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   977
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   978
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   979
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   980
lemma pt_set_infinite_ineq: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   981
  fixes X  :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   982
  and   pi :: "'y prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   983
  assumes pt: "pt TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   984
  and     at: "at TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   985
  shows "infinite (pi\<bullet>X) = infinite X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   986
using pt at by (simp add: pt_set_finite_ineq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   987
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   988
lemma pt_perm_supp_ineq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   989
  fixes  pi  :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   990
  and    x   :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   991
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   992
  and     ptb: "pt TYPE('y) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   993
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   994
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   995
  shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   996
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   997
  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   998
  also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   999
  proof (rule Collect_permI, rule allI, rule iffI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1000
    fix a
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1001
    assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1002
    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1003
    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1004
  next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1005
    fix a
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1006
    assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1007
    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1008
    thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1009
      by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1010
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1011
  also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1012
    by (simp add: pt_set_eq_ineq[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1013
  also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1014
    by (simp add: pt_bij[OF pta, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1015
  also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1016
  proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1017
    fix a::"'y" and b::"'y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1018
    have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1019
      by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1020
    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
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1021
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1022
  finally show "?LHS = ?RHS" by (simp add: supp_def) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1023
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1024
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1025
lemma pt_perm_supp:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1026
  fixes  pi  :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1027
  and    x   :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1028
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1029
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1030
  shows "(pi\<bullet>((supp x)::'x set)) = supp (pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1031
apply(rule pt_perm_supp_ineq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1032
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1033
apply(rule at_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1034
apply(rule at)+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1035
apply(rule cp_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1036
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1037
apply(rule at)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1038
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1039
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1040
lemma pt_supp_finite_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1041
  fixes  pi  :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1042
  and    x   :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1043
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1044
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1045
  and     f: "finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1046
  shows "finite ((supp (pi\<bullet>x))::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1047
apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1048
apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1049
apply(rule f)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1050
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1051
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1052
lemma pt_fresh_left_ineq:  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1053
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1054
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1055
  and     a :: "'y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1056
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1057
  and     ptb: "pt TYPE('y) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1058
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1059
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1060
  shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1061
apply(simp add: fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1062
apply(simp add: pt_set_bij1[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1063
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1064
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1065
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1066
lemma pt_fresh_right_ineq:  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1067
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1068
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1069
  and     a :: "'y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1070
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1071
  and     ptb: "pt TYPE('y) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1072
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1073
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1074
  shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1075
apply(simp add: fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1076
apply(simp add: pt_set_bij1[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1077
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1078
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1079
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1080
lemma pt_fresh_bij_ineq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1081
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1082
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1083
  and     a :: "'y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1084
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1085
  and     ptb: "pt TYPE('y) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1086
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1087
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1088
  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1089
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1090
apply(simp add: pt_rev_pi[OF ptb, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1091
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1092
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1093
lemma pt_fresh_left:  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1094
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1095
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1096
  and     a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1097
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1098
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1099
  shows "a\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1100
apply(rule pt_fresh_left_ineq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1101
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1102
apply(rule at_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1103
apply(rule at)+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1104
apply(rule cp_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1105
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1106
apply(rule at)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1107
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1108
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1109
lemma pt_fresh_right:  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1110
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1111
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1112
  and     a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1113
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1114
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1115
  shows "(pi\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1116
apply(rule pt_fresh_right_ineq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1117
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1118
apply(rule at_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1119
apply(rule at)+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1120
apply(rule cp_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1121
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1122
apply(rule at)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1123
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1124
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1125
lemma pt_fresh_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1126
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1127
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1128
  and     a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1129
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1130
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1131
  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1132
apply(rule pt_fresh_bij_ineq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1133
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1134
apply(rule at_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1135
apply(rule at)+
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1136
apply(rule cp_pt_inst)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1137
apply(rule pt)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1138
apply(rule at)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1139
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1140
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1141
lemma pt_fresh_bij1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1142
  fixes  pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1143
  and     x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1144
  and     a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1145
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1146
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1147
  and     a:  "a\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1148
  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1149
using a by (simp add: pt_fresh_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1150
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1151
lemma pt_perm_fresh1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1152
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1153
  and   b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1154
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1155
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1156
  and     at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1157
  and     a1: "\<not>(a\<sharp>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1158
  and     a2: "b\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1159
  shows "[(a,b)]\<bullet>x \<noteq> x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1160
proof
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1161
  assume neg: "[(a,b)]\<bullet>x = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1162
  from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1163
  from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1164
  from a1' a2' have a3: "a\<noteq>b" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1165
  from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1166
    by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1167
  hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1168
  hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1169
  with a2' neg show False by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1170
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1171
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1172
-- "three helper lemmas for the perm_fresh_fresh-lemma"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1173
lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1174
  by (auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1175
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1176
lemma infinite_or_neg_infinite:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1177
  assumes h:"infinite (UNIV::'a set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1178
  shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1179
proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1180
  assume j:"finite {b::'a. P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1181
  have "infinite ((UNIV::'a set) - {b::'a. P b})"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1182
    using Diff_infinite_finite[OF j h] by auto
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1183
  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1184
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1185
  assume j:"infinite {b::'a. P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1186
  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1187
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1188
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1189
--"the co-set of a finite set is infinte"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1190
lemma finite_infinite:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1191
  assumes a: "finite {b::'x. P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1192
  and     b: "infinite (UNIV::'x set)"        
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1193
  shows "infinite {b. \<not>P b}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1194
  using a and infinite_or_neg_infinite[OF b] by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1195
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1196
lemma pt_fresh_fresh:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1197
  fixes   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1198
  and     a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1199
  and     b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1200
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1201
  and     at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1202
  and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1203
  shows "[(a,b)]\<bullet>x=x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1204
proof (cases "a=b")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1205
  assume c1: "a=b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1206
  have "[(a,a)] \<sim> []" by (rule at_ds1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1207
  hence "[(a,b)] \<sim> []" using c1 by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1208
  hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1209
  thus ?thesis by (simp only: pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1210
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1211
  assume c2: "a\<noteq>b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1212
  from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1213
  from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1214
  from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1215
    by (force simp only: Collect_disj_eq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1216
  have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1217
    by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1218
  hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1219
    by (force dest: Diff_infinite_finite)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1220
  hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1221
    by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1222
  hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1223
  then obtain c 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1224
    where eq1: "[(a,c)]\<bullet>x = x" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1225
      and eq2: "[(b,c)]\<bullet>x = x" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1226
      and ineq: "a\<noteq>c \<and> b\<noteq>c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1227
    by (force)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1228
  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1229
  hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1230
  from c2 ineq have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" by (simp add: at_ds3[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1231
  hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1232
  thus ?thesis using eq3 by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1233
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1234
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1235
lemma pt_perm_compose:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1236
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1237
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1238
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1239
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1240
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1241
  shows "pi2\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1242
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1243
  have "(pi2@pi1) \<sim> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1244
  hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1245
  thus ?thesis by (simp add: pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1246
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1247
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1248
lemma pt_perm_compose_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1249
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1250
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1251
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1252
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1253
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1254
  shows "(rev pi2)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1255
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1256
  have "((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1257
  hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1258
  thus ?thesis by (simp add: pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1259
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1260
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1261
section {* facts about supports *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1262
(*==============================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1263
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1264
lemma supports_subset:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1265
  fixes x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1266
  and   S1 :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1267
  and   S2 :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1268
  assumes  a: "S1 supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1269
  and      b: "S1\<subseteq>S2"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1270
  shows "S2 supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1271
  using a b
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1272
  by (force simp add: "op supports_def")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1273
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1274
lemma supp_supports:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1275
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1276
  assumes  pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1277
  and      at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1278
  shows "((supp x)::'x set) supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1279
proof (unfold "op supports_def", intro strip)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1280
  fix a b
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1281
  assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1282
  hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1283
  thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1284
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1285
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1286
lemma supp_is_subset:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1287
  fixes S :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1288
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1289
  assumes a1: "S supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1290
  and     a2: "finite S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1291
  shows "(supp x)\<subseteq>S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1292
proof (rule ccontr)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1293
  assume "\<not>(supp x \<subseteq> S)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1294
  hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1295
  then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1296
  from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1297
  with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1298
  with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1299
  hence "a\<notin>(supp x)" by (unfold supp_def, auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1300
  with b1 show False by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1301
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1302
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1303
lemma supports_finite:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1304
  fixes S :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1305
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1306
  assumes a1: "S supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1307
  and     a2: "finite S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1308
  shows "finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1309
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1310
  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1311
  thus ?thesis using a2 by (simp add: finite_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1312
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1313
  
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1314
lemma supp_is_inter:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1315
  fixes  x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1316
  assumes  pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1317
  and      at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1318
  and      fs: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1319
  shows "((supp x)::'x set) = (\<Inter> {S. finite S \<and> S supports x})"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1320
proof (rule equalityI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1321
  show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1322
  proof (clarify)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1323
    fix S c
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1324
    assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1325
    hence  "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1326
    with b show "c\<in>S" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1327
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1328
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1329
  show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1330
  proof (clarify, simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1331
    fix c
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1332
    assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1333
    have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1334
    with d fs1[OF fs] show "c\<in>supp x" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1335
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1336
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1337
    
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1338
lemma supp_is_least_supports:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1339
  fixes S :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1340
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1341
  assumes  pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1342
  and      at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1343
  and      a1: "S supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1344
  and      a2: "finite S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1345
  and      a3: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1346
  shows "S = (supp x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1347
proof (rule equalityI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1348
  show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1349
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1350
  have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1351
  have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1352
  hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1353
  with s1 a3 show "S\<subseteq>supp x" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1354
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1355
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1356
lemma supports_set:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1357
  fixes S :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1358
  and   X :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1359
  assumes  pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1360
  and      at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1361
  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)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1362
  shows  "S supports X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1363
using a
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1364
apply(auto simp add: "op supports_def")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1365
apply(simp add: pt_set_bij1a[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1366
apply(force simp add: pt_swap_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1367
apply(simp add: pt_set_bij1a[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1368
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1369
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1370
lemma supports_fresh:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1371
  fixes S :: "'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1372
  and   a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1373
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1374
  assumes a1: "S supports x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1375
  and     a2: "finite S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1376
  and     a3: "a\<notin>S"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1377
  shows "a\<sharp>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1378
proof (simp add: fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1379
  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1380
  thus "a\<notin>(supp x)" using a3 by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1381
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1382
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1383
lemma at_fin_set_supports:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1384
  fixes X::"'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1385
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1386
  shows "X supports X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1387
proof (simp add: "op supports_def", intro strip)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1388
  fix a b
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1389
  assume "a\<notin>X \<and> b\<notin>X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1390
  thus "[(a,b)]\<bullet>X = X" by (force simp add: perm_set_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1391
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1392
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1393
lemma at_fin_set_supp:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1394
  fixes X::"'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1395
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1396
  and     fs: "finite X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1397
  shows "(supp X) = X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1398
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1399
  have pt_set: "pt TYPE('x set) TYPE('x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1400
    by (rule pt_set_inst[OF at_pt_inst[OF at]])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1401
  have X_supports_X: "X supports X" by (rule at_fin_set_supports[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1402
  show ?thesis using  pt_set at X_supports_X fs
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1403
  proof (rule supp_is_least_supports[symmetric])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1404
    show "\<forall>S'. finite S' \<and> S' supports X \<longrightarrow> X \<subseteq> S'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1405
    proof (auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1406
      fix S'::"'x set" and x::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1407
      assume f: "finite S'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1408
      and    s: "S' supports X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1409
      and    e1: "x\<in>X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1410
      show "x\<in>S'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1411
      proof (rule ccontr)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1412
	assume e2: "x\<notin>S'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1413
	have "\<exists>b. b\<notin>(X\<union>S')" by (force intro: ex_in_inf[OF at] simp only: fs f)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1414
	then obtain b where b1: "b\<notin>X" and b2: "b\<notin>S'" by (auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1415
	from s e2 b2 have c1: "[(x,b)]\<bullet>X=X" by (simp add: "op supports_def")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1416
	from e1 b1 have c2: "[(x,b)]\<bullet>X\<noteq>X" by (force simp add: perm_set_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1417
	show "False" using c1 c2 by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1418
      qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1419
    qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1420
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1421
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1422
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1423
section {* Permutations acting on Functions *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1424
(*==========================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1425
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1426
lemma pt_fun_app_eq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1427
  fixes f  :: "'a\<Rightarrow>'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1428
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1429
  and   pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1430
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1431
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1432
  shows "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1433
  by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1434
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1435
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1436
--"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1437
lemma pt_perm:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1438
  fixes x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1439
  and   pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1440
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1441
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1442
  and     at: "at TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1443
  shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1444
  by (simp add: pt_fun_app_eq[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1445
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1446
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1447
lemma pt_fun_eq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1448
  fixes f  :: "'a\<Rightarrow>'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1449
  and   pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1450
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1451
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1452
  shows "(pi\<bullet>f = f) = (\<forall> x. pi\<bullet>(f x) = f (pi\<bullet>x))" (is "?LHS = ?RHS")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1453
proof
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1454
  assume a: "?LHS"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1455
  show "?RHS"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1456
  proof
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1457
    fix x
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1458
    have "pi\<bullet>(f x) = (pi\<bullet>f)(pi\<bullet>x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1459
    also have "\<dots> = f (pi\<bullet>x)" using a by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1460
    finally show "pi\<bullet>(f x) = f (pi\<bullet>x)" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1461
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1462
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1463
  assume b: "?RHS"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1464
  show "?LHS"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1465
  proof (rule ccontr)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1466
    assume "(pi\<bullet>f) \<noteq> f"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1467
    hence "\<exists>c. (pi\<bullet>f) c \<noteq> f c" by (simp add: expand_fun_eq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1468
    then obtain c where b1: "(pi\<bullet>f) c \<noteq> f c" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1469
    from b have "pi\<bullet>(f ((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1470
    hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>c)) = f (pi\<bullet>((rev pi)\<bullet>c))" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1471
      by (simp add: pt_fun_app_eq[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1472
    hence "(pi\<bullet>f) c = f c" by (simp add: pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1473
    with b1 show "False" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1474
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1475
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1476
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1477
-- "two helper lemmas for the equivariance of functions"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1478
lemma pt_swap_eq_aux:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1479
  fixes   y :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1480
  and    pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1481
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1482
  and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1483
  shows "pi\<bullet>y = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1484
proof(induct pi)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1485
    case Nil show ?case by (simp add: pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1486
  next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1487
    case (Cons x xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1488
    have "\<exists>a b. x=(a,b)" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1489
    then obtain a b where p: "x=(a,b)" by force
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1490
    assume i: "xs\<bullet>y = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1491
    have "x#xs = [x]@xs" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1492
    hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1493
    hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1494
    thus ?case using a i p by (force)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1495
  qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1496
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1497
lemma pt_swap_eq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1498
  fixes   y :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1499
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1500
  shows "(\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y) = (\<forall>pi::'x prm. pi\<bullet>y = y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1501
  by (force intro: pt_swap_eq_aux[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1502
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1503
lemma pt_eqvt_fun1a:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1504
  fixes f     :: "'a\<Rightarrow>'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1505
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1506
  and     ptb: "pt TYPE('b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1507
  and     at:  "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1508
  and     a:   "((supp f)::'x set)={}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1509
  shows "\<forall>(pi::'x prm). pi\<bullet>f = f" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1510
proof (intro strip)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1511
  fix pi
c35381811d5c Initial revision.
berghofe