127 subsubsection {* Type definition *} |
127 subsubsection {* Type definition *} |
128 |
128 |
129 definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where |
129 definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where |
130 "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)" |
130 "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)" |
131 |
131 |
132 typedef (prod) ('a, 'b) "*" (infixr "*" 20) |
132 typedef ('a, 'b) prod (infixr "*" 20) |
133 = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}" |
133 = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}" |
134 proof |
134 proof |
135 fix a b show "Pair_Rep a b \<in> ?prod" |
135 fix a b show "Pair_Rep a b \<in> ?prod" |
136 by rule+ |
136 by rule+ |
137 qed |
137 qed |
138 |
138 |
139 type_notation (xsymbols) |
139 type_notation (xsymbols) |
140 "*" ("(_ \<times>/ _)" [21, 20] 20) |
140 "prod" ("(_ \<times>/ _)" [21, 20] 20) |
141 type_notation (HTML output) |
141 type_notation (HTML output) |
142 "*" ("(_ \<times>/ _)" [21, 20] 20) |
142 "prod" ("(_ \<times>/ _)" [21, 20] 20) |
143 |
143 |
144 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where |
144 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where |
145 "Pair a b = Abs_prod (Pair_Rep a b)" |
145 "Pair a b = Abs_prod (Pair_Rep a b)" |
146 |
146 |
147 rep_datatype (prod) Pair proof - |
147 rep_datatype Pair proof - |
148 fix P :: "'a \<times> 'b \<Rightarrow> bool" and p |
148 fix P :: "'a \<times> 'b \<Rightarrow> bool" and p |
149 assume "\<And>a b. P (Pair a b)" |
149 assume "\<And>a b. P (Pair a b)" |
150 then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) |
150 then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) |
151 next |
151 next |
152 fix a c :: 'a and b d :: 'b |
152 fix a c :: 'a and b d :: 'b |
273 (SML "!((_),/ (_))") |
273 (SML "!((_),/ (_))") |
274 (OCaml "!((_),/ (_))") |
274 (OCaml "!((_),/ (_))") |
275 (Haskell "!((_),/ (_))") |
275 (Haskell "!((_),/ (_))") |
276 (Scala "!((_),/ (_))") |
276 (Scala "!((_),/ (_))") |
277 |
277 |
278 code_instance * :: eq |
278 code_instance prod :: eq |
279 (Haskell -) |
279 (Haskell -) |
280 |
280 |
281 code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
281 code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
282 (Haskell infixl 4 "==") |
282 (Haskell infixl 4 "==") |
283 |
283 |
284 types_code |
284 types_code |
285 "*" ("(_ */ _)") |
285 "prod" ("(_ */ _)") |
286 attach (term_of) {* |
286 attach (term_of) {* |
287 fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; |
287 fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; |
288 *} |
288 *} |
289 attach (test) {* |
289 attach (test) {* |
290 fun gen_id_42 aG aT bG bT i = |
290 fun term_of_prod aG aT bG bT i = |
291 let |
291 let |
292 val (x, t) = aG i; |
292 val (x, t) = aG i; |
293 val (y, u) = bG i |
293 val (y, u) = bG i |
294 in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end; |
294 in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end; |
295 *} |
295 *} |
436 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" |
436 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" |
437 by (simp add: prod_case_unfold) |
437 by (simp add: prod_case_unfold) |
438 |
438 |
439 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q" |
439 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q" |
440 -- {* Prevents simplification of @{term c}: much faster *} |
440 -- {* Prevents simplification of @{term c}: much faster *} |
441 by (erule arg_cong) |
441 by (fact weak_case_cong) |
442 |
442 |
443 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" |
443 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" |
444 by (simp add: split_eta) |
444 by (simp add: split_eta) |
445 |
445 |
446 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
446 lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" |
687 *} |
687 *} |
688 |
688 |
689 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
689 lemmas prod_caseI = prod.cases [THEN iffD2, standard] |
690 |
690 |
691 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
691 lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" |
692 by auto |
692 by (fact splitI2) |
693 |
693 |
694 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" |
694 lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x" |
695 by (auto simp: split_tupled_all) |
695 by (fact splitI2') |
696 |
696 |
697 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
697 lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" |
698 by (induct p) auto |
698 by (fact splitE) |
699 |
699 |
700 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
700 lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" |
701 by (induct p) auto |
701 by (fact splitE') |
702 |
702 |
703 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] |
703 declare prod_caseI [intro!] |
704 declare prod_caseE' [elim!] prod_caseE [elim!] |
|
705 |
704 |
706 lemma prod_case_beta: |
705 lemma prod_case_beta: |
707 "prod_case f p = f (fst p) (snd p)" |
706 "prod_case f p = f (fst p) (snd p)" |
708 by (fact split_beta) |
707 by (fact split_beta) |
709 |
708 |
793 notation fcomp (infixl "o>" 60) |
792 notation fcomp (infixl "o>" 60) |
794 |
793 |
795 definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where |
794 definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where |
796 "f o\<rightarrow> g = (\<lambda>x. split g (f x))" |
795 "f o\<rightarrow> g = (\<lambda>x. split g (f x))" |
797 |
796 |
|
797 lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))" |
|
798 by (simp add: expand_fun_eq scomp_def split_def) |
|
799 |
798 lemma scomp_apply: "(f o\<rightarrow> g) x = split g (f x)" |
800 lemma scomp_apply: "(f o\<rightarrow> g) x = split g (f x)" |
799 by (simp add: scomp_def) |
801 by (simp add: scomp_unfold split_def) |
800 |
802 |
801 lemma Pair_scomp: "Pair x o\<rightarrow> f = f x" |
803 lemma Pair_scomp: "Pair x o\<rightarrow> f = f x" |
802 by (simp add: expand_fun_eq scomp_apply) |
804 by (simp add: expand_fun_eq scomp_apply) |
803 |
805 |
804 lemma scomp_Pair: "x o\<rightarrow> Pair = x" |
806 lemma scomp_Pair: "x o\<rightarrow> Pair = x" |
805 by (simp add: expand_fun_eq scomp_apply) |
807 by (simp add: expand_fun_eq scomp_apply) |
806 |
808 |
807 lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)" |
809 lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)" |
808 by (simp add: expand_fun_eq split_twice scomp_def) |
810 by (simp add: expand_fun_eq scomp_unfold) |
809 |
811 |
810 lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)" |
812 lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)" |
811 by (simp add: expand_fun_eq scomp_apply fcomp_def split_def) |
813 by (simp add: expand_fun_eq scomp_unfold fcomp_def) |
812 |
814 |
813 lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)" |
815 lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)" |
814 by (simp add: expand_fun_eq scomp_apply fcomp_apply) |
816 by (simp add: expand_fun_eq scomp_unfold fcomp_apply) |
815 |
817 |
816 code_const scomp |
818 code_const scomp |
817 (Eval infixl 3 "#->") |
819 (Eval infixl 3 "#->") |
818 |
820 |
819 no_notation fcomp (infixl "o>" 60) |
821 no_notation fcomp (infixl "o>" 60) |