Adapted to changes in FCBs.

--- a/src/HOL/Nominal/Examples/Compile.thy	Mon Oct 23 00:48:45 2006 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Mon Oct 23 00:51:16 2006 +0200
@@ -1,4 +1,4 @@
-(* $Id: *)
+(* $Id$ *)
 
 (* A challenge suggested by Adam Chlipala *)
 
@@ -190,9 +190,12 @@
 
 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"
+  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 add: subst_Case_def abs_fresh)
+  by (simp_all add: subst_Case_def abs_fresh)
+
+lemmas trm_recs = trm.recs[where P="\<lambda>_. True", simplified]
 
 lemma subst:
   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
@@ -209,22 +212,25 @@
                                     (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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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)
@@ -239,46 +245,53 @@
 apply(simp, simp)
 apply(simp add: subst_Lam_def)
 apply(rule trans)
-apply(rule trm.recs[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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)
@@ -374,6 +387,8 @@
   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'])"
@@ -387,17 +402,17 @@
   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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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)
@@ -414,37 +429,37 @@
 apply(simp, simp)
 apply(simp add: subst_ILam_def)
 apply(rule trans)
-apply(rule trmI.recs[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+apply(rule trmI_recs)
 apply(rule fin_supp_Isubst)+
 apply(simp add: fcb_subst_ILam)
 apply(simp add: subst_Iif_def)
@@ -539,15 +554,17 @@
   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[where P="\<lambda>_. True", simplified])
+apply(rule ty_recs)
 apply(simp add: trans_data_def)
 apply(rule trans)
-apply(rule ty.recs[where P="\<lambda>_. True", simplified])
+apply(rule ty_recs)
 apply(simp add: trans_arrow_def)
 done
 
@@ -631,9 +648,10 @@
 
 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"
+  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 add: trans_Case_def abs_fresh Isubst_fresh)
+  by (simp_all add: trans_Case_def abs_fresh Isubst_fresh)
   
 lemma trans:
   shows "trans (Var x) = (IVar x)"
@@ -663,22 +681,25 @@
               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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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)
@@ -691,46 +712,53 @@
 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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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[where P="\<lambda>_. True", simplified])
+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)

--- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Oct 23 00:48:45 2006 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Oct 23 00:51:16 2006 +0200
@@ -260,23 +260,25 @@
   shows "X\<sharp>(size_ty_All X T1 T2 r1 r2)"
 by (simp add: fresh_def supp_nat)
 
+lemmas ty_recs = ty.recs[where P="\<lambda>_. True" and z="()", simplified]
+
 lemma size_ty[simp]:
   shows "size_ty (Tvar X) = 1"
   and   "size_ty (Top) = 1"
   and   "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
   and   "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
 apply(unfold size_ty_def)
-apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified])
-apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(rule trans, rule ty_recs)
+apply(simp_all add: fin_size_ty fcb_size_ty_All supp_unit)
 apply(simp add: size_ty_Tvar_def)
-apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified])
-apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(rule trans, rule ty_recs)
+apply(simp_all add: fin_size_ty fcb_size_ty_All supp_unit)
 apply(simp add: size_ty_Top_def)
-apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified])
-apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(rule trans, rule ty_recs)
+apply(simp_all add: fin_size_ty fcb_size_ty_All supp_unit)
 apply(simp add: size_ty_Fun_def)
-apply(rule trans, rule ty.recs[where P="\<lambda>_. True", simplified])
-apply(simp_all add: fin_size_ty fcb_size_ty_All)
+apply(rule trans, rule ty_recs)
+apply(simp_all add: fin_size_ty fcb_size_ty_All supp_unit)
 apply(fresh_guess add: perm_nat_def size_ty_Tvar_def size_ty_Top_def size_ty_Fun_def size_ty_All_def)+
 apply(simp add: size_ty_All_def)
 done
@@ -352,19 +354,27 @@
 apply -
 apply(unfold subst_ty_def)
 apply(rule trans)
-apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All])
+apply(rule ty_recs)
+apply(simp add: fin_supp_subst supp_unit)+
+apply(rule fcb_subst_All)
 apply(assumption)+
 apply(simp add: subst_Tvar_def)
 apply(rule trans)
-apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All])
+apply(rule ty_recs)
+apply(simp add: fin_supp_subst supp_unit)+
+apply(rule fcb_subst_All)
 apply(assumption)+
 apply(simp add: subst_Top_def)
 apply(rule trans)
-apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All])
+apply(rule ty_recs)
+apply(simp add: fin_supp_subst supp_unit)+
+apply(rule fcb_subst_All)
 apply(assumption)+
 apply(simp add: subst_Fun_def)
 apply(rule trans)
-apply(rule ty.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_All])
+apply(rule ty_recs)
+apply(simp add: fin_supp_subst supp_unit)+
+apply(rule fcb_subst_All)
 apply(assumption)+
 apply(rule supports_fresh)
 apply(rule supports_subst_Tvar)

--- a/src/HOL/Nominal/Examples/Height.thy	Mon Oct 23 00:48:45 2006 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Mon Oct 23 00:51:16 2006 +0200
@@ -41,19 +41,25 @@
 done
 
 text {* derive the characteristic equations for height from the iteration combinator *}
+
+lemmas lam_recs = lam.recs[where P="\<lambda>_. True" and z="()", simplified]
+
 lemma height[simp]:
   shows "height (Var c) = 1"
   and   "height (App t1 t2) = (max (height t1) (height t2))+1"
   and   "height (Lam [a].t) = (height t)+1"
 apply(simp add: height_def)
-apply(simp add: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam])
+apply(simp add: lam_recs fin_supp_height fcb_height_Lam supp_unit)
 apply(simp add: height_Var_def)
 apply(simp add: height_def)
-apply(simp add: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam])
+apply(simp add: lam_recs fin_supp_height fcb_height_Lam supp_unit)
 apply(simp add: height_App_def)
 apply(simp add: height_def)
 apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_height, OF fcb_height_Lam])
+apply(rule lam_recs)
+apply(rule fin_supp_height)+
+apply(simp add: supp_unit)
+apply(rule fcb_height_Lam)
 apply(assumption)
 apply(fresh_guess add: height_Var_def perm_int_def)
 apply(fresh_guess add: height_App_def perm_int_def)
@@ -106,12 +112,15 @@
   and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
   and   "\<lbrakk>a\<sharp>y; a\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [a].t)[y::=t'] = Lam [a].(t[y::=t'])"
 apply(unfold subst_lam_def)
-apply(simp only: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam])
+apply(simp add: lam_recs fin_supp_subst fcb_subst_Lam supp_unit)
 apply(simp add: subst_Var_def)
-apply(simp only: lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam])
+apply(simp add: lam_recs fin_supp_subst fcb_subst_Lam supp_unit)
 apply(simp only: subst_App_def)
 apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True", simplified, OF fin_supp_subst, OF fcb_subst_Lam])
+apply(rule lam_recs)
+apply(rule fin_supp_subst)+
+apply(simp add: supp_unit)
+apply(rule fcb_subst_Lam)
 apply(assumption)
 apply(rule supports_fresh, rule supports_subst_Var, simp add: fs_name1, simp add: fresh_def supp_prod)
 apply(fresh_guess add: fresh_prod subst_App_def fs_name1)