isabelle: src/HOL/Predicate_Compile_Examples/Hotel_Example_Small

40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	1	theory Hotel_Example_Small_Generator
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 41231 diff changeset	2	imports Hotel_Example "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	3	uses "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	4	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	5
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	6	declare Let_def[code_pred_inline]
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	7
40137 9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	8	lemma [code_pred_inline]: "insert == (%y A x. y = x \| A x)"
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	9	by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	10
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	11	lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	12	by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	13
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	14	instantiation room :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	15	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	16
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	17	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	18	"small_lazy i = Lazy_Sequence.single Room0"
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	19
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	20	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	21
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	22	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	23
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	24	instantiation key :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	25	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	26
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	27	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	28	"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Key0) (Lazy_Sequence.append (Lazy_Sequence.single Key1) (Lazy_Sequence.append (Lazy_Sequence.single Key2) (Lazy_Sequence.single Key3)))"
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	29
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	30	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	31
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	32	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	33
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	34	instantiation guest :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	35	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	36
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	37	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	38	"small_lazy i = Lazy_Sequence.append (Lazy_Sequence.single Guest0) (Lazy_Sequence.single Guest1)"
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	39
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	40	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	41
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	42	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	43
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	44	setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_14", Predicate_Compile_Quickcheck.quickcheck_compile_term
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	45	Predicate_Compile_Aux.Pos_Generator_DSeq true true 14)) *}
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	46
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	47
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	48	setup {* Context.theory_map (Quickcheck.add_generator ("small_generators_depth_15", Predicate_Compile_Quickcheck.quickcheck_compile_term
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	49	Predicate_Compile_Aux.Pos_Generator_DSeq true true 15)) *}
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	50
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	51	lemma
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	52	"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
42291 682b35dc1926 raised timeout further, for SML/NJ krauss parents: 42142 diff changeset	53	(quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 1200.0, expect = no_counterexample])
42397 13798dcbdca5 raised timeouts further, for SML/NJ! krauss parents: 42291 diff changeset	54	quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 2400.0, expect = counterexample]
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	55	oops
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	56
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	57
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	58	end

author	blanchet
	Mon, 06 Jun 2011 20:36:35 +0200
changeset 43188	0c36ae874fcc
parent 42397	13798dcbdca5
child 43888	ee4be704c2a4
permissions	-rw-r--r--