isabelle: src/HOL/ex/Case_Product.thy@9ac558ab0906 (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>
41828 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.
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
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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	20	text \<open>
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	21	The attribute honors preconditions
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	22	\<close>
41828 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
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	26	text \<open>
41828 d5b294734373 add example for case_product usage noschinl parents: diff changeset	27	Also, case names are generated based on the old names
61343 5b5656a63bd6 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	28	\<close>
41828 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	haftmann
	Sat, 11 Jun 2016 16:22:42 +0200
changeset 63290	9ac558ab0906
parent 61343	5b5656a63bd6
child 65563	e83c9e94e891
permissions	-rw-r--r--