src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 38730 5bbdd9a9df62
child 38731 2c8a595af43e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:49 2010 +0200
     1.3 @@ -0,0 +1,93 @@
     1.4 +theory Hotel_Example
     1.5 +imports Predicate_Compile_Alternative_Defs Code_Prolog
     1.6 +begin
     1.7 +
     1.8 +datatype guest = Guest0 | Guest1
     1.9 +datatype key = Key0 | Key1 | Key2 | Key3
    1.10 +datatype room = Room0
    1.11 +
    1.12 +types card = "key * key"
    1.13 +
    1.14 +datatype event =
    1.15 +   Check_in guest room card | Enter guest room card | Exit guest room
    1.16 +
    1.17 +definition initk :: "room \<Rightarrow> key"
    1.18 +  where "initk = (%r. Key0)"
    1.19 +
    1.20 +declare initk_def[code_pred_def, code]
    1.21 +
    1.22 +primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    1.23 +where
    1.24 +  "owns [] r = None"
    1.25 +| "owns (e#s) r = (case e of
    1.26 +    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    1.27 +    Enter g r' c \<Rightarrow> owns s r |
    1.28 +    Exit g r' \<Rightarrow> owns s r)"
    1.29 +
    1.30 +primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    1.31 +where
    1.32 +  "currk [] r = initk r"
    1.33 +| "currk (e#s) r = (let k = currk s r in
    1.34 +    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    1.35 +            | Enter g r' c \<Rightarrow> k
    1.36 +            | Exit g r \<Rightarrow> k)"
    1.37 +
    1.38 +primrec issued :: "event list \<Rightarrow> key set"
    1.39 +where
    1.40 +  "issued [] = range initk"
    1.41 +| "issued (e#s) = issued s \<union>
    1.42 +  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    1.43 +
    1.44 +primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    1.45 +where
    1.46 +  "cards [] g = {}"
    1.47 +| "cards (e#s) g = (let C = cards s g in
    1.48 +                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    1.49 +                                                else C
    1.50 +                            | Enter g r c \<Rightarrow> C
    1.51 +                            | Exit g r \<Rightarrow> C)"
    1.52 +
    1.53 +primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    1.54 +where
    1.55 +  "roomk [] r = initk r"
    1.56 +| "roomk (e#s) r = (let k = roomk s r in
    1.57 +    case e of Check_in g r' c \<Rightarrow> k
    1.58 +            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    1.59 +            | Exit g r \<Rightarrow> k)"
    1.60 +
    1.61 +primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    1.62 +where
    1.63 +  "isin [] r = {}"
    1.64 +| "isin (e#s) r = (let G = isin s r in
    1.65 +                 case e of Check_in g r c \<Rightarrow> G
    1.66 +                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    1.67 +                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    1.68 +
    1.69 +primrec hotel :: "event list \<Rightarrow> bool"
    1.70 +where
    1.71 +  "hotel []  = True"
    1.72 +| "hotel (e # s) = (hotel s & (case e of
    1.73 +  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    1.74 +  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    1.75 +  Exit g r \<Rightarrow> False))"
    1.76 +
    1.77 +lemma issued_nil: "issued [] = {Key0}"
    1.78 +by (auto simp add: initk_def)
    1.79 +
    1.80 +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    1.81 +
    1.82 +declare Let_def[code_pred_inline]
    1.83 +
    1.84 +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    1.85 +by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    1.86 +
    1.87 +lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    1.88 +by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    1.89 +
    1.90 +code_pred [new_random_dseq inductify, skip_proof] hotel .
    1.91 +
    1.92 +ML {* Code_Prolog.options := {ensure_groundness = true} *}
    1.93 +
    1.94 +values 10 "{s. hotel s}"
    1.95 +
    1.96 +end
    1.97 \ No newline at end of file