equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Case_Product.thy |
1 (* Title: HOL/ex/Case_Product.thy |
2 Author: Lars Noschinski |
2 Author: Lars Noschinski |
3 Copyright 2011 TU Muenchen |
3 Copyright 2011 TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 section {* Examples for the 'case_product' attribute *} |
6 section \<open>Examples for the 'case_product' attribute\<close> |
7 |
7 |
8 theory Case_Product |
8 theory Case_Product |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text \<open> |
13 The {@attribute case_product} attribute combines multiple case distinction |
13 The {@attribute case_product} attribute combines multiple case distinction |
14 lemmas into a single case distinction lemma by building the product of all |
14 lemmas into a single case distinction lemma by building the product of all |
15 these case distinctions. |
15 these case distinctions. |
16 *} |
16 \<close> |
17 |
17 |
18 lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust] |
18 lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust] |
19 |
19 |
20 text {* |
20 text \<open> |
21 The attribute honors preconditions |
21 The attribute honors preconditions |
22 *} |
22 \<close> |
23 |
23 |
24 lemmas trancl_acc_cases= trancl.cases[case_product acc.cases] |
24 lemmas trancl_acc_cases= trancl.cases[case_product acc.cases] |
25 |
25 |
26 text {* |
26 text \<open> |
27 Also, case names are generated based on the old names |
27 Also, case names are generated based on the old names |
28 *} |
28 \<close> |
29 |
29 |
30 end |
30 end |