changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
authorbulwahn
Tue Aug 31 08:00:56 2010 +0200 (2010-08-31)
changeset 3895480ce658600b0
parent 38953 0c38eb5fc4ca
child 38955 80169aaf6ee6
changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:55 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Aug 31 08:00:56 2010 +0200
     1.3 @@ -112,18 +112,16 @@
     1.4     s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
     1.5     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.6  
     1.7 -ML {* set Code_Prolog.trace *}
     1.8 -
     1.9  setup {* Code_Prolog.map_code_options (K 
    1.10    {ensure_groundness = true,
    1.11     limited_types = [],
    1.12 -   limited_predicates = [("hotel", 2)],
    1.13 +   limited_predicates = [("hotel", 5)],
    1.14     replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.15     prolog_system = Code_Prolog.SWI_PROLOG}) *}
    1.16  
    1.17  lemma
    1.18 -  "hotel s ==> feels_safe s (Room0) ==> g \<in> isin s (Room0) ==> owns s Room0 = Some g"
    1.19 -quickcheck[generator = prolog, iterations = 1]
    1.20 +  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.21 +quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.22  oops
    1.23  
    1.24  end
    1.25 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:55 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Aug 31 08:00:56 2010 +0200
     2.3 @@ -351,7 +351,7 @@
     2.4          |> map (fn (resargs, (names', prems')) =>
     2.5            let
     2.6              val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
     2.7 -          in (prem'::prems', names') end)
     2.8 +          in (prems' @ [prem'], names') end)
     2.9        end
    2.10      val intro_ts' = folds_map rewrite prems frees
    2.11        |> maps (fn (prems', frees') =>