# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316593821 -7200
# Node ID 9133086a08173100bb80e9e55e1ab8645df0f78b
# Parent  833d65c6ad88c1600f6c86e3f7d947d9bdf52270# Parent  c46def7dc4a79d42f33fcd8df83630cc273d46ed
merged

diff -r c46def7dc4a7 -r 9133086a0817 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 17:28:19 2011 +0900
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 10:30:21 2011 +0200
@@ -764,7 +764,8 @@
   permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
   (similarly for $\approx_{\,\textit{list}}$).  It can also relatively easily be
   shown that all three notions of alpha-equivalence coincide, if we only
-  abstract a single atom.
+  abstract a single atom. In this case they also agree with alpha-equivalence
+  used in older versions of Nominal Isabelle \cite{Urban08}.
 
   In the rest of this section we are going to show that the alpha-equivalences
   really lead to abstractions where some atoms are bound (or more precisely
@@ -1121,12 +1122,10 @@
   \hspace{5mm}$\mid$~@{text "Let_pat p::pat trm t::trm"} 
      \;\;\isacommand{binds} @{text "bn(p)"} \isacommand{in} @{text t}\\
   \isacommand{and} @{text pat} $=$\\
-  \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
-  \hspace{5mm}$\mid$~@{text "PVar name"}\\
+  \hspace{5mm}\phantom{$\mid$}~@{text "PVar name"}\\
   \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
-  \isacommand{where}~@{text "bn(PNil) = []"}\\
-  \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
+  \isacommand{where}~@{text "bn(PVar x) = [atom x]"}\\
   \hspace{5mm}$\mid$~@{text "bn(PTup p\<^isub>1 p\<^isub>2) = bn(p\<^isub>1) @ bn(p\<^isub>2)"}\smallskip\\ 
   \end{tabular}}
   \end{equation}\smallskip
