author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 48891  c0eafbd55de3 
permissions  rwrr 
19494  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  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  9 
("nominal_atoms.ML") 
31936  10 
("nominal_datatype.ML") 
18264  11 
("nominal_induct.ML") 
18068  12 
("nominal_permeq.ML") 
22762  13 
("nominal_fresh_fun.ML") 
21541
ea881fbe0489
Implemented new "nominal_primrec" command for defining
berghofe
parents:
21405
diff
changeset

14 
("nominal_primrec.ML") 
22312  15 
("nominal_inductive.ML") 
28652  16 
("nominal_inductive2.ML") 
44689  17 
begin 
17870  18 

19 
section {* Permutations *} 

20 
(*======================*) 

21 

41798  22 
type_synonym 
17870  23 
'x prm = "('x \<times> 'x) list" 
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  26 
consts 
18491  27 
perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) 
17870  28 
swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" 
29 

30983
e54777ab68bd
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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  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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

35 

24544  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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

37 
(* permutations (to avoid loops when using permcompositions) *) 
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

38 
definition 
44683  39 
"perm_aux pi x = pi\<bullet>x" 
19477  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 typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

44 
perm_bool \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool" (unchecked) 
45961  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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

46 
perm_unit \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit" (unchecked) 
44689  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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

57 

44838  58 
definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where 
44833  59 
"perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))" 
44683  60 

44689  61 
definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where 
44833  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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

63 

45961  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  66 

44683  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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

69 

44683  70 
primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where 
44833  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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

72 

44683  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 typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

76 

44683  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 typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

80 

44683  81 
definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where 
44833  82 
"perm_char pi c = c" 
44683  83 

84 
definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where 

44833  85 
"perm_nat pi i = i" 
44683  86 

87 
definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where 

44833  88 
"perm_int pi i = i" 
44683  89 

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 typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

93 

44683  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 typeclasses)
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  96 

30983
e54777ab68bd
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with typeclasses)
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

99 
(* permutations on booleans *) 
44689  100 
lemmas perm_bool = perm_bool_def 
101 

102 
lemma true_eqvt [simp]: 

103 
"pi \<bullet> True \<longleftrightarrow> True" 

104 
by (simp add: perm_bool_def) 

105 

106 
lemma false_eqvt [simp]: 

107 
"pi \<bullet> False \<longleftrightarrow> False" 

108 
by (simp add: perm_bool_def) 

18264  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 freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

121 
fixes pi::"'a prm" 
7fe928722821
added the missing freshnesslemmas 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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

123 
by (simp add: perm_fun_def) 
21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

124 

22514  125 
lemma imp_eqvt: 
126 
shows "pi\<bullet>(A\<longrightarrow>B) = ((pi\<bullet>A)\<longrightarrow>(pi\<bullet>B))" 

127 
by (simp add: perm_bool) 

128 

129 
lemma conj_eqvt: 

130 
shows "pi\<bullet>(A\<and>B) = ((pi\<bullet>A)\<and>(pi\<bullet>B))" 

131 
by (simp add: perm_bool) 

132 

133 
lemma disj_eqvt: 

134 
shows "pi\<bullet>(A\<or>B) = ((pi\<bullet>A)\<or>(pi\<bullet>B))" 

135 
by (simp add: perm_bool) 

136 

137 
lemma neg_eqvt: 

138 
shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))" 

139 
by (simp add: perm_bool) 

140 

26806  141 
(* permutation on sets *) 
142 
lemma empty_eqvt: 

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  145 

146 
lemma union_eqvt: 

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  153 

30983
e54777ab68bd
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

154 
(* permutations on products *) 
26806  155 
lemma fst_eqvt: 
156 
"pi\<bullet>(fst x) = fst (pi\<bullet>x)" 

157 
by (cases x) simp 

158 

159 
lemma snd_eqvt: 

160 
"pi\<bullet>(snd x) = snd (pi\<bullet>x)" 

161 
by (cases x) simp 

162 

163 
(* permutation on lists *) 

164 
lemma append_eqvt: 

165 
fixes pi :: "'x prm" 

166 
and l1 :: "'a list" 

167 
and l2 :: "'a list" 

168 
shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)" 

169 
by (induct l1) auto 

170 

171 
lemma rev_eqvt: 

172 
fixes pi :: "'x prm" 

173 
and l :: "'a list" 

174 
shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)" 

175 
by (induct l) (simp_all add: append_eqvt) 

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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

183 
(* permutation on characters and strings *) 
23050  184 
lemma perm_string: 
185 
fixes s::"string" 

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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

188 

17870  189 

190 
section {* permutation equality *} 

191 
(*==============================*) 

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  194 
"pi1 \<triangleq> pi2 \<longleftrightarrow> (\<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a)" 
17870  195 

196 
section {* Support, Freshness and Supports*} 

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  199 
"supp x = {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}" 
17870  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  202 
"a \<sharp> x \<longleftrightarrow> a \<notin> supp x" 
17870  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  205 
"S supports x \<longleftrightarrow> (\<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x))" 
17870  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  208 
lemma supp_fresh_iff: 
209 
fixes x :: "'a" 

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  213 
lemma supp_unit: 
214 
shows "supp () = {}" 

215 
by (simp add: supp_def) 

216 

18264  217 
lemma supp_set_empty: 
218 
shows "supp {} = {}" 

26806  219 
by (force simp add: supp_def empty_eqvt) 
18264  220 

