# HG changeset patch # User Christian Urban # Date 1305294617 -3600 # Node ID 8412c7e503d4dfe321f47b5371b1de1ea8d47e51 # Parent 2cb34b1e7e1961316a42ad5be87c425254125864 misc diff -r 2cb34b1e7e19 -r 8412c7e503d4 Nominal/Ex/PaperTest.thy --- /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 \ name \ name \ 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 \ name \ name \ 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 \ 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" +| "\(\p x. t1 = App (Const ''unpermute'') (Var p) \ t2 = (Var x)) \ 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 (\t. size t)") + apply(simp_all) + done + +fun + uss :: "utrm \ 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 \ bool" +where + "ufree (UVar x)" +| "s \ ''unpermute'' \ ufree (UConst s)" +| "ufree t \ ufree (ULam [x].t)" +| "ufree (UnPermute x y)" +| "\ufree t1; ufree t2\ \ ufree (UApp t1 t2)" + +fun + trans :: "utrm \ trm" ("\_\" [100] 100) +where + "\(UVar x)\ = Var x" +| "\(UConst x)\ = Const x" +| "\(UnPermute p x)\ = (App (App (Const ''unpermute'') (Var p)) (Var x))" +| "\(ULam [x].t)\ = Lam [x].(\t\)" +| "\(UApp t1 t2)\ = App (\t1\) (\t2\)" + +lemma elim1: + "ufree t \ \t\ \(Const ''unpermute'')" +apply(erule ufree.induct) +apply(auto) +done + +lemma elim2: + "ufree t \ \(\p. \t\ = App (Const ''unpermute'') (Var p))" +apply(erule ufree.induct) +apply(auto dest: elim1) +done + +lemma + "ufree t \ uss t = ss (\t\)" +apply(erule ufree.induct) +apply(simp_all) +apply(subst ss.simps) +apply(auto) +apply(drule elim2) +apply(auto) +done + + +fun + fr :: "trm \ name set" +where + "fr (Var x) = {x}" +| "fr (Const s) = {}" +| "fr (Lam [x].t) = fr t - {x}" +| "fr (App t1 t2) = fr t1 \ fr t2" + +function + sfr :: "trm \ 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}" +| "\(\p x. t1 = App (Const ''unpermute'') (Var p) \ t2 = (Var x)) \ sfr (App t1 t2) = sfr t1 \ 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 (\t. size t)") + apply(simp_all) + done + +function + ss :: "trm \ 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" +| "\(\p x. t1 = App (Const ''unpermute'') (Var p) \ t2 = (Var x)) \ 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 (\t. size t)") + apply(simp_all) + done + +inductive + improper :: "trm \ bool" +where + "improper (App (App (Const ''unpermute'') (Var p)) (Var x))" +| "improper p x t \ improper p x (Lam [y].t)" +| "\improper p x t1; improper p x t2\ \ improper p x (App t1 t2)" + +lemma trm_ss: + shows "\improper p x t \ 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 \ trm \ 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 ((\x. t1 = App (Const ''unpermute'') (Var p) \ 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 (\(_, t). size t)") +apply(simp_all) + +end \ No newline at end of file diff -r 2cb34b1e7e19 -r 8412c7e503d4 Pearl-jv/Paper.thy --- 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 "\ \ \"}, then equivariance can also be stated as + type @{text "\ \ \"}, 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 "\"} must be equivariant. From this + which means the constant @{text "\"} must be equivariant. From this we can deduce that the existential quantifier @{text "\"} 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 "\ \ 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 \} 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 \) \') 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 \) \') 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 \)"} 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 "\ \ 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 "\ \(\x. x)"} reduces by {\it ii)} to @{term "\x. \ \ (- \) \ x"}, to which we can apply rule {\it iii)} in order to obtain @{term - "\x. x"}, as is desired---there is no free variable in the original - term and so the permutation should completely vanish. However, the + "\x. x"}, as is desired---since there is no free variable in the original + term. the permutation should completely vanish. However, the subterm @{text "(- \) \ x"} is also an application. Consequently, - the term @{term "\x. \ \ (- \) \x"} can reduce to @{text "\x. (- (\ - \ \)) \ (\ \ 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 "\x. \ \ (- \) \x"} can also reduce to @{text "\x. (- (\ + \ \)) \ (\ \ 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 "\ \ ((- \) \ x)"} where @{text \} and @{text x} are free variables, then we \emph{do} want to apply rule {\it i)} + in order to obtain @{text "(\ \ (- \)) \ (\ \ x)"} and not rule {\it iii)}. The latter would eliminate @{text \} - 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 \ x"} and @{text "\ \ 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 "\ \ 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 "\ \ 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 "\"}-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 "\"}-proper} HOL-terms \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% \begin{tabular}{@ {}ll} diff -r 2cb34b1e7e19 -r 8412c7e503d4 TODO --- 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: