src/HOL/Nominal/Examples/Crary.thy

-(* "$Id$" *)
 (*                                                    *)
 (* Formalisation of the chapter on Logical Relations  *)
 (* and a Case Study in Equivalence Checking           *)
 (* by Karl Crary from the book on Advanced Topics in  *)
 (* Types and Programming Languages, MIT Press 2005    *)

 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
 by (induct T rule:ty.induct) (auto)
 
-instance ty :: size ..
-
-nominal_primrec
+instantiation ty :: size
+begin
+
+nominal_primrec size_ty
+where
   "size (TBase) = 1"
-  "size (TUnit) = 1"
-  "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
+| "size (TUnit) = 1"
+| "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
 by (rule TrueI)+
+
+instance ..
+
+end
 
 lemma ty_size_greater_zero[simp]:
   fixes T::"ty"
   shows "size T > 0"
 by (nominal_induct rule: ty.strong_induct) (simp_all)

   assumes a: "z\<sharp>\<theta>"
   shows "lookup \<theta> z = Var z"
 using a
 by (induct rule: lookup.induct)
    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
-
-consts
-  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
  
 nominal_primrec
+  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
+where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
-  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
-  "\<theta><(Const n)> = Const n"
-  "\<theta><(Unit)> = Unit"
+| "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
+| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
+| "\<theta><(Const n)> = Const n"
+| "\<theta><(Unit)> = Unit"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
 apply(fresh_guess)+
 done