17870  221 
lemma supp_prod: 
222 
fixes x :: "'a" 

223 
and y :: "'b" 

224 
shows "(supp (x,y)) = (supp x)\<union>(supp y)" 

225 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

226 

18600  227 
lemma supp_nprod: 
228 
fixes x :: "'a" 

229 
and y :: "'b" 

230 
shows "(supp (nPair x y)) = (supp x)\<union>(supp y)" 

231 
by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) 

232 

17870  233 
lemma supp_list_nil: 
234 
shows "supp [] = {}" 

44696  235 
by (simp add: supp_def) 
17870  236 

237 
lemma supp_list_cons: 

238 
fixes x :: "'a" 

239 
and xs :: "'a list" 

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  242 

243 
lemma supp_list_append: 

244 
fixes xs :: "'a list" 

245 
and ys :: "'a list" 

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  248 

249 
lemma supp_list_rev: 

250 
fixes xs :: "'a list" 

251 
shows "supp (rev xs) = (supp xs)" 

252 
by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil) 

253 

254 
lemma supp_bool: 

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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

257 
by (cases "x") (simp_all add: supp_def) 
17870  258 

259 
lemma supp_some: 

260 
fixes x :: "'a" 

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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

262 
by (simp add: supp_def) 
17870  263 

264 
lemma supp_none: 

265 
fixes x :: "'a" 

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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

267 
by (simp add: supp_def) 
17870  268 

269 
lemma supp_int: 

270 
fixes i::"int" 

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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

272 
by (simp add: supp_def perm_int_def) 
17870  273 

20388  274 
lemma supp_nat: 
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

277 
by (simp add: supp_def perm_nat_def) 
20388  278 

18627  279 
lemma supp_char: 
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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

282 
by (simp add: supp_def perm_char_def) 
18627  283 

284 
lemma supp_string: 

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 typeclasses)
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 typeclasses)
Christian Urban <urbanc@in.tum.de>
parents:
30242
diff
changeset

287 
by (simp add: supp_def perm_string) 
18627  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  290 
lemma fresh_set_empty: 
291 
shows "a\<sharp>{}" 

292 
by (simp add: fresh_def supp_set_empty) 

293 

19858  294 
lemma fresh_unit: 
295 
shows "a\<sharp>()" 

296 
by (simp add: fresh_def supp_unit) 

297 

17870  298 
lemma fresh_prod: 
299 
fixes a :: "'x" 

300 
and x :: "'a" 

301 
and y :: "'b" 

302 
shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)" 

303 
by (simp add: fresh_def supp_prod) 

304 

305 
lemma fresh_list_nil: 

306 
fixes a :: "'x" 

18264  307 
shows "a\<sharp>[]" 
17870  308 
by (simp add: fresh_def supp_list_nil) 
309 

310 
lemma fresh_list_cons: 

311 
fixes a :: "'x" 

312 
and x :: "'a" 

313 
and xs :: "'a list" 

314 
shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>xs)" 

315 
by (simp add: fresh_def supp_list_cons) 

316 

317 
lemma fresh_list_append: 

318 
fixes a :: "'x" 

319 
and xs :: "'a list" 

320 
and ys :: "'a list" 

321 
shows "a\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)" 

322 
by (simp add: fresh_def supp_list_append) 

323 

324 
lemma fresh_list_rev: 

325 
fixes a :: "'x" 

326 
and xs :: "'a list" 

327 
shows "a\<sharp>(rev xs) = a\<sharp>xs" 

328 
by (simp add: fresh_def supp_list_rev) 

329 

330 
lemma fresh_none: 

331 
fixes a :: "'x" 

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  334 

335 
lemma fresh_some: 

336 
fixes a :: "'x" 

337 
and x :: "'a" 

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  340 

21010
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

341 
lemma fresh_int: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

342 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

343 
and i :: "int" 
7fe928722821
added the missing freshnesslemmas 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 freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

346 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

347 
lemma fresh_nat: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

348 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

349 
and n :: "nat" 
7fe928722821
added the missing freshnesslemmas 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 freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

352 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

353 
lemma fresh_char: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

354 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

355 
and c :: "char" 
7fe928722821
added the missing freshnesslemmas 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 freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

358 

7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

359 
lemma fresh_string: 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

360 
fixes a :: "'x" 
7fe928722821
added the missing freshnesslemmas for nat, int, char and string and
urbanc
parents:
20809
diff
changeset

361 
and s :: "string" 
7fe928722821
added the missing freshnesslemmas 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 freshnesslemmas 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  391 
ML {* 
392 
val mksimps_pairs = (@{const_name Nominal.fresh}, @{thms fresh_prodD}) :: mksimps_pairs; 

393 
*} 

