examples using code_pred

--- a/src/HOL/ex/Predicate_Compile.thy	Tue May 12 17:09:35 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue May 12 17:09:36 2009 +0200
@@ -7,11 +7,6 @@
 
 setup {* Predicate_Compile.setup *}
 
-ML {*
-  OuterSyntax.local_theory_to_proof "code_pred" "sets up goal for cases rule from given introduction rules and compiles predicate"
-  OuterKeyword.thy_goal (OuterParse.term_group >> Predicate_Compile.code_pred_cmd)
-*}
-
 
 text {* Experimental code *}
 
@@ -59,16 +54,20 @@
   | "even n \<Longrightarrow> odd (Suc n)"
   | "odd n \<Longrightarrow> even (Suc n)"
 
-setup {* pred_compile "even" *}
-thm even_codegen
+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)"
 
-setup {* pred_compile "append" *}
-thm append_codegen
+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"
@@ -77,27 +76,21 @@
   | "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 {* pred_compile "partition" *}
-thm partition_codegen
+code_pred partition
+  using assms by (rule partition.cases)
+
+thm partition.equation
+
 
-setup {* pred_compile "tranclp" *}
-thm tranclp_codegen
+code_pred tranclp
+  using assms by (rule tranclp.cases)
+
+thm tranclp.equation
+
 
 ML_val {* Predicate_Compile.modes_of @{theory} @{const_name partition} *}
 ML_val {* Predicate_Compile.modes_of @{theory} @{const_name tranclp} *}
 
 ML_val {* Predicate.analyze_compr @{theory} @{term "{n. odd n}"} *}
 
-section {* Example for user interface *}
-
-inductive append2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-    append2_Nil: "append2 [] xs xs"
-  | append2_Cons: "append2 xs ys zs \<Longrightarrow> append2 (x # xs) ys (x # zs)"
-
-(*code_pred append2
-  using assms by (rule append2.cases)
-
-thm append2_codegen
-thm append2_cases*)
-
 end
\ No newline at end of file