src/HOL/ex/Predicate_Compile_ex.thy
changeset 31195 12741f23527d
parent 31129 d2cead76fca2
child 31217 c025f32afd4e
equal deleted inserted replaced
31194:1d6926f96440 31195:12741f23527d
    10 code_pred even
    10 code_pred even
    11   using assms by (rule even.cases)
    11   using assms by (rule even.cases)
    12 
    12 
    13 thm even.equation
    13 thm even.equation
    14 
    14 
       
    15 ML_val {* Predicate.yieldn 10 @{code even_0} *}
       
    16 
    15 
    17 
    16 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    18 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    17     append_Nil: "append [] xs xs"
    19     append_Nil: "append [] xs xs"
    18   | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    20   | append_Cons: "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
    19 
    21 
    20 code_pred append
    22 code_pred append
    21   using assms by (rule append.cases)
    23   using assms by (rule append.cases)
    22 
    24 
    23 thm append.equation
    25 thm append.equation
       
    26 
       
    27 ML_val {* Predicate.yieldn 10 (@{code append_3} [1, 2, 3]) *}
    24 
    28 
    25 
    29 
    26 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    30 inductive partition :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    27   for f where
    31   for f where
    28     "partition f [] [] []"
    32     "partition f [] [] []"