394 
declaration {* fn _ => 

45625
750c5a47400b
modernized some oldstyle 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  398 
section {* Abstract Properties for Permutations and Atoms *} 
399 
(*=========================================================*) 

400 

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  403 
"pt TYPE('a) TYPE('x) \<equiv> 
404 
(\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and> 

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  407 

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  410 
"at TYPE('x) \<equiv> 
411 
(\<forall>(x::'x). ([]::'x prm)\<bullet>x = x) \<and> 

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> 

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> 

414 
(infinite (UNIV::'x set))" 

415 

416 
(* property of two atomtypes 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  418 
"disjoint TYPE('x) TYPE('y) \<equiv> 
419 
(\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and> 

420 
(\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)" 

421 

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  424 
"cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
425 
(\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))" 

426 

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  429 
"fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)" 
430 

431 
section {* Lemmas about the atomtype properties*} 

432 
(*==============================================*) 

433 

434 
lemma at1: 

435 
fixes x::"'x" 

436 
assumes a: "at TYPE('x)" 

437 
shows "([]::'x prm)\<bullet>x = x" 

438 
using a by (simp add: at_def) 

439 

440 
lemma at2: 

441 
fixes a ::"'x" 

442 
and b ::"'x" 

443 
and x ::"'x" 

444 
and pi::"'x prm" 

445 
assumes a: "at TYPE('x)" 

446 
shows "((a,b)#pi)\<bullet>x = swap (a,b) (pi\<bullet>x)" 

447 
using a by (simp only: at_def) 

448 

449 
lemma at3: 

450 
fixes a ::"'x" 

451 
and b ::"'x" 

452 
and c ::"'x" 

453 
assumes a: "at TYPE('x)" 

454 
shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))" 

455 
using a by (simp only: at_def) 

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  458 
lemmas at_calc = at2 at1 at3 
459 

22610  460 
lemma at_swap_simps: 
461 
fixes a ::"'x" 

462 
and b ::"'x" 

463 
assumes a: "at TYPE('x)" 

464 
shows "[(a,b)]\<bullet>a = b" 

465 
and "[(a,b)]\<bullet>b = a" 

27374  466 
and "\<lbrakk>a\<noteq>c; b\<noteq>c\<rbrakk> \<Longrightarrow> [(a,b)]\<bullet>c = c" 
22610  467 
using a by (simp_all add: at_calc) 
468 

17870  469 
lemma at4: 
470 
assumes a: "at TYPE('x)" 

471 
shows "infinite (UNIV::'x set)" 

472 
using a by (simp add: at_def) 

473 

474 
lemma at_append: 

475 
fixes pi1 :: "'x prm" 

476 
and pi2 :: "'x prm" 

477 
and c :: "'x" 

478 
assumes at: "at TYPE('x)" 

479 
shows "(pi1@pi2)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)" 

480 
proof (induct pi1) 

481 
case Nil show ?case by (simp add: at1[OF at]) 

482 
next 

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  487 
qed 
488 

489 
lemma at_swap: 

490 
fixes a :: "'x" 

491 
and b :: "'x" 

492 
and c :: "'x" 

493 
assumes at: "at TYPE('x)" 

494 
shows "swap (a,b) (swap (a,b) c) = c" 

495 
by (auto simp add: at3[OF at]) 

496 

497 
lemma at_rev_pi: 

498 
fixes pi :: "'x prm" 

499 
and c :: "'x" 

500 
assumes at: "at TYPE('x)" 

501 
shows "(rev pi)\<bullet>(pi\<bullet>c) = c" 

502 
proof(induct pi) 

503 
case Nil show ?case by (simp add: at1[OF at]) 

504 
next 

505 
case (Cons x xs) thus ?case 

506 
by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at]) 

507 
qed 

508 

509 
lemma at_pi_rev: 

510 
fixes pi :: "'x prm" 

511 
and x :: "'x" 

512 
assumes at: "at TYPE('x)" 

513 
shows "pi\<bullet>((rev pi)\<bullet>x) = x" 

514 
by (rule at_rev_pi[OF at, of "rev pi" _,simplified]) 

515 

516 
lemma at_bij1: 

517 
fixes pi :: "'x prm" 

518 
and x :: "'x" 

519 
and y :: "'x" 

520 
assumes at: "at TYPE('x)" 

521 
and a: "(pi\<bullet>x) = y" 

522 
shows "x=(rev pi)\<bullet>y" 

523 
proof  

524 
from a have "y=(pi\<bullet>x)" by (rule sym) 

525 
thus ?thesis by (simp only: at_rev_pi[OF at]) 

526 
qed 

527 

528 
lemma at_bij2: 

529 
fixes pi :: "'x prm" 

530 
and x :: "'x" 

531 
and y :: "'x" 

532 
assumes at: "at TYPE('x)" 

533 
and a: "((rev pi)\<bullet>x) = y" 

534 
shows "x=pi\<bullet>y" 

535 
proof  

536 
from a have "y=((rev pi)\<bullet>x)" by (rule sym) 

537 
thus ?thesis by (simp only: at_pi_rev[OF at]) 

538 
qed 

539 

540 
lemma at_bij: 

541 
fixes pi :: "'x prm" 

542 
and x :: "'x" 

543 
and y :: "'x" 

544 
assumes at: "at TYPE('x)" 

545 
shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 

546 
proof 

547 
assume "pi\<bullet>x = pi\<bullet>y" 

548 
hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 

549 
thus "x=y" by (simp only: at_rev_pi[OF at]) 

550 
next 

551 
assume "x=y" 

552 
thus "pi\<bullet>x = pi\<bullet>y" by simp 

553 
qed 

554 

555 
lemma at_supp: 

556 
fixes x :: "'x" 

557 
assumes at: "at TYPE('x)" 

558 
shows "supp x = {x}" 

29903  559 
by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at]) 
17870  560 

561 
lemma at_fresh: 

562 
fixes a :: "'x" 

563 
and b :: "'x" 

564 
assumes at: "at TYPE('x)" 

565 
shows "(a\<sharp>b) = (a\<noteq>b)" 

566 
by (simp add: at_supp[OF at] fresh_def) 

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 permutationequivalence for the
urbanc
parents:
19045
diff
changeset

