# HG changeset patch
# User bulwahn
# Date 1283234455 -7200
# Node ID 0c38eb5fc4ca89816c306d6d0016c54e740a8503
# Parent  694d0c88d86ab4c6fe88b91090f9914d7c9fc2f4
added further hotel key card attack in example file

diff -r 694d0c88d86a -r 0c38eb5fc4ca src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:54 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:55 2010 +0200
@@ -102,4 +102,28 @@
 oops
 
 
+definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
+[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
+
+
+definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
+where
+  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
+   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
+   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+
+ML {* set Code_Prolog.trace *}
+
+setup {* Code_Prolog.map_code_options (K 
+  {ensure_groundness = true,
+   limited_types = [],
+   limited_predicates = [("hotel", 2)],
+   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma
+  "hotel s ==> feels_safe s (Room0) ==> g \<in> isin s (Room0) ==> owns s Room0 = Some g"
+quickcheck[generator = prolog, iterations = 1]
+oops
+
 end
\ No newline at end of file