5 *) |
5 *) |
6 |
6 |
7 header {* Cartesian products *} |
7 header {* Cartesian products *} |
8 |
8 |
9 theory Product_Type |
9 theory Product_Type |
10 imports Typedef Fun |
10 imports Inductive |
11 uses ("Tools/split_rule.ML") |
11 uses |
|
12 ("Tools/split_rule.ML") |
|
13 ("Tools/inductive_set_package.ML") |
|
14 ("Tools/inductive_realizer.ML") |
|
15 ("Tools/datatype_realizer.ML") |
12 begin |
16 begin |
|
17 |
|
18 subsection {* @{typ bool} is a datatype *} |
|
19 |
|
20 rep_datatype bool |
|
21 distinct True_not_False False_not_True |
|
22 induction bool_induct |
|
23 |
|
24 declare case_split [cases type: bool] |
|
25 -- "prefer plain propositional version" |
|
26 |
13 |
27 |
14 subsection {* Unit *} |
28 subsection {* Unit *} |
15 |
29 |
16 typedef unit = "{True}" |
30 typedef unit = "{True}" |
17 proof |
31 proof |
18 show "True : ?unit" .. |
32 show "True : ?unit" .. |
19 qed |
33 qed |
20 |
34 |
21 constdefs |
35 definition |
22 Unity :: unit ("'(')") |
36 Unity :: unit ("'(')") |
23 "() == Abs_unit True" |
37 where |
|
38 "() = Abs_unit True" |
24 |
39 |
25 lemma unit_eq [noatp]: "u = ()" |
40 lemma unit_eq [noatp]: "u = ()" |
26 by (induct u) (simp add: unit_def Unity_def) |
41 by (induct u) (simp add: unit_def Unity_def) |
27 |
42 |
28 text {* |
43 text {* |
30 this rule directly --- it loops! |
45 this rule directly --- it loops! |
31 *} |
46 *} |
32 |
47 |
33 ML_setup {* |
48 ML_setup {* |
34 val unit_eq_proc = |
49 val unit_eq_proc = |
35 let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in |
50 let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in |
36 Simplifier.simproc (the_context ()) "unit_eq" ["x::unit"] |
51 Simplifier.simproc @{theory} "unit_eq" ["x::unit"] |
37 (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq) |
52 (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq) |
38 end; |
53 end; |
39 |
54 |
40 Addsimprocs [unit_eq_proc]; |
55 Addsimprocs [unit_eq_proc]; |
41 *} |
56 *} |
42 |
57 |
|
58 lemma unit_induct [noatp,induct type: unit]: "P () ==> P x" |
|
59 by simp |
|
60 |
|
61 rep_datatype unit |
|
62 induction unit_induct |
|
63 |
43 lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" |
64 lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" |
44 by simp |
65 by simp |
45 |
66 |
46 lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P" |
67 lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P" |
47 by (rule triv_forall_equality) |
68 by (rule triv_forall_equality) |
48 |
|
49 lemma unit_induct [noatp,induct type: unit]: "P () ==> P x" |
|
50 by simp |
|
51 |
69 |
52 text {* |
70 text {* |
53 This rewrite counters the effect of @{text unit_eq_proc} on @{term |
71 This rewrite counters the effect of @{text unit_eq_proc} on @{term |
54 [source] "%u::unit. f u"}, replacing it by @{term [source] |
72 [source] "%u::unit. f u"}, replacing it by @{term [source] |
55 f} rather than by @{term [source] "%u. f ()"}. |
73 f} rather than by @{term [source] "%u. f ()"}. |
341 by (simp add: curry_def) |
358 by (simp add: curry_def) |
342 |
359 |
343 lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" |
360 lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" |
344 by fast |
361 by fast |
345 |
362 |
|
363 rep_datatype prod |
|
364 inject Pair_eq |
|
365 induction prod_induct |
|
366 |
346 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" |
367 lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" |
347 by fast |
368 by fast |
348 |
369 |
349 lemma split_conv [simp, code func]: "split c (a, b) = c a b" |
370 lemma split_conv [simp, code func]: "split c (a, b) = c a b" |
350 by (simp add: split_def) |
371 by (simp add: split_def) |
761 |
782 |
762 hide const internal_split |
783 hide const internal_split |
763 |
784 |
764 use "Tools/split_rule.ML" |
785 use "Tools/split_rule.ML" |
765 setup SplitRule.setup |
786 setup SplitRule.setup |
|
787 |
|
788 |
|
789 |
|
790 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
|
791 |
|
792 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
|
793 by auto |
|
794 |
|
795 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" |
|
796 by (auto simp: split_tupled_all) |
|
797 |
|
798 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
|
799 by (induct p) auto |
|
800 |
|
801 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
|
802 by (induct p) auto |
|
803 |
|
804 lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" |
|
805 by (simp add: expand_fun_eq) |
|
806 |
|
807 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] |
|
808 declare prod_caseE' [elim!] prod_caseE [elim!] |
|
809 |
|
810 lemma prod_case_split [code post]: |
|
811 "prod_case = split" |
|
812 by (auto simp add: expand_fun_eq) |
|
813 |
|
814 lemmas [code inline] = prod_case_split [symmetric] |
|
815 |
|
816 |
|
817 subsection {* Further cases/induct rules for tuples *} |
|
818 |
|
819 lemma prod_cases3 [cases type]: |
|
820 obtains (fields) a b c where "y = (a, b, c)" |
|
821 by (cases y, case_tac b) blast |
|
822 |
|
823 lemma prod_induct3 [case_names fields, induct type]: |
|
824 "(!!a b c. P (a, b, c)) ==> P x" |
|
825 by (cases x) blast |
|
826 |
|
827 lemma prod_cases4 [cases type]: |
|
828 obtains (fields) a b c d where "y = (a, b, c, d)" |
|
829 by (cases y, case_tac c) blast |
|
830 |
|
831 lemma prod_induct4 [case_names fields, induct type]: |
|
832 "(!!a b c d. P (a, b, c, d)) ==> P x" |
|
833 by (cases x) blast |
|
834 |
|
835 lemma prod_cases5 [cases type]: |
|
836 obtains (fields) a b c d e where "y = (a, b, c, d, e)" |
|
837 by (cases y, case_tac d) blast |
|
838 |
|
839 lemma prod_induct5 [case_names fields, induct type]: |
|
840 "(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
841 by (cases x) blast |
|
842 |
|
843 lemma prod_cases6 [cases type]: |
|
844 obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" |
|
845 by (cases y, case_tac e) blast |
|
846 |
|
847 lemma prod_induct6 [case_names fields, induct type]: |
|
848 "(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
849 by (cases x) blast |
|
850 |
|
851 lemma prod_cases7 [cases type]: |
|
852 obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" |
|
853 by (cases y, case_tac f) blast |
|
854 |
|
855 lemma prod_induct7 [case_names fields, induct type]: |
|
856 "(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
857 by (cases x) blast |
766 |
858 |
767 |
859 |
768 subsection {* Further lemmas *} |
860 subsection {* Further lemmas *} |
769 |
861 |
770 lemma |
862 lemma |