26 |
26 |
27 primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where |
27 primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where |
28 "varsOf (Var a) = {a}" |
28 "varsOf (Var a) = {a}" |
29 | "varsOf (App f x) = varsOf f \<union> varsOf x" |
29 | "varsOf (App f x) = varsOf f \<union> varsOf x" |
30 | "varsOf (Lam x b) = {x} \<union> varsOf b" |
30 | "varsOf (Lam x b) = {x} \<union> varsOf b" |
31 | "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) F})" |
31 | "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})" |
32 |
32 |
33 primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where |
33 primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where |
34 "fvarsOf (Var x) = {x}" |
34 "fvarsOf (Var x) = {x}" |
35 | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2" |
35 | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2" |
36 | "fvarsOf (Lam x t) = fvarsOf t - {x}" |
36 | "fvarsOf (Lam x t) = fvarsOf t - {x}" |
37 | "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts} \<union> |
37 | "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts} \<union> |
38 (\<Union> {X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts})" |
38 (\<Union> {X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts})" |
39 |
39 |
40 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 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast |
41 |
41 |
42 lemma in_fmap_map_pair_fset_iff[simp]: |
42 lemma in_fmap_map_pair_fset_iff[simp]: |
43 "(x, y) |\<in>| fmap (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)" |
43 "(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)" |
44 by transfer auto |
44 by force |
45 |
45 |
46 lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t" |
46 lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t" |
47 proof induct |
47 proof induct |
48 case (Lt xts t) thus ?case unfolding fvarsOf.simps varsOf.simps by (elim diff_Un_incl_triv) auto |
48 case (Lt xts t) thus ?case unfolding fvarsOf.simps varsOf.simps by (elim diff_Un_incl_triv) auto |
49 qed auto |
49 qed auto |