# HG changeset patch
# User urbanc
# Date 1164632743 -3600
# Node ID 229c0158de9295b05cd7fcf140d13cb45c62e68c
# Parent  0625898865a9461991f1faee35ed03f307e47281
adapted function definitions to new syntax

diff -r 0625898865a9 -r 229c0158de92 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Mon Nov 27 14:00:08 2006 +0100
+++ b/src/HOL/Nominal/Examples/CR.thy	Mon Nov 27 14:05:43 2006 +0100
@@ -149,17 +149,16 @@
 next
   case (Lam b N1)
   have ih: "y\<sharp>N1 \<Longrightarrow> (N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L])" by fact
-  have f: "b\<sharp>y" "b\<sharp>x" "b\<sharp>L" by fact
-  from f have a:"b\<noteq>y" and b: "b\<noteq>x" and c: "b\<sharp>L" by (simp add: fresh_atm)+
+  have vc: "b\<sharp>y" "b\<sharp>x" "b\<sharp>L" by fact
   have "y\<sharp>Lam [b].N1" by fact
-  hence "y\<sharp>N1" using a by (simp add: abs_fresh)
+  hence "y\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm)
   hence d: "N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L]" using ih by simp
   show "(Lam [b].N1)[x::=L] = ([(y,x)]\<bullet>(Lam [b].N1))[y::=L]" (is "?LHS = ?RHS")
   proof -
-    have    "?LHS = Lam [b].(N1[x::=L])" using b c by simp
+    have    "?LHS = Lam [b].(N1[x::=L])" using vc by simp
     also have "\<dots> = Lam [b].(([(y,x)]\<bullet>N1)[y::=L])" using d by simp
-    also have "\<dots> = (Lam [b].([(y,x)]\<bullet>N1))[y::=L]" using a c by simp
-    also have "\<dots> = ?RHS" using a b by (simp add: calc_atm)
+    also have "\<dots> = (Lam [b].([(y,x)]\<bullet>N1))[y::=L]" using vc by simp
+    also have "\<dots> = ?RHS" using vc by (simp add: calc_atm fresh_atm)
     finally show "?LHS = ?RHS" by simp
   qed
 qed
diff -r 0625898865a9 -r 229c0158de92 src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Mon Nov 27 14:00:08 2006 +0100
+++ b/src/HOL/Nominal/Examples/Height.thy	Mon Nov 27 14:05:43 2006 +0100
@@ -12,120 +12,41 @@
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-text {* definition of the height-function by "structural recursion" ;o) *} 
+text {* definition of the height-function *} 
 
-constdefs 
-  height_Var :: "name \<Rightarrow> int"
-  "height_Var \<equiv> \<lambda>_. 1"
-  
-  height_App :: "lam\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int\<Rightarrow>int"
-  "height_App \<equiv> \<lambda>_ _ n1 n2. (max n1 n2)+1"
-
-  height_Lam :: "name\<Rightarrow>lam\<Rightarrow>int\<Rightarrow>int"
-  "height_Lam \<equiv> \<lambda>_ _ n. n+1"
-
+consts 
   height :: "lam \<Rightarrow> int"
-  "height \<equiv> lam_rec height_Var height_App height_Lam"
-
-text {* show that height is a function *}
-lemma fin_supp_height:
-  shows "finite ((supp height_Var)::name set)"
-  and   "finite ((supp height_App)::name set)"
-  and   "finite ((supp height_Lam)::name set)"
-  by (finite_guess add: height_Var_def height_App_def height_Lam_def perm_int_def fs_name1)+
-
-lemma fcb_height_Lam:
-  assumes fr: "a\<sharp>height_Lam"
-  shows "a\<sharp>height_Lam a t n"
-apply(simp add: height_Lam_def perm_int_def fresh_def supp_int)
-done
 
-text {* derive the characteristic equations for height from the iteration combinator *}
-
-lemmas lam_recs = lam.recs[where P="\<lambda>_. True" and z="()", simplified]
+nominal_primrec
+  "height (Var x) = 1"
+  "height (App t1 t2) = (max (height t1) (height t2)) + 1"
+  "height (Lam [a].t) = (height t) + 1"
+  apply(finite_guess add: perm_int_def)+
+  apply(rule TrueI)+
+  apply(simp add: fresh_int)
+  apply(fresh_guess add: perm_int_def)+
+  done
 
