isabelle: src/HOL/ex/Case_Product.thy@70b0362c784d (annotated)

41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	1	(* Title: HOL/ex/Case_Product.thy
d5b294734373 add example for case_product usage noschinl parents: diff changeset	2	Author: Lars Noschinski
d5b294734373 add example for case_product usage noschinl parents: diff changeset	3	Copyright 2011 TU Muenchen
d5b294734373 add example for case_product usage noschinl parents: diff changeset	4	*)
d5b294734373 add example for case_product usage noschinl parents: diff changeset	5
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 41828 diff changeset	6	section {* Examples for the 'case_product' attribute *}
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	7
d5b294734373 add example for case_product usage noschinl parents: diff changeset	8	theory Case_Product
d5b294734373 add example for case_product usage noschinl parents: diff changeset	9	imports Main
d5b294734373 add example for case_product usage noschinl parents: diff changeset	10	begin
d5b294734373 add example for case_product usage noschinl parents: diff changeset	11
d5b294734373 add example for case_product usage noschinl parents: diff changeset	12	text {*
d5b294734373 add example for case_product usage noschinl parents: diff changeset	13	The {@attribute case_product} attribute combines multiple case distinction
d5b294734373 add example for case_product usage noschinl parents: diff changeset	14	lemmas into a single case distinction lemma by building the product of all
d5b294734373 add example for case_product usage noschinl parents: diff changeset	15	these case distinctions.
d5b294734373 add example for case_product usage noschinl parents: diff changeset	16	*}
d5b294734373 add example for case_product usage noschinl parents: diff changeset	17
d5b294734373 add example for case_product usage noschinl parents: diff changeset	18	lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
d5b294734373 add example for case_product usage noschinl parents: diff changeset	19
d5b294734373 add example for case_product usage noschinl parents: diff changeset	20	text {*
d5b294734373 add example for case_product usage noschinl parents: diff changeset	21	The attribute honors preconditions
d5b294734373 add example for case_product usage noschinl parents: diff changeset	22	*}
d5b294734373 add example for case_product usage noschinl parents: diff changeset	23
d5b294734373 add example for case_product usage noschinl parents: diff changeset	24	lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
d5b294734373 add example for case_product usage noschinl parents: diff changeset	25
d5b294734373 add example for case_product usage noschinl parents: diff changeset	26	text {*
d5b294734373 add example for case_product usage noschinl parents: diff changeset	27	Also, case names are generated based on the old names
d5b294734373 add example for case_product usage noschinl parents: diff changeset	28	*}
d5b294734373 add example for case_product usage noschinl parents: diff changeset	29
d5b294734373 add example for case_product usage noschinl parents: diff changeset	30	end

author	wenzelm
	Sun, 07 Jun 2015 23:37:32 +0200
changeset 60383	70b0362c784d
parent 58889	5b7a9633cfa8
child 61343	5b5656a63bd6
permissions	-rw-r--r--