src/HOL/ex/Predicate_Compile_ex.thy
 author haftmann Mon, 18 May 2009 15:45:42 +0200 changeset 31195 12741f23527d parent 31129 d2cead76fca2 child 31217 c025f32afd4e permissions -rw-r--r--
```
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

ML_val {* Predicate.yieldn 10 @{code even_0} *}

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

ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}

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
```