--- 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
--- 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
--- /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
--- 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 [