splitting Hotel Key card example into specification and the two tests for counter example generation
--- 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 \
--- 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') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
Exit g r \<Rightarrow> 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 \<and> \<not> 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 "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> 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 \<Rightarrow> room \<Rightarrow> bool" where(*>*)
[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
-
definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
where
"feels_safe s r = (\<exists>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 \<and>
no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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
--- /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 \<and> \<not> 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 "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+end
\ No newline at end of file
--- /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 \<in> 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
--- 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"]);