equal
deleted
inserted
replaced
15 fixes Rep and Abs and pair and dest1 and dest2 |
15 fixes Rep and Abs and pair and dest1 and dest2 |
16 assumes "typedef": "type_definition Rep Abs UNIV" |
16 assumes "typedef": "type_definition Rep Abs UNIV" |
17 and pair: "pair == (\<lambda>a b. Abs (a, b))" |
17 and pair: "pair == (\<lambda>a b. Abs (a, b))" |
18 and dest1: "dest1 == (\<lambda>p. fst (Rep p))" |
18 and dest1: "dest1 == (\<lambda>p. fst (Rep p))" |
19 and dest2: "dest2 == (\<lambda>p. snd (Rep p))" |
19 and dest2: "dest2 == (\<lambda>p. snd (Rep p))" |
20 |
|
21 lemmas product_typeI = |
|
22 product_type.intro [OF product_type_axioms.intro] |
|
23 |
20 |
24 lemma (in product_type) |
21 lemma (in product_type) |
25 "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')" |
22 "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')" |
26 by (simp add: pair type_definition.Abs_inject [OF "typedef"]) |
23 by (simp add: pair type_definition.Abs_inject [OF "typedef"]) |
27 |
24 |