# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1364854973 -3600
# Node ID d67a6a48f1c732b2ba1af163f7f4ff91a6b1117a
# Parent  bc2c3a1f87ef43b9eb1dac0c41caba051587bad2
added example for locales (by Tjark Weber)

diff -r bc2c3a1f87ef -r d67a6a48f1c7 Nominal/Ex/Local_Contexts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Local_Contexts.thy	Mon Apr 01 23:22:53 2013 +0100
@@ -0,0 +1,89 @@
+theory Local_Contexts 
+imports "../Nominal2" 
+begin
+
+text {*
+This theory, contributed by Tjark Weber, contains examples 
+and test cases that illustrate the useof Nominal2 in local 
+contexts (locales, type classes, etc.).
+
+As a running example, we use a variant of the untyped lambda-calculus
+whose lambda-binder binds lists of names, rather than single names.
+*}
+
+atom_decl name
+
+nominal_datatype lam = Var name
+                     | App lam lam ("_ \<cdot> _" [110,110] 110)
+                     | Lam xs::"name list" t::lam binds xs in t ("Lam _. _" [100,100] 100)
+
+locale name_subst =
+  fixes name_subst :: "name \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam"
+  assumes name_subst_eqvt [eqvt]:
+    "p \<bullet> name_subst x xs t = name_subst (p \<bullet> x) (p \<bullet> xs) (p \<bullet> t)"
+  and name_subst_fresh: "supp xs \<sharp>* t \<Longrightarrow> supp xs \<sharp>* name_subst x xs t"
+
+lemma set_map_atom_eq_supp: "set (map atom xs) = supp xs"
+by (metis List.finite_set image_set supp_finite_set_at_base supp_set)
+
+lemma atom_image_set_eq_supp: "atom ` set xs = supp xs"
+by (metis image_set set_map_atom_eq_supp)
+
+nominal_primrec (in name_subst)
+  subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120)
+where
+  "(Var x)[xs::=t] = name_subst x xs t"
+| "(s \<cdot> t)[xs::=u] = s[xs::=u] \<cdot> t[xs::=u]"
+| "\<lbrakk>supp xs \<sharp>* ys; supp xs \<sharp>* u\<rbrakk> \<Longrightarrow> (Lam xs. t)[ys::=u] = Lam xs. t[ys::=u]"
+        apply auto
+-- {* 3 subgoals *}
+  -- {* eqvt *}
+  apply (unfold eqvt_def subst_graph_def subst_graph_aux_def)
+  apply (rule, perm_simp, rule)
+ -- {* exhaustion *}
+ apply (rule_tac y=a and c="(aa, b)" in lam.strong_exhaust)
+   apply auto
+ apply (metis atom_image_set_eq_supp fresh_star_Pair)
+-- {* well-defined (compatibility) *}
+apply (rename_tac xs' ys u t')
+apply (erule Abs_lst_fcb2)
+    apply (metis Abs_fresh_star(3) subset_refl)
+   apply (metis fresh_star_Pair set_map_atom_eq_supp)
+  apply (metis fresh_star_Pair set_map_atom_eq_supp)
+ apply (auto simp add: eqvt_at_def)
+ apply (metis Pair_eqvt perm_supp_eq)
+apply (metis Pair_eqvt perm_supp_eq)
+done
+
+termination (in name_subst) (eqvt) by lexicographic_order
+
+inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90)
+where
+  redex: "supp xs \<sharp>* u \<Longrightarrow> (Lam xs. t) \<cdot> u \<longrightarrow>\<^sub>\<beta> t[xs::=u]"
+| "s \<longrightarrow>\<^sub>\<beta> s' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s' \<cdot> t"
+| "t \<longrightarrow>\<^sub>\<beta> t' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s \<cdot> t'"
+
+equivariance (in name_subst) beta
+
+
+lemma lam_bound_fresh: "supp xs \<sharp>* (Lam xs. t)"
+by (simp add: atom_image_set_eq_supp fresh_star_def)
+
+
+lemma (in name_subst) subst_fresh: "supp xs \<sharp>* u \<Longrightarrow> supp xs \<sharp>* t[xs::=u]"
+apply (nominal_induct t avoiding: xs u rule: lam.strong_induct)
+  apply (simp_all add: atom_image_set_eq_supp)
+  apply (metis name_subst_fresh)
+ apply (metis fresh_star_def lam.fresh(2))
+apply (simp add: fresh_star_def)
+done
+
+nominal_inductive (in name_subst) beta
+avoids
+  redex: xs
+apply (auto simp add: fresh_star_Pair)
+ apply (metis atom_image_set_eq_supp fresh_star_def lam.fresh(2) lam_bound_fresh)
+apply (simp add: atom_image_set_eq_supp subst_fresh)
+done
+
+end
diff -r bc2c3a1f87ef -r d67a6a48f1c7 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Wed Mar 27 17:23:00 2013 +0000
+++ b/Nominal/ROOT.ML	Mon Apr 01 23:22:53 2013 +0100
@@ -28,7 +28,8 @@
     "Ex/Foo2",
     "Ex/CoreHaskell",
     "Ex/CoreHaskell2",
-    "Ex/Pi"
+    "Ex/Pi",
+    "Ex/Local_Contexts"
    ];
 
 quick_and_dirty := true;
diff -r bc2c3a1f87ef -r d67a6a48f1c7 ROOT
--- a/ROOT	Wed Mar 27 17:23:00 2013 +0000
+++ b/ROOT	Mon Apr 01 23:22:53 2013 +0100
@@ -34,6 +34,7 @@
     "Ex/CoreHaskell"
     "Ex/CoreHaskell2"
     "Ex/Pi"
+    "Ex/Local_Contexts"
   theories [quick_and_dirty]
     "Ex/Let"