Nominal/Nominal2_Eqvt.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 06 Jan 2011 13:28:19 +0000
changeset 2642 f338b455314c
parent 2635 64b4cb2c2bf8
child 2651 4aa72a88b2c1
permissions -rw-r--r--
same
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     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>
parents: 1803
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>
parents: 1803
diff changeset
     3
    Author:     Christian Urban
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     4
1869
Christian Urban <urbanc@in.tum.de>
parents: 1867
diff changeset
     5
    Equivariance, supp and freshness lemmas for various operators 
Christian Urban <urbanc@in.tum.de>
parents: 1867
diff changeset
     6
    (contains many, but not all such lemmas).
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     7
*)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     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>
parents: 1872
diff changeset
     9
imports Nominal2_Base 
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    10
uses ("nominal_thmdecls.ML")
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    11
     ("nominal_permeq.ML")
1833
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents: 1827
diff changeset
    12
     ("nominal_eqvt.ML")
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    13
begin
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    14
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    15
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    16
section {* Permsimp and Eqvt infrastructure *}
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    17
1869
Christian Urban <urbanc@in.tum.de>
parents: 1867
diff changeset
    18
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
Christian Urban <urbanc@in.tum.de>
parents: 1867
diff changeset
    19
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    20
use "nominal_thmdecls.ML"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    21
setup "Nominal_ThmDecls.setup"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    22
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    23
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    24
section {* eqvt lemmas *}
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    25
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    26
lemmas [eqvt] =
2635
64b4cb2c2bf8 simple cases for string rule inductions
Christian Urban <urbanc@in.tum.de>
parents: 2591
diff changeset
    27
  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt uminus_eqvt
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    28
  imp_eqvt[folded induct_implies_def]
2635
64b4cb2c2bf8 simple cases for string rule inductions
Christian Urban <urbanc@in.tum.de>
parents: 2591
diff changeset
    29
  all_eqvt[folded induct_forall_def]
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    30
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    31
  (* nominal *)
2470
bdb1eab47161 moved everything out of Nominal_Supp
Christian Urban <urbanc@in.tum.de>
parents: 2467
diff changeset
    32
  supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
2467
67b3933c3190 got rid of Nominal_Atoms (folded into Nominal2_Base)
Christian Urban <urbanc@in.tum.de>
parents: 2466
diff changeset
    33
  swap_eqvt flip_eqvt
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    34
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    35
  (* datatypes *)
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    36
  Pair_eqvt permute_list.simps 
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    37
2470
bdb1eab47161 moved everything out of Nominal_Supp
Christian Urban <urbanc@in.tum.de>
parents: 2467
diff changeset
    38
  (* sets *)
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
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>
parents: 2479
diff changeset
    40
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    41
  (* fsets *)
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    42
  permute_fset fset_eqvt
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
    43
2635
64b4cb2c2bf8 simple cases for string rule inductions
Christian Urban <urbanc@in.tum.de>
parents: 2591
diff changeset
    44
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    45
text {* helper lemmas for the perm_simp *}
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    46
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    47
definition
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    48
  "unpermute p = permute (- p)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    49
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    50
lemma eqvt_apply:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    51
  fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    52
  and x :: "'a::pt"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    53
  shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    54
  unfolding permute_fun_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    55
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    56
lemma eqvt_lambda:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    57
  fixes f :: "'a::pt \<Rightarrow> 'b::pt"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    58
  shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    59
  unfolding permute_fun_def unpermute_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    60
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    61
lemma eqvt_bound:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    62
  shows "p \<bullet> unpermute p x \<equiv> x"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    63
  unfolding unpermute_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    64
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    65
text {* provides perm_simp methods *}
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    66
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    67
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>
parents: 1774
diff changeset
    68
setup Nominal_Permeq.setup
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    69
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>
parents: 1774
diff changeset
    70
method_setup perm_simp =
1947
51f411b1197d tuned and cleaned
Christian Urban <urbanc@in.tum.de>
parents: 1934
diff changeset
    71
 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
51f411b1197d tuned and cleaned
Christian Urban <urbanc@in.tum.de>
parents: 1934
diff changeset
    72
 {* 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>
parents: 1774
diff changeset
    73
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>
parents: 1800
diff changeset
    74
method_setup perm_strict_simp =
1947
51f411b1197d tuned and cleaned
Christian Urban <urbanc@in.tum.de>
parents: 1934
diff changeset
    75
 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *}
