# HG changeset patch # User bulwahn # Date 1287765539 -7200 # Node ID 82873a6f2b813a1334bf214e3f38f7474b023c53 # Parent ef73a90ab6e6f8f8dba53ae7923389f3588616ea splitting Hotel Key card example into specification and the two tests for counter example generation diff -r ef73a90ab6e6 -r 82873a6f2b81 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Oct 22 18:38:59 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 22 18:38:59 2010 +0200 @@ -1354,6 +1354,8 @@ Predicate_Compile_Examples/Examples.thy \ Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \ Predicate_Compile_Examples/Hotel_Example.thy \ + Predicate_Compile_Examples/Hotel_Example_Prolog.thy \ + Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy \ Predicate_Compile_Examples/IMP_1.thy \ Predicate_Compile_Examples/IMP_2.thy \ Predicate_Compile_Examples/IMP_3.thy \ diff -r ef73a90ab6e6 -r 82873a6f2b81 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Fri Oct 22 18:38:59 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Fri Oct 22 18:38:59 2010 +0200 @@ -1,5 +1,5 @@ theory Hotel_Example -imports Predicate_Compile_Alternative_Defs Code_Prolog +imports Main begin datatype guest = Guest0 | Guest1 @@ -71,145 +71,21 @@ Enter g r (k,k') \ (k,k') : cards s g & (roomk s r : {k, k'}) | Exit g r \ g : isin s r))" -lemma issued_nil: "issued [] = {Key0}" -by (auto simp add: initk_def) - -lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) - -declare Let_def[code_pred_inline] - -lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" -by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) - -lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" -by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) - -setup {* Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = NONE, - limited_types = [], - limited_predicates = [], - replacing = [], - manual_reorder = []}) *} - -values 40 "{s. hotel s}" - - -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} - -lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" -(*quickcheck[generator = code, iterations = 100000, report]*) -quickcheck[generator = prolog, iterations = 1, expect = counterexample] -oops - - definition no_Check_in :: "event list \ room \ bool" where(*>*) [code del]: "no_Check_in s r \ \(\g c. Check_in g r c \ set s)" - definition feels_safe :: "event list \ room \ bool" where "feels_safe s r = (\s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'. s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \ no_Check_in (s\<^isub>3 @ s\<^isub>2) r \ isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})" -section {* Manual setup to find the counterexample *} -setup {* Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = NONE, - limited_types = [], - limited_predicates = [(["hotel"], 4)], - replacing = [(("hotel", "limited_hotel"), "quickcheck")], - manual_reorder = []}) *} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] -oops - -setup {* Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = NONE, - limited_types = [], - limited_predicates = [(["hotel"], 5)], - replacing = [(("hotel", "limited_hotel"), "quickcheck")], - manual_reorder = []}) *} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = counterexample] -oops - -section {* Simulating a global depth limit manually by limiting all predicates *} - -setup {* - Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = NONE, - limited_types = [], - limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", - "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)], - replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], - manual_reorder = []}) -*} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] -oops - +section {* Some setup *} -setup {* - Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = NONE, - limited_types = [], - limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", - "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)], - replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], - manual_reorder = []}) -*} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = counterexample] -oops - -section {* Using a global limit for limiting the execution *} - -text {* A global depth limit of 13 does not suffice to find the counterexample. *} +lemma issued_nil: "issued [] = {Key0}" +by (auto simp add: initk_def) -setup {* - Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = SOME 13, - limited_types = [], - limited_predicates = [], - replacing = [], - manual_reorder = []}) -*} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] -oops - -text {* But a global depth limit of 14 does. *} - -setup {* - Code_Prolog.map_code_options (K - {ensure_groundness = true, - limit_globally = SOME 14, - limited_types = [], - limited_predicates = [], - replacing = [], - manual_reorder = []}) -*} - -lemma - "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" -quickcheck[generator = prolog, iterations = 1, expect = counterexample] -oops +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) end \ No newline at end of file diff -r ef73a90ab6e6 -r 82873a6f2b81 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Fri Oct 22 18:38:59 2010 +0200 @@ -0,0 +1,128 @@ +theory Hotel_Example_Prolog +imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog +begin + +declare Let_def[code_pred_inline] + +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" +by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) + +lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" +by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection) + +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = NONE, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = []}) *} + +values 40 "{s. hotel s}" + +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} + +lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" +quickcheck[generator = code, iterations = 100000, report] +quickcheck[generator = prolog, iterations = 1, expect = counterexample] +oops + +section {* Manual setup to find the counterexample *} + +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = NONE, + limited_types = [], + limited_predicates = [(["hotel"], 4)], + replacing = [(("hotel", "limited_hotel"), "quickcheck")], + manual_reorder = []}) *} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] +oops + +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = NONE, + limited_types = [], + limited_predicates = [(["hotel"], 5)], + replacing = [(("hotel", "limited_hotel"), "quickcheck")], + manual_reorder = []}) *} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = counterexample] +oops + +section {* Simulating a global depth limit manually by limiting all predicates *} + +setup {* + Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = NONE, + limited_types = [], + limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", + "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)], + replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], + manual_reorder = []}) +*} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] +oops + +setup {* + Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = NONE, + limited_types = [], + limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP", + "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)], + replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")], + manual_reorder = []}) +*} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = counterexample] +oops + +section {* Using a global limit for limiting the execution *} + +text {* A global depth limit of 13 does not suffice to find the counterexample. *} + +setup {* + Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = SOME 13, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = []}) +*} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample] +oops + +text {* But a global depth limit of 14 does. *} + +setup {* + Code_Prolog.map_code_options (K + {ensure_groundness = true, + limit_globally = SOME 14, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = []}) +*} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = prolog, iterations = 1, expect = counterexample] +oops + +end \ No newline at end of file diff -r ef73a90ab6e6 -r 82873a6f2b81 src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Fri Oct 22 18:38:59 2010 +0200 @@ -0,0 +1,52 @@ +theory Hotel_Example_Small_Generator +imports Hotel_Example Predicate_Compile_Alternative_Defs +uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML" +begin + +declare Let_def[code_pred_inline] + +instantiation room :: small_lazy +begin + +definition + "small_lazy i = Lazy_Sequence.single Room0" + +instance .. + +end + +instantiation key :: small_lazy +begin + +definition + "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Key0) (Lazy_Sequence.append (Lazy_Sequence.single Key1) (Lazy_Sequence.append (Lazy_Sequence.single Key2) (Lazy_Sequence.single Key3)))" + +instance .. + +end + +instantiation guest :: small_lazy +begin + +definition + "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)" + +instance .. + +end + +setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term + Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *} + + +setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term + Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *} + +lemma + "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" +quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample] +quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample] +oops + + +end \ No newline at end of file diff -r ef73a90ab6e6 -r 82873a6f2b81 src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Fri Oct 22 18:38:59 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Fri Oct 22 18:38:59 2010 +0200 @@ -3,6 +3,7 @@ "Predicate_Compile_Tests", (* "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *) "Specialisation_Examples", + "Hotel_Example_Small_Generator", "IMP_1", "IMP_2", "IMP_3", @@ -14,7 +15,7 @@ (use_thys [ "Code_Prolog_Examples", "Context_Free_Grammar_Example", - "Hotel_Example", + "Hotel_Example_Prolog", "Lambda_Example", "List_Examples"]; Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]);