--- 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