src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 39799 fdbea66eae4b
parent 39463 7ce0ed8dc4d6
child 40104 82873a6f2b81
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 30 10:48:11 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     1.3 @@ -86,6 +86,7 @@
     1.4  
     1.5  setup {* Code_Prolog.map_code_options (K
     1.6    {ensure_groundness = true,
     1.7 +  limit_globally = NONE,
     1.8    limited_types = [],
     1.9    limited_predicates = [],
    1.10    replacing = [],
    1.11 @@ -97,7 +98,7 @@
    1.12  setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    1.13  
    1.14  lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.15 -quickcheck[generator = code, iterations = 100000, report]
    1.16 +(*quickcheck[generator = code, iterations = 100000, report]*)
    1.17  quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.18  oops
    1.19  
    1.20 @@ -112,8 +113,24 @@
    1.21     s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    1.22     no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
    1.23  
    1.24 +section {* Manual setup to find the counterexample *}
    1.25 +
    1.26  setup {* Code_Prolog.map_code_options (K 
    1.27    {ensure_groundness = true,
    1.28 +   limit_globally = NONE,
    1.29 +   limited_types = [],
    1.30 +   limited_predicates = [(["hotel"], 4)],
    1.31 +   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.32 +   manual_reorder = []}) *}
    1.33 +
    1.34 +lemma
    1.35 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.36 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    1.37 +oops
    1.38 +
    1.39 +setup {* Code_Prolog.map_code_options (K 
    1.40 +  {ensure_groundness = true,
    1.41 +   limit_globally = NONE,
    1.42     limited_types = [],
    1.43     limited_predicates = [(["hotel"], 5)],
    1.44     replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.45 @@ -124,4 +141,75 @@
    1.46  quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.47  oops
    1.48  
    1.49 +section {* Simulating a global depth limit manually by limiting all predicates *}
    1.50 +
    1.51 +setup {*
    1.52 +  Code_Prolog.map_code_options (K
    1.53 +  {ensure_groundness = true,
    1.54 +  limit_globally = NONE,
    1.55 +  limited_types = [],
    1.56 +  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    1.57 +    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
    1.58 +  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    1.59 +  manual_reorder = []})
    1.60 +*}
    1.61 +
    1.62 +lemma
    1.63 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.64 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    1.65 +oops
    1.66 +
    1.67 +
    1.68 +setup {*
    1.69 +  Code_Prolog.map_code_options (K
    1.70 +  {ensure_groundness = true,
    1.71 +  limit_globally = NONE,
    1.72 +  limited_types = [],
    1.73 +  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    1.74 +    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
    1.75 +  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    1.76 +  manual_reorder = []})
    1.77 +*}
    1.78 +
    1.79 +lemma
    1.80 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.81 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.82 +oops
    1.83 +
    1.84 +section {* Using a global limit for limiting the execution *} 
    1.85 +
    1.86 +text {* A global depth limit of 13 does not suffice to find the counterexample. *}
    1.87 +
    1.88 +setup {*
    1.89 +  Code_Prolog.map_code_options (K
    1.90 +  {ensure_groundness = true,
    1.91 +  limit_globally = SOME 13,
    1.92 +  limited_types = [],
    1.93 +  limited_predicates = [],
    1.94 +  replacing = [],
    1.95 +  manual_reorder = []})
    1.96 +*}
    1.97 +
    1.98 +lemma
    1.99 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.100 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   1.101 +oops
   1.102 +
   1.103 +text {* But a global depth limit of 14 does. *}
   1.104 +
   1.105 +setup {*
   1.106 +  Code_Prolog.map_code_options (K
   1.107 +  {ensure_groundness = true,
   1.108 +  limit_globally = SOME 14,
   1.109 +  limited_types = [],
   1.110 +  limited_predicates = [],
   1.111 +  replacing = [],
   1.112 +  manual_reorder = []})
   1.113 +*}
   1.114 +
   1.115 +lemma
   1.116 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.117 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   1.118 +oops
   1.119 +
   1.120  end
   1.121 \ No newline at end of file