equal
deleted
inserted
replaced
354 |
354 |
355 use "Tools/Quickcheck/narrowing_generators.ML" |
355 use "Tools/Quickcheck/narrowing_generators.ML" |
356 |
356 |
357 setup {* Narrowing_Generators.setup *} |
357 setup {* Narrowing_Generators.setup *} |
358 |
358 |
|
359 definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term" |
|
360 where |
|
361 "narrowing_dummy_partial_term_of = partial_term_of" |
|
362 |
|
363 definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons" |
|
364 where |
|
365 "narrowing_dummy_narrowing = narrowing" |
|
366 |
|
367 lemma [code]: |
|
368 "ensure_testable f = |
|
369 (let |
|
370 x = narrowing_dummy_narrowing :: code_int => bool cons; |
|
371 y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term; |
|
372 z = (conv :: _ => _ => unit) in f)" |
|
373 unfolding Let_def ensure_testable_def .. |
|
374 |
|
375 |
359 subsection {* Narrowing for integers *} |
376 subsection {* Narrowing for integers *} |
360 |
377 |
361 |
378 |
362 definition drawn_from :: "'a list => 'a cons" |
379 definition drawn_from :: "'a list => 'a cons" |
363 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)" |
380 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)" |