src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
changeset 40104 82873a6f2b81
parent 39799 fdbea66eae4b
child 42463 f270e3e18be5
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Oct 22 18:38:59 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Fri Oct 22 18:38:59 2010 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  theory Hotel_Example
     1.5 -imports Predicate_Compile_Alternative_Defs Code_Prolog
     1.6 +imports Main
     1.7  begin
     1.8  
     1.9  datatype guest = Guest0 | Guest1
    1.10 @@ -71,145 +71,21 @@
    1.11    Enter g r (k,k') \<Rightarrow> (k,k') : cards s g & (roomk s r : {k, k'}) |
    1.12    Exit g r \<Rightarrow> g : isin s r))"
    1.13  
    1.14 -lemma issued_nil: "issued [] = {Key0}"
    1.15 -by (auto simp add: initk_def)
    1.16 -
    1.17 -lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
    1.18 -
    1.19 -declare Let_def[code_pred_inline]
    1.20 -
    1.21 -lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    1.22 -by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    1.23 -
    1.24 -lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
    1.25 -by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
    1.26 -
    1.27 -setup {* Code_Prolog.map_code_options (K
    1.28 -  {ensure_groundness = true,
    1.29 -  limit_globally = NONE,
    1.30 -  limited_types = [],
    1.31 -  limited_predicates = [],
    1.32 -  replacing = [],
    1.33 -  manual_reorder = []}) *}
    1.34 -
    1.35 -values 40 "{s. hotel s}"
    1.36 -
    1.37 -
    1.38 -setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
    1.39 -
    1.40 -lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
    1.41 -(*quickcheck[generator = code, iterations = 100000, report]*)
    1.42 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.43 -oops
    1.44 -
    1.45 -
    1.46  definition no_Check_in :: "event list \<Rightarrow> room \<Rightarrow> bool" where(*>*)
    1.47  [code del]: "no_Check_in s r \<equiv> \<not>(\<exists>g c. Check_in g r c \<in> set s)"
    1.48  
    1.49 -
    1.50  definition feels_safe :: "event list \<Rightarrow> room \<Rightarrow> bool"
    1.51  where
    1.52    "feels_safe s r = (\<exists>s\<^isub>1 s\<^isub>2 s\<^isub>3 g c c'.
    1.53     s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
    1.54     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.55  
    1.56 -section {* Manual setup to find the counterexample *}
    1.57  
    1.58 -setup {* Code_Prolog.map_code_options (K 
    1.59 -  {ensure_groundness = true,
    1.60 -   limit_globally = NONE,
    1.61 -   limited_types = [],
    1.62 -   limited_predicates = [(["hotel"], 4)],
    1.63 -   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.64 -   manual_reorder = []}) *}
    1.65 -
    1.66 -lemma
    1.67 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.68 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
    1.69 -oops
    1.70 -
    1.71 -setup {* Code_Prolog.map_code_options (K 
    1.72 -  {ensure_groundness = true,
    1.73 -   limit_globally = NONE,
    1.74 -   limited_types = [],
    1.75 -   limited_predicates = [(["hotel"], 5)],
    1.76 -   replacing = [(("hotel", "limited_hotel"), "quickcheck")],
    1.77 -   manual_reorder = []}) *}
    1.78 -
    1.79 -lemma
    1.80 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.81 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
    1.82 -oops
    1.83 -
    1.84 -section {* Simulating a global depth limit manually by limiting all predicates *}
    1.85 -
    1.86 -setup {*
    1.87 -  Code_Prolog.map_code_options (K
    1.88 -  {ensure_groundness = true,
    1.89 -  limit_globally = NONE,
    1.90 -  limited_types = [],
    1.91 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
    1.92 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
    1.93 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
    1.94 -  manual_reorder = []})
    1.95 -*}
    1.96 -
    1.97 -lemma
    1.98 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    1.99 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   1.100 -oops
   1.101 -
   1.102 +section {* Some setup *}
   1.103  
   1.104 -setup {*
   1.105 -  Code_Prolog.map_code_options (K
   1.106 -  {ensure_groundness = true,
   1.107 -  limit_globally = NONE,
   1.108 -  limited_types = [],
   1.109 -  limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
   1.110 -    "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
   1.111 -  replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
   1.112 -  manual_reorder = []})
   1.113 -*}
   1.114 -
   1.115 -lemma
   1.116 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.117 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   1.118 -oops
   1.119 -
   1.120 -section {* Using a global limit for limiting the execution *} 
   1.121 -
   1.122 -text {* A global depth limit of 13 does not suffice to find the counterexample. *}
   1.123 +lemma issued_nil: "issued [] = {Key0}"
   1.124 +by (auto simp add: initk_def)
   1.125  
   1.126 -setup {*
   1.127 -  Code_Prolog.map_code_options (K
   1.128 -  {ensure_groundness = true,
   1.129 -  limit_globally = SOME 13,
   1.130 -  limited_types = [],
   1.131 -  limited_predicates = [],
   1.132 -  replacing = [],
   1.133 -  manual_reorder = []})
   1.134 -*}
   1.135 -
   1.136 -lemma
   1.137 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.138 -quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
   1.139 -oops
   1.140 -
   1.141 -text {* But a global depth limit of 14 does. *}
   1.142 -
   1.143 -setup {*
   1.144 -  Code_Prolog.map_code_options (K
   1.145 -  {ensure_groundness = true,
   1.146 -  limit_globally = SOME 14,
   1.147 -  limited_types = [],
   1.148 -  limited_predicates = [],
   1.149 -  replacing = [],
   1.150 -  manual_reorder = []})
   1.151 -*}
   1.152 -
   1.153 -lemma
   1.154 -  "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
   1.155 -quickcheck[generator = prolog, iterations = 1, expect = counterexample]
   1.156 -oops
   1.157 +lemmas issued_simps[code, code_pred_def] = issued_nil issued.simps(2)
   1.158  
   1.159  end
   1.160 \ No newline at end of file