diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Ex/Lambda.thy
--- 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"