src/HOL/Nominal/Nominal.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 48891 c0eafbd55de3
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19494
2e909d5309f4 Renamed "nominal" theory to "Nominal".
berghofe
parents: 19477
diff changeset
     1
theory Nominal 
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 39777
diff changeset
     2
imports Main "~~/src/HOL/Library/Infinite_Set"
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
     3
keywords
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
     4
  "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
     5
  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
     6
  "avoids"
18068
e8c3d371594e Moved atom stuff to new file nominal_atoms.ML
berghofe
parents: 18053
diff changeset
     7
uses
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22231
diff changeset
     8
  ("nominal_thmdecls.ML")
18068
e8c3d371594e Moved atom stuff to new file nominal_atoms.ML
berghofe
parents: 18053
diff changeset
     9
  ("nominal_atoms.ML")
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31723
diff changeset
    10
  ("nominal_datatype.ML")
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
    11
  ("nominal_induct.ML") 
18068
e8c3d371594e Moved atom stuff to new file nominal_atoms.ML
berghofe
parents: 18053
diff changeset
    12
  ("nominal_permeq.ML")
22762
f28f62754644 tuned the setup of fresh_fun
urbanc
parents: 22732
diff changeset
    13
  ("nominal_fresh_fun.ML")
21541
ea881fbe0489 Implemented new "nominal_primrec" command for defining
berghofe
parents: 21405
diff changeset
    14
  ("nominal_primrec.ML")
22312
90694c1fa714 Added new file nominal_inductive.ML
berghofe
parents: 22245
diff changeset
    15
  ("nominal_inductive.ML")
28652
659d64d59f16 Added nominal_inductive2.ML
berghofe
parents: 28371
diff changeset
    16
  ("nominal_inductive2.ML")
44689
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
    17
begin
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    18
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    19
section {* Permutations *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    20
(*======================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    21
41798
c3aa3c87ef21 modernized specifications;
wenzelm
parents: 41562
diff changeset
    22
type_synonym 
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    23
  'x prm = "('x \<times> 'x) list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    24
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
    25
(* polymorphic constants for permutation and swapping *)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    26
consts 
18491
1ce410ff9941 Tuned syntax for perm.
berghofe
parents: 18431
diff changeset
    27
  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     (infixr "\<bullet>" 80)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    28
  swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
    29
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    30
(* a "private" copy of the option type used in the abstraction function *)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    31
datatype 'a noption = nSome 'a | nNone
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    32
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    33
(* a "private" copy of the product type used in the nominal induct method *)
44689
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
    34
datatype ('a, 'b) nprod = nPair 'a 'b
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    35
24544
da7de38392df trivial cleaning up
urbanc
parents: 23755
diff changeset
    36
(* an auxiliary constant for the decision procedure involving *) 
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    37
(* permutations (to avoid loops when using perm-compositions)  *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
    38
definition
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    39
  "perm_aux pi x = pi\<bullet>x"
19477
a95176d0f0dd isar-keywords.el
urbanc
parents: 19329
diff changeset
    40
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
    41
(* overloaded permutation operations *)
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    42
overloading
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    43
  perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    44
  perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
45961
5cefe17916a6 treatment of type constructor `set`
haftmann
parents: 45694
diff changeset
    45
  perm_set    \<equiv> "perm :: 'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set"           (unchecked)
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    46
  perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
44689
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
    47
  perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"    (unchecked)
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    48
  perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    49
  perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    50
  perm_char   \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char"           (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    51
  perm_nat    \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat"             (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    52
  perm_int    \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int"             (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    53
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    54
  perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"   (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    55
  perm_nprod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    56
begin
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    57
44838
haftmann
parents: 44835
diff changeset
    58
definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
44833
haftmann
parents: 44696
diff changeset
    59
  "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))"
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    60
44689
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
    61
definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
44833
haftmann
parents: 44696
diff changeset
    62
  "perm_bool pi b = b"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    63
45961
5cefe17916a6 treatment of type constructor `set`
haftmann
parents: 45694
diff changeset
    64
definition perm_set :: "'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" where
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
    65
  "perm_set pi X = {pi \<bullet> x | x. x \<in> X}"
45961
5cefe17916a6 treatment of type constructor `set`
haftmann
parents: 45694
diff changeset
    66
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    67
primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    68
  "perm_unit pi () = ()"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    69
  
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    70
primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where
44833
haftmann
parents: 44696
diff changeset
    71
  "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    72
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    73
primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    74
  nil_eqvt:  "perm_list pi []     = []"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    75
| cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    76
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    77
primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    78
  some_eqvt:  "perm_option pi (Some x) = Some (pi\<bullet>x)"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    79
| none_eqvt:  "perm_option pi None     = None"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    80
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    81
definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where
44833
haftmann
parents: 44696
diff changeset
    82
  "perm_char pi c = c"
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    83
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    84
definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where
44833
haftmann
parents: 44696
diff changeset
    85
  "perm_nat pi i = i"
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    86
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    87
definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where
44833
haftmann
parents: 44696
diff changeset
    88
  "perm_int pi i = i"
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    89
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    90
primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    91
  nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pi\<bullet>x)"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    92
| nnone_eqvt:  "perm_noption pi nNone     = nNone"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    93
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    94
primrec perm_nprod :: "'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" where
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    95
  "perm_nprod pi (nPair x y) = nPair (pi\<bullet>x) (pi\<bullet>y)"
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
    96
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    97
end
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    98
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
    99
(* permutations on booleans *)
44689
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   100
lemmas perm_bool = perm_bool_def
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   101
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   102
lemma true_eqvt [simp]:
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   103
  "pi \<bullet> True \<longleftrightarrow> True"
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   104
  by (simp add: perm_bool_def)
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   105
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   106
lemma false_eqvt [simp]:
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   107
  "pi \<bullet> False \<longleftrightarrow> False"
f247fc952f31 tuned specifications
haftmann
parents: 44683
diff changeset
   108
  by (simp add: perm_bool_def)
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   109
19972
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   110
lemma perm_boolI:
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   111
  assumes a: "P"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   112
  shows "pi\<bullet>P"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   113
  using a by (simp add: perm_bool)
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   114
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   115
lemma perm_boolE:
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   116
  assumes a: "pi\<bullet>P"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   117
  shows "P"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   118
  using a by (simp add: perm_bool)
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
   119
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
   120
lemma if_eqvt:
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   121
  fixes pi::"'a prm"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   122
  shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   123
  by (simp add: perm_fun_def)
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   124
22514
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   125
lemma imp_eqvt:
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   126
  shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))"
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   127
  by (simp add: perm_bool)
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   128
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   129
lemma conj_eqvt:
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   130
  shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))"
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   131
  by (simp add: perm_bool)
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   132
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   133
lemma disj_eqvt:
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   134
  shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))"
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   135
  by (simp add: perm_bool)
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   136
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   137
lemma neg_eqvt:
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   138
  shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   139
  by (simp add: perm_bool)
