Nominal-General/Nominal2_Eqvt.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 11 Apr 2010 10:36:09 +0200
changeset 1801 6d2a39db3862
parent 1800 78fdc6b36a1c
child 1803 ed46cf122016
permissions -rw-r--r--
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
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
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     2
    Authors:    Brian Huffman, Christian Urban
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     3
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     4
    Equivariance, Supp and Fresh Lemmas for Operators. 
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
     5
    (Contains most, but not all such lemmas.)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     6
*)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     7
theory Nominal2_Eqvt
1315
43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
     8
imports Nominal2_Base Nominal2_Atoms
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
     9
uses ("nominal_thmdecls.ML")
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    10
     ("nominal_permeq.ML")
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    11
begin
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    12
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    13
section {* Logical Operators *}
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
lemma eq_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    16
  shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    17
  unfolding permute_eq_iff permute_bool_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    18
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    19
lemma if_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    20
  shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    21
  by (simp add: permute_fun_def permute_bool_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    22
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    23
lemma True_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    24
  shows "p \<bullet> True = True"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    25
  unfolding permute_bool_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    26
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    27
lemma False_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    28
  shows "p \<bullet> False = False"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    29
  unfolding permute_bool_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    30
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    31
lemma imp_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    32
  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    33
  by (simp add: permute_bool_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    34
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    35
lemma conj_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    36
  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    37
  by (simp add: permute_bool_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    38
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    39
lemma disj_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    40
  shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    41
  by (simp add: permute_bool_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    42
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    43
lemma Not_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    44
  shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    45
  by (simp add: permute_bool_def)
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
lemma all_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    48
  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    49
  unfolding permute_fun_def permute_bool_def
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    50
  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    51
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    52
lemma all_eqvt2:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    53
  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    54
  unfolding permute_fun_def permute_bool_def
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    55
  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    56
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    57
lemma ex_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    58
  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    59
  unfolding permute_fun_def permute_bool_def
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    60
  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    61
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    62
lemma ex_eqvt2:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    63
  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    64
  unfolding permute_fun_def permute_bool_def
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    65
  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    66
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    67
lemma ex1_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    68
  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    69
  unfolding Ex1_def 
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    70
  by (simp add: ex_eqvt permute_fun_def conj_eqvt all_eqvt imp_eqvt eq_eqvt)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    71
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    72
lemma ex1_eqvt2:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    73
  shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    74
  unfolding Ex1_def ex_eqvt2 conj_eqvt all_eqvt2 imp_eqvt eq_eqvt
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    75
  by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    76
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    77
lemma the_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    78
  assumes unique: "\<exists>!x. P x"
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    79
  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    80
  apply(rule the1_equality [symmetric])
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    81
  apply(simp add: ex1_eqvt2[symmetric])
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    82
  apply(simp add: permute_bool_def unique)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    83
  apply(simp add: permute_bool_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    84
  apply(rule theI'[OF unique])
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    85
  done
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    86
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    87
section {* Set Operations *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    88
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    89
lemma mem_permute_iff:
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    90
  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    91
unfolding mem_def permute_fun_def permute_bool_def
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    92
by simp
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    93
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    94
lemma mem_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    95
  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
    96
  unfolding mem_permute_iff permute_bool_def by simp
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    97
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    98
lemma not_mem_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
    99
  shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   100
  unfolding mem_def permute_fun_def by (simp add: Not_eqvt)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   101
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   102
lemma Collect_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   103
  shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   104
  unfolding Collect_def permute_fun_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   105
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   106
lemma Collect_eqvt2:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   107
  shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   108
  unfolding Collect_def permute_fun_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   109
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   110
lemma empty_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   111
  shows "p \<bullet> {} = {}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   112
  unfolding empty_def Collect_eqvt2 False_eqvt ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   113
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   114
lemma supp_set_empty:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   115
  shows "supp {} = {}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   116
  by (simp add: supp_def empty_eqvt)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   117
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   118
lemma fresh_set_empty:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   119
  shows "a \<sharp> {}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   120
  by (simp add: fresh_def supp_set_empty)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   121
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   122
lemma UNIV_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   123
  shows "p \<bullet> UNIV = UNIV"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   124
  unfolding UNIV_def Collect_eqvt2 True_eqvt ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   125
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   126
lemma union_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   127
  shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   128
  unfolding Un_def Collect_eqvt2 disj_eqvt mem_eqvt by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   129
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   130
lemma inter_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   131
  shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   132
  unfolding Int_def Collect_eqvt2 conj_eqvt mem_eqvt by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   133
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   134
lemma Diff_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   135
  fixes A B :: "'a::pt set"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   136
  shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   137
  unfolding set_diff_eq Collect_eqvt2 conj_eqvt Not_eqvt mem_eqvt by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   138
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   139
lemma Compl_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   140
  fixes A :: "'a::pt set"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   141
  shows "p \<bullet> (- A) = - (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   142
  unfolding Compl_eq_Diff_UNIV Diff_eqvt UNIV_eqvt ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   143
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   144
lemma insert_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   145
  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   146
  unfolding permute_set_eq_image image_insert ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   147
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   148
lemma vimage_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   149
  shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   150
  unfolding vimage_def permute_fun_def [where f=f]
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   151
  unfolding Collect_eqvt2 mem_eqvt ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   152
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   153
lemma image_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   154
  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   155
  unfolding permute_set_eq_image
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   156
  unfolding permute_fun_def [where f=f]
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   157
  by (simp add: image_image)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   158
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   159
lemma finite_permute_iff:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   160
  shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   161
  unfolding permute_set_eq_vimage
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   162
  using bij_permute by (rule finite_vimage_iff)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   163
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   164
lemma finite_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   165
  shows "p \<bullet> finite A = finite (p \<bullet> A)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   166
  unfolding finite_permute_iff permute_bool_def ..
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   167
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   168
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   169
section {* List Operations *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   170
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   171
lemma append_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   172
  shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   173
  by (induct xs) auto
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   174
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   175
lemma supp_append:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   176
  shows "supp (xs @ ys) = supp xs \<union> supp ys"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   177
  by (induct xs) (auto simp add: supp_Nil supp_Cons)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   178
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   179
lemma fresh_append:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   180
  shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   181
  by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   182
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   183
lemma rev_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   184
  shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   185
  by (induct xs) (simp_all add: append_eqvt)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   186
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   187
lemma supp_rev:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   188
  shows "supp (rev xs) = supp xs"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   189
  by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   190
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   191
lemma fresh_rev:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   192
  shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   193
  by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   194
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   195
lemma set_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   196
  shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   197
  by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   198
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   199
(* needs finite support premise
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   200
lemma supp_set:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   201
  fixes x :: "'a::pt"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   202
  shows "supp (set xs) = supp xs"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   203
*)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   204
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   205
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   206
section {* Product Operations *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   207
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   208
lemma fst_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   209
  "p \<bullet> (fst x) = fst (p \<bullet> x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   210
 by (cases x) simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   211
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   212
lemma snd_eqvt:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   213
  "p \<bullet> (snd x) = snd (p \<bullet> x)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   214
 by (cases x) simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   215
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   216
section {* Units *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   217
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   218
lemma supp_unit:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   219
  shows "supp () = {}"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   220
  by (simp add: supp_def)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   221
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   222
lemma fresh_unit:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   223
  shows "a \<sharp> ()"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   224
  by (simp add: fresh_def supp_unit)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   225
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
   226
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>
parents: 1774
diff changeset
   227
  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>
parents: 1774
diff changeset
   228
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>
parents: 1774
diff changeset
   229
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>
parents: 1774
diff changeset
   230
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>
parents: 1774
diff changeset
   231
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>
parents: 1774
diff changeset
   232
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   233
section {* Equivariance automation *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   234
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   235
text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_force} *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   236
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   237
use "nominal_thmdecls.ML"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   238
setup "Nominal_ThmDecls.setup"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   239
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   240
lemmas [eqvt] = 
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   241
  (* connectives *)
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   242
  eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
   243
  True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   244
  imp_eqvt [folded induct_implies_def]
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   245
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   246
  (* nominal *)
1326
4bc9278a808d weird eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1315
diff changeset
   247
  supp_eqvt fresh_eqvt
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   248
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   249
  (* datatypes *)
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
   250
  permute_prod.simps append_eqvt rev_eqvt set_eqvt
1423
d59f851926c5 finally the proof that new and old alpha agree
Christian Urban <urbanc@in.tum.de>
parents: 1331
diff changeset
   251
  fst_eqvt snd_eqvt Pair_eqvt
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   252
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   253
  (* sets *)
1087
bb7f4457091a moved some lemmas to Nominal; updated all files
Christian Urban <urbanc@in.tum.de>
parents: 1079
diff changeset
   254
  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
1315
43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   255
  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt
43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   256
1331
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1326
diff changeset
   257
  atom_eqvt add_perm_eqvt
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   258
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
   259
lemmas [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>
parents: 1774
diff changeset
   260
  permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) 
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
   261
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   262
thm eqvts
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   263
thm eqvts_raw
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   264
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   265
text {* helper lemmas for the eqvt_tac *}
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   266
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   267
definition
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   268
  "unpermute p = permute (- p)"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   269
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   270
lemma eqvt_apply:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   271
  fixes f :: "'a::pt \<Rightarrow> 'b::pt" 
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   272
  and x :: "'a::pt"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   273
  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
   274
  unfolding permute_fun_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   275
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   276
lemma eqvt_lambda:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   277
  fixes f :: "'a::pt \<Rightarrow> 'b::pt"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   278
  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
   279
  unfolding permute_fun_def unpermute_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   280
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   281
lemma eqvt_bound:
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   282
  shows "p \<bullet> unpermute p x \<equiv> x"
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   283
  unfolding unpermute_def by simp
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   284
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   285
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
   286
setup Nominal_Permeq.setup
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   287
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
   288
method_setup perm_simp =
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
   289
 {* Attrib.thms >> 
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
   290
    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["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
   291
 {* 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>
parents: 1774
diff changeset
   292
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
   293
method_setup perm_strict_simp =
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
   294
 {* Attrib.thms >> 
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
   295
    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *}
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
   296
 {* 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>
parents: 1800
diff changeset
   297
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
   298
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>
parents: 1774
diff changeset
   299
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
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
   301
  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
   302
  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
   303
apply(perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   304
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   305
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
   306
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
   307
  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
   308
  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
   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
  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
   314
  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
   315
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
   316
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
   317
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
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
   319
  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
   320
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
   321
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
   322
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
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
   324
  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
   325
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
   326
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
   327
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
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
   329
  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
   330
apply (perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   331
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   332
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
   333
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
   334
  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
   335
apply (perm_simp)
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   336
oops
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   337
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   338
lemma 
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   339
  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
   340
  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
   341
  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
   342
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
   343
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
   344
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
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
   346
  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
   347
  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
   348
  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
   349
apply(perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   350
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   351
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
   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>
parents: 1774
diff changeset
   353
  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
   354
  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
   355
apply (perm_simp)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   356
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   357
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
   358
lemma 
78fdc6b36a1c changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
   359
  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
   360
  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
   361
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
   362
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
   363
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
   364
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
   365
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
   366
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>
parents: 1774
diff changeset
   367
lemma "p \<bullet> (THE x. P 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
   368
apply(perm_simp)
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
   369
(* apply(perm_strict_simp) *)
1062
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   370
oops
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   371
dfea9e739231 rollback of the test
Christian Urban <urbanc@in.tum.de>
parents: 1061
diff changeset
   372
1315
43d6e3730353 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   373
end