-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 fin_supp_height fcb_height_Lam supp_unit)
-apply(simp add: height_Var_def)
-apply(simp add: height_def)
-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)
-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)
-apply(fresh_guess add: height_Lam_def perm_int_def)
-apply(simp add: height_Lam_def)
-done
-
-text {* define capture-avoiding substitution *}
+text {* definition of capture-avoiding substitution *}
 
-constdefs 
-  subst_Var :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam"
-  "subst_Var x t' \<equiv> \<lambda>y. (if y=x then t' else (Var y))"
-  
-  subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_App x t' \<equiv> \<lambda>_ _ r1 r2. App r1 r2"
-
-  subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_Lam x t' \<equiv> \<lambda>a _ r. Lam [a].r"
-
-  subst_lam :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
-  "t[x::=t'] \<equiv> (lam_rec (subst_Var x t') (subst_App x t') (subst_Lam x t')) t"
-
-lemma supports_subst_Var:
-  shows "((supp (x,t))::name set) supports (subst_Var x t)"
-apply(supports_simp add: subst_Var_def)
-apply(rule impI)
-apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(perm_simp)
-done
+lemma eq_eqvt:
+  fixes pi::"name prm"
+  and   x::"'a::pt_name"
+  shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))"
+  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_App x t))::name set)"
-  and   "finite ((supp (subst_Lam x t))::name set)"
-proof -
-  case goal1
-  have f: "finite ((supp (x,t))::name set)" by (simp add: fs_name1)
-  then have "supp (subst_Var x t) \<subseteq> ((supp (x,t))::name set)"
-    using supp_is_subset[OF supports_subst_Var] by simp
-  then show "finite ((supp (subst_Var x t))::name set)" using f by (simp add: finite_subset)
-qed (finite_guess add: subst_App_def subst_Lam_def fs_name1)+
-
-lemma fcb_subst_Lam:
-  assumes fr: "a\<sharp>(subst_Lam y t')" 
-  shows "a\<sharp>(subst_Lam y t') a t r"
-  by (simp add: subst_Lam_def abs_fresh)
+consts
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
 
-lemma subst_lam[simp]:
-  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>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 add: lam_recs fin_supp_subst fcb_subst_Lam supp_unit)
-apply(simp add: subst_Var_def)
-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)
-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)
-apply(fresh_guess add: fresh_prod subst_Lam_def fs_name1)
-apply(simp add: subst_Lam_def)
+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'])"
+apply(finite_guess add: eq_eqvt perm_if fs_name1)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh)
+apply(fresh_guess add: eq_eqvt perm_if fs_name1)+
 done
 
 text{* the next lemma is needed in the Var-case of the theorem *}
@@ -136,7 +57,8 @@
      (simp | arith)+
 
 text {* unlike the proplem suggested by Wang, however, the 
-        theorem is formulated here entirely by using functions *}
+        theorem is here formulated here entirely by using 
+        functions *}
 
 theorem height_subst:
   shows "height (e[x::=e']) \<le> (((height e) - 1) + (height e'))"
@@ -149,7 +71,7 @@
   hence ih: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" by simp
   moreover
   have vc: "y\<sharp>x" "y\<sharp>e'" by fact (* usual variable convention *)
-  ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp 
+  ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
 next    
   case (App e1 e2)
   hence ih1: "height (e1[x::=e']) \<le> (((height e1) - 1) + (height e'))" 
diff -r 0625898865a9 -r 229c0158de92 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Mon Nov 27 14:00:08 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Mon Nov 27 14:05:43 2006 +0100
@@ -10,73 +10,21 @@
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-
-constdefs 
-  depth_Var :: "name \<Rightarrow> nat"
-  "depth_Var \<equiv> \<lambda>(a::name). 1"
-  
-  depth_App :: "lam \<Rightarrow> lam \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
-  "depth_App \<equiv> \<lambda>_ _ n1 n2. (max n1 n2)+1"
-
-  depth_Lam :: "name \<Rightarrow> lam \<Rightarrow> nat \<Rightarrow> nat"
-  "depth_Lam \<equiv> \<lambda>_ _ n. n+1"
-
-  depth_lam :: "lam \<Rightarrow> nat"
-  "depth_lam t \<equiv> (lam_rec depth_Var depth_App depth_Lam) t"
-
-lemma fin_supp_depth_lam:
-  shows "finite ((supp depth_Var)::name set)"
-  and   "finite ((supp depth_Lam)::name set)"
-  and   "finite ((supp depth_App)::name set)"
-  by (finite_guess add: depth_Var_def depth_Lam_def depth_App_def perm_nat_def)+
-
-lemma fcb_depth_lam:
-  fixes a::"name"
-  shows "a\<sharp>(depth_Lam a t n)"
-  by (simp add: fresh_nat)
+consts 
+  depth :: "lam \<Rightarrow> nat"
 
