# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269326600 -3600
# Node ID 7cebb576fae3fb71cef5b0d546f72e31a1770f3f
# Parent  b6da798cef68e323df7b171aaf004499a2861a52# Parent  d804729d6cf4ba9fc45210cf2a9f2670e3b53f00
merged

diff -r d804729d6cf4 -r 7cebb576fae3 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Tue Mar 23 07:04:27 2010 +0100
+++ b/Nominal/Abs.thy	Tue Mar 23 07:43:20 2010 +0100
@@ -118,22 +118,6 @@
   by (rule_tac x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma alpha_gen_swap_fun:
-  assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"
-  assumes a1: "a \<notin> (f x) - bs"
-  and     a2: "b \<notin> (f x) - bs"
-  shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"
-  apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)
-  apply(simp add: alpha_gen)
-  apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])
-  apply(simp add: swap_set_not_in[OF a1 a2])
-  apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")
-  using a1 a2
-  apply(simp add: fresh_star_def fresh_def)
-  apply(blast)
-  apply(simp add: supp_swap)
-  done
-
 fun
   supp_abs_fun
 where
diff -r d804729d6cf4 -r 7cebb576fae3 Nominal/Term5.thy
--- a/Nominal/Term5.thy	Tue Mar 23 07:04:27 2010 +0100
+++ b/Nominal/Term5.thy	Tue Mar 23 07:43:20 2010 +0100
@@ -71,22 +71,121 @@
 "(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
 (alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
+apply (tactic {* symp_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms alpha5_eqvt} @{context} 1 *})
+done
+
+lemma alpha5_symp1:
+"(a \<approx>5 b \<longrightarrow> b \<approx>5 a) \<and>
+(x \<approx>l y \<longrightarrow> y \<approx>l x) \<and>
+(alpha_rbv5 x y \<longrightarrow> alpha_rbv5 y x)"
 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
-apply (simp only: alpha5_inj)
-apply (simp add: alpha5_inj)
+apply (simp_all add: alpha5_inj)
 apply (erule exE)
-apply (simp only: alpha5_inj)
 apply (rule_tac x="- pi" in exI)
