--- a/Nominal/Abs.thy Fri Mar 26 22:22:41 2010 +0100
+++ b/Nominal/Abs.thy Fri Mar 26 22:23:22 2010 +0100
@@ -117,33 +117,6 @@
apply(rule_tac [!] x="p \<bullet> pa" in exI)
by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
-lemma alphas_abs_swap1:
- assumes a1: "a \<notin> (supp x) - bs"
- and a2: "b \<notin> (supp x) - bs"
- shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- and "(bs, x) \<approx>abs_res ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- unfolding alphas_abs
- unfolding alphas
- unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
- unfolding fresh_star_def fresh_def
- unfolding swap_set_not_in[OF a1 a2]
- by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
- (auto simp add: supp_perm swap_atom)
-
-lemma alphas_abs_swap2:
- assumes a1: "a \<notin> (supp x) - (set bs)"
- and a2: "b \<notin> (supp x) - (set bs)"
- shows "(bs, x) \<approx>abs_lst ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- unfolding alphas_abs
- unfolding alphas
- unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
- unfolding fresh_star_def fresh_def
- unfolding swap_set_not_in[OF a1 a2]
- by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
- (auto simp add: supp_perm swap_atom)
-
fun
aux_set
where
@@ -227,9 +200,16 @@
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"
- apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
- apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])
- apply(lifting prod.induct[where 'a="atom list" and 'b="'a"])
+ 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_eq_iff:
+ shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+ and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
+ and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
+ apply(simp_all)
+ apply(lifting alphas_abs)
done
instantiation abs_gen :: (pt) pt
@@ -297,6 +277,42 @@
lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemma abs_swap1:
+ assumes a1: "a \<notin> (supp x) - bs"
+ and a2: "b \<notin> (supp x) - bs"
+ shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ unfolding abs_eq_iff
+ unfolding alphas_abs
+ unfolding alphas
+ unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]
+ unfolding fresh_star_def fresh_def
+ unfolding swap_set_not_in[OF a1 a2]
+ using a1 a2
+ by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ (auto simp add: supp_perm swap_atom)
+
+lemma abs_swap2:
+ assumes a1: "a \<notin> (supp x) - (set bs)"
+ and a2: "b \<notin> (supp x) - (set bs)"
+ shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+ unfolding abs_eq_iff
+ unfolding alphas_abs
+ unfolding alphas
+ unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
+ unfolding fresh_star_def fresh_def
+ unfolding swap_set_not_in[OF a1 a2]
+ using a1 a2
+ by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
+ (auto simp add: supp_perm swap_atom)
+
+lemma abs_supports:
+ shows "((supp x) - as) supports (Abs as x)"
+ and "((supp x) - as) supports (Abs_res as x)"
+ and "((supp x) - (set bs)) supports (Abs_lst bs x)"
+ unfolding supports_def
+ unfolding permute_abs
+ by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
quotient_definition
"supp_gen :: ('a::pt) abs_gen \<Rightarrow> atom set"
@@ -317,10 +333,7 @@
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)"
- apply(lifting aux_set.simps)
- apply(lifting aux_set.simps)
- apply(lifting aux_list.simps)
- done
+ by (lifting aux_set.simps aux_set.simps aux_list.simps)
lemma aux_supp_eqvt[eqvt]:
shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
@@ -342,30 +355,6 @@
apply(simp_all add: eqvts_raw)
done
-lemma abs_swap1:
- assumes a1: "a \<notin> (supp x) - bs"
- and a2: "b \<notin> (supp x) - bs"
- shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- and "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2
- apply(lifting alphas_abs_swap1(1))
- apply(lifting alphas_abs_swap1(2))
- done
-
-lemma abs_swap2:
- assumes a1: "a \<notin> (supp x) - (set bs)"
- and a2: "b \<notin> (supp x) - (set bs)"
- shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
- using a1 a2 by (lifting alphas_abs_swap2)
-
-lemma abs_supports:
- shows "((supp x) - as) supports (Abs as x)"
- and "((supp x) - as) supports (Abs_res as x)"
- and "((supp x) - (set bs)) supports (Abs_lst bs x)"
- unfolding supports_def
- unfolding permute_abs
- by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
-
lemma supp_abs_subset1:
assumes a: "finite (supp x)"
shows "(supp x) - as \<subseteq> supp (Abs as x)"
@@ -430,14 +419,6 @@
unfolding supp_abs
by auto
-lemma abs_eq_iff:
- shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
- and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
- and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
- apply(simp_all)
- apply(lifting alphas_abs)
- done
-
section {* BELOW is stuff that may or may not be needed *}
--- a/Paper/Paper.thy Fri Mar 26 22:22:41 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 26 22:23:22 2010 +0100
@@ -6,8 +6,6 @@
consts
fv :: "'a \<Rightarrow> 'b"
abs_set :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
- Abs_lst :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
- Abs_res :: "'a \<Rightarrow> 'b \<Rightarrow> 'c"
definition
"equal \<equiv> (op =)"
@@ -19,9 +17,9 @@
supp ("supp _" [78] 73) and
uminus ("-_" [78] 73) and
If ("if _ then _ else _" 10) and
- alpha_gen ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{set}}$}>\<^bsup>_,_,_\<^esup> _") and
- alpha_lst ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{list}}$}>\<^bsup>_,_,_\<^esup> _") and
- alpha_res ("_ \<approx>\<^raw:\makebox[0mm][l]{$\,_{\textit{res}}$}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_gen ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{set}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_lst ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_,_,_\<^esup> _") and
+ alpha_res ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{res}}$}}>\<^bsup>_,_,_\<^esup> _") and
abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
fv ("fv'(_')" [100] 100) and
equal ("=") and
@@ -412,9 +410,9 @@
\noindent
For a proof see \cite{HuffmanUrban10}.
- \begin{property}
- @{thm[mode=IfThen] at_set_avoiding[no_vars]}
- \end{property}
+ %\begin{property}
+ %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
+ %\end{property}
*}
@@ -444,8 +442,8 @@
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
{\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
- say \mbox{@{text "_ R _"}}, two equal terms. We also require {\it iv)} that
- @{text p} makes the abstracted sets @{text as} and @{text bs} equal. The
+ 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
requirements {\it i)} to {\it iv)} can be stated formally as follows:
%
\begin{equation}\label{alphaset}
@@ -502,7 +500,8 @@
\end{equation}
\begin{exmple}\rm
- It might be useful to consider some examples for how these definitions pan out in practise.
+ 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).
We set @{text R} to be the equality and for @{text "fv(T)"} we define
@@ -556,55 +555,53 @@
In the rest of this section we are going to introduce a type- and term-constructor
- for abstractions. For this we define
+ for abstractions. For this we define (similarly for $\approx_{\textit{abs\_list}}$
+ and $\approx_{\textit{abs\_res}}$)
%
\begin{equation}
@{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
\end{equation}
\noindent
- Similarly for @{text "abs_list"} and @{text "abs_res"}. We can show that these
- relations are equivalence relations and equivariant
+ We can show that these relations are equivalence relations and equivariant
(we only show the $\approx_{\textit{abs\_set}}$-case).
- \begin{lemma}
+ \begin{lemma}\label{alphaeq}
$\approx_{\textit{abs\_set}}$ is an equivalence
- relations, and if @{term "abs_set (as, x) (bs, x)"} then also
- @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> x)"}.
+ 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)"}.
\end{lemma}
\begin{proof}
Reflexivity is by taking @{text "p"} to be @{text "0"}. For symmetry we have
a permutation @{text p} and for the proof obligation take @{term "-p"}. In case
- of transitivity we have two permutations @{text p} and @{text q}, and for the
- proof obligation use @{text "q + p"}. All the conditions are then by simple
+ of transitivity, we have two permutations @{text p} and @{text q}, and for the
+ proof obligation use @{text "q + p"}. All conditions are then by simple
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 following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
- $\approx_{\textit{abs\_res}}$) will be crucial below:
-
- \begin{lemma}
- @{thm[mode=IfThen] alpha_abs_swap[no_vars]}
- \end{lemma}
+ 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}
- \begin{proof}
- This lemma is straightforward by observing that the assumptions give us
- @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
- is equivariant.
- \end{proof}
-
- \noindent
- We are also define the following
-
- @{text "aux (as, x) \<equiv> supp x - as"}
-
-
-
- \noindent
- This allows us to use our quotient package and introduce new types
- @{text "\<beta> abs_set"}, @{text "\<beta> abs_res"} and @{text "\<beta> abs_list"}
+ Lemma \ref{alphaeq} 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
we will, respectively, write as:
@@ -614,6 +611,28 @@
@{term "Abs_res as x"}
\end{center}
+ \noindent
+ By definition we have
+
+ \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]}
+ \end{center}
+
+
+ \noindent
+ The following lemma (and similar ones for $\approx_{\textit{abs\_list}}$ and
+ $\approx_{\textit{abs\_res}}$) will be crucial below:
+
+ \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
+ @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - bs) = (supp x - bs)"} and that @{text supp}
+ is equivariant.
+ \end{proof}
\begin{lemma}
$supp ([as]set. x) = supp x - as$
@@ -1000,6 +1019,13 @@
text {*
Complication when the single scopedness restriction is lifted (two
overlapping permutations)
+
+
+ The formalisation presented here will eventually become part of the
+ Isabelle distribution, but for the moment it can be downloaded from
+ the Mercurial repository linked at
+ \href{http://isabelle.in.tum.de/nominal/download}
+ {http://isabelle.in.tum.de/nominal/download}.\medskip
*}
text {*