1062
+ − 1
(* Title: Nominal2_Eqvt
1810
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2
Author: Brian Huffman,
894930834ca8
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 3
Author: Christian Urban
1062
+ − 4
1869
+ − 5
Equivariance, supp and freshness lemmas for various operators
+ − 6
(contains many, but not all such lemmas).
1062
+ − 7
*)
+ − 8
theory Nominal2_Eqvt
1933
9eab1dfc14d2
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
imports Nominal2_Base
1062
+ − 10
uses ("nominal_thmdecls.ML")
+ − 11
("nominal_permeq.ML")
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 12
("nominal_eqvt.ML")
1062
+ − 13
begin
+ − 14
+ − 15
1995
+ − 16
section {* Permsimp and Eqvt infrastructure *}
1062
+ − 17
1869
+ − 18
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+ − 19
1062
+ − 20
use "nominal_thmdecls.ML"
+ − 21
setup "Nominal_ThmDecls.setup"
+ − 22
2466
+ − 23
+ − 24
section {* eqvt lemmas *}
+ − 25
+ − 26
lemmas [eqvt] =
2470
+ − 27
conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
2466
+ − 28
imp_eqvt[folded induct_implies_def]
2467
+ − 29
uminus_eqvt
2466
+ − 30
+ − 31
(* nominal *)
2470
+ − 32
supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt
2467
+ − 33
swap_eqvt flip_eqvt
2466
+ − 34
+ − 35
(* datatypes *)
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
Pair_eqvt permute_list.simps
2466
+ − 37
2470
+ − 38
(* sets *)
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
mem_eqvt empty_eqvt insert_eqvt set_eqvt
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
(* fsets *)
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
permute_fset fset_eqvt
2466
+ − 43
1995
+ − 44
text {* helper lemmas for the perm_simp *}
1062
+ − 45
+ − 46
definition
+ − 47
"unpermute p = permute (- p)"
+ − 48
+ − 49
lemma eqvt_apply:
+ − 50
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 51
and x :: "'a::pt"
+ − 52
shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ − 53
unfolding permute_fun_def by simp
+ − 54
+ − 55
lemma eqvt_lambda:
+ − 56
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 57
shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ − 58
unfolding permute_fun_def unpermute_def by simp
+ − 59
+ − 60
lemma eqvt_bound:
+ − 61
shows "p \<bullet> unpermute p x \<equiv> x"
+ − 62
unfolding unpermute_def by simp
+ − 63
1995
+ − 64
text {* provides perm_simp methods *}
+ − 65
1062
+ − 66
use "nominal_permeq.ML"
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 67
setup Nominal_Permeq.setup
1062
+ − 68
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
method_setup perm_simp =
1947
+ − 70
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ − 71
{* pushes permutations inside. *}
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 73
method_setup perm_strict_simp =
1947
+ − 74
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ − 75
{* pushes permutations inside, raises an error if it cannot solve all permutations. *}
1801
6d2a39db3862
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
1995
+ − 77
(* the normal version of this lemma would cause loops *)
+ − 78
lemma permute_eqvt_raw[eqvt_raw]:
+ − 79
shows "p \<bullet> permute \<equiv> permute"
2479
+ − 80
apply(simp add: fun_eq_iff permute_fun_def)
1995
+ − 81
apply(subst permute_eqvt)
+ − 82
apply(simp)
+ − 83
done
+ − 84
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
subsection {* Equivariance of Logical Operators *}
1995
+ − 86
+ − 87
lemma eq_eqvt[eqvt]:
+ − 88
shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ − 89
unfolding permute_eq_iff permute_bool_def ..
+ − 90
+ − 91
lemma if_eqvt[eqvt]:
+ − 92
shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ − 93
by (simp add: permute_fun_def permute_bool_def)
+ − 94
+ − 95
lemma True_eqvt[eqvt]:
+ − 96
shows "p \<bullet> True = True"
+ − 97
unfolding permute_bool_def ..
+ − 98
+ − 99
lemma False_eqvt[eqvt]:
+ − 100
shows "p \<bullet> False = False"
+ − 101
unfolding permute_bool_def ..
+ − 102
+ − 103
lemma disj_eqvt[eqvt]:
+ − 104
shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ − 105
by (simp add: permute_bool_def)
+ − 106
+ − 107
lemma all_eqvt2:
+ − 108
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ − 109
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 110
+ − 111
lemma ex_eqvt2:
+ − 112
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ − 113
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 114
+ − 115
lemma ex1_eqvt[eqvt]:
+ − 116
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ − 117
unfolding Ex1_def
+ − 118
by (perm_simp) (rule refl)
+ − 119
+ − 120
lemma ex1_eqvt2:
+ − 121
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ − 122
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 123
+ − 124
lemma the_eqvt:
+ − 125
assumes unique: "\<exists>!x. P x"
+ − 126
shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+ − 127
apply(rule the1_equality [symmetric])
+ − 128
apply(simp add: ex1_eqvt2[symmetric])
+ − 129
apply(simp add: permute_bool_def unique)
+ − 130
apply(simp add: permute_bool_def)
+ − 131
apply(rule theI'[OF unique])
+ − 132
done
+ − 133
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
subsection {* Equivariance Set Operations *}
1995
+ − 135
+ − 136
lemma not_mem_eqvt:
+ − 137
shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
+ − 138
by (perm_simp) (rule refl)
+ − 139
+ − 140
lemma Collect_eqvt[eqvt]:
+ − 141
shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ − 142
unfolding Collect_def permute_fun_def ..
+ − 143
+ − 144
lemma Collect_eqvt2:
+ − 145
shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
+ − 146
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 147
2002
+ − 148
lemma Bex_eqvt[eqvt]:
+ − 149
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ − 150
unfolding Bex_def
+ − 151
by (perm_simp) (rule refl)
+ − 152
+ − 153
lemma Ball_eqvt[eqvt]:
+ − 154
shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ − 155
unfolding Ball_def
+ − 156
by (perm_simp) (rule refl)
+ − 157
1995
+ − 158
lemma UNIV_eqvt[eqvt]:
+ − 159
shows "p \<bullet> UNIV = UNIV"
+ − 160
unfolding UNIV_def
+ − 161
by (perm_simp) (rule refl)
+ − 162
+ − 163
lemma union_eqvt[eqvt]:
+ − 164
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ − 165
unfolding Un_def
+ − 166
by (perm_simp) (rule refl)
+ − 167
+ − 168
lemma inter_eqvt[eqvt]:
+ − 169
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ − 170
unfolding Int_def
+ − 171
by (perm_simp) (rule refl)
+ − 172
+ − 173
lemma Diff_eqvt[eqvt]:
+ − 174
fixes A B :: "'a::pt set"
+ − 175
shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ − 176
unfolding set_diff_eq
+ − 177
by (perm_simp) (rule refl)
+ − 178
+ − 179
lemma Compl_eqvt[eqvt]:
+ − 180
fixes A :: "'a::pt set"
+ − 181
shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ − 182
unfolding Compl_eq_Diff_UNIV
+ − 183
by (perm_simp) (rule refl)
+ − 184
2466
+ − 185
lemma image_eqvt:
+ − 186
shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ − 187
unfolding permute_set_eq_image
+ − 188
unfolding permute_fun_def [where f=f]
+ − 189
by (simp add: image_image)
+ − 190
1995
+ − 191
lemma vimage_eqvt[eqvt]:
+ − 192
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ − 193
unfolding vimage_def
+ − 194
by (perm_simp) (rule refl)
+ − 195
2002
+ − 196
lemma Union_eqvt[eqvt]:
+ − 197
shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+ − 198
unfolding Union_eq
+ − 199
by (perm_simp) (rule refl)
+ − 200
1995
+ − 201
lemma finite_permute_iff:
+ − 202
shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+ − 203
unfolding permute_set_eq_vimage
+ − 204
using bij_permute by (rule finite_vimage_iff)
+ − 205
+ − 206
lemma finite_eqvt[eqvt]:
+ − 207
shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ − 208
unfolding finite_permute_iff permute_bool_def ..
+ − 209
2466
+ − 210
1995
+ − 211
section {* List Operations *}
+ − 212
+ − 213
lemma append_eqvt[eqvt]:
+ − 214
shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ − 215
by (induct xs) auto
+ − 216
+ − 217
lemma rev_eqvt[eqvt]:
+ − 218
shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ − 219
by (induct xs) (simp_all add: append_eqvt)
+ − 220
+ − 221
lemma supp_rev:
+ − 222
shows "supp (rev xs) = supp xs"
+ − 223
by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+ − 224
+ − 225
lemma fresh_rev:
+ − 226
shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ − 227
by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+ − 228
+ − 229
lemma map_eqvt[eqvt]:
+ − 230
shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ − 231
by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+ − 232
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 233
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 234
subsection {* Equivariance for fsets *}
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 235
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 236
lemma map_fset_eqvt[eqvt]:
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 237
shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 238
by (lifting map_eqvt)
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 239
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 241
subsection {* Product Operations *}
1995
+ − 242
+ − 243
lemma fst_eqvt[eqvt]:
+ − 244
"p \<bullet> (fst x) = fst (p \<bullet> x)"
+ − 245
by (cases x) simp
+ − 246
+ − 247
lemma snd_eqvt[eqvt]:
+ − 248
"p \<bullet> (snd x) = snd (p \<bullet> x)"
+ − 249
by (cases x) simp
+ − 250
2080
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 251
lemma split_eqvt[eqvt]:
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
unfolding split_def
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
by (perm_simp) (rule refl)
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
1995
+ − 256
+ − 257
section {* Test cases *}
+ − 258
+ − 259
2009
+ − 260
declare [[trace_eqvt = false]]
+ − 261
(* declare [[trace_eqvt = true]] *)
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 263
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 264
fixes B::"'a::pt"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 265
shows "p \<bullet> (B = C)"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
apply(perm_simp)
1062
+ − 267
oops
+ − 268
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 270
fixes B::"bool"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 271
shows "p \<bullet> (B = C)"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
apply(perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 274
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
fixes B::"bool"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
shows "p \<bullet> (A \<longrightarrow> B = C)"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 278
apply (perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
apply(perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 287
shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 288
apply (perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 290
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 292
shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
apply (perm_simp)
1062
+ − 294
oops
+ − 295
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
apply (perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
fixes p q::"perm"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
and x::"'a::pt"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
shows "p \<bullet> (q \<bullet> x) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
apply(perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
fixes p q r::"perm"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
and x::"'a::pt"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312
apply(perm_simp)
1062
+ − 313
oops
+ − 314
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 315
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 316
fixes p r::"perm"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 317
shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 318
apply (perm_simp)
1062
+ − 319
oops
+ − 320
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 321
lemma
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 322
fixes C D::"bool"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 323
shows "B (p \<bullet> (C = D))"
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
apply(perm_simp)
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 325
oops
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 326
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 327
declare [[trace_eqvt = false]]
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 328
2200
31f1ec832d39
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 329
text {* there is no raw eqvt-rule for The *}
1800
78fdc6b36a1c
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 330
lemma "p \<bullet> (THE x. P x) = foo"
1867
+ − 331
apply(perm_strict_simp exclude: The)
+ − 332
apply(perm_simp exclude: The)
1062
+ − 333
oops
+ − 334
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
lemma
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 336
fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)"
2080
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
shows "p \<bullet> (P The) = foo"
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 338
apply(perm_simp exclude: The)
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 339
oops
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 340
2080
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 341
lemma
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 342
fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool"
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 343
shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)"
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 344
apply(perm_simp)
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 345
oops
0532006ec7ec
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 346
1953
+ − 347
thm eqvts
+ − 348
thm eqvts_raw
+ − 349
1995
+ − 350
ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
1953
+ − 351
+ − 352
2565
6bf332360510
moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 353
section {* automatic equivariance procedure for inductive definitions *}
1995
+ − 354
1835
+ − 355
use "nominal_eqvt.ML"
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 356
1315
+ − 357
end