src/HOL/BNF_Examples/Lambda_Term.thy
 author blanchet Fri Jan 24 11:51:45 2014 +0100 (2014-01-24) changeset 55129 26bd1cba3ab5 parent 55076 1e73e090a514 child 55530 3dfb724db099 permissions -rw-r--r--
killed 'More_BNFs' by moving its various bits where they (now) belong
```     1 (*  Title:      HOL/BNF_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_new 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_pair id varsOf) F})"
```
```    31
```
```    32 primrec_new 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_pair id varsOf) xts} \<union>
```
```    37     (\<Union> {X | x X. (x,X) |\<in>| fimage (map_pair 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_pair_fset_iff[simp]:
```
```    42   "(x, y) |\<in>| fimage (map_pair 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
```