diff -r 562e99c3d316 -r b6d0cff57d96 src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sat Dec 24 15:53:10 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Sat Dec 24 15:53:10 2011 +0100
@@ -6,12 +6,68 @@
 begin
 
 declare Let_def[code_pred_inline]
-
+(*
+thm hotel_def
 lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
 by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
 
 lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
 by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+*)
+
+definition issuedp :: "event list => key => bool"
+where
+  "issuedp evs k = (k \<in> issued evs)"
+
+lemma [code_pred_def]:
+  "issuedp [] Key0 = True"
+  "issuedp (e # s) k = (issuedp s k \<or> (case e of Check_in g r (k1, k2) => k = k2 | _ => False))"
+unfolding issuedp_def issued.simps initk_def
+by (auto split: event.split)
+
+definition cardsp
+where
+ "cardsp s g k = (k \<in> cards s g)"
+
+lemma [code_pred_def]:
+  "cardsp [] g k = False"
+  "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
+unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
+
+definition
+  "isinp evs r g = (g \<in> isin evs r)"
+
+lemma [code_pred_def]:
+  "isinp [] r g = False"
+  "isinp (e # s) r g =
+  (let G = isinp s r
+   in case e of Check_in g' r c => G g
+    | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
+    | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
+unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
+
+declare hotel.simps(1)[code_pred_def]
+lemma [code_pred_def]:
+"hotel (e # s) =
+  (hotel s & (case e of Check_in g r (k, k') => k = currk s r & \<not> issuedp s k'
+  | Enter g r (k, k') => cardsp s g (k, k') & (roomk s r = k \<or> roomk s r = k')
+  | Exit g r => isinp s r g))"
+unfolding hotel.simps issuedp_def cardsp_def isinp_def
+by (auto split: event.split)
+
+declare List.member_rec[code_pred_def]
+
+lemma [code_pred_def]: "no_Check_in s r = (~ (EX g c. List.member s (Check_in g r c)))"
+unfolding no_Check_in_def member_def by auto
+
+lemma [code_pred_def]: "feels_safe s r =
+(EX 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 &
+    no_Check_in (s\<^isub>3 @ s\<^isub>2) r &
+    (\<not> (\<exists> g'. isinp (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r g')))"
+unfolding feels_safe_def isinp_def by auto
 
 setup {* Code_Prolog.map_code_options (K
   {ensure_groundness = true,
@@ -25,8 +81,7 @@
 
 setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
 
-lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[tester = random, iterations = 10000, report]
+lemma "\<lbrakk> hotel s; isinp s r g \<rbrakk> \<Longrightarrow> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
@@ -41,7 +96,7 @@
    manual_reorder = []}) *}
 
 lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
 oops
 
@@ -54,52 +109,18 @@
    manual_reorder = []}) *}
 
 lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = counterexample]
-oops
-
-section {* Simulating a global depth limit manually by limiting all predicates *}
-
-setup {*
-  Code_Prolog.map_code_options (K
-  {ensure_groundness = true,
-  limit_globally = NONE,
-  limited_types = [],
-  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
-    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
-  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
-  manual_reorder = []})
-*}
-
-lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
-oops
-
-setup {*
-  Code_Prolog.map_code_options (K
-  {ensure_groundness = true,
-  limit_globally = NONE,
-  limited_types = [],
-  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
-    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
-  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
-  manual_reorder = []})
-*}
-
-lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops
 
 section {* Using a global limit for limiting the execution *} 
 
-text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+text {* A global depth limit of 10 does not suffice to find the counterexample. *}
 
 setup {*
   Code_Prolog.map_code_options (K
   {ensure_groundness = true,
-  limit_globally = SOME 13,
+  limit_globally = SOME 10,
   limited_types = [],
   limited_predicates = [],
   replacing = [],
@@ -107,16 +128,16 @@
 *}
 
 lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
 oops
 
-text {* But a global depth limit of 14 does. *}
+text {* But a global depth limit of 11 does. *}
 
 setup {*
   Code_Prolog.map_code_options (K
   {ensure_groundness = true,
-  limit_globally = SOME 14,
+  limit_globally = SOME 11,
   limited_types = [],
   limited_predicates = [],
   replacing = [],
@@ -124,7 +145,7 @@
 *}
 
 lemma
-  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+  "hotel s ==> feels_safe s r ==> isinp s r g ==> owns s r = Some g"
 quickcheck[tester = prolog, iterations = 1, expect = counterexample]
 oops