# HG changeset patch
# User berghofe
# Date 1164625903 -3600
# Node ID e855f25df0c8e599d099842c6e5905466450b8af
# Parent  4462ee172ef07278c3b6e864121c16e72daab2a4
Adapted to new nominal_primrec command.

diff -r 4462ee172ef0 -r e855f25df0c8 src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Mon Nov 27 12:11:20 2006 +0100
+++ b/src/HOL/Nominal/Examples/Compile.thy	Mon Nov 27 12:11:43 2006 +0100
@@ -104,47 +104,6 @@
 
 text {* capture-avoiding substitution *}
 
-consts
- subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
-
-constdefs 
-  subst_Var :: "name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm"
-  "subst_Var x t' \<equiv> \<lambda>y. (if y=x then t' else (Var y))"
-  
-  subst_App :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_App x t' \<equiv> \<lambda>_ _ r1 r2. App r1 r2"
-
-  subst_Lam :: "name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_Lam x t' \<equiv> \<lambda>a _ r. Lam [a].r"
-
-  subst_Const :: "name \<Rightarrow> trm \<Rightarrow> nat \<Rightarrow> trm"
-  "subst_Const x t' \<equiv> \<lambda>n. Const n"
-
-  subst_Pr :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_Pr x t' \<equiv> \<lambda>_ _ r1 r2. Pr r1 r2"
-
-  subst_Fst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_Fst x t' \<equiv> \<lambda>_ r. Fst r"
-
-  subst_Snd :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_Snd x t' \<equiv> \<lambda>_ r. Snd r"
- 
-  subst_InL :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_InL x t' \<equiv> \<lambda>_ r. InL r"
-
-  subst_InR :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_InR x t' \<equiv> \<lambda>_ r. InR r"
-
-  subst_Case :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
-  "subst_Case x t' \<equiv> \<lambda>_ x _ y _ r r1 r2. Case r of inl x \<rightarrow> r1 | inr y \<rightarrow> r2"
-
-defs(overloaded)
-  subst_def: 
-    "t[x::=t'] \<equiv> trm_rec (subst_Var x t') (subst_Lam x t') (subst_App x t')
-                        (subst_Const x t') (subst_Pr x t') (subst_Fst x t') (subst_Snd x t')
-                         (subst_InL x t') (subst_InR x t') (subst_Case x t') t"
-
-(* FIXME: the next two lemmas need to be in Nominal.thy *)
 lemma perm_if:
   fixes pi::"'a prm"
   shows "pi\<bullet>(if b then c1 else c2) = (if (pi\<bullet>b) then (pi\<bullet>c1) else (pi\<bullet>c2))"
@@ -158,312 +117,109 @@
   apply(simp add: perm_bool perm_bij)
   done
 
-lemma fin_supp_subst:
-  shows "finite ((supp (subst_Var x t))::name set)"
-  and   "finite ((supp (subst_Lam x t))::name set)"
-  and   "finite ((supp (subst_App x t))::name set)"
-  and   "finite ((supp (subst_Const x t))::name set)"
-  and   "finite ((supp (subst_Pr x t))::name set)"
-  and   "finite ((supp (subst_Fst x t))::name set)"
-  and   "finite ((supp (subst_Snd x t))::name set)"
-  and   "finite ((supp (subst_InL x t))::name set)"
-  and   "finite ((supp (subst_InR x t))::name set)"
-  and   "finite ((supp (subst_Case x t))::name set)"
-apply -
-apply(finite_guess add: fs_name1 subst_Var_def perm_if eq_eqvt)
-apply(finite_guess add: fs_name1 subst_Lam_def)
-apply(finite_guess add: fs_name1 subst_App_def)
-apply(finite_guess add: fs_name1 subst_Const_def)
-apply(finite_guess add: fs_name1 subst_Pr_def)
-apply(finite_guess add: fs_name1 subst_Fst_def)
-apply(finite_guess add: fs_name1 subst_Snd_def)
-apply(finite_guess add: fs_name1 subst_InL_def)
-apply(finite_guess add: fs_name1 subst_InR_def)
-apply(finite_guess only: fs_name1 subst_Case_def)
-apply(perm_simp)
-apply(simp)
-done
-
-lemma fcb_subst_Lam:
-  shows "x\<sharp>(subst_Lam y t') x t r"
-  by (simp add: subst_Lam_def abs_fresh)
-
-lemma fcb_subst_Case:
-  assumes a: "x\<sharp>r" "x\<sharp>r2" "y\<sharp>r" "y\<sharp>r1"
-  shows "x\<sharp>(subst_Case z t') e x e1 y e2 r r1 r2"
-  and "y\<sharp>(subst_Case z t') e x e1 y e2 r r1 r2"
-  using a
-  by (simp_all add: subst_Case_def abs_fresh)
-
-lemmas trm_recs = trm.recs[where P="\<lambda>_. True", simplified]
+consts
+  subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 
-lemma subst:
-  shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
-  and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
-  and   "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
-  and   "(Const n)[y::=t'] = Const n"
-  and   "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
-  and   "(Fst e)[y::=t'] = Fst (e[y::=t'])"
-  and   "(Snd e)[y::=t'] = Snd (e[y::=t'])"
-  and   "(InL e)[y::=t'] = InL (e[y::=t'])"
-  and   "(InR e)[y::=t'] = InR (e[y::=t'])"
-  and   "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> 
-         \<Longrightarrow> (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] =
-                                    (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))"
-apply(unfold subst_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_Var_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_App_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 subst_Lam_def)
-apply(fresh_guess add: fs_name1 subst_App_def)
-apply(fresh_guess add: fs_name1 subst_Const_def)
-apply(fresh_guess add: fs_name1 subst_Pr_def)
-apply(fresh_guess add: fs_name1 subst_Fst_def)
-apply(fresh_guess add: fs_name1 subst_Snd_def)
-apply(fresh_guess add: fs_name1 subst_InL_def)
-apply(fresh_guess add: fs_name1 subst_InR_def)
-apply(fresh_guess only: fs_name1 subst_Case_def)
-apply(perm_simp)
-apply(simp, simp)
-apply(simp add: subst_Lam_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_Const_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_Pr_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_Fst_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_Snd_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_InL_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(simp add: subst_InR_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_subst)+
-apply(simp add: fcb_subst_Lam)
-apply(simp add: fcb_subst_Case)
-apply(simp add: fcb_subst_Case)
-apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 subst_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 subst_Lam_def)
-apply(fresh_guess add: fs_name1 subst_Lam_def)
-apply(fresh_guess add: fs_name1 subst_App_def)
-apply(fresh_guess add: fs_name1 subst_App_def)
-apply(fresh_guess add: fs_name1 subst_Const_def)
-apply(fresh_guess add: fs_name1 subst_Const_def)
-apply(fresh_guess add: fs_name1 subst_Pr_def)
-apply(fresh_guess add: fs_name1 subst_Pr_def)
-apply(fresh_guess add: fs_name1 subst_Fst_def)
-apply(fresh_guess add: fs_name1 subst_Fst_def)
-apply(fresh_guess add: fs_name1 subst_Snd_def)
-apply(fresh_guess add: fs_name1 subst_Snd_def)
-apply(fresh_guess add: fs_name1 subst_InL_def)
-apply(fresh_guess add: fs_name1 subst_InL_def)
-apply(fresh_guess add: fs_name1 subst_InR_def)
-apply(fresh_guess add: fs_name1 subst_InR_def)
-apply(fresh_guess only: fs_name1 subst_Case_def)
-apply(perm_simp)
-apply(simp, simp)
-apply(fresh_guess only: fs_name1 subst_Case_def)
-apply(perm_simp)
-apply(simp, simp)
-apply(assumption)+
-apply(simp add: subst_Case_def)
-done
-
-constdefs 
-  subst_IVar :: "name \<Rightarrow> trmI \<Rightarrow> name \<Rightarrow> trmI"
-  "subst_IVar x t' \<equiv> \<lambda>y. (if y=x then t' else (IVar y))"
-  
-  subst_IApp :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_IApp x t' \<equiv> \<lambda>_ _ r1 r2. IApp r1 r2"
-
-  subst_ILam :: "name \<Rightarrow> trmI \<Rightarrow> name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_ILam x t' \<equiv> \<lambda>a _ r. ILam [a].r"
+nominal_primrec
+  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
+  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
+  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+  "(Const n)[y::=t'] = Const n"
+  "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
+  "(Fst e)[y::=t'] = Fst (e[y::=t'])"
+  "(Snd e)[y::=t'] = Snd (e[y::=t'])"
+  "(InL e)[y::=t'] = InL (e[y::=t'])"
+  "(InR e)[y::=t'] = InR (e[y::=t'])"
+  "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
+     (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] =
+       (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))"
+  apply (finite_guess add: fs_name1 perm_if eq_eqvt)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess only: fs_name1)
+  apply perm_simp
+  apply (simp add: supp_unit)
+  apply (rule TrueI)+
+  apply (simp add: abs_fresh)
+  apply (simp_all add: abs_fresh)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess only: fs_name1)
+  apply perm_simp
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess only: fs_name1)
+  apply perm_simp
+  apply (fresh_guess only: fs_name1)
+  apply perm_simp
+  done
 
