--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/PaperTest.thy	Fri May 13 14:50:17 2011 +0100
@@ -0,0 +1,235 @@
+theory PaperTest
+imports "../Nominal2"
+begin
+
+atom_decl name 
+
+datatype trm = 
+  Const "string"
+| Var "name"
+| App "trm" "trm"
+| Lam "name" "trm"  ("Lam [_]. _" [100, 100] 100)
+
+fun
+  subst :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"  ("_[_::=_]" [100,100,100] 100)
+where
+  "(Var x)[y::=p] = (if x=y then (App (App (Const ''unpermute'') (Var p)) (Var x)) else (Var x))"
+| "(App t\<^isub>1 t\<^isub>2)[y::=p] = App (t\<^isub>1[y::=p]) (t\<^isub>2[y::=p])"
+| "(Lam [x].t)[y::=p] = (if x=y then (Lam [x].t) else Lam [x].(t[y::=p]))"
+| "(Const n)[y::=p] = Const n"
+
+datatype utrm = 
+  UConst "string"
+| UnPermute "name" "name"
+| UVar "name"
+| UApp "utrm" "utrm"
+| ULam "name" "utrm"  ("ULam [_]. _" [100, 100] 100)
+
+fun
+  usubst :: "utrm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> utrm"  ("_[_:::=_]" [100,100,100] 100)
+where
+  "(UVar x)[y:::=p] = (if x=y then UnPermute x p else (UVar x))"
+| "(UApp t\<^isub>1 t\<^isub>2)[y:::=p] = UApp (t\<^isub>1[y:::=p]) (t\<^isub>2[y:::=p])"
+| "(ULam [x].t)[y:::=p] = (if x=y then (ULam [x].t) else ULam [x].(t[y:::=p]))"
+| "(UConst n)[y:::=p] = UConst n"
+| "(UnPermute x q)[y:::=p] = UnPermute x q"
+
+function
+  ss :: "trm \<Rightarrow> nat"
+where
+  "ss (Var x) = 1"
+| "ss (Const s) = 1"
+| "ss (Lam [x].t) = 1 + ss t"
+| "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1"
+| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2"
+defer
+apply(simp_all)
+apply(auto)[1]
+apply(case_tac x)
+apply(simp_all)
+apply(auto)
+apply(blast)
+done
+
+termination
+  apply(relation "measure (\<lambda>t. size t)")
+  apply(simp_all)
+  done
+
+fun
+  uss :: "utrm \<Rightarrow> nat"
+where
+  "uss (UVar x) = 1"
+| "uss (UConst s) = 1"
+| "uss (ULam [x].t) = 1 + uss t"
+| "uss (UnPermute x y) = 1"
+| "uss (UApp t1 t2) = 1 + uss t1 + uss t2"
+
+lemma trm_uss:
+  shows "uss (t[x:::=p]) = uss t"
+apply(induct rule: uss.induct)
+apply(simp_all)
+done
+
+inductive
+  ufree :: "utrm \<Rightarrow> bool"
+where
+  "ufree (UVar x)"
+| "s \<noteq> ''unpermute'' \<Longrightarrow> ufree (UConst s)"
+| "ufree t \<Longrightarrow> ufree (ULam [x].t)"
+| "ufree (UnPermute x y)"
+| "\<lbrakk>ufree t1; ufree t2\<rbrakk> \<Longrightarrow> ufree (UApp t1 t2)"
+
+fun
+  trans :: "utrm \<Rightarrow> trm" ("\<parallel>_\<parallel>" [100] 100)
+where
+  "\<parallel>(UVar x)\<parallel> = Var x"
+| "\<parallel>(UConst x)\<parallel> = Const x"
+| "\<parallel>(UnPermute p x)\<parallel> = (App (App (Const ''unpermute'') (Var p)) (Var x))"
+| "\<parallel>(ULam [x].t)\<parallel> = Lam [x].(\<parallel>t\<parallel>)"
+| "\<parallel>(UApp t1 t2)\<parallel> = App (\<parallel>t1\<parallel>) (\<parallel>t2\<parallel>)"
+
+lemma elim1:
+  "ufree t \<Longrightarrow> \<parallel>t\<parallel> \<noteq>(Const ''unpermute'')"
+apply(erule ufree.induct)
+apply(auto)
+done
+
+lemma elim2:
+  "ufree t \<Longrightarrow> \<not>(\<exists>p. \<parallel>t\<parallel> = App (Const ''unpermute'') (Var p))"
+apply(erule ufree.induct)
+apply(auto dest: elim1)
+done
+
+lemma
+  "ufree t \<Longrightarrow> uss t = ss (\<parallel>t\<parallel>)"
+apply(erule ufree.induct)
+apply(simp_all)
+apply(subst ss.simps)
+apply(auto)
+apply(drule elim2)
+apply(auto)
+done
+
+
+fun
+  fr :: "trm \<Rightarrow> name set"
+where
+  "fr (Var x) = {x}"
+| "fr (Const s) = {}"
+| "fr (Lam [x].t) = fr t - {x}"
+| "fr (App t1 t2) = fr t1 \<union> fr t2"
+
+function
+  sfr :: "trm \<Rightarrow> name set"
+where
+  "sfr (Var x) = {}"
+| "sfr (Const s) = {}"
+| "sfr (Lam [x].t) = sfr t - {x}"
+| "sfr (App (App (Const ''unpermute'') (Var p)) (Var x)) = {p, x}"
+| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> sfr (App t1 t2) = sfr t1 \<union> sfr t2"
+defer
+apply(simp_all)
+apply(auto)[1]
+apply(case_tac x)
+apply(simp_all)
+apply(auto)
+apply(blast)
+done
+
+termination
+  apply(relation "measure (\<lambda>t. size t)")
+  apply(simp_all)
+  done
+
+function
+  ss :: "trm \<Rightarrow> nat"
+where
+  "ss (Var x) = 1"
+| "ss (Const s) = 1"
+| "ss (Lam [x].t) = 1 + ss t"
+| "ss (App (App (Const ''unpermute'') (Var p)) (Var x)) = 1"
+| "\<not>(\<exists>p x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x)) \<Longrightarrow> ss (App t1 t2) = 1 + ss t1 + ss t2"
+defer
+apply(simp_all)
+apply(auto)[1]
+apply(case_tac x)
+apply(simp_all)
+apply(auto)
+apply(blast)
+done 
+
+termination
+  apply(relation "measure (\<lambda>t. size t)")
+  apply(simp_all)
+  done
+
+inductive
+  improper :: "trm \<Rightarrow> bool"
+where
+  "improper (App (App (Const ''unpermute'') (Var p)) (Var x))"
+| "improper p x t \<Longrightarrow> improper p x (Lam [y].t)"
+| "\<lbrakk>improper p x t1; improper p x t2\<rbrakk> \<Longrightarrow> improper p x (App t1 t2)"
+
+lemma trm_ss:
+  shows "\<not>improper p x t \<Longrightarrow> ss (t[x::= p]) = ss t"
+apply(induct rule: ss.induct)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(auto)[1]
+apply(case_tac "improper p x t")
+apply(drule improper.intros(2))
+apply(blast)
+apply(simp)
+using improper.intros(1)
+apply(blast)
+apply(erule contrapos_pn)
+thm contrapos_np
+apply(simp)
+apply(auto)[1]
+apply(simp)
+apply(erule disjE)
+apply(erule conjE)+
+apply(subst ss.simps)
+apply(simp)
+apply(rule disjI1)
+apply(rule allI)
+apply(rule notI)
+
+apply(simp del: ss.simps)
+apply(erule disjE)
+apply(subst ss.simps)
+apply(simp)
+apply(simp only: subst.simps)
+apply(subst ss.simps)
+apply(simp del: ss.simps)
+apply(rule conjI)
+apply(rule impI)
+apply(erule conjE)
+apply(erule exE)+
+apply(subst ss.simps)
+apply(simp)
+apply(auto)[1]
+apply(simp add: if_splits)
+apply()
+
+function
+  simp :: "name \<Rightarrow> trm \<Rightarrow> trm"
+where
+  "simp p (Const c) = (Const c)"
+| "simp p (Var x) = App (App (Const ''permute'') (Var p)) (Var x)"
+| "simp p (App t1 t2) = (if ((\<exists>x. t1 = App (Const ''unpermute'') (Var p) \<and> t2 = (Var x))) 
+                         then t2
+                         else App (simp p t1) (simp p t2))"
+| "simp p (Lam [x].t) = Lam [x]. (simp p (t[x ::= p]))"
+apply(pat_completeness)
+apply(simp_all)
+apply(auto)
+done
+
+termination
+apply(relation "measure (\<lambda>(_, t). size t)")
+apply(simp_all)
+
+end
\ No newline at end of file

