isabelle: src/HOL/ex/Case_Product.thy@5fca489a6ac1 (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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	6	section \<open>Examples for the 'case_product' attribute\<close>
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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	12	text \<open>
65563 e83c9e94e891 actually use theory; wenzelm parents: 61343 diff changeset	13	The @{attribute case_product} attribute combines multiple case distinction
41828 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.
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	16	\<close>
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	17
65563 e83c9e94e891 actually use theory; wenzelm parents: 61343 diff changeset	18	lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust]
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	19
65563 e83c9e94e891 actually use theory; wenzelm parents: 61343 diff changeset	20	text \<open>The attribute honours preconditions.\<close>
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	21
65563 e83c9e94e891 actually use theory; wenzelm parents: 61343 diff changeset	22	lemmas trancl_acc_cases = trancl.cases [case_product acc.cases]
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	23
65563 e83c9e94e891 actually use theory; wenzelm parents: 61343 diff changeset	24	text \<open>Also, case names are generated based on the old names.\<close>
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	25
d5b294734373 add example for case_product usage noschinl parents: diff changeset	26	end

author	wenzelm
	Sat, 13 Nov 2021 17:26:35 +0100
changeset 74779	5fca489a6ac1
parent 65563	e83c9e94e891
permissions	-rw-r--r--