--- a/Nominal/Ex/Lambda.thy Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Lambda.thy Tue Jul 05 18:42:34 2011 +0200
@@ -1,5 +1,7 @@
theory Lambda
-imports "../Nominal2"
+imports
+ "../Nominal2"
+ "~~/src/HOL/Library/Monad_Syntax"
begin
@@ -8,7 +10,7 @@
nominal_datatype lam =
Var "name"
| App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
ML {* Method.SIMPLE_METHOD' *}
ML {* Sign.intern_const *}
@@ -320,24 +322,56 @@
termination
by lexicographic_order
+
+text {* count the occurences of lambdas in a term *}
+
+nominal_primrec
+ cntlams :: "lam \<Rightarrow> nat"
+where
+ "cntlams (Var x) = 0"
+| "cntlams (App t1 t2) = (cntlams t1) + (cntlams t2)"
+| "cntlams (Lam [x]. t) = Suc (cntlams t)"
+ apply(simp add: eqvt_def cntlams_graph_def)
+ apply(rule, perm_simp, rule)
+ apply(rule TrueI)
+ apply(rule_tac y="x" in lam.exhaust)
+ apply(auto)[3]
+ apply(all_trivials)
+ apply(simp)
+ apply(simp)
+ apply(erule_tac c="()" in Abs_lst1_fcb2')
+ apply(simp add: pure_fresh)
+ apply(simp add: fresh_star_def pure_fresh)
+ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+ done
+
+termination
+ by lexicographic_order
+
+
text {* count the bound-variable occurences in a lambda-term *}
nominal_primrec
- cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
+ cntbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
where
- "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
-| "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)"
-| "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = cbvs t (x # xs)"
- apply(simp add: eqvt_def cbvs_graph_def)
+ "cntbvs (Var x) xs = (if x \<in> set xs then 1 else 0)"
+| "cntbvs (App t1 t2) xs = (cntbvs t1 xs) + (cntbvs t2 xs)"
+| "atom x \<sharp> xs \<Longrightarrow> cntbvs (Lam [x]. t) xs = cntbvs t (x # xs)"
+ apply(simp add: eqvt_def cntbvs_graph_def)
apply(rule, perm_simp, rule)
- apply(simp_all)
+ apply(rule TrueI)
apply(case_tac x)
apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
apply(auto simp add: fresh_star_def)[3]
+ apply(all_trivials)
+ apply(simp)
+ apply(simp)
+ apply(simp)
apply(erule conjE)
apply(erule Abs_lst1_fcb2')
apply(simp add: pure_fresh fresh_star_def)
- apply(simp add: pure_fresh fresh_star_def)
+ apply(simp add: fresh_star_def)
apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
done
@@ -380,11 +414,14 @@
"(p \<bullet> vindex l v n) = vindex (p \<bullet> l) (p \<bullet> v) (p \<bullet> n)"
by (induct l arbitrary: n) (simp_all add: permute_pure)
+
+
nominal_primrec
transdb :: "lam \<Rightarrow> name list \<Rightarrow> db option"
where
"transdb (Var x) l = vindex l x 0"
-| "transdb (App t1 t2) xs = Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
+| "transdb (App t1 t2) xs =
+ Option.bind (transdb t1 xs) (\<lambda>d1. Option.bind (transdb t2 xs) (\<lambda>d2. Some (DBApp d1 d2)))"
| "x \<notin> set xs \<Longrightarrow> transdb (Lam [x].t) xs = Option.map DBLam (transdb t (x # xs))"
unfolding eqvt_def transdb_graph_def
apply (rule, perm_simp, rule)
@@ -421,47 +458,6 @@
Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"
using a by simp
-
-abbreviation
- mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65)
-where
- "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
-
-lemma mbind_eqvt:
- fixes c::"'a::pt option"
- shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
-apply(cases c)
-apply(simp_all)
-apply(perm_simp)
-apply(rule refl)
-done
-
-lemma mbind_eqvt_raw[eqvt_raw]:
- shows "(p \<bullet> option_case) \<equiv> option_case"
-apply(rule eq_reflection)
-apply(rule ext)+
-apply(case_tac xb)
-apply(simp_all)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-apply(rule_tac p="-p" in permute_boolE)
-apply(perm_simp add: permute_minus_cancel)
-apply(simp)
-done
-
-fun
- index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option"
-where
- "index [] n x = None"
-| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
-
-lemma [eqvt]:
- shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-apply(induct xs arbitrary: n)
-apply(simp_all add: permute_pure)
-done
-
lemma supp_subst:
"supp (t[x ::= s]) \<subseteq> supp t \<union> supp s"
by (induct t x s rule: subst.induct) (auto simp add: lam.supp)
@@ -569,13 +565,59 @@
termination
by lexicographic_order
+
+(*
+abbreviation
+ mbind :: "'a option => ('a => 'b option) => 'b option" ("_ \<guillemotright>= _" [65,65] 65)
+where
+ "c \<guillemotright>= f \<equiv> case c of None => None | (Some v) => f v"
+
+lemma mbind_eqvt:
+ fixes c::"'a::pt option"
+ shows "(p \<bullet> (c \<guillemotright>= f)) = ((p \<bullet> c) \<guillemotright>= (p \<bullet> f))"
+apply(cases c)
+apply(simp_all)
+apply(perm_simp)
+apply(rule refl)
+done
+
+lemma mbind_eqvt_raw[eqvt_raw]:
+ shows "(p \<bullet> option_case) \<equiv> option_case"
+apply(rule eq_reflection)
+apply(rule ext)+
+apply(case_tac xb)
+apply(simp_all)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: permute_minus_cancel)
+apply(simp)
+done
+
+fun
+ index :: "atom list \<Rightarrow> nat \<Rightarrow> atom \<Rightarrow> nat option"
+where
+ "index [] n x = None"
+| "index (y # ys) n x = (if x = y then (Some n) else (index ys (n + 1) x))"
+
+lemma [eqvt]:
+ shows "(p \<bullet> index xs n x) = index (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+apply(induct xs arbitrary: n)
+apply(simp_all add: permute_pure)
+done
+*)
+
+(*
nominal_primrec
trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
where
- "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))"
-| "trans2 (App t1 t2) xs = ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2. Some (DBApp db1 db2))))"
-| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
+ "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n::nat. Some (DBVar n)))"
+| "trans2 (App t1 t2) xs =
+ ((trans2 t1 xs) \<guillemotright>= (\<lambda>db1::db. (trans2 t2 xs) \<guillemotright>= (\<lambda>db2::db. Some (DBApp db1 db2))))"
+| "trans2 (Lam [x].t) xs = (trans2 t (atom x # xs) \<guillemotright>= (\<lambda>db::db. Some (DBLam db)))"
oops
+*)
nominal_primrec
CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"