bulwahn@38730: theory Hotel_Example bulwahn@38730: imports Predicate_Compile_Alternative_Defs Code_Prolog bulwahn@38730: begin bulwahn@38730: bulwahn@38730: datatype guest = Guest0 | Guest1 bulwahn@38730: datatype key = Key0 | Key1 | Key2 | Key3 bulwahn@38730: datatype room = Room0 bulwahn@38730: bulwahn@38730: types card = "key * key" bulwahn@38730: bulwahn@38730: datatype event = bulwahn@38730: Check_in guest room card | Enter guest room card | Exit guest room bulwahn@38730: bulwahn@38730: definition initk :: "room \ key" bulwahn@38730: where "initk = (%r. Key0)" bulwahn@38730: bulwahn@38730: declare initk_def[code_pred_def, code] bulwahn@38730: bulwahn@38730: primrec owns :: "event list \ room \ guest option" bulwahn@38730: where bulwahn@38730: "owns [] r = None" bulwahn@38730: | "owns (e#s) r = (case e of bulwahn@38730: Check_in g r' c \ if r' = r then Some g else owns s r | bulwahn@38730: Enter g r' c \ owns s r | bulwahn@38730: Exit g r' \ owns s r)" bulwahn@38730: bulwahn@38730: primrec currk :: "event list \ room \ key" bulwahn@38730: where bulwahn@38730: "currk [] r = initk r" bulwahn@38730: | "currk (e#s) r = (let k = currk s r in bulwahn@38730: case e of Check_in g r' (k1, k2) \ if r' = r then k2 else k bulwahn@38730: | Enter g r' c \ k bulwahn@38730: | Exit g r \ k)" bulwahn@38730: bulwahn@38730: primrec issued :: "event list \ key set" bulwahn@38730: where bulwahn@38730: "issued [] = range initk" bulwahn@38730: | "issued (e#s) = issued s \ bulwahn@38730: (case e of Check_in g r (k1, k2) \ {k2} | Enter g r c \ {} | Exit g r \ {})" bulwahn@38730: bulwahn@38730: primrec cards :: "event list \ guest \ card set" bulwahn@38730: where bulwahn@38730: "cards [] g = {}" bulwahn@38730: | "cards (e#s) g = (let C = cards s g in bulwahn@38730: case e of Check_in g' r c \ if g' = g then insert c C bulwahn@38730: else C bulwahn@38730: | Enter g r c \ C bulwahn@38730: | Exit g r \ C)" bulwahn@38730: bulwahn@38730: primrec roomk :: "event list \ room \ key" bulwahn@38730: where bulwahn@38730: "roomk [] r = initk r" bulwahn@38730: | "roomk (e#s) r = (let k = roomk s r in bulwahn@38730: case e of Check_in g r' c \ k bulwahn@38730: | Enter g r' (x,y) \ if r' = r (*& x = k*) then y else k bulwahn@38730: | Exit g r \ k)" bulwahn@38730: bulwahn@38730: primrec isin :: "event list \ room \ guest set" bulwahn@38730: where bulwahn@38730: "isin [] r = {}" bulwahn@38730: | "isin (e#s) r = (let G = isin s r in bulwahn@38730: case e of Check_in g r c \ G bulwahn@38730: | Enter g r' c \ if r' = r then {g} \ G else G bulwahn@38730: | Exit g r' \ if r'=r then G - {g} else G)" bulwahn@38730: bulwahn@38730: primrec hotel :: "event list \ bool" bulwahn@38730: where bulwahn@38730: "hotel [] = True" bulwahn@38730: | "hotel (e # s) = (hotel s & (case e of bulwahn@38730: Check_in g r (k,k') \ k = currk s r \ k' \ issued s | bulwahn@38730: Enter g r (k,k') \ (k,k') : cards s g & (roomk s r : {k, k'}) | bulwahn@38734: Exit g r \ g : isin s r))" bulwahn@38730: bulwahn@38730: lemma issued_nil: "issued [] = {Key0}" bulwahn@38730: by (auto simp add: initk_def) bulwahn@38730: bulwahn@38730: lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2) bulwahn@38730: bulwahn@38730: declare Let_def[code_pred_inline] bulwahn@38730: bulwahn@38730: lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" bulwahn@38730: by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) bulwahn@38730: bulwahn@38730: lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" bulwahn@38730: by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) bulwahn@38730: bulwahn@38950: setup {* Code_Prolog.map_code_options (K bulwahn@38949: {ensure_groundness = true, bulwahn@38949: limited_types = [], bulwahn@38949: limited_predicates = [], bulwahn@38949: replacing = [], bulwahn@38950: prolog_system = Code_Prolog.SWI_PROLOG}) *} bulwahn@38730: bulwahn@38734: values 40 "{s. hotel s}" bulwahn@38730: bulwahn@38731: bulwahn@38733: setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} bulwahn@38733: bulwahn@38733: lemma "\ hotel s; g \ isin s r \ \ owns s r = Some g" bulwahn@38733: quickcheck[generator = code, iterations = 100000, report] bulwahn@38949: quickcheck[generator = prolog, iterations = 1, expect = counterexample] bulwahn@38733: oops bulwahn@38733: bulwahn@38731: bulwahn@38953: definition no_Check_in :: "event list \ room \ bool" where(*>*) bulwahn@38953: [code del]: "no_Check_in s r \ \(\g c. Check_in g r c \ set s)" bulwahn@38953: bulwahn@38953: bulwahn@38953: definition feels_safe :: "event list \ room \ bool" bulwahn@38953: where bulwahn@38953: "feels_safe s r = (\s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'. bulwahn@38953: s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \ bulwahn@38953: no_Check_in (s\<^isub>3 @ s\<^isub>2) r \ isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})" bulwahn@38953: bulwahn@38953: setup {* Code_Prolog.map_code_options (K bulwahn@38953: {ensure_groundness = true, bulwahn@38953: limited_types = [], bulwahn@38954: limited_predicates = [("hotel", 5)], bulwahn@38953: replacing = [(("hotel", "limited_hotel"), "quickcheck")], bulwahn@38953: prolog_system = Code_Prolog.SWI_PROLOG}) *} bulwahn@38953: bulwahn@38953: lemma bulwahn@38954: "hotel s ==> feels_safe s r ==> g \ isin s r ==> owns s r = Some g" bulwahn@38954: quickcheck[generator = prolog, iterations = 1, expect = counterexample] bulwahn@38953: oops bulwahn@38953: bulwahn@38730: end