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	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	4
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 43888 diff changeset	5	ML_file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 43888 diff changeset	6
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	7	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	8
40137 9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	9	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	10	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	11
9eabcb1bfe50 changing test parameters in examples to get to a result within the global timelimit bulwahn parents: 40104 diff changeset	12	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	13	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	14
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	15	instantiation room :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	16	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	17
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	18	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	19	"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	20
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	21	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	22
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	23	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	24
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	25	instantiation key :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	26	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	27
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	28	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	29	"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	30
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	31	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	32
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	33	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	34
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	35	instantiation guest :: small_lazy
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	36	begin
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	37
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	38	definition
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	39	"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	40
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	41	instance ..
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	42
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	43	end
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	44
43888 ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	45	ML {*
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	46	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	47	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	48	*}
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	49
43888 ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	50	setup {*
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	51	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	52	(small_14_active, Predicate_Compile_Quickcheck.test_goals
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	53	(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	54	#> 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	55	(small_15_active, Predicate_Compile_Quickcheck.test_goals
ee4be704c2a4 adapting an experimental setup to changes in quickcheck's infrastructure bulwahn parents: 42397 diff changeset	56	(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	57	*}
40104 82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	58
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	59	lemma
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	60	"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	61	(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	62	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	63	oops
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
82873a6f2b81 splitting Hotel Key card example into specification and the two tests for counter example generation bulwahn parents: diff changeset	66	end

author	kuncar
	Sat, 15 Feb 2014 00:11:17 +0100
changeset 55487	6380313b8ed5
parent 48891	c0eafbd55de3
child 62390	842917225d56
permissions	-rw-r--r--