|
1 (* Title: HOL/Datatype_Examples/Lambda_Term.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Lambda-terms. |
|
7 *) |
|
8 |
|
9 header {* Lambda-Terms *} |
|
10 |
|
11 theory Lambda_Term |
|
12 imports "~~/src/HOL/Library/FSet" |
|
13 begin |
|
14 |
|
15 section {* Datatype definition *} |
|
16 |
|
17 datatype_new 'a trm = |
|
18 Var 'a | |
|
19 App "'a trm" "'a trm" | |
|
20 Lam 'a "'a trm" | |
|
21 Lt "('a \<times> 'a trm) fset" "'a trm" |
|
22 |
|
23 |
|
24 subsection {* Example: The set of all variables varsOf and free variables fvarsOf of a term *} |
|
25 |
|
26 primrec varsOf :: "'a trm \<Rightarrow> 'a set" where |
|
27 "varsOf (Var a) = {a}" |
|
28 | "varsOf (App f x) = varsOf f \<union> varsOf x" |
|
29 | "varsOf (Lam x b) = {x} \<union> varsOf b" |
|
30 | "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})" |
|
31 |
|
32 primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where |
|
33 "fvarsOf (Var x) = {x}" |
|
34 | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2" |
|
35 | "fvarsOf (Lam x t) = fvarsOf t - {x}" |
|
36 | "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union> |
|
37 (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})" |
|
38 |
|
39 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast |
|
40 |
|
41 lemma in_fimage_map_prod_fset_iff[simp]: |
|
42 "(x, y) |\<in>| fimage (map_prod f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)" |
|
43 by force |
|
44 |
|
45 lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t" |
|
46 proof induct |
|
47 case (Lt xts t) thus ?case unfolding fvarsOf.simps varsOf.simps by (elim diff_Un_incl_triv) auto |
|
48 qed auto |
|
49 |
|
50 end |