584 
lemma at_prm_fresh: 
17870  585 
fixes c :: "'x" 
586 
and pi:: "'x prm" 

587 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

588 
and a: "c\<sharp>pi" 
b16a45c53884
added a few lemmas to do with permutationequivalence 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  591 

592 
lemma at_prm_rev_eq: 

593 
fixes pi1 :: "'x prm" 

594 
and pi2 :: "'x prm" 

595 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

596 
shows "((rev pi1) \<triangleq> (rev pi2)) = (pi1 \<triangleq> pi2)" 
17870  597 
proof (simp add: prm_eq_def, auto) 
598 
fix x 

599 
assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x" 

600 
hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp 

601 
hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at]) 

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  604 
next 
605 
fix x 

606 
assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x" 

607 
hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp 

608 
hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at]) 

609 
hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at]) 

610 
thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp 

611 
qed 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

612 

b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

613 
lemma at_prm_eq_append: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

614 
fixes pi1 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

615 
and pi2 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

616 
and pi3 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

617 
assumes at: "at TYPE('x)" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

618 
and a: "pi1 \<triangleq> pi2" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

619 
shows "(pi3@pi1) \<triangleq> (pi3@pi2)" 
b16a45c53884
added a few lemmas to do with permutationequivalence 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 permutationequivalence for the
urbanc
parents:
19045
diff
changeset

621 

19325  622 
lemma at_prm_eq_append': 
623 
fixes pi1 :: "'x prm" 

624 
and pi2 :: "'x prm" 

625 
and pi3 :: "'x prm" 

626 
assumes at: "at TYPE('x)" 

627 
and a: "pi1 \<triangleq> pi2" 

628 
shows "(pi1@pi3) \<triangleq> (pi2@pi3)" 

629 
using a by (simp add: prm_eq_def at_append[OF at]) 

630 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

631 
lemma at_prm_eq_trans: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

632 
fixes pi1 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

633 
and pi2 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

634 
and pi3 :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

635 
assumes a1: "pi1 \<triangleq> pi2" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

636 
and a2: "pi2 \<triangleq> pi3" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

637 
shows "pi1 \<triangleq> pi3" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

638 
using a1 a2 by (auto simp add: prm_eq_def) 
17870  639 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

640 
lemma at_prm_eq_refl: 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

641 
fixes pi :: "'x prm" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

642 
shows "pi \<triangleq> pi" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

643 
by (simp add: prm_eq_def) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

644 

17870  645 
lemma at_prm_rev_eq1: 
646 
fixes pi1 :: "'x prm" 

647 
and pi2 :: "'x prm" 

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  650 
by (simp add: at_prm_rev_eq[OF at]) 
651 

652 
lemma at_ds1: 

653 
fixes a :: "'x" 

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  656 
by (force simp add: prm_eq_def at_calc[OF at]) 
657 

658 
lemma at_ds2: 

659 
fixes pi :: "'x prm" 

660 
and a :: "'x" 

661 
and b :: "'x" 

662 
assumes at: "at TYPE('x)" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

663 
shows "([(a,b)]@pi) \<triangleq> (pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)])" 
17870  664 
by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
665 
at_rev_pi[OF at] at_calc[OF at]) 

666 

667 
lemma at_ds3: 

668 
fixes a :: "'x" 

669 
and b :: "'x" 

670 
and c :: "'x" 

671 
assumes at: "at TYPE('x)" 

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  674 
using a by (force simp add: prm_eq_def at_calc[OF at]) 
675 

676 
lemma at_ds4: 

677 
fixes a :: "'x" 

678 
and b :: "'x" 

679 
and pi :: "'x prm" 

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  682 
by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
683 
at_pi_rev[OF at] at_rev_pi[OF at]) 

684 

685 
lemma at_ds5: 

686 
fixes a :: "'x" 

687 
and b :: "'x" 

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  690 
by (force simp add: prm_eq_def at_calc[OF at]) 
691 

19164  692 
lemma at_ds5': 
693 
fixes a :: "'x" 

694 
and b :: "'x" 

695 
assumes at: "at TYPE('x)" 

696 
shows "[(a,b),(b,a)] \<triangleq> []" 

697 
by (force simp add: prm_eq_def at_calc[OF at]) 

698 

17870  699 
lemma at_ds6: 
700 
fixes a :: "'x" 

701 
and b :: "'x" 

702 
and c :: "'x" 

703 
assumes at: "at TYPE('x)" 

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  706 
using a by (force simp add: prm_eq_def at_calc[OF at]) 
707 

708 
lemma at_ds7: 

709 
fixes pi :: "'x prm" 

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  712 
by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at]) 
713 

714 
lemma at_ds8_aux: 

715 
fixes pi :: "'x prm" 

716 
and a :: "'x" 

717 
and b :: "'x" 

718 
and c :: "'x" 

719 
assumes at: "at TYPE('x)" 

720 
shows "pi\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>c)" 

721 
by (force simp add: at_calc[OF at] at_bij[OF at]) 

722 

723 
lemma at_ds8: 

724 
fixes pi1 :: "'x prm" 

725 
and pi2 :: "'x prm" 

726 
and a :: "'x" 

727 
and b :: "'x" 

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  730 
apply(induct_tac pi2) 
731 
apply(simp add: prm_eq_def) 

732 
apply(auto simp add: prm_eq_def) 

733 
apply(simp add: at2[OF at]) 

734 
apply(drule_tac x="aa" in spec) 

735 
apply(drule sym) 

736 
apply(simp) 