4dfa84906915 moving lemmas into appropriate sections
urbanc
parents: 22511
diff changeset
   140
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   141
(* permutation on sets *)
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   142
lemma empty_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   143
  shows "pi\<bullet>{} = {}"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   144
  by (simp add: perm_set_def)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   145
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   146
lemma union_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   147
  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   148
  by (auto simp add: perm_set_def)
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   149
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   150
lemma insert_eqvt:
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   151
  shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   152
  by (auto simp add: perm_set_def)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   153
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   154
(* permutations on products *)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   155
lemma fst_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   156
  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   157
 by (cases x) simp
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   158
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   159
lemma snd_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   160
  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   161
 by (cases x) simp
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   162
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   163
(* permutation on lists *)
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   164
lemma append_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   165
  fixes pi :: "'x prm"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   166
  and   l1 :: "'a list"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   167
  and   l2 :: "'a list"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   168
  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   169
  by (induct l1) auto
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   170
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   171
lemma rev_eqvt:
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   172
  fixes pi :: "'x prm"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   173
  and   l  :: "'a list"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   174
  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   175
  by (induct l) (simp_all add: append_eqvt)
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   176
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   177
lemma set_eqvt:
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   178
  fixes pi :: "'x prm"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   179
  and   xs :: "'a list"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   180
  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   181
by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
   182
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   183
(* permutation on characters and strings *)
23050
722f58379538 added lemma for permutations on strings
urbanc
parents: 22846
diff changeset
   184
lemma perm_string:
722f58379538 added lemma for permutations on strings
urbanc
parents: 22846
diff changeset
   185
  fixes s::"string"
