adapting example files to latest changes
authorbulwahn
Tue Aug 31 08:00:52 2010 +0200 (2010-08-31)
changeset 389491afa9e89c885
parent 38948 c4e6afaa8dcd
child 38950 62578950e748
adapting example files to latest changes
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 08:00:51 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Tue Aug 31 08:00:52 2010 +0200
     1.3 @@ -10,17 +10,26 @@
     1.4    "append [] ys ys"
     1.5  | "append xs ys zs ==> append (x # xs) ys (x # zs)"
     1.6  
     1.7 -ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
     1.8 +ML {* Code_Prolog.options :=
     1.9 +  {ensure_groundness = false,
    1.10 +   limited_types = [], limited_predicates = [], replacing = [],
    1.11 +   prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.12  
    1.13  values "{(x, y, z). append x y z}"
    1.14  
    1.15  values 3 "{(x, y, z). append x y z}"
    1.16  
    1.17 -ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.YAP} *}
    1.18 +ML {* Code_Prolog.options :=
    1.19 +  {ensure_groundness = false,
    1.20 +   limited_types = [], limited_predicates = [], replacing = [],
    1.21 +   prolog_system = Code_Prolog.YAP} *}
    1.22  
    1.23  values "{(x, y, z). append x y z}"
    1.24  
    1.25 -ML {* Code_Prolog.options := { ensure_groundness = false, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.26 +ML {* Code_Prolog.options :=
    1.27 +  {ensure_groundness = false,
    1.28 +   limited_types = [], limited_predicates = [], replacing = [],
    1.29 +   prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.30  
    1.31  
    1.32  section {* Example queens *}
    1.33 @@ -183,7 +192,11 @@
    1.34  where
    1.35    "y \<noteq> B \<Longrightarrow> notB y"
    1.36  
    1.37 -ML {* Code_Prolog.options := {ensure_groundness = true, limited_types = [], prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.38 +ML {* Code_Prolog.options := {ensure_groundness = true,
    1.39 +  limited_types = [],
    1.40 +  limited_predicates = [],
    1.41 +  replacing = [], 
    1.42 +  prolog_system = Code_Prolog.SWI_PROLOG} *}
    1.43  
    1.44  values 2 "{y. notB y}"
    1.45  
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:51 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:52 2010 +0200
     2.3 @@ -84,17 +84,21 @@
     2.4  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
     2.5  by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
     2.6  
     2.7 -ML {* Code_Prolog.options := {ensure_groundness = true} *}
     2.8 +ML {* Code_Prolog.options :=
     2.9 +  {ensure_groundness = true,
    2.10 +  limited_types = [],
    2.11 +  limited_predicates = [],
    2.12 +  replacing = [],
    2.13 +  prolog_system = Code_Prolog.SWI_PROLOG} *}
    2.14  
    2.15  values 40 "{s. hotel s}"
    2.16  
    2.17  
    2.18  setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
    2.19 -ML {* set Code_Prolog.trace *}
    2.20  
    2.21  lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    2.22  quickcheck[generator = code, iterations = 100000, report]
    2.23 -quickcheck[generator = prolog, iterations = 1]
    2.24 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    2.25  oops
    2.26  
    2.27