-  subst_IUnit :: "name \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_IUnit x t' \<equiv> IUnit"
-
-  subst_INat :: "name \<Rightarrow> trmI \<Rightarrow> nat \<Rightarrow> trmI"
-  "subst_INat x t' \<equiv> \<lambda>n. INat n"
-
-  subst_ISucc :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_ISucc x t' \<equiv> \<lambda>_ r. ISucc r"
-
-  subst_IAss :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_IAss x t' \<equiv> \<lambda>_ _ r1 r2. r1\<mapsto>r2"
- 
-  subst_IRef :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_IRef x t' \<equiv> \<lambda>_ r. IRef r"
-
-  subst_ISeq :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_ISeq x t' \<equiv> \<lambda>_ _ r1 r2. ISeq r1 r2"
-
-  subst_Iif :: "name \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "subst_Iif x t' \<equiv> \<lambda>_ _ _ r r1 r2. Iif r r1 r2"
-
-defs(overloaded)
-  subst_trmI_def: 
-    "t[x::=t'] \<equiv> trmI_rec (subst_IVar x t') (subst_ILam x t') (subst_IApp x t')
-                        (subst_IUnit x t') (subst_INat x t') (subst_ISucc x t') (subst_IAss x t')
-                         (subst_IRef x t') (subst_ISeq x t') (subst_Iif x t') t"
-
-lemma fin_supp_Isubst:
-  shows "finite ((supp (subst_IVar x t))::name set)"
-  and   "finite ((supp (subst_ILam x t))::name set)"
-  and   "finite ((supp (subst_IApp x t))::name set)"
-  and   "finite ((supp (subst_INat x t))::name set)"
-  and   "finite ((supp (subst_IUnit x t))::name set)"
-  and   "finite ((supp (subst_ISucc x t))::name set)"
-  and   "finite ((supp (subst_IAss x t))::name set)"
-  and   "finite ((supp (subst_IRef x t))::name set)"
-  and   "finite ((supp (subst_ISeq x t))::name set)"
-  and   "finite ((supp (subst_Iif x t))::name set)"
-apply -
-apply(finite_guess add: fs_name1 subst_IVar_def perm_if eq_eqvt)
-apply(finite_guess add: fs_name1 subst_ILam_def)
-apply(finite_guess add: fs_name1 subst_IApp_def)
-apply(finite_guess add: fs_name1 subst_INat_def)
-apply(finite_guess add: fs_name1 subst_IUnit_def)
-apply(finite_guess add: fs_name1 subst_ISucc_def)
-apply(finite_guess add: fs_name1 subst_IAss_def)
-apply(finite_guess add: fs_name1 subst_IRef_def)
-apply(finite_guess add: fs_name1 subst_ISeq_def)
-apply(finite_guess only: fs_name1 subst_Iif_def)
-apply(perm_simp)
-apply(simp)
-done
-
-lemma fcb_subst_ILam:
-  shows "x\<sharp>(subst_ILam y t') x t r"
-  by (simp add: subst_ILam_def abs_fresh)
-
-lemmas trmI_recs = trmI.recs[where P="\<lambda>_. True", simplified]
-
-lemma Isubst:
-  shows "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
-  and   "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
-  and   "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
-  and   "(INat n)[y::=t'] = INat n"
-  and   "(IUnit)[y::=t'] = IUnit"
-  and   "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
-  and   "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
-  and   "(IRef e)[y::=t'] = IRef (e[y::=t'])"
-  and   "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
-  and   "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
-apply(unfold subst_trmI_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_IVar_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_IApp_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(fresh_guess add: fs_name1 subst_IVar_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 subst_ILam_def)
-apply(fresh_guess add: fs_name1 subst_IApp_def)
-apply(fresh_guess add: fs_name1 subst_IUnit_def)
-apply(fresh_guess add: fs_name1 subst_INat_def)
-apply(fresh_guess add: fs_name1 subst_ISucc_def)
-apply(fresh_guess add: fs_name1 subst_IAss_def)
-apply(fresh_guess add: fs_name1 subst_IRef_def)
-apply(fresh_guess add: fs_name1 subst_ISeq_def)
-apply(fresh_guess only: fs_name1 subst_Iif_def)
-apply(perm_simp)
-apply(simp, simp)
-apply(simp add: subst_ILam_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_INat_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_IUnit_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_ISucc_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_IAss_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_IRef_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_ISeq_def)
-apply(rule trans)
-apply(rule trmI_recs)
-apply(rule fin_supp_Isubst)+
-apply(simp add: fcb_subst_ILam)
-apply(simp add: subst_Iif_def)
-done
+nominal_primrec (Isubst)
+  "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
+  "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
+  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
+  "(INat n)[y::=t'] = INat n"
+  "(IUnit)[y::=t'] = IUnit"
+  "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
+  "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
+  "(IRef e)[y::=t'] = IRef (e[y::=t'])"
+  "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
+  "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
+  apply (finite_guess add: fs_name1 perm_if eq_eqvt)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess only: fs_name1)
+  apply perm_simp
+  apply (simp add: supp_unit)
+  apply (rule TrueI)+
+  apply (simp add: abs_fresh)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess only: fs_name1)
+  apply perm_simp
+  done
 
 lemma Isubst_eqvt:
   fixes pi::"name prm"