51f411b1197d tuned and cleaned
Christian Urban <urbanc@in.tum.de>
parents: 1934
diff changeset
    76
 {* 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>
parents: 1800
diff changeset
    77
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    78
(* the normal version of this lemma would cause loops *)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    79
lemma permute_eqvt_raw[eqvt_raw]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    80
  shows "p \<bullet> permute \<equiv> permute"
2479
a9b6a00b1ba0 updated to Isabelle Sept 16
Christian Urban <urbanc@in.tum.de>
parents: 2470
diff changeset
    81
apply(simp add: fun_eq_iff permute_fun_def)
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    82
apply(subst permute_eqvt)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    83
apply(simp)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    84
done
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    85
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
    86
subsection {* Equivariance of Logical Operators *}
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    87
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    88
lemma eq_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    89
  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    90
  unfolding permute_eq_iff permute_bool_def ..
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    91
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    92
lemma if_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    93
  shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    94
  by (simp add: permute_fun_def permute_bool_def)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    95
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    96
lemma True_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    97
  shows "p \<bullet> True = True"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    98
  unfolding permute_bool_def ..
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
    99
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   100
lemma False_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   101
  shows "p \<bullet> False = False"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   102
  unfolding permute_bool_def ..
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   103
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   104
lemma disj_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   105
  shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   106
  by (simp add: permute_bool_def)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   107
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   108
lemma all_eqvt2:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   109
  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   110
  by (perm_simp add: permute_minus_cancel) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   111
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   112
lemma ex_eqvt2:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   113
  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   114
  by (perm_simp add: permute_minus_cancel) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   115
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   116
lemma ex1_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   117
  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   118
  unfolding Ex1_def
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   119
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   120
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   121
lemma ex1_eqvt2:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   122
  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   123
  by (perm_simp add: permute_minus_cancel) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   124
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   125
lemma the_eqvt:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   126
  assumes unique: "\<exists>!x. P x"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   127
  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   128
  apply(rule the1_equality [symmetric])
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   129
  apply(simp add: ex1_eqvt2[symmetric])
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   130
  apply(simp add: permute_bool_def unique)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   131
  apply(simp add: permute_bool_def)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   132
  apply(rule theI'[OF unique])
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   133
  done
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   134
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   135
subsection {* Equivariance Set Operations *}
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   136
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   137
lemma not_mem_eqvt:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   138
  shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   139
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   140
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   141
lemma Collect_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   142
  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   143
  unfolding Collect_def permute_fun_def ..
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   144
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   145
lemma Collect_eqvt2:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   146
  shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   147
  by (perm_simp add: permute_minus_cancel) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   148
2002
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   149
lemma Bex_eqvt[eqvt]:
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   150
  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   151
  unfolding Bex_def
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   152
  by (perm_simp) (rule refl)
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   153
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   154
lemma Ball_eqvt[eqvt]:
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   155
  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   156
  unfolding Ball_def
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   157
  by (perm_simp) (rule refl)
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   158
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   159
lemma UNIV_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   160
  shows "p \<bullet> UNIV = UNIV"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   161
  unfolding UNIV_def
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   162
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   163
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   164
lemma union_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   165
  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   166
  unfolding Un_def
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   167
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   168
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   169
lemma inter_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   170
  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   171
  unfolding Int_def 
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   172
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   173
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   174
lemma Diff_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   175
  fixes A B :: "'a::pt set"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   176
  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   177
  unfolding set_diff_eq
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   178
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   179
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   180
lemma Compl_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   181
  fixes A :: "'a::pt set"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   182
  shows "p \<bullet> (- A) = - (p \<bullet> A)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   183
  unfolding Compl_eq_Diff_UNIV
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   184
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   185
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   186
lemma image_eqvt:
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   187
  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   188
  unfolding permute_set_eq_image
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   189
  unfolding permute_fun_def [where f=f]
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   190
  by (simp add: image_image)
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   191
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   192
lemma vimage_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   193
  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   194
  unfolding vimage_def
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   195
  by (perm_simp) (rule refl)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   196
2002
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   197
lemma Union_eqvt[eqvt]:
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   198
  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   199
  unfolding Union_eq 
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   200
  by (perm_simp) (rule refl)
74d869595fed added eqvt-lemmas for Bex, Ball and Union
Christian Urban <urbanc@in.tum.de>
parents: 1995
diff changeset
   201
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   202
lemma finite_permute_iff:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   203
  shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   204
  unfolding permute_set_eq_vimage
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   205
  using bij_permute by (rule finite_vimage_iff)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   206
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   207
lemma finite_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   208
  shows "p \<bullet> finite A = finite (p \<bullet> A)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   209
  unfolding finite_permute_iff permute_bool_def ..
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   210
2466
47c840599a6b cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents: 2310
diff changeset
   211
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   212
section {* List Operations *}
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   213
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   214
lemma append_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   215
  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   216
  by (induct xs) auto
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   217
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   218
lemma rev_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   219
  shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   220
  by (induct xs) (simp_all add: append_eqvt)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   221
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   222
lemma supp_rev:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   223
  shows "supp (rev xs) = supp xs"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   224
  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   225
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   226
lemma fresh_rev:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   227
  shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   228
  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   229
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   230
lemma map_eqvt[eqvt]: 
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   231
  shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   232
  by (induct xs) (simp_all, simp only: permute_fun_app_eq)
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   233
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   234
2642
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   235
subsection {* Equivariance Finite-Set Operations *}
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   236
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   237
lemma in_fset_eqvt[eqvt]:
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   238
  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   239
unfolding in_fset
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   240
by (perm_simp) (simp)
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   241
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   242
lemma union_fset_eqvt[eqvt]:
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   243
  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   244
by (induct S) (simp_all)
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   245
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   246
lemma supp_union_fset:
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   247
  fixes S T::"'a::fs fset"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   248
  shows "supp (S |\<union>| T) = supp S \<union> supp T"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   249
by (induct S) (auto)
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   250
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   251
lemma fresh_union_fset:
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   252
  fixes S T::"'a::fs fset"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   253
  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   254
unfolding fresh_def
Christian Urban <urbanc@in.tum.de>
parents: 2635
diff changeset
   255
by (simp add: supp_union_fset)
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   256
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   257
lemma map_fset_eqvt[eqvt]: 
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   258
  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>
parents: 2479
diff changeset
   259
  by (lifting map_eqvt)
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   260
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   261
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   262
subsection {* Product Operations *}
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   263
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   264
lemma fst_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   265
  "p \<bullet> (fst x) = fst (p \<bullet> x)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   266
 by (cases x) simp
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   267
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   268
lemma snd_eqvt[eqvt]:
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   269
  "p \<bullet> (snd x) = snd (p \<bullet> x)"
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   270
 by (cases x) simp
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   271
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>
parents: 2064
diff changeset
   272
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>
parents: 2064
diff changeset
   273
  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>
parents: 2064
diff changeset
   274
  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>
parents: 2064
diff changeset
   275
  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>
parents: 2064
diff changeset
   276
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   277
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   278
section {* Test cases *}
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   279
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   280
2009
4f7d7cbd4bc8 removed duplicate eqvt attribute
Christian Urban <urbanc@in.tum.de>
parents: 2002
diff changeset
   281
declare [[trace_eqvt = false]]
4f7d7cbd4bc8 removed duplicate eqvt attribute
Christian Urban <urbanc@in.tum.de>
parents: 2002
diff changeset
   282
(* 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>
parents: 1774
diff changeset
   283
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   284
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>
parents: 1774
diff changeset
   285
  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>
parents: 1774
diff changeset
   286
  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>
parents: 1774
diff changeset
   287
apply(perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   288
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   289
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>
parents: 1774
diff changeset
   290
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>
parents: 1774
diff changeset
   291
  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>
parents: 1774
diff changeset
   292
  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>
parents: 1774
diff changeset
   293
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>
parents: 1774
diff changeset
   294
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>
parents: 1774
diff changeset
   295
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
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>
parents: 1774
diff changeset
   297
  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>
parents: 1774
diff changeset
   298
  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>
parents: 1774
diff changeset
   299
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>
parents: 1774
diff changeset
   300
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>
parents: 1774
diff changeset
   301
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   302
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>
parents: 1774
diff changeset
   303
  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>
parents: 1774
diff changeset
   304
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>
parents: 1774
diff changeset
   305
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>
parents: 1774
diff changeset
   306
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   307
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>
parents: 1774
diff changeset
   308
  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>
parents: 1774
diff changeset
   309
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>
parents: 1774
diff changeset
   310
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>
parents: 1774
diff changeset
   311
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   312
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>
parents: 1774
diff changeset
   313
  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>
parents: 1774
diff changeset
   314
apply (perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   315
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   316
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>
parents: 1774
diff changeset
   317
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>
parents: 1774
diff changeset
   318
  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>
parents: 1774
diff changeset
   319
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>
parents: 1774
diff changeset
   320
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>
parents: 1774
diff changeset
   321
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   322
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>
parents: 1774
diff changeset
   323
  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>
parents: 1774
diff changeset
   324
  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>
parents: 1774
diff changeset
   325
  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>
parents: 1774
diff changeset
   326
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>
parents: 1774
diff changeset
   327
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>
parents: 1774
diff changeset
   328
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   329
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>
parents: 1774
diff changeset
   330
  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>
parents: 1774
diff changeset
   331
  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>
parents: 1774
diff changeset
   332
  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>
parents: 1774
diff changeset
   333
apply(perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   334
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   335
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>
parents: 1774
diff changeset
   336
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>
parents: 1774
diff changeset
   337
  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>
parents: 1774
diff changeset
   338
  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>
parents: 1774
diff changeset
   339
apply (perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   340
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   341
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>
parents: 1774
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>
parents: 1774
diff changeset
   343
  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>
parents: 1774
diff changeset
   344
  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>
parents: 1774
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>
parents: 1774
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>
parents: 1774
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>
parents: 1774
diff changeset
   348
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>
parents: 1774
diff changeset
   349
2200
31f1ec832d39 fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set
Christian Urban <urbanc@in.tum.de>
parents: 2129
diff changeset
   350
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>
parents: 1774
diff changeset
   351
lemma "p \<bullet> (THE x. P x) = foo"
1867
f4477d3fe520 preliminary parser for perm_simp metod
Christian Urban <urbanc@in.tum.de>
parents: 1866
diff changeset
   352
apply(perm_strict_simp exclude: The)
f4477d3fe520 preliminary parser for perm_simp metod
Christian Urban <urbanc@in.tum.de>
parents: 1866
diff changeset
   353
apply(perm_simp exclude: The)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   354
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   355
2064
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents: 2009
diff changeset
   356
lemma 
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents: 2009
diff changeset
   357
  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>
parents: 2064
diff changeset
   358
  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>
parents: 2009
diff changeset
   359
apply(perm_simp exclude: The)
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents: 2009
diff changeset
   360
oops
2725853f43b9 solved the problem with equivariance by first eta-normalising the goal
Christian Urban <urbanc@in.tum.de>
parents: 2009
diff changeset
   361
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>
parents: 2064
diff changeset
   362
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>
parents: 2064
diff changeset
   363
  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>
parents: 2064
diff changeset
   364
  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>
parents: 2064
diff changeset
   365
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>
parents: 2064
diff changeset
   366
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>
parents: 2064
diff changeset
   367
1953
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up
Christian Urban <urbanc@in.tum.de>
parents: 1947
diff changeset
   368
thm eqvts
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up
Christian Urban <urbanc@in.tum.de>
parents: 1947
diff changeset
   369
thm eqvts_raw
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up
Christian Urban <urbanc@in.tum.de>
parents: 1947
diff changeset
   370
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   371
ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
1953
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up
Christian Urban <urbanc@in.tum.de>
parents: 1947
diff changeset
   372
186d8486dfd5 rewrote eqvts_raw to be a symtab, that can be looked up
Christian Urban <urbanc@in.tum.de>
parents: 1947
diff changeset
   373
2565
6bf332360510 moved most material fron Nominal2_FSet into the Nominal_Base theory
Christian Urban <urbanc@in.tum.de>
parents: 2479
diff changeset
   374
section {* automatic equivariance procedure for inductive definitions *}
1995
652f310f0dba reorganised eqvt-file (now uses perm_simp already)
Christian Urban <urbanc@in.tum.de>
parents: 1971
diff changeset
   375
1835
636de31888a6 tuned and removed dead code
Christian Urban <urbanc@in.tum.de>
parents: 1833
diff changeset
   376
use "nominal_eqvt.ML"
1833
2050b5723c04 added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents: 1827
diff changeset
   377
1315
43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   378
end