added a new example for the predicate compiler
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32670cc0bae788b7e
parent 32669 462b1dd67a58
child 32671 fbd224850767
added a new example for the predicate compiler
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -181,17 +181,22 @@
     1.4  
     1.5  value [code] "Predicate.singleton (divmod_rel_1_2 1705 42)"
     1.6  
     1.7 -subsection {* Executing definitions *}
     1.8 +section {* Executing definitions *}
     1.9  
    1.10  definition Min
    1.11  where "Min s r x \<equiv> s x \<and> (\<forall>y. r x y \<longrightarrow> x = y)"
    1.12  
    1.13  code_pred (inductify_all) Min .
    1.14  
    1.15 +subsection {* Examples with lists *}
    1.16 +
    1.17  code_pred (inductify_all) lexord .
    1.18  
    1.19  thm lexord.equation
    1.20 -
    1.21 +(*
    1.22 +lemma "(u, v) : lexord r ==> (x @ u, x @ v) : lexord r"
    1.23 +quickcheck
    1.24 +*)
    1.25  
    1.26  lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv
    1.27  
    1.28 @@ -204,6 +209,10 @@
    1.29  code_pred (inductify_all) (rpred) lenlex .
    1.30  thm lenlex.rpred_equation
    1.31  *)
    1.32 +thm lists.intros
    1.33 +code_pred (inductify_all) lists .
    1.34 +
    1.35 +thm lists.equation
    1.36  
    1.37  datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
    1.38  fun height :: "'a tree => nat" where