fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
theory IMP_2
imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
begin
subsection {* IMP *}
text {*
In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
*}
type_synonym var = unit
type_synonym state = bool
datatype com =
Skip |
Ass bool |
Seq com com |
IF com com |
While com
inductive exec :: "com => state => state => bool" where
"exec Skip s s" |
"exec (Ass e) s e" |
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
"s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
"\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
"\<not> s ==> exec (While c) s s" |
"s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''"
lemma
"exec c s s' ==> exec (Seq c c) s s'"
quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
oops
end