1062
+ − 1
(* Title: Nominal2_Atoms
+ − 2
Authors: Brian Huffman, Christian Urban
+ − 3
+ − 4
Definitions for concrete atom types.
+ − 5
*)
+ − 6
theory Nominal2_Atoms
+ − 7
imports Nominal2_Base
1933
9eab1dfc14d2
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 8
Nominal2_Eqvt
1079
+ − 9
uses ("nominal_atoms.ML")
1062
+ − 10
begin
+ − 11
1972
+ − 12
section {* Infrastructure for concrete atom types *}
1933
9eab1dfc14d2
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 13
1941
+ − 14
1062
+ − 15
section {* A swapping operation for concrete atoms *}
+ − 16
+ − 17
definition
+ − 18
flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
+ − 19
where
+ − 20
"(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
+ − 21
+ − 22
lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
+ − 23
unfolding flip_def by (rule swap_self)
+ − 24
+ − 25
lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
+ − 26
unfolding flip_def by (rule swap_commute)
+ − 27
+ − 28
lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
+ − 29
unfolding flip_def by (rule minus_swap)
+ − 30
+ − 31
lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
+ − 32
unfolding flip_def by (rule swap_cancel)
+ − 33
+ − 34
lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
+ − 35
unfolding permute_plus [symmetric] add_flip_cancel by simp
+ − 36
+ − 37
lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
+ − 38
by (simp add: flip_commute)
+ − 39
2129
+ − 40
lemma flip_eqvt[eqvt]:
1062
+ − 41
fixes a b c::"'a::at_base"
+ − 42
shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
+ − 43
unfolding flip_def
+ − 44
by (simp add: swap_eqvt atom_eqvt)
+ − 45
+ − 46
lemma flip_at_base_simps [simp]:
+ − 47
shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
+ − 48
and "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
+ − 49
and "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
+ − 50
and "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
+ − 51
unfolding flip_def
+ − 52
unfolding atom_eq_iff [symmetric]
+ − 53
unfolding atom_eqvt [symmetric]
+ − 54
by simp_all
+ − 55
+ − 56
text {* the following two lemmas do not hold for at_base,
+ − 57
only for single sort atoms from at *}
+ − 58
+ − 59
lemma permute_flip_at:
+ − 60
fixes a b c::"'a::at"
+ − 61
shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
+ − 62
unfolding flip_def
+ − 63
apply (rule atom_eq_iff [THEN iffD1])
+ − 64
apply (subst atom_eqvt [symmetric])
+ − 65
apply (simp add: swap_atom)
+ − 66
done
+ − 67
+ − 68
lemma flip_at_simps [simp]:
+ − 69
fixes a b::"'a::at"
+ − 70
shows "(a \<leftrightarrow> b) \<bullet> a = b"
+ − 71
and "(a \<leftrightarrow> b) \<bullet> b = a"
+ − 72
unfolding permute_flip_at by simp_all
+ − 73
1499
+ − 74
lemma flip_fresh_fresh:
+ − 75
fixes a b::"'a::at_base"
+ − 76
assumes "atom a \<sharp> x" "atom b \<sharp> x"
+ − 77
shows "(a \<leftrightarrow> b) \<bullet> x = x"
+ − 78
using assms
+ − 79
by (simp add: flip_def swap_fresh_fresh)
1062
+ − 80
+ − 81
subsection {* Syntax for coercing at-elements to the atom-type *}
+ − 82
+ − 83
syntax
+ − 84
"_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
+ − 85
+ − 86
translations
1569
+ − 87
"_atom_constrain a t" => "CONST atom (_constrain a t)"
+ − 88
1062
+ − 89
+ − 90
subsection {* A lemma for proving instances of class @{text at}. *}
+ − 91
+ − 92
setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
+ − 93
setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
+ − 94
+ − 95
text {*
+ − 96
New atom types are defined as subtypes of @{typ atom}.
+ − 97
*}
+ − 98
1079
+ − 99
lemma exists_eq_simple_sort:
1062
+ − 100
shows "\<exists>a. a \<in> {a. sort_of a = s}"
+ − 101
by (rule_tac x="Atom s 0" in exI, simp)
+ − 102
1079
+ − 103
lemma exists_eq_sort:
+ − 104
shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
+ − 105
by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
+ − 106
1062
+ − 107
lemma at_base_class:
1079
+ − 108
fixes sort_fun :: "'b \<Rightarrow>atom_sort"
1062
+ − 109
fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
1079
+ − 110
assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
1062
+ − 111
assumes atom_def: "\<And>a. atom a = Rep a"
+ − 112
assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ − 113
shows "OFCLASS('a, at_base_class)"
+ − 114
proof
1079
+ − 115
interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
+ − 116
have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
1062
+ − 117
fix a b :: 'a and p p1 p2 :: perm
+ − 118
show "0 \<bullet> a = a"
+ − 119
unfolding permute_def by (simp add: Rep_inverse)
+ − 120
show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ − 121
unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ − 122
show "atom a = atom b \<longleftrightarrow> a = b"
+ − 123
unfolding atom_def by (simp add: Rep_inject)
+ − 124
show "p \<bullet> atom a = atom (p \<bullet> a)"
+ − 125
unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+ − 126
qed
+ − 127
1079
+ − 128
(*
+ − 129
lemma at_class:
+ − 130
fixes s :: atom_sort
+ − 131
fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ − 132
assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
+ − 133
assumes atom_def: "\<And>a. atom a = Rep a"
+ − 134
assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ − 135
shows "OFCLASS('a, at_class)"
+ − 136
proof
+ − 137
interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
+ − 138
have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+ − 139
fix a b :: 'a and p p1 p2 :: perm
+ − 140
show "0 \<bullet> a = a"
+ − 141
unfolding permute_def by (simp add: Rep_inverse)
+ − 142
show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ − 143
unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ − 144
show "sort_of (atom a) = sort_of (atom b)"
+ − 145
unfolding atom_def by (simp add: sort_of_Rep)
+ − 146
show "atom a = atom b \<longleftrightarrow> a = b"
+ − 147
unfolding atom_def by (simp add: Rep_inject)
+ − 148
show "p \<bullet> atom a = atom (p \<bullet> a)"
+ − 149
unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+ − 150
qed
+ − 151
*)
+ − 152
1062
+ − 153
lemma at_class:
+ − 154
fixes s :: atom_sort
+ − 155
fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+ − 156
assumes type: "type_definition Rep Abs {a. sort_of a = s}"
+ − 157
assumes atom_def: "\<And>a. atom a = Rep a"
+ − 158
assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+ − 159
shows "OFCLASS('a, at_class)"
+ − 160
proof
+ − 161
interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
1079
+ − 162
have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
1062
+ − 163
fix a b :: 'a and p p1 p2 :: perm
+ − 164
show "0 \<bullet> a = a"
+ − 165
unfolding permute_def by (simp add: Rep_inverse)
+ − 166
show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+ − 167
unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+ − 168
show "sort_of (atom a) = sort_of (atom b)"
+ − 169
unfolding atom_def by (simp add: sort_of_Rep)
+ − 170
show "atom a = atom b \<longleftrightarrow> a = b"
+ − 171
unfolding atom_def by (simp add: Rep_inject)
+ − 172
show "p \<bullet> atom a = atom (p \<bullet> a)"
+ − 173
unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+ − 174
qed
+ − 175
+ − 176
setup {* Sign.add_const_constraint
+ − 177
(@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
+ − 178
setup {* Sign.add_const_constraint
+ − 179
(@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
+ − 180
+ − 181
section {* Automation for creating concrete atom types *}
+ − 182
+ − 183
text {* at the moment only single-sort concrete atoms are supported *}
+ − 184
1079
+ − 185
use "nominal_atoms.ML"
+ − 186
+ − 187
1062
+ − 188
end