--- a/Pearl-jv/Paper.thy	Tue May 10 17:10:22 2011 +0100
+++ b/Pearl-jv/Paper.thy	Fri May 13 14:50:17 2011 +0100
@@ -223,7 +223,7 @@
   \end{proposition}
 
   \noindent
-  This property will be used later on whenever we have to chose a `fresh' atom.
+  This property will be used later whenever we have to chose a `fresh' atom.
 
   For implementing sort-respecting permutations, we use functions of type @{typ
   "atom => atom"} that are bijective; are the
@@ -520,7 +520,7 @@
 
   There are a number of equivalent formulations for the equivariance
   property.  For example, assuming @{text f} is a function of permutation 
-  type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance can also be stated as
+  type @{text "\<alpha> \<Rightarrow> \<beta>"}, then equivariance of @{text f} can also be stated as
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -633,7 +633,7 @@
   \end{isabelle} 
 
   \noindent
-  and consequently, the constant @{text "\<forall>"} must be equivariant. From this
+  which means the constant @{text "\<forall>"} must be equivariant. From this
   we can deduce that the existential quantifier @{text "\<exists>"} is equivariant. 
   Its definition in HOL is
 
@@ -656,7 +656,9 @@
   of reasoning we can build up a database of equivariant constants.
 
   Before we proceed, let us give a justification for the equivariance principle. 
