adding hotel keycard example for prolog generation
authorbulwahn
Wed Aug 25 16:59:49 2010 +0200 (2010-08-25)
changeset 387305bbdd9a9df62
parent 38729 9c9d14827380
child 38731 2c8a595af43e
adding hotel keycard example for prolog generation
src/HOL/IsaMakefile
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Aug 25 16:59:48 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Aug 25 16:59:49 2010 +0200
     1.3 @@ -1321,7 +1321,8 @@
     1.4    Predicate_Compile_Examples/ROOT.ML					\
     1.5    Predicate_Compile_Examples/Predicate_Compile_Examples.thy		\
     1.6    Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
     1.7 -  Predicate_Compile_Examples/Code_Prolog_Examples.thy
     1.8 +  Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
     1.9 +  Predicate_Compile_Examples/Hotel_Example.thy
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
    1.11  
    1.12  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Wed Aug 25 16:59:49 2010 +0200
     2.3 @@ -0,0 +1,93 @@
     2.4 +theory Hotel_Example
     2.5 +imports Predicate_Compile_Alternative_Defs Code_Prolog
     2.6 +begin
     2.7 +
     2.8 +datatype guest = Guest0 | Guest1
     2.9 +datatype key = Key0 | Key1 | Key2 | Key3
    2.10 +datatype room = Room0
    2.11 +
    2.12 +types card = "key * key"
    2.13 +
    2.14 +datatype event =
    2.15 +   Check_in guest room card | Enter guest room card | Exit guest room
    2.16 +
    2.17 +definition initk :: "room \<Rightarrow> key"
    2.18 +  where "initk = (%r. Key0)"
    2.19 +
    2.20 +declare initk_def[code_pred_def, code]
    2.21 +
    2.22 +primrec owns :: "event list \<Rightarrow> room \<Rightarrow> guest option"
    2.23 +where
    2.24 +  "owns [] r = None"
    2.25 +| "owns (e#s) r = (case e of
    2.26 +    Check_in g r' c \<Rightarrow> if r' = r then Some g else owns s r |
    2.27 +    Enter g r' c \<Rightarrow> owns s r |
    2.28 +    Exit g r' \<Rightarrow> owns s r)"
    2.29 +
    2.30 +primrec currk :: "event list \<Rightarrow> room \<Rightarrow> key"
    2.31 +where
    2.32 +  "currk [] r = initk r"
    2.33 +| "currk (e#s) r = (let k = currk s r in
    2.34 +    case e of Check_in g r' (k1, k2) \<Rightarrow> if r' = r then k2 else k
    2.35 +            | Enter g r' c \<Rightarrow> k
    2.36 +            | Exit g r \<Rightarrow> k)"
    2.37 +
    2.38 +primrec issued :: "event list \<Rightarrow> key set"
    2.39 +where
    2.40 +  "issued [] = range initk"
    2.41 +| "issued (e#s) = issued s \<union>
    2.42 +  (case e of Check_in g r (k1, k2) \<Rightarrow> {k2} | Enter g r c \<Rightarrow> {} | Exit g r \<Rightarrow> {})"
    2.43 +
    2.44 +primrec cards :: "event list \<Rightarrow> guest \<Rightarrow> card set"
    2.45 +where
    2.46 +  "cards [] g = {}"
    2.47 +| "cards (e#s) g = (let C = cards s g in
    2.48 +                    case e of Check_in g' r c \<Rightarrow> if g' = g then insert c C
    2.49 +                                                else C
    2.50 +                            | Enter g r c \<Rightarrow> C
    2.51 +                            | Exit g r \<Rightarrow> C)"
    2.52 +
    2.53 +primrec roomk :: "event list \<Rightarrow> room \<Rightarrow> key"
    2.54 +where
    2.55 +  "roomk [] r = initk r"
    2.56 +| "roomk (e#s) r = (let k = roomk s r in
    2.57 +    case e of Check_in g r' c \<Rightarrow> k
    2.58 +            | Enter g r' (x,y) \<Rightarrow> if r' = r (*& x = k*) then y else k
    2.59 +            | Exit g r \<Rightarrow> k)"
    2.60 +
    2.61 +primrec isin :: "event list \<Rightarrow> room \<Rightarrow> guest set"
    2.62 +where
    2.63 +  "isin [] r = {}"
    2.64 +| "isin (e#s) r = (let G = isin s r in
    2.65 +                 case e of Check_in g r c \<Rightarrow> G
    2.66 +                 | Enter g r' c \<Rightarrow> if r' = r then {g} \<union> G else G
    2.67 +                 | Exit g r' \<Rightarrow> if r'=r then G - {g} else G)"
    2.68 +
    2.69 +primrec hotel :: "event list \<Rightarrow> bool"
    2.70 +where
    2.71 +  "hotel []  = True"
    2.72 +| "hotel (e # s) = (hotel s & (case e of
    2.73 +  Check_in g r (k,k') \<Rightarrow> k = currk s r \<and> k' \<notin> issued s |
    2.74 +  Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    2.75 +  Exit g r \<Rightarrow> False))"
    2.76 +
    2.77 +lemma issued_nil: "issued [] = {Key0}"
    2.78 +by (auto simp add: initk_def)
    2.79 +
    2.80 +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    2.81 +
    2.82 +declare Let_def[code_pred_inline]
    2.83 +
    2.84 +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    2.85 +by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    2.86 +
    2.87 +lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    2.88 +by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    2.89 +
    2.90 +code_pred [new_random_dseq inductify, skip_proof] hotel .
    2.91 +
    2.92 +ML {* Code_Prolog.options := {ensure_groundness = true} *}
    2.93 +
    2.94 +values 10 "{s. hotel s}"
    2.95 +
    2.96 +end
    2.97 \ No newline at end of file
     3.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Aug 25 16:59:48 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Wed Aug 25 16:59:49 2010 +0200
     3.3 @@ -1,2 +1,2 @@
     3.4  use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
     3.5 -if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples"];
     3.6 +if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"];