# HG changeset patch
# User haftmann
# Date 1242155867 -7200
# Node ID d2cead76fca25ef671f7bc7fe8d27eee254b15d5
# Parent  b3bb28c8740989c03d65d9c2bca923b32d2c0a04
split Predicate_Compile examples into separate theory

diff -r b3bb28c87409 -r d2cead76fca2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 12 21:17:38 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue May 12 21:17:47 2009 +0200
@@ -854,7 +854,7 @@
   ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
   ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
-  ex/Predicate_Compile.thy ex/predicate_compile.ML
+  ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
diff -r b3bb28c87409 -r d2cead76fca2 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Tue May 12 21:17:38 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Tue May 12 21:17:47 2009 +0200
@@ -46,51 +46,4 @@
 end;
 *}
 
-
-text {* Example(s) *}
-
-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
-
-
-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}"} *}
-
 end
\ No newline at end of file
diff -r b3bb28c87409 -r d2cead76fca2 src/HOL/ex/Predicate_Compile_ex.thy
--- /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
diff -r b3bb28c87409 -r d2cead76fca2 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Tue May 12 21:17:38 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Tue May 12 21:17:47 2009 +0200
@@ -16,7 +16,8 @@
   "Codegenerator_Pretty",
   "NormalForm",
   "../NumberTheory/Factorization",
-  "Predicate_Compile"
+  "Predicate_Compile",
+  "Predicate_Compile_ex"
 ];
 
 use_thys [