Quot/Nominal/Nominal2_Atoms.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 26 Jan 2010 20:07:50 +0100
changeset 947 fa810f01f7b5
child 1061 8de99358f309
permissions -rw-r--r--
added an LamEx example together with the new nominal infrastructure
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
947
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
(*  Title:      Nominal2_Atoms
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
    Authors:    Brian Huffman, Christian Urban
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
    Definitions for concrete atom types. 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
*)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
theory Nominal2_Atoms
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
imports Nominal2_Base
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
uses ("atom_decl.ML")
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
begin
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
section {* Concrete atom types *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
text {*
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  Class @{text at_base} allows types containing multiple sorts of atoms.
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
  Class @{text at} only allows types with a single sort.
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
*}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
class at_base = pt +
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
  fixes atom :: "'a \<Rightarrow> atom"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
  assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
  assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
class at = at_base +
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
  assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
instance at < at_base ..
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
lemma supp_at_base: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
  fixes a::"'a::at_base"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
  shows "supp a = {atom a}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
  by (simp add: supp_atom [symmetric] supp_def atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
lemma fresh_at: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
  shows "a \<sharp> b \<longleftrightarrow> a \<noteq> atom b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
  unfolding fresh_def by (simp add: supp_at_base)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
instance at_base < fs
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
proof qed (simp add: supp_at_base)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
lemma at_base_infinite [simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
  shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U")
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
proof
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
  obtain a :: 'a where "True" by auto
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    45
  assume "finite ?U"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    46
  hence "finite (atom ` ?U)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    47
    by (rule finite_imageI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    48
  then obtain b where b: "b \<notin> atom ` ?U" "sort_of b = sort_of (atom a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
    by (rule obtain_atom)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    50
  from b(2) have "b = atom ((atom a \<rightleftharpoons> b) \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    51
    unfolding atom_eqvt [symmetric]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    52
    by (simp add: swap_atom)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
  hence "b \<in> atom ` ?U" by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
  with b(1) show "False" by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
lemma swap_at_base_simps [simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  fixes x y::"'a::at_base"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
  shows "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> x = y"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
  and   "sort_of (atom x) = sort_of (atom y) \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> y = x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  and   "atom x \<noteq> a \<Longrightarrow> atom x \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
  unfolding atom_eq_iff [symmetric]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    63
  unfolding atom_eqvt [symmetric]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
  by simp_all
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
lemma obtain_at_base:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
  assumes X: "finite X"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
  obtains a::"'a::at_base" where "atom a \<notin> X"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
proof -
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    70
  have "inj (atom :: 'a \<Rightarrow> atom)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
    by (simp add: inj_on_def)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
  with X have "finite (atom -` X :: 'a set)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
    by (rule finite_vimageI)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
  with at_base_infinite have "atom -` X \<noteq> (UNIV :: 'a set)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
    by auto
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
  then obtain a :: 'a where "atom a \<notin> X"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
    by auto
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
  thus ?thesis ..
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
section {* A swapping operation for concrete atoms *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
  
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
definition
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    85
  flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
where
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
  "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
  unfolding flip_def by (rule swap_self)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    93
  unfolding flip_def by (rule swap_commute)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    94
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    95
lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    96
  unfolding flip_def by (rule minus_swap)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    97
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    98
lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    99
  unfolding flip_def by (rule swap_cancel)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   100
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   101
lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   102
  unfolding permute_plus [symmetric] add_flip_cancel by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   103
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   104
lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   105
  by (simp add: flip_commute)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   106
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   107
lemma flip_eqvt: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
  fixes a b c::"'a::at_base"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   109
  shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
  unfolding flip_def
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   111
  by (simp add: swap_eqvt atom_eqvt)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   113
lemma flip_at_base_simps [simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
  shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   115
  and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
  and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
  and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
  unfolding flip_def
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
  unfolding atom_eq_iff [symmetric]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
  unfolding atom_eqvt [symmetric]
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
  by simp_all
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   123
text {* the following two lemmas do not hold for at_base, 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   124
  only for single sort atoms from at *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   125
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   126
lemma permute_flip_at:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   127
  fixes a b c::"'a::at"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
  unfolding flip_def
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   130
  apply (rule atom_eq_iff [THEN iffD1])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   131
  apply (subst atom_eqvt [symmetric])
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
  apply (simp add: swap_atom)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   133
  done
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
lemma flip_at_simps [simp]:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
  fixes a b::"'a::at"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
  shows "(a \<leftrightarrow> b) \<bullet> a = b" 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
  and   "(a \<leftrightarrow> b) \<bullet> b = a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139
  unfolding permute_flip_at by simp_all
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   140
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   141
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   142
subsection {* Syntax for coercing at-elements to the atom-type *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   143
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   144
syntax
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   145
  "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   146
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   147
translations
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   148
  "_atom_constrain a t" => "atom (_constrain a t)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   149
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   150
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   151
subsection {* A lemma for proving instances of class @{text at}. *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   152
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   153
setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   154
setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   155
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   156
text {*
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   157
  New atom types are defined as subtypes of @{typ atom}.
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   158
*}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   159
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   160
lemma exists_eq_sort: 
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   161
  shows "\<exists>a. a \<in> {a. sort_of a = s}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   162
  by (rule_tac x="Atom s 0" in exI, simp)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   163
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   164
lemma at_base_class:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   165
  fixes s :: atom_sort
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   166
  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   167
  assumes type: "type_definition Rep Abs {a. P (sort_of a)}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   168
  assumes atom_def: "\<And>a. atom a = Rep a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   169
  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   170
  shows "OFCLASS('a, at_base_class)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   171
proof
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   172
  interpret type_definition Rep Abs "{a. P (sort_of a)}" by (rule type)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   173
  have sort_of_Rep: "\<And>a. P (sort_of (Rep a))" using Rep by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   174
  fix a b :: 'a and p p1 p2 :: perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   175
  show "0 \<bullet> a = a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   176
    unfolding permute_def by (simp add: Rep_inverse)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   177
  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   178
    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   179
  show "atom a = atom b \<longleftrightarrow> a = b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   180
    unfolding atom_def by (simp add: Rep_inject)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   181
  show "p \<bullet> atom a = atom (p \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   182
    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   183
qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   184
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   185
lemma at_class:
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   186
  fixes s :: atom_sort
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   187
  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   188
  assumes type: "type_definition Rep Abs {a. sort_of a = s}"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   189
  assumes atom_def: "\<And>a. atom a = Rep a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   190
  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   191
  shows "OFCLASS('a, at_class)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   192
proof
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   193
  interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   194
  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by simp
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   195
  fix a b :: 'a and p p1 p2 :: perm
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   196
  show "0 \<bullet> a = a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   197
    unfolding permute_def by (simp add: Rep_inverse)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   198
  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   199
    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   200
  show "sort_of (atom a) = sort_of (atom b)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   201
    unfolding atom_def by (simp add: sort_of_Rep)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   202
  show "atom a = atom b \<longleftrightarrow> a = b"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   203
    unfolding atom_def by (simp add: Rep_inject)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   204
  show "p \<bullet> atom a = atom (p \<bullet> a)"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   205
    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   206
qed
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   207
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   208
setup {* Sign.add_const_constraint
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   209
  (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   210
setup {* Sign.add_const_constraint
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   211
  (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   212
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   213
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   214
section {* Automation for creating concrete atom types *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   215
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   216
text {* at the moment only single-sort concrete atoms are supported *}
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   217
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   218
use "atom_decl.ML"
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   219
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   220
fa810f01f7b5 added an LamEx example together with the new nominal infrastructure
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   221
end