--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue May 12 21:17:47 2009 +0200
@@ -0,0 +1,43 @@
+theory Predicate_Compile_ex
+imports Complex_Main Predicate_Compile
+begin
+
+inductive even :: "nat \<Rightarrow> bool" and odd :: "nat \<Rightarrow> bool" where
+ "even 0"
+ | "even n \<Longrightarrow> odd (Suc n)"
+ | "odd n \<Longrightarrow> even (Suc n)"
+
+code_pred even
+ using assms by (rule even.cases)
+
+thm even.equation
+
+
+inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
+ append_Nil: "append [] xs xs"
+ | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
+
+code_pred append
+ using assms by (rule append.cases)
+
+thm append.equation
+
+
+inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+ for f where
+ "partition f [] [] []"
+ | "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
+ | "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
+
+code_pred partition
+ using assms by (rule partition.cases)
+
+thm partition.equation
+
+
+code_pred tranclp
+ using assms by (rule tranclp.cases)
+
+thm tranclp.equation
+
+end
\ No newline at end of file