splitting Hotel Key card example into specification and the two tests for counter example generation
authorbulwahn
Fri Oct 22 18:38:59 2010 +0200 (2010-10-22)
changeset 4010482873a6f2b81
parent 40103 ef73a90ab6e6
child 40105 0d579da1902a
splitting Hotel Key card example into specification and the two tests for counter example generation
src/HOL/IsaMakefile
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
src/HOL/Predicate_Compile_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 22 18:38:59 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 22 18:38:59 2010 +0200
     1.3 @@ -1354,6 +1354,8 @@
     1.4    Predicate_Compile_Examples/Examples.thy				\
     1.5    Predicate_Compile_Examples/Context_Free_Grammar_Example.thy 		\
     1.6    Predicate_Compile_Examples/Hotel_Example.thy 				\
     1.7 +  Predicate_Compile_Examples/Hotel_Example_Prolog.thy 			\
     1.8 +  Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy 		\
     1.9    Predicate_Compile_Examples/IMP_1.thy 					\
    1.10    Predicate_Compile_Examples/IMP_2.thy 					\
    1.11    Predicate_Compile_Examples/IMP_3.thy 					\
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Oct 22 18:38:59 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Oct 22 18:38:59 2010 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Hotel_Example
     2.5 -imports Predicate_Compile_Alternative_Defs Code_Prolog
     2.6 +imports Main
     2.7  begin
     2.8  
     2.9  datatype guest = Guest0 | Guest1
    2.10 @@ -71,145 +71,21 @@
    2.11    Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    2.12    Exit g r \<Rightarrow> g : isin s r))"
    2.13  
    2.14 -lemma issued_nil: "issued [] = {Key0}"
    2.15 -by (auto simp add: initk_def)
    2.16 -
    2.17 -lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    2.18 -
    2.19 -declare Let_def[code_pred_inline]
    2.20 -
    2.21 -lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    2.22 -by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    2.23 -
    2.24 -lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    2.25 -by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    2.26 -
    2.27 -setup {* Code_Prolog.map_code_options (K
    2.28 -  {ensure_groundness = true,
    2.29 -  limit_globally = NONE,
    2.30 -  limited_types = [],
    2.31 -  limited_predicates = [],
    2.32 -  replacing = [],
    2.33 -  manual_reorder = []}) *}
    2.34 -
    2.35 -values 40 "{s. hotel s}"
    2.36 -
    2.37 -
    2.38 -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    2.39 -
    2.40 -lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    2.41 -(*quickcheck[generator = code, iterations = 100000, report]*)
    2.42 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    2.43 -oops
    2.44 -
    2.45 -
    2.46  definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
    2.47  [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
    2.48  
    2.49 -
    2.50  definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    2.51  where
    2.52    "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
    2.53     s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    2.54     no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
    2.55  
    2.56 -section {* Manual setup to find the counterexample *}
    2.57  
    2.58 -setup {* Code_Prolog.map_code_options (K 
    2.59 -  {ensure_groundness = true,
    2.60 -   limit_globally = NONE,
    2.61 -   limited_types = [],
    2.62 -   limited_predicates = [(["hotel"], 4)],
    2.63 -   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    2.64 -   manual_reorder = []}) *}
    2.65 -
    2.66 -lemma
    2.67 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    2.68 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    2.69 -oops
    2.70 -
    2.71 -setup {* Code_Prolog.map_code_options (K 
    2.72 -  {ensure_groundness = true,
    2.73 -   limit_globally = NONE,
    2.74 -   limited_types = [],
    2.75 -   limited_predicates = [(["hotel"], 5)],
    2.76 -   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    2.77 -   manual_reorder = []}) *}
    2.78 -
    2.79 -lemma
    2.80 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    2.81 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    2.82 -oops
    2.83 -
    2.84 -section {* Simulating a global depth limit manually by limiting all predicates *}
    2.85 -
    2.86 -setup {*
    2.87 -  Code_Prolog.map_code_options (K
    2.88 -  {ensure_groundness = true,
    2.89 -  limit_globally = NONE,
    2.90 -  limited_types = [],
    2.91 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    2.92 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
    2.93 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    2.94 -  manual_reorder = []})
    2.95 -*}
    2.96 -
    2.97 -lemma
    2.98 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    2.99 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   2.100 -oops
   2.101 -
   2.102 +section {* Some setup *}
   2.103  
   2.104 -setup {*
   2.105 -  Code_Prolog.map_code_options (K
   2.106 -  {ensure_groundness = true,
   2.107 -  limit_globally = NONE,
   2.108 -  limited_types = [],
   2.109 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
   2.110 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
   2.111 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
   2.112 -  manual_reorder = []})
   2.113 -*}
   2.114 -
   2.115 -lemma
   2.116 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   2.117 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   2.118 -oops
   2.119 -
   2.120 -section {* Using a global limit for limiting the execution *} 
   2.121 -
   2.122 -text {* A global depth limit of 13 does not suffice to find the counterexample. *}
   2.123 +lemma issued_nil: "issued [] = {Key0}"
   2.124 +by (auto simp add: initk_def)
   2.125  
   2.126 -setup {*
   2.127 -  Code_Prolog.map_code_options (K
   2.128 -  {ensure_groundness = true,
   2.129 -  limit_globally = SOME 13,
   2.130 -  limited_types = [],
   2.131 -  limited_predicates = [],
   2.132 -  replacing = [],
   2.133 -  manual_reorder = []})
   2.134 -*}
   2.135 -
   2.136 -lemma
   2.137 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   2.138 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   2.139 -oops
   2.140 -
   2.141 -text {* But a global depth limit of 14 does. *}
   2.142 -
   2.143 -setup {*
   2.144 -  Code_Prolog.map_code_options (K
   2.145 -  {ensure_groundness = true,
   2.146 -  limit_globally = SOME 14,
   2.147 -  limited_types = [],
   2.148 -  limited_predicates = [],
   2.149 -  replacing = [],
   2.150 -  manual_reorder = []})
   2.151 -*}
   2.152 -
   2.153 -lemma
   2.154 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   2.155 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   2.156 -oops
   2.157 +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
   2.158  
   2.159  end
   2.160 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Oct 22 18:38:59 2010 +0200
     3.3 @@ -0,0 +1,128 @@
     3.4 +theory Hotel_Example_Prolog
     3.5 +imports Hotel_Example Predicate_Compile_Alternative_Defs Code_Prolog
     3.6 +begin
     3.7 +
     3.8 +declare Let_def[code_pred_inline]
     3.9 +
    3.10 +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    3.11 +by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    3.12 +
    3.13 +lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    3.14 +by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    3.15 +
    3.16 +setup {* Code_Prolog.map_code_options (K
    3.17 +  {ensure_groundness = true,
    3.18 +  limit_globally = NONE,
    3.19 +  limited_types = [],
    3.20 +  limited_predicates = [],
    3.21 +  replacing = [],
    3.22 +  manual_reorder = []}) *}
    3.23 +
    3.24 +values 40 "{s. hotel s}"
    3.25 +
    3.26 +setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    3.27 +
    3.28 +lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    3.29 +quickcheck[generator = code, iterations = 100000, report]
    3.30 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    3.31 +oops
    3.32 +
    3.33 +section {* Manual setup to find the counterexample *}
    3.34 +
    3.35 +setup {* Code_Prolog.map_code_options (K 
    3.36 +  {ensure_groundness = true,
    3.37 +   limit_globally = NONE,
    3.38 +   limited_types = [],
    3.39 +   limited_predicates = [(["hotel"], 4)],
    3.40 +   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    3.41 +   manual_reorder = []}) *}
    3.42 +
    3.43 +lemma
    3.44 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    3.45 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    3.46 +oops
    3.47 +
    3.48 +setup {* Code_Prolog.map_code_options (K 
    3.49 +  {ensure_groundness = true,
    3.50 +   limit_globally = NONE,
    3.51 +   limited_types = [],
    3.52 +   limited_predicates = [(["hotel"], 5)],
    3.53 +   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    3.54 +   manual_reorder = []}) *}
    3.55 +
    3.56 +lemma
    3.57 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    3.58 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    3.59 +oops
    3.60 +
    3.61 +section {* Simulating a global depth limit manually by limiting all predicates *}
    3.62 +
    3.63 +setup {*
    3.64 +  Code_Prolog.map_code_options (K
    3.65 +  {ensure_groundness = true,
    3.66 +  limit_globally = NONE,
    3.67 +  limited_types = [],
    3.68 +  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    3.69 +    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
    3.70 +  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    3.71 +  manual_reorder = []})
    3.72 +*}
    3.73 +
    3.74 +lemma
    3.75 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    3.76 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    3.77 +oops
    3.78 +
    3.79 +setup {*
    3.80 +  Code_Prolog.map_code_options (K
    3.81 +  {ensure_groundness = true,
    3.82 +  limit_globally = NONE,
    3.83 +  limited_types = [],
    3.84 +  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    3.85 +    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
    3.86 +  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    3.87 +  manual_reorder = []})
    3.88 +*}
    3.89 +
    3.90 +lemma
    3.91 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    3.92 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    3.93 +oops
    3.94 +
    3.95 +section {* Using a global limit for limiting the execution *} 
    3.96 +
    3.97 +text {* A global depth limit of 13 does not suffice to find the counterexample. *}
    3.98 +
    3.99 +setup {*
   3.100 +  Code_Prolog.map_code_options (K
   3.101 +  {ensure_groundness = true,
   3.102 +  limit_globally = SOME 13,
   3.103 +  limited_types = [],
   3.104 +  limited_predicates = [],
   3.105 +  replacing = [],
   3.106 +  manual_reorder = []})
   3.107 +*}
   3.108 +
   3.109 +lemma
   3.110 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   3.111 +quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   3.112 +oops
   3.113 +
   3.114 +text {* But a global depth limit of 14 does. *}
   3.115 +
   3.116 +setup {*
   3.117 +  Code_Prolog.map_code_options (K
   3.118 +  {ensure_groundness = true,
   3.119 +  limit_globally = SOME 14,
   3.120 +  limited_types = [],
   3.121 +  limited_predicates = [],
   3.122 +  replacing = [],
   3.123 +  manual_reorder = []})
   3.124 +*}
   3.125 +
   3.126 +lemma
   3.127 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   3.128 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   3.129 +oops
   3.130 +
   3.131 +end
   3.132 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Fri Oct 22 18:38:59 2010 +0200
     4.3 @@ -0,0 +1,52 @@
     4.4 +theory Hotel_Example_Small_Generator
     4.5 +imports Hotel_Example Predicate_Compile_Alternative_Defs
     4.6 +uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
     4.7 +begin
     4.8 +
     4.9 +declare Let_def[code_pred_inline]
    4.10 +
    4.11 +instantiation room :: small_lazy
    4.12 +begin
    4.13 +
    4.14 +definition
    4.15 +  "small_lazy i = Lazy_Sequence.single Room0"
    4.16 +
    4.17 +instance ..
    4.18 +
    4.19 +end
    4.20 +
    4.21 +instantiation key :: small_lazy
    4.22 +begin
    4.23 +
    4.24 +definition
    4.25 +  "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)))"
    4.26 +
    4.27 +instance ..
    4.28 +
    4.29 +end
    4.30 +
    4.31 +instantiation guest :: small_lazy
    4.32 +begin
    4.33 +
    4.34 +definition
    4.35 +  "small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
    4.36 +
    4.37 +instance ..
    4.38 +
    4.39 +end
    4.40 +
    4.41 +setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
    4.42 +  Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
    4.43 +
    4.44 +
    4.45 +setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
    4.46 +  Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
    4.47 +
    4.48 +lemma
    4.49 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    4.50 +quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample]
    4.51 +quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample]
    4.52 +oops
    4.53 +
    4.54 +
    4.55 +end
    4.56 \ No newline at end of file
     5.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Fri Oct 22 18:38:59 2010 +0200
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Fri Oct 22 18:38:59 2010 +0200
     5.3 @@ -3,6 +3,7 @@
     5.4    "Predicate_Compile_Tests",
     5.5  (*  "Predicate_Compile_Quickcheck_Examples", -- should be added again soon *)
     5.6    "Specialisation_Examples",
     5.7 +  "Hotel_Example_Small_Generator",
     5.8    "IMP_1",
     5.9    "IMP_2",
    5.10    "IMP_3",
    5.11 @@ -14,7 +15,7 @@
    5.12    (use_thys [
    5.13      "Code_Prolog_Examples",
    5.14      "Context_Free_Grammar_Example",
    5.15 -    "Hotel_Example",
    5.16 +    "Hotel_Example_Prolog",
    5.17      "Lambda_Example",
    5.18      "List_Examples"];
    5.19     Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]);