author | wenzelm |
Tue, 13 Aug 2013 16:25:47 +0200 | |
changeset 53015 | a1119cf551e8 |
parent 29097 | 68245155eb58 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
21107 | 1 |
theory Lam_Funs |
25751 | 2 |
imports "../Nominal" |
21107 | 3 |
begin |
4 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
5 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
6 |
Provides useful definitions for reasoning |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
7 |
with lambda-terms. |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
8 |
*} |
25751 | 9 |
|
21107 | 10 |
atom_decl name |
11 |
||
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
12 |
nominal_datatype lam = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
13 |
Var "name" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
14 |
| App "lam" "lam" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
15 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
21107 | 16 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
17 |
text {* The depth of a lambda-term. *} |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
18 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
19 |
nominal_primrec |
21555 | 20 |
depth :: "lam \<Rightarrow> nat" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
21 |
where |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
22 |
"depth (Var x) = 1" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
23 |
| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
24 |
| "depth (Lam [a].t) = (depth t) + 1" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
25 |
apply(finite_guess)+ |
21555 | 26 |
apply(rule TrueI)+ |
27 |
apply(simp add: fresh_nat) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
28 |
apply(fresh_guess)+ |
21555 | 29 |
done |
21107 | 30 |
|
25751 | 31 |
text {* |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
32 |
The free variables of a lambda-term. A complication in this |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
33 |
function arises from the fact that it returns a name set, which |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
34 |
is not a finitely supported type. Therefore we have to prove |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
35 |
the invariant that frees always returns a finite set of names. |
25751 | 36 |
*} |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
37 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
38 |
nominal_primrec (invariant: "\<lambda>s::name set. finite s") |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
39 |
frees :: "lam \<Rightarrow> name set" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
40 |
where |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
41 |
"frees (Var a) = {a}" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
42 |
| "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
43 |
| "frees (Lam [a].t) = (frees t) - {a}" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
44 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
45 |
apply(simp)+ |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
46 |
apply(simp add: fresh_def) |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
47 |
apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]]) |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
48 |
apply(simp add: supp_atm) |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
49 |
apply(blast) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
50 |
apply(fresh_guess)+ |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
51 |
done |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
52 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
53 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
54 |
We can avoid the definition of frees by |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
55 |
using the build in notion of support. |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
56 |
*} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
57 |
|
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
58 |
lemma frees_equals_support: |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
59 |
shows "frees t = supp t" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26764
diff
changeset
|
60 |
by (nominal_induct t rule: lam.strong_induct) |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
61 |
(simp_all add: lam.supp supp_atm abs_supp) |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
62 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
63 |
text {* Parallel and single capture-avoiding substitution. *} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
64 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
65 |
fun |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
66 |
lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
67 |
where |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
68 |
"lookup [] x = Var x" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
69 |
| "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
70 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
71 |
lemma lookup_eqvt[eqvt]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
72 |
fixes pi::"name prm" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
73 |
and \<theta>::"(name\<times>lam) list" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
74 |
and X::"name" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
75 |
shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
76 |
by (induct \<theta>) (auto simp add: eqvts) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
77 |
|
21555 | 78 |
nominal_primrec |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
79 |
psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [95,95] 105) |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
80 |
where |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
81 |
"\<theta><(Var x)> = (lookup \<theta> x)" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
29097
diff
changeset
|
82 |
| "\<theta><(App e\<^sub>1 e\<^sub>2)> = App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>)" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
83 |
| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
84 |
apply(finite_guess)+ |
21555 | 85 |
apply(rule TrueI)+ |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
86 |
apply(simp add: abs_fresh)+ |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
87 |
apply(fresh_guess)+ |
21107 | 88 |
done |
89 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
90 |
lemma psubst_eqvt[eqvt]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
91 |
fixes pi::"name prm" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
92 |
and t::"lam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
93 |
shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26764
diff
changeset
|
94 |
by (nominal_induct t avoiding: \<theta> rule: lam.strong_induct) |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
95 |
(simp_all add: eqvts fresh_bij) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
96 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
97 |
abbreviation |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
98 |
subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
99 |
where |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
100 |
"t[x::=t'] \<equiv> ([(x,t')])<t>" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
101 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
102 |
lemma subst[simp]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
103 |
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
104 |
and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
105 |
and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
106 |
by (simp_all add: fresh_list_cons fresh_list_nil) |
21107 | 107 |
|
108 |
lemma subst_supp: |
|
109 |
shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26764
diff
changeset
|
110 |
apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) |
21107 | 111 |
apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) |
112 |
apply(blast)+ |
|
113 |
done |
|
114 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
115 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
116 |
Contexts - lambda-terms with a single hole. |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
117 |
Note that the lambda case in contexts does not bind a |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
118 |
name, even if we introduce the notation [_]._ for CLam. |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
119 |
*} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
120 |
nominal_datatype clam = |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
121 |
Hole ("\<box>" 1000) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
122 |
| CAppL "clam" "lam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
123 |
| CAppR "lam" "clam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
124 |
| CLam "name" "clam" ("CLam [_]._" [100,100] 100) |
21107 | 125 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
126 |
text {* Filling a lambda-term into a context. *} |
21107 | 127 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
128 |
nominal_primrec |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
129 |
filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100) |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
130 |
where |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
131 |
"\<box>\<lbrakk>t\<rbrakk> = t" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
132 |
| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
133 |
| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
134 |
| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
135 |
by (rule TrueI)+ |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
136 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
137 |
text {* Composition od two contexts *} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
138 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
139 |
nominal_primrec |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
140 |
clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100) |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
141 |
where |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
142 |
"\<box> \<circ> E' = E'" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
143 |
| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
144 |
| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
26966
diff
changeset
|
145 |
| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')" |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
146 |
by (rule TrueI)+ |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
147 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
148 |
lemma clam_compose: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
149 |
shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26764
diff
changeset
|
150 |
by (induct E1 rule: clam.induct) (auto) |
21107 | 151 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21107
diff
changeset
|
152 |
end |