adapting and tuning example theories
authorbulwahn
Tue Aug 31 15:21:56 2010 +0200 (2010-08-31)
changeset 38963b5d126d7be4b
parent 38962 3917c2acaec4
child 38964 b1a7bef0907a
adapting and tuning example theories
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 15:07:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 15:21:56 2010 +0200
     1.3 @@ -10,8 +10,12 @@
     1.4    "append [] ys ys"
     1.5  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
     1.6  
     1.7 -setup {* Code_Prolog.map_code_options (K {ensure_groundness = false,
     1.8 -   limited_types = [], limited_predicates = [], replacing = [],
     1.9 +setup {* Code_Prolog.map_code_options (K
    1.10 +  {ensure_groundness = false,
    1.11 +   limited_types = [],
    1.12 +   limited_predicates = [],
    1.13 +   replacing = [],
    1.14 +   manual_reorder = [],
    1.15     prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.16  
    1.17  values "{(x, y, z). append x y z}"
    1.18 @@ -20,14 +24,20 @@
    1.19  
    1.20  setup {* Code_Prolog.map_code_options (K
    1.21    {ensure_groundness = false,
    1.22 -   limited_types = [], limited_predicates = [], replacing = [],
    1.23 +   limited_types = [],
    1.24 +   limited_predicates = [],
    1.25 +   replacing = [],
    1.26 +   manual_reorder = [],
    1.27     prolog_system = Code_Prolog.YAP}) *}
    1.28  
    1.29  values "{(x, y, z). append x y z}"
    1.30  
    1.31  setup {* Code_Prolog.map_code_options (K
    1.32    {ensure_groundness = false,
    1.33 -   limited_types = [], limited_predicates = [], replacing = [],
    1.34 +   limited_types = [],
    1.35 +   limited_predicates = [],
    1.36 +   replacing = [],
    1.37 +   manual_reorder = [],
    1.38     prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.39  
    1.40  
    1.41 @@ -191,11 +201,13 @@
    1.42  where
    1.43    "y \<noteq> B \<Longrightarrow> notB y"
    1.44  
    1.45 -setup {* Code_Prolog.map_code_options (K {ensure_groundness = true,
    1.46 -  limited_types = [],
    1.47 -  limited_predicates = [],
    1.48 -  replacing = [], 
    1.49 -  prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.50 +setup {* Code_Prolog.map_code_options (K
    1.51 +  {ensure_groundness = true,
    1.52 +   limited_types = [],
    1.53 +   limited_predicates = [],
    1.54 +   replacing = [],
    1.55 +   manual_reorder = [], 
    1.56 +   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.57  
    1.58  values 2 "{y. notB y}"
    1.59  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 15:07:51 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 15:21:56 2010 +0200
     2.3 @@ -89,6 +89,7 @@
     2.4    limited_types = [],
     2.5    limited_predicates = [],
     2.6    replacing = [],
     2.7 +  manual_reorder = [],
     2.8    prolog_system = Code_Prolog.SWI_PROLOG}) *}
     2.9  
    2.10  values 40 "{s. hotel s}"
    2.11 @@ -115,8 +116,9 @@
    2.12  setup {* Code_Prolog.map_code_options (K 
    2.13    {ensure_groundness = true,
    2.14     limited_types = [],
    2.15 -   limited_predicates = [("hotel", 5)],
    2.16 +   limited_predicates = [(["hotel"], 5)],
    2.17     replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    2.18 +   manual_reorder = [],
    2.19     prolog_system = Code_Prolog.SWI_PROLOG}) *}
    2.20  
    2.21  lemma
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 15:07:51 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Tue Aug 31 15:21:56 2010 +0200
     3.3 @@ -84,9 +84,10 @@
     3.4  setup {* Code_Prolog.map_code_options (K 
     3.5    { ensure_groundness = true,
     3.6      limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
     3.7 -    limited_predicates = [("typing", 2), ("nthel1", 2)],
     3.8 +    limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
     3.9      replacing = [(("typing", "limited_typing"), "quickcheck"),
    3.10                   (("nthel1", "limited_nthel1"), "lim_typing")],
    3.11 +    manual_reorder = [],
    3.12      prolog_system = Code_Prolog.SWI_PROLOG}) *}
    3.13  
    3.14  lemma