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