--- a/Nominal-General/Atoms.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal-General/Atoms.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -5,6 +5,7 @@
 *)
 theory Atoms
 imports Nominal2_Base
+uses "~~/src/Tools/subtyping.ML"
 begin
 
 
@@ -193,4 +194,29 @@
   unfolding atom_eqvt [symmetric]
   by simp
 
+
+section {* Tests with subtyping and automatic coercions *}
+
+setup Subtyping.setup
+
+atom_decl var1
+atom_decl var2
+
+declare [[coercion "atom::var1\<Rightarrow>atom"]]
+
+declare [[coercion "atom::var2\<Rightarrow>atom"]]
+
+lemma
+  fixes a::"var1" and b::"var2"
+  shows "a \<sharp> t \<and> b \<sharp> t"
+oops
+
+(* does not yet work: it needs image as
+   coercion map *)
+
+lemma
+  fixes as::"var1 set"
+  shows "atom ` as \<sharp>* t"
+oops
+
 end

--- a/Nominal/Ex/Datatypes.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/Ex/Datatypes.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -7,6 +7,7 @@
   atom_decl - example by John Matthews
 *)
 
+(* FIXME: throws an problem with fv-function
 nominal_datatype 'a Maybe = 
   Nothing 
 | Just 'a
@@ -22,6 +23,7 @@
 thm Maybe.fv_bn_eqvt
 thm Maybe.size_eqvt
 thm Maybe.supp
+*)
 
 (*
   using a datatype inside a nominal_datatype

--- a/Nominal/Ex/TypeSchemes.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -4,7 +4,8 @@
 
 section {*** Type Schemes ***}
 
-atom_decl name
+atom_decl name 
+
 
 (* defined as a single nominal datatype *)
 
@@ -50,6 +51,45 @@
 thm tys2.fresh
 
 
+lemma strong_exhaust:
+  fixes c::"'a::fs"
+  assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in tys2.exhaust)
+apply(rename_tac names ty2)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q")
+apply(erule exE)
+apply(perm_simp)
+apply(erule conjE)
+apply(rule assms(1))
+apply(assumption)
+apply(clarify)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+thm at_set_avoiding
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: tys2.fresh)
+done
+
+
+lemma strong_induct:
+  fixes c::"'a::fs"
+  assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)"
+  shows "P c tys"
+using assms
+apply(induction_schema)
+apply(rule_tac y="tys" in strong_exhaust)
+apply(blast)
+apply(relation "measure (\<lambda>(x,y). size y)")
+apply(simp_all add: tys2.size)
+done
+
+
 text {* *}
 
 (*

--- a/Nominal/Ex/TypeVarsTest.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -8,6 +8,7 @@
 class s1
 class s2
 
+(* FIXME
 nominal_datatype ('a, 'b) lam =
   Var "name"
 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam"
@@ -22,7 +23,7 @@
 thm lam.eq_iff
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
-
+*)
 
 end
 

--- a/Nominal/ROOT.ML	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/ROOT.ML	Sat Nov 06 06:18:41 2010 +0000
@@ -1,8 +1,8 @@
 
 
 no_document use_thys
-   ["Ex/Classical",    
-    "Ex/CoreHaskell",
+   ["../Nominal-General/Atoms",
+    "Ex/Classical",    
     "Ex/Datatypes",
     "Ex/Ex1",
     "Ex/ExPS3",
@@ -19,5 +19,7 @@
     "Ex/SingleLet",
     "Ex/TypeSchemes",
     "Ex/TypeVarsTest",
-    "Ex/Foo1"
+    "Ex/Foo1",
+    "Ex/Foo2",
+    "Ex/CoreHaskell"
     ];