# HG changeset patch
# User urbanc
# Date 1162392271 -3600
# Node ID de048d4968d9a6c5da1bbb636831992611a654b9
# Parent  88d1daae0319ec36b4569281ddda1d141e846150
these files are superseded by the internal recursion combinator and the file Lam_Funs.thy

diff -r 88d1daae0319 -r de048d4968d9 src/HOL/Nominal/Examples/Iteration.thy
--- a/src/HOL/Nominal/Examples/Iteration.thy	Wed Nov 01 15:39:20 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,190 +0,0 @@
-(* $Id$ *)
-
-theory Iteration
-imports "../Nominal"
-begin
-
-atom_decl name
-
-nominal_datatype lam = Var "name"
-                     | App "lam" "lam"
-                     | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
-
-types 'a f1_ty  = "name\<Rightarrow>('a::pt_name)"
-      'a f2_ty  = "'a\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
-      'a f3_ty  = "name\<Rightarrow>'a\<Rightarrow>('a::pt_name)"
-
-consts
-  it :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> (lam \<times> 'a::pt_name) set"
-
-inductive "it f1 f2 f3"
-intros
-it1: "(Var a, f1 a) \<in> it f1 f2 f3"
-it2: "\<lbrakk>(t1,r1) \<in> it f1 f2 f3; (t2,r2) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (App t1 t2, f2 r1 r2) \<in> it f1 f2 f3"
-it3: "\<lbrakk>a\<sharp>(f1,f2,f3); (t,r) \<in> it f1 f2 f3\<rbrakk> \<Longrightarrow> (Lam [a].t,f3 a r) \<in> it f1 f2 f3"
-
-lemma it_equiv:
-  fixes pi::"name prm"
-  assumes a: "(t,r) \<in> it f1 f2 f3"
-  shows "(pi\<bullet>t,pi\<bullet>r) \<in> it (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3)"
-  using a
-  apply(induct)
-  apply(perm_simp | auto intro!: it.intros simp add: fresh_right)+
-  done
-
-lemma it_fin_supp:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     a: "(t,r) \<in> it f1 f2 f3"
-  shows "finite ((supp r)::name set)" 
-  using a f
-  apply(induct)
-  apply(finite_guess, simp add: supp_prod fs_name1)+
-  done
-
-lemma it_total:
-  assumes a: "finite ((supp (f1,f2,f3))::name set)"
-  and     b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  shows "\<exists>r. (t,r)\<in>it f1 f2 f3"
-apply(rule_tac lam.induct'[of "\<lambda>_. (supp (f1,f2,f3))" "\<lambda>z. \<lambda>t. \<exists>r. (t,r)\<in>it f1 f2 f3", simplified])
-apply(fold fresh_def)
-apply(auto intro: it.intros a)
-done
-
-lemma it_unique: 
-  assumes a: "finite ((supp (f1,f2,f3))::name set)"
-  and     b: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
-  and     c1: "(t,r)\<in>it f1 f2 f3"
-  and     c2: "(t,r')\<in>it f1 f2 f3"
-  shows   "r=r'"
-using c1 c2
-proof (induct arbitrary: r')
-  case it1
-  then show ?case by cases (simp_all add: lam.inject)
-next
-  case (it2 r1 r2 t1 t2)
-  have ih1: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
-  have ih2: "\<And>r'. (t2,r') \<in> it f1 f2 f3 \<Longrightarrow> r2 = r'" by fact
-  have "(App t1 t2, r') \<in>it f1 f2 f3" by fact
-  then show ?case
-  proof cases
-    case it2
-    then show ?thesis using ih1 ih2 by (simp add: lam.inject) 
-  qed (simp_all (no_asm_use))
-next
-  case (it3 a1 r1 t1)
-  have f1: "a1\<sharp>(f1,f2,f3)" by fact
-  have ih: "\<And>r'. (t1,r') \<in> it f1 f2 f3 \<Longrightarrow> r1 = r'" by fact
-  have it1: "(t1,r1) \<in> it f1 f2 f3" by fact
-  have "(Lam [a1].t1, r') \<in> it f1 f2 f3" by fact
-  then show ?case
-  proof cases
-    case (it3 a2 r2 t2)
-    then have f2: "a2\<sharp>(f1,f2,f3)" 
-         and  it2: "(t2,r2) \<in> it f1 f2 f3"
-         and  eq1: "[a1].t1 = [a2].t2" and eq2: "r' = f3 a2 r2" by (simp_all add: lam.inject) 
-    have "\<exists>(c::name). c\<sharp>(f1,f2,f3,a1,a2,t1,t2,r1,r2)" using a it1 it2
-      by (auto intro!: at_exists_fresh[OF at_name_inst] simp add: supp_prod fs_name1 it_fin_supp[OF a])
-    then obtain c where fresh: "c\<sharp>f1" "c\<sharp>f2" "c\<sharp>f3" "c\<noteq>a1" "c\<noteq>a2" "c\<sharp>t1" "c\<sharp>t2" "c\<sharp>r1" "c\<sharp>r2"
-      by (force simp add: fresh_prod fresh_atm)
-    have eq3: "[(a1,c)]\<bullet>t1 = [(a2,c)]\<bullet>t2" using eq1 fresh
-      apply(auto simp add: alpha)
-      apply(rule trans)
-      apply(rule perm_compose)
-      apply(simp add: calc_atm perm_fresh_fresh)
-      apply(rule pt_name3, rule at_ds5[OF at_name_inst])
-      done
-    have eq4: "[(a1,c)]\<bullet>r1 = [(a2,c)]\<bullet>r2" using eq3 it2 f1 f2 fresh
-      apply(drule_tac sym)
-      apply(rule_tac pt_bij2[OF pt_name_inst, OF at_name_inst])
-      apply(rule ih)
-      apply(drule_tac pi="[(a2,c)]" in it_equiv)
-      apply(perm_simp only: fresh_prod)
-      apply(drule_tac pi="[(a1,c)]" in it_equiv)
-      apply(perm_simp)
-      done
-    have fs1: "a1\<sharp>f3 a1 r1" using b f1
-      apply(auto)
-      apply(rule_tac pi="[(a1,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
-      apply(perm_simp add: calc_atm fresh_prod)
-      done      
-    have fs2: "a2\<sharp>f3 a2 r2" using b f2
-      apply(auto)
-      apply(rule_tac pi="[(a2,a)]" in pt_fresh_bij2[OF pt_name_inst, OF at_name_inst])
-      apply(perm_simp add: calc_atm fresh_prod)
-      done      
-    have fs3: "c\<sharp>f3 a1 r1" using fresh it1 a
-      by (fresh_guess add: supp_prod fs_name1 it_fin_supp[OF a] fresh_atm)
-    have fs4: "c\<sharp>f3 a2 r2" using fresh it2 a
-      by (fresh_guess add: supp_prod fs_name1 it_fin_supp[OF a] fresh_atm)
-    have "f3 a1 r1 = [(a1,c)]\<bullet>(f3 a1 r1)" using fs1 fs3 by perm_simp
-    also have "\<dots> = f3 c ([(a1,c)]\<bullet>r1)" using f1 fresh by (perm_simp add: calc_atm fresh_prod)
-    also have "\<dots> = f3 c ([(a2,c)]\<bullet>r2)" using eq4 by simp
-    also have "\<dots> = [(a2,c)]\<bullet>(f3 a2 r2)" using f2 fresh by (perm_simp add: calc_atm fresh_prod)
-    also have "\<dots> = f3 a2 r2" using fs2 fs4 by perm_simp
-    finally have eq4: "f3 a1 r1 = f3 a2 r2" by simp
-    then show ?thesis using eq2 by simp
-  qed (simp_all (no_asm_use))
-qed
-
-lemma it_function:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  shows "\<exists>!r. (t,r) \<in> it f1 f2 f3"
-proof (rule ex_ex1I, rule it_total[OF f, OF c])
-  case (goal1 r1 r2)
-  have a1: "(t,r1) \<in> it f1 f2 f3" and a2: "(t,r2) \<in> it f1 f2 f3" by fact
-  thus "r1 = r2" using it_unique[OF f, OF c] by simp
-qed
-
-constdefs
-  itfun :: "'a f1_ty \<Rightarrow> 'a f2_ty \<Rightarrow> 'a f3_ty \<Rightarrow> lam \<Rightarrow> ('a::pt_name)" 
-  "itfun f1 f2 f3 t \<equiv> (THE r. (t,r) \<in> it f1 f2 f3)"
-
-lemma itfun_eqvt:
-  fixes pi::"name prm"
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  shows "pi\<bullet>(itfun f1 f2 f3 t) = itfun (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)"
-proof -
-  have f_pi: "finite ((supp (pi\<bullet>f1,pi\<bullet>f2,pi\<bullet>f3))::name set)" using f
-    by (simp add: supp_prod pt_supp_finite_pi[OF pt_name_inst, OF at_name_inst])
-  have fs_pi: "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" 
-  proof -
-    from c obtain a where fs1: "a\<sharp>f3" and fs2: "\<forall>(r::'a::pt_name). a\<sharp>f3 a r" by force
-    have "(pi\<bullet>a)\<sharp>(pi\<bullet>f3)" using fs1 by (simp add: fresh_bij)
-    moreover
-    have "\<forall>(r::'a::pt_name). (pi\<bullet>a)\<sharp>((pi\<bullet>f3) (pi\<bullet>a) r)" using fs2 by (perm_simp add: fresh_right)
-    ultimately show "\<exists>(a::name). a\<sharp>(pi\<bullet>f3) \<and> (\<forall>(r::'a::pt_name). a\<sharp>(pi\<bullet>f3) a r)" by blast
-  qed
-  show ?thesis
-    apply(rule sym)
-    apply(auto simp add: itfun_def)
-    apply(rule the1_equality[OF it_function, OF f_pi, OF fs_pi])
-    apply(rule it_equiv)
-    apply(rule theI'[OF it_function,OF f, OF c])
-    done
-qed
-
-lemma itfun_Var:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  shows "itfun f1 f2 f3 (Var c) = (f1 c)"
-using f c by (auto intro!: the1_equality it_function it.intros simp add: itfun_def)
-
-lemma itfun_App:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  shows "itfun f1 f2 f3 (App t1 t2) = (f2 (itfun f1 f2 f3 t1) (itfun f1 f2 f3 t2))"
-by (auto intro!: the1_equality it_function[OF f, OF c] it.intros 
-         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
-
-lemma itfun_Lam:
-  assumes f: "finite ((supp (f1,f2,f3))::name set)"
-  and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(r::'a::pt_name). a\<sharp>f3 a r)"
-  and     a: "a\<sharp>(f1,f2,f3)"
-  shows "itfun f1 f2 f3 (Lam [a].t) = f3 a (itfun f1 f2 f3 t)"
-using a
-by (auto intro!: the1_equality it_function[OF f, OF c] it.intros 
-         intro: theI'[OF it_function, OF f, OF c] simp add: itfun_def)
-
-end
diff -r 88d1daae0319 -r de048d4968d9 src/HOL/Nominal/Examples/Lam_substs.thy
--- a/src/HOL/Nominal/Examples/Lam_substs.thy	Wed Nov 01 15:39:20 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,347 +0,0 @@
-(* $Id$ *)
-
-theory Lam_substs
-imports Iteration
-begin
-
-constdefs 
-  depth_Var :: "name \<Rightarrow> nat"
-  "depth_Var \<equiv> \<lambda>(a::name). 1"
-  
-  depth_App :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-  "depth_App \<equiv> \<lambda>n1 n2. (max n1 n2)+1"
-
-  depth_Lam :: "name \<Rightarrow> nat \<Rightarrow> nat"
-  "depth_Lam \<equiv> \<lambda>(a::name) n. n+1"
-
-  depth_lam :: "lam \<Rightarrow> nat"
-  "depth_lam \<equiv> itfun depth_Var depth_App depth_Lam"
-
-lemma supp_depth_Var:
-  shows "((supp depth_Var)::name set)={}"
-  apply(simp add: depth_Var_def)
-  apply(simp add: supp_def)
-  apply(simp add: perm_fun_def)
-  apply(simp add: perm_nat_def)
-  done
-
-lemma supp_depth_App:
-  shows "((supp depth_App)::name set)={}"
-  apply(simp add: depth_App_def)
-  apply(simp add: supp_def)
-  apply(simp add: perm_fun_def)
-  apply(simp add: perm_nat_def)
-  done
-
-lemma supp_depth_Lam:
-  shows "((supp depth_Lam)::name set)={}"
-  apply(simp add: depth_Lam_def)
-  apply(simp add: supp_def)
-  apply(simp add: perm_fun_def)
-  apply(simp add: perm_nat_def)
-  done
- 
-lemma fin_supp_depth:
-  shows "finite ((supp (depth_Var,depth_App,depth_Lam))::name set)"
-  by (finite_guess add: depth_Var_def depth_App_def depth_Lam_def perm_nat_def fs_name1)
-
-lemma fresh_depth_Lam:
-  shows "\<exists>(a::name). a\<sharp>depth_Lam \<and> (\<forall>n. a\<sharp>depth_Lam a n)"
-apply(rule exI)
-apply(rule conjI)
-apply(simp add: fresh_def)
-apply(force simp add: supp_depth_Lam)
-apply(unfold fresh_def)
-apply(simp add: supp_def)
-apply(simp add: perm_nat_def)
-done
-
-lemma depth_Var:
-  shows "depth_lam (Var c) = 1"
-apply(simp add: depth_lam_def)
-apply(simp add: itfun_Var[OF fin_supp_depth, OF fresh_depth_Lam])
-apply(simp add: depth_Var_def)
-done
-
-lemma depth_App:
-  shows "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1"
-apply(simp add: depth_lam_def)
-apply(simp add: itfun_App[OF fin_supp_depth, OF fresh_depth_Lam])
-apply(simp add: depth_App_def)
-done
-
-lemma depth_Lam:
-  shows "depth_lam (Lam [a].t) = (depth_lam t)+1"
-apply(simp add: depth_lam_def)
-apply(rule trans)
-apply(rule itfun_Lam[OF fin_supp_depth, OF fresh_depth_Lam])
-apply(simp add: fresh_def supp_prod supp_depth_Var supp_depth_App supp_depth_Lam)
-apply(simp add: depth_Lam_def)
-done
-
-text {* 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"
-  "subst_App b t \<equiv> \<lambda>r1 r2. App r1 r2"
-
-  subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_Lam b t \<equiv> \<lambda>a r. Lam [a].r"
-
-  subst_lam :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam"
-  "subst_lam b t \<equiv> itfun (subst_Var b t) (subst_App b t) (subst_Lam b t)"
-
-lemma supports_subst_Var:
-  shows "((supp (b,t))::name set) supports (subst_Var b t)"
-apply(supports_simp add: subst_Var_def)
-apply(rule impI)
-apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
-apply(simp add: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
-done
-
-lemma supports_subst_App:
-  shows "((supp (b,t))::name set) supports subst_App b t"
-by  (supports_simp add: subst_App_def)
-
-lemma supports_subst_Lam:
-  shows "((supp (b,t))::name set) supports subst_Lam b t"
-  by (supports_simp add: subst_Lam_def)
-
-lemma fin_supp_subst:
-  shows "finite ((supp (subst_Var b t,subst_App b t,subst_Lam b t))::name set)"
-apply(auto simp add: supp_prod)
-apply(rule supports_finite)
-apply(rule supports_subst_Var)
-apply(simp add: fs_name1)
-apply(rule supports_finite)
-apply(rule supports_subst_App)
-apply(simp add: fs_name1)
-apply(rule supports_finite)
-apply(rule supports_subst_Lam)
-apply(simp add: fs_name1)
-done
-
-lemma fresh_subst_Lam:
-  shows "\<exists>(a::name). a\<sharp>(subst_Lam b t)\<and> (\<forall>y. a\<sharp>(subst_Lam b t) a y)"
-apply(subgoal_tac "\<exists>(c::name). c\<sharp>(b,t)")
-apply(auto)
-apply(rule_tac x="c" in exI)
-apply(auto)
-apply(rule supports_fresh)
-apply(rule supports_subst_Lam)
-apply(simp_all add: fresh_def[symmetric] fs_name1)
-apply(simp add: subst_Lam_def)
-apply(simp add: abs_fresh)
-apply(rule at_exists_fresh[OF at_name_inst])
-apply(simp add: fs_name1)
-done
-
-lemma subst_Var:
-  shows "subst_lam b t (Var a) = (if a=b then t else (Var a))"
-apply(simp add: subst_lam_def)
-apply(auto simp add: itfun_Var[OF fin_supp_subst, OF fresh_subst_Lam])
-apply(auto simp add: subst_Var_def)
-done
-
-lemma subst_App:
-  shows "subst_lam b t (App t1 t2) = App (subst_lam b t t1) (subst_lam b t t2)"
-apply(simp add: subst_lam_def)
-apply(auto simp add: itfun_App[OF fin_supp_subst, OF fresh_subst_Lam])
-apply(auto simp add: subst_App_def)
-done
-
-lemma subst_Lam:
-  assumes a: "a\<sharp>(b,t)"
-  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
-using a
-apply(simp add: subst_lam_def)
-apply(subgoal_tac "a\<sharp>(subst_Var b t,subst_App b t,subst_Lam b t)")
-apply(auto simp add: itfun_Lam[OF fin_supp_subst, OF fresh_subst_Lam])
-apply(simp (no_asm) add: subst_Lam_def)
-apply(auto simp add: fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_subst_Var)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_subst_App)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_subst_Lam)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-done
-
-lemma subst_Lam':
-  assumes a: "a\<noteq>b"
-  and     b: "a\<sharp>t"
-  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
-by (simp add: subst_Lam fresh_prod a b fresh_atm)
-
-lemma subst_Lam'':
-  assumes a: "a\<sharp>b"
-  and     b: "a\<sharp>t"
-  shows "subst_lam b t (Lam [a].t1) = Lam [a].(subst_lam b t t1)"
-by (simp add: subst_Lam fresh_prod a b)
-
-consts
-  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900)
-translations 
-  "t1[a::=t2]" \<rightleftharpoons> "subst_lam a t2 t1"
-
-declare subst_Var[simp]
-declare subst_App[simp]
-declare subst_Lam[simp]
-declare subst_Lam'[simp]
-declare subst_Lam''[simp]
-
-lemma subst_eqvt[simp]:
-  fixes pi:: "name prm"
-  and   t1:: "lam"
-  and   t2:: "lam"
-  and   a :: "name"
-  shows "pi\<bullet>(t1[b::=t2]) = (pi\<bullet>t1)[(pi\<bullet>b)::=(pi\<bullet>t2)]"
-apply(nominal_induct t1 avoiding: b t2 rule: lam.induct)
-apply(auto simp add: perm_bij fresh_prod fresh_atm)
-apply(subgoal_tac "(pi\<bullet>name)\<sharp>(pi\<bullet>b,pi\<bullet>t2)")(*A*)
-apply(simp)
-(*A*)
-apply(simp add: pt_fresh_right[OF pt_name_inst, OF at_name_inst], perm_simp add: fresh_prod fresh_atm) 
-done
-
-lemma subst_supp: 
-  shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)"
-apply(nominal_induct t1 avoiding: a t2 rule: lam.induct)
-apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
-apply(blast)+
-done
-
-(* parallel substitution *)
-
-consts
-  "domain" :: "(name\<times>lam) list \<Rightarrow> (name list)"
-primrec
-  "domain []    = []"
-  "domain (x#\<theta>) = (fst x)#(domain \<theta>)" 
-
-consts
-  "apply_sss"  :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" (" _ < _ >" [80,80] 80)
-primrec  
-"(x#\<theta>)<a>  = (if (a = fst x) then (snd x) else \<theta><a>)" 
-
-
-lemma apply_sss_eqvt[rule_format]:
-  fixes pi::"name prm"
-  shows "a\<in>set (domain \<theta>) \<longrightarrow> pi\<bullet>(\<theta><a>) = (pi\<bullet>\<theta>)<pi\<bullet>a>"
-apply(induct_tac \<theta>)
-apply(auto)
-apply(simp add: pt_bij[OF pt_name_inst, OF at_name_inst])
-done
-
-lemma domain_eqvt[rule_format]:
-  fixes pi::"name prm"
-  shows "((pi\<bullet>a)\<in>set (domain \<theta>)) =  (a\<in>set (domain ((rev pi)\<bullet>\<theta>)))"
-apply(induct_tac \<theta>)
-apply(auto)
-apply(simp_all add: pt_rev_pi[OF pt_name_inst, OF at_name_inst])
-apply(simp_all add: pt_pi_rev[OF pt_name_inst, OF at_name_inst])
-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"
-  "psubst_App \<theta> \<equiv> \<lambda>r1 r2. App r1 r2"
-
-  psubst_Lam :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"
-  "psubst_Lam \<theta> \<equiv> \<lambda>a r. Lam [a].r"
-
-  psubst_lam :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"
-  "psubst_lam \<theta> \<equiv> itfun (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)"
-
-lemma supports_psubst_Var:
-  shows "((supp \<theta>)::name set) supports (psubst_Var \<theta>)"
-  by (supports_simp add: psubst_Var_def apply_sss_eqvt domain_eqvt)
-
-lemma supports_psubst_App:
-  shows "((supp \<theta>)::name set) supports psubst_App \<theta>"
-  by (supports_simp add: psubst_App_def)
-
-lemma supports_psubst_Lam:
-  shows "((supp \<theta>)::name set) supports psubst_Lam \<theta>"
-  by (supports_simp add: psubst_Lam_def)
-
-lemma fin_supp_psubst:
-  shows "finite ((supp (psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>))::name set)"
-apply(auto simp add: supp_prod)
-apply(rule supports_finite)
-apply(rule supports_psubst_Var)
-apply(simp add: fs_name1)
-apply(rule supports_finite)
-apply(rule supports_psubst_App)
-apply(simp add: fs_name1)
-apply(rule supports_finite)
-apply(rule supports_psubst_Lam)
-apply(simp add: fs_name1)
-done
-
-lemma fresh_psubst_Lam:
-  shows "\<exists>(a::name). a\<sharp>(psubst_Lam \<theta>)\<and> (\<forall>y. a\<sharp>(psubst_Lam \<theta>) a y)"
-apply(subgoal_tac "\<exists>(c::name). c\<sharp>\<theta>")
-apply(auto)
-apply(rule_tac x="c" in exI)
-apply(auto)
-apply(rule supports_fresh)
-apply(rule supports_psubst_Lam)
-apply(simp_all add: fresh_def[symmetric] fs_name1)
-apply(simp add: psubst_Lam_def)
-apply(simp add: abs_fresh)
-apply(rule at_exists_fresh[OF at_name_inst])
-apply(simp add: fs_name1)
-done
-
-lemma psubst_Var:
-  shows "psubst_lam \<theta> (Var a) = (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))"
-apply(simp add: psubst_lam_def)
-apply(auto simp add: itfun_Var[OF fin_supp_psubst, OF fresh_psubst_Lam])
-apply(auto simp add: psubst_Var_def)
-done
-
-lemma psubst_App:
-  shows "psubst_lam \<theta> (App t1 t2) = App (psubst_lam \<theta> t1) (psubst_lam \<theta> t2)"
-apply(simp add: psubst_lam_def)
-apply(auto simp add: itfun_App[OF fin_supp_psubst, OF fresh_psubst_Lam])
-apply(auto simp add: psubst_App_def)
-done
-
-lemma psubst_Lam:
-  assumes a: "a\<sharp>\<theta>"
-  shows "psubst_lam \<theta> (Lam [a].t1) = Lam [a].(psubst_lam \<theta> t1)"
-using a
-apply(simp add: psubst_lam_def)
-apply(subgoal_tac "a\<sharp>(psubst_Var \<theta>,psubst_App \<theta>,psubst_Lam \<theta>)")
-apply(auto simp add: itfun_Lam[OF fin_supp_psubst, OF fresh_psubst_Lam])
-apply(simp (no_asm) add: psubst_Lam_def)
-apply(auto simp add: fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_psubst_Var)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_psubst_App)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-apply(rule supports_fresh)
-apply(rule supports_psubst_Lam)
-apply(simp_all add: fs_name1 fresh_def[symmetric] fresh_prod)
-done
-
-declare psubst_Var[simp]
-declare psubst_App[simp]
-declare psubst_Lam[simp]
-
-consts
-  psubst_syn  :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900)
-translations 
-  "t[<\<theta>>]" \<rightleftharpoons> "psubst_lam \<theta> t"
-
-end
\ No newline at end of file