@@ -471,8 +227,8 @@
   and   t2::"trmI"
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
-  apply(nominal_induct t1 avoiding: x t2 rule: trmI.induct)
-  apply(simp_all add: Isubst perm_if eq_eqvt fresh_bij)
+  apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
+  apply (simp_all add: Isubst.simps perm_if eq_eqvt fresh_bij)
   done
 
 lemma Isubst_supp:
@@ -480,10 +236,10 @@
   and   t2::"trmI"
   and   x::"name"
   shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})"
-apply(nominal_induct t1 avoiding: x t2 rule: trmI.induct)
-apply(auto simp add: Isubst trmI.supp supp_atm abs_supp supp_nat)
-apply(blast)+
-done
+  apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
+  apply (auto simp add: Isubst.simps trmI.supp supp_atm abs_supp supp_nat)
+  apply blast+
+  done
 
 lemma Isubst_fresh:
   fixes x::"name"
@@ -544,244 +300,85 @@
 
 text {* Translation functions *}
 
-constdefs 
-  trans_data :: "data \<Rightarrow> tyI"
-  "trans_data \<equiv> \<lambda>_. DataI(NatI)"
-  
-  trans_arrow :: "ty \<Rightarrow> ty \<Rightarrow> tyI \<Rightarrow> tyI \<Rightarrow> tyI"
-  "trans_arrow \<equiv> \<lambda>_ _ r1 r2. ArrowI r1 r2"
-
-  trans_type::"ty \<Rightarrow> tyI"  
-  "trans_type \<tau> \<equiv> ty_rec (trans_data) (trans_arrow) \<tau>"
-
-lemmas ty_recs = ty.recs[where P="\<lambda>_. True", simplified]
-
-lemma trans_type:
-  shows "trans_type (Data \<sigma>) = DataI(NatI)"
-  and   "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
-apply(unfold trans_type_def)
-apply(rule trans)
-apply(rule ty_recs)
-apply(simp add: trans_data_def)
-apply(rule trans)
-apply(rule ty_recs)
-apply(simp add: trans_arrow_def)
-done
-
-constdefs 
-  trans_Var :: "name \<Rightarrow> trmI"
-  "trans_Var \<equiv> \<lambda>x. IVar x"
-  
-  trans_App :: "trm \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_App \<equiv> \<lambda>_ _ r1 r2. IApp r1 r2"
-
-  trans_Lam :: "name \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_Lam \<equiv> \<lambda>a _ r. ILam [a].r"
-
-  trans_Const :: "nat \<Rightarrow> trmI"
-  "trans_Const \<equiv> \<lambda>n. INat n"
-
-  trans_Pr :: "trm \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_Pr \<equiv> \<lambda>_ _ r1 r2. 
-         let limit = IRef(INat 0) in 
-         let v1 = r1 in 
-         let v2 = r2 in 
-         (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit)))"
-
-  trans_Fst :: "trm \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_Fst \<equiv> \<lambda>_ r. IRef (ISucc r)"
-
-  trans_Snd :: "trm \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_Snd \<equiv> \<lambda>_ r. IRef (ISucc (ISucc r))"
- 
-  trans_InL :: "trm \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_InL \<equiv> \<lambda>_ r. 
-         let limit = IRef(INat 0) in 
-         let v = r in 
-         (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit)))"
-
-  trans_InR :: "trm \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_InR \<equiv> \<lambda>_ r. 
-         let limit = IRef(INat 0) in 
-         let v = r in 
-         (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit)))"
-
-  trans_Case :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI \<Rightarrow> trmI"
-  "trans_Case \<equiv> \<lambda>_ x1 _ x2 _ r r1 r2. 
-         let v = r in
-         let v1 = r1 in
-         let v2 = r2 in 
-         Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))])"
-
-  trans :: "trm \<Rightarrow> trmI" 
-    "trans t \<equiv> trm_rec (trans_Var) (trans_Lam) (trans_App)
-                           (trans_Const) (trans_Pr) (trans_Fst) (trans_Snd)
-                           (trans_InL) (trans_InR) (trans_Case) t"
-
-lemma fin_supp_trans:
-  shows "finite ((supp (trans_Var))::name set)"
-  and   "finite ((supp (trans_Lam))::name set)"
-  and   "finite ((supp (trans_App))::name set)"
-  and   "finite ((supp (trans_Const))::name set)"
-  and   "finite ((supp (trans_Pr))::name set)"
-  and   "finite ((supp (trans_Fst))::name set)"
-  and   "finite ((supp (trans_Snd))::name set)"
-  and   "finite ((supp (trans_InL))::name set)"
-  and   "finite ((supp (trans_InR))::name set)"
-  and   "finite ((supp (trans_Case))::name set)"
-apply -
-apply(finite_guess add: fs_name1 trans_Var_def)
-apply(finite_guess add: fs_name1 trans_Lam_def)
-apply(finite_guess add: fs_name1 trans_App_def)
-apply(finite_guess add: fs_name1 trans_Const_def)
-apply(finite_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def)
-apply(finite_guess add: fs_name1 trans_Fst_def)
-apply(finite_guess add: fs_name1 trans_Snd_def)
-apply(finite_guess add: fs_name1 trans_InL_def Let_def perm_nat_def)
-apply(finite_guess add: fs_name1 trans_InR_def Let_def perm_nat_def)
-apply(finite_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt)
-done
-
-lemma fcb_trans_Lam:
-  shows "x\<sharp>(trans_Lam) x t r"
-  by (simp add: trans_Lam_def abs_fresh)
+consts trans :: "trm \<Rightarrow> trmI" 
 