-lemma depth_lam:
-  shows "depth_lam (Var a)     = 1"
-  and   "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1"
-  and   "depth_lam (Lam [a].t) = (depth_lam t)+1"
-apply -
-apply(unfold depth_lam_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp_all add: fin_supp_depth_lam supp_unit)
-apply(simp add: fcb_depth_lam)
-apply(simp add: depth_Var_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp_all add: fin_supp_depth_lam supp_unit)
-apply(simp add: fcb_depth_lam)
-apply(simp add: depth_App_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp_all add: fin_supp_depth_lam supp_unit)
-apply(simp add: fcb_depth_lam)
-apply(simp add: depth_Var_def, fresh_guess add: perm_nat_def)
-apply(simp add: depth_App_def, fresh_guess add: perm_nat_def)
-apply(simp add: depth_Lam_def, fresh_guess add: perm_nat_def)
-apply(simp add: depth_Lam_def)
-done
+nominal_primrec
+  "depth (Var x) = 1"
+  "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
+  "depth (Lam [a].t) = (depth t) + 1"
+  apply(finite_guess add: perm_nat_def)+
+  apply(rule TrueI)+
+  apply(simp add: fresh_nat)
+  apply(fresh_guess add: perm_nat_def)+
+  done
 
 text {* capture-avoiding substitution *}
-constdefs 
-  subst_Var :: "name \<Rightarrow>lam \<Rightarrow> name \<Rightarrow> lam"
-  "subst_Var b t \<equiv> \<lambda>a. (if a=b then t else (Var a))"
-  
-  subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_App b t \<equiv> \<lambda>_ _ r1 r2. App r1 r2"
 
-  subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_Lam b t \<equiv> \<lambda>a _ r. Lam [a].r"
-
-abbreviation
-  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900) where
-  "t'[b::=t] \<equiv> (lam_rec (subst_Var b t) (subst_App b t) (subst_Lam b t)) t'"
-
-(* FIXME: this lemma needs to be in Nominal.thy *)
 lemma eq_eqvt:
   fixes pi::"name prm"
   and   x::"'a::pt_name"
@@ -84,62 +32,17 @@
   apply(simp add: perm_bool perm_bij)
   done
 
-lemma fin_supp_subst:
-  shows "finite ((supp (subst_Var b t))::name set)"
-  and   "finite ((supp (subst_Lam b t))::name set)"
-  and   "finite ((supp (subst_App b t))::name set)"
-apply -
-apply(finite_guess add: subst_Var_def perm_if eq_eqvt fs_name1)
-apply(finite_guess add: subst_Lam_def fs_name1)
-apply(finite_guess add: subst_App_def fs_name1)
-done
-
-lemma fcb_subst:
-  fixes a::"name"
-  shows "a\<sharp>(subst_Lam b t) a t' r"
-  by (simp add: subst_Lam_def abs_fresh)
+consts
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
 
-lemma subst[simp]:
-  shows "(Var a)[b::=t] = (if a=b then t else (Var a))"
-  and   "(App t1 t2)[b::=t] = App (t1[b::=t]) (t2[b::=t])"
-  and   "a\<sharp>(b,t)    \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])"
-  and   "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])"
-  and   "\<lbrakk>a\<sharp>b; a\<sharp>t\<rbrakk> \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])"
-apply -
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp add: fs_name1 fin_supp_subst)+
-apply(simp add: fcb_subst)
-apply(simp add: subst_Var_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp add: fs_name1 fin_supp_subst)+
-apply(simp add: fcb_subst)
-apply(simp add: subst_App_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp add: fs_name1 fin_supp_subst)+
-apply(simp add: fcb_subst)
-apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1)
-apply(fresh_guess add: subst_App_def fs_name1)
-apply(fresh_guess add: subst_Lam_def fs_name1)
-apply(simp add: subst_Lam_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp add: fs_name1 fin_supp_subst)+
-apply(simp add: fcb_subst)
-apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1 fresh_atm)
-apply(fresh_guess add: subst_App_def fs_name1 fresh_atm)
-apply(fresh_guess add: subst_Lam_def fs_name1 fresh_atm)
-apply(simp add: subst_Lam_def)
-apply(rule trans)
-apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-apply(simp add: fs_name1 fin_supp_subst)+
-apply(simp add: fcb_subst)
-apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1)
-apply(fresh_guess add: subst_App_def fs_name1)
-apply(fresh_guess add: subst_Lam_def fs_name1)
-apply(simp add: subst_Lam_def)
+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'])"
+  "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+apply(finite_guess add: eq_eqvt perm_if fs_name1)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh)
+apply(fresh_guess add: eq_eqvt perm_if fs_name1)+
 done
 
 lemma subst_eqvt[simp]:
