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
1995
+ − 23
text {* helper lemmas for the perm_simp *}
1062
+ − 24
+ − 25
definition
+ − 26
"unpermute p = permute (- p)"
+ − 27
+ − 28
lemma eqvt_apply:
+ − 29
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 30
and x :: "'a::pt"
+ − 31
shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ − 32
unfolding permute_fun_def by simp
+ − 33
+ − 34
lemma eqvt_lambda:
+ − 35
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 36
shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ − 37
unfolding permute_fun_def unpermute_def by simp
+ − 38
+ − 39
lemma eqvt_bound:
+ − 40
shows "p \<bullet> unpermute p x \<equiv> x"
+ − 41
unfolding unpermute_def by simp
+ − 42
1995
+ − 43
text {* provides perm_simp methods *}
+ − 44
1062
+ − 45
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
+ − 46
setup Nominal_Permeq.setup
1062
+ − 47
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
+ − 48
method_setup perm_simp =
1947
+ − 49
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
+ − 50
{* 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
+ − 51
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
+ − 52
method_setup perm_strict_simp =
1947
+ − 53
{* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
+ − 54
{* 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
+ − 55
1995
+ − 56
(* the normal version of this lemma would cause loops *)
+ − 57
lemma permute_eqvt_raw[eqvt_raw]:
+ − 58
shows "p \<bullet> permute \<equiv> permute"
+ − 59
apply(simp add: expand_fun_eq permute_fun_def)
+ − 60
apply(subst permute_eqvt)
+ − 61
apply(simp)
+ − 62
done
+ − 63
+ − 64
section {* Logical Operators *}
+ − 65
+ − 66
lemma eq_eqvt[eqvt]:
+ − 67
shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ − 68
unfolding permute_eq_iff permute_bool_def ..
+ − 69
+ − 70
lemma if_eqvt[eqvt]:
+ − 71
shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ − 72
by (simp add: permute_fun_def permute_bool_def)
+ − 73
+ − 74
lemma True_eqvt[eqvt]:
+ − 75
shows "p \<bullet> True = True"
+ − 76
unfolding permute_bool_def ..
+ − 77
+ − 78
lemma False_eqvt[eqvt]:
+ − 79
shows "p \<bullet> False = False"
+ − 80
unfolding permute_bool_def ..
+ − 81
+ − 82
lemma imp_eqvt[eqvt]:
+ − 83
shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ − 84
by (simp add: permute_bool_def)
+ − 85
+ − 86
lemma conj_eqvt[eqvt]:
+ − 87
shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ − 88
by (simp add: permute_bool_def)
+ − 89
+ − 90
lemma disj_eqvt[eqvt]:
+ − 91
shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ − 92
by (simp add: permute_bool_def)
+ − 93
+ − 94
lemma Not_eqvt[eqvt]:
+ − 95
shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
+ − 96
by (simp add: permute_bool_def)
+ − 97
+ − 98
lemma all_eqvt[eqvt]:
+ − 99
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ − 100
unfolding permute_fun_def permute_bool_def
+ − 101
by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+ − 102
+ − 103
lemma all_eqvt2:
+ − 104
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ − 105
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 106
+ − 107
lemma ex_eqvt[eqvt]:
+ − 108
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ − 109
unfolding permute_fun_def permute_bool_def
+ − 110
by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+ − 111
+ − 112
lemma ex_eqvt2:
+ − 113
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ − 114
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 115
+ − 116
lemma ex1_eqvt[eqvt]:
+ − 117
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ − 118
unfolding Ex1_def
+ − 119
by (perm_simp) (rule refl)
+ − 120
+ − 121
lemma ex1_eqvt2:
+ − 122
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ − 123
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 124
+ − 125
lemma the_eqvt:
+ − 126
assumes unique: "\<exists>!x. P x"
+ − 127
shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
+ − 128
apply(rule the1_equality [symmetric])
+ − 129
apply(simp add: ex1_eqvt2[symmetric])
+ − 130
apply(simp add: permute_bool_def unique)
+ − 131
apply(simp add: permute_bool_def)
+ − 132
apply(rule theI'[OF unique])
+ − 133
done
+ − 134
+ − 135
section {* Set Operations *}
+ − 136
+ − 137
lemma mem_permute_iff:
+ − 138
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+ − 139
unfolding mem_def permute_fun_def permute_bool_def
+ − 140
by simp
+ − 141
+ − 142
lemma mem_eqvt[eqvt]:
+ − 143
shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+ − 144
unfolding mem_def
+ − 145
by (perm_simp) (rule refl)
+ − 146
+ − 147
lemma not_mem_eqvt:
+ − 148
shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
+ − 149
by (perm_simp) (rule refl)
+ − 150
+ − 151
lemma Collect_eqvt[eqvt]:
+ − 152
shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ − 153
unfolding Collect_def permute_fun_def ..
+ − 154
+ − 155
lemma Collect_eqvt2:
+ − 156
shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
+ − 157
by (perm_simp add: permute_minus_cancel) (rule refl)
+ − 158
2002
+ − 159
lemma Bex_eqvt[eqvt]:
+ − 160
shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ − 161
unfolding Bex_def
+ − 162
by (perm_simp) (rule refl)
+ − 163
+ − 164
lemma Ball_eqvt[eqvt]:
+ − 165
shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+ − 166
unfolding Ball_def
+ − 167
by (perm_simp) (rule refl)
+ − 168
1995
+ − 169
lemma empty_eqvt[eqvt]:
+ − 170
shows "p \<bullet> {} = {}"
+ − 171
unfolding empty_def
+ − 172
by (perm_simp) (rule refl)
+ − 173
+ − 174
lemma supp_set_empty:
+ − 175
shows "supp {} = {}"
+ − 176
unfolding supp_def
+ − 177
by (simp add: empty_eqvt)
+ − 178
+ − 179
lemma fresh_set_empty:
+ − 180
shows "a \<sharp> {}"
+ − 181
by (simp add: fresh_def supp_set_empty)
+ − 182
+ − 183
lemma UNIV_eqvt[eqvt]:
+ − 184
shows "p \<bullet> UNIV = UNIV"
+ − 185
unfolding UNIV_def
+ − 186
by (perm_simp) (rule refl)
+ − 187
+ − 188
lemma union_eqvt[eqvt]:
+ − 189
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ − 190
unfolding Un_def
+ − 191
by (perm_simp) (rule refl)
+ − 192
+ − 193
lemma inter_eqvt[eqvt]:
+ − 194
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ − 195
unfolding Int_def
+ − 196
by (perm_simp) (rule refl)
+ − 197
+ − 198
lemma Diff_eqvt[eqvt]:
+ − 199
fixes A B :: "'a::pt set"
+ − 200
shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ − 201
unfolding set_diff_eq
+ − 202
by (perm_simp) (rule refl)
+ − 203
+ − 204
lemma Compl_eqvt[eqvt]:
+ − 205
fixes A :: "'a::pt set"
+ − 206
shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ − 207
unfolding Compl_eq_Diff_UNIV
+ − 208
by (perm_simp) (rule refl)
+ − 209
+ − 210
lemma insert_eqvt[eqvt]:
+ − 211
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
+ − 212
unfolding permute_set_eq_image image_insert ..
+ − 213
+ − 214
lemma vimage_eqvt[eqvt]:
+ − 215
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ − 216
unfolding vimage_def
+ − 217
by (perm_simp) (rule refl)
+ − 218
2002
+ − 219
lemma Union_eqvt[eqvt]:
+ − 220
shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+ − 221
unfolding Union_eq
+ − 222
by (perm_simp) (rule refl)
+ − 223
1995
+ − 224
lemma finite_permute_iff:
+ − 225
shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+ − 226
unfolding permute_set_eq_vimage
+ − 227
using bij_permute by (rule finite_vimage_iff)
+ − 228
+ − 229
lemma finite_eqvt[eqvt]:
+ − 230
shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ − 231
unfolding finite_permute_iff permute_bool_def ..
+ − 232
+ − 233
section {* List Operations *}
+ − 234
+ − 235
lemma append_eqvt[eqvt]:
+ − 236
shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ − 237
by (induct xs) auto
+ − 238
+ − 239
lemma supp_append:
+ − 240
shows "supp (xs @ ys) = supp xs \<union> supp ys"
+ − 241
by (induct xs) (auto simp add: supp_Nil supp_Cons)
+ − 242
+ − 243
lemma fresh_append:
+ − 244
shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+ − 245
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+ − 246
+ − 247
lemma rev_eqvt[eqvt]:
+ − 248
shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ − 249
by (induct xs) (simp_all add: append_eqvt)
+ − 250
+ − 251
lemma supp_rev:
+ − 252
shows "supp (rev xs) = supp xs"
+ − 253
by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+ − 254
+ − 255
lemma fresh_rev:
+ − 256
shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ − 257
by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+ − 258
+ − 259
lemma set_eqvt[eqvt]:
+ − 260
shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
+ − 261
by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+ − 262
+ − 263
(* needs finite support premise
+ − 264
lemma supp_set:
+ − 265
fixes x :: "'a::pt"
+ − 266
shows "supp (set xs) = supp xs"
+ − 267
*)
+ − 268
+ − 269
lemma map_eqvt[eqvt]:
+ − 270
shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ − 271
by (induct xs) (simp_all, simp only: permute_fun_app_eq)
+ − 272
+ − 273
section {* Product Operations *}
+ − 274
+ − 275
lemma fst_eqvt[eqvt]:
+ − 276
"p \<bullet> (fst x) = fst (p \<bullet> x)"
+ − 277
by (cases x) simp
+ − 278
+ − 279
lemma snd_eqvt[eqvt]:
+ − 280
"p \<bullet> (snd x) = snd (p \<bullet> x)"
+ − 281
by (cases x) simp
+ − 282
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
+ − 283
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
+ − 284
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
+ − 285
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
+ − 286
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
+ − 287
1995
+ − 288
section {* Units *}
+ − 289
+ − 290
lemma supp_unit:
+ − 291
shows "supp () = {}"
+ − 292
by (simp add: supp_def)
+ − 293
+ − 294
lemma fresh_unit:
+ − 295
shows "a \<sharp> ()"
+ − 296
by (simp add: fresh_def supp_unit)
+ − 297
+ − 298
2009
+ − 299
section {* additional eqvt lemmas *}
1995
+ − 300
+ − 301
lemmas [eqvt] =
+ − 302
imp_eqvt [folded induct_implies_def]
+ − 303
+ − 304
(* nominal *)
2129
+ − 305
supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt
1995
+ − 306
+ − 307
(* datatypes *)
2009
+ − 308
Pair_eqvt permute_list.simps
1995
+ − 309
+ − 310
(* sets *)
+ − 311
image_eqvt
+ − 312
+ − 313
+ − 314
section {* Test cases *}
+ − 315
+ − 316
2009
+ − 317
declare [[trace_eqvt = false]]
+ − 318
(* 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
+ − 319
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
+ − 320
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
+ − 321
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
+ − 322
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
+ − 323
apply(perm_simp)
1062
+ − 324
oops
+ − 325
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
+ − 326
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
+ − 327
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
+ − 328
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
+ − 329
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
+ − 330
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
+ − 331
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
+ − 332
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
+ − 333
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
+ − 334
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
+ − 335
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
+ − 336
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
+ − 337
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
+ − 338
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
+ − 339
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
+ − 340
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
+ − 341
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
+ − 342
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
+ − 343
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
+ − 344
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
+ − 345
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
+ − 346
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
+ − 347
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
+ − 348
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
+ − 349
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
+ − 350
apply (perm_simp)
1062
+ − 351
oops
+ − 352
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
+ − 353
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
+ − 354
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
+ − 355
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
+ − 356
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
+ − 357
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
+ − 358
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
+ − 359
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
+ − 360
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
+ − 361
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
+ − 362
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
+ − 363
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
+ − 364
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
+ − 365
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
+ − 366
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
+ − 367
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
+ − 368
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
+ − 369
apply(perm_simp)
1062
+ − 370
oops
+ − 371
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
+ − 372
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
+ − 373
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
+ − 374
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
+ − 375
apply (perm_simp)
1062
+ − 376
oops
+ − 377
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
+ − 378
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
+ − 379
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
+ − 380
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
+ − 381
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
+ − 382
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
+ − 383
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
+ − 384
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
+ − 385
2200
31f1ec832d39
fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 386
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
+ − 387
lemma "p \<bullet> (THE x. P x) = foo"
1867
+ − 388
apply(perm_strict_simp exclude: The)
+ − 389
apply(perm_simp exclude: The)
1062
+ − 390
oops
+ − 391
2064
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 392
lemma
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 393
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
+ − 394
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
+ − 395
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
+ − 396
oops
2725853f43b9
solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 397
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
+ − 398
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
+ − 399
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
+ − 400
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
+ − 401
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
+ − 402
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
+ − 403
1953
+ − 404
thm eqvts
+ − 405
thm eqvts_raw
+ − 406
1995
+ − 407
ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
1953
+ − 408
+ − 409
2009
+ − 410
section {* Automatic equivariance procedure for inductive definitions *}
1995
+ − 411
1835
+ − 412
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
+ − 413
1315
+ − 414
end