Download HOL-TestGen: User Guide

lemma triangle_abscase4 [test"triangle2"]:"triangle 2 2 1"
by(auto simp: triangle_def)
lemma triangle_abscase5 [test"triangle2"]:"triangle 3 4 5"
by(auto simp: triangle_def)
lemma triangle_abscase6 [test"triangle2"]:"¬ triangle -1 1 2"
by(auto simp: triangle_def)
lemma triangle_abscase7 [test"triangle2"]:"¬ triangle 1 -1 2"
by(auto simp: triangle_def)
lemma triangle_abscase8 [test"triangle2"]:"¬ triangle 1 2 -1"
by(auto simp: triangle_def)
lemma triangle_abscase9 [test "triangle2"]: "¬ triangle -1 -1 -1"
by(auto simp: triangle_def)
lemma triangle_abscase10 [test "triangle2"]: "¬ triangle -1 1 -1"
by(auto simp: triangle_def)
lemma triangle_abscase11 [test "triangle2"]: "¬ triangle 1 -1 -1"
by(auto simp: triangle_def)
lemma triangle_abscase12 [test "triangle2"]: "¬ triangle -1 -1 1"
by(auto simp: triangle_def)
lemmas abs_cases = triangle_abscase1 triangle_abscase2 triangle_abscase3 triangle_abscase4
triangle_abscase5 triangle_abscase6 triangle_abscase7 triangle_abscase8
triangle_abscase9 triangle_abscase10 triangle_abscase11 triangle_abscase12
Just for demonstration purposes, we apply the abstract test data solver directly in the proof:
test spec "prog(x,y,z) = classify_triangle x y z"
apply(gen_test_cases "prog" simp add: classify_triangle_def)
apply(tactic "TestGen.ALLCASES(TestGen.SOLVE_ASMS @{context}
oops
(TestGen.auto_solver (thms"abs_cases")))
test spec "prog(x,y,z) = classify_triangle x y z"
apply(gen_test_cases "prog" simp add: classify_triangle_def)
store test thm "triangle2"
thm "triangle2.test_thm"
gen test data "triangle2"
The test data generation is started and implicitly uses the abstract test data assigned to the test
theorem triangle2. Again, we inspect the results:
prog
prog
prog
prog
prog
42
(1, 1, 1) = equilateral
(-1, -1, -1) = error
(2, 1, 2) = isosceles
(-1, 1, -1) = error
(1, 2, 2) = isosceles