737 
apply(simp add: at_append[OF at]) 

738 
apply(simp add: at2[OF at]) 

739 
apply(simp add: at_ds8_aux[OF at]) 

740 
done 

741 

742 
lemma at_ds9: 

743 
fixes pi1 :: "'x prm" 

744 
and pi2 :: "'x prm" 

745 
and a :: "'x" 

746 
and b :: "'x" 

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  749 
apply(induct_tac pi2) 
750 
apply(simp add: prm_eq_def) 

751 
apply(auto simp add: prm_eq_def) 

752 
apply(simp add: at_append[OF at]) 

753 
apply(simp add: at2[OF at] at1[OF at]) 

754 
apply(drule_tac x="swap(pi1\<bullet>a,pi1\<bullet>b) aa" in spec) 

755 
apply(drule sym) 

756 
apply(simp) 

757 
apply(simp add: at_ds8_aux[OF at]) 

758 
apply(simp add: at_rev_pi[OF at]) 

759 
done 

760 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

761 
lemma at_ds10: 
19132  762 
fixes pi :: "'x prm" 
19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

763 
and a :: "'x" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

764 
and b :: "'x" 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

765 
assumes at: "at TYPE('x)" 
19132  766 
and a: "b\<sharp>(rev pi)" 
767 
shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])" 

19107
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

768 
using a 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

769 
apply  
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

770 
apply(rule at_prm_eq_trans) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

771 
apply(rule at_ds2[OF at]) 
b16a45c53884
added a few lemmas to do with permutationequivalence 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 permutationequivalence for the
urbanc
parents:
19045
diff
changeset

773 
apply(rule at_prm_eq_refl) 
b16a45c53884
added a few lemmas to do with permutationequivalence for the
urbanc
parents:
19045
diff
changeset

774 
done 
b16a45c53884
added a few lemmas to do with permutationequivalence 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  777 
lemma ex_in_inf: 
778 
fixes A::"'x set" 

779 
assumes at: "at TYPE('x)" 

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  782 
proof  
783 
from fs at4[OF at] have "infinite ((UNIV::'x set)  A)" 

784 
by (simp add: Diff_infinite_finite) 

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  788 
then show ?thesis .. 
17870  789 
qed 
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  799 
lemma at_exists_fresh: 
800 
fixes x :: "'a" 

801 
assumes at: "at TYPE('x)" 

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  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  819 
done 
820 

19140  821 
lemma at_different: 
19132  822 
assumes at: "at TYPE('x)" 
19140  823 
shows "\<exists>(b::'x). a\<noteq>b" 
19132  824 
proof  
19140  825 
have "infinite (UNIV::'x set)" by (rule at4[OF at]) 
826 
hence inf2: "infinite (UNIV{a})" by (rule infinite_remove) 

19132  827 
have "(UNIV{a}) \<noteq> ({}::'x set)" 
828 
proof (rule_tac ccontr, drule_tac notnotD) 

829 
assume "UNIV{a} = ({}::'x set)" 

830 
with inf2 have "infinite ({}::'x set)" by simp 

19869  831 
then show "False" by auto 
19132  832 
qed 
833 
hence "\<exists>(b::'x). b\<in>(UNIV{a})" by blast 

834 
then obtain b::"'x" where mem2: "b\<in>(UNIV{a})" by blast 

19140  835 
from mem2 have "a\<noteq>b" by blast 
836 
then show "\<exists>(b::'x). a\<noteq>b" by blast 

19132  837 
qed 
838 

17870  839 
"the atprops imply the ptprops" 
840 
lemma at_pt_inst: 

841 
assumes at: "at TYPE('x)" 

842 
shows "pt TYPE('x) TYPE('x)" 

843 
apply(auto simp only: pt_def) 

844 
apply(simp only: at1[OF at]) 

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  847 
done 
848 

849 
section {* finite support properties *} 

850 
(*===================================*) 

851 

852 
lemma fs1: 

853 
fixes x :: "'a" 

854 
assumes a: "fs TYPE('a) TYPE('x)" 

855 
shows "finite ((supp x)::'x set)" 

856 
using a by (simp add: fs_def) 

857 

858 
lemma fs_at_inst: 

859 
fixes a :: "'x" 

860 
assumes at: "at TYPE('x)" 

861 
shows "fs TYPE('x) TYPE('x)" 

862 
apply(simp add: fs_def) 

863 
apply(simp add: at_supp[OF at]) 

864 
done 

865 

866 
lemma fs_unit_inst: 

867 
shows "fs TYPE(unit) TYPE('x)" 

868 
apply(simp add: fs_def) 

869 
apply(simp add: supp_unit) 

870 
done 

871 

872 
lemma fs_prod_inst: 

873 
assumes fsa: "fs TYPE('a) TYPE('x)" 

874 
and fsb: "fs TYPE('b) TYPE('x)" 

875 
shows "fs TYPE('a\<times>'b) TYPE('x)" 

876 
apply(unfold fs_def) 

877 
apply(auto simp add: supp_prod) 

878 
apply(rule fs1[OF fsa]) 

879 
apply(rule fs1[OF fsb]) 

880 
done 

881 

18600  882 
lemma fs_nprod_inst: 
883 
assumes fsa: "fs TYPE('a) TYPE('x)" 

884 
and fsb: "fs TYPE('b) TYPE('x)" 

885 
shows "fs TYPE(('a,'b) nprod) TYPE('x)" 

886 
apply(unfold fs_def, rule allI) 

887 
apply(case_tac x) 

