author  wenzelm 
Wed, 17 Oct 2001 20:24:03 +0200  
changeset 11820  015a82d4ee96 
parent 11777  b03c8a3fcc6d 
child 11838  02d75712061d 
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 

11777  5 
*) 
10213  6 

11777  7 
header {* Finite products (including unit) *} 
10213  8 

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

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

12 

11777  13 
subsection {* Products *} 
10213  14 

11777  15 
subsubsection {* Type definition *} 
10213  16 

17 
constdefs 

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

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

21 
global 

22 

23 
typedef (Prod) 

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

11032  25 
= "{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

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

27 
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

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

29 
qed 
10213  30 

31 
syntax (symbols) 

11493  32 
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) 
10213  33 
syntax (HTML output) 
11493  34 
"*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20) 
10213  35 

11777  36 
local 
10213  37 

11777  38 

39 
subsubsection {* Abstract constants and syntax *} 

40 

41 
global 

10213  42 

43 
consts 

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

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

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

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

47 
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

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

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

11777  51 
local 
10213  52 

11777  53 
text {* 
54 
Patterns  extends predefined type @{typ pttrn} used in 

55 
abstractions. 

56 
*} 

10213  57 

58 
nonterminals 

59 
tuple_args patterns 

60 

61 
syntax 

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

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

64 
"_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

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

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

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

68 
"@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

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

71 
translations 

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

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

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

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

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

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

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

79 

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

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

82 

83 
syntax (symbols) 

11493  84 
"@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10) 
85 
"@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80) 

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

86 

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

89 

11777  90 
subsubsection {* Definitions *} 
10213  91 

92 
defs 

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

93 
Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)" 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11425
diff
changeset

94 
fst_def: "fst p == THE a. EX b. p = (a, b)" 
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11425
diff
changeset

95 
snd_def: "snd p == THE b. EX a. p = (a, b)" 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

96 
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

97 
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

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

100 

11777  101 
subsection {* Unit *} 
10213  102 

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

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

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

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

107 
qed 
10213  108 

11602  109 
constdefs 
110 
Unity :: unit ("'(')") 

111 
"() == Abs_unit True" 

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

112 

11032  113 

11777  114 
subsection {* Lemmas and tool setup *} 
11032  115 

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

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

117 

11820
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

118 
lemma (*split_paired_all:*) "(!!x. PROP P x) == (!!a b. PROP P (a, b))" (* FIXME unused *) 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

119 
proof 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

120 
fix a b 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

121 
assume "!!x. PROP P x" 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

122 
thus "PROP P (a, b)" . 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

123 
next 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

124 
fix x 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

125 
assume "!!a b. PROP P (a, b)" 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

126 
hence "PROP P (fst x, snd x)" . 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

127 
thus "PROP P x" by simp 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

128 
qed 
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

129 

11493  130 
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" 
11777  131 
apply (rule_tac x = "(a, b)" in image_eqI) 
132 
apply auto 

133 
done 

134 

11493  135 

11032  136 
constdefs 
11425  137 
internal_split :: "('a => 'b => 'c) => 'a * 'b => 'c" 
11032  138 
"internal_split == split" 
139 

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

141 
by (simp only: internal_split_def split_conv) 

142 

143 
hide const internal_split 

144 

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

145 
use "Tools/split_rule.ML" 
11032  146 
setup SplitRule.setup 
10213  147 

148 
end 