# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1305364576 -3600
# Node ID 61384946ba2c2a768844be763a76b73c76fb6e4d
# Parent  8412c7e503d4dfe321f47b5371b1de1ea8d47e51
added a problem with inductive_cases (reported by Randy)

diff -r 8412c7e503d4 -r 61384946ba2c Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Fri May 13 14:50:17 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Sat May 14 10:16:16 2011 +0100
@@ -2,23 +2,24 @@
 imports "../Nominal2" 
 begin
 
-inductive
-  even :: "nat \<Rightarrow> bool" and
-  odd  :: "nat \<Rightarrow> bool"
-where
-  "even 0"
-| "odd n \<Longrightarrow> even (Suc n)"
-| "even n \<Longrightarrow> odd (Suc n)"
+
+(* inductive_cases do not simplify with simple equations *)
+atom_decl var
+nominal_datatype expr =
+  eCnst nat
+| eVar nat
 
-thm even_odd_def
+inductive 
+  eval :: "expr \<Rightarrow> nat \<Rightarrow> bool"
+where
+  evCnst: "eval (eCnst c) 0"
+| evVar: "eval (eVar n) 2"
 
-lemma
-  shows "p \<bullet> (even n) = even (p \<bullet> n)"
-unfolding even_def
-unfolding even_odd_def
-apply(perm_simp)
-apply(rule refl)
-done
+inductive_cases 
+  evInv_Cnst: "eval (eCnst c) m"
+
+thm evInv_Cnst[simplified expr.distinct expr.eq_iff]
+
 
 atom_decl name