src/HOL/ex/Case_Product.thy
changeset 41828 d5b294734373
child 58889 5b7a9633cfa8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Case_Product.thy	Wed Feb 23 11:23:26 2011 +0100
     1.3 @@ -0,0 +1,30 @@
     1.4 +(*  Title:      HOL/ex/Case_Product.thy
     1.5 +    Author:     Lars Noschinski
     1.6 +    Copyright   2011 TU Muenchen
     1.7 +*)
     1.8 +
     1.9 +header {* Examples for the 'case_product' attribute *}
    1.10 +
    1.11 +theory Case_Product
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +text {*
    1.16 +  The {@attribute case_product} attribute combines multiple case distinction
    1.17 +  lemmas into a single case distinction lemma by building the product of all
    1.18 +  these case distinctions.
    1.19 +*}
    1.20 +
    1.21 +lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
    1.22 +
    1.23 +text {*
    1.24 +  The attribute honors preconditions
    1.25 +*}
    1.26 +
    1.27 +lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
    1.28 +
    1.29 +text {*
    1.30 +  Also, case names are generated based on the old names
    1.31 +*}
    1.32 +
    1.33 +end