722f58379538 added lemma for permutations on strings
urbanc
parents: 22846
diff changeset
   186
  shows "pi\<bullet>s = s"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   187
  by (induct s)(auto simp add: perm_char_def)
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   188
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   189
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   190
section {* permutation equality *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   191
(*==============================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   192
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   193
definition prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool" (" _ \<triangleq> _ " [80,80] 80) where
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
   194
  "pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   195
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   196
section {* Support, Freshness and Supports*}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   197
(*========================================*)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   198
definition supp :: "'a \<Rightarrow> ('x set)" where  
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
   199
   "supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   200
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   201
definition fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [80,80] 80) where
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
   202
   "a \<sharp> x \<longleftrightarrow> a \<notin> supp x"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   203
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   204
definition supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "supports" 80) where
44683
daeb538c57bf tuned specifications and proofs
haftmann
parents: 44567
diff changeset
   205
   "S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   206
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   207
(* lemmas about supp *)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   208
lemma supp_fresh_iff: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   209
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   210
  shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   211
  by (simp add: fresh_def)
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   212
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   213
lemma supp_unit:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   214
  shows "supp () = {}"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   215
  by (simp add: supp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   216
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   217
lemma supp_set_empty:
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   218
  shows "supp {} = {}"
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
   219
  by (force simp add: supp_def empty_eqvt)
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   220
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   221
lemma supp_prod: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   222
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   223
  and   y :: "'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   224
  shows "(supp (x,y)) = (supp x)\<union>(supp y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   225
  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   226
18600
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   227
lemma supp_nprod: 
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   228
  fixes x :: "'a"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   229
  and   y :: "'b"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   230
  shows "(supp (nPair x y)) = (supp x)\<union>(supp y)"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   231
  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   232
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   233
lemma supp_list_nil:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   234
  shows "supp [] = {}"
44696
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
   235
  by (simp add: supp_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   236
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   237
lemma supp_list_cons:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   238
  fixes x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   239
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   240
  shows "supp (x#xs) = (supp x)\<union>(supp xs)"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   241
  by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   242
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   243
lemma supp_list_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   244
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   245
  and   ys :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   246
  shows "supp (xs@ys) = (supp xs)\<union>(supp ys)"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   247
  by (induct xs) (auto simp add: supp_list_nil supp_list_cons)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   248
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   249
lemma supp_list_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   250
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   251
  shows "supp (rev xs) = (supp xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   252
  by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   253
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   254
lemma supp_bool:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   255
  fixes x  :: "bool"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   256
  shows "supp x = {}"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   257
  by (cases "x") (simp_all add: supp_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   258
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   259
lemma supp_some:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   260
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   261
  shows "supp (Some x) = (supp x)"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   262
  by (simp add: supp_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   263
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   264
lemma supp_none:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   265
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   266
  shows "supp (None) = {}"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   267
  by (simp add: supp_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   268
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   269
lemma supp_int:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   270
  fixes i::"int"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   271
  shows "supp (i) = {}"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   272
  by (simp add: supp_def perm_int_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   273
20388
b5a61270ea5a added missing supp_nat lemma
urbanc
parents: 19986
diff changeset
   274
lemma supp_nat:
b5a61270ea5a added missing supp_nat lemma
urbanc
parents: 19986
diff changeset
   275
  fixes n::"nat"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   276
  shows "(supp n) = {}"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   277
  by (simp add: supp_def perm_nat_def)
20388
b5a61270ea5a added missing supp_nat lemma
urbanc
parents: 19986
diff changeset
   278
18627
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   279
lemma supp_char:
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   280
  fixes c::"char"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   281
  shows "(supp c) = {}"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   282
  by (simp add: supp_def perm_char_def)
18627
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   283
  
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   284
lemma supp_string:
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   285
  fixes s::"string"
30983
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   286
  shows "(supp s) = {}"
e54777ab68bd adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
Christian Urban <urbanc@in.tum.de>
parents: 30242
diff changeset
   287
  by (simp add: supp_def perm_string)
18627
f0acb66858b4 added the lemmas supp_char and supp_string
urbanc
parents: 18600
diff changeset
   288
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   289
(* lemmas about freshness *)
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   290
lemma fresh_set_empty:
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   291
  shows "a\<sharp>{}"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   292
  by (simp add: fresh_def supp_set_empty)
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   293
19858
d319e39a2e0e added lemma fresh_unit to Nominal.thy
urbanc
parents: 19856
diff changeset
   294
lemma fresh_unit:
d319e39a2e0e added lemma fresh_unit to Nominal.thy
urbanc
parents: 19856
diff changeset
   295
  shows "a\<sharp>()"
d319e39a2e0e added lemma fresh_unit to Nominal.thy
urbanc
parents: 19856
diff changeset
   296
  by (simp add: fresh_def supp_unit)
d319e39a2e0e added lemma fresh_unit to Nominal.thy
urbanc
parents: 19856
diff changeset
   297
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   298
lemma fresh_prod:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   299
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   300
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   301
  and   y :: "'b"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   302
  shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   303
  by (simp add: fresh_def supp_prod)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   304
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   305
lemma fresh_list_nil:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   306
  fixes a :: "'x"
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
   307
  shows "a\<sharp>[]"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   308
  by (simp add: fresh_def supp_list_nil) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   309
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   310
lemma fresh_list_cons:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   311
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   312
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   313
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   314
  shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   315
  by (simp add: fresh_def supp_list_cons)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   316
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   317
lemma fresh_list_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   318
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   319
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   320
  and   ys :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   321
  shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   322
  by (simp add: fresh_def supp_list_append)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   323
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   324
lemma fresh_list_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   325
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   326
  and   xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   327
  shows "a\<sharp>(rev xs) = a\<sharp>xs"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   328
  by (simp add: fresh_def supp_list_rev)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   329
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   330
lemma fresh_none:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   331
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   332
  shows "a\<sharp>None"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   333
  by (simp add: fresh_def supp_none)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   334
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   335
lemma fresh_some:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   336
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   337
  and   x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   338
  shows "a\<sharp>(Some x) = a\<sharp>x"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   339
  by (simp add: fresh_def supp_some)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   340
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   341
lemma fresh_int:
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   342
  fixes a :: "'x"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   343
  and   i :: "int"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   344
  shows "a\<sharp>i"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   345
  by (simp add: fresh_def supp_int)
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   346
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   347
lemma fresh_nat:
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   348
  fixes a :: "'x"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   349
  and   n :: "nat"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   350
  shows "a\<sharp>n"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   351
  by (simp add: fresh_def supp_nat)
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   352
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   353
lemma fresh_char:
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   354
  fixes a :: "'x"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   355
  and   c :: "char"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   356
  shows "a\<sharp>c"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   357
  by (simp add: fresh_def supp_char)
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   358
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   359
lemma fresh_string:
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   360
  fixes a :: "'x"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   361
  and   s :: "string"
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   362
  shows "a\<sharp>s"
22831
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   363
  by (simp add: fresh_def supp_string)
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   364
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   365
lemma fresh_bool:
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   366
  fixes a :: "'x"
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   367
  and   b :: "bool"
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   368
  shows "a\<sharp>b"
18f4014e1259 tuned some of the proofs and added the lemma fresh_bool
urbanc
parents: 22829
diff changeset
   369
  by (simp add: fresh_def supp_bool)
21010
7fe928722821 added the missing freshness-lemmas for nat, int, char and string and
urbanc
parents: 20809
diff changeset
   370
18294
bbfd64cc91ab fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
wenzelm
parents: 18268
diff changeset
   371
text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   372
lemma fresh_unit_elim: 
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   373
  shows "(a\<sharp>() \<Longrightarrow> PROP C) \<equiv> PROP C"
18294
bbfd64cc91ab fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
wenzelm
parents: 18268
diff changeset
   374
  by (simp add: fresh_def supp_unit)
bbfd64cc91ab fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
wenzelm
parents: 18268
diff changeset
   375
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   376
lemma fresh_prod_elim: 
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   377
  shows "(a\<sharp>(x,y) \<Longrightarrow> PROP C) \<equiv> (a\<sharp>x \<Longrightarrow> a\<sharp>y \<Longrightarrow> PROP C)"
18294
bbfd64cc91ab fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
wenzelm
parents: 18268
diff changeset
   378
  by rule (simp_all add: fresh_prod)
bbfd64cc91ab fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
wenzelm
parents: 18268
diff changeset
   379
21405
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   380
(* this rule needs to be added before the fresh_prodD is *)
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   381
(* added to the simplifier with mksimps                  *) 
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   382
lemma [simp]:
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   383
  shows "a\<sharp>x1 \<Longrightarrow> a\<sharp>x2 \<Longrightarrow> a\<sharp>(x1,x2)"
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   384
  by (simp add: fresh_prod)
26b51f724fe6 added an intro lemma for freshness of products; set up
urbanc
parents: 21377
diff changeset
   385
21318
edb595802d22 added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents: 21010
diff changeset
   386
lemma fresh_prodD:
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   387
  shows "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>x"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   388
  and   "a\<sharp>(x,y) \<Longrightarrow> a\<sharp>y"
21318
edb595802d22 added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents: 21010
diff changeset
   389
  by (simp_all add: fresh_prod)
edb595802d22 added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents: 21010
diff changeset
   390
26342
0f65fa163304 more antiquotations;
wenzelm
parents: 26090
diff changeset
   391
ML {*
0f65fa163304 more antiquotations;
wenzelm
parents: 26090
diff changeset
   392
  val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs;
0f65fa163304 more antiquotations;
wenzelm
parents: 26090
diff changeset
   393
*}
0f65fa163304 more antiquotations;
wenzelm
parents: 26090
diff changeset
   394
declaration {* fn _ =>
45625
750c5a47400b modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 44838
diff changeset
   395
  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
21318
edb595802d22 added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents: 21010
diff changeset
   396
*}
edb595802d22 added fresh_prodD, which is included fresh_prodD into mksimps setup;
wenzelm
parents: 21010
diff changeset
   397
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   398
section {* Abstract Properties for Permutations and  Atoms *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   399
(*=========================================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   400
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   401
(* properties for being a permutation type *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   402
definition
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   403
  "pt TYPE('a) TYPE('x) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   404
     (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   405
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and> 
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   406
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   407
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   408
(* properties for being an atom type *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   409
definition
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   410
  "at TYPE('x) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   411
     (\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and>
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   412
     (\<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
   413
     (\<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
   414
     (infinite (UNIV::'x set))"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   415
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   416
(* property of two atom-types being disjoint *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   417
definition
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   418
  "disjoint TYPE('x) TYPE('y) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   419
       (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   420
       (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   421
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   422
(* composition property of two permutation on a type 'a *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   423
definition
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   424
  "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   425
      (\<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
   426
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   427
(* property of having finite support *)
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 32960
diff changeset
   428
definition
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   429
  "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   430
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   431
section {* Lemmas about the atom-type properties*}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   432
(*==============================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   433
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   434
lemma at1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   435
  fixes x::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   436
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   437
  shows "([]::'x prm)\<bullet>x = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   438
  using a by (simp add: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   439
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   440
lemma at2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   441
  fixes a ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   442
  and   b ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   443
  and   x ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   444
  and   pi::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   445
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   446
  shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   447
  using a by (simp only: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   448
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   449
lemma at3: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   450
  fixes a ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   451
  and   b ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   452
  and   c ::"'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   453
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   454
  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
   455
  using a by (simp only: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   456
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   457
(* rules to calculate simple permutations *)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   458
lemmas at_calc = at2 at1 at3
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   459
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   460
lemma at_swap_simps:
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   461
  fixes a ::"'x"
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   462
  and   b ::"'x"
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   463
  assumes a: "at TYPE('x)"
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   464
  shows "[(a,b)]\<bullet>a = b"
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   465
  and   "[(a,b)]\<bullet>b = a"
27374
2a3c22fd95ab added a lemma to at_swap_simps
urbanc
parents: 27228
diff changeset
   466
  and   "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c"
22610
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   467
  using a by (simp_all add: at_calc)
c8b5133045f3 tuned slightly the previous commit
urbanc
parents: 22609
diff changeset
   468
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   469
lemma at4: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   470
  assumes a: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   471
  shows "infinite (UNIV::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   472
  using a by (simp add: at_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   473
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   474
lemma at_append:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   475
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   476
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   477
  and   c   :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   478
  assumes at: "at TYPE('x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   479
  shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   480
proof (induct pi1)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   481
  case Nil show ?case by (simp add: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   482
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   483
  case (Cons x xs)
18053
2719a6b7d95e some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents: 18048
diff changeset
   484
  have "(xs@pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)" by fact
2719a6b7d95e some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents: 18048
diff changeset
   485
  also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
2719a6b7d95e some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents: 18048
diff changeset
   486
  ultimately show ?case by (cases "x", simp add:  at2[OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   487
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   488
 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   489
lemma at_swap:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   490
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   491
  and   b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   492
  and   c :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   493
  assumes at: "at TYPE('x)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   494
  shows "swap (a,b) (swap (a,b) c) = c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   495
  by (auto simp add: at3[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   496
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   497
lemma at_rev_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   498
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   499
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   500
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   501
  shows "(rev pi)\<bullet>(pi\<bullet>c) = c"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   502
proof(induct pi)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   503
  case Nil show ?case by (simp add: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   504
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   505
  case (Cons x xs) thus ?case 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   506
    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
   507
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   508
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   509
lemma at_pi_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   510
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   511
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   512
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   513
  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   514
  by (rule at_rev_pi[OF at, of "rev pi" _,simplified])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   515
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   516
lemma at_bij1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   517
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   518
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   519
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   520
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   521
  and     a:  "(pi\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   522
  shows   "x=(rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   523
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   524
  from a have "y=(pi\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   525
  thus ?thesis by (simp only: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   526
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   527
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   528
lemma at_bij2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   529
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   530
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   531
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   532
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   533
  and     a:  "((rev pi)\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   534
  shows   "x=pi\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   535
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   536
  from a have "y=((rev pi)\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   537
  thus ?thesis by (simp only: at_pi_rev[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   538
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   539
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   540
lemma at_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   541
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   542
  and   x  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   543
  and   y  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   544
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   545
  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   546
proof 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   547
  assume "pi\<bullet>x = pi\<bullet>y" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   548
  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   549
  thus "x=y" by (simp only: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   550
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   551
  assume "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   552
  thus "pi\<bullet>x = pi\<bullet>y" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   553
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   554
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   555
lemma at_supp:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   556
  fixes x :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   557
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   558
  shows "supp x = {x}"
29903
2c0046b26f80 more finiteness changes
nipkow
parents: 29128
diff changeset
   559
by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   560
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   561
lemma at_fresh:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   562
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   563
  and   b :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   564
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   565
  shows "(a\<sharp>b) = (a\<noteq>b)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   566
  by (simp add: at_supp[OF at] fresh_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   567
26766
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   568
lemma at_prm_fresh1:
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   569
  fixes c :: "'x"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   570
  and   pi:: "'x prm"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   571
  assumes at: "at TYPE('x)"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   572
  and     a: "c\<sharp>pi" 
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   573
  shows "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   574
using a by (induct pi) (auto simp add: fresh_list_cons fresh_prod at_fresh[OF at])
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   575
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   576
lemma at_prm_fresh2:
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   577
  fixes c :: "'x"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   578
  and   pi:: "'x prm"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   579
  assumes at: "at TYPE('x)"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   580
  and     a: "\<forall>(a,b)\<in>set pi. c\<noteq>a \<and> c\<noteq>b" 
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   581
  shows "pi\<bullet>c = c"
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   582
using a  by(induct pi) (auto simp add: at1[OF at] at2[OF at] at3[OF at])
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   583
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   584
lemma at_prm_fresh:
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   585
  fixes c :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   586
  and   pi:: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   587
  assumes at: "at TYPE('x)"
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   588
  and     a: "c\<sharp>pi" 
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   589
  shows "pi\<bullet>c = c"
26766
0e2a29a1065c polished the proof for atm_prm_fresh and more lemmas for fresh_star
urbanc
parents: 26522
diff changeset
   590
by (rule at_prm_fresh2[OF at], rule at_prm_fresh1[OF at, OF a])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   591
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   592
lemma at_prm_rev_eq:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   593
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   594
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   595
  assumes at: "at TYPE('x)"
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   596
  shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   597
proof (simp add: prm_eq_def, auto)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   598
  fix x
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   599
  assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   600
  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
   601
  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
   602
  hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   603
  thus "pi1\<bullet>x  =  pi2\<bullet>x" by simp
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   604
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   605
  fix x
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   606
  assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   607
  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
   608
  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
   609
  hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   610
  thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   611
qed
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   612
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   613
lemma at_prm_eq_append:
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   614
  fixes pi1 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   615
  and   pi2 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   616
  and   pi3 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   617
  assumes at: "at TYPE('x)"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   618
  and     a: "pi1 \<triangleq> pi2"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   619
  shows "(pi3@pi1) \<triangleq> (pi3@pi2)"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   620
using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at])
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   621
19325
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   622
lemma at_prm_eq_append':
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   623
  fixes pi1 :: "'x prm"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   624
  and   pi2 :: "'x prm"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   625
  and   pi3 :: "'x prm"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   626
  assumes at: "at TYPE('x)"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   627
  and     a: "pi1 \<triangleq> pi2"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   628
  shows "(pi1@pi3) \<triangleq> (pi2@pi3)"
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   629
using a by (simp add: prm_eq_def at_append[OF at])
35177b864f80 tuned some proofs
urbanc
parents: 19216
diff changeset
   630
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   631
lemma at_prm_eq_trans:
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   632
  fixes pi1 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   633
  and   pi2 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   634
  and   pi3 :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   635
  assumes a1: "pi1 \<triangleq> pi2"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   636
  and     a2: "pi2 \<triangleq> pi3"  
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   637
  shows "pi1 \<triangleq> pi3"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   638
using a1 a2 by (auto simp add: prm_eq_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   639
  
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   640
lemma at_prm_eq_refl:
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   641
  fixes pi :: "'x prm"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   642
  shows "pi \<triangleq> pi"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   643
by (simp add: prm_eq_def)
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   644
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   645
lemma at_prm_rev_eq1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   646
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   647
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   648
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   649
  shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1) \<triangleq> (rev pi2)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   650
  by (simp add: at_prm_rev_eq[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   651
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   652
lemma at_ds1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   653
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   654
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   655
  shows "[(a,a)] \<triangleq> []"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   656
  by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   657
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   658
lemma at_ds2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   659
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   660
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   661
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   662
  assumes at: "at TYPE('x)"
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   663
  shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   664
  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
   665
      at_rev_pi[OF at] at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   666
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   667
lemma at_ds3: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   668
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   669
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   670
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   671
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   672
  and     a:  "distinct [a,b,c]"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   673
  shows "[(a,c),(b,c),(a,c)] \<triangleq> [(a,b)]"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   674
  using a by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   675
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   676
lemma at_ds4: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   677
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   678
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   679
  and   pi  :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   680
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   681
  shows "(pi@[(a,(rev pi)\<bullet>b)]) \<triangleq> ([(pi\<bullet>a,b)]@pi)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   682
  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
   683
      at_pi_rev[OF at] at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   684
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   685
lemma at_ds5: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   686
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   687
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   688
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   689
  shows "[(a,b)] \<triangleq> [(b,a)]"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   690
  by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   691
19164
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   692
lemma at_ds5': 
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   693
  fixes a  :: "'x"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   694
  and   b  :: "'x"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   695
  assumes at: "at TYPE('x)"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   696
  shows "[(a,b),(b,a)] \<triangleq> []"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   697
  by (force simp add: prm_eq_def at_calc[OF at])
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
   698
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   699
lemma at_ds6: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   700
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   701
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   702
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   703
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   704
  and     a: "distinct [a,b,c]"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   705
  shows "[(a,c),(a,b)] \<triangleq> [(b,c),(a,c)]"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   706
  using a by (force simp add: prm_eq_def at_calc[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   707
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   708
lemma at_ds7:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   709
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   710
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   711
  shows "((rev pi)@pi) \<triangleq> []"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   712
  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
   713
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   714
lemma at_ds8_aux:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   715
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   716
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   717
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   718
  and   c  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   719
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   720
  shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   721
  by (force simp add: at_calc[OF at] at_bij[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   722
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   723
lemma at_ds8: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   724
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   725
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   726
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   727
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   728
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   729
  shows "(pi1@pi2) \<triangleq> ((pi1\<bullet>pi2)@pi1)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   730
apply(induct_tac pi2)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   731
apply(simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   732
apply(auto simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   733
apply(simp add: at2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   734
apply(drule_tac x="aa" in spec)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   735
apply(drule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   736
apply(simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   737
apply(simp add: at_append[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   738
apply(simp add: at2[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   739
apply(simp add: at_ds8_aux[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   740
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   741
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   742
lemma at_ds9: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   743
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   744
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   745
  and   a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   746
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   747
  assumes at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   748
  shows " ((rev pi2)@(rev pi1)) \<triangleq> ((rev pi1)@(rev (pi1\<bullet>pi2)))"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   749
apply(induct_tac pi2)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   750
apply(simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   751
apply(auto simp add: prm_eq_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   752
apply(simp add: at_append[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   753
apply(simp add: at2[OF at] at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   754
apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   755
apply(drule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   756
apply(simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   757
apply(simp add: at_ds8_aux[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   758
apply(simp add: at_rev_pi[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   759
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   760
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   761
lemma at_ds10:
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   762
  fixes pi :: "'x prm"
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   763
  and   a  :: "'x"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   764
  and   b  :: "'x"
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   765
  assumes at: "at TYPE('x)"
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   766
  and     a:  "b\<sharp>(rev pi)"
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   767
  shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])"
19107
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   768
using a
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   769
apply -
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   770
apply(rule at_prm_eq_trans)
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   771
apply(rule at_ds2[OF at])
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   772
apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   773
apply(rule at_prm_eq_refl)
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   774
done
b16a45c53884 added a few lemmas to do with permutation-equivalence for the
urbanc
parents: 19045
diff changeset
   775
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   776
--"there always exists an atom that is not being in a finite set"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   777
lemma ex_in_inf:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   778
  fixes   A::"'x set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   779
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   780
  and     fs: "finite A"
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   781
  obtains c::"'x" where "c\<notin>A"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   782
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   783
  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   784
    by (simp add: Diff_infinite_finite)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   785
  hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   786
  then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   787
  then have "c\<notin>A" by simp
41550
efa734d9b221 eliminated global prems;
wenzelm
parents: 41413
diff changeset
   788
  then show ?thesis ..
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   789
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   790
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   791
text {* there always exists a fresh name for an object with finite support *}
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   792
lemma at_exists_fresh': 
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   793
  fixes  x :: "'a"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   794
  assumes at: "at TYPE('x)"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   795
  and     fs: "finite ((supp x)::'x set)"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   796
  shows "\<exists>c::'x. c\<sharp>x"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   797
  by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs])
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   798
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   799
lemma at_exists_fresh: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   800
  fixes  x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   801
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   802
  and     fs: "finite ((supp x)::'x set)"
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   803
  obtains c::"'x" where  "c\<sharp>x"
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   804
  by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   805
21377
c29146dc14f1 replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents: 21318
diff changeset
   806
lemma at_finite_select: 
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   807
  fixes S::"'a set"
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   808
  assumes a: "at TYPE('a)"
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   809
  and     b: "finite S" 
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   810
  shows "\<exists>x. x \<notin> S" 
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   811
  using a b
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   812
  apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   813
  apply(simp add: at_def)
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   814
  apply(subgoal_tac "UNIV - S \<noteq> {}")
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   815
  apply(simp only: ex_in_conv [symmetric])
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   816
  apply(blast)
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   817
  apply(rule notI)
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
   818
  apply(simp)
18657
0a37df3bb99d Added theorem at_finite_select.
berghofe
parents: 18656
diff changeset
   819
  done
0a37df3bb99d Added theorem at_finite_select.
berghofe
parents: 18656
diff changeset
   820
19140
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   821
lemma at_different:
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   822
  assumes at: "at TYPE('x)"
19140
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   823
  shows "\<exists>(b::'x). a\<noteq>b"
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   824
proof -
19140
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   825
  have "infinite (UNIV::'x set)" by (rule at4[OF at])
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   826
  hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   827
  have "(UNIV-{a}) \<noteq> ({}::'x set)" 
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   828
  proof (rule_tac ccontr, drule_tac notnotD)
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   829
    assume "UNIV-{a} = ({}::'x set)"
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   830
    with inf2 have "infinite ({}::'x set)" by simp
19869
eba1b9e7c458 removal of the obsolete "infinite_nonempty"
paulson
parents: 19858
diff changeset
   831
    then show "False" by auto
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   832
  qed
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   833
  hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   834
  then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast
19140
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   835
  from mem2 have "a\<noteq>b" by blast
5a98cdf99079 replaced the lemma at_two by at_different;
urbanc
parents: 19132
diff changeset
   836
  then show "\<exists>(b::'x). a\<noteq>b" by blast
19132
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   837
qed
ff41946e5092 added lemmas
urbanc
parents: 19107
diff changeset
   838
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   839
--"the at-props imply the pt-props"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   840
lemma at_pt_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   841
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   842
  shows "pt TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   843
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   844
apply(simp only: at1[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   845
apply(simp only: at_append[OF at]) 
18053
2719a6b7d95e some minor tweaks in some proofs (nothing extraordinary)
urbanc
parents: 18048
diff changeset
   846
apply(simp only: prm_eq_def)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   847
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   848
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   849
section {* finite support properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   850
(*===================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   851
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   852
lemma fs1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   853
  fixes x :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   854
  assumes a: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   855
  shows "finite ((supp x)::'x set)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   856
  using a by (simp add: fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   857
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   858
lemma fs_at_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   859
  fixes a :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   860
  assumes at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   861
  shows "fs TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   862
apply(simp add: fs_def) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   863
apply(simp add: at_supp[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   864
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   865
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   866
lemma fs_unit_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   867
  shows "fs TYPE(unit) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   868
apply(simp add: fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   869
apply(simp add: supp_unit)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   870
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   871
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   872
lemma fs_prod_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   873
  assumes fsa: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   874
  and     fsb: "fs TYPE('b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   875
  shows "fs TYPE('a\<times>'b) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   876
apply(unfold fs_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   877
apply(auto simp add: supp_prod)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   878
apply(rule fs1[OF fsa])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   879
apply(rule fs1[OF fsb])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   880
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   881
18600
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   882
lemma fs_nprod_inst:
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   883
  assumes fsa: "fs TYPE('a) TYPE('x)"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   884
  and     fsb: "fs TYPE('b) TYPE('x)"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   885
  shows "fs TYPE(('a,'b) nprod) TYPE('x)"
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   886
apply(unfold fs_def, rule allI)
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   887
apply(case_tac x)
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   888
apply(auto simp add: supp_nprod)
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   889
apply(rule fs1[OF fsa])
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   890
apply(rule fs1[OF fsb])
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   891
done
20ad06db427b added private datatype nprod (copy of prod) to be
urbanc
parents: 18579
diff changeset
   892
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   893
lemma fs_list_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   894
  assumes fs: "fs TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   895
  shows "fs TYPE('a list) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   896
apply(simp add: fs_def, rule allI)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   897
apply(induct_tac x)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   898
apply(simp add: supp_list_nil)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   899
apply(simp add: supp_list_cons)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   900
apply(rule fs1[OF fs])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   901
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   902
18431
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   903
lemma fs_option_inst:
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   904
  assumes fs: "fs TYPE('a) TYPE('x)"
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   905
  shows "fs TYPE('a option) TYPE('x)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   906
apply(simp add: fs_def, rule allI)
18431
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   907
apply(case_tac x)
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   908
apply(simp add: supp_none)
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   909
apply(simp add: supp_some)
a59c79a3544c improved the finite-support proof
urbanc
parents: 18351
diff changeset
   910
apply(rule fs1[OF fs])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   911
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   912
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   913
section {* Lemmas about the permutation properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   914
(*=================================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   915
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   916
lemma pt1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   917
  fixes x::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   918
  assumes a: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   919
  shows "([]::'x prm)\<bullet>x = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   920
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   921
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   922
lemma pt2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   923
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   924
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   925
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   926
  assumes a: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   927
  shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   928
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   929
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   930
lemma pt3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   931
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   932
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   933
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   934
  assumes a: "pt TYPE('a) TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   935
  shows "pi1 \<triangleq> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>x"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   936
  using a by (simp add: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   937
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   938
lemma pt3_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   939
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   940
  and   pi2::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   941
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   942
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   943
  and     at: "at TYPE('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
   944
  shows "pi1 \<triangleq> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   945
  by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   946
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   947
section {* composition properties *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   948
(* ============================== *)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   949
lemma cp1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   950
  fixes pi1::"'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   951
  and   pi2::"'y prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   952
  and   x  ::"'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   953
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   954
  shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   955
  using cp by (simp add: cp_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   956
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   957
lemma cp_pt_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   958
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   959
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   960
  shows "cp TYPE('a) TYPE('x) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   961
apply(auto simp add: cp_def pt2[OF pt,symmetric])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   962
apply(rule pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   963
apply(rule at_ds8[OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   964
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
   965
19638
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   966
section {* disjointness properties *}
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   967
(*=================================*)
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   968
lemma dj_perm_forget:
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   969
  fixes pi::"'y prm"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   970
  and   x ::"'x"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   971
  assumes dj: "disjoint TYPE('x) TYPE('y)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   972
  shows "pi\<bullet>x=x" 
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   973
  using dj by (simp_all add: disjoint_def)
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   974
28371
471a356fdea9 Added some more lemmas that are useful in proof of strong induction rule.
berghofe
parents: 28322
diff changeset
   975
lemma dj_perm_set_forget:
471a356fdea9 Added some more lemmas that are useful in proof of strong induction rule.
berghofe
parents: 28322
diff changeset
   976
  fixes pi::"'y prm"
471a356fdea9 Added some more lemmas that are useful in proof of strong induction rule.
berghofe
parents: 28322
diff changeset
   977
  and   x ::"'x set"
471a356fdea9 Added some more lemmas that are useful in proof of strong induction rule.
berghofe
parents: 28322
diff changeset
   978
  assumes dj: "disjoint TYPE('x) TYPE('y)"
44833
haftmann
parents: 44696
diff changeset
   979
  shows "pi\<bullet>x=x" 
45961
5cefe17916a6 treatment of type constructor `set`
haftmann
parents: 45694
diff changeset
   980
  using dj by (simp_all add: perm_set_def disjoint_def)
28371
471a356fdea9 Added some more lemmas that are useful in proof of strong induction rule.
berghofe
parents: 28322
diff changeset
   981
19638
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   982
lemma dj_perm_perm_forget:
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   983
  fixes pi1::"'x prm"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   984
  and   pi2::"'y prm"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   985
  assumes dj: "disjoint TYPE('x) TYPE('y)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   986
  shows "pi2\<bullet>pi1=pi1"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   987
  using dj by (induct pi1, auto simp add: disjoint_def)
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   988
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   989
lemma dj_cp:
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   990
  fixes pi1::"'x prm"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   991
  and   pi2::"'y prm"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   992
  and   x  ::"'a"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   993
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   994
  and     dj: "disjoint TYPE('y) TYPE('x)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   995
  shows "pi1\<bullet>(pi2\<bullet>x) = (pi2)\<bullet>(pi1\<bullet>x)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   996
  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   997
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   998
lemma dj_supp:
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
   999
  fixes a::"'x"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
  1000
  assumes dj: "disjoint TYPE('x) TYPE('y)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
  1001
  shows "(supp a) = ({}::'y set)"
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
  1002
apply(simp add: supp_def dj_perm_forget[OF dj])
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
  1003
done
4358b88a9d12 added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
urbanc
parents: 19634
diff changeset
  1004
19972
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1005
lemma at_fresh_ineq:
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1006
  fixes a :: "'x"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1007
  and   b :: "'y"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1008
  assumes dj: "disjoint TYPE('y) TYPE('x)"
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1009
  shows "a\<sharp>b" 
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1010
  by (simp add: fresh_def dj_supp[OF dj])
89c5afe4139a added more infrastructure for the recursion combinator
urbanc
parents: 19869
diff changeset
  1011
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1012
section {* permutation type instances *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1013
(* ===================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1014
44696
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1015
lemma pt_fun_inst:
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1016
  assumes pta: "pt TYPE('a) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1017
  and     ptb: "pt TYPE('b) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1018
  and     at:  "at TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1019
  shows  "pt TYPE('a\<Rightarrow>'b) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1020
apply(auto simp only: pt_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1021
apply(simp_all add: perm_fun_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1022
apply(simp add: pt1[OF pta] pt1[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1023
apply(simp add: pt2[OF pta] pt2[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1024
apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1025
apply(simp add: pt3[OF pta] pt3[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1026
(*A*)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1027
apply(simp add: at_prm_rev_eq[OF at])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1028
done
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1029
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1030
lemma pt_bool_inst:
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1031
  shows  "pt TYPE(bool) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1032
  by (simp add: pt_def perm_bool_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1033
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1034
lemma pt_set_inst:
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1035
  assumes pt: "pt TYPE('a) TYPE('x)"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1036
  shows  "pt TYPE('a set) TYPE('x)"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1037
apply(simp add: pt_def)
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1038
apply(simp_all add: perm_set_def)
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1039
apply(simp add: pt1[OF pt])
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1040
apply(force simp add: pt2[OF pt] pt3[OF pt])
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1041
done
44696
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1042
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1043
lemma pt_unit_inst:
44833
haftmann
parents: 44696
diff changeset
  1044
  shows "pt TYPE(unit) TYPE('x)"
44696
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1045
  by (simp add: pt_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1046
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1047
lemma pt_prod_inst:
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1048
  assumes pta: "pt TYPE('a) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1049
  and     ptb: "pt TYPE('b) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1050
  shows  "pt TYPE('a \<times> 'b) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1051
  apply(auto simp add: pt_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1052
  apply(rule pt1[OF pta])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1053
  apply(rule pt1[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1054
  apply(rule pt2[OF pta])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1055
  apply(rule pt2[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1056
  apply(rule pt3[OF pta],assumption)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1057
  apply(rule pt3[OF ptb],assumption)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1058
  done
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1059
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1060
lemma pt_list_nil: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1061
  fixes xs :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1062
  assumes pt: "pt TYPE('a) TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1063
  shows "([]::'x prm)\<bullet>xs = xs" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1064
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1065
apply(simp_all add: pt1[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1066
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1067
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1068
lemma pt_list_append: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1069
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1070
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1071
  and   xs  :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1072
  assumes pt: "pt TYPE('a) TYPE ('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1073
  shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1074
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1075
apply(simp_all add: pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1076
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1077
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1078
lemma pt_list_prm_eq: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1079
  fixes pi1 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1080
  and   pi2 :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1081
  and   xs  :: "'a list"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1082
  assumes pt: "pt TYPE('a) TYPE ('x)"
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
  1083
  shows "pi1 \<triangleq> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>xs"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1084
apply(induct_tac xs)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1085
apply(simp_all add: prm_eq_def pt3[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1086
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1087
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1088
lemma pt_list_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1089
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1090
  shows  "pt TYPE('a list) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1091
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1092
apply(rule pt_list_nil[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1093
apply(rule pt_list_append[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1094
apply(rule pt_list_prm_eq[OF pt],assumption)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1095
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1096
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1097
lemma pt_option_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1098
  assumes pta: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1099
  shows  "pt TYPE('a option) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1100
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1101
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1102
apply(simp_all add: pt1[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1103
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1104
apply(simp_all add: pt2[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1105
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1106
apply(simp_all add: pt3[OF pta])
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_noption_inst:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1110
  assumes pta: "pt TYPE('a) TYPE('x)"
18579
002d371401f5 changed the name of the type "nOption" to "noption".
urbanc
parents: 18578
diff changeset
  1111
  shows  "pt TYPE('a noption) TYPE('x)"
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1112
apply(auto simp only: pt_def)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1113
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1114
apply(simp_all add: pt1[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1115
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1116
apply(simp_all add: pt2[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1117
apply(case_tac "x")
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1118
apply(simp_all add: pt3[OF pta])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1119
done
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1120
44696
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1121
lemma pt_nprod_inst:
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1122
  assumes pta: "pt TYPE('a) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1123
  and     ptb: "pt TYPE('b) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1124
  shows  "pt TYPE(('a,'b) nprod) TYPE('x)"
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1125
  apply(auto simp add: pt_def)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1126
  apply(case_tac x)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1127
  apply(simp add: pt1[OF pta] pt1[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1128
  apply(case_tac x)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1129
  apply(simp add: pt2[OF pta] pt2[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1130
  apply(case_tac x)
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1131
  apply(simp add: pt3[OF pta] pt3[OF ptb])
4e99277c81f2 pseudo-definition for perms on sets; tuned
haftmann
parents: 44689
diff changeset
  1132
  done
24544
da7de38392df trivial cleaning up
urbanc
parents: 23755
diff changeset
  1133
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1134
section {* further lemmas for permutation types *}
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1135
(*==============================================*)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1136
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1137
lemma pt_rev_pi:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1138
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1139
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1140
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1141
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1142
  shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1143
proof -
18295
dd50de393330 changed \<sim> of permutation equality to \<triangleq>
urbanc
parents: 18294
diff changeset
  1144
  have "((rev pi)@pi) \<triangleq> ([]::'x prm)" by (simp add: at_ds7[OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1145
  hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1146
  thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1147
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1148
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1149
lemma pt_pi_rev:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1150
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1151
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1152
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1153
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1154
  shows "pi\<bullet>((rev pi)\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1155
  by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1156
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1157
lemma pt_bij1: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1158
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1159
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1160
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1161
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1162
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1163
  and     a:  "(pi\<bullet>x) = y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1164
  shows   "x=(rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1165
proof -
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1166
  from a have "y=(pi\<bullet>x)" by (rule sym)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1167
  thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1168
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1169
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1170
lemma pt_bij2: 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1171
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1172
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1173
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1174
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1175
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1176
  and     a:  "x = (rev pi)\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1177
  shows   "(pi\<bullet>x)=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1178
  using a by (simp add: pt_pi_rev[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1179
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1180
lemma pt_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1181
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1182
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1183
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1184
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1185
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1186
  shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1187
proof 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1188
  assume "pi\<bullet>x = pi\<bullet>y" 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1189
  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1190
  thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1191
next
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1192
  assume "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1193
  thus "pi\<bullet>x = pi\<bullet>y" by simp
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1194
qed
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1195
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1196
lemma pt_eq_eqvt:
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1197
  fixes pi :: "'x prm"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1198
  and   x  :: "'a"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1199
  and   y  :: "'a"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1200
  assumes pt: "pt TYPE('a) TYPE('x)"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1201
  and     at: "at TYPE('x)"
22829
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1202
  shows "pi\<bullet>(x=y) = (pi\<bullet>x = pi\<bullet>y)"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
  1203
  using pt at
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
  1204
  by (auto simp add: pt_bij perm_bool)
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1205
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1206
lemma pt_bij3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1207
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1208
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1209
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1210
  assumes a:  "x=y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1211
  shows "(pi\<bullet>x = pi\<bullet>y)"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
  1212
  using a by simp 
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1213
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1214
lemma pt_bij4:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1215
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1216
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1217
  and   y  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1218
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1219
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1220
  and     a:  "pi\<bullet>x = pi\<bullet>y"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1221
  shows "x = y"
30990
4872eef36167 reorganised the section about fresh_star and added lemma pt_fresh_star_pi
Christian Urban <urbanc@in.tum.de>
parents: 30983
diff changeset
  1222
  using a by (simp add: pt_bij[OF pt, OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1223
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1224
lemma pt_swap_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1225
  fixes a  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1226
  and   b  :: "'x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1227
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1228
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1229
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1230
  shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1231
  by (rule pt_bij2[OF pt, OF at], simp)
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1232
19164
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1233
lemma pt_swap_bij':
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1234
  fixes a  :: "'x"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1235
  and   b  :: "'x"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1236
  and   x  :: "'a"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1237
  assumes pt: "pt TYPE('a) TYPE('x)"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1238
  and     at: "at TYPE('x)"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1239
  shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x"
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1240
apply(simp add: pt2[OF pt,symmetric])
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1241
apply(rule trans)
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1242
apply(rule pt3[OF pt])
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1243
apply(rule at_ds5'[OF at])
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1244
apply(rule pt1[OF pt])
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1245
done
0eccb98b1fdb added initialisation-code for finite_guess
urbanc
parents: 19140
diff changeset
  1246
24571
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1247
lemma pt_swap_bij'':
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1248
  fixes a  :: "'x"
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1249
  and   x  :: "'a"
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1250
  assumes pt: "pt TYPE('a) TYPE('x)"
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1251
  and     at: "at TYPE('x)"
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1252
  shows "[(a,a)]\<bullet>x = x"
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1253
apply(rule trans)
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1254
apply(rule pt3[OF pt])
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1255
apply(rule at_ds1[OF at])
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1256
apply(rule pt1[OF pt])
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1257
done
a6d0428dea8e some cleaning up to do with contexts
urbanc
parents: 24568
diff changeset
  1258
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
  1259
lemma supp_singleton:
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1260
  shows "supp {x} = supp x"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1261
  by (force simp add: supp_def perm_set_def)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
  1262
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
  1263
lemma fresh_singleton:
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1264
  shows "a\<sharp>{x} = a\<sharp>x"
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1265
  by (simp add: fresh_def supp_singleton)
26806
40b411ec05aa Adapted to encoding of sets as predicates
berghofe
parents: 26773
diff changeset
  1266
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1267
lemma pt_set_bij1:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1268
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1269
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1270
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1271
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1272
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1273
  shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1274
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1275
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1276
lemma pt_set_bij1a:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1277
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1278
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1279
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1280
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1281
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1282
  shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1283
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1284
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1285
lemma pt_set_bij:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1286
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1287
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1288
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1289
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1290
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1291
  shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1292
  by (simp add: perm_set_def pt_bij[OF pt, OF at])
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1293
22418
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1294
lemma pt_in_eqvt:
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1295
  fixes pi :: "'x prm"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1296
  and   x  :: "'a"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1297
  and   X  :: "'a set"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1298
  assumes pt: "pt TYPE('a) TYPE('x)"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1299
  and     at: "at TYPE('x)"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1300
  shows "pi\<bullet>(x\<in>X)=((pi\<bullet>x)\<in>(pi\<bullet>X))"
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1301
using assms
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1302
by (auto simp add:  pt_set_bij perm_bool)
49e2d9744ae1 major update of the nominal package; there is now an infrastructure
urbanc
parents: 22326
diff changeset
  1303
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1304
lemma pt_set_bij2:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1305
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1306
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1307
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1308
  assumes pt: "pt TYPE('a) TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1309
  and     at: "at TYPE('x)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1310
  and     a:  "x\<in>X"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1311
  shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1312
  using a by (simp add: pt_set_bij[OF pt, OF at])
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1313
18264
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1314
lemma pt_set_bij2a:
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1315
  fixes pi :: "'x prm"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1316
  and   x  :: "'a"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1317
  and   X  :: "'a set"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1318
  assumes pt: "pt TYPE('a) TYPE('x)"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1319
  and     at: "at TYPE('x)"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1320
  and     a:  "x\<in>((rev pi)\<bullet>X)"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1321
  shows "(pi\<bullet>x)\<in>X"
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1322
  using a by (simp add: pt_set_bij1[OF pt, OF at])
3b808e24667b added the version of nominal.thy that contains
urbanc
parents: 18246
diff changeset
  1323
26773
ba8b1a8a12a7 added more infrastructure for fresh_star
urbanc
parents: 26766
diff changeset
  1324
(* FIXME: is this lemma needed anywhere? *)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1325
lemma pt_set_bij3:
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1326
  fixes pi :: "'x prm"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1327
  and   x  :: "'a"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1328
  and   X  :: "'a set"
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1329
  shows "pi\<bullet>(x\<in>X) = (x\<in>X)"
26773
ba8b1a8a12a7 added more infrastructure for fresh_star
urbanc
parents: 26766
diff changeset
  1330
by (simp add: perm_bool)
17870
c35381811d5c Initial revision.
berghofe
parents:
diff changeset
  1331
18159
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1332
lemma pt_subseteq_eqvt:
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1333
  fixes pi :: "'x prm"
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1334
  and   Y  :: "'a set"
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1335
  and   X  :: "'a set"
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1336
  assumes pt: "pt TYPE('a) TYPE('x)"
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1337
  and     at: "at TYPE('x)"
26090
ec111fa4f8c5 added eqvt-flag to subseteq-lemma
urbanc
parents: 25950
diff changeset
  1338
  shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1339
by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
18159
08282ca0402e added a few equivariance lemmas (they need to be automated
urbanc
parents: 18068
diff changeset
  1340
19772
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1341
lemma pt_set_diff_eqvt:
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1342
  fixes X::"'a set"
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1343
  and   Y::"'a set"
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1344
  and   pi::"'x prm"
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1345
  assumes pt: "pt TYPE('a) TYPE('x)"
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1346
  and     at: "at TYPE('x)"
22829
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1347
  shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1348
  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
19772
45897b49fdd2 added some further lemmas that deal with permutations and set-operators
urbanc
parents: 19771
diff changeset
  1349
22829
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1350
lemma pt_Collect_eqvt:
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1351
  fixes pi::"'x prm"
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1352
  assumes pt: "pt TYPE('a) TYPE('x)"
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1353
  and     at: "at TYPE('x)"
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1354
  shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
46179
47bcf3d5d1f0 Reverted several lemmas involving sets to the state before the
berghofe
parents: 45961
diff changeset
  1355
apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
22829
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808
diff changeset
  1356
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
f1db55c7534d tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents: 22808