src/HOL/ex/Predicate_Compile_ex.thy

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 09 11:11:13 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 09 12:05:22 2009 +0200
@@ -7,9 +7,13 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
+
+(*
 code_pred even
   using assms by (rule even.cases)
-
+*)
+setup {* Predicate_Compile.add_equations @{const_name even} *}
+thm odd.equation
 thm even.equation
 
 values "{x. even 2}"
@@ -22,8 +26,20 @@
     append_Nil: "append [] xs xs"
   | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
+inductive rev
+where
+"rev [] []"
+| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
+
+setup {* Predicate_Compile.add_equations @{const_name rev} *}
+
+thm rev.equation
+thm append.equation
+
+(*
 code_pred append
   using assms by (rule append.cases)
+*)
 
 thm append.equation
 
@@ -38,17 +54,22 @@
   | "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)"
 
+setup {* Predicate_Compile.add_equations @{const_name partition} *}
+(*
 code_pred partition
   using assms by (rule partition.cases)
+*)
 
 thm partition.equation
 
 (*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
   [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*)
 
-
+setup {* Predicate_Compile.add_equations @{const_name tranclp} *}
+(*
 code_pred tranclp
   using assms by (rule tranclp.cases)
+*)
 
 thm tranclp.equation
 
@@ -56,13 +77,17 @@
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
 
+setup {* Predicate_Compile.add_equations @{const_name succ} *} 
+(*
 code_pred succ
   using assms by (rule succ.cases)
-
+*)
 thm succ.equation
 
+(*
 values 20 "{n. tranclp succ 10 n}"
 values "{n. tranclp succ n 10}"
 values 20 "{(n, m). tranclp succ n m}"
+*)
 
 end
\ No newline at end of file