-lemma fcb_trans_Case:
-  assumes a: "x\<sharp>r" "x\<sharp>r2" "y\<sharp>r" "y\<sharp>r1"
-  shows "x\<sharp>(trans_Case) e x e1 y e2 r r1 r2"
-  and "y\<sharp>(trans_Case) e x e1 y e2 r r1 r2"
-  using a
-  by (simp_all add: trans_Case_def abs_fresh Isubst_fresh)
-  
-lemma trans:
-  shows "trans (Var x) = (IVar x)"
-  and   "trans (App e1 e2) = IApp (trans e1) (trans e2)"
-  and   "trans (Lam [x].e) = ILam [x].(trans e)"
-  and   "trans (Const n) = INat n"
-  and   "trans (Pr e1 e2) = 
-             (let limit = IRef(INat 0) in 
-              let v1 = (trans e1) in 
-              let v2 = (trans e2) in 
-              (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  and   "trans (Fst e) = IRef (ISucc (trans e))"
-  and   "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
-  and   "trans (InL e) = 
-              (let limit = IRef(INat 0) in 
-               let v = (trans e) in 
-               (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  and   "trans (InR e) = 
-              (let limit = IRef(INat 0) in 
-               let v = (trans e) in 
-               (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  and   "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
-         trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
-             (let v = (trans e) in
-              let v1 = (trans e1) in
-              let v2 = (trans e2) in 
-              Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))"
-apply(unfold trans_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_Var_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_App_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 trans_Lam_def)
-apply(fresh_guess add: fs_name1 trans_App_def)
-apply(fresh_guess add: fs_name1 trans_Const_def)
-apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_Fst_def)
-apply(fresh_guess add: fs_name1 trans_Snd_def)
-apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt)
-apply(simp add: trans_Lam_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_Const_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_Pr_def Let_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_Fst_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_Snd_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_InL_def Let_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(simp add: trans_InR_def Let_def)
-apply(rule trans)
-apply(rule trm_recs)
-apply(rule fin_supp_trans)+
-apply(simp add: fcb_trans_Lam)
-apply(simp add: fcb_trans_Case)
-apply(simp add: fcb_trans_Case)
-apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 trans_Var_def perm_if eq_eqvt)
-apply(fresh_guess add: fs_name1 trans_Lam_def)
-apply(fresh_guess add: fs_name1 trans_Lam_def)
-apply(fresh_guess add: fs_name1 trans_App_def)
-apply(fresh_guess add: fs_name1 trans_App_def)
-apply(fresh_guess add: fs_name1 trans_Const_def)
-apply(fresh_guess add: fs_name1 trans_Const_def)
-apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_Pr_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_Fst_def)
-apply(fresh_guess add: fs_name1 trans_Fst_def)
-apply(fresh_guess add: fs_name1 trans_Snd_def)
-apply(fresh_guess add: fs_name1 trans_Snd_def)
-apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_InL_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_InR_def Let_def perm_nat_def)
-apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt)
-apply(fresh_guess add: fs_name1 trans_Case_def Let_def Isubst_eqvt)
-apply(assumption)+
-apply(simp add: trans_Case_def Let_def)
-done
+nominal_primrec
+  "trans (Var x) = (IVar x)"
+  "trans (App e1 e2) = IApp (trans e1) (trans e2)"
+  "trans (Lam [x].e) = ILam [x].(trans e)"
+  "trans (Const n) = INat n"
+  "trans (Pr e1 e2) = 
+       (let limit = IRef(INat 0) in 
+        let v1 = (trans e1) in 
+        let v2 = (trans e2) in 
+        (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+  "trans (Fst e) = IRef (ISucc (trans e))"
+  "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
+  "trans (InL e) = 
+        (let limit = IRef(INat 0) in 
+         let v = (trans e) in 
+         (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+  "trans (InR e) = 
+        (let limit = IRef(INat 0) in 
+         let v = (trans e) in 
+         (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
+  "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
+   trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
+       (let v = (trans e) in
+        let v1 = (trans e1) in
+        let v2 = (trans e2) in 
+        Iif (IRef (ISucc v)) (v2[x2::=IRef (ISucc (ISucc v))]) (v1[x1::=IRef (ISucc (ISucc v))]))"
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1)
+  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
+  apply (finite_guess add: fs_name1 Let_def perm_nat_def)
+  apply (finite_guess add: fs_name1 Let_def Isubst_eqvt)
+  apply (simp add: supp_unit)
+  apply (rule TrueI)+
+  apply (simp add: abs_fresh)
+  apply (simp_all add: abs_fresh Isubst_fresh)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1 perm_if eq_eqvt)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def perm_nat_def)
+  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
+  apply (fresh_guess add: fs_name1 Let_def Isubst_eqvt)
+  done
 
+consts trans_type :: "ty \<Rightarrow> tyI"
+
+nominal_primrec
+  "trans_type (Data \<sigma>) = DataI(NatI)"
+  "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
+  by (rule TrueI)+
 
 end
\ No newline at end of file