src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
changeset 39189 d183bf90dabd
parent 38963 b5d126d7be4b
child 39463 7ce0ed8dc4d6
equal deleted inserted replaced
39188:cd6558ed65d7 39189:d183bf90dabd
    14   {ensure_groundness = false,
    14   {ensure_groundness = false,
    15    limited_types = [],
    15    limited_types = [],
    16    limited_predicates = [],
    16    limited_predicates = [],
    17    replacing = [],
    17    replacing = [],
    18    manual_reorder = [],
    18    manual_reorder = [],
       
    19    timeout = Time.fromSeconds 10,
    19    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    20    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    20 
    21 
    21 values "{(x, y, z). append x y z}"
    22 values "{(x, y, z). append x y z}"
    22 
    23 
    23 values 3 "{(x, y, z). append x y z}"
    24 values 3 "{(x, y, z). append x y z}"
    26   {ensure_groundness = false,
    27   {ensure_groundness = false,
    27    limited_types = [],
    28    limited_types = [],
    28    limited_predicates = [],
    29    limited_predicates = [],
    29    replacing = [],
    30    replacing = [],
    30    manual_reorder = [],
    31    manual_reorder = [],
       
    32    timeout = Time.fromSeconds 10,
    31    prolog_system = Code_Prolog.YAP}) *}
    33    prolog_system = Code_Prolog.YAP}) *}
    32 
    34 
    33 values "{(x, y, z). append x y z}"
    35 values "{(x, y, z). append x y z}"
    34 
    36 
    35 setup {* Code_Prolog.map_code_options (K
    37 setup {* Code_Prolog.map_code_options (K
    36   {ensure_groundness = false,
    38   {ensure_groundness = false,
    37    limited_types = [],
    39    limited_types = [],
    38    limited_predicates = [],
    40    limited_predicates = [],
    39    replacing = [],
    41    replacing = [],
    40    manual_reorder = [],
    42    manual_reorder = [],
       
    43    timeout = Time.fromSeconds 10,
    41    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    44    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    42 
    45 
    43 
    46 
    44 section {* Example queens *}
    47 section {* Example queens *}
    45 
    48 
   205   {ensure_groundness = true,
   208   {ensure_groundness = true,
   206    limited_types = [],
   209    limited_types = [],
   207    limited_predicates = [],
   210    limited_predicates = [],
   208    replacing = [],
   211    replacing = [],
   209    manual_reorder = [], 
   212    manual_reorder = [], 
       
   213    timeout = Time.fromSeconds 10,
   210    prolog_system = Code_Prolog.SWI_PROLOG}) *}
   214    prolog_system = Code_Prolog.SWI_PROLOG}) *}
   211 
   215 
   212 values 2 "{y. notB y}"
   216 values 2 "{y. notB y}"
   213 
   217 
   214 inductive notAB :: "abc * abc \<Rightarrow> bool"
   218 inductive notAB :: "abc * abc \<Rightarrow> bool"