diff -r 036a19936feb -r 32979078bfe9 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu May 26 06:36:29 2011 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 31 00:17:22 2011 +0100
@@ -3,26 +3,6 @@
 begin
 
 
-(* inductive_cases do not simplify with simple equations *)
-atom_decl var
-nominal_datatype expr =
-  eCnst nat
-| eVar nat
-
-inductive 
-  eval :: "expr \<Rightarrow> nat list \<Rightarrow> bool"
-where
-  evCnst1: "eval (eCnst c) [2,1]"
-| evCnst2: "eval (eCnst b) [1,2]"
-| evVar: "eval (eVar n) [1]"
-
-inductive_cases 
-  evInv_Cnst: "eval (eCnst c) [1,2]"
-
-thm evInv_Cnst
-
-
-
 atom_decl name
 
 nominal_datatype lam =
@@ -515,7 +495,59 @@
 apply(simp_all add: permute_pure)
 done
 
-(*
+
+text {* tests of functions containing if and case *}
+
+consts P :: "lam \<Rightarrow> bool"
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (App M N) = (if (True \<or> P M) then (A M) else (A N))"
+| "A (Var x) = (Var x)" 
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  C :: "lam => lam"
+where  
+  "C (App M N) = (case (True \<or> P M) of True \<Rightarrow> (A M) | False \<Rightarrow> (A N))"
+| "C (Var x) = (Var x)" 
+| "C (App M N) = (if True then M else C N)"
+oops
+
+nominal_primrec
+  map_term :: "(lam \<Rightarrow> lam) \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "map_term f (Var x) = f (Var x)"
+| "map_term f (App t1 t2) = App (f t1) (f t2)"
+| "map_term f (Lam [x].t) = Lam [x].(f t)"
+oops
+
+nominal_primrec  
+  A :: "lam => lam"
+where  
+  "A (Lam [x].M) = (Lam [x].M)"
+| "A (Var x) = (Var x)"
+| "A (App M N) = (if True then M else A N)"
+oops
+
+nominal_primrec  
+  B :: "lam => lam"
+where  
+  "B (Lam [x].M) = (Lam [x].M)"
+| "B (Var x) = (Var x)"
+| "B (App M N) = (if True then M else (B N))"
+unfolding eqvt_def
+unfolding B_graph_def
+apply(perm_simp)
+apply(rule allI)
+apply(rule refl)
+oops
+
+text {* not working yet *}
+
+(* not working yet
 nominal_primrec
   trans :: "lam \<Rightarrow> atom list \<Rightarrow> db option"
 where
@@ -524,6 +556,30 @@
 | "trans (Lam [x].t) xs = (trans t (atom x # xs) \<guillemotright>= (\<lambda>db. Some (DBLam db)))"
 *)
 
+(* not working yet
+nominal_primrec
+  CPS :: "lam \<Rightarrow> (lam \<Rightarrow> lam) \<Rightarrow> lam"
+where
+  "CPS (Var x) k = Var x"
+| "CPS (App M N) k = CPS M (\<lambda>m. CPS N (\<lambda>n. n))"
+*)
+
+
+(* function tests *)
+
+(* similar problem with function package *)
+function
+  f :: "int list \<Rightarrow> int"
+where
+  "f [] = 0"
+| "f [e] = e"
+| "f (l @ m) = f l + f m"
+apply(simp_all)
+oops
+
+
+
+
 
 
 end