-apply (erule alpha_gen_compose_sym2)
-apply (simp_all add: alpha5_inj eqvts alpha5_eqvt)
+apply (simp add: alpha_gen)
+  apply(simp add: fresh_star_def fresh_minus_perm)
+apply clarify
+apply (rule conjI)
+apply (rotate_tac 3)
+apply (frule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (rule conjI)
+apply (rotate_tac 5)
+apply (frule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 6)
+apply simp
+apply (drule_tac p1="- pi" in permute_eq_iff[symmetric,THEN iffD1])
+apply (simp)
+done
+
+thm alpha_gen_sym[no_vars]
+thm alpha_gen_compose_sym[no_vars]
+
+lemma tt: 
+  "\<lbrakk>R (- p \<bullet> x) y \<Longrightarrow> R (p \<bullet> y) x; (bs, x) \<approx>gen R f (- p) (cs, y)\<rbrakk> \<Longrightarrow> (cs, y) \<approx>gen R f p (bs, x)"
+  unfolding alphas
+  unfolding fresh_star_def
+  by (auto simp add:  fresh_minus_perm)
+
+lemma alpha5_symp2:
+  shows "a \<approx>5 b \<Longrightarrow> b \<approx>5 a"
+  and   "x \<approx>l y \<Longrightarrow> y \<approx>l x"
+  and   "alpha_rbv5 x y \<Longrightarrow> alpha_rbv5 y x"
+apply(induct rule:  alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* binding case *)
+apply(simp add: alpha5_inj)
+apply(erule exE)
+apply(rule_tac x="- pi" in exI)
+apply(rule tt)
+apply(simp add: alphas)
+apply(erule conjE)+
+apply(drule_tac p="- pi" in alpha5_eqvt(2))
+apply(drule_tac p="- pi" in alpha5_eqvt(2))
+apply(drule_tac p="- pi" in alpha5_eqvt(1))
+apply(drule_tac p="- pi" in alpha5_eqvt(1))
+apply(simp)
+apply(simp add: alphas)
+apply(erule conjE)+
+apply metis
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
+(* non-binding case *)
+apply(simp add: alpha5_inj)
 done
 
 lemma alpha5_transp:
 "(a \<approx>5 b \<longrightarrow> (\<forall>c. b \<approx>5 c \<longrightarrow> a \<approx>5 c)) \<and>
 (x \<approx>l y \<longrightarrow> (\<forall>z. y \<approx>l z \<longrightarrow> x \<approx>l z)) \<and>
 (alpha_rbv5 k l \<longrightarrow> (\<forall>m. alpha_rbv5 l m \<longrightarrow> alpha_rbv5 k m))"
-apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})
+(*apply (tactic {* transp_tac @{context} @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} [] @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{thms alpha5_eqvt} 1 *})*)
+apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct)
+apply (rule_tac [!] allI)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+defer
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
+apply (simp_all add: alpha5_inj)
+apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+(* HERE *)
+(*
+apply(rule alpha_gen_trans)
+thm alpha_gen_trans
+defer
+apply (simp add: alpha_gen)
+apply clarify
+apply(simp add: fresh_star_plus)
+apply (rule conjI)
+apply (erule_tac x="- pi \<bullet> rltsaa" in allE)
+apply (rotate_tac 5)
+apply (drule_tac p="- pi" in alpha5_eqvt(2))
+apply simp
+apply (drule_tac p="pi" in alpha5_eqvt(2))
+apply simp
+apply (erule_tac x="- pi \<bullet> rtrm5aa" in allE)
+apply (rotate_tac 7)
+apply (drule_tac p="- pi" in alpha5_eqvt(1))
+apply simp
+apply (rotate_tac 3)
+apply (drule_tac p="pi" in alpha5_eqvt(1))
+apply simp
 done
+*)
+sorry
 
 lemma alpha5_equivp:
   "equivp alpha_rtrm5"
diff -r d804729d6cf4 -r 7cebb576fae3 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 23 07:04:27 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 07:43:20 2010 +0100
@@ -54,8 +54,8 @@
   also there one would like to bind multiple variables at once.
 
   Binding multiple variables has interesting properties that cannot be captured
-  easily by iterating single binders. For example in the case of type-schemes we do not
-  like to make a distinction about the order of the bound variables. Therefore
+  easily by iterating single binders. For example in case of type-schemes we do not
+  want to make a distinction about the order of the bound variables. Therefore
   we would like to regard the following two type-schemes as alpha-equivalent
   %
   \begin{equation}\label{ex1}
@@ -63,14 +63,15 @@
   \end{equation}
 
   \noindent
-  but  the following two should \emph{not} be alpha-equivalent
+  but assuming that $x$, $y$ and $z$ are distinct variables,
+  the following two should \emph{not} be alpha-equivalent
   %
   \begin{equation}\label{ex2}
   \forall \{x, y\}. x \rightarrow y  \;\not\approx_\alpha\; \forall \{z\}. z \rightarrow z 
   \end{equation}
 
   \noindent
-  assuming that $x$, $y$ and $z$ are distinct. Moreover, we like to regard type-schemes as 
+  Moreover, we like to regard type-schemes as 
   alpha-equivalent, if they differ only on \emph{vacuous} binders, such as
   %
   \begin{equation}\label{ex3}
@@ -87,7 +88,7 @@
 
   However, the notion of alpha-equivalence that is preserved by vacuous binders is not
   always wanted. For example in terms like
-
+  %
   \begin{equation}\label{one}
   \LET x = 3 \AND y = 2 \IN x\,-\,y \END
   \end{equation}
@@ -96,7 +97,7 @@
   we might not care in which order the assignments $x = 3$ and $y = 2$ are
   given, but it would be unusual to regard \eqref{one} as alpha-equivalent 
   with