@@ -1156,12 +1155,12 @@
  
   \begin{equation}\label{letrecs}
   \mbox{%
-  \begin{tabular}{@ {}l@ {}}
+  \begin{tabular}{@ {}l@ {}l}
   \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
-     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
+     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
-     \;\;\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
+     & \hspace{-19mm}\isacommand{binds} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
   \isacommand{and} @{text "assn"} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
   \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
@@ -1919,7 +1918,7 @@
   \infer{P}
   {\begin{array}{l}
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. y = C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k \<Rightarrow> P"}\\
-  \hspace{5mm}\ldots\\
+  \hspace{5mm}\vdots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. y = C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l \<Rightarrow> P"}\\
   \end{array}}
   \end{equation}\smallskip
@@ -1934,7 +1933,7 @@
   \infer{@{text "P\<^isub>1 y\<^isub>1 \<and> \<dots> \<and> P\<^isub>n y\<^isub>n "}}
   {\begin{array}{l}
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>k. P\<^isub>i x\<^isub>i \<and> \<dots> \<and> P\<^isub>j x\<^isub>j \<Rightarrow> P (C\<AL>\<^isub>1 x\<^isub>1 \<dots> x\<^isub>k)"}\\
-  \hspace{5mm}\ldots\\
+  \hspace{5mm}\vdots\\
   @{text "\<forall>x\<^isub>1\<dots>x\<^isub>l. P\<^isub>r x\<^isub>r \<and> \<dots> \<and> P\<^isub>s x\<^isub>s \<Rightarrow> P (C\<AL>\<^isub>m x\<^isub>1 \<dots> x\<^isub>l)"}\\
   \end{array}}
   \end{equation}\smallskip
@@ -1972,7 +1971,6 @@
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
   {\begin{array}{@ {}l@ {}}
-   @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
   \end{array}}\medskip\\
@@ -1985,7 +1983,6 @@
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (App\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>trm\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub> (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>trm\<^esub> x\<^isub>2 \<and> P\<^bsub>trm\<^esub> x\<^isub>3 \<Rightarrow> P\<^bsub>trm\<^esub> (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "P\<^bsub>pat\<^esub> (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x. P\<^bsub>pat\<^esub> (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. P\<^bsub>pat\<^esub> x\<^isub>1 \<and> P\<^bsub>pat\<^esub> x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub> (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
   \end{array}}
@@ -2137,7 +2134,6 @@
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. atom x\<^isub>1 # c \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>trm\<^esub> c (Lam\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3 c. (set (bn\<^sup>\<alpha> x\<^isub>1)) #\<^sup>* c \<and>"}\\ 
    \hspace{10mm}@{text "(\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>2) \<and> (\<forall>d. P\<^bsub>trm\<^esub> d x\<^isub>3) \<Rightarrow> P\<^bsub>trm\<^esub> c (Let_pat\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 x\<^isub>3)"}\\
-   @{text "\<forall>c. P\<^bsub>pat\<^esub> c (PNil\<^sup>\<alpha>)"}\\
    @{text "\<forall>x c. P\<^bsub>pat\<^esub> c (PVar\<^sup>\<alpha> x)"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2 c. (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>1) \<and> (\<forall>d. P\<^bsub>pat\<^esub> d x\<^isub>2) \<Rightarrow> P\<^bsub>pat\<^esub> c (PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2)"}
   \end{array}}
@@ -2200,7 +2196,6 @@
 
   \infer{@{text "P\<^bsub>pat\<^esub>"}}
   {\begin{array}{@ {}l@ {}}
-   @{text "y = PNil\<^sup>\<alpha>  \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x. y = PVar\<^sup>\<alpha> x \<Rightarrow> P\<^bsub>pat\<^esub>"}\\
    @{text "\<forall>x\<^isub>1 x\<^isub>2. y = PTup\<^sup>\<alpha> x\<^isub>1 x\<^isub>2 \<Rightarrow> P\<^bsub>pat\<^esub>"}
   \end{array}}
diff -r c46def7dc4a7 -r 9133086a0817 Nominal/Ex/LetFun.thy
--- a/Nominal/Ex/LetFun.thy	Wed Sep 21 17:28:19 2011 +0900
+++ b/Nominal/Ex/LetFun.thy	Wed Sep 21 10:30:21 2011 +0200
@@ -34,6 +34,7 @@
 thm exp_pat.eq_iff
 thm exp_pat.fv_bn_eqvt
 thm exp_pat.size_eqvt
+thm exp_pat.size
 thm exp_pat.supports
 thm exp_pat.fsupp
 thm exp_pat.supp
diff -r c46def7dc4a7 -r 9133086a0817 Nominal/Ex/LetPat.thy
--- a/Nominal/Ex/LetPat.thy	Wed Sep 21 17:28:19 2011 +0900
+++ b/Nominal/Ex/LetPat.thy	Wed Sep 21 10:30:21 2011 +0200
@@ -7,28 +7,96 @@
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"       binds (set) x in t
-| Let p::"pat" "trm" t::"trm"  binds (set) "f p" in t
+| Lam x::"name" t::"trm"       binds x in t
+| Let p::"pat" "trm" t::"trm"  binds "bn p" in t
 and pat =
-  PN
-| PS "name"
-| PD "name" "name"
+  PNil
+| PVar "name"
+| PTup "pat" "pat"
 binder
-  f::"pat \<Rightarrow> atom set"
+  bn::"pat \<Rightarrow> atom list"
 where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
+  "bn PNil = []"
+| "bn (PVar x) = [atom x]"
+| "bn (PTup p1 p2) = bn p1 @ bn p2"
 
+thm trm_pat.eq_iff
 thm trm_pat.distinct
 thm trm_pat.induct
+thm trm_pat.strong_induct[no_vars]
 thm trm_pat.exhaust
+thm trm_pat.strong_exhaust[no_vars]
 thm trm_pat.fv_defs
 thm trm_pat.bn_defs
 thm trm_pat.perm_simps
 thm trm_pat.eq_iff
 thm trm_pat.fv_bn_eqvt
-thm trm_pat.size_eqvt
+thm trm_pat.size
+
+(* Nominal_Abs test *)
+
+lemma alpha_res_alpha_set:
+  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> 
+  (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+
+
+lemma
+  fixes x::"'a::fs"
+  assumes "(supp x - as) \<sharp>* p"
+      and "p \<bullet> x = y"
+      and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y"
+  shows "(as, x) \<approx>res (op =) supp p (bs, y)"
+  using assms
+  unfolding alpha_res_alpha_set
+  unfolding alphas
+  apply simp
+  apply rule
+  apply (rule trans)
+  apply (rule supp_perm_eq[symmetric, of _ p])
+  apply(subst supp_finite_atom_set)
+  apply (metis finite_Diff finite_supp)
+  apply (simp add: fresh_star_def)
+  apply blast
+  apply(perm_simp)
+  apply(simp)
+  done
+
+lemma
+  fixes x::"'a::fs"
+  assumes "(supp x - as) \<sharp>* p"
+      and "p \<bullet> x = y"
+      and "p \<bullet> as = bs"
+  shows "(as, x) \<approx>set (op =) supp p (bs, y)"
+  using assms
+  unfolding alphas
+  apply simp
+  apply (rule trans)
+  apply (rule supp_perm_eq[symmetric, of _ p])
+  apply(subst supp_finite_atom_set)
+  apply (metis finite_Diff finite_supp)
+  apply(simp)
+  apply(perm_simp)
+  apply(simp)
+  done
+
+lemma
+  fixes x::"'a::fs"
+  assumes "(supp x - set as) \<sharp>* p"
+      and "p \<bullet> x = y"
+      and "p \<bullet> as = bs"
+  shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
+  using assms
+  unfolding alphas
+  apply simp
+  apply (rule trans)
+  apply (rule supp_perm_eq[symmetric, of _ p])
+  apply(subst supp_finite_atom_set)
+  apply (metis finite_Diff finite_supp)
+  apply(simp)
+  apply(perm_simp)
+  apply(simp)
+  done
 
 
 end
diff -r c46def7dc4a7 -r 9133086a0817 Nominal/Ex/LetRec2.thy
--- a/Nominal/Ex/LetRec2.thy	Wed Sep 21 17:28:19 2011 +0900
+++ b/Nominal/Ex/LetRec2.thy	Wed Sep 21 10:30:21 2011 +0200
@@ -5,26 +5,29 @@
 atom_decl name
 
 nominal_datatype trm =
-  Vr "name"
-| Ap "trm" "trm"
-| Lm x::"name" t::"trm"  binds (set) x in t
-| Lt a::"lts" t::"trm"   binds "bn a" in a t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  binds x in t
+| Let as::"assn" t::"trm"   binds "bn as" in t
+| Let_rec as::"assn" t::"trm"   binds "bn as" in as t
+and assn =
+  ANil
+| ACons "name" "trm" "assn"
 binder
   bn
 where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
+  "bn (ANil) = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
 
+thm trm_assn.eq_iff
+thm trm_assn.supp
 
-thm trm_lts.fv_defs
-thm trm_lts.eq_iff
-thm trm_lts.bn_defs
-thm trm_lts.perm_simps
-thm trm_lts.induct
-thm trm_lts.distinct
+thm trm_assn.fv_defs
+thm trm_assn.eq_iff
+thm trm_assn.bn_defs
+thm trm_assn.perm_simps
+thm trm_assn.induct
+thm trm_assn.distinct
 
 
 
diff -r c46def7dc4a7 -r 9133086a0817 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Wed Sep 21 17:28:19 2011 +0900
+++ b/Nominal/Ex/TypeVarsTest.thy	Wed Sep 21 10:30:21 2011 +0200
@@ -44,6 +44,15 @@
 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
+nominal_datatype 'a foo = 
+  Node x::"name" f::"'a foo" binds x in f
+| Leaf "'a"
+
+term "Leaf"
+
+
+
+
 end
 
 
diff -r c46def7dc4a7 -r 9133086a0817 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Wed Sep 21 17:28:19 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Wed Sep 21 10:30:21 2011 +0200
@@ -564,7 +564,7 @@
         [ etac @{thm exE},
           etac @{thm exE},
           perm_inst_tac ctxt, 
-          resolve_tac @{thms alpha_trans_eqvt}, 
+          resolve_tac @{thms alpha_trans_eqvt},
           atac,
           aatac pred_names ctxt, 
           eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},