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
43888 ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	44	ML {*
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	45	val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	46	val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	47	*}
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	48
43888 ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	49	setup {*
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	50	Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	51	(small_14_active, Predicate_Compile_Quickcheck.test_goals
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	52	(Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	53	#> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	54	(small_15_active, Predicate_Compile_Quickcheck.test_goals
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	55	(Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	56	*}
40104 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	lemma
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	59	"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	60	(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	61	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	62	oops
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	63
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	64
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	65	end

author	wenzelm
	Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389	e8552cba702d
parent 43888	ee4be704c2a4
child 48891	c0eafbd55de3
permissions	-rw-r--r--