-
+  %
   \begin{center}
   $\LET x = 3 \AND y = 2 \AND z = loop \IN x\,-\,y \END$
   \end{center}
@@ -109,7 +110,7 @@
   However, we found that this is still not sufficient for dealing with
   language constructs frequently occurring in programming language
   research. For example in $\mathtt{let}$s containing patterns
-
+  %
   \begin{equation}\label{two}
   \LET (x, y) = (3, 2) \IN x\,-\,y \END
   \end{equation}
@@ -118,7 +119,7 @@
   we want to bind all variables from the pattern inside the body of the
   $\mathtt{let}$, but we also care about the order of these variables, since
   we do not want to regard \eqref{two} as alpha-equivalent with
-
+  %
   \begin{center}
   $\LET (y, x) = (3, 2) \IN x\,- y\,\END$
   \end{center}
@@ -131,7 +132,7 @@
   By providing these general binding mechanisms, however, we have to work around 
   a problem that has been pointed out by Pottier in \cite{Pottier06}: in 
   $\mathtt{let}$-constructs of the form
-
+  %
   \begin{center}
   $\LET x_1 = t_1 \AND \ldots \AND x_n = t_n \IN s \END$
   \end{center}
@@ -141,7 +142,7 @@
   which the $x_i = t_i$ are given, but we do care about the information that there are 
   as many $x_i$ as there are $t_i$. We lose this information if we represent the 
   $\mathtt{let}$-constructor by something like 
-
+  %
   \begin{center}
   $\LET [x_1,\ldots,x_n].s\;\; [t_1,\ldots,t_n]$
   \end{center}
@@ -154,7 +155,7 @@
   lists are of equal length. This can result into very messy reasoning (see
   for example~\cite{BengtsonParow09}). To avoid this, we will allow type specifications
   for $\mathtt{let}$s as follows
-
+  %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
   $trm$ & $::=$  & \ldots\\ 
@@ -385,10 +386,10 @@
 section {* General Binders *}
 
 text {*
-  In Nominal Isabelle the user is expected to write down a specification of a
-  term-calculus and a reasoning infrastructure is then automatically derived
+  In Nominal Isabelle, the user is expected to write down a specification of a
+  term-calculus and then a reasoning infrastructure is automatically derived
   from this specifcation (remember that Nominal Isabelle is a definitional
-  extension of Isabelle/HOL and cannot introduce new axioms).
+  extension of Isabelle/HOL, which does not introduce any new axioms).
 
 
   In order to keep our work manageable, we will wherever possible state
@@ -508,11 +509,50 @@
   \begin{proof}
   All properties are by unfolding the definitions and simple calculations. 
   \end{proof}
+
+
+  \begin{lemma}
+  $supp ([as]set. x) = supp x - as$ 
+  \end{lemma}
 *}
 
 section {* Alpha-Equivalence and Free Variables *}
 
 text {*
+  A specification of a term-calculus in Nominal Isabelle is a collection
+  of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ 
+  written as follows:
+
+  \begin{center}
+  \begin{tabular}{l}
+  \isacommand{nominal\_datatype} $ty_1 =$\\
+  \isacommand{and} $ty_2 =$\\
+  $\ldots$\\ 
+  \isacommand{and} $ty_n =$\\ 
+  $\ldots$\\
+  \isacommand{with}\\
+  $\ldots$\\
+  \end{tabular}
+  \end{center}
+
+  \noindent
+  The section below the \isacommand{with} are binding functions, which
+  will be explained below.
+  
+
+
+  A specification of a term-calculus in Nominal Isabell is very similar to 
+  the usual datatype definition of Isabelle/HOL: 
+
+
+  Because of the problem Pottier pointed out in \cite{Pottier06}, the general 
+  binders from the previous section cannot be used directly to represent w 
+  be used directly 
+*}
+
+
+
+text {*
   Restrictions
 
   \begin{itemize}