diff -r da6461d8891f -r de6b601c8d3d Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Jun 15 12:52:48 2011 +0100 +++ b/Nominal/Ex/Lambda.thy Wed Jun 15 22:36:59 2011 +0100 @@ -10,6 +10,36 @@ | App "lam" "lam" | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) + +text {* free name function - returns an atom list *} + +nominal_primrec + frees_lst :: "lam \ atom list" +where + "frees_lst (Var x) = [atom x]" +| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" +| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" + unfolding eqvt_def frees_lst_graph_def + apply (rule, perm_simp, rule) +apply(rule TrueI) +apply(rule_tac y="x" in lam.exhaust) +apply(auto) +apply (erule Abs_lst1_fcb) +apply(simp add: supp_removeAll fresh_def) +apply(drule supp_eqvt_at) +apply(simp add: finite_supp) +apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) +done + +termination + by lexicographic_order + +text {* a small test lemma *} +lemma shows "supp t = set (frees_lst t)" + by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) + +text {* free name function - returns an atom set *} + nominal_primrec (invariant "\x (y::atom set). finite y") frees_set :: "lam \ atom set" where @@ -30,7 +60,7 @@ done termination - by (relation "measure size") (auto simp add: lam.size) + by lexicographic_order lemma "frees_set t = supp t" by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) @@ -42,6 +72,9 @@ using fresh_fun_eqvt_app[OF a b(1)] a b by (metis fresh_fun_app) + +text {* A test with a locale and an interpretation. *} + locale test = fixes f1::"name \ ('a::pt)" and f2::"lam \ lam \ 'a \ 'a \ ('a::pt)" @@ -78,18 +111,10 @@ done termination - by (relation "measure size") (auto simp add: lam.size) - -thm f.simps + by lexicographic_order end - -thm test.f.simps -thm test.f.simps[simplified test_def] - -thm test_def - interpretation hei: test "%n. (1 :: nat)" "%t1 t2 r1 r2. (r1 + r2)" @@ -100,44 +125,6 @@ apply (simp_all add: eqvt_def permute_fun_def permute_pure) done -thm hei.f.simps - -inductive - triv :: "lam \ nat \ bool" -where - Var: "triv (Var x) n" -| App: "\triv t1 n; triv t2 n\ \ triv (App t1 t2) n" - -lemma - "p \ (triv t x) = triv (p \ t) (p \ x)" -unfolding triv_def -apply(perm_simp) -apply(rule refl) -oops -(*apply(perm_simp)*) - -ML {* - Inductive.the_inductive @{context} "Lambda.triv" -*} - -thm triv_def - -equivariance triv -nominal_inductive triv avoids Var: "{}::name set" -apply(auto simp add: fresh_star_def) -done - -inductive - triv2 :: "lam \ nat \ bool" -where - Var1: "triv2 (Var x) 0" -| Var2: "triv2 (Var x) (n + n)" -| Var3: "triv2 (Var x) n" - -equivariance triv2 -nominal_inductive triv2 . - - text {* height function *} nominal_primrec @@ -156,38 +143,11 @@ done termination - by (relation "measure size") (simp_all add: lam.size) + by lexicographic_order thm height.simps -text {* free name function - returns atom lists *} - -nominal_primrec - frees_lst :: "lam \ atom list" -where - "frees_lst (Var x) = [atom x]" -| "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" -| "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" - unfolding eqvt_def frees_lst_graph_def - apply (rule, perm_simp, rule) -apply(rule TrueI) -apply(rule_tac y="x" in lam.exhaust) -apply(auto) -apply (erule Abs_lst1_fcb) -apply(simp add: supp_removeAll fresh_def) -apply(drule supp_eqvt_at) -apply(simp add: finite_supp) -apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) -done - -termination - by (relation "measure size") (simp_all add: lam.size) - -text {* a small test lemma *} -lemma shows "supp t = set (frees_lst t)" - by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) - text {* capture - avoiding substitution *} nominal_primrec @@ -213,8 +173,10 @@ apply(simp_all add: swap_fresh_fresh) done +declare lam.size[simp] + termination - by (relation "measure (\(t,_,_). size t)") (simp_all add: lam.size) + by lexicographic_order lemma subst_eqvt[eqvt]: shows "(p \ t[x ::= s]) = (p \ t)[(p \ x) ::= (p \ s)]" @@ -335,8 +297,6 @@ finally show "App (Lam [x].t1) s1 \1 t2[x ::= s2]" by simp qed - - section {* Locally Nameless Terms *} nominal_datatype ln = @@ -374,6 +334,8 @@ shows "(p \ lookup xs n x) = lookup (p \ xs) (p \ n) (p \ x)" by (induct xs arbitrary: n) (simp_all add: permute_pure) +text {* Function that translates lambda-terms into locally nameless terms *} + nominal_primrec (invariant "\(_, xs) y. atom ` set xs \* y") trans :: "lam \ name list \ ln" where @@ -397,16 +359,17 @@ apply (simp add: eqvt_at_def swap_fresh_fresh) done +termination + by lexicographic_order -termination - by (relation "measure (size o fst)") (simp_all add: lam.size) +text {* count bound-variable occurences *} nominal_primrec cbvs :: "lam \ name list \ nat" where "cbvs (Var x) xs = (if x \ set xs then 1 else 0)" | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" -| "atom x \ xs \ cbvs (Lam [x]. t) xs = (cbvs t (x # xs))" +| "atom x \ xs \ cbvs (Lam [x]. t) xs = cbvs t (x # xs)" apply(simp add: eqvt_def cbvs_graph_def) apply(rule, perm_simp, rule) apply(simp_all) @@ -419,8 +382,9 @@ done termination - by (relation "measure (size o fst)") (simp_all add: lam.size) + by lexicographic_order +section {* De Bruijn Terms *} nominal_datatype db = DBVar nat @@ -486,7 +450,7 @@ done termination - by (relation "measure (\(t,_). size t)") (simp_all add: lam.size) + by lexicographic_order lemma transdb_eqvt[eqvt]: "p \ transdb t l = transdb (p \t) (p \l)" @@ -502,7 +466,8 @@ lemma db_trans_test: assumes a: "y \ x" - shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" + shows "transdb (Lam [x]. Lam [y]. App (Var x) (Var y)) [] = + Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))" using a by simp abbreviation @@ -656,7 +621,7 @@ done termination - by (relation "measure (\(_,t). size t)") (simp_all add: lam.size) + by lexicographic_order nominal_primrec trans2 :: "lam \ atom list \ db option"