src/HOL/Nominal/Examples/W.thy

--- a/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 13:24:45 2008 +0100
+++ b/src/HOL/Nominal/Examples/W.thy	Sat Dec 13 16:26:06 2008 +0100
@@ -1,5 +1,3 @@
-(* "$Id$" *)
-
 theory W
 imports Nominal
 begin
@@ -50,26 +48,68 @@
   Ctxt  = "(var\<times>tyS) list" 
 
 text {* free type variables *}
-consts
-  ftv    :: "'a \<Rightarrow> tvar list"
+
+class ftv = type +
+  fixes ftv :: "'a \<Rightarrow> tvar list"
+
+instantiation * :: (ftv, ftv) ftv
+begin
+
+primrec ftv_prod
+where
+ "ftv (x::'a::ftv, y::'b::ftv) = (ftv x)@(ftv y)"
+
+instance ..
+
+end
 
-primrec (ftv_of_prod)
- "ftv (x,y) = (ftv x)@(ftv y)"
+instantiation tvar :: ftv
+begin
+
+definition
+  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
 
-defs (overloaded)
-  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
+instance ..
+
+end
+
+instantiation var :: ftv
+begin
+
+definition
   ftv_of_var[simp]:   "ftv (x::var) \<equiv> []" 
 
-primrec (ftv_of_list)
+instance ..
+
+end
+
+instantiation list :: (ftv) ftv
+begin
+
+primrec ftv_list
+where
   "ftv [] = []"
-  "ftv (x#xs) = (ftv x)@(ftv xs)"
+| "ftv (x#xs) = (ftv x)@(ftv xs)"
+
+instance ..
+
+end
 
 (* free type-variables of types *)
-nominal_primrec (ftv_ty)
+
+instantiation ty :: ftv
+begin
+
+nominal_primrec ftv_ty
+where
   "ftv (TVar X) = [X]"
-  "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
+| "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ftv_ty_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   T::"ty"
@@ -77,9 +117,13 @@
 by (nominal_induct T rule: ty.strong_induct)
    (perm_simp add: append_eqvt)+
 
-nominal_primrec (ftv_tyS)
+instantiation tyS :: ftv
+begin
+
+nominal_primrec ftv_tyS
+where
   "ftv (Ty T)    = ftv T"
-  "ftv (\<forall>[X].S) = (ftv S) - [X]"
+| "ftv (\<forall>[X].S) = (ftv S) - [X]"
 apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
 apply(rule TrueI)+
 apply(rule difference_fresh)
@@ -87,6 +131,10 @@
 apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
 done
 
+instance ..
+
+end
+
 lemma ftv_tyS_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   S::"tyS"
@@ -140,11 +188,11 @@
 
 types Subst = "(tvar\<times>ty) list"
 
-consts
- psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
+class psubst =
+  fixes psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
 
 abbreviation 
-  subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
+  subst :: "'a::psubst \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 where
   "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
 
@@ -159,11 +207,19 @@
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
 
-nominal_primrec (psubst_ty)
+instantiation ty :: psubst
+begin
+
+nominal_primrec psubst_ty
+where
   "\<theta><TVar X>   = lookup \<theta> X"
-  "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
+| "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma psubst_ty_eqvt[eqvt]:
   fixes pi1::"tvar prm"
   and   \<theta>::"Subst"