added further hotel key card attack in example file
authorbulwahn
Tue Aug 31 08:00:55 2010 +0200 (2010-08-31)
changeset 389530c38eb5fc4ca
parent 38952 694d0c88d86a
child 38954 80ce658600b0
added further hotel key card attack in example file
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:54 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:55 2010 +0200
     1.3 @@ -102,4 +102,28 @@
     1.4  oops
     1.5  
     1.6  
     1.7 +definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
     1.8 +[code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
     1.9 +
    1.10 +
    1.11 +definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    1.12 +where
    1.13 +  "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
    1.14 +   s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    1.15 +   no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
    1.16 +
    1.17 +ML {* set Code_Prolog.trace *}
    1.18 +
    1.19 +setup {* Code_Prolog.map_code_options (K 
    1.20 +  {ensure_groundness = true,
    1.21 +   limited_types = [],
    1.22 +   limited_predicates = [("hotel", 2)],
    1.23 +   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.24 +   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.25 +
    1.26 +lemma
    1.27 +  "hotel s ==> feels_safe s (Room0) ==> g \<in> isin s (Room0) ==> owns s Room0 = Some g"
    1.28 +quickcheck[generator = prolog, iterations = 1]
    1.29 +oops
    1.30 +
    1.31  end
    1.32 \ No newline at end of file