author | Christian Urban <urbanc@in.tum.de> |
Wed, 16 Mar 2011 21:07:50 +0100 | |
changeset 2746 | 6aa98a113e6c |
parent 2744 | 56b8d977d1c0 |
child 2747 | a5da7b6aff8f |
permissions | -rw-r--r-- |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(*<*) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Paper |
2568
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2523
diff
changeset
|
3 |
imports "../Nominal/Nominal2_Base" |
8193bbaa07fe
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents:
2523
diff
changeset
|
4 |
"../Nominal/Atoms" |
2734
eee5deb35aa8
included old test cases for perm_simp into ROOT.ML file
Christian Urban <urbanc@in.tum.de>
parents:
2568
diff
changeset
|
5 |
"../Nominal/Nominal2_Abs" |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
"LaTeXsugar" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
begin |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
|
2742 | 9 |
abbreviation |
10 |
UNIV_atom ("\<allatoms>") |
|
11 |
where |
|
12 |
"UNIV_atom \<equiv> UNIV::atom set" |
|
13 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
notation (latex output) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
sort_of ("sort _" [1000] 100) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
Abs_perm ("_") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
Rep_perm ("_") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
swap ("'(_ _')" [1000, 1000] 1000) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
fresh ("_ # _" [51, 51] 50) and |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
20 |
fresh_star ("_ #\<^sup>* _" [51, 51] 50) and |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
Cons ("_::_" [78,77] 73) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
supp ("supp _" [78] 73) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
uminus ("-_" [78] 73) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
atom ("|_|") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
If ("if _ then _ else _" 10) and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
Rep_name ("\<lfloor>_\<rfloor>") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
Abs_name ("\<lceil>_\<rceil>") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
Rep_var ("\<lfloor>_\<rfloor>") and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
Abs_var ("\<lceil>_\<rceil>") and |
2742 | 30 |
sort_of_ty ("sort'_ty _") |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
(* BH: uncomment if you really prefer the dot notation |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
syntax (latex output) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
"_Collect" :: "pttrn => bool => 'a set" ("(1{_ . _})") |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
*) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
(* sort is used in Lists for sorting *) |
2005
233bb805a4df
replaced hide by the new hide_const
Christian Urban <urbanc@in.tum.de>
parents:
1809
diff
changeset
|
38 |
hide_const sort |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
abbreviation |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
"sort \<equiv> sort_of" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
|
2742 | 43 |
lemma infinite_collect: |
44 |
assumes "\<forall>x \<in> S. P x" "infinite S" |
|
45 |
shows "infinite {x \<in> S. P x}" |
|
46 |
using assms |
|
47 |
apply(subgoal_tac "infinite {x. x \<in> S}") |
|
48 |
apply(simp only: Inf_many_def[symmetric]) |
|
49 |
apply(erule INFM_mono) |
|
50 |
apply(auto) |
|
51 |
done |
|
52 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
(*>*) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
section {* Introduction *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
text {* |
2521
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
59 |
Nominal Isabelle provides a proving infratructure for convenient reasoning |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
60 |
about syntax involving binders, such as lambda terms or type schemes: |
2466
47c840599a6b
cleaned a bit various thy-files in Nominal-General
Christian Urban <urbanc@in.tum.de>
parents:
2382
diff
changeset
|
61 |
|
2521
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
62 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
2742 | 63 |
@{text "\<lambda>x. t \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. \<tau>"} |
2521
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
64 |
\end{isabelle} |
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
65 |
|
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
66 |
\noindent |
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
67 |
At its core Nominal Isabelle is based on the nominal logic work by Pitts at |
2736 | 68 |
al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a |
2521
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
69 |
sort-respecting permutation operation defined over a countably infinite |
2746
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
70 |
collection of sorted atoms. The aim of this paper is to describe how to |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
71 |
adapt this work so that it can be implemented in a theorem prover based |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
72 |
on Higher-Order Logic (HOL). For this we present the definition we made |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
73 |
in the implementation and also review many proofs. There are a two main |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
74 |
design choices to be made. One is |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
75 |
how to represent sorted atoms. We opt here for a single unified atom type to |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
76 |
represent atoms of different sorts. The other is how to present sort-respecting |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
77 |
permutations. For them we use the standard technique of |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
78 |
HOL-formalisations of introducing an appropriate substype of functions from |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
79 |
atoms to atoms. |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
80 |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
81 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
82 |
The nominal logic work has been the starting point for a number of proving |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
83 |
infrastructures, most notable by Norrish \cite{norrish04} in HOL4, by |
2742 | 84 |
Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and the work by Urban |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
85 |
and Berghofer in Isabelle/HOL \cite{Urban08}. Its key attraction is a very |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
86 |
general notion, called \emph{support}, for the `set of free variables, or |
2742 | 87 |
atoms, of an object' that applies not just to lambda terms and type schemes, |
88 |
but also to sets, products, lists, booleans and even functions. The notion of support |
|
89 |
is derived from the permutation operation defined over the |
|
90 |
hierarchy of types. This |
|
91 |
permutation operation, written @{text "_ \<bullet> _"}, has proved to be much more |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
92 |
convenient for reasoning about syntax, in comparison to, say, arbitrary |
2742 | 93 |
renaming substitutions of atoms. One reason is that permutations are |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
94 |
bijective renamings of atoms and thus they can be easily `undone'---namely |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
95 |
by applying the inverse permutation. A corresponding inverse substitution |
2742 | 96 |
might not always exist, since renaming substitutions are in general only injective. |
97 |
Another reason is that permutations preserve many constructions when reasoning about syntax. |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
98 |
For example, suppose a typing context @{text "\<Gamma>"} of the form |
2521
e7cc033f72c7
tiny work on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2470
diff
changeset
|
99 |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
100 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
101 |
@{text "x\<^isub>1:\<tau>\<^isub>1, \<dots>, x\<^isub>n:\<tau>\<^isub>n"} |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
102 |
\end{isabelle} |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
103 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
104 |
\noindent |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
105 |
is said to be \emph{valid} provided none of its variables, or atoms, @{text "x\<^isub>i"} |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
106 |
occur twice. Then validity of typing contexts is preserved under |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
107 |
permutations in the sense that if @{text \<Gamma>} is valid then so is \mbox{@{text "\<pi> \<bullet> \<Gamma>"}} for |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
108 |
all permutations @{text "\<pi>"}. Again, this is \emph{not} the case for arbitrary |
2742 | 109 |
renaming substitutions, as they might identify some of the @{text "x\<^isub>i"} in @{text \<Gamma>}. |
110 |
||
111 |
Permutations also behave uniformly with respect to HOL's logic connectives. |
|
112 |
Applying a permutation to a formula gives, for example |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
|
2742 | 114 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
115 |
\begin{tabular}{@ {}lcl} |
|
116 |
@{term "\<pi> \<bullet> (A \<and> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<and> (\<pi> \<bullet> B)"}\\ |
|
117 |
@{term "\<pi> \<bullet> (A \<longrightarrow> B)"} & if and only if & @{text "(\<pi> \<bullet> A) \<longrightarrow> (\<pi> \<bullet> B)"}\\ |
|
118 |
\end{tabular} |
|
119 |
\end{isabelle} |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
120 |
|
2742 | 121 |
\noindent |
122 |
This uniform behaviour can also be extended to quantifiers and functions. |
|
123 |
Because of these good properties of permutations, we are able to automate |
|
124 |
reasoning to do with \emph{equivariance}. By equivariance we mean the property |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
125 |
that every permutation leaves a function unchanged, that is @{term "\<pi> \<bullet> f = f"} |
2742 | 126 |
for all @{text "\<pi>"}. This will often simplify arguments involving support |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
127 |
of functions, since if they are equivariant then they have empty support---or |
2742 | 128 |
`no free atoms'. |
129 |
||
130 |
There are a number of subtle differences between the nominal logic work by |
|
131 |
Pitts and the formalisation we will present in this paper. One difference |
|
132 |
is that our |
|
133 |
formalisation is compatible with HOL, in the sense that we only extend |
|
134 |
HOL by some definitions, withouth the introduction of any new axioms. |
|
135 |
The reason why the original nominal logic work is |
|
136 |
incompatible with HOL has to do with the way how the finite support property |
|
137 |
is enforced: FM-set theory is defined in \cite{Pitts01b} so that every set |
|
138 |
in the FM-set-universe has finite support. In nominal logic \cite{Pitts03}, |
|
139 |
the axioms (E3) and (E4) imply that every function symbol and proposition |
|
140 |
has finite support. However, there are notions in HOL that do \emph{not} |
|
141 |
have finite support (we will give some examples). In our formalisation, we |
|
142 |
will avoid the incompatibility of the original nominal logic work by not a |
|
143 |
priory restricting our discourse to only finitely supported entities, rather |
|
144 |
we will explicitly assume this property whenever it is needed in proofs. One |
|
145 |
consequence is that we state our basic definitions not in terms of nominal |
|
146 |
sets (as done for example in \cite{Pitts06}), but in terms of the weaker |
|
147 |
notion of permutation types---essentially sets equipped with a ``sensible'' |
|
148 |
notion of permutation operation. |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
149 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
150 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
151 |
|
2742 | 152 |
In the nominal logic woworkrk, the `new quantifier' plays a prominent role. |
153 |
$\new$ |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
154 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
155 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
156 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
157 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
158 |
Two binders |
2746
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
159 |
|
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
160 |
A preliminary version |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
161 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
162 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
163 |
section {* Sorted Atoms and Sort-Respecting Permutations *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
164 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
text {* |
2742 | 166 |
The two most basic notions in the nominal logic work are a countably |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
167 |
infinite collection of sorted atoms and sort-respecting permutations of atoms. |
2746
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
168 |
The atoms are used for representing variable names |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
169 |
that might be bound or free. Multiple sorts are necessary for being able to |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
170 |
represent different kinds of variables. For example, in the language Mini-ML |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
171 |
there are bound term variables in lambda abstractions and bound type variables in |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
172 |
type schemes. In order to be able to separate them, each kind of variables needs to be |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
173 |
represented by a different sort of atoms. |
6aa98a113e6c
a lit bit more on the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2744
diff
changeset
|
174 |
|
2742 | 175 |
The existing nominal logic work usually leaves implicit |
176 |
the sorting information for atoms and as far as we know leaves out a |
|
177 |
description of how sorts are represented. In our formalisation, we |
|
178 |
therefore have to make a design decision about how to implement sorted atoms |
|
179 |
and sort-respecting permutations. One possibility, which we described in |
|
180 |
\cite{Urban08}, is to have separate types for the different sorts of |
|
181 |
atoms. However, we found that this does not blend well with type-classes in |
|
182 |
Isabelle/HOL (see Section~\ref{related} about related work). Therefore we use here a |
|
183 |
single unified atom type to represent atoms of different sorts. A basic |
|
184 |
requirement is that there must be a countably infinite number of atoms of |
|
185 |
each sort. This can be implemented as the datatype |
|
2736 | 186 |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
189 |
datatype atom\<iota> = Atom\<iota> string nat |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
190 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
191 |
text {* |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
192 |
\noindent |
2522
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
193 |
whereby the string argument specifies the sort of the atom.\footnote{A |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
194 |
similar design choice was made by Gunter et al \cite{GunterOsbornPopescu09} |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
195 |
for their variables.} The use of type \emph{string} for sorts is merely for |
2742 | 196 |
convenience; any countably infinite type would work as well. |
197 |
The set of all atoms we shall write as @{term "UNIV::atom set"}. |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
198 |
We have two auxiliary functions for atoms, namely @{text sort} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
199 |
and @{const nat_of} which are defined as |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
200 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
201 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
2742 | 202 |
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
203 |
@{thm (lhs) sort_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) sort_of.simps[no_vars]}\\ |
|
204 |
@{thm (lhs) nat_of.simps[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) nat_of.simps[no_vars]} |
|
205 |
\end{tabular}\hfill\numbered{sortnatof} |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
206 |
\end{isabelle} |
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
207 |
|
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
208 |
\noindent |
2742 | 209 |
We clearly have for every finite set @{text S} |
2522
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
210 |
of atoms and every sort @{text s} the property: |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
211 |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
212 |
\begin{proposition}\label{choosefresh}\mbox{}\\ |
2522
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
213 |
@{text "For a finite set of atoms S, there exists an atom a such that |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
214 |
sort a = s and a \<notin> S"}. |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
215 |
\end{proposition} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
216 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
217 |
For implementing sort-respecting permutations, we use functions of type @{typ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
218 |
"atom => atom"} that @{text "i)"} are bijective; @{text "ii)"} are the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
219 |
identity on all atoms, except a finite number of them; and @{text "iii)"} map |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
220 |
each atom to one of the same sort. These properties can be conveniently stated |
2742 | 221 |
in Isabelle/HOL for a function @{text \<pi>} as follows: |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
222 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
223 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
224 |
\begin{tabular}{r@ {\hspace{4mm}}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
225 |
i) & @{term "bij \<pi>"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
226 |
ii) & @{term "finite {a. \<pi> a \<noteq> a}"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
227 |
iii) & @{term "\<forall>a. sort (\<pi> a) = sort a"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
228 |
\end{tabular}\hfill\numbered{permtype} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
229 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
230 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
231 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
232 |
Like all HOL-based theorem provers, Isabelle/HOL allows us to |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
233 |
introduce a new type @{typ perm} that includes just those functions |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
234 |
satisfying all three properties. For example the identity function, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
235 |
written @{term id}, is included in @{typ perm}. Also function composition, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
236 |
written \mbox{@{text "_ \<circ> _"}}, and function inversion, given by Isabelle/HOL's |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
237 |
inverse operator and written \mbox{@{text "inv _"}}, preserve the properties |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
238 |
@{text "i"}-@{text "iii"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
239 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
240 |
However, a moment of thought is needed about how to construct non-trivial |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
241 |
permutations. In the nominal logic work it turned out to be most convenient |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
242 |
to work with swappings, written @{text "(a b)"}. In our setting the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
243 |
type of swappings must be |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
244 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
245 |
@{text [display,indent=10] "(_ _) :: atom \<Rightarrow> atom \<Rightarrow> perm"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
246 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
247 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
248 |
but since permutations are required to respect sorts, we must carefully |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
249 |
consider what happens if a user states a swapping of atoms with different |
2742 | 250 |
sorts. The following definition\footnote{To increase legibility, we omit |
251 |
here and in what follows the @{term Rep_perm} and @{term "Abs_perm"} |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
252 |
wrappers that are needed in our implementation in Isabelle/HOL since we defined permutation |
2742 | 253 |
not to be the full function space, but only those functions of type @{typ |
254 |
perm} satisfying properties @{text i}-@{text "iii"} in \eqref{permtype}.} |
|
255 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
256 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
257 |
@{text [display,indent=10] "(a b) \<equiv> \<lambda>c. if a = c then b else (if b = c then a else c)"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
258 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
259 |
\noindent |
2742 | 260 |
does not work in general, because @{text a} and @{text b} may have different |
261 |
sorts---in which case the function would violate property @{text iii} in \eqref{permtype}. We |
|
262 |
could make the definition of swappings partial by adding the precondition |
|
263 |
@{term "sort a = sort b"}, which would mean that in case @{text a} and |
|
264 |
@{text b} have different sorts, the value of @{text "(a b)"} is unspecified. |
|
265 |
However, this looked like a cumbersome solution, since sort-related side |
|
266 |
conditions would be required everywhere, even to unfold the definition. It |
|
267 |
turned out to be more convenient to actually allow the user to state |
|
268 |
`ill-sorted' swappings but limit their `damage' by defaulting to the |
|
269 |
identity permutation in the ill-sorted case: |
|
270 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
271 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
272 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
273 |
\begin{tabular}{@ {}rl} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
274 |
@{text "(a b) \<equiv>"} & @{text "if (sort a = sort b)"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
275 |
& \hspace{3mm}@{text "then \<lambda>c. if a = c then b else (if b = c then a else c)"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
276 |
& \hspace{3mm}@{text "else id"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
277 |
\end{tabular}\hfill\numbered{swapdef} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
278 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
279 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
280 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
281 |
This function is bijective, the identity on all atoms except |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
282 |
@{text a} and @{text b}, and sort respecting. Therefore it is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
283 |
a function in @{typ perm}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
284 |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
285 |
One advantage of using functions as a representation for |
2742 | 286 |
permutations is that it is unique. For example the swappings |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
287 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
288 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
289 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
290 |
@{thm swap_commute[no_vars]}\hspace{10mm} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
291 |
@{text "(a a) = id"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
292 |
\end{tabular}\hfill\numbered{swapeqs} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
293 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
294 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
295 |
\noindent |
2742 | 296 |
are \emph{equal}. Another advantage of the function representation is that |
297 |
they form a (non-com\-mu\-ta\-tive) group provided we define |
|
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
298 |
|
2742 | 299 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
300 |
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{10mm}}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
301 |
@{thm (lhs) zero_perm_def[no_vars]} & @{text "\<equiv>"} & @{thm (rhs) zero_perm_def[no_vars]} & |
|
302 |
@{thm (lhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & |
|
303 |
@{thm (rhs) plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2"]}\\ |
|
304 |
@{thm (lhs) uminus_perm_def[where p="\<pi>"]} & @{text "\<equiv>"} & @{thm (rhs) uminus_perm_def[where p="\<pi>"]} & |
|
305 |
@{thm (lhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} & @{text "\<equiv>"} & |
|
306 |
@{thm (rhs) minus_perm_def[where ?p1.0="\<pi>\<^isub>1" and ?p2.0="\<pi>\<^isub>2"]} |
|
307 |
\end{tabular}\hfill\numbered{groupprops} |
|
308 |
\end{isabelle} |
|
309 |
||
310 |
\noindent |
|
311 |
and verify the four simple properties |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
312 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
313 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
314 |
\begin{tabular}{@ {}l} |
2742 | 315 |
@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\ |
316 |
@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm} |
|
317 |
@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
318 |
@{thm group_add_class.left_minus[where a="\<pi>::perm"]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
319 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
320 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
321 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
322 |
\noindent |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
323 |
The technical importance of this fact is that we can rely on |
1809
08e4d3cbcf8c
folded changes from the conference version
Christian Urban <urbanc@in.tum.de>
parents:
1790
diff
changeset
|
324 |
Isabelle/HOL's existing simplification infrastructure for groups, which will |
08e4d3cbcf8c
folded changes from the conference version
Christian Urban <urbanc@in.tum.de>
parents:
1790
diff
changeset
|
325 |
come in handy when we have to do calculations with permutations. |
1790 | 326 |
Note that Isabelle/HOL defies standard conventions of mathematical notation |
327 |
by using additive syntax even for non-commutative groups. Obviously, |
|
328 |
composition of permutations is not commutative in general, because @{text |
|
329 |
"\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
|
330 |
nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
|
331 |
the non-standard notation in order to reuse the existing libraries. |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
332 |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
333 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
334 |
A permutation operation, written @{text "\<pi> \<bullet> x"}, applies a permutation |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
335 |
@{text "\<pi>"} to an object @{text "x"}. This operation has the generic type |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
336 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
337 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
338 |
@{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
339 |
\end{isabelle} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
340 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
341 |
\noindent |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
342 |
and Isabelle/HOL will allow us to give a definition of this operation for |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
343 |
`base' types, such as booleans and atoms, and for type-constructors, such as |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
344 |
products and lists. In order to reason abstractly about this operation, |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
345 |
we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two |
2742 | 346 |
\emph{permutation properties}: |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
347 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
348 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
349 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
350 |
i) & @{thm permute_zero[no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
351 |
ii) & @{thm permute_plus[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2",no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
352 |
\end{tabular}\hfill\numbered{newpermprops} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
353 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
354 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
355 |
\noindent |
2742 | 356 |
The use of type classes allows us to delegate much of the routine resoning involved in |
357 |
determining whether these properties are satisfied to Isabelle/HOL's type system: |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
358 |
we only have to establish that base types satisfy them and that type-constructors |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
359 |
preserve them. Isabelle/HOL will use this information and determine whether |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
360 |
an object @{text x} with a compound type satisfies the permutation properties. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
361 |
For this we define the notion of a \emph{permutation type}: |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
362 |
|
2742 | 363 |
\begin{definition}[Permutation type] |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
364 |
A type @{text "\<beta>"} is a \emph{permutation type} if the permutation |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
365 |
properties in \eqref{newpermprops} are satisfied for every @{text "x"} of type |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
366 |
@{text "\<beta>"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
367 |
\end{definition} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
368 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
369 |
\noindent |
2742 | 370 |
The type classes also allows us to establish generic lemmas involving the |
2740
a9e63abf3feb
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2736
diff
changeset
|
371 |
permutation operation. First, it follows from the laws governing |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
372 |
groups that a permutation and its inverse cancel each other. That is, for any |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
373 |
@{text "x"} of a permutation type: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
374 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
375 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
376 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
377 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
378 |
@{thm permute_minus_cancel(1)[where p="\<pi>", no_vars]}\hspace{10mm} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
379 |
@{thm permute_minus_cancel(2)[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
380 |
\end{tabular}\hfill\numbered{cancel} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
381 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
382 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
383 |
\noindent |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
384 |
Consequently, in a permutation type the permutation operation @{text "\<pi> \<bullet> _"}~~is bijective, |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
385 |
which in turn implies the property |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
386 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
387 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
388 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
389 |
@{thm (lhs) permute_eq_iff[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
390 |
$\;$if and only if$\;$ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
391 |
@{thm (rhs) permute_eq_iff[where p="\<pi>", no_vars]}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
392 |
\end{tabular}\hfill\numbered{permuteequ} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
393 |
\end{isabelle} |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
394 |
|
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
395 |
\noindent |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
396 |
We can also show that the following property holds for any permutation type. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
397 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
398 |
\begin{lemma}\label{permutecompose} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
399 |
Given @{term x} is of permutation type, then |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
400 |
@{text "\<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x) = (\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
401 |
\end{lemma} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
402 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
403 |
\begin{proof} The proof is as follows: |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
404 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
405 |
\begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
406 |
& @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> x"}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
407 |
@{text "="} & @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> (-\<pi>\<^isub>1) \<bullet> \<pi>\<^isub>1 \<bullet> x"} & by \eqref{cancel}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
408 |
@{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2 - \<pi>\<^isub>1) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"} & by {\rm(\ref{newpermprops}.@{text "ii"})}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
409 |
@{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2) \<bullet> (\<pi>\<^isub>1 \<bullet> x)"}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
410 |
\end{tabular}\hfill\qed |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
411 |
\end{isabelle} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
412 |
\end{proof} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
413 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
414 |
\noindent |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
415 |
Next we define the permutation operation for some types: |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
416 |
|
2742 | 417 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
418 |
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
|
419 |
atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\ |
|
420 |
functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\ |
|
421 |
permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\ |
|
422 |
sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
423 |
booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
424 |
lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
425 |
& @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
426 |
products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
427 |
nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
428 |
\end{tabular}\hfill\numbered{permdefs} |
|
429 |
\end{isabelle} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
430 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
431 |
\noindent |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
432 |
and establish: |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
433 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
434 |
\begin{theorem} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
435 |
If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
436 |
then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
437 |
@{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
438 |
@{text bool} and @{text "nat"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
439 |
\end{theorem} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
440 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
441 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
442 |
All statements are by unfolding the definitions of the permutation operations and simple |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
443 |
calculations involving addition and minus. With permutations for example we |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
444 |
have |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
445 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
446 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
447 |
\begin{tabular}[b]{@ {}rcl} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
448 |
@{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
449 |
@{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
450 |
& @{text "="} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - \<pi>\<^isub>2 - \<pi>\<^isub>1"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
451 |
& @{text "="} & @{text "\<pi>\<^isub>1 + (\<pi>\<^isub>2 + \<pi>' - \<pi>\<^isub>2) - \<pi>\<^isub>1"} @{text "\<equiv>"} @{text "\<pi>\<^isub>1 \<bullet> \<pi>\<^isub>2 \<bullet> \<pi>'"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
452 |
\end{tabular}\hfill\qed |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
453 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
454 |
\end{proof} |
2742 | 455 |
|
456 |
\noindent |
|
457 |
Note that the permutation operation for functions is defined so that we have the property |
|
458 |
||
459 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
460 |
@{text "\<pi> \<bullet> (f x) ="} |
|
461 |
@{thm (rhs) permute_fun_app_eq[where p="\<pi>", no_vars]} |
|
462 |
\hfill\numbered{permutefunapp} |
|
463 |
\end{isabelle} |
|
464 |
||
465 |
\noindent |
|
466 |
which is a simple consequence of the definition and the cancellation property in \eqref{cancel}. |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
467 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
468 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
469 |
section {* Equivariance *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
470 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
471 |
text {* |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
472 |
An important notion in the nominal logic work is \emph{equivariance}. |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
473 |
An equivariant function is one that is invariant under the |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
474 |
permutation operation. This notion can be defined |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
475 |
uniformly for all constants in HOL as follows: |
1809
08e4d3cbcf8c
folded changes from the conference version
Christian Urban <urbanc@in.tum.de>
parents:
1790
diff
changeset
|
476 |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
477 |
|
2742 | 478 |
\begin{definition}[Equivariance]\label{equivariance} |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
479 |
A constant @{text c} is \emph{equivariant} if @{term "\<forall>\<pi>. \<pi> \<bullet> c = c"}. |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
480 |
\end{definition} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
481 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
482 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
483 |
There are a number of equivalent formulations for the equivariance property. |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
484 |
For example, assuming @{text c} is of type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
485 |
can also be stated as |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
486 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
487 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
488 |
\begin{tabular}{@ {}l} |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
489 |
@{text "\<forall>\<pi> x. \<pi> \<bullet> (c x) = c (\<pi> \<bullet> x)"} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
490 |
\end{tabular}\hfill\numbered{altequivariance} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
491 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
492 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
493 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
494 |
To see that this formulation implies the definition, we just unfold the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
495 |
definition of the permutation operation for functions and simplify with the equation |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
496 |
and the cancellation property shown in \eqref{cancel}. To see the other direction, we use |
2742 | 497 |
\eqref{permutefunapp}. Similarly for functions with more than one argument. |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
498 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
499 |
Both formulations of equivariance have their advantages and disadvantages: |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
500 |
\eqref{altequivariance} is usually easier to establish, since statements are |
2742 | 501 |
commonly given in a form where functions are fully applied. For example we |
502 |
can easily show that equality is equivariant |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
503 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
504 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
505 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
506 |
@{thm eq_eqvt[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
507 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
508 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
509 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
510 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
511 |
using the permutation operation on booleans and property \eqref{permuteequ}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
512 |
Lemma~\ref{permutecompose} establishes that the permutation operation is |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
513 |
equivariant. The permutation operation for lists and products, shown in \eqref{permdefs}, |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
514 |
state that the constructors for products, @{text "Nil"} and @{text Cons} are equivariant. Also |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
515 |
the booleans @{const True} and @{const False} are equivariant by the permutation |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
516 |
operation. Furthermore |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
517 |
a simple calculation will show that our swapping functions are equivariant, that is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
518 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
519 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
520 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
521 |
@{thm swap_eqvt[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
522 |
\end{tabular}\hfill\numbered{swapeqvt} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
523 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
524 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
525 |
\noindent |
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
526 |
for all @{text a}, @{text b} and @{text \<pi>}. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
527 |
It is also easy to see that the boolean operators, like |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
528 |
@{text "\<and>"}, @{text "\<or>"}, @{text "\<not>"} and @{text "\<longrightarrow>"} are all equivariant. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
529 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
530 |
In contrast, the equation in Definition~\ref{equivariance} together with the permutation |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
531 |
operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
532 |
leads to a simple rewrite system that pushes permutations inside a term until they reach |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
533 |
either function constants or variables. The permutations in front of |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
534 |
equivariant constants disappear. This helps us to establish equivariance |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
535 |
for any notion in HOL that is defined in terms of more primitive notions. To |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
536 |
see this let us define \emph{HOL-terms}. They are given by the grammar |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
537 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
538 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
539 |
@{text "t ::= c | x | t\<^isub>1 t\<^isub>2 | \<lambda>x. t"} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
540 |
\hfill\numbered{holterms} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
541 |
\end{isabelle} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
542 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
543 |
\noindent |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
544 |
whereby @{text c} stands for constants. We assume HOL-terms are fully typed, but |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
545 |
for the sake of greater legibility we leave the typing information implicit. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
546 |
We also assume the usual notions for free and bound variables of a HOL-term. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
547 |
With these definitions in place we can define the notion of an \emph{equivariant} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
548 |
HOL-term |
2742 | 549 |
|
2744
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
550 |
\begin{definition}[Equivariant HOL-term] |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
551 |
A HOL-term is \emph{equivariant}, provided it is closed and composed of applications, |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
552 |
abstractions and equivariant constants only. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
553 |
\end{definition} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
554 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
555 |
\noindent |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
556 |
For equivariant terms we have |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
557 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
558 |
\begin{lemma} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
559 |
For an equivariant HOL-term @{text "t"}, @{term "\<pi> \<bullet> t = t"} for all permutations @{term "\<pi>"}. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
560 |
\end{lemma} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
561 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
562 |
\begin{proof} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
563 |
By induction on the grammar of HOL-terms. The case for variables cannot arise since |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
564 |
equivariant HOL-terms are closed. The case for constants is clear by Definition |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
565 |
\ref{equivariance}. The case for applications is also straightforward since by |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
566 |
\eqref{permutefunapp} we have @{term "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2) = (\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}. |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
567 |
For the case of abstractions we can reason as follows |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
568 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
569 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
570 |
\begin{tabular}[b]{@ {}c@ {\hspace{2mm}}l@ {\hspace{8mm}}l} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
571 |
& @{text "\<pi> \<bullet> (\<lambda>x. t)"}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
572 |
@{text "\<equiv>"} & @{text "\<lambda>y. \<pi> \<bullet> ((\<lambda>x. t) ((-\<pi>) \<bullet> y))"} & by \eqref{permdefs}\\ |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
573 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
574 |
\end{tabular}\hfill\qed |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
575 |
\end{isabelle} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
576 |
\end{proof} |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
577 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
578 |
database of equivariant functions |
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
579 |
|
56b8d977d1c0
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2742
diff
changeset
|
580 |
Such a rewrite system is often very helpful |
2742 | 581 |
in determining whether @{text "\<pi> \<bullet> t = t"} holds for a compound term @{text t}. ??? |
582 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
583 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
584 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
585 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
586 |
section {* Support and Freshness *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
587 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
588 |
text {* |
2742 | 589 |
The most original aspect of the nominal logic work of Pitts is a general |
590 |
definition for `the set of free variables, or free atoms, of an object @{text "x"}'. This |
|
591 |
definition is general in the sense that it applies not only to lambda terms, |
|
592 |
but to any type for which a permutation operation is defined |
|
593 |
(like lists, sets, functions and so on). |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
594 |
|
2742 | 595 |
\begin{definition}[Support] Given @{text x} is of permutation type, then |
596 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
597 |
@{thm [display,indent=10] supp_def[no_vars, THEN eq_reflection]} |
2742 | 598 |
\end{definition} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
599 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
600 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
601 |
(Note that due to the definition of swapping in \eqref{swapdef}, we do not |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
602 |
need to explicitly restrict @{text a} and @{text b} to have the same sort.) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
603 |
There is also the derived notion for when an atom @{text a} is \emph{fresh} |
2742 | 604 |
for an @{text x} of permutation type, defined as |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
605 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
606 |
@{thm [display,indent=10] fresh_def[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
607 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
608 |
\noindent |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
609 |
We also use the notation @{thm (lhs) fresh_star_def[no_vars]} for sets ot atoms |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
610 |
defined as follows |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
611 |
|
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
612 |
@{thm [display,indent=10] fresh_star_def[no_vars]} |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
613 |
|
2742 | 614 |
|
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
615 |
\noindent |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
616 |
A striking consequence of these definitions is that we can prove |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
617 |
without knowing anything about the structure of @{term x} that |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
618 |
swapping two fresh atoms, say @{text a} and @{text b}, leave |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
619 |
@{text x} unchanged. For the proof we use the following lemma |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
620 |
about swappings applied to an @{text x}: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
621 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
622 |
\begin{lemma}\label{swaptriple} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
623 |
Assuming @{text x} is of permutation type, and @{text a}, @{text b} and @{text c} |
2742 | 624 |
have the same sort, then \mbox{@{thm (prem 3) swap_rel_trans[no_vars]}} and |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
625 |
@{thm (prem 4) swap_rel_trans[no_vars]} imply @{thm (concl) swap_rel_trans[no_vars]}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
626 |
\end{lemma} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
627 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
628 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
629 |
The cases where @{text "a = c"} and @{text "b = c"} are immediate. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
630 |
For the remaining case it is, given our assumptions, easy to calculate |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
631 |
that the permutations |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
632 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
633 |
@{thm [display,indent=10] (concl) swap_triple[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
634 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
635 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
636 |
are equal. The lemma is then by application of the second permutation |
2742 | 637 |
property shown in~\eqref{newpermprops}.\hfill\qed |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
638 |
\end{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
639 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
640 |
\begin{theorem}\label{swapfreshfresh} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
641 |
Let @{text x} be of permutation type. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
642 |
@{thm [mode=IfThen] swap_fresh_fresh[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
643 |
\end{theorem} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
644 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
645 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
646 |
If @{text a} and @{text b} have different sort, then the swapping is the identity. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
647 |
If they have the same sort, we know by definition of support that both |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
648 |
@{term "finite {c. (a \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} and @{term "finite {c. (b \<rightleftharpoons> c) \<bullet> x \<noteq> x}"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
649 |
hold. So the union of these sets is finite too, and we know by Proposition~\ref{choosefresh} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
650 |
that there is an atom @{term c}, with the same sort as @{term a} and @{term b}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
651 |
that satisfies \mbox{@{term "(a \<rightleftharpoons> c) \<bullet> x = x"}} and @{term "(b \<rightleftharpoons> c) \<bullet> x = x"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
652 |
Now the theorem follows from Lemma~\ref{swaptriple}.\hfill\qed |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
653 |
\end{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
654 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
655 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
656 |
Two important properties that need to be established for later calculations is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
657 |
that @{text "supp"} and freshness are equivariant. For this we first show that: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
658 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
659 |
\begin{lemma}\label{half} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
660 |
If @{term x} is a permutation type, then @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
661 |
if and only if @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
662 |
\end{lemma} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
663 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
664 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
665 |
\begin{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
666 |
\begin{tabular}[t]{c@ {\hspace{2mm}}l@ {\hspace{5mm}}l} |
2742 | 667 |
& @{thm (lhs) fresh_permute_iff[where p="\<pi>",no_vars]}\\ |
668 |
@{text "\<equiv>"} & |
|
669 |
@{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"}\\ |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
670 |
@{text "\<Leftrightarrow>"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
671 |
& @{term "finite {b. (\<pi> \<bullet> a \<rightleftharpoons> \<pi> \<bullet> b) \<bullet> \<pi> \<bullet> x \<noteq> \<pi> \<bullet> x}"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
672 |
& since @{text "\<pi> \<bullet> _"} is bijective\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
673 |
@{text "\<Leftrightarrow>"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
674 |
& @{term "finite {b. \<pi> \<bullet> (a \<rightleftharpoons> b) \<bullet> x \<noteq> \<pi> \<bullet> x}"} |
2742 | 675 |
& by Lemma~\ref{permutecompose} and \eqref{swapeqvt}\\ |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
676 |
@{text "\<Leftrightarrow>"} |
2742 | 677 |
& @{term "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
678 |
& by \eqref{permuteequ}\\ |
2742 | 679 |
@{text "\<equiv>"} |
680 |
& @{thm (rhs) fresh_permute_iff[where p="\<pi>",no_vars]} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
681 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
682 |
\end{isabelle}\hfill\qed |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
683 |
\end{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
684 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
685 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
686 |
Together with the definition of the permutation operation on booleans, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
687 |
we can immediately infer equivariance of freshness: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
688 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
689 |
@{thm [display,indent=10] fresh_eqvt[where p="\<pi>",no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
690 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
691 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
692 |
Now equivariance of @{text "supp"}, namely |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
693 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
694 |
@{thm [display,indent=10] supp_eqvt[where p="\<pi>",no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
695 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
696 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
697 |
is by noting that @{thm supp_conv_fresh[no_vars]} and that freshness and |
2742 | 698 |
the logical connectives are equivariant. ??? Equivariance |
699 |
||
700 |
A simple consequence of the definition of support and equivariance is that |
|
701 |
if a function @{text f} is equivariant then we have |
|
702 |
||
703 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
704 |
\begin{tabular}{@ {}l} |
|
705 |
@{thm (concl) supp_fun_eqvt[no_vars]} |
|
706 |
\end{tabular}\hfill\numbered{suppeqvtfun} |
|
707 |
\end{isabelle} |
|
708 |
||
709 |
\noindent |
|
710 |
For function applications we can establish the two following properties. |
|
711 |
||
712 |
\begin{lemma} Let @{text f} and @{text x} be of permutation type, then |
|
713 |
\begin{isabelle} |
|
714 |
\begin{tabular}{r@ {\hspace{4mm}}p{10cm}} |
|
715 |
@{text "i)"} & @{thm[mode=IfThen] fresh_fun_app[no_vars]}\\ |
|
716 |
@{text "ii)"} & @{thm supp_fun_app[no_vars]}\\ |
|
717 |
\end{tabular} |
|
718 |
\end{isabelle} |
|
719 |
\end{lemma} |
|
720 |
||
721 |
\begin{proof} |
|
722 |
??? |
|
723 |
\end{proof} |
|
724 |
||
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
725 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
726 |
While the abstract properties of support and freshness, particularly |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
727 |
Theorem~\ref{swapfreshfresh}, are useful for developing Nominal Isabelle, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
728 |
one often has to calculate the support of some concrete object. This is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
729 |
straightforward for example for booleans, nats, products and lists: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
730 |
|
2742 | 731 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
732 |
\begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
733 |
@{text "booleans"}: & @{term "supp b = {}"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
734 |
@{text "nats"}: & @{term "supp n = {}"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
735 |
@{text "products"}: & @{thm supp_Pair[no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
736 |
@{text "lists:"} & @{thm supp_Nil[no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
737 |
& @{thm supp_Cons[no_vars]}\\ |
2742 | 738 |
\end{tabular} |
739 |
\end{isabelle} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
740 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
741 |
\noindent |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
742 |
But establishing the support of atoms and permutations is a bit |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
743 |
trickier. To do so we will use the following notion about a \emph{supporting set}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
744 |
|
2742 | 745 |
\begin{definition}[Supporting Set] |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
746 |
A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
747 |
not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
748 |
\end{definition} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
749 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
750 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
751 |
The main motivation for this notion is that we can characterise @{text "supp x"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
752 |
as the smallest finite set that supports @{text "x"}. For this we prove: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
753 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
754 |
\begin{lemma}\label{supports} Let @{text x} be of permutation type. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
755 |
\begin{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
756 |
\begin{tabular}{r@ {\hspace{4mm}}p{10cm}} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
757 |
i) & @{thm[mode=IfThen] supp_is_subset[no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
758 |
ii) & @{thm[mode=IfThen] supp_supports[no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
759 |
iii) & @{thm (concl) supp_is_least_supports[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
760 |
provided @{thm (prem 1) supp_is_least_supports[no_vars]}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
761 |
@{thm (prem 2) supp_is_least_supports[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
762 |
and @{text "S"} is the least such set, that means formally, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
763 |
for all @{text "S'"}, if @{term "finite S'"} and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
764 |
@{term "S' supports x"} then @{text "S \<subseteq> S'"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
765 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
766 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
767 |
\end{lemma} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
768 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
769 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
770 |
For @{text "i)"} we derive a contradiction by assuming there is an atom @{text a} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
771 |
with @{term "a \<in> supp x"} and @{text "a \<notin> S"}. Using the second fact, the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
772 |
assumption that @{term "S supports x"} gives us that @{text S} is a superset of |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
773 |
@{term "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}"}, which is finite by the assumption of @{text S} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
774 |
being finite. But this means @{term "a \<notin> supp x"}, contradicting our assumption. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
775 |
Property @{text "ii)"} is by a direct application of |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
776 |
Theorem~\ref{swapfreshfresh}. For the last property, part @{text "i)"} proves |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
777 |
one ``half'' of the claimed equation. The other ``half'' is by property |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
778 |
@{text "ii)"} and the fact that @{term "supp x"} is finite by @{text "i)"}.\hfill\qed |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
779 |
\end{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
780 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
781 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
782 |
These are all relatively straightforward proofs adapted from the existing |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
783 |
nominal logic work. However for establishing the support of atoms and |
2742 | 784 |
permutations we found the following `optimised' variant of @{text "iii)"} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
785 |
more useful: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
786 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
787 |
\begin{lemma}\label{optimised} Let @{text x} be of permutation type. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
788 |
We have that @{thm (concl) finite_supp_unique[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
789 |
provided @{thm (prem 1) finite_supp_unique[no_vars]}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
790 |
@{thm (prem 2) finite_supp_unique[no_vars]}, and for |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
791 |
all @{text "a \<in> S"} and all @{text "b \<notin> S"}, with @{text a} |
1809
08e4d3cbcf8c
folded changes from the conference version
Christian Urban <urbanc@in.tum.de>
parents:
1790
diff
changeset
|
792 |
and @{text b} having the same sort, \mbox{@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"}} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
793 |
\end{lemma} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
794 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
795 |
\begin{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
796 |
By Lemma \ref{supports}@{text ".iii)"} we have to show that for every finite |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
797 |
set @{text S'} that supports @{text x}, \mbox{@{text "S \<subseteq> S'"}} holds. We will |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
798 |
assume that there is an atom @{text "a"} that is element of @{text S}, but |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
799 |
not @{text "S'"} and derive a contradiction. Since both @{text S} and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
800 |
@{text S'} are finite, we can by Proposition \ref{choosefresh} obtain an atom |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
801 |
@{text b}, which has the same sort as @{text "a"} and for which we know |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
802 |
@{text "b \<notin> S"} and @{text "b \<notin> S'"}. Since we assumed @{text "a \<notin> S'"} and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
803 |
we have that @{text "S' supports x"}, we have on one hand @{term "(a \<rightleftharpoons> b) \<bullet> x |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
804 |
= x"}. On the other hand, the fact @{text "a \<in> S"} and @{text "b \<notin> S"} imply |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
805 |
@{term "(a \<rightleftharpoons> b) \<bullet> x \<noteq> x"} using the assumed implication. This gives us the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
806 |
contradiction.\hfill\qed |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
807 |
\end{proof} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
808 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
809 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
810 |
Using this lemma we only have to show the following three proof-obligations |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
811 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
812 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
813 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
814 |
i) & @{term "{c} supports c"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
815 |
ii) & @{term "finite {c}"}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
816 |
iii) & @{text "\<forall>a \<in> {c} b \<notin> {c}. sort a = sort b \<longrightarrow> (a b) \<bullet> c \<noteq> c"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
817 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
818 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
819 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
820 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
821 |
in order to establish that @{thm supp_atom[where a="c", no_vars]} holds. In |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
822 |
Isabelle/HOL these proof-obligations can be discharged by easy |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
823 |
simplifications. Similar proof-obligations arise for the support of |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
824 |
permutations, which is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
825 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
826 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
827 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
828 |
@{thm supp_perm[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
829 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
830 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
831 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
832 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
833 |
The only proof-obligation that is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
834 |
interesting is the one where we have to show that |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
835 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
836 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
837 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
838 |
@{text "If \<pi> \<bullet> a \<noteq> a, \<pi> \<bullet> b = b and sort a = sort b, then (a b) \<bullet> \<pi> \<noteq> \<pi>"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
839 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
840 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
841 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
842 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
843 |
For this we observe that |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
844 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
845 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
846 |
\begin{tabular}{@ {}rcl} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
847 |
@{thm (lhs) perm_swap_eq[where p="\<pi>", no_vars]} & |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
848 |
if and only if & |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
849 |
@{thm (rhs) perm_swap_eq[where p="\<pi>", no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
850 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
851 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
852 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
853 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
854 |
holds by a simple calculation using the group properties of permutations. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
855 |
The proof-obligation can then be discharged by analysing the inequality |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
856 |
between the permutations @{term "(\<pi> \<bullet> a \<rightleftharpoons> b)"} and @{term "(a \<rightleftharpoons> b)"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
857 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
858 |
The main point about support is that whenever an object @{text x} has finite |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
859 |
support, then Proposition~\ref{choosefresh} allows us to choose for @{text x} a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
860 |
fresh atom with arbitrary sort. This is an important operation in Nominal |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
861 |
Isabelle in situations where, for example, a bound variable needs to be |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
862 |
renamed. To allow such a choice, we only have to assume that |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
863 |
@{text "finite (supp x)"} holds. For more convenience we |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
864 |
can define a type class for types where every element has finite support, and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
865 |
prove that the types @{term "atom"}, @{term "perm"}, lists, products and |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
866 |
booleans are instances of this type class. |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
867 |
|
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
868 |
Unfortunately, this does not work for sets or Isabelle/HOL's function |
2742 | 869 |
type. There are functions and sets definable in Isabelle/HOL for which the |
870 |
finite support property does not hold. A simple example of a function with |
|
871 |
infinite support is @{const nat_of} shown in \eqref{sortnatof}. This |
|
872 |
function's support is the set of \emph{all} atoms @{term "UNIV::atom set"}. |
|
873 |
To establish this we show |
|
874 |
@{term "\<not> a \<sharp> nat_of"}. This is equivalent to assuming the set @{term |
|
875 |
"{b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"} is finite and deriving a |
|
876 |
contradiction. From the assumption we also know that @{term "{a} \<union> {b. (a \<rightleftharpoons> |
|
877 |
b) \<bullet> nat_of \<noteq> nat_of}"} is finite. Then we can use |
|
878 |
Proposition~\ref{choosefresh} to choose an atom @{text c} such that @{term |
|
879 |
"c \<noteq> a"}, @{term "sort_of c = sort_of a"} and @{term "(a \<rightleftharpoons> c) \<bullet> nat_of = |
|
880 |
nat_of"}. Now we can reason as follows: |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
881 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
882 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
883 |
\begin{tabular}[b]{@ {}rcl@ {\hspace{5mm}}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
884 |
@{text "nat_of a"} & @{text "="} & @{text "(a \<rightleftharpoons> c) \<bullet> (nat_of a)"} & by def.~of permutations on nats\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
885 |
& @{text "="} & @{term "((a \<rightleftharpoons> c) \<bullet> nat_of) ((a \<rightleftharpoons> c) \<bullet> a)"} & by \eqref{permutefunapp}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
886 |
& @{text "="} & @{term "nat_of c"} & by assumptions on @{text c}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
887 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
888 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
889 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
890 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
891 |
But this means we have that @{term "nat_of a = nat_of c"} and @{term "sort_of a = sort_of c"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
892 |
This implies that atoms @{term a} and @{term c} must be equal, which clashes with our |
2742 | 893 |
assumption @{term "c \<noteq> a"} about how we chose @{text c}.\footnote{Cheney \cite{Cheney06} |
894 |
gives similar examples for constructions that have infinite support.} |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
895 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
896 |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
897 |
section {* Support of Finite Sets *} |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
898 |
|
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
899 |
text {* |
2742 | 900 |
Also the set type is one instance whose elements are not generally finitely |
901 |
supported (we will give an example in Section~\ref{concrete}). |
|
902 |
However, we can easily show that finite sets and co-finite sets of atoms are finitely |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
903 |
supported, because their support can be characterised as: |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
904 |
|
2742 | 905 |
\begin{lemma}\label{finatomsets}\mbox{}\\ |
906 |
@{text "i)"} If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.\\ |
|
907 |
@{text "ii)"} If @{term "UNIV - (S::atom set)"} is a finite set of atoms, then |
|
908 |
@{thm (concl) supp_cofinite_atom_set[no_vars]}. |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
909 |
\end{lemma} |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
910 |
|
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
911 |
\begin{proof} |
2742 | 912 |
Both parts can be easily shown by Lemma~\ref{optimised}. We only have to observe |
913 |
that a swapping @{text "(a b)"} leaves a set @{text S} unchanged provided both |
|
914 |
@{text a} and @{text b} are elements in @{text S} or both are not in @{text S}. |
|
915 |
However if the sorts of a @{text a} and @{text b} agree, then the swapping will |
|
916 |
change @{text S} if either of them is an element in @{text S} and the other is |
|
917 |
not.\hfill\qed |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
918 |
\end{proof} |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
919 |
|
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
920 |
\noindent |
2742 | 921 |
Note that a consequence of the second part of this lemma is that |
922 |
@{term "supp (UNIV::atom set) = {}"}. |
|
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
923 |
More difficult, however, is it to establish that finite sets of finitely |
2742 | 924 |
supported objects are finitely supported. For this we first show that |
925 |
the union of the suports of finitely many and finitely supported objects |
|
926 |
is finite, namely |
|
927 |
||
928 |
\begin{lemma}\label{unionsupp} |
|
929 |
If @{text S} is a finite set whose elements are all finitely supported, then\\ |
|
930 |
@{text "i)"} @{thm (concl) Union_of_finite_supp_sets[no_vars]} and\\ |
|
931 |
@{text "ii)"} @{thm (concl) Union_included_in_supp[no_vars]}. |
|
932 |
\end{lemma} |
|
933 |
||
934 |
\begin{proof} |
|
935 |
The first part is by a straightforward induction on the finiteness of @{text S}. |
|
936 |
For the second part, we know that @{term "\<Union>x\<in>S. supp x"} is a set of atoms, which |
|
937 |
by the first part is finite. Therefore we know by Lemma~\ref{finatomsets}.@{text "i)"} |
|
938 |
that @{term "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"}. Taking @{text "f"} to be |
|
939 |
\mbox{@{text "\<lambda>S. \<Union> (supp ` S)"}}, we can write the right hand side as @{text "supp (f S)"}. |
|
940 |
Since @{text "f"} is an equivariant function, we have that |
|
941 |
@{text "supp (f S) \<subseteq> supp S"} by ??? This completes the second part.\hfill\qed |
|
942 |
\end{proof} |
|
943 |
||
944 |
\noindent |
|
945 |
With this lemma in place we can establish that |
|
946 |
||
947 |
\begin{lemma} |
|
948 |
@{thm[mode=IfThen] supp_of_finite_sets[no_vars]} |
|
949 |
\end{lemma} |
|
950 |
||
951 |
\begin{proof} |
|
952 |
The right-to-left inclusion is proved in Lemma~\ref{unionsupp}.@{text "ii)"}. To show the inclusion |
|
953 |
in the other direction we have to show Lemma~\ref{supports}.@{text "i)"} |
|
954 |
\end{proof} |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
955 |
*} |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
956 |
|
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
957 |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
958 |
section {* Induction Principles *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
959 |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
960 |
text {* |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
961 |
While the use of functions as permutation provides us with a unique |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
962 |
representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
963 |
@{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
964 |
one draw back: it does not come readily with an induction principle. |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
965 |
Such an induction principle is handy for deriving properties like |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
966 |
|
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
967 |
@{thm [display, indent=10] supp_perm_eq[no_vars]} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
968 |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
969 |
\noindent |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
970 |
However, it is not too difficult to derive an induction principle, |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
971 |
given the fact that we allow only permutations with a finite domain. |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
972 |
*} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
973 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
974 |
|
2522
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
975 |
section {* An Abstraction Type *} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
976 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
977 |
text {* |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
978 |
To that end, we will consider |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
979 |
first pairs @{text "(as, x)"} of type @{text "(atom set) \<times> \<beta>"}. These pairs |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
980 |
are intended to represent the abstraction, or binding, of the set of atoms @{text |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
981 |
"as"} in the body @{text "x"}. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
982 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
983 |
The first question we have to answer is when two pairs @{text "(as, x)"} and |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
984 |
@{text "(bs, y)"} are $\alpha$-equivalent? (For the moment we are interested in |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
985 |
the notion of $\alpha$-equivalence that is \emph{not} preserved by adding |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
986 |
vacuous binders.) To answer this question, we identify four conditions: {\it (i)} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
987 |
given a free-atom function @{text "fa"} of type \mbox{@{text "\<beta> \<Rightarrow> atom |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
988 |
set"}}, then @{text x} and @{text y} need to have the same set of free |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
989 |
atoms; moreover there must be a permutation @{text p} such that {\it |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
990 |
(ii)} @{text p} leaves the free atoms of @{text x} and @{text y} unchanged, but |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
991 |
{\it (iii)} ``moves'' their bound names so that we obtain modulo a relation, |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
992 |
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
993 |
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
994 |
requirements {\it (i)} to {\it (iv)} can be stated formally as follows: |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
995 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
996 |
\begin{equation}\label{alphaset} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
997 |
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
998 |
\multicolumn{3}{l}{@{text "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm] |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
999 |
& @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1000 |
@{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1001 |
@{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1002 |
@{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1003 |
\end{array} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1004 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1005 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1006 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1007 |
Note that this relation depends on the permutation @{text |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1008 |
"p"}; $\alpha$-equivalence between two pairs is then the relation where we |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1009 |
existentially quantify over this @{text "p"}. Also note that the relation is |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1010 |
dependent on a free-atom function @{text "fa"} and a relation @{text |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1011 |
"R"}. The reason for this extra generality is that we will use |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1012 |
$\approx_{\,\textit{set}}$ for both ``raw'' terms and $\alpha$-equated terms. In |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1013 |
the latter case, @{text R} will be replaced by equality @{text "="} and we |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1014 |
will prove that @{text "fa"} is equal to @{text "supp"}. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1015 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1016 |
It might be useful to consider first some examples about how these definitions |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1017 |
of $\alpha$-equivalence pan out in practice. For this consider the case of |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1018 |
abstracting a set of atoms over types (as in type-schemes). We set |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1019 |
@{text R} to be the usual equality @{text "="} and for @{text "fa(T)"} we |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1020 |
define |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1021 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1022 |
\begin{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1023 |
@{text "fa(x) = {x}"} \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1024 |
\end{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1025 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1026 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1027 |
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1028 |
\eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1029 |
@{text "({y, x}, y \<rightarrow> x)"} are $\alpha$-equivalent according to |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1030 |
$\approx_{\,\textit{set}}$ and $\approx_{\,\textit{res}}$ by taking @{text p} to |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1031 |
be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1032 |
"([x, y], x \<rightarrow> y)"} $\not\approx_{\,\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1033 |
since there is no permutation that makes the lists @{text "[x, y]"} and |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1034 |
@{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1035 |
unchanged. Another example is @{text "({x}, x)"} $\approx_{\,\textit{res}}$ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1036 |
@{text "({x, y}, x)"} which holds by taking @{text p} to be the identity |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1037 |
permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1038 |
$\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1039 |
permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1040 |
(similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1041 |
shown that all three notions of $\alpha$-equivalence coincide, if we only |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1042 |
abstract a single atom. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1043 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1044 |
In the rest of this section we are going to introduce three abstraction |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1045 |
types. For this we define |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1046 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1047 |
\begin{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1048 |
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1049 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1050 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1051 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1052 |
(similarly for $\approx_{\,\textit{abs\_res}}$ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1053 |
and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1054 |
relations and equivariant. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1055 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1056 |
\begin{lemma}\label{alphaeq} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1057 |
The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1058 |
and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1059 |
"abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1060 |
bs, p \<bullet> y)"} (similarly for the other two relations). |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1061 |
\end{lemma} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1062 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1063 |
\begin{proof} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1064 |
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1065 |
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1066 |
of transitivity, we have two permutations @{text p} and @{text q}, and for the |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1067 |
proof obligation use @{text "q + p"}. All conditions are then by simple |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1068 |
calculations. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1069 |
\end{proof} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1070 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1071 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1072 |
This lemma allows us to use our quotient package for introducing |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1073 |
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1074 |
representing $\alpha$-equivalence classes of pairs of type |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1075 |
@{text "(atom set) \<times> \<beta>"} (in the first two cases) and of type @{text "(atom list) \<times> \<beta>"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1076 |
(in the third case). |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1077 |
The elements in these types will be, respectively, written as: |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1078 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1079 |
\begin{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1080 |
@{term "Abs_set as x"} \hspace{5mm} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1081 |
@{term "Abs_res as x"} \hspace{5mm} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1082 |
@{term "Abs_lst as x"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1083 |
\end{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1084 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1085 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1086 |
indicating that a set (or list) of atoms @{text as} is abstracted in @{text x}. We will |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1087 |
call the types \emph{abstraction types} and their elements |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1088 |
\emph{abstractions}. The important property we need to derive is the support of |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1089 |
abstractions, namely: |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1090 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1091 |
\begin{theorem}[Support of Abstractions]\label{suppabs} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1092 |
Assuming @{text x} has finite support, then\\[-6mm] |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1093 |
\begin{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1094 |
\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1095 |
%@ {thm (lhs) supp_abs(1)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(1)[no_vars]}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1096 |
%@ {thm (lhs) supp_abs(2)[no_vars]} & $=$ & @ {thm (rhs) supp_abs(2)[no_vars]}\\ |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1097 |
%@ {thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @ {thm (rhs) supp_abs(3)[where bs="as", no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1098 |
\end{tabular} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1099 |
\end{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1100 |
\end{theorem} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1101 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1102 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1103 |
Below we will show the first equation. The others |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1104 |
follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1105 |
we have |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1106 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1107 |
\begin{equation}\label{abseqiff} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1108 |
%@ {thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1109 |
%@ {thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1110 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1111 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1112 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1113 |
and also |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1114 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1115 |
\begin{equation}\label{absperm} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1116 |
@{thm permute_Abs[no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1117 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1118 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1119 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1120 |
The second fact derives from the definition of permutations acting on pairs |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1121 |
\eqref{permute} and $\alpha$-equivalence being equivariant |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1122 |
(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1123 |
the following lemma about swapping two atoms in an abstraction. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1124 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1125 |
\begin{lemma} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1126 |
%@ {thm[mode=IfThen] abs_swap1(1)[where bs="as", no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1127 |
\end{lemma} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1128 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1129 |
\begin{proof} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1130 |
This lemma is straightforward using \eqref{abseqiff} and observing that |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1131 |
the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1132 |
Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}). |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1133 |
\end{proof} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1134 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1135 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1136 |
Assuming that @{text "x"} has finite support, this lemma together |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1137 |
with \eqref{absperm} allows us to show |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1138 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1139 |
\begin{equation}\label{halfone} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1140 |
%@ {thm abs_supports(1)[no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1141 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1142 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1143 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1144 |
which by Property~\ref{supportsprop} gives us ``one half'' of |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1145 |
Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1146 |
it, we use a trick from \cite{Pitts04} and first define an auxiliary |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1147 |
function @{text aux}, taking an abstraction as argument: |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1148 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1149 |
\begin{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1150 |
@{thm supp_set.simps[THEN eq_reflection, no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1151 |
\end{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1152 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1153 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1154 |
Using the second equation in \eqref{equivariance}, we can show that |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1155 |
@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1156 |
(supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1157 |
This in turn means |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1158 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1159 |
\begin{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1160 |
@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1161 |
\end{center} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1162 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1163 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1164 |
using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set, |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1165 |
we further obtain |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1166 |
% |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1167 |
\begin{equation}\label{halftwo} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1168 |
%@ {thm (concl) supp_abs_subset1(1)[no_vars]} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1169 |
\end{equation} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1170 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1171 |
\noindent |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1172 |
since for finite sets of atoms, @{text "bs"}, we have |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1173 |
@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1174 |
Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1175 |
Theorem~\ref{suppabs}. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1176 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1177 |
The method of first considering abstractions of the |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1178 |
form @{term "Abs_set as x"} etc is motivated by the fact that |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1179 |
we can conveniently establish at the Isabelle/HOL level |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1180 |
properties about them. It would be |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1181 |
laborious to write custom ML-code that derives automatically such properties |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1182 |
for every term-constructor that binds some atoms. Also the generality of |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1183 |
the definitions for $\alpha$-equivalence will help us in the next section. |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1184 |
*} |
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1185 |
|
0cb0c88b2cad
added a section about abstractions
Christian Urban <urbanc@in.tum.de>
parents:
2521
diff
changeset
|
1186 |
|
2742 | 1187 |
section {* Concrete Atom Types\label{concrete} *} |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1188 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1189 |
text {* |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1190 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1191 |
So far, we have presented a system that uses only a single multi-sorted atom |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1192 |
type. This design gives us the flexibility to define operations and prove |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1193 |
theorems that are generic with respect to atom sorts. For example, as |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1194 |
illustrated above the @{term supp} function returns a set that includes the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1195 |
free atoms of \emph{all} sorts together; the flexibility offered by the new |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1196 |
atom type makes this possible. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1197 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1198 |
However, the single multi-sorted atom type does not make an ideal interface |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1199 |
for end-users of Nominal Isabelle. If sorts are not distinguished by |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1200 |
Isabelle's type system, users must reason about atom sorts manually. That |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1201 |
means subgoals involving sorts must be discharged explicitly within proof |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1202 |
scripts, instead of being inferred by Isabelle/HOL's type checker. In other |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1203 |
cases, lemmas might require additional side conditions about sorts to be true. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1204 |
For example, swapping @{text a} and @{text b} in the pair \mbox{@{term "(a, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1205 |
b)"}} will only produce the expected result if we state the lemma in |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1206 |
Isabelle/HOL as: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1207 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1208 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1209 |
lemma |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1210 |
fixes a b :: "atom" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1211 |
assumes asm: "sort a = sort b" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1212 |
shows "(a \<rightleftharpoons> b) \<bullet> (a, b) = (b, a)" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1213 |
using asm by simp |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1214 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1215 |
text {* |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1216 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1217 |
Fortunately, it is possible to regain most of the type-checking automation |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1218 |
that is lost by moving to a single atom type. We accomplish this by defining |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1219 |
\emph{subtypes} of the generic atom type that only include atoms of a single |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1220 |
specific sort. We call such subtypes \emph{concrete atom types}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1221 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1222 |
The following Isabelle/HOL command defines a concrete atom type called |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1223 |
\emph{name}, which consists of atoms whose sort equals the string @{term |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1224 |
"''name''"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1225 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1226 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1227 |
\isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1228 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1229 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1230 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1231 |
This command automatically generates injective functions that map from the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1232 |
concrete atom type into the generic atom type and back, called |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1233 |
representation and abstraction functions, respectively. We will write these |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1234 |
functions as follows: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1235 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1236 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1237 |
\begin{tabular}{@ {}l@ {\hspace{10mm}}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1238 |
@{text "\<lfloor>_\<rfloor> :: name \<Rightarrow> atom"} & |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1239 |
@{text "\<lceil>_\<rceil> :: atom \<Rightarrow> name"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1240 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1241 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1242 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1243 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1244 |
With the definition @{thm permute_name_def [where p="\<pi>", THEN |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1245 |
eq_reflection, no_vars]}, it is straightforward to verify that the type |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1246 |
@{typ name} is a permutation type. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1247 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1248 |
In order to reason uniformly about arbitrary concrete atom types, we define a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1249 |
type class that characterises type @{typ name} and other similarly-defined |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1250 |
types. The definition of the concrete atom type class is as follows: First, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1251 |
every concrete atom type must be a permutation type. In addition, the class |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1252 |
defines an overloaded function that maps from the concrete type into the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1253 |
generic atom type, which we will write @{text "|_|"}. For each class |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1254 |
instance, this function must be injective and equivariant, and its outputs |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1255 |
must all have the same sort, that is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1256 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1257 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1258 |
\begin{tabular}{r@ {\hspace{3mm}}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1259 |
i) if @{thm (lhs) atom_eq_iff [no_vars]} then @{thm (rhs) atom_eq_iff [no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1260 |
ii) @{thm atom_eqvt[where p="\<pi>", no_vars]}\\ |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1261 |
iii) @{thm sort_of_atom_eq [no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1262 |
\end{tabular}\hfill\numbered{atomprops} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1263 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1264 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1265 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1266 |
With the definition @{thm atom_name_def [THEN eq_reflection, no_vars]} we can |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1267 |
show that @{typ name} satisfies all the above requirements of a concrete atom |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1268 |
type. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1269 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1270 |
The whole point of defining the concrete atom type class was to let users |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1271 |
avoid explicit reasoning about sorts. This benefit is realised by defining a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1272 |
special swapping operation of type @{text "\<alpha> \<Rightarrow> \<alpha> |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1273 |
\<Rightarrow> perm"}, where @{text "\<alpha>"} is a concrete atom type: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1274 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1275 |
@{thm [display,indent=10] flip_def [THEN eq_reflection, no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1276 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1277 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1278 |
As a consequence of its type, the @{text "\<leftrightarrow>"}-swapping |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1279 |
operation works just like the generic swapping operation, but it does not |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1280 |
require any sort-checking side conditions---the sort-correctness is ensured by |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1281 |
the types! For @{text "\<leftrightarrow>"} we can establish the following |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1282 |
simplification rule: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1283 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1284 |
@{thm [display,indent=10] permute_flip_at[no_vars]} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1285 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1286 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1287 |
If we now want to swap the \emph{concrete} atoms @{text a} and @{text b} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1288 |
in the pair @{term "(a, b)"} we can establish the lemma as follows: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1289 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1290 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1291 |
lemma |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1292 |
fixes a b :: "name" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1293 |
shows "(a \<leftrightarrow> b) \<bullet> (a, b) = (b, a)" |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1294 |
by simp |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1295 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1296 |
text {* |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1297 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1298 |
There is no need to state an explicit premise involving sorts. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1299 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1300 |
We can automate the process of creating concrete atom types, so that users |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1301 |
can define a new one simply by issuing the command |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1302 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1303 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1304 |
\begin{tabular}{@ {}l} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1305 |
\isacommand{atom\_decl}~~@{text "name"} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1306 |
\end{tabular} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1307 |
\end{isabelle} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1308 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1309 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1310 |
This command can be implemented using less than 100 lines of custom ML-code. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1311 |
In comparison, the old version of Nominal Isabelle included more than 1000 |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1312 |
lines of ML-code for creating concrete atom types, and for defining various |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1313 |
type classes and instantiating generic lemmas for them. In addition to |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1314 |
simplifying the ML-code, the setup here also offers user-visible improvements: |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1315 |
Now concrete atoms can be declared at any point of a formalisation, and |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1316 |
theories that separately declare different atom types can be merged |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1317 |
together---it is no longer required to collect all atom declarations in one |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1318 |
place. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1319 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1320 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1321 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1322 |
|
2742 | 1323 |
section {* Related Work\label{related} *} |
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
1324 |
|
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
1325 |
text {* |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
1326 |
Add here comparison with old work. |
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
1327 |
|
2742 | 1328 |
Using a single atom type to represent atoms of different sorts and |
1329 |
representing permutations as functions are not new ideas; see |
|
1330 |
\cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution |
|
1331 |
of this paper is to show an example of how to make better theorem proving |
|
1332 |
tools by choosing the right level of abstraction for the underlying |
|
1333 |
theory---our design choices take advantage of Isabelle's type system, type |
|
1334 |
classes and reasoning infrastructure. The novel technical contribution is a |
|
1335 |
mechanism for dealing with ``Church-style'' lambda-terms \cite{Church40} and |
|
1336 |
HOL-based languages \cite{PittsHOL4} where variables and variable binding |
|
1337 |
depend on type annotations. |
|
1338 |
||
1339 |
The paper is organised as follows\ldots |
|
1340 |
||
1341 |
||
2523
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
1342 |
The main point is that the above reasoning blends smoothly with the reasoning |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
1343 |
infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single |
e903c32ec24f
more on the pearl paper
Christian Urban <urbanc@in.tum.de>
parents:
2522
diff
changeset
|
1344 |
type class suffices. |
2736 | 1345 |
|
1346 |
With this |
|
1347 |
design one can represent permutations as lists of pairs of atoms and the |
|
1348 |
operation of applying a permutation to an object as the function |
|
1349 |
||
1350 |
||
1351 |
@{text [display,indent=10] "_ \<bullet> _ :: (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
|
1352 |
||
1353 |
\noindent |
|
1354 |
where @{text "\<alpha>"} stands for a type of atoms and @{text "\<beta>"} for the type |
|
1355 |
of the objects on which the permutation acts. For atoms |
|
1356 |
the permutation operation is defined over the length of lists as follows |
|
1357 |
||
1358 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
1359 |
\begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
1360 |
@{text "[] \<bullet> c"} & @{text "="} & @{text c}\\ |
|
1361 |
@{text "(a b)::\<pi> \<bullet> c"} & @{text "="} & |
|
1362 |
$\begin{cases} @{text a} & \textrm{if}~@{text "\<pi> \<bullet> c = b"}\\ |
|
1363 |
@{text b} & \textrm{if}~@{text "\<pi> \<bullet> c = a"}\\ |
|
1364 |
@{text "\<pi> \<bullet> c"} & \textrm{otherwise}\end{cases}$ |
|
1365 |
\end{tabular}\hfill\numbered{atomperm} |
|
1366 |
\end{isabelle} |
|
1367 |
||
1368 |
\noindent |
|
1369 |
where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and |
|
1370 |
@{text "b"}. For atoms with different type than the permutation, we |
|
1371 |
define @{text "\<pi> \<bullet> c \<equiv> c"}. |
|
1372 |
||
1373 |
With the separate atom types and the list representation of permutations it |
|
1374 |
is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' |
|
1375 |
permutation, since the type system excludes lists containing atoms of |
|
1376 |
different type. However, a disadvantage is that whenever we need to |
|
1377 |
generalise induction hypotheses by quantifying over permutations, we have to |
|
1378 |
build quantifications like |
|
1379 |
||
1380 |
@{text [display,indent=10] "\<forall>\<pi>\<^isub>1 \<dots> \<forall>\<pi>\<^isub>n. \<dots>"} |
|
1381 |
||
1382 |
\noindent |
|
1383 |
where the @{text "\<pi>\<^isub>i"} are of type @{text "(\<alpha>\<^isub>i \<times> \<alpha>\<^isub>i) list"}. |
|
1384 |
The reason is that the permutation operation behaves differently for |
|
1385 |
every @{text "\<alpha>\<^isub>i"} and the type system does not allow use to have a |
|
1386 |
single quantification to stand for all permutations. Similarly, the |
|
1387 |
notion of support |
|
1388 |
||
1389 |
@{text [display,indent=10] "supp _ :: \<beta> \<Rightarrow> \<alpha> set"} |
|
1390 |
||
1391 |
\noindent |
|
1392 |
which we will define later, cannot be |
|
1393 |
used to express the support of an object over \emph{all} atoms. The reason |
|
1394 |
is that support can behave differently for each @{text |
|
1395 |
"\<alpha>\<^isub>i"}. This problem is annoying, because if we need to know in |
|
1396 |
a statement that an object, say @{text "x"}, is finitely supported we end up |
|
1397 |
with having to state premises of the form |
|
1398 |
||
1399 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
1400 |
\begin{tabular}{@ {}l} |
|
1401 |
@{text "finite ((supp x) :: \<alpha>\<^isub>1 set) , \<dots>, finite ((supp x) :: \<alpha>\<^isub>n set)"} |
|
1402 |
\end{tabular}\hfill\numbered{fssequence} |
|
1403 |
\end{isabelle} |
|
1404 |
||
1405 |
\noindent |
|
1406 |
Because of these disadvantages, we will use in this paper a single unified atom type to |
|
1407 |
represent atoms of different sorts. Consequently, we have to deal with the |
|
1408 |
case that a swapping of two atoms is ill-sorted: we cannot rely anymore on |
|
1409 |
the type systems to exclude them. |
|
1410 |
||
1411 |
We also will not represent permutations as lists of pairs of atoms (as done in |
|
1412 |
\cite{Urban08}). Although an |
|
1413 |
advantage of this representation is that the basic operations on |
|
1414 |
permutations are already defined in Isabelle's list library: composition of |
|
1415 |
two permutations (written @{text "_ @ _"}) is just list append, and |
|
1416 |
inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just |
|
1417 |
list reversal, and another advantage is that there is a well-understood |
|
1418 |
induction principle for lists, a disadvantage is that permutations |
|
1419 |
do not have unique representations as lists. We have to explicitly identify |
|
1420 |
them according to the relation |
|
1421 |
||
1422 |
||
1423 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
1424 |
\begin{tabular}{@ {}l} |
|
1425 |
@{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2 \<equiv> \<forall>a. \<pi>\<^isub>1 \<bullet> a = \<pi>\<^isub>2 \<bullet> a"} |
|
1426 |
\end{tabular}\hfill\numbered{permequ} |
|
1427 |
\end{isabelle} |
|
1428 |
||
1429 |
\noindent |
|
1430 |
This is a problem when lifting the permutation operation to other types, for |
|
1431 |
example sets, functions and so on. For this we need to ensure that every definition |
|
1432 |
is well-behaved in the sense that it satisfies some |
|
1433 |
\emph{permutation properties}. In the list representation we need |
|
1434 |
to state these properties as follows: |
|
1435 |
||
1436 |
||
1437 |
\begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
1438 |
\begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} |
|
1439 |
i) & @{text "[] \<bullet> x = x"}\\ |
|
1440 |
ii) & @{text "(\<pi>\<^isub>1 @ \<pi>\<^isub>2) \<bullet> x = \<pi>\<^isub>1 \<bullet> (\<pi>\<^isub>2 \<bullet> x)"}\\ |
|
1441 |
iii) & if @{text "\<pi>\<^isub>1 \<sim> \<pi>\<^isub>2"} then @{text "\<pi>\<^isub>1 \<bullet> x = \<pi>\<^isub>2 \<bullet> x"} |
|
1442 |
\end{tabular}\hfill\numbered{permprops} |
|
1443 |
\end{isabelle} |
|
1444 |
||
1445 |
\noindent |
|
1446 |
where the last clause explicitly states that the permutation operation has |
|
1447 |
to produce the same result for related permutations. Moreover, |
|
1448 |
``permutations-as-lists'' do not satisfy the group properties. This means by |
|
1449 |
using this representation we will not be able to reuse the extensive |
|
1450 |
reasoning infrastructure in Isabelle about groups. Because of this, we will represent |
|
1451 |
in this paper permutations as functions from atoms to atoms. This representation |
|
1452 |
is unique and satisfies the laws of non-commutative groups. |
|
2033
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
1453 |
*} |
74bd7bfb484b
some preliminary changes to the pearl-jv paper
Christian Urban <urbanc@in.tum.de>
parents:
2005
diff
changeset
|
1454 |
|
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1455 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1456 |
section {* Conclusion *} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1457 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1458 |
text {* |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1459 |
This proof pearl describes a new formalisation of the nominal logic work by |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1460 |
Pitts et al. With the definitions we presented here, the formal reasoning blends |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1461 |
smoothly with the infrastructure of the Isabelle/HOL theorem prover. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1462 |
Therefore the formalisation will be the underlying theory for a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1463 |
new version of Nominal Isabelle. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1464 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1465 |
The main difference of this paper with respect to existing work on Nominal |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1466 |
Isabelle is the representation of atoms and permutations. First, we used a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1467 |
single type for sorted atoms. This design choice means for a term @{term t}, |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1468 |
say, that its support is completely characterised by @{term "supp t"}, even |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1469 |
if the term contains different kinds of atoms. Also, whenever we have to |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1470 |
generalise an induction so that a property @{text P} is not just established |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1471 |
for all @{text t}, but for all @{text t} \emph{and} under all permutations |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1472 |
@{text \<pi>}, then we only have to state @{term "\<forall>\<pi>. P (\<pi> \<bullet> t)"}. The reason is |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1473 |
that permutations can now consist of multiple swapping each of which can |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1474 |
swap different kinds of atoms. This simplifies considerably the reasoning |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1475 |
involved in building Nominal Isabelle. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1476 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1477 |
Second, we represented permutations as functions so that the associated |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1478 |
permutation operation has only a single type parameter. This is very convenient |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1479 |
because the abstract reasoning about permutations fits cleanly |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1480 |
with Isabelle/HOL's type classes. No custom ML-code is required to work |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1481 |
around rough edges. Moreover, by establishing that our permutations-as-functions |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1482 |
representation satisfy the group properties, we were able to use extensively |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1483 |
Isabelle/HOL's reasoning infrastructure for groups. This often reduced proofs |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1484 |
to simple calculations over @{text "+"}, @{text "-"} and @{text "0"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1485 |
An interesting point is that we defined the swapping operation so that a |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1486 |
swapping of two atoms with different sorts is \emph{not} excluded, like |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1487 |
in our older work on Nominal Isabelle, but there is no ``effect'' of such |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1488 |
a swapping (it is defined as the identity). This is a crucial insight |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1489 |
in order to make the approach based on a single type of sorted atoms to work. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1490 |
But of course it is analogous to the well-known trick of defining division by |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1491 |
zero to return zero. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1492 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1493 |
We noticed only one disadvantage of the permutations-as-functions: Over |
1809
08e4d3cbcf8c
folded changes from the conference version
Christian Urban <urbanc@in.tum.de>
parents:
1790
diff
changeset
|
1494 |
lists we can easily perform inductions. For permutations made up from |
1785
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1495 |
functions, we have to manually derive an appropriate induction principle. We |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1496 |
can establish such a principle, but we have no real experience yet whether ours |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1497 |
is the most useful principle: such an induction principle was not needed in |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1498 |
any of the reasoning we ported from the old Nominal Isabelle, except |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1499 |
when showing that if @{term "\<forall>a \<in> supp x. a \<sharp> p"} implies @{term "p \<bullet> x = x"}. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1500 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1501 |
Finally, our implementation of sorted atoms turned out powerful enough to |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1502 |
use it for representing variables that carry on additional information, for |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1503 |
example typing annotations. This information is encoded into the sorts. With |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1504 |
this we can represent conveniently binding in ``Church-style'' lambda-terms |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1505 |
and HOL-based languages. While dealing with such additional information in |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1506 |
dependent type-theories, such as LF or Coq, is straightforward, we are not |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1507 |
aware of any other approach in a non-dependent HOL-setting that can deal |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1508 |
conveniently with such binders. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1509 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1510 |
The formalisation presented here will eventually become part of the Isabelle |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1511 |
distribution, but for the moment it can be downloaded from the |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1512 |
Mercurial repository linked at |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1513 |
\href{http://isabelle.in.tum.de/nominal/download} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1514 |
{http://isabelle.in.tum.de/nominal/download}.\smallskip |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1515 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1516 |
\noindent |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1517 |
{\bf Acknowledgements:} We are very grateful to Jesper Bengtson, Stefan |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1518 |
Berghofer and Cezary Kaliszyk for their comments on earlier versions |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1519 |
of this paper. We are also grateful to the anonymous referee who helped us to |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1520 |
put the work into the right context. |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1521 |
*} |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1522 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1523 |
|
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1524 |
(*<*) |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1525 |
end |
95df71c3df2f
added new paper directory for further work
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1526 |
(*>*) |