src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
author bulwahn
Thu Sep 30 10:48:12 2010 +0200 (2010-09-30)
changeset 39799 fdbea66eae4b
parent 39463 7ce0ed8dc4d6
child 40104 82873a6f2b81
permissions -rw-r--r--
finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)
     1 theory Hotel_Example
     2 imports Predicate_Compile_Alternative_Defs Code_Prolog
     3 begin
     4 
     5 datatype guest = Guest0 | Guest1
     6 datatype key = Key0 | Key1 | Key2 | Key3
     7 datatype room = Room0
     8 
     9 types card = "key * key"
    10 
    11 datatype event =
    12    Check_in guest room card | Enter guest room card | Exit guest room
    13 
    14 definition initk :: "room \<Rightarrow> key"
    15   where "initk = (%r. Key0)"
    16 
    17 declare initk_def[code_pred_def, code]
    18 
    19 primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    20 where
    21   "owns [] r = None"
    22 | "owns (e#s) r = (case e of
    23     Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    24     Enter g r' c \<Rightarrow> owns s r |
    25     Exit g r' \<Rightarrow> owns s r)"
    26 
    27 primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    28 where
    29   "currk [] r = initk r"
    30 | "currk (e#s) r = (let k = currk s r in
    31     case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    32             | Enter g r' c \<Rightarrow> k
    33             | Exit g r \<Rightarrow> k)"
    34 
    35 primrec issued :: "event list \<Rightarrow> key set"
    36 where
    37   "issued [] = range initk"
    38 | "issued (e#s) = issued s \<union>
    39   (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    40 
    41 primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    42 where
    43   "cards [] g = {}"
    44 | "cards (e#s) g = (let C = cards s g in
    45                     case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    46                                                 else C
    47                             | Enter g r c \<Rightarrow> C
    48                             | Exit g r \<Rightarrow> C)"
    49 
    50 primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    51 where
    52   "roomk [] r = initk r"
    53 | "roomk (e#s) r = (let k = roomk s r in
    54     case e of Check_in g r' c \<Rightarrow> k
    55             | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    56             | Exit g r \<Rightarrow> k)"
    57 
    58 primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    59 where
    60   "isin [] r = {}"
    61 | "isin (e#s) r = (let G = isin s r in
    62                  case e of Check_in g r c \<Rightarrow> G
    63                  | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    64                  | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    65 
    66 primrec hotel :: "event list \<Rightarrow> bool"
    67 where
    68   "hotel []  = True"
    69 | "hotel (e # s) = (hotel s & (case e of
    70   Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    71   Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    72   Exit g r \<Rightarrow> g : isin s r))"
    73 
    74 lemma issued_nil: "issued [] = {Key0}"
    75 by (auto simp add: initk_def)
    76 
    77 lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    78 
    79 declare Let_def[code_pred_inline]
    80 
    81 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    82 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    83 
    84 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    85 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    86 
    87 setup {* Code_Prolog.map_code_options (K
    88   {ensure_groundness = true,
    89   limit_globally = NONE,
    90   limited_types = [],
    91   limited_predicates = [],
    92   replacing = [],
    93   manual_reorder = []}) *}
    94 
    95 values 40 "{s. hotel s}"
    96 
    97 
    98 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    99 
   100 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
   101 (*quickcheck[generator = code, iterations = 100000, report]*)
   102 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   103 oops
   104 
   105 
   106 definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
   107 [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
   108 
   109 
   110 definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
   111 where
   112   "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
   113    s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
   114    no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
   115 
   116 section {* Manual setup to find the counterexample *}
   117 
   118 setup {* Code_Prolog.map_code_options (K 
   119   {ensure_groundness = true,
   120    limit_globally = NONE,
   121    limited_types = [],
   122    limited_predicates = [(["hotel"], 4)],
   123    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   124    manual_reorder = []}) *}
   125 
   126 lemma
   127   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   128 quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   129 oops
   130 
   131 setup {* Code_Prolog.map_code_options (K 
   132   {ensure_groundness = true,
   133    limit_globally = NONE,
   134    limited_types = [],
   135    limited_predicates = [(["hotel"], 5)],
   136    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   137    manual_reorder = []}) *}
   138 
   139 lemma
   140   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   141 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   142 oops
   143 
   144 section {* Simulating a global depth limit manually by limiting all predicates *}
   145 
   146 setup {*
   147   Code_Prolog.map_code_options (K
   148   {ensure_groundness = true,
   149   limit_globally = NONE,
   150   limited_types = [],
   151   limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
   152     "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
   153   replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
   154   manual_reorder = []})
   155 *}
   156 
   157 lemma
   158   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   159 quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   160 oops
   161 
   162 
   163 setup {*
   164   Code_Prolog.map_code_options (K
   165   {ensure_groundness = true,
   166   limit_globally = NONE,
   167   limited_types = [],
   168   limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
   169     "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
   170   replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
   171   manual_reorder = []})
   172 *}
   173 
   174 lemma
   175   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   176 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   177 oops
   178 
   179 section {* Using a global limit for limiting the execution *} 
   180 
   181 text {* A global depth limit of 13 does not suffice to find the counterexample. *}
   182 
   183 setup {*
   184   Code_Prolog.map_code_options (K
   185   {ensure_groundness = true,
   186   limit_globally = SOME 13,
   187   limited_types = [],
   188   limited_predicates = [],
   189   replacing = [],
   190   manual_reorder = []})
   191 *}
   192 
   193 lemma
   194   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   195 quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   196 oops
   197 
   198 text {* But a global depth limit of 14 does. *}
   199 
   200 setup {*
   201   Code_Prolog.map_code_options (K
   202   {ensure_groundness = true,
   203   limit_globally = SOME 14,
   204   limited_types = [],
   205   limited_predicates = [],
   206   replacing = [],
   207   manual_reorder = []})
   208 *}
   209 
   210 lemma
   211   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   212 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   213 oops
   214 
   215 end