author  wenzelm 
Fri, 02 Feb 2001 22:18:10 +0100  
changeset 11032  83f723e86dac 
parent 11025  a70b796d9af8 
child 11425  4988fd27d6e6 
permissions  rwrr 
10213  1 
(* Title: HOL/Product_Type.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Ordered Pairs and the Cartesian product type. 

7 
The unit type. 

8 
*) 

9 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

10 
theory Product_Type = Fun 
11032  11 
files ("Product_Type_lemmas.ML") ("Tools/split_rule.ML"): 
10213  12 

13 

14 
(** products **) 

15 

16 
(* type definition *) 

17 

18 
constdefs 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

19 
Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" 
11032  20 
"Pair_Rep == (%a b. %x y. x=a & y=b)" 
10213  21 

22 
global 

23 

24 
typedef (Prod) 

25 
('a, 'b) "*" (infixr 20) 

11032  26 
= "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}" 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

27 
proof 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

28 
fix a b show "Pair_Rep a b : ?Prod" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

29 
by blast 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

30 
qed 
10213  31 

32 
syntax (symbols) 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

33 
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) 
10213  34 
syntax (HTML output) 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

35 
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) 
10213  36 

37 

38 
(* abstract constants and syntax *) 

39 

40 
consts 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

41 
fst :: "'a * 'b => 'a" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

42 
snd :: "'a * 'b => 'b" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

43 
split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

44 
prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

45 
Pair :: "['a, 'b] => 'a * 'b" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

46 
Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" 
10213  47 

48 

49 
(* patterns  extends predefined type "pttrn" used in abstractions *) 

50 

51 
nonterminals 

52 
tuple_args patterns 

53 

54 
syntax 

55 
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))") 

56 
"_tuple_arg" :: "'a => tuple_args" ("_") 

57 
"_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _") 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

58 
"_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

59 
"" :: "pttrn => patterns" ("_") 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

60 
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

61 
"@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

62 
"@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80) 
10213  63 

64 
translations 

65 
"(x, y)" == "Pair x y" 

66 
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" 

67 
"%(x,y,zs).b" == "split(%x (y,zs).b)" 

68 
"%(x,y).b" == "split(%x y. b)" 

69 
"_abs (Pair x y) t" => "%(x,y).t" 

70 
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...' 

71 
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) 

72 

73 
"SIGMA x:A. B" => "Sigma A (%x. B)" 

74 
"A <*> B" => "Sigma A (_K B)" 

75 

76 
syntax (symbols) 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

77 
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

78 
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

79 

11032  80 
print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))] *} 
10213  81 

82 

83 
(* definitions *) 

84 

85 
local 

86 

87 
defs 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

88 
Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" 
11032  89 
fst_def: "fst p == SOME a. EX b. p = (a, b)" 
90 
snd_def: "snd p == SOME b. EX a. p = (a, b)" 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

91 
split_def: "split == (%c p. c (fst p) (snd p))" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

92 
prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

93 
Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}" 
10213  94 

95 

96 

97 
(** unit **) 

98 

99 
global 

100 

11032  101 
typedef unit = "{True}" 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

102 
proof 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

103 
show "True : ?unit" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

104 
by blast 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

105 
qed 
10213  106 

107 
consts 

108 
"()" :: unit ("'(')") 

109 

110 
local 

111 

112 
defs 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

113 
Unity_def: "() == Abs_unit True" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

114 

11032  115 

116 

117 
(** lemmas and tool setup **) 

118 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

119 
use "Product_Type_lemmas.ML" 
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

120 

11032  121 
constdefs 
122 
internal_split :: "('a \<Rightarrow> 'b => 'c) => 'a * 'b => 'c" 

123 
"internal_split == split" 

124 

125 
lemma internal_split_conv: "internal_split c (a, b) = c a b" 

126 
by (simp only: internal_split_def split_conv) 

127 

128 
hide const internal_split 

129 

11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

130 
use "Tools/split_rule.ML" 
11032  131 
setup SplitRule.setup 
10213  132 

133 
end 