@@ -159,9 +62,8 @@
 apply(blast)+
 done
 
-(* parallel substitution *)
+text{* parallel substitution *}
 
-(* simultaneous substitution *)
 consts
   "domain" :: "(name\<times>lam) list \<Rightarrow> (name list)"
 primrec
@@ -189,56 +91,17 @@
 apply(perm_simp)+
 done
 
-constdefs 
-  psubst_Var :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"
-  "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
-  
-  psubst_App :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "psubst_App \<theta> \<equiv> \<lambda>_ _ r1 r2. App r1 r2"
-
-  psubst_Lam :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "psubst_Lam \<theta> \<equiv> \<lambda>a _ r. Lam [a].r"
-
-abbreviation
-  psubst_lam :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900) where
-  "t[<\<theta>>] \<equiv> (lam_rec (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)) t"
-
-lemma fin_supp_psubst:
-  shows "finite ((supp (psubst_Var \<theta>))::name set)"
-  and   "finite ((supp (psubst_Lam \<theta>))::name set)"
-  and   "finite ((supp (psubst_App \<theta>))::name set)"
-  apply -
-  apply(finite_guess add: fs_name1 psubst_Var_def domain_eqvt apply_sss_eqvt)
-  apply(finite_guess add: fs_name1 psubst_Lam_def)
-  apply(finite_guess add: fs_name1 psubst_App_def)
-done
+consts
+ psubst :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900)
 
-lemma fcb_psubst_Lam:
-  shows "x\<sharp>(psubst_Lam \<theta>) x t r"
-  by (simp add: psubst_Lam_def abs_fresh)
-
-lemma psubst[simp]:
-  shows "(Var a)[<\<theta>>] = (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
-  and   "(App t1 t2)[<\<theta>>] = App (t1[<\<theta>>]) (t2[<\<theta>>])"
-  and   "a\<sharp>\<theta> \<Longrightarrow> (Lam [a].t1)[<\<theta>>] = Lam [a].(t1[<\<theta>>])"
-  apply(rule trans)
-  apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-  apply(simp add: fin_supp_psubst fs_name1)+
-  apply(simp add: fcb_psubst_Lam)
-  apply(simp add: psubst_Var_def)
-  apply(rule trans)
-  apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-  apply(simp add: fin_supp_psubst fs_name1)+
-  apply(simp add: fcb_psubst_Lam)
-  apply(simp add: psubst_App_def)
-  apply(rule trans)
-  apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified])
-  apply(simp add: fin_supp_psubst fs_name1)+
-  apply(simp add: fcb_psubst_Lam)
-  apply(fresh_guess add: psubst_Var_def domain_eqvt apply_sss_eqvt fs_name1)
-  apply(fresh_guess add: psubst_App_def fs_name1)
-  apply(fresh_guess add: psubst_Lam_def fs_name1)
-  apply(simp add: psubst_Lam_def)
+nominal_primrec
+  "(Var x)[<\<theta>>] = (if x\<in>set (domain \<theta>) then \<theta><x> else (Var x))"
+  "(App t1 t2)[<\<theta>>] = App (t1[<\<theta>>]) (t2[<\<theta>>])"
+  "x\<sharp>\<theta>\<Longrightarrow>(Lam [x].t)[<\<theta>>] = Lam [x].(t[<\<theta>>])"
+apply(finite_guess add: domain_eqvt apply_sss_eqvt fs_name1)+
+apply(rule TrueI)+
+apply(simp add: abs_fresh)
+apply(fresh_guess add: domain_eqvt apply_sss_eqvt fs_name1)+
 done
 
 end