src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
author bulwahn
Tue Aug 31 15:21:56 2010 +0200 (2010-08-31)
changeset 38963 b5d126d7be4b
parent 38954 80ce658600b0
child 39189 d183bf90dabd
child 39198 f967a16dfcdd
permissions -rw-r--r--
adapting and tuning example theories
     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] expand_fun_eq 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] expand_fun_eq intro!: eq_reflection)
    86 
    87 setup {* Code_Prolog.map_code_options (K
    88   {ensure_groundness = true,
    89   limited_types = [],
    90   limited_predicates = [],
    91   replacing = [],
    92   manual_reorder = [],
    93   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    94 
    95 values 40 "{s. hotel s}"
    96 
    97 
    98 setup {* 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 setup {* Code_Prolog.map_code_options (K 
   117   {ensure_groundness = true,
   118    limited_types = [],
   119    limited_predicates = [(["hotel"], 5)],
   120    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
   121    manual_reorder = [],
   122    prolog_system = Code_Prolog.SWI_PROLOG}) *}
   123 
   124 lemma
   125   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   126 quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   127 oops
   128 
   129 end