equal
deleted
inserted
replaced
77 predicate. |
77 predicate. |
78 *} |
78 *} |
79 |
79 |
80 subsection {* Operators and lemmas for types isomorphic to tuples *} |
80 subsection {* Operators and lemmas for types isomorphic to tuples *} |
81 |
81 |
82 datatype ('a, 'b, 'c) tuple_isomorphism = |
82 datatype_new (dead 'a, dead 'b, dead 'c) tuple_isomorphism = |
83 Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a" |
83 Tuple_Isomorphism "'a \<Rightarrow> 'b \<times> 'c" "'b \<times> 'c \<Rightarrow> 'a" |
84 |
84 |
85 primrec |
85 primrec |
86 repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where |
86 repr :: "('a, 'b, 'c) tuple_isomorphism \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'c" where |
87 "repr (Tuple_Isomorphism r a) = r" |
87 "repr (Tuple_Isomorphism r a) = r" |