author | urbanc |
Thu, 22 May 2008 16:34:41 +0200 | |
changeset 26966 | 071f40487734 |
parent 26764 | 805eece49928 |
child 29097 | 68245155eb58 |
permissions | -rw-r--r-- |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21107
diff
changeset
|
1 |
(* $Id$ *) |
21107 | 2 |
|
3 |
theory Lam_Funs |
|
25751 | 4 |
imports "../Nominal" |
21107 | 5 |
begin |
6 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
7 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
8 |
Provides useful definitions for reasoning |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
9 |
with lambda-terms. |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
10 |
*} |
25751 | 11 |
|
21107 | 12 |
atom_decl name |
13 |
||
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
14 |
nominal_datatype lam = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
15 |
Var "name" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
16 |
| App "lam" "lam" |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22540
diff
changeset
|
17 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
21107 | 18 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
19 |
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
|
20 |
|
21555 | 21 |
consts |
22 |
depth :: "lam \<Rightarrow> nat" |
|
21107 | 23 |
|
21555 | 24 |
nominal_primrec |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
25 |
"depth (Var x) = 1" |
21555 | 26 |
"depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
27 |
"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
|
28 |
apply(finite_guess)+ |
21555 | 29 |
apply(rule TrueI)+ |
30 |
apply(simp add: fresh_nat) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
31 |
apply(fresh_guess)+ |
21555 | 32 |
done |
21107 | 33 |
|
25751 | 34 |
text {* |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
the invariant that frees always returns a finite set of names. |
25751 | 39 |
*} |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
40 |
|
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
41 |
consts |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
42 |
frees :: "lam \<Rightarrow> name set" |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
43 |
|
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
44 |
nominal_primrec (invariant: "\<lambda>s::name set. finite s") |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
45 |
"frees (Var a) = {a}" |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
46 |
"frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
47 |
"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
|
48 |
apply(finite_guess)+ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
49 |
apply(simp)+ |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
50 |
apply(simp add: fresh_def) |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
51 |
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
|
52 |
apply(simp add: supp_atm) |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
53 |
apply(blast) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
54 |
apply(fresh_guess)+ |
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
55 |
done |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
56 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
57 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
*} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
61 |
|
21557
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
62 |
lemma frees_equals_support: |
3c8e29a6e4f0
added the function for free variables of a lambda-term, which is a
urbanc
parents:
21555
diff
changeset
|
63 |
shows "frees t = supp t" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26764
diff
changeset
|
64 |
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
|
65 |
(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
|
66 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
67 |
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
|
68 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
69 |
fun |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
70 |
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
|
71 |
where |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
72 |
"lookup [] x = Var x" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
73 |
| "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
|
74 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
75 |
lemma lookup_eqvt[eqvt]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
76 |
fixes pi::"name prm" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
77 |
and \<theta>::"(name\<times>lam) list" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
78 |
and X::"name" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
79 |
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
|
80 |
by (induct \<theta>) (auto simp add: eqvts) |
21107 | 81 |
|
21555 | 82 |
consts |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
83 |
psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam" ("_<_>" [95,95] 105) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
84 |
|
21555 | 85 |
nominal_primrec |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
86 |
"\<theta><(Var x)> = (lookup \<theta> x)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
87 |
"\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
88 |
"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
|
89 |
apply(finite_guess)+ |
21555 | 90 |
apply(rule TrueI)+ |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
91 |
apply(simp add: abs_fresh)+ |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
21557
diff
changeset
|
92 |
apply(fresh_guess)+ |
21107 | 93 |
done |
94 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
95 |
lemma psubst_eqvt[eqvt]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
96 |
fixes pi::"name prm" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
97 |
and t::"lam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
98 |
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
|
99 |
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
|
100 |
(simp_all add: eqvts fresh_bij) |
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 |
abbreviation |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
103 |
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
|
104 |
where |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
105 |
"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
|
106 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
107 |
lemma subst[simp]: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
108 |
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
|
109 |
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
|
110 |
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
|
111 |
by (simp_all add: fresh_list_cons fresh_list_nil) |
21107 | 112 |
|
113 |
lemma subst_supp: |
|
114 |
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
|
115 |
apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) |
21107 | 116 |
apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp) |
117 |
apply(blast)+ |
|
118 |
done |
|
119 |
||
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
120 |
text {* |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
*} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
125 |
nominal_datatype clam = |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
126 |
Hole ("\<box>" 1000) |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
127 |
| CAppL "clam" "lam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
128 |
| CAppR "lam" "clam" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
129 |
| CLam "name" "clam" ("CLam [_]._" [100,100] 100) |
21107 | 130 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
131 |
text {* Filling a lambda-term into a context. *} |
21107 | 132 |
|
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
133 |
consts |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
134 |
filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100) |
21107 | 135 |
|
21555 | 136 |
nominal_primrec |
26764
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
137 |
"\<box>\<lbrakk>t\<rbrakk> = t" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
138 |
"(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
139 |
"(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
140 |
"(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
141 |
by (rule TrueI)+ |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
142 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
143 |
text {* Composition od two contexts *} |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
144 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
145 |
consts |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
146 |
clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100) |
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 |
nominal_primrec |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
149 |
"\<box> \<circ> E' = E'" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
150 |
"(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
151 |
"(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
152 |
"(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')" |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
153 |
by (rule TrueI)+ |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
154 |
|
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
155 |
lemma clam_compose: |
805eece49928
extended to be a library of general facts about the lambda calculus
urbanc
parents:
25751
diff
changeset
|
156 |
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
|
157 |
by (induct E1 rule: clam.induct) (auto) |
21107 | 158 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21107
diff
changeset
|
159 |
end |