--- a/Nominal/Abs.thy Sat Mar 27 16:20:39 2010 +0100
+++ b/Nominal/Abs.thy Mon Mar 29 00:30:47 2010 +0200
@@ -120,37 +120,6 @@
apply(rule_tac [!] x="p \<bullet> pa" in exI)
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
-fun
- aux_set
-where
- "aux_set (bs, x) = (supp x) - bs"
-
-fun
- aux_list
-where
- "aux_list (cs, x) = (supp x) - (set cs)"
-
-lemma aux_abs_lemma:
- assumes a: "(bs, x) \<approx>abs (cs, y)"
- shows "aux_set (bs, x) = aux_set (cs, y)"
- using a
- by (induct rule: alpha_abs.induct)
- (simp add: alphas_abs alphas)
-
-lemma aux_abs_res_lemma:
- assumes a: "(bs, x) \<approx>abs_res (cs, y)"
- shows "aux_set (bs, x) = aux_set (cs, y)"
- using a
- by (induct rule: alpha_abs_res.induct)
- (simp add: alphas_abs alphas)
-
-lemma aux_abs_list_lemma:
- assumes a: "(bs, x) \<approx>abs_lst (cs, y)"
- shows "aux_list (bs, x) = aux_list (cs, y)"
- using a
- by (induct rule: alpha_abs_lst.induct)
- (simp add: alphas_abs alphas)
-
quotient_type
'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
@@ -188,24 +157,13 @@
unfolding fun_rel_def
by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
-lemma [quot_respect]:
- shows "(alpha_abs ===> op=) aux_set aux_set"
- and "(alpha_abs_res ===> op=) aux_set aux_set"
- and "(alpha_abs_lst ===> op=) aux_list aux_list"
- unfolding fun_rel_def
- apply(rule_tac [!] allI)
- apply(rule_tac [!] allI)
- apply(case_tac [!] x, case_tac [!] y)
- apply(rule_tac [!] impI)
- by (simp_all only: aux_abs_lemma aux_abs_res_lemma aux_abs_list_lemma)
-
-lemma abs_inducts:
- shows "(\<And>as (x::'a::pt). P1 (Abs as x)) \<Longrightarrow> P1 x1"
- and "(\<And>as (x::'a::pt). P2 (Abs_res as x)) \<Longrightarrow> P2 x2"
- and "(\<And>as (x::'a::pt). P3 (Abs_lst as x)) \<Longrightarrow> P3 x3"
- by (lifting prod.induct[where 'a="atom set" and 'b="'a"]
- prod.induct[where 'a="atom set" and 'b="'a"]
- prod.induct[where 'a="atom list" and 'b="'a"])
+lemma abs_exhausts:
+ shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+ and "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
+ and "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
+ by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
+ prod.exhaust[where 'a="atom set" and 'b="'a"]
+ prod.exhaust[where 'a="atom list" and 'b="'a"])
lemma abs_eq_iff:
shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
@@ -230,7 +188,7 @@
instance
apply(default)
- apply(induct_tac [!] x rule: abs_inducts(1))
+ apply(case_tac [!] x rule: abs_exhausts(1))
apply(simp_all)
done
@@ -251,7 +209,7 @@
instance
apply(default)
- apply(induct_tac [!] x rule: abs_inducts(2))
+ apply(case_tac [!] x rule: abs_exhausts(2))
apply(simp_all)
done
@@ -272,7 +230,7 @@
instance
apply(default)
- apply(induct_tac [!] x rule: abs_inducts(3))
+ apply(case_tac [!] x rule: abs_exhausts(3))
apply(simp_all)
done
@@ -317,37 +275,52 @@
unfolding permute_abs
by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
-quotient_definition
- "supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
-is
- "aux_set"
+function
+ supp_gen :: "('a::pt) abs_gen \<Rightarrow> atom set"
+where
+ "supp_gen (Abs as x) = supp x - as"
+apply(case_tac x rule: abs_exhausts(1))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
-quotient_definition
- "supp_res :: ('a::pt) abs_res \<Rightarrow> atom set"
-is
- "aux_set"
+termination supp_gen
+ by (auto intro!: local.termination)
-quotient_definition
- "supp_lst :: ('a::pt) abs_lst \<Rightarrow> atom set"
-is
- "aux_list"
+function
+ supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
+where
+ "supp_res (Abs_res as x) = supp x - as"
+apply(case_tac x rule: abs_exhausts(2))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
+
+termination supp_res
+ by (auto intro!: local.termination)
-lemma aux_supps:
- shows "supp_gen (Abs bs x) = (supp x) - bs"
- and "supp_res (Abs_res bs x) = (supp x) - bs"
- and "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
- by (lifting aux_set.simps aux_set.simps aux_list.simps)
+function
+ supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
+where
+ "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
+apply(case_tac x rule: abs_exhausts(3))
+apply(simp)
+apply(simp add: abs_eq_iff alphas_abs alphas)
+done
-lemma aux_supp_eqvt[eqvt]:
+termination supp_lst
+ by (auto intro!: local.termination)
+
+lemma [eqvt]:
shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
and "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
and "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
- apply(induct_tac x rule: abs_inducts(1))
- apply(simp add: aux_supps supp_eqvt Diff_eqvt)
- apply(induct_tac y rule: abs_inducts(2))
- apply(simp add: aux_supps supp_eqvt Diff_eqvt)
- apply(induct_tac z rule: abs_inducts(3))
- apply(simp add: aux_supps supp_eqvt Diff_eqvt set_eqvt)
+ apply(case_tac x rule: abs_exhausts(1))
+ apply(simp add: supp_eqvt Diff_eqvt)
+ apply(case_tac y rule: abs_exhausts(2))
+ apply(simp add: supp_eqvt Diff_eqvt)
+ apply(case_tac z rule: abs_exhausts(3))
+ apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
done
lemma aux_fresh:
@@ -364,7 +337,7 @@
and "(supp x) - as \<subseteq> supp (Abs_res as x)"
and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
unfolding supp_conv_fresh
- apply(auto dest!: aux_fresh simp add: aux_supps)
+ apply(auto dest!: aux_fresh)
apply(simp_all add: fresh_def supp_finite_atom_set a)
done
@@ -397,19 +370,19 @@
instance abs_gen :: (fs) fs
apply(default)
- apply(induct_tac x rule: abs_inducts(1))
+ apply(case_tac x rule: abs_exhausts(1))
apply(simp add: supp_abs finite_supp)
done
instance abs_res :: (fs) fs
apply(default)
- apply(induct_tac x rule: abs_inducts(2))
+ apply(case_tac x rule: abs_exhausts(2))
apply(simp add: supp_abs finite_supp)
done
instance abs_lst :: (fs) fs
apply(default)
- apply(induct_tac x rule: abs_inducts(3))
+ apply(case_tac x rule: abs_exhausts(3))
apply(simp add: supp_abs finite_supp)
done
@@ -422,7 +395,6 @@
unfolding supp_abs
by auto
-
section {* BELOW is stuff that may or may not be needed *}
(* support of concrete atom sets *)
--- a/Paper/Paper.thy Sat Mar 27 16:20:39 2010 +0100
+++ b/Paper/Paper.thy Mon Mar 29 00:30:47 2010 +0200
@@ -41,7 +41,7 @@
\end{center}
\noindent
- where free and bound variables have names. For such terms Nominal Isabelle
+ where free and bound variables have names. For such alpha-equated terms, Nominal Isabelle
derives automatically a reasoning infrastructure that has been used
successfully in formalisations of an equivalence checking algorithm for LF
\cite{UrbanCheneyBerghofer08}, Typed
@@ -52,8 +52,8 @@
binding \cite{SatoPollack10}.
However, Nominal Isabelle has fared less well in a formalisation of
- the algorithm W \cite{UrbanNipkow09}, where types and type-schemes
- are of the form
+ the algorithm W \cite{UrbanNipkow09}, where types and type-schemes,
+ respectively, are of the form
%
\begin{equation}\label{tysch}
\begin{array}{l}
@@ -171,7 +171,8 @@
where the notation @{text "[_]._"} indicates that the @{text "x\<^isub>i"}
become bound in @{text s}. In this representation the term
\mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} would be a perfectly legal
- instance. To exclude such terms, additional predicates about well-formed
+ instance, but the lengths of two lists do not agree. To exclude such terms,
+ additional predicates about well-formed
terms are needed in order to ensure that the two lists are of equal
length. This can result into very messy reasoning (see for
example~\cite{BengtsonParow09}). To avoid this, we will allow type
@@ -190,7 +191,7 @@
\noindent
where @{text assn} is an auxiliary type representing a list of assignments
and @{text bn} an auxiliary function identifying the variables to be bound
- by the @{text "\<LET>"}. This function is defined by recursion over @{text
+ by the @{text "\<LET>"}. This function can be defined by recursion over @{text
assn} as follows
\begin{center}
@@ -238,7 +239,9 @@
only support specifications that make sense on the level of alpha-equated
terms (offending specifications, which for example bind a variable according
to a variable bound somewhere else, are not excluded by Ott, but we have
- to). Our insistence on reasoning with alpha-equated terms comes from the
+ to).
+
+ Our insistence on reasoning with alpha-equated terms comes from the
wealth of experience we gained with the older version of Nominal Isabelle:
for non-trivial properties, reasoning about alpha-equated terms is much
easier than reasoning with raw terms. The fundamental reason for this is
@@ -311,7 +314,7 @@
\end{center}
\noindent
- then with not too great effort we obtain a function @{text "fv\<^sup>\<alpha>"}
+ then with the help of te quotient package we obtain a function @{text "fv\<^sup>\<alpha>"}
operating on quotients, or alpha-equivalence classes of lambda-terms. This
lifted function is characterised by the equations
@@ -325,18 +328,20 @@
(Note that this means also the term-constructors for variables, applications
and lambda are lifted to the quotient level.) This construction, of course,
only works if alpha-equivalence is indeed an equivalence relation, and the lifted
- definitions and theorems are respectful w.r.t.~alpha-equivalence. Accordingly, we
+ definitions and theorems are respectful w.r.t.~alpha-equivalence. For exmple, we
will not be able to lift a bound-variable function, which can be defined for
- raw terms, to alpha-equated terms
- (since it does not respect alpha-equivalence). To sum up, every lifting of
+ raw terms. The reason is that this function does not respect alpha-equivalence.
+ To sum up, every lifting of
theorems to the quotient level needs proofs of some respectfulness
- properties. In the paper we show that we are able to automate these
+ properties (see \cite{Homeier05}). In the paper we show that we are able to
+ automate these
proofs and therefore can establish a reasoning infrastructure for
alpha-equated terms.
The examples we have in mind where our reasoning infrastructure will be
- immeasurably helpful is what is often referred to as Core-Haskell (see
- Figure~\ref{corehas}). There terms include patterns which include a list of
+ helpful is the term language of System @{text "F\<^isub>C"}, also known as
+ Core-Haskell (see Figure~\ref{corehas}). This term language has patterns
+ which include lists of
type- and term- variables (the arguments of constructors) all of which are
bound in case expressions. One difficulty is that each of these variables
come with a kind or type annotation. Representing such binders with single
@@ -355,8 +360,45 @@
have the variable convention already built in.
\begin{figure}
-
- \caption{Core Haskell.\label{corehas}}
+ \begin{boxedminipage}{\linewidth}
+ \begin{center}
+ \begin{tabular}{l}
+ Type Kinds\\
+ @{text "\<kappa> ::= \<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\\
+ Coercion Kinds\\
+ @{text "\<iota> ::= \<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\\
+ Types\\
+ @{text "\<sigma> ::= a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"}\\
+ @{text "| \<forall>a:\<kappa>. \<sigma> "}\\
+ ??? Type equality\\
+ Coercion Types\\
+ @{text "\<gamma> ::= a | C | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}\\
+ @{text "| \<forall>a:\<iota>. \<gamma>"}\\
+ ??? Coercion Type equality\\
+ @{text "| sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | left \<gamma> | right \<gamma> | \<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 "}\\
+ @{text "| rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\\
+ Terms\\
+ @{text "e ::= x | K | \<Lambda>a:\<kappa>. e | \<Lambda>a:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+ @{text "| \<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2"}\\
+ @{text "| \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+ @{text "| \<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$\\
+ @{text "| e \<triangleright> \<gamma>"}\\
+ Patterns\\
+ @{text "p ::= K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\\
+ Constants\\
+ @{text C} coercion constant\\
+ @{text T} value type constructor\\
+ @{text "S\<^isub>n"} n-ary type function\\
+ @{text K} data constructor\\
+ Variables\\
+ @{text a} type variable\\
+ @{text x} term variable\\
+ \end{tabular}
+ \end{center}
+ \end{boxedminipage}
+ \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell,
+ according to \cite{CoreHaskell}. We only made an issential modification by
+ separating the grammars for type kinds and coercion types.\label{corehas}}
\end{figure}
*}
@@ -455,7 +497,7 @@
given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
set"}}, then @{text x} and @{text y} need to have the same set of free
variables; moreover there must be a permutation @{text p} such that {\it
- ii)} it leaves the free variables of @{text x} and @{text y} unchanged, but
+ ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
{\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
@{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
@@ -463,7 +505,7 @@
%
\begin{equation}\label{alphaset}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>gen R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
& @{term "fv(x) - as = fv(y) - bs"}\\
@{text "\<and>"} & @{term "(fv(x) - as) \<sharp>* p"}\\
@{text "\<and>"} & @{text "(p \<bullet> x) R y"}\\
@@ -489,7 +531,7 @@
%
\begin{equation}\label{alphalist}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
& @{term "fv(x) - (set as) = fv(y) - (set bs)"}\\
\wedge & @{term "(fv(x) - set as) \<sharp>* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
@@ -507,14 +549,13 @@
%
\begin{equation}\label{alphares}
\begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l}
- \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"} @{text "\<equiv>"}\hspace{30mm}}\\[1mm]
+ \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fv p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}\hspace{30mm}}\\[1mm]
& @{term "fv(x) - as = fv(y) - bs"}\\
\wedge & @{term "(fv(x) - as) \<sharp>* p"}\\
\wedge & @{text "(p \<bullet> x) R y"}\\
\end{array}
\end{equation}
- \begin{exmple}\rm
It might be useful to consider some examples for how these definitions of alpha-equivalence
pan out in practise.
For this consider the case of abstracting a set of variables over types (as in type-schemes).
@@ -526,20 +567,21 @@
\noindent
Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
- \eqref{ex3}. It can be easily checked that @{text "({x,y}, x \<rightarrow> y)"} and
- @{text "({y,x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
+ \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
+ @{text "({y, x}, y \<rightarrow> x)"} are equal according to $\approx_{\textit{set}}$ and
$\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
- $\not\approx_{\textit{list}}$ @{text "([y,x], x \<rightarrow> y)"} since there is no permutation
+ $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
- @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x,y}, x)"} which holds by
+ @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by
taking @{text p} to be the
identity permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
- $\not\approx_{\textit{set}}$ @{text "({x,y}, x)"} since there is no permutation
+ $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation
that makes the
- sets @{text "{x}"} and @{text "{x,y}"} equal (similarly for $\approx_{\textit{list}}$).
- \end{exmple}
+ sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
+ It can also relatively easily be shown that all tree notions of alpha-equivalence
+ coincide, if we only abstract a single atom.
% looks too ugly
%\noindent
@@ -569,22 +611,26 @@
%\end{proof}
- In the rest of this section we are going to introduce a type- and term-constructor
- for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$
- and $\approx_{\textit{abs\_res}}$)
+ In the rest of this section we are going to introduce a type- and term-constructors
+ for abstraction. For this we define
%
\begin{equation}
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
\end{equation}
\noindent
- We can show that these relations are equivalence relations and equivariant
- (we only show the $\approx_{\textit{abs\_set}}$-case).
+ (similarly for $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$). We can show that these relations are equivalence
+ relations and equivariant.
- \begin{lemma}\label{alphaeq}
- $\approx_{\textit{abs\_set}}$ is an equivalence
+ \begin{lemma}\label{alphaeq} The relations
+ $\approx_{\textit{abs\_set}}$,
+ $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$
+ are equivalence
relations, and if @{term "abs_set (as, x) (bs, y)"} then also
- @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"}.
+ @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for
+ the other two relations).
\end{lemma}
\begin{proof}
@@ -595,29 +641,10 @@
calculations.
\end{proof}
- \noindent
- We are also define the following two auxiliary functions taking a pair
- as argument.
- %
- \begin{equation}\label{aux}
- \begin{array}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
- @{text "aux (as, x)"} & @{text "\<equiv>"} & @{text "supp x - as"}\\
- @{text "aux_list (bs, x)"} & @{text "\<equiv>"} & @{text "supp x - set bs"}
- \end{array}
- \end{equation}
-
\noindent
- The point of these two functions is that they are preserved under
- alpha-equivalence, that means for instance
- %
- \begin{equation}\label{auxpreserved}
- @{term "abs_set (as, x) (bs, y)"} \;\;\text{implies}\;\;
- @{term "aux (as, x) = aux (bs, y)"}
- \end{equation}
-
- Lemma \ref{alphaeq} allows us to use our quotient package and introduce
+ This lemma allows us to use our quotient package and introduce
new types @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
- representing the alpha-equivalence classes. Elements in these types
+ representing alpha-equivalence classes of pairs. The elements in these types
we will, respectively, write as:
\begin{center}
@@ -627,31 +654,71 @@
\end{center}
\noindent
- By definition we have
+ indicating that a set or list is abstracted in @{text x}. We will call the types
+ \emph{abstraction types} and their elements \emph{abstractions}. The important
+ property we need is a characterisation for the support of abstractions, namely
+ \begin{thm}[Support of Abstractions]\label{suppabs}
+ Assuming @{text x} has finite support, then
\begin{center}
- @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;iff\;
- @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
+ @{thm (lhs) supp_abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_abs(1)[no_vars]}\\
+ @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}\\
+ @{thm (lhs) supp_abs(3)[no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[no_vars]}
+ \end{tabular}
\end{center}
-
+ \end{thm}
\noindent
- The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
- $\approx_{\textit{abs\_res}}$) will be crucial below:
+ We will only show in the rest of the section the first equation, as the others
+ follow similar arguments. By definition of the abstraction type @{text "abs_set"}
+ we have
+ %
+ \begin{equation}\label{abseqiff}
+ @{thm (lhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\text{if and only if}\;
+ @{thm (rhs) abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+ \end{equation}
+
+ \noindent
+ With this, we can show the following lemma about swapping two atoms (the permutation
+ operation for abstractions is the one lifted for pairs).\footnote{metion this in the nominal
+ logic section}
\begin{lemma}
@{thm[mode=IfThen] abs_swap1(1)[no_vars]}
\end{lemma}
\begin{proof}
- This lemma is straightforward by observing that the assumptions give us
+ By using \eqref{abseqiff}, this lemma is straightforward when observing that
+ the assumptions give us
@{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
- is equivariant.
+ and set difference are equivariant.
\end{proof}
+ \noindent
+ This lemma gives us
+ %
+ \begin{equation}\label{halfone}
+ @{thm abs_supports(1)[no_vars]}
+ \end{equation}
+
+ \noindent
+ which with \ref{} gives us one half of Thm~\ref{suppabs}. The other half is
+ a bit more involved. We first define an auxiliary function
+ %
+ \begin{center}
+ @{thm supp_res.simps[THEN eq_reflection, no_vars]}
+ \end{center}
+
+
\begin{lemma}
$supp ([as]set. x) = supp x - as$
\end{lemma}
+
+ \noindent
+ The point of these general lemmas about pairs is that we can define and prove properties
+ about them conveninently on the Isabelle level, and in addition can use them in what
+ follows next when we have to deal with specific instances of term-specification.
*}
section {* Alpha-Equivalence and Free Variables *}