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
section {* Logical Operators *}
+ − 16
+ − 17
lemma eq_eqvt:
+ − 18
shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
+ − 19
unfolding permute_eq_iff permute_bool_def ..
+ − 20
+ − 21
lemma if_eqvt:
+ − 22
shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
+ − 23
by (simp add: permute_fun_def permute_bool_def)
+ − 24
+ − 25
lemma True_eqvt:
+ − 26
shows "p \<bullet> True = True"
+ − 27
unfolding permute_bool_def ..
+ − 28
+ − 29
lemma False_eqvt:
+ − 30
shows "p \<bullet> False = False"
+ − 31
unfolding permute_bool_def ..
+ − 32
+ − 33
lemma imp_eqvt:
+ − 34
shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+ − 35
by (simp add: permute_bool_def)
+ − 36
+ − 37
lemma conj_eqvt:
+ − 38
shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+ − 39
by (simp add: permute_bool_def)
+ − 40
+ − 41
lemma disj_eqvt:
+ − 42
shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
+ − 43
by (simp add: permute_bool_def)
+ − 44
+ − 45
lemma Not_eqvt:
+ − 46
shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
+ − 47
by (simp add: permute_bool_def)
+ − 48
+ − 49
lemma all_eqvt:
+ − 50
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+ − 51
unfolding permute_fun_def permute_bool_def
+ − 52
by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+ − 53
+ − 54
lemma all_eqvt2:
+ − 55
shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
+ − 56
unfolding permute_fun_def permute_bool_def
+ − 57
by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+ − 58
+ − 59
lemma ex_eqvt:
+ − 60
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+ − 61
unfolding permute_fun_def permute_bool_def
+ − 62
by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+ − 63
+ − 64
lemma ex_eqvt2:
+ − 65
shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
+ − 66
unfolding permute_fun_def permute_bool_def
+ − 67
by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+ − 68
+ − 69
lemma ex1_eqvt:
+ − 70
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
+ − 71
unfolding Ex1_def
+ − 72
by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)
+ − 73
+ − 74
lemma ex1_eqvt2:
+ − 75
shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
+ − 76
unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt
+ − 77
by simp
+ − 78
+ − 79
lemma the_eqvt:
+ − 80
assumes unique: "\<exists>!x. P x"
1087
+ − 81
shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
1062
+ − 82
apply(rule the1_equality [symmetric])
+ − 83
apply(simp add: ex1_eqvt2[symmetric])
+ − 84
apply(simp add: permute_bool_def unique)
+ − 85
apply(simp add: permute_bool_def)
+ − 86
apply(rule theI'[OF unique])
+ − 87
done
+ − 88
+ − 89
section {* Set Operations *}
+ − 90
1087
+ − 91
lemma mem_permute_iff:
+ − 92
shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+ − 93
unfolding mem_def permute_fun_def permute_bool_def
+ − 94
by simp
+ − 95
1062
+ − 96
lemma mem_eqvt:
+ − 97
shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
1087
+ − 98
unfolding mem_permute_iff permute_bool_def by simp
1062
+ − 99
+ − 100
lemma not_mem_eqvt:
+ − 101
shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
+ − 102
unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
+ − 103
+ − 104
lemma Collect_eqvt:
+ − 105
shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
+ − 106
unfolding Collect_def permute_fun_def ..
+ − 107
+ − 108
lemma Collect_eqvt2:
+ − 109
shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
+ − 110
unfolding Collect_def permute_fun_def ..
+ − 111
+ − 112
lemma empty_eqvt:
+ − 113
shows "p \<bullet> {} = {}"
+ − 114
unfolding empty_def Collect_eqvt2 False_eqvt ..
+ − 115
+ − 116
lemma supp_set_empty:
+ − 117
shows "supp {} = {}"
+ − 118
by (simp add: supp_def empty_eqvt)
+ − 119
+ − 120
lemma fresh_set_empty:
+ − 121
shows "a \<sharp> {}"
+ − 122
by (simp add: fresh_def supp_set_empty)
+ − 123
+ − 124
lemma UNIV_eqvt:
+ − 125
shows "p \<bullet> UNIV = UNIV"
+ − 126
unfolding UNIV_def Collect_eqvt2 True_eqvt ..
+ − 127
+ − 128
lemma union_eqvt:
+ − 129
shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
+ − 130
unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp
+ − 131
+ − 132
lemma inter_eqvt:
+ − 133
shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
+ − 134
unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp
+ − 135
+ − 136
lemma Diff_eqvt:
+ − 137
fixes A B :: "'a::pt set"
+ − 138
shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
+ − 139
unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
+ − 140
+ − 141
lemma Compl_eqvt:
+ − 142
fixes A :: "'a::pt set"
+ − 143
shows "p \<bullet> (- A) = - (p \<bullet> A)"
+ − 144
unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..
+ − 145
+ − 146
lemma insert_eqvt:
+ − 147
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
+ − 148
unfolding permute_set_eq_image image_insert ..
+ − 149
+ − 150
lemma vimage_eqvt:
+ − 151
shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
+ − 152
unfolding vimage_def permute_fun_def [where f=f]
+ − 153
unfolding Collect_eqvt2 mem_eqvt ..
+ − 154
+ − 155
lemma image_eqvt:
+ − 156
shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+ − 157
unfolding permute_set_eq_image
+ − 158
unfolding permute_fun_def [where f=f]
+ − 159
by (simp add: image_image)
+ − 160
+ − 161
lemma finite_permute_iff:
+ − 162
shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
+ − 163
unfolding permute_set_eq_vimage
+ − 164
using bij_permute by (rule finite_vimage_iff)
+ − 165
+ − 166
lemma finite_eqvt:
+ − 167
shows "p \<bullet> finite A = finite (p \<bullet> A)"
+ − 168
unfolding finite_permute_iff permute_bool_def ..
+ − 169
+ − 170
+ − 171
section {* List Operations *}
+ − 172
+ − 173
lemma append_eqvt:
+ − 174
shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
+ − 175
by (induct xs) auto
+ − 176
+ − 177
lemma supp_append:
+ − 178
shows "supp (xs @ ys) = supp xs \<union> supp ys"
+ − 179
by (induct xs) (auto simp add: supp_Nil supp_Cons)
+ − 180
+ − 181
lemma fresh_append:
+ − 182
shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
+ − 183
by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+ − 184
+ − 185
lemma rev_eqvt:
+ − 186
shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
+ − 187
by (induct xs) (simp_all add: append_eqvt)
+ − 188
+ − 189
lemma supp_rev:
+ − 190
shows "supp (rev xs) = supp xs"
+ − 191
by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
+ − 192
+ − 193
lemma fresh_rev:
+ − 194
shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
+ − 195
by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
+ − 196
+ − 197
lemma set_eqvt:
+ − 198
shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
+ − 199
by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
+ − 200
+ − 201
(* needs finite support premise
+ − 202
lemma supp_set:
+ − 203
fixes x :: "'a::pt"
+ − 204
shows "supp (set xs) = supp xs"
+ − 205
*)
+ − 206
1815
+ − 207
lemma map_eqvt:
+ − 208
shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
+ − 209
by (induct xs) (simp_all, simp only: permute_fun_app_eq)
1062
+ − 210
+ − 211
section {* Product Operations *}
+ − 212
+ − 213
lemma fst_eqvt:
+ − 214
"p \<bullet> (fst x) = fst (p \<bullet> x)"
+ − 215
by (cases x) simp
+ − 216
+ − 217
lemma snd_eqvt:
+ − 218
"p \<bullet> (snd x) = snd (p \<bullet> x)"
+ − 219
by (cases x) simp
+ − 220
+ − 221
section {* Units *}
+ − 222
+ − 223
lemma supp_unit:
+ − 224
shows "supp () = {}"
+ − 225
by (simp add: supp_def)
+ − 226
+ − 227
lemma fresh_unit:
+ − 228
shows "a \<sharp> ()"
+ − 229
by (simp add: fresh_def supp_unit)
+ − 230
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
+ − 231
lemma permute_eqvt_raw:
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
+ − 232
shows "p \<bullet> permute = permute"
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
+ − 233
apply(simp add: expand_fun_eq permute_fun_def)
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
+ − 234
apply(subst permute_eqvt)
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
+ − 235
apply(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
+ − 236
done
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
+ − 237
1062
+ − 238
section {* Equivariance automation *}
+ − 239
1869
+ − 240
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+ − 241
1062
+ − 242
use "nominal_thmdecls.ML"
+ − 243
setup "Nominal_ThmDecls.setup"
+ − 244
+ − 245
lemmas [eqvt] =
+ − 246
(* connectives *)
+ − 247
eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt
1087
+ − 248
True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt
1062
+ − 249
imp_eqvt [folded induct_implies_def]
+ − 250
+ − 251
(* nominal *)
1934
+ − 252
supp_eqvt fresh_eqvt add_perm_eqvt
1062
+ − 253
+ − 254
(* datatypes *)
1087
+ − 255
permute_prod.simps append_eqvt rev_eqvt set_eqvt
1815
+ − 256
map_eqvt fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
1062
+ − 257
+ − 258
(* sets *)
1087
+ − 259
empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
1315
+ − 260
Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
+ − 261
1934
+ − 262
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
+ − 263
lemmas [eqvt_raw] =
1811
ae176476b525
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 264
permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *)
1062
+ − 265
+ − 266
text {* helper lemmas for the eqvt_tac *}
+ − 267
+ − 268
definition
+ − 269
"unpermute p = permute (- p)"
+ − 270
+ − 271
lemma eqvt_apply:
+ − 272
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 273
and x :: "'a::pt"
+ − 274
shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
+ − 275
unfolding permute_fun_def by simp
+ − 276
+ − 277
lemma eqvt_lambda:
+ − 278
fixes f :: "'a::pt \<Rightarrow> 'b::pt"
+ − 279
shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
+ − 280
unfolding permute_fun_def unpermute_def by simp
+ − 281
+ − 282
lemma eqvt_bound:
+ − 283
shows "p \<bullet> unpermute p x \<equiv> x"
+ − 284
unfolding unpermute_def by simp
+ − 285
1835
+ − 286
(* provides perm_simp methods *)
1062
+ − 287
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
+ − 288
setup Nominal_Permeq.setup
1062
+ − 289
1867
+ − 290
ML {*
1934
+ − 291
val add_thms = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [];
+ − 292
val exclude_consts = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |--
1867
+ − 293
(Scan.repeat (Args.const true))) []
1934
+ − 294
+ − 295
val parser =
+ − 296
add_thms -- exclude_consts ||
+ − 297
exclude_consts -- add_thms >> swap
1867
+ − 298
*}
+ − 299
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
+ − 300
method_setup perm_simp =
1934
+ − 301
{* parser >>
+ − 302
(fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL
+ − 303
(Nominal_Permeq.eqvt_tac ctxt [] consts))) *}
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
+ − 304
{* pushes permutations inside *}
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
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
+ − 306
method_setup perm_strict_simp =
1934
+ − 307
{* parser >>
+ − 308
(fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL
+ − 309
(Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *}
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
+ − 310
{* pushes permutations inside, raises an error if it cannot solve all permutations *}
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
+ − 311
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
+ − 312
declare [[trace_eqvt = true]]
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
+ − 313
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
+ − 314
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
+ − 315
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
+ − 316
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
+ − 317
apply(perm_simp)
1062
+ − 318
oops
+ − 319
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
+ − 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::"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
+ − 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)
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
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
+ − 325
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> (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
+ − 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
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
+ − 334
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
+ − 335
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
+ − 336
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
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
+ − 338
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
+ − 339
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
+ − 340
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
+ − 341
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
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
+ − 343
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
+ − 344
apply (perm_simp)
1062
+ − 345
oops
+ − 346
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
+ − 347
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
+ − 348
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
+ − 349
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
+ − 350
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
+ − 351
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
+ − 352
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
+ − 353
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
+ − 354
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
+ − 355
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
+ − 356
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
+ − 357
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
+ − 358
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
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
+ − 360
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
+ − 361
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
+ − 362
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
+ − 363
apply(perm_simp)
1062
+ − 364
oops
+ − 365
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
+ − 366
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
+ − 367
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
+ − 368
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
+ − 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 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
+ − 374
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
+ − 375
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
+ − 376
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
+ − 377
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
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
+ − 379
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
text {* Problem: there is no raw eqvt-rule for The *}
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
lemma "p \<bullet> (THE x. P x) = foo"
1867
+ − 382
apply(perm_strict_simp exclude: The)
+ − 383
apply(perm_simp exclude: The)
1062
+ − 384
oops
+ − 385
1835
+ − 386
(* automatic equivariance procedure for
+ − 387
inductive definitions *)
+ − 388
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
+ − 389
1315
+ − 390
end