# HG changeset patch # User bulwahn # Date 1282748389 -7200 # Node ID 5bbdd9a9df6252663bfe4992d836b14241640de3 # Parent 9c9d1482738045da3a909cf43978d5c4ea7362ec adding hotel keycard example for prolog generation diff -r 9c9d14827380 -r 5bbdd9a9df62 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Aug 25 16:59:48 2010 +0200 +++ b/src/HOL/IsaMakefile Wed Aug 25 16:59:49 2010 +0200 @@ -1321,7 +1321,8 @@ Predicate_Compile_Examples/ROOT.ML \ Predicate_Compile_Examples/Predicate_Compile_Examples.thy \ Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \ - Predicate_Compile_Examples/Code_Prolog_Examples.thy + Predicate_Compile_Examples/Code_Prolog_Examples.thy \ + Predicate_Compile_Examples/Hotel_Example.thy @$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples diff -r 9c9d14827380 -r 5bbdd9a9df62 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Wed Aug 25 16:59:49 2010 +0200 @@ -0,0 +1,93 @@ +theory Hotel_Example +imports Predicate_Compile_Alternative_Defs Code_Prolog +begin + +datatype guest = Guest0 | Guest1 +datatype key = Key0 | Key1 | Key2 | Key3 +datatype room = Room0 + +types card = "key * key" + +datatype event = + Check_in guest room card | Enter guest room card | Exit guest room + +definition initk :: "room \ key" + where "initk = (%r. Key0)" + +declare initk_def[code_pred_def, code] + +primrec owns :: "event list \ room \ guest option" +where + "owns [] r = None" +| "owns (e#s) r = (case e of + Check_in g r' c \ if r' = r then Some g else owns s r | + Enter g r' c \ owns s r | + Exit g r' \ owns s r)" + +primrec currk :: "event list \ room \ key" +where + "currk [] r = initk r" +| "currk (e#s) r = (let k = currk s r in + case e of Check_in g r' (k1, k2) \ if r' = r then k2 else k + | Enter g r' c \ k + | Exit g r \ k)" + +primrec issued :: "event list \ key set" +where + "issued [] = range initk" +| "issued (e#s) = issued s \ + (case e of Check_in g r (k1, k2) \ {k2} | Enter g r c \ {} | Exit g r \ {})" + +primrec cards :: "event list \ guest \ card set" +where + "cards [] g = {}" +| "cards (e#s) g = (let C = cards s g in + case e of Check_in g' r c \ if g' = g then insert c C + else C + | Enter g r c \ C + | Exit g r \ C)" + +primrec roomk :: "event list \ room \ key" +where + "roomk [] r = initk r" +| "roomk (e#s) r = (let k = roomk s r in + case e of Check_in g r' c \ k + | Enter g r' (x,y) \ if r' = r (*& x = k*) then y else k + | Exit g r \ k)" + +primrec isin :: "event list \ room \ guest set" +where + "isin [] r = {}" +| "isin (e#s) r = (let G = isin s r in + case e of Check_in g r c \ G + | Enter g r' c \ if r' = r then {g} \ G else G + | Exit g r' \ if r'=r then G - {g} else G)" + +primrec hotel :: "event list \ bool" +where + "hotel [] = True" +| "hotel (e # s) = (hotel s & (case e of + Check_in g r (k,k') \ k = currk s r \ k' \ issued s | + Enter g r (k,k') \ (k,k') : cards s g & (roomk s r : {k, k'}) | + Exit g r \ False))" + +lemma issued_nil: "issued [] = {Key0}" +by (auto simp add: initk_def) + +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) + +declare Let_def[code_pred_inline] + +lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" +by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) + +lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" +by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) + +code_pred [new_random_dseq inductify, skip_proof] hotel . + +ML {* Code_Prolog.options := {ensure_groundness = true} *} + +values 10 "{s. hotel s}" + +end \ No newline at end of file diff -r 9c9d14827380 -r 5bbdd9a9df62 src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Aug 25 16:59:48 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Wed Aug 25 16:59:49 2010 +0200 @@ -1,2 +1,2 @@ use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"]; -if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples"]; +if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example"];