# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285667771 14400
# Node ID 11133eb76f61a524f47bd31ddd1e36ce39a10bfd
# Parent  2e174807c89107efe92d60921e1524cb6daddc52
added Foo1 to explore a contrived example

diff -r 2e174807c891 -r 11133eb76f61 Nominal/Ex/Foo1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Foo1.thy	Tue Sep 28 05:56:11 2010 -0400
@@ -0,0 +1,49 @@
+theory Foo1
+imports "../Nominal2" 
+begin
+
+(* 
+  Contrived example that has more than one
+  binding function for a datatype
+*)
+
+atom_decl name
+
+nominal_datatype foo: trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
+| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
+| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
+and assg =
+  As "name" "name" "trm"
+binder
+  bn1::"assg \<Rightarrow> atom list" and
+  bn2::"assg \<Rightarrow> atom list" and
+  bn3::"assg \<Rightarrow> atom list"
+where
+  "bn1 (As x y t) = [atom x]"
+| "bn2 (As x y t) = [atom y]"
+| "bn3 (As x y t) = [atom x, atom y]"
+
+thm foo.distinct
+thm foo.induct
+thm foo.inducts
+thm foo.exhaust
+thm foo.fv_defs
+thm foo.bn_defs
+thm foo.perm_simps
+thm foo.eq_iff
+thm foo.fv_bn_eqvt
+thm foo.size_eqvt
+thm foo.supports
+thm foo.fsupp
+thm foo.supp
+thm foo.fresh
+
+
+end
+
+
+
diff -r 2e174807c891 -r 11133eb76f61 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Mon Sep 27 12:19:17 2010 -0400
+++ b/Nominal/Ex/Let.thy	Tue Sep 28 05:56:11 2010 -0400
@@ -18,7 +18,7 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-
+thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
@@ -36,6 +36,54 @@
   apply(simp_all)
   done
 
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw p (ANil_raw) = ANil_raw"
+| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
+  apply simp_all
+  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
+  apply simp_all
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma uu:
+  shows "alpha_bn (permute_bn p as) as"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+done
+
+lemma tt:
+  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+thm trm_assn.supp
+
+lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
+apply(simp add: fresh_def)
+apply(simp add: fresh_star_def)
+oops
 
 inductive
     test_trm :: "trm \<Rightarrow> bool"
@@ -51,7 +99,6 @@
 declare trm_assn.fv_bn_eqvt[eqvt]
 equivariance test_trm
 
-(*
 lemma 
   fixes p::"perm"
   shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
@@ -74,23 +121,29 @@
 apply(rule test_trm_test_assn.intros)
 apply(assumption)
 apply(assumption)
-apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
+apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
+apply(drule_tac c="()" in at_set_avoiding2)
+apply(simp add: supp_Unit)
+prefer 2
+apply(assumption)
+apply(simp add: finite_supp)
+apply(erule exE)
+apply(erule conjE)
+apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
+               s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
 apply(rule trm_assn.eq_iff(4)[THEN iffD2])
+apply(simp add: uu)
+apply(drule supp_perm_eq)
+apply(simp add: tt)
+apply(rule test_trm_test_assn.intros(4))
 defer
-apply(rule test_trm_test_assn.intros)
-prefer 3
-apply(simp add: fresh_star_def trm_assn.fresh)
-thm freshs
---"HERE"
-
-thm supps
-apply(rule test_trm_test_assn.intros)
-apply(assumption)
-
-apply(assumption)
+apply(subst permute_plus[symmetric])
+apply(blast)
+oops
 
 
-
+(* 
 lemma 
   fixes t::trm
   and   as::assn
diff -r 2e174807c891 -r 11133eb76f61 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Mon Sep 27 12:19:17 2010 -0400
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Sep 28 05:56:11 2010 -0400
@@ -25,6 +25,7 @@
 thm ty_tys.size_eqvt
 thm ty_tys.supports
 thm ty_tys.supp
+thm ty_tys.fresh
 
 (* defined as two separate nominal datatypes *)
 
@@ -46,7 +47,7 @@
 thm tys2.size_eqvt
 thm tys2.supports
 thm tys2.supp
-
+thm tys2.fresh
 
 
 text {* *}
diff -r 2e174807c891 -r 11133eb76f61 Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Mon Sep 27 12:19:17 2010 -0400
+++ b/Nominal/ROOT.ML	Tue Sep 28 05:56:11 2010 -0400
@@ -18,5 +18,6 @@
     "Ex/Modules",
     "Ex/SingleLet",
     "Ex/TypeSchemes",
-    "Ex/TypeVarsTest"
+    "Ex/TypeVarsTest",
+    "Ex/Foo1"
     ];