isabelle: src/HOL/Predicate_Compile_Examples/IMP

39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	1	theory IMP_1
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	2	imports "HOL-Library.Predicate_Compile_Quickcheck"
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	3	begin
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	4
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58310 diff changeset	5	subsection \<open>IMP\<close>
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	6
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58310 diff changeset	7	text \<open>
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	8	In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58310 diff changeset	9	\<close>
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	10
42031 2de57cda5b24 adapting predicate_compile_quickcheck; tuned bulwahn parents: 41413 diff changeset	11	type_synonym var = unit
2de57cda5b24 adapting predicate_compile_quickcheck; tuned bulwahn parents: 41413 diff changeset	12	type_synonym state = bool
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	13
58310 91ea607a34d8 updated news blanchet parents: 58249 diff changeset	14	datatype com =
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	15	Skip \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	16	Ass bool \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	17	Seq com com \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	18	IF com com
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	19
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	20	inductive exec :: "com => state => state => bool" where
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	21	"exec Skip s s" \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	22	"exec (Ass e) s e" \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	23	"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	24	"s ==> exec c1 s t ==> exec (IF c1 c2) s t" \|
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	25	"\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t"
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	26
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	27	lemma
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	28	"exec c s s' ==> exec (Seq c c) s s'"
45451 74515e8e6046 renaming example invocations: tester predicate_compile is renamed to smart_exhaustive bulwahn parents: 43686 diff changeset	29	quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
39186 475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	30	oops
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	31
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	32
475856793715 adding IMP quickcheck examples bulwahn parents: diff changeset	33	end

author	wenzelm
	Tue, 26 Jan 2021 23:34:40 +0100
changeset 73194	c0d6d57a9a31
parent 66453	cc19f7ca2ed6
permissions	-rw-r--r--