# HG changeset patch
# User bulwahn
# Date 1283234456 -7200
# Node ID 80ce658600b0fee4ce589165c1fad1d3e34e5e95
# Parent  0c38eb5fc4ca89816c306d6d0016c54e740a8503
changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system

diff -r 0c38eb5fc4ca -r 80ce658600b0 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:55 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:56 2010 +0200
@@ -112,18 +112,16 @@
    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)],
+   limited_predicates = [("hotel", 5)],
    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]
+  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
 oops
 
 end
\ No newline at end of file
diff -r 0c38eb5fc4ca -r 80ce658600b0 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:56 2010 +0200
@@ -351,7 +351,7 @@
         |> map (fn (resargs, (names', prems')) =>
           let
             val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
-          in (prem'::prems', names') end)
+          in (prems' @ [prem'], names') end)
       end
     val intro_ts' = folds_map rewrite prems frees
       |> maps (fn (prems', frees') =>