-  For this we will use a rewrite system consisting of a series of equalities 
+  This justification cannot be given directly inside Isabelle/HOL since we cannot
+  prove any statement about HOL-terms. Instead, we will use a rewrite 
+  system consisting of a series of equalities 
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   @{text "\<pi> \<cdot> t  =  ...  =  t'"}
@@ -676,7 +678,7 @@
   results or does not terminate.  We then give a modification in order
   to obtain the desired properties.
 
-  Consider the following oriented equations
+  Consider the following for oriented equations
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
@@ -689,27 +691,16 @@
   \end{isabelle}
 
   \noindent
-  A permutation @{text \<pi>} can be pushed into applications and abstractions as follows
-
-  The first equation we established in \eqref{permutefunapp};
+  These equation are oriented in the sense of being applied in the left-to-right
+  direction. The first equation we established in \eqref{permutefunapp};
   the second follows from the definition of permutations acting on functions
   and the fact that HOL-terms are equal modulo beta-equivalence.
-  Once the permutations are pushed towards the leaves, we need the
-  following two equations
-
-  \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \begin{tabular}{@ {}lr@ {\hspace{3mm}}c@ {\hspace{3mm}}l}
-  
-  \end{tabular}\hfill\numbered{rewriteother}
-  \end{isabelle}
-
-  \noindent
-  in order to remove permuations in front of bound variables and
-  equivariant constants.  Unfortunately, we have to be careful with
-  the rules {\it i)} and {\it iv}): they can lead to a loop whenever
-  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}, where
-  we do not write the permutation operation infix, as usual, but
-  as an application. Recall that we established in Lemma \ref{permutecompose} that the
+  The third is a consequence of \eqref{cancel} and the fourth from 
+  Definition~\ref{equivariance}. Unfortunately, we have to be careful with
+  the rules {\it i)} and {\it iv}) since they can lead to a loop whenever
+  \mbox{@{text "t\<^isub>1 t\<^isub>2"}} is of the form @{text "((op \<bullet>) \<pi>') t"}.\footnote{Note we 
+  deviate here from our usual convention of writing the permutation operation infix, 
+  instead as an application.} Recall that we established in Lemma \ref{permutecompose} that the
   constant @{text "(op \<bullet>)"} is equivariant and consider the infinite
   reduction sequence
 
@@ -725,8 +716,8 @@
   \end{isabelle}
 
   \noindent