888 
apply(auto simp add: supp_nprod) 

889 
apply(rule fs1[OF fsa]) 

890 
apply(rule fs1[OF fsb]) 

891 
done 

892 

17870  893 
lemma fs_list_inst: 
894 
assumes fs: "fs TYPE('a) TYPE('x)" 

895 
shows "fs TYPE('a list) TYPE('x)" 

896 
apply(simp add: fs_def, rule allI) 

897 
apply(induct_tac x) 

898 
apply(simp add: supp_list_nil) 

899 
apply(simp add: supp_list_cons) 

900 
apply(rule fs1[OF fs]) 

901 
done 

902 

18431  903 
lemma fs_option_inst: 
904 
assumes fs: "fs TYPE('a) TYPE('x)" 

905 
shows "fs TYPE('a option) TYPE('x)" 

17870  906 
apply(simp add: fs_def, rule allI) 
18431  907 
apply(case_tac x) 
908 
apply(simp add: supp_none) 

909 
apply(simp add: supp_some) 

910 
apply(rule fs1[OF fs]) 

17870  911 
done 
912 

913 
section {* Lemmas about the permutation properties *} 

914 
(*=================================================*) 

915 

916 
lemma pt1: 

917 
fixes x::"'a" 

918 
assumes a: "pt TYPE('a) TYPE('x)" 

919 
shows "([]::'x prm)\<bullet>x = x" 

920 
using a by (simp add: pt_def) 

921 

922 
lemma pt2: 

923 
fixes pi1::"'x prm" 

924 
and pi2::"'x prm" 

925 
and x ::"'a" 

926 
assumes a: "pt TYPE('a) TYPE('x)" 

927 
shows "(pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)" 

928 
using a by (simp add: pt_def) 

929 

930 
lemma pt3: 

931 
fixes pi1::"'x prm" 

932 
and pi2::"'x prm" 

933 
and x ::"'a" 

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  936 
using a by (simp add: pt_def) 
937 

938 
lemma pt3_rev: 

939 
fixes pi1::"'x prm" 

940 
and pi2::"'x prm" 

941 
and x ::"'a" 

942 
assumes pt: "pt TYPE('a) TYPE('x)" 

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  945 
by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at]) 
946 

947 
section {* composition properties *} 

948 
(* ============================== *) 

949 
lemma cp1: 

950 
fixes pi1::"'x prm" 

951 
and pi2::"'y prm" 

952 
and x ::"'a" 

953 
assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" 

954 
shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x)" 

955 
using cp by (simp add: cp_def) 

956 

957 
lemma cp_pt_inst: 

958 
assumes pt: "pt TYPE('a) TYPE('x)" 

959 
and at: "at TYPE('x)" 

960 
shows "cp TYPE('a) TYPE('x) TYPE('x)" 

961 
apply(auto simp add: cp_def pt2[OF pt,symmetric]) 

962 
apply(rule pt3[OF pt]) 

963 
apply(rule at_ds8[OF at]) 

964 
done 

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  979 
shows "pi\<bullet>x=x" 
45961  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  1012 
section {* permutation type instances *} 
1013 
(* ===================================*) 

1014 

44696  1015 
lemma pt_fun_inst: 
1016 
assumes pta: "pt TYPE('a) TYPE('x)" 

1017 
and ptb: "pt TYPE('b) TYPE('x)" 

1018 
and at: "at TYPE('x)" 

1019 
shows "pt TYPE('a\<Rightarrow>'b) TYPE('x)" 

1020 
apply(auto simp only: pt_def) 

1021 
apply(simp_all add: perm_fun_def) 

1022 
apply(simp add: pt1[OF pta] pt1[OF ptb]) 

1023 
apply(simp add: pt2[OF pta] pt2[OF ptb]) 

1024 
apply(subgoal_tac "(rev pi1) \<triangleq> (rev pi2)")(*A*) 

1025 
apply(simp add: pt3[OF pta] pt3[OF ptb]) 

1026 
(*A*) 

1027 
apply(simp add: at_prm_rev_eq[OF at]) 

1028 
done 

1029 

1030 
lemma pt_bool_inst: 

1031 
shows "pt TYPE(bool) TYPE('x)" 

1032 
by (simp add: pt_def perm_bool_def) 

1033 

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  1042 

1043 
lemma pt_unit_inst: 

44833  1044 
shows "pt TYPE(unit) TYPE('x)" 
44696  1045 
by (simp add: pt_def) 
1046 

1047 
lemma pt_prod_inst: 

1048 
assumes pta: "pt TYPE('a) TYPE('x)" 

1049 
and ptb: "pt TYPE('b) TYPE('x)" 

1050 
shows "pt TYPE('a \<times> 'b) TYPE('x)" 

1051 
apply(auto simp add: pt_def) 

1052 
apply(rule pt1[OF pta]) 

1053 
apply(rule pt1[OF ptb]) 

1054 
apply(rule pt2[OF pta]) 

1055 
apply(rule pt2[OF ptb]) 

1056 
apply(rule pt3[OF pta],assumption) 

1057 
apply(rule pt3[OF ptb],assumption) 

1058 
done 

1059 

17870  1060 
lemma pt_list_nil: 
1061 
fixes xs :: "'a list" 

1062 
assumes pt: "pt TYPE('a) TYPE ('x)" 

1063 
shows "([]::'x prm)\<bullet>xs = xs" 

1064 
apply(induct_tac xs) 

1065 
apply(simp_all add: pt1[OF pt]) 

1066 
done 

1067 

1068 
lemma pt_list_append: 

1069 
fixes pi1 :: "'x prm" 

1070 
and pi2 :: "'x prm" 

1071 
and xs :: "'a list" 

1072 
assumes pt: "pt TYPE('a) TYPE ('x)" 

1073 
shows "(pi1@pi2)\<bullet>xs = pi1\<bullet>(pi2\<bullet>xs)" 

1074 
apply(induct_tac xs) 

1075 
apply(simp_all add: pt2[OF pt]) 

1076 
done 

1077 

1078 
lemma pt_list_prm_eq: 

1079 
fixes pi1 :: "'x prm" 

1080 
and pi2 :: "'x prm" 

1081 
and xs :: "'a list" 

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  1084 
apply(induct_tac xs) 
1085 
apply(simp_all add: prm_eq_def pt3[OF pt]) 

1086 
done 

1087 

1088 
lemma pt_list_inst: 

1089 
assumes pt: "pt TYPE('a) TYPE('x)" 

1090 
shows "pt TYPE('a list) TYPE('x)" 

1091 
apply(auto simp only: pt_def) 

1092 
apply(rule pt_list_nil[OF pt]) 

1093 
apply(rule pt_list_append[OF pt]) 

1094 
apply(rule pt_list_prm_eq[OF pt],assumption) 

1095 
done 

1096 

1097 
lemma pt_option_inst: 

1098 
assumes pta: "pt TYPE('a) TYPE('x)" 

1099 
shows "pt TYPE('a option) TYPE('x)" 

1100 
apply(auto simp only: pt_def) 

1101 
apply(case_tac "x") 

1102 
apply(simp_all add: pt1[OF pta]) 

1103 
apply(case_tac "x") 

1104 
apply(simp_all add: pt2[OF pta]) 

1105 
apply(case_tac "x") 

1106 
apply(simp_all add: pt3[OF pta]) 

1107 
done 

1108 

1109 
lemma pt_noption_inst: 

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  1112 
apply(auto simp only: pt_def) 
1113 
apply(case_tac "x") 

1114 
apply(simp_all add: pt1[OF pta]) 

1115 
apply(case_tac "x") 

1116 
apply(simp_all add: pt2[OF pta]) 

1117 
apply(case_tac "x") 

1118 
apply(simp_all add: pt3[OF pta]) 

1119 
done 

1120 

44696  1121 
lemma pt_nprod_inst: 
1122 
assumes pta: "pt TYPE('a) TYPE('x)" 

1123 
and ptb: "pt TYPE('b) TYPE('x)" 

1124 
shows "pt TYPE(('a,'b) nprod) TYPE('x)" 

1125 
apply(auto simp add: pt_def) 

1126 
apply(case_tac x) 

1127 
apply(simp add: pt1[OF pta] pt1[OF ptb]) 

1128 
apply(case_tac x) 

1129 
apply(simp add: pt2[OF pta] pt2[OF ptb]) 

1130 
apply(case_tac x) 

1131 
apply(simp add: pt3[OF pta] pt3[OF ptb]) 

1132 
done 

24544  1133 

17870  1134 
section {* further lemmas for permutation types *} 
1135 
(*==============================================*) 

1136 

1137 
lemma pt_rev_pi: 

1138 
fixes pi :: "'x prm" 

1139 
and x :: "'a" 

1140 
assumes pt: "pt TYPE('a) TYPE('x)" 

1141 
and at: "at TYPE('x)" 

1142 
shows "(rev pi)\<bullet>(pi\<bullet>x) = x" 

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  1145 
hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>x" by (simp add: pt3[OF pt]) 
1146 
thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt]) 

1147 
qed 

1148 

1149 
lemma pt_pi_rev: 

1150 
fixes pi :: "'x prm" 

1151 
and x :: "'a" 

1152 
assumes pt: "pt TYPE('a) TYPE('x)" 

1153 
and at: "at TYPE('x)" 

1154 
shows "pi\<bullet>((rev pi)\<bullet>x) = x" 

1155 
by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified]) 

1156 

1157 
lemma pt_bij1: 

1158 
fixes pi :: "'x prm" 

1159 
and x :: "'a" 

1160 
and y :: "'a" 

1161 
assumes pt: "pt TYPE('a) TYPE('x)" 

1162 
and at: "at TYPE('x)" 

1163 
and a: "(pi\<bullet>x) = y" 

1164 
shows "x=(rev pi)\<bullet>y" 

1165 
proof  

1166 
from a have "y=(pi\<bullet>x)" by (rule sym) 

1167 
thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at]) 

1168 
qed 

1169 

1170 
lemma pt_bij2: 

1171 
fixes pi :: "'x prm" 

1172 
and x :: "'a" 

1173 
and y :: "'a" 

1174 
assumes pt: "pt TYPE('a) TYPE('x)" 

1175 
and at: "at TYPE('x)" 

1176 
and a: "x = (rev pi)\<bullet>y" 

1177 
shows "(pi\<bullet>x)=y" 

1178 
using a by (simp add: pt_pi_rev[OF pt, OF at]) 

1179 

1180 
lemma pt_bij: 

1181 
fixes pi :: "'x prm" 

1182 
and x :: "'a" 

1183 
and y :: "'a" 

1184 
assumes pt: "pt TYPE('a) TYPE('x)" 

1185 
and at: "at TYPE('x)" 

1186 
shows "(pi\<bullet>x = pi\<bullet>y) = (x=y)" 

1187 
proof 

1188 
assume "pi\<bullet>x = pi\<bullet>y" 

1189 
hence "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule pt_bij1[OF pt, OF at]) 

1190 
thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at]) 

1191 
next 

1192 
assume "x=y" 

1193 
thus "pi\<bullet>x = pi\<bullet>y" by simp 

1194 
qed 

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  1206 
lemma pt_bij3: 
1207 
fixes pi :: "'x prm" 

1208 
and x :: "'a" 

1209 
and y :: "'a" 

1210 
assumes a: "x=y" 

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  1213 

1214 
lemma pt_bij4: 

1215 
fixes pi :: "'x prm" 

1216 
and x :: "'a" 

1217 
and y :: "'a" 

1218 
assumes pt: "pt TYPE('a) TYPE('x)" 

1219 
and at: "at TYPE('x)" 

1220 
and a: "pi\<bullet>x = pi\<bullet>y" 

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  1223 

1224 
lemma pt_swap_bij: 

1225 
fixes a :: "'x" 

1226 
and b :: "'x" 

1227 
and x :: "'a" 

1228 
assumes pt: "pt TYPE('a) TYPE('x)" 

1229 
and at: "at TYPE('x)" 

1230 
shows "[(a,b)]\<bullet>([(a,b)]\<bullet>x) = x" 

1231 
by (rule pt_bij2[OF pt, OF at], simp) 

1232 

19164  1233 
lemma pt_swap_bij': 
1234 
fixes a :: "'x" 

1235 
and b :: "'x" 

1236 
and x :: "'a" 

1237 
assumes pt: "pt TYPE('a) TYPE('x)" 

1238 
and at: "at TYPE('x)" 

1239 
shows "[(a,b)]\<bullet>([(b,a)]\<bullet>x) = x" 

1240 
apply(simp add: pt2[OF pt,symmetric]) 

1241 
apply(rule trans) 

1242 
apply(rule pt3[OF pt]) 

1243 
apply(rule at_ds5'[OF at]) 

1244 
apply(rule pt1[OF pt]) 

1245 
done 

1246 

24571  1247 
lemma pt_swap_bij'': 
1248 
fixes a :: "'x" 

1249 
and x :: "'a" 

1250 
assumes pt: "pt TYPE('a) TYPE('x)" 

1251 
and at: "at TYPE('x)" 

1252 
shows "[(a,a)]\<bullet>x = x" 

1253 
apply(rule trans) 

1254 
apply(rule pt3[OF pt]) 

1255 
apply(rule at_ds1[OF at]) 

1256 
apply(rule pt1[OF pt]) 

1257 
done 

1258 

26806  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  1262 

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  1266 

17870  1267 
lemma pt_set_bij1: 
1268 
fixes pi :: "'x prm" 

1269 
and x :: "'a" 

1270 
and X :: "'a set" 

1271 
assumes pt: "pt TYPE('a) TYPE('x)" 

1272 
and at: "at TYPE('x)" 

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  1275 

1276 
lemma pt_set_bij1a: 

1277 
fixes pi :: "'x prm" 

1278 
and x :: "'a" 

1279 
and X :: "'a set" 

1280 
assumes pt: "pt TYPE('a) TYPE('x)" 

1281 
and at: "at TYPE('x)" 

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  1284 

1285 
lemma pt_set_bij: 

1286 
fixes pi :: "'x prm" 

1287 
and x :: "'a" 

1288 
and X :: "'a set" 

1289 
assumes pt: "pt TYPE('a) TYPE('x)" 

1290 
and at: "at TYPE('x)" 

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  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  1304 
lemma pt_set_bij2: 
1305 
fixes pi :: "'x prm" 

1306 
and x :: "'a" 

1307 
and X :: "'a set" 

1308 
assumes pt: "pt TYPE('a) TYPE('x)" 

1309 
and at: "at TYPE('x)" 

1310 
and a: "x\<in>X" 

1311 
shows "(pi\<bullet>x)\<in>(pi\<bullet>X)" 

1312 
using a by (simp add: pt_set_bij[OF pt, OF at]) 

1313 

18264  1314 
lemma pt_set_bij2a: 
1315 
fixes pi :: "'x prm" 

1316 
and x :: "'a" 

1317 
and X :: "'a set" 

1318 
assumes pt: "pt TYPE('a) TYPE('x)" 

1319 
and at: "at TYPE('x)" 

1320 
and a: "x\<in>((rev pi)\<bullet>X)" 

1321 
shows "(pi\<bullet>x)\<in>X" 

1322 
using a by (simp add: pt_set_bij1[OF pt, OF at]) 

1323 

26773  1324 
(* FIXME: is this lemma needed anywhere? *) 
17870  1325 
lemma pt_set_bij3: 
1326 
fixes pi :: "'x prm" 

1327 
and x :: "'a" 

1328 
and X :: "'a set" 

1329 
shows "pi\<bullet>(x\<in>X) = (x\<in>X)" 

26773  1330 
by (simp add: perm_bool) 
17870  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  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 setoperators
urbanc
parents:
19771
diff
changeset

1341 
lemma pt_set_diff_eqvt: 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1342 
fixes X::"'a set" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1343 
and Y::"'a set" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1344 
and pi::"'x prm" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
urbanc
parents:
19771
diff
changeset

1345 
assumes pt: "pt TYPE('a) TYPE('x)" 
45897b49fdd2
added some further lemmas that deal with permutations and setoperators
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 setoperators
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