-  The last term is again an instance of rewrite rule {\it i}), but the term
-  is bigger.  To avoid this loop we need to apply our rewrite rule
+  where the last term is again an instance of rewrite rule {\it i}), but bigger.  
+  To avoid this loop we will apply the rewrite rule
   using an `outside to inside' strategy.  This strategy is sufficient
   since we are only interested of rewriting terms of the form @{term
   "\<pi> \<bullet> t"}, where an outermost permutation needs to pushed inside a term.
@@ -735,18 +726,20 @@
   iii)} can `overlap'. For this note that the term @{term "\<pi>
   \<bullet>(\<lambda>x. x)"} reduces by {\it ii)} to @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to
   which we can apply rule {\it iii)} in order to obtain @{term
-  "\<lambda>x. x"}, as is desired---there is no free variable in the original
-  term and so the permutation should completely vanish. However, the
+  "\<lambda>x. x"}, as is desired---since there is no free variable in the original
+  term. the permutation should completely vanish. However, the
   subterm @{text "(- \<pi>) \<bullet> x"} is also an application. Consequently,
-  the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can reduce to @{text "\<lambda>x. (- (\<pi>
-  \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}.  Given our strategy we cannot
-  apply rule {\it iii)} anymore and even worse the measure we will
-  introduce shortly increased. On the other hand, if we had started
+  the term @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet>x"} can also reduce to @{text "\<lambda>x. (- (\<pi>
+  \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} using {\it i)}.  Given our strategy, we cannot
+  apply rule {\it iii)} anymore in order to eliminate the permutation. 
+  In contrast, if we start 
   with the term @{text "\<pi> \<bullet> ((- \<pi>) \<bullet> x)"} where @{text \<pi>} and @{text
   x} are free variables, then we \emph{do} want to apply rule {\it i)}
+  in order to obtain @{text "(\<pi> \<bullet> (- \<pi>)) \<bullet> (\<pi> \<bullet> x)"}
   and not rule {\it iii)}. The latter would eliminate @{text \<pi>}
-  completely. The problem is that rule {\it iii)} should only apply to
-  instances where the variable is to bound; for free variables we want
+  completely and thus violating our correctness property. The problem is that 
+  rule {\it iii)} should only apply to
+  instances where the corresponding variable is to bound; for free variables we want
   to use {\it ii)}.  In order to distinguish these cases we have to
   maintain the information which variable is bound when inductively
   taking a term `apart'. This, unfortunately, does not mesh well with
@@ -761,7 +754,7 @@
   \end{isabelle}
 
   \noindent
-  The point is that now we can formulate the rewrite rules as follows
+  The point is that now we can re-formulate the rewrite rules as follows
   
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}lrcl}
@@ -776,9 +769,10 @@
   \end{isabelle}
 
   \noindent
-  and @{text unpermutes} are only generated in case of bound variables.
+  where @{text unpermutes} are only generated in case of bound variables.
   Clearly none of these rules overlap. Moreover, given our
-  outside-to-inside strategy, they terminate. To see this, notice that
+  outside-to-inside strategy, applying them repeatedly must terminate. 
+To see this, notice that
   the permutation on the right-hand side of the rewrite rules is
   always applied to a smaller term, provided we take the measure consisting
   of lexicographically ordered pairs whose first component is the size
@@ -786,15 +780,15 @@
   leaves) and the second is the number of occurences of @{text
   "unpermute \<pi> x"} and @{text "\<pi> \<bullet> c"}.
 
-  With the rules of the conversions tactic in place, we can
+  With the rewrite rules of the conversions tactic in place, we can
   establish its correctness. The property we are after is that 
   for a HOL-term @{text t} whose constants are all equivariant the 
   term \mbox{@{text "\<pi> \<bullet> t"}} is equal to @{text "t'"} with @{text "t'"}
   being equal to @{text t} except that every free variable @{text x}
   in @{text t} is replaced by \mbox{@{text "\<pi> \<bullet> x"}}. Let us call
   a variable @{text x} \emph{really free}, if it is free and not occuring
-  in an unpermute, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
-  We need the following technical notion characterising a \emph{@{text "\<pi>"}-proper} HOL-term
+  in an @{term unpermute}, such as @{text "unpermute _ x"} and @{text "unpermute x _"}.
+  We need the following technical notion characterising \emph{@{text "\<pi>"}-proper} HOL-terms
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
   \begin{tabular}{@ {}ll}

--- a/TODO	Tue May 10 17:10:22 2011 +0100
+++ b/TODO	Fri May 13 14:50:17 2011 +0100
@@ -1,7 +1,11 @@
 Function definitions
 
 - export proofs bout alpha_bn
+- equations like
 
+    | "simp p (App t1 t2) = (if True then (App (simp p t1) (simp p t2)) else t1)"
+
+  do not work
 
 Parser should check that: