author  haftmann 
Wed, 26 May 2010 16:05:25 +0200  
changeset 37136  e0c9d3e49e15 
parent 36664  6302f9ad7047 
child 37166  e8400e31528a 
permissions  rwrr 
10213  1 
(* Title: HOL/Product_Type.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1992 University of Cambridge 

11777  4 
*) 
10213  5 

11838  6 
header {* Cartesian products *} 
10213  7 

15131  8 
theory Product_Type 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33638
diff
changeset

9 
imports Typedef Inductive Fun 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

10 
uses 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

11 
("Tools/split_rule.ML") 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31667
diff
changeset

12 
("Tools/inductive_set.ML") 
15131  13 
begin 
11838  14 

24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

15 
subsection {* @{typ bool} is a datatype *} 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

16 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

17 
rep_datatype True False by (auto intro: bool_induct) 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

18 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

19 
declare case_split [cases type: bool] 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

20 
 "prefer plain propositional version" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

21 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

22 
lemma 
28562  23 
shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P" 
24 
and [code]: "eq_class.eq True P \<longleftrightarrow> P" 

25 
and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 

26 
and [code]: "eq_class.eq P True \<longleftrightarrow> P" 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

27 
and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True" 
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

28 
by (simp_all add: eq) 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25511
diff
changeset

29 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

30 
code_const "eq_class.eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool" 
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25511
diff
changeset

31 
(Haskell infixl 4 "==") 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25511
diff
changeset

32 

d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25511
diff
changeset

33 
code_instance bool :: eq 
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25511
diff
changeset

34 
(Haskell ) 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

35 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

36 

11838  37 
subsection {* Unit *} 
38 

39 
typedef unit = "{True}" 

40 
proof 

20588  41 
show "True : ?unit" .. 
11838  42 
qed 
43 

24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

44 
definition 
11838  45 
Unity :: unit ("'(')") 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

46 
where 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

47 
"() = Abs_unit True" 
11838  48 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

49 
lemma unit_eq [no_atp]: "u = ()" 
11838  50 
by (induct u) (simp add: unit_def Unity_def) 
51 

52 
text {* 

53 
Simplification procedure for @{thm [source] unit_eq}. Cannot use 

54 
this rule directly  it loops! 

55 
*} 

56 

26480  57 
ML {* 
13462  58 
val unit_eq_proc = 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

59 
let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

60 
Simplifier.simproc @{theory} "unit_eq" ["x::unit"] 
15531  61 
(fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq) 
13462  62 
end; 
11838  63 

64 
Addsimprocs [unit_eq_proc]; 

65 
*} 

66 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

67 
rep_datatype "()" by simp 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

68 

11838  69 
lemma unit_all_eq1: "(!!x::unit. PROP P x) == PROP P ()" 
70 
by simp 

71 

72 
lemma unit_all_eq2: "(!!x::unit. PROP P) == PROP P" 

73 
by (rule triv_forall_equality) 

74 

75 
text {* 

76 
This rewrite counters the effect of @{text unit_eq_proc} on @{term 

77 
[source] "%u::unit. f u"}, replacing it by @{term [source] 

78 
f} rather than by @{term [source] "%u. f ()"}. 

79 
*} 

80 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

81 
lemma unit_abs_eta_conv [simp,no_atp]: "(%u::unit. f ()) = f" 
11838  82 
by (rule ext) simp 
10213  83 

30924  84 
instantiation unit :: default 
85 
begin 

86 

87 
definition "default = ()" 

88 

89 
instance .. 

90 

91 
end 

10213  92 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

93 
text {* code generator setup *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

94 

28562  95 
lemma [code]: 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

96 
"eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+ 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

97 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

98 
code_type unit 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

99 
(SML "unit") 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

100 
(OCaml "unit") 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

101 
(Haskell "()") 
34886  102 
(Scala "Unit") 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

103 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

104 
code_instance unit :: eq 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

105 
(Haskell ) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

106 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

107 
code_const "eq_class.eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

108 
(Haskell infixl 4 "==") 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

109 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

110 
code_const Unity 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

111 
(SML "()") 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

112 
(OCaml "()") 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

113 
(Haskell "()") 
34886  114 
(Scala "()") 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

115 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

116 
code_reserved SML 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

117 
unit 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

118 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

119 
code_reserved OCaml 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

120 
unit 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

121 

34886  122 
code_reserved Scala 
123 
Unit 

124 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

125 

11838  126 
subsection {* Pairs *} 
10213  127 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

128 
subsubsection {* Product type, basic operations and concrete syntax *} 
10213  129 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

130 
definition 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

131 
Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

132 
where 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

133 
"Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)" 
10213  134 

135 
global 

136 

137 
typedef (Prod) 

22838  138 
('a, 'b) "*" (infixr "*" 20) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

139 
= "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}" 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

140 
proof 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

141 
fix a b show "Pair_Rep a b \<in> ?Prod" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

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

143 
qed 
10213  144 

35427  145 
type_notation (xsymbols) 
146 
"*" ("(_ \<times>/ _)" [21, 20] 20) 

147 
type_notation (HTML output) 

148 
"*" ("(_ \<times>/ _)" [21, 20] 20) 

10213  149 

150 
consts 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

151 
Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

152 
fst :: "'a \<times> 'b \<Rightarrow> 'a" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

153 
snd :: "'a \<times> 'b \<Rightarrow> 'b" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

154 
split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

155 
curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" 
10213  156 

11777  157 
local 
10213  158 

19535  159 
defs 
160 
Pair_def: "Pair a b == Abs_Prod (Pair_Rep a b)" 

161 
fst_def: "fst p == THE a. EX b. p = Pair a b" 

162 
snd_def: "snd p == THE b. EX a. p = Pair a b" 

24162
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
23247
diff
changeset

163 
split_def: "split == (%c p. c (fst p) (snd p))" 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
23247
diff
changeset

164 
curry_def: "curry == (%c x y. c (Pair x y))" 
19535  165 

11777  166 
text {* 
167 
Patterns  extends predefined type @{typ pttrn} used in 

168 
abstractions. 

169 
*} 

10213  170 

171 
nonterminals 

172 
tuple_args patterns 

173 

174 
syntax 

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

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

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

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

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

180 
"_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") 
10213  181 

182 
translations 

35115  183 
"(x, y)" == "CONST Pair x y" 
10213  184 
"_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))" 
35115  185 
"%(x, y, zs). b" == "CONST split (%x (y, zs). b)" 
186 
"%(x, y). b" == "CONST split (%x y. b)" 

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

10213  188 
(* The last rule accommodates tuples in `case C ... (x,y) ... => ...' 
189 
The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) 

190 

35115  191 
(*reconstruct pattern from (nested) splits, avoiding etacontraction of body; 
192 
works best with enclosing "let", if "let" does not avoid etacontraction*) 

14359  193 
print_translation {* 
35115  194 
let 
195 
fun split_tr' [Abs (x, T, t as (Abs abs))] = 

196 
(* split (%x y. t) => %(x,y) t *) 

197 
let 

198 
val (y, t') = atomic_abs_tr' abs; 

199 
val (x', t'') = atomic_abs_tr' (x, T, t'); 

200 
in 

201 
Syntax.const @{syntax_const "_abs"} $ 

202 
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 

203 
end 

204 
 split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] = 

205 
(* split (%x. (split (%y z. t))) => %(x,y,z). t *) 

206 
let 

207 
val Const (@{syntax_const "_abs"}, _) $ 

208 
(Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t]; 

209 
val (x', t'') = atomic_abs_tr' (x, T, t'); 

210 
in 

211 
Syntax.const @{syntax_const "_abs"} $ 

212 
(Syntax.const @{syntax_const "_pattern"} $ x' $ 

213 
(Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t'' 

214 
end 

215 
 split_tr' [Const (@{const_syntax split}, _) $ t] = 

216 
(* split (split (%x y z. t)) => %((x, y), z). t *) 

217 
split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *) 

218 
 split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = 

219 
(* split (%pttrn z. t) => %(pttrn,z). t *) 

220 
let val (z, t) = atomic_abs_tr' abs in 

221 
Syntax.const @{syntax_const "_abs"} $ 

222 
(Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t 

223 
end 

224 
 split_tr' _ = raise Match; 

225 
in [(@{const_syntax split}, split_tr')] end 

14359  226 
*} 
227 

15422
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

228 
(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

229 
typed_print_translation {* 
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

230 
let 
35115  231 
fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match 
232 
 split_guess_names_tr' _ T [Abs (x, xT, t)] = 

15422
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

233 
(case (head_of t) of 
35115  234 
Const (@{const_syntax split}, _) => raise Match 
235 
 _ => 

236 
let 

237 
val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; 

238 
val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); 

239 
val (x', t'') = atomic_abs_tr' (x, xT, t'); 

240 
in 

241 
Syntax.const @{syntax_const "_abs"} $ 

242 
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 

243 
end) 

15422
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

244 
 split_guess_names_tr' _ T [t] = 
35115  245 
(case head_of t of 
246 
Const (@{const_syntax split}, _) => raise Match 

247 
 _ => 

248 
let 

249 
val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; 

250 
val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); 

251 
val (x', t'') = atomic_abs_tr' ("x", xT, t'); 

252 
in 

253 
Syntax.const @{syntax_const "_abs"} $ 

254 
(Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 

255 
end) 

15422
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

256 
 split_guess_names_tr' _ _ _ = raise Match; 
35115  257 
in [(@{const_syntax split}, split_guess_names_tr')] end 
15422
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

258 
*} 
cbdddc0efadf
added print translation for split: split f > %(x,y). f x y
schirmer
parents:
15404
diff
changeset

259 

10213  260 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

261 
text {* Towards a datatype declaration *} 
11838  262 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

263 
lemma surj_pair [simp]: "EX x y. p = (x, y)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

264 
apply (unfold Pair_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

265 
apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

266 
apply (erule exE, erule exE, rule exI, rule exI) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

267 
apply (rule Rep_Prod_inverse [symmetric, THEN trans]) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

268 
apply (erule arg_cong) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

269 
done 
11838  270 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

271 
lemma PairE [cases type: *]: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

272 
obtains x y where "p = (x, y)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

273 
using surj_pair [of p] by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

274 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

275 
lemma ProdI: "Pair_Rep a b \<in> Prod" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

276 
unfolding Prod_def by rule+ 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

277 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

278 
lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' \<Longrightarrow> a = a' \<and> b = b'" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

279 
unfolding Pair_Rep_def by (drule fun_cong, drule fun_cong) blast 
10213  280 

11838  281 
lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" 
282 
apply (rule inj_on_inverseI) 

283 
apply (erule Abs_Prod_inverse) 

284 
done 

285 

286 
lemma Pair_inject: 

18372  287 
assumes "(a, b) = (a', b')" 
288 
and "a = a' ==> b = b' ==> R" 

289 
shows R 

290 
apply (insert prems [unfolded Pair_def]) 

291 
apply (rule inj_on_Abs_Prod [THEN inj_onD, THEN Pair_Rep_inject, THEN conjE]) 

292 
apply (assumption  rule ProdI)+ 

293 
done 

10213  294 

27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

295 
rep_datatype (prod) Pair 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

296 
proof  
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

297 
fix P p 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

298 
assume "\<And>x y. P (x, y)" 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

299 
then show "P p" by (cases p) simp 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

300 
qed (auto elim: Pair_inject) 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

301 

791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26975
diff
changeset

302 
lemmas Pair_eq = prod.inject 
11838  303 

22886  304 
lemma fst_conv [simp, code]: "fst (a, b) = a" 
19535  305 
unfolding fst_def by blast 
11838  306 

22886  307 
lemma snd_conv [simp, code]: "snd (a, b) = b" 
19535  308 
unfolding snd_def by blast 
11025
a70b796d9af8
converted to Isar therory, adding attributes complete_split and split_format
oheimb
parents:
10289
diff
changeset

309 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

310 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

311 
subsubsection {* Basic rules and proof tools *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

312 

11838  313 
lemma fst_eqD: "fst (x, y) = a ==> x = a" 
314 
by simp 

315 

316 
lemma snd_eqD: "snd (x, y) = a ==> y = a" 

317 
by simp 

318 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

319 
lemma pair_collapse [simp]: "(fst p, snd p) = p" 
11838  320 
by (cases p) simp 
321 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

322 
lemmas surjective_pairing = pair_collapse [symmetric] 
11838  323 

324 
lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" 

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

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

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

327 
assume "!!x. PROP P x" 
19535  328 
then show "PROP P (a, b)" . 
11820
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

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

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

331 
assume "!!a b. PROP P (a, b)" 
19535  332 
from `PROP P (fst x, snd x)` show "PROP P x" by simp 
11820
015a82d4ee96
proper proof of split_paired_all (presently unused);
wenzelm
parents:
11777
diff
changeset

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

334 

11838  335 
text {* 
336 
The rule @{thm [source] split_paired_all} does not work with the 

337 
Simplifier because it also affects premises in congrence rules, 

338 
where this can lead to premises of the form @{text "!!a b. ... = 

339 
?P(a, b)"} which cannot be solved by reflexivity. 

340 
*} 

341 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

342 
lemmas split_tupled_all = split_paired_all unit_all_eq2 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

343 

26480  344 
ML {* 
11838  345 
(* replace parameters of product type by individual component parameters *) 
346 
val safe_full_simp_tac = generic_simp_tac true (true, false, false); 

347 
local (* filtering with exists_paired_all is an essential optimization *) 

16121  348 
fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = 
11838  349 
can HOLogic.dest_prodT T orelse exists_paired_all t 
350 
 exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u 

351 
 exists_paired_all (Abs (_, _, t)) = exists_paired_all t 

352 
 exists_paired_all _ = false; 

353 
val ss = HOL_basic_ss 

26340  354 
addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] 
11838  355 
addsimprocs [unit_eq_proc]; 
356 
in 

357 
val split_all_tac = SUBGOAL (fn (t, i) => 

358 
if exists_paired_all t then safe_full_simp_tac ss i else no_tac); 

359 
val unsafe_split_all_tac = SUBGOAL (fn (t, i) => 

360 
if exists_paired_all t then full_simp_tac ss i else no_tac); 

361 
fun split_all th = 

26340  362 
if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th; 
11838  363 
end; 
26340  364 
*} 
11838  365 

26340  366 
declaration {* fn _ => 
367 
Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac)) 

16121  368 
*} 
11838  369 

370 
lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" 

371 
 {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} 

372 
by fast 

373 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

374 
lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

375 
by fast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

376 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

377 
lemma Pair_fst_snd_eq: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

378 
by (cases s, cases t) simp 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

379 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

380 
lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

381 
by (simp add: Pair_fst_snd_eq) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

382 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

383 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

384 
subsubsection {* @{text split} and @{text curry} *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

385 

28562  386 
lemma split_conv [simp, code]: "split f (a, b) = f a b" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

387 
by (simp add: split_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

388 

28562  389 
lemma curry_conv [simp, code]: "curry f a b = f (a, b)" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

390 
by (simp add: curry_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

391 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

392 
lemmas split = split_conv  {* for backwards compatibility *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

393 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

394 
lemma splitI: "f a b \<Longrightarrow> split f (a, b)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

395 
by (rule split_conv [THEN iffD2]) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

396 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

397 
lemma splitD: "split f (a, b) \<Longrightarrow> f a b" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

398 
by (rule split_conv [THEN iffD1]) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

399 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

400 
lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

401 
by (simp add: curry_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

402 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

403 
lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

404 
by (simp add: curry_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

405 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

406 
lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

407 
by (simp add: curry_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

408 

14189  409 
lemma curry_split [simp]: "curry (split f) = f" 
410 
by (simp add: curry_def split_def) 

411 

412 
lemma split_curry [simp]: "split (curry f) = f" 

413 
by (simp add: curry_def split_def) 

414 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

415 
lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

416 
by (simp add: split_def id_def) 
11838  417 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

418 
lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f" 
36664
6302f9ad7047
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
krauss
parents:
36622
diff
changeset

419 
 {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

420 
by (rule ext) auto 
11838  421 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

422 
lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

423 
by (cases x) simp 
11838  424 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

425 
lemma split_twice: "split f (split g p) = split (\<lambda>x y. split f (g x y)) p" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

426 
unfolding split_def .. 
11838  427 

428 
lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" 

429 
 {* Can't be added to simpset: loops! *} 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

430 
by (simp add: split_eta) 
11838  431 

432 
lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" 

433 
by (simp add: split_def) 

434 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

435 
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q" 
11838  436 
 {* Prevents simplification of @{term c}: much faster *} 
437 
by (erule arg_cong) 

438 

439 
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" 

440 
by (simp add: split_eta) 

441 

442 
text {* 

443 
Simplification procedure for @{thm [source] cond_split_eta}. Using 

444 
@{thm [source] split_eta} as a rewrite rule is not general enough, 

445 
and using @{thm [source] cond_split_eta} directly would render some 

446 
existing proofs very inefficient; similarly for @{text 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

447 
split_beta}. 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

448 
*} 
11838  449 

26480  450 
ML {* 
11838  451 
local 
35364  452 
val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta}; 
453 
fun Pair_pat k 0 (Bound m) = (m = k) 

454 
 Pair_pat k i (Const (@{const_name Pair}, _) $ Bound m $ t) = 

455 
i > 0 andalso m = k + i andalso Pair_pat k (i  1) t 

456 
 Pair_pat _ _ _ = false; 

457 
fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t 

458 
 no_args k i (t $ u) = no_args k i t andalso no_args k i u 

459 
 no_args k i (Bound m) = m < k orelse m > k + i 

460 
 no_args _ _ _ = true; 

461 
fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE 

462 
 split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t 

463 
 split_pat tp i _ = NONE; 

20044
92cc2f4c7335
simprocs: no theory argument  use simpset context instead;
wenzelm
parents:
19656
diff
changeset

464 
fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] [] 
35364  465 
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) 
18328  466 
(K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1))); 
11838  467 

35364  468 
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t 
469 
 beta_term_pat k i (t $ u) = 

470 
Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u) 

471 
 beta_term_pat k i t = no_args k i t; 

472 
fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg 

473 
 eta_term_pat _ _ _ = false; 

11838  474 
fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) 
35364  475 
 subst arg k i (t $ u) = 
476 
if Pair_pat k i (t $ u) then incr_boundvars k arg 

477 
else (subst arg k i t $ subst arg k i u) 

478 
 subst arg k i t = t; 

479 
fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) = 

11838  480 
(case split_pat beta_term_pat 1 t of 
35364  481 
SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f)) 
15531  482 
 NONE => NONE) 
35364  483 
 beta_proc _ _ = NONE; 
484 
fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) = 

11838  485 
(case split_pat eta_term_pat 1 t of 
35364  486 
SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end)) 
15531  487 
 NONE => NONE) 
35364  488 
 eta_proc _ _ = NONE; 
11838  489 
in 
32010  490 
val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc); 
491 
val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc); 

11838  492 
end; 
493 

494 
Addsimprocs [split_beta_proc, split_eta_proc]; 

495 
*} 

496 

26798
a9134a089106
split_beta is now declared as monotonicity rule, to allow bounded
berghofe
parents:
26588
diff
changeset

497 
lemma split_beta [mono]: "(%(x, y). P x y) z = P (fst z) (snd z)" 
11838  498 
by (subst surjective_pairing, rule split_conv) 
499 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

500 
lemma split_split [no_atp]: "R(split c p) = (ALL x y. p = (x, y) > R(c x y))" 
11838  501 
 {* For use with @{text split} and the Simplifier. *} 
15481  502 
by (insert surj_pair [of p], clarify, simp) 
11838  503 

504 
text {* 

505 
@{thm [source] split_split} could be declared as @{text "[split]"} 

506 
done after the Splitter has been speeded up significantly; 

507 
precompute the constants involved and don't do anything unless the 

508 
current goal contains one of those constants. 

509 
*} 

510 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

511 
lemma split_split_asm [no_atp]: "R (split c p) = (~(EX x y. p = (x, y) & (~R (c x y))))" 
14208  512 
by (subst split_split, simp) 
11838  513 

514 

515 
text {* 

516 
\medskip @{term split} used as a logical connective or set former. 

517 

518 
\medskip These rules are for use with @{text blast}; could instead 

519 
call @{text simp} using @{thm [source] split} as rewrite. *} 

520 

521 
lemma splitI2: "!!p. [ !!a b. p = (a, b) ==> c a b ] ==> split c p" 

522 
apply (simp only: split_tupled_all) 

523 
apply (simp (no_asm_simp)) 

524 
done 

525 

526 
lemma splitI2': "!!p. [ !!a b. (a, b) = p ==> c a b x ] ==> split c p x" 

527 
apply (simp only: split_tupled_all) 

528 
apply (simp (no_asm_simp)) 

529 
done 

530 

531 
lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" 

532 
by (induct p) (auto simp add: split_def) 

533 

534 
lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" 

535 
by (induct p) (auto simp add: split_def) 

536 

537 
lemma splitE2: 

538 
"[ Q (split P z); !!x y. [z = (x, y); Q (P x y)] ==> R ] ==> R" 

539 
proof  

540 
assume q: "Q (split P z)" 

541 
assume r: "!!x y. [z = (x, y); Q (P x y)] ==> R" 

542 
show R 

543 
apply (rule r surjective_pairing)+ 

544 
apply (rule split_beta [THEN subst], rule q) 

545 
done 

546 
qed 

547 

548 
lemma splitD': "split R (a,b) c ==> R a b c" 

549 
by simp 

550 

551 
lemma mem_splitI: "z: c a b ==> z: split c (a, b)" 

552 
by simp 

553 

554 
lemma mem_splitI2: "!!p. [ !!a b. p = (a, b) ==> z: c a b ] ==> z: split c p" 

14208  555 
by (simp only: split_tupled_all, simp) 
11838  556 

18372  557 
lemma mem_splitE: 
558 
assumes major: "z: split c p" 

559 
and cases: "!!x y. [ p = (x,y); z: c x y ] ==> Q" 

560 
shows Q 

561 
by (rule major [unfolded split_def] cases surjective_pairing)+ 

11838  562 

563 
declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] 

564 
declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] 

565 

26340  566 
ML {* 
11838  567 
local (* filtering with exists_p_split is an essential optimization *) 
35364  568 
fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true 
11838  569 
 exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u 
570 
 exists_p_split (Abs (_, _, t)) = exists_p_split t 

571 
 exists_p_split _ = false; 

35364  572 
val ss = HOL_basic_ss addsimps @{thms split_conv}; 
11838  573 
in 
574 
val split_conv_tac = SUBGOAL (fn (t, i) => 

575 
if exists_p_split t then safe_full_simp_tac ss i else no_tac); 

576 
end; 

26340  577 
*} 
578 

11838  579 
(* This prevents applications of splitE for already splitted arguments leading 
580 
to quite timeconsuming computations (in particular for nested tuples) *) 

26340  581 
declaration {* fn _ => 
582 
Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac)) 

16121  583 
*} 
11838  584 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

585 
lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" 
18372  586 
by (rule ext) fast 
11838  587 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

588 
lemma split_eta_SetCompr2 [simp,no_atp]: "(%u. EX x y. u = (x, y) & P x y) = split P" 
18372  589 
by (rule ext) fast 
11838  590 

591 
lemma split_part [simp]: "(%(a,b). P & Q a b) = (%ab. P & split Q ab)" 

592 
 {* Allows simplifications of nested splits in case of independent predicates. *} 

18372  593 
by (rule ext) blast 
11838  594 

14337
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

595 
(* Do NOT make this a simp rule as it 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

596 
a) only helps in special situations 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

597 
b) can lead to nontermination in the presence of split_def 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

598 
*) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

599 
lemma split_comp_eq: 
20415  600 
fixes f :: "'a => 'b => 'c" and g :: "'d => 'a" 
601 
shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" 

18372  602 
by (rule ext) auto 
14101  603 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

604 
lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

605 
apply (rule_tac x = "(a, b)" in image_eqI) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

606 
apply auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

607 
done 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

608 

11838  609 
lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)" 
610 
by blast 

611 

612 
(* 

613 
the following would be slightly more general, 

614 
but cannot be used as rewrite rule: 

615 
### Cannot add premise as rewrite rule because it contains (type) unknowns: 

616 
### ?y = .x 

617 
Goal "[ P y; !!x. P x ==> x = y ] ==> (@(x',y). x = x' & P y) = (x,y)" 

14208  618 
by (rtac some_equality 1) 
619 
by ( Simp_tac 1) 

620 
by (split_all_tac 1) 

621 
by (Asm_full_simp_tac 1) 

11838  622 
qed "The_split_eq"; 
623 
*) 

624 

625 
text {* 

626 
Setup of internal @{text split_rule}. 

627 
*} 

628 

25511  629 
definition 
630 
internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" 

631 
where 

11032  632 
"internal_split == split" 
633 

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

635 
by (simp only: internal_split_def split_conv) 

636 

35364  637 
use "Tools/split_rule.ML" 
35365  638 
setup Split_Rule.setup 
35364  639 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35831
diff
changeset

640 
hide_const internal_split 
11032  641 

10213  642 

24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

643 
lemmas prod_caseI = prod.cases [THEN iffD2, standard] 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

644 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

645 
lemma prod_caseI2: "!!p. [ !!a b. p = (a, b) ==> c a b ] ==> prod_case c p" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

646 
by auto 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

647 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

648 
lemma prod_caseI2': "!!p. [ !!a b. (a, b) = p ==> c a b x ] ==> prod_case c p x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

649 
by (auto simp: split_tupled_all) 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

650 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

651 
lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

652 
by (induct p) auto 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

653 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

654 
lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

655 
by (induct p) auto 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

656 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

657 
lemma prod_case_unfold: "prod_case = (%c p. c (fst p) (snd p))" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

658 
by (simp add: expand_fun_eq) 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

659 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

660 
declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!] 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

661 
declare prod_caseE' [elim!] prod_caseE [elim!] 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

662 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

663 
lemma prod_case_split: 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

664 
"prod_case = split" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

665 
by (auto simp add: expand_fun_eq) 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

666 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
25885
diff
changeset

667 
lemma prod_case_beta: 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
25885
diff
changeset

668 
"prod_case f p = f (fst p) (snd p)" 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
25885
diff
changeset

669 
unfolding prod_case_split split_beta .. 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
25885
diff
changeset

670 

24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

671 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

672 
subsection {* Further cases/induct rules for tuples *} 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

673 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

674 
lemma prod_cases3 [cases type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

675 
obtains (fields) a b c where "y = (a, b, c)" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

676 
by (cases y, case_tac b) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

677 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

678 
lemma prod_induct3 [case_names fields, induct type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

679 
"(!!a b c. P (a, b, c)) ==> P x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

680 
by (cases x) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

681 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

682 
lemma prod_cases4 [cases type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

683 
obtains (fields) a b c d where "y = (a, b, c, d)" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

684 
by (cases y, case_tac c) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

685 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

686 
lemma prod_induct4 [case_names fields, induct type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

687 
"(!!a b c d. P (a, b, c, d)) ==> P x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

688 
by (cases x) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

689 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

690 
lemma prod_cases5 [cases type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

691 
obtains (fields) a b c d e where "y = (a, b, c, d, e)" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

692 
by (cases y, case_tac d) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

693 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

694 
lemma prod_induct5 [case_names fields, induct type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

695 
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

696 
by (cases x) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

697 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

698 
lemma prod_cases6 [cases type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

699 
obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

700 
by (cases y, case_tac e) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

701 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

702 
lemma prod_induct6 [case_names fields, induct type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

703 
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

704 
by (cases x) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

705 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

706 
lemma prod_cases7 [cases type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

707 
obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

708 
by (cases y, case_tac f) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

709 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

710 
lemma prod_induct7 [case_names fields, induct type]: 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

711 
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

712 
by (cases x) blast 
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

713 

c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

714 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

715 
subsubsection {* Derived operations *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

716 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

717 
text {* 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

718 
The compositionuncurry combinator. 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

719 
*} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

720 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

721 
notation fcomp (infixl "o>" 60) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

722 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

723 
definition 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

724 
scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

725 
where 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

726 
"f o\<rightarrow> g = (\<lambda>x. split g (f x))" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

727 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

728 
lemma scomp_apply: "(f o\<rightarrow> g) x = split g (f x)" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

729 
by (simp add: scomp_def) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

730 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

731 
lemma Pair_scomp: "Pair x o\<rightarrow> f = f x" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

732 
by (simp add: expand_fun_eq scomp_apply) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

733 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

734 
lemma scomp_Pair: "x o\<rightarrow> Pair = x" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

735 
by (simp add: expand_fun_eq scomp_apply) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

736 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

737 
lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

738 
by (simp add: expand_fun_eq split_twice scomp_def) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

739 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

740 
lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

741 
by (simp add: expand_fun_eq scomp_apply fcomp_def split_def) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

742 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

743 
lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)" 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

744 
by (simp add: expand_fun_eq scomp_apply fcomp_apply) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

745 

31202
52d332f8f909
pretty printing of functional combinators for evaluation code
haftmann
parents:
30924
diff
changeset

746 
code_const scomp 
52d332f8f909
pretty printing of functional combinators for evaluation code
haftmann
parents:
30924
diff
changeset

747 
(Eval infixl 3 "#>") 
52d332f8f909
pretty printing of functional combinators for evaluation code
haftmann
parents:
30924
diff
changeset

748 

26588
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

749 
no_notation fcomp (infixl "o>" 60) 
d83271bfaba5
removed syntax from monad combinators; renamed mbind to scomp
haftmann
parents:
26480
diff
changeset

750 
no_notation scomp (infixl "o\<rightarrow>" 60) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

751 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

752 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

753 
text {* 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

754 
@{term prod_fun}  action of the product functor upon 
36664
6302f9ad7047
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
krauss
parents:
36622
diff
changeset

755 
functions. 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

756 
*} 
21195  757 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

758 
definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where 
28562  759 
[code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

760 

28562  761 
lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

762 
by (simp add: prod_fun_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

763 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

764 
lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

765 
by (rule ext) auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

766 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

767 
lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

768 
by (rule ext) auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

769 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

770 
lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

771 
apply (rule image_eqI) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

772 
apply (rule prod_fun [symmetric], assumption) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

773 
done 
21195  774 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

775 
lemma prod_fun_imageE [elim!]: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

776 
assumes major: "c: (prod_fun f g)`r" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

777 
and cases: "!!x y. [ c=(f(x),g(y)); (x,y):r ] ==> P" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

778 
shows P 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

779 
apply (rule major [THEN imageE]) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

780 
apply (rule_tac p = x in PairE) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

781 
apply (rule cases) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

782 
apply (blast intro: prod_fun) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

783 
apply blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

784 
done 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

785 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

786 
definition 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

787 
apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

788 
where 
28562  789 
[code del]: "apfst f = prod_fun f id" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

790 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

791 
definition 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

792 
apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

793 
where 
28562  794 
[code del]: "apsnd f = prod_fun id f" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

795 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

796 
lemma apfst_conv [simp, code]: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

797 
"apfst f (x, y) = (f x, y)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

798 
by (simp add: apfst_def) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

799 

33638
548a34929e98
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
hoelzl
parents:
33594
diff
changeset

800 
lemma apsnd_conv [simp, code]: 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

801 
"apsnd f (x, y) = (x, f y)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

802 
by (simp add: apsnd_def) 
21195  803 

33594  804 
lemma fst_apfst [simp]: 
805 
"fst (apfst f x) = f (fst x)" 

806 
by (cases x) simp 

807 

808 
lemma fst_apsnd [simp]: 

809 
"fst (apsnd f x) = fst x" 

810 
by (cases x) simp 

811 

812 
lemma snd_apfst [simp]: 

813 
"snd (apfst f x) = snd x" 

814 
by (cases x) simp 

815 

816 
lemma snd_apsnd [simp]: 

817 
"snd (apsnd f x) = f (snd x)" 

818 
by (cases x) simp 

819 

820 
lemma apfst_compose: 

821 
"apfst f (apfst g x) = apfst (f \<circ> g) x" 

822 
by (cases x) simp 

823 

824 
lemma apsnd_compose: 

825 
"apsnd f (apsnd g x) = apsnd (f \<circ> g) x" 

826 
by (cases x) simp 

827 

828 
lemma apfst_apsnd [simp]: 

829 
"apfst f (apsnd g x) = (f (fst x), g (snd x))" 

830 
by (cases x) simp 

831 

832 
lemma apsnd_apfst [simp]: 

833 
"apsnd f (apfst g x) = (g (fst x), f (snd x))" 

834 
by (cases x) simp 

835 

836 
lemma apfst_id [simp] : 

837 
"apfst id = id" 

838 
by (simp add: expand_fun_eq) 

839 

840 
lemma apsnd_id [simp] : 

841 
"apsnd id = id" 

842 
by (simp add: expand_fun_eq) 

843 

844 
lemma apfst_eq_conv [simp]: 

845 
"apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)" 

846 
by (cases x) simp 

847 

848 
lemma apsnd_eq_conv [simp]: 

849 
"apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)" 

850 
by (cases x) simp 

851 

33638
548a34929e98
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
hoelzl
parents:
33594
diff
changeset

852 
lemma apsnd_apfst_commute: 
548a34929e98
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
hoelzl
parents:
33594
diff
changeset

853 
"apsnd f (apfst g p) = apfst g (apsnd f p)" 
548a34929e98
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
hoelzl
parents:
33594
diff
changeset

854 
by simp 
21195  855 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

856 
text {* 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

857 
Disjoint union of a family of sets  Sigma. 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

858 
*} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

859 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

860 
definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

861 
Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

862 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

863 
abbreviation 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

864 
Times :: "['a set, 'b set] => ('a * 'b) set" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

865 
(infixr "<*>" 80) where 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

866 
"A <*> B == Sigma A (%_. B)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

867 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

868 
notation (xsymbols) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

869 
Times (infixr "\<times>" 80) 
15394  870 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

871 
notation (HTML output) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

872 
Times (infixr "\<times>" 80) 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

873 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

874 
syntax 
35115  875 
"_Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

876 
translations 
35115  877 
"SIGMA x:A. B" == "CONST Sigma A (%x. B)" 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

878 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

879 
lemma SigmaI [intro!]: "[ a:A; b:B(a) ] ==> (a,b) : Sigma A B" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

880 
by (unfold Sigma_def) blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

881 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

882 
lemma SigmaE [elim!]: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

883 
"[ c: Sigma A B; 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

884 
!!x y.[ x:A; y:B(x); c=(x,y) ] ==> P 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

885 
] ==> P" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

886 
 {* The general elimination rule. *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

887 
by (unfold Sigma_def) blast 
20588  888 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

889 
text {* 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

890 
Elimination of @{term "(a, b) : A \<times> B"}  introduces no 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

891 
eigenvariables. 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

892 
*} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

893 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

894 
lemma SigmaD1: "(a, b) : Sigma A B ==> a : A" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

895 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

896 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

897 
lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

898 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

899 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

900 
lemma SigmaE2: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

901 
"[ (a, b) : Sigma A B; 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

902 
[ a:A; b:B(a) ] ==> P 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

903 
] ==> P" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

904 
by blast 
20588  905 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

906 
lemma Sigma_cong: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

907 
"\<lbrakk>A = B; !!x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

908 
\<Longrightarrow> (SIGMA x: A. C x) = (SIGMA x: B. D x)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

909 
by auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

910 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

911 
lemma Sigma_mono: "[ A <= C; !!x. x:A ==> B x <= D x ] ==> Sigma A B <= Sigma C D" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

912 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

913 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

914 
lemma Sigma_empty1 [simp]: "Sigma {} B = {}" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

915 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

916 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

917 
lemma Sigma_empty2 [simp]: "A <*> {} = {}" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

918 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

919 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

920 
lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

921 
by auto 
21908  922 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

923 
lemma Compl_Times_UNIV1 [simp]: " (UNIV <*> A) = UNIV <*> (A)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

924 
by auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

925 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

926 
lemma Compl_Times_UNIV2 [simp]: " (A <*> UNIV) = (A) <*> UNIV" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

927 
by auto 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

928 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

929 
lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

930 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

931 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

932 
lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

933 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

934 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

935 
lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

936 
by (blast elim: equalityE) 
20588  937 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

938 
lemma SetCompr_Sigma_eq: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

939 
"Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

940 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

941 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

942 
lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

943 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

944 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

945 
lemma UN_Times_distrib: 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

946 
"(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

947 
 {* Suggested by Pierre Chartier *} 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

948 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

949 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

950 
lemma split_paired_Ball_Sigma [simp,no_atp]: 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

951 
"(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

952 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

953 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35427
diff
changeset

954 
lemma split_paired_Bex_Sigma [simp,no_atp]: 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

955 
"(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

956 
by blast 
21908  957 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

958 
lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

959 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

960 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

961 
lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

962 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

963 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

964 
lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

965 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

966 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

967 
lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

968 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

969 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

970 
lemma Sigma_Diff_distrib1: "(SIGMA i:I  J. C(i)) = (SIGMA i:I. C(i))  (SIGMA j:J. C(j))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

971 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

972 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

973 
lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i)  B(i)) = (SIGMA i:I. A(i))  (SIGMA i:I. B(i))" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

974 
by blast 
21908  975 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

976 
lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)" 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

977 
by blast 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

978 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

979 
text {* 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

980 
Nondependent versions are needed to avoid the need for higherorder 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

981 
matching, especially when the rules are reoriented. 
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

982 
*} 
21908  983 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

984 
lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" 
28719  985 
by blast 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

986 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

987 
lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" 
28719  988 
by blast 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

989 

d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

990 
lemma Times_Diff_distrib1: "(A  B) <*> C = (A <*> C)  (B <*> C)" 
28719  991 
by blast 
26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

992 

36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

993 
lemma Times_empty[simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

994 
by auto 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

995 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

996 
lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

997 
by (auto intro!: image_eqI) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

998 

e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

999 
lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1000 
by (auto intro!: image_eqI) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1001 

28719  1002 
lemma insert_times_insert[simp]: 
1003 
"insert a A \<times> insert b B = 

1004 
insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)" 

1005 
by blast 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

1006 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33089
diff
changeset

1007 
lemma vimage_Times: "f ` (A \<times> B) = ((fst \<circ> f) ` A) \<inter> ((snd \<circ> f) ` B)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33089
diff
changeset

1008 
by (auto, rule_tac p = "f x" in PairE, auto) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33089
diff
changeset

1009 

35822  1010 
lemma swap_inj_on: 
36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1011 
"inj_on (\<lambda>(i, j). (j, i)) A" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1012 
by (auto intro!: inj_onI) 
35822  1013 

1014 
lemma swap_product: 

1015 
"(%(i, j). (j, i)) ` (A \<times> B) = B \<times> A" 

1016 
by (simp add: split_def image_def) blast 

1017 

36622
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1018 
lemma image_split_eq_Sigma: 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1019 
"(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f ` {x} \<inter> A))" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1020 
proof (safe intro!: imageI vimageI) 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1021 
fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1022 
show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1023 
using * eq[symmetric] by auto 
e393a91f86df
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
hoelzl
parents:
36176
diff
changeset

1024 
qed simp_all 
35822  1025 

26358
d6a508c16908
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
haftmann
parents:
26340
diff
changeset

1026 
subsubsection {* Code generator setup *} 
21908  1027 

28562  1028 
lemma [code]: 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

1029 
"eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq) 
20588  1030 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1031 
lemma split_case_cert: 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1032 
assumes "CASE \<equiv> split f" 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1033 
shows "CASE (a, b) \<equiv> f a b" 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1034 
using assms by simp 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1035 

98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1036 
setup {* 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1037 
Code.add_case @{thm split_case_cert} 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1038 
*} 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24699
diff
changeset

1039 

21908  1040 
code_type * 
1041 
(SML infix 2 "*") 

1042 
(OCaml infix 2 "*") 

1043 
(Haskell "!((_),/ (_))") 

34900  1044 
(Scala "((_),/ (_))") 
21908  1045 

20588  1046 
code_instance * :: eq 
1047 
(Haskell ) 

1048 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28262
diff
changeset

1049 
code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" 
20588  1050 
(Haskell infixl 4 "==") 
1051 

21908  1052 
code_const Pair 
1053 
(SML "!((_),/ (_))") 

1054 
(OCaml "!((_),/ (_))") 

1055 
(Haskell "!((_),/ (_))") 

34886  1056 
(Scala "!((_),/ (_))") 
20588  1057 

22389  1058 
code_const fst and snd 
1059 
(Haskell "fst" and "snd") 

1060 

15394  1061 
types_code 
1062 
"*" ("(_ */ _)") 

16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16634
diff
changeset

1063 
attach (term_of) {* 
25885  1064 
fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT $ aF x $ bF y; 
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16634
diff
changeset

1065 
*} 
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16634
diff
changeset

1066 
attach (test) {* 
25885  1067 
fun gen_id_42 aG aT bG bT i = 
1068 
let 

1069 
val (x, t) = aG i; 

1070 
val (y, u) = bG i 

1071 
in ((x, y), fn () => HOLogic.pair_const aT bT $ t () $ u ()) end; 

16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16634
diff
changeset

1072 
*} 
15394  1073 

18706
1e7562c7afe6
Reinserted consts_code declaration accidentally deleted
berghofe
parents:
18702
diff
changeset

1074 
consts_code 
1e7562c7afe6
Reinserted consts_code declaration accidentally deleted
berghofe
parents:
18702
diff
changeset

1075 
"Pair" ("(_,/ _)") 
1e7562c7afe6
Reinserted consts_code declaration accidentally deleted
berghofe
parents:
18702
diff
changeset

1076 

21908  1077 
setup {* 
1078 
let 

18013  1079 

19039  1080 
fun strip_abs_split 0 t = ([], t) 
1081 
 strip_abs_split i (Abs (s, T, t)) = 

18013  1082 
let 
1083 
val s' = Codegen.new_name t s; 

1084 
val v = Free (s', T) 

19039  1085 
in apfst (cons v) (strip_abs_split (i1) (subst_bound (v, t))) end 
35364  1086 
 strip_abs_split i (u as Const (@{const_name split}, _) $ t) = 
1087 
(case strip_abs_split (i+1) t of 

15394  1088 
(v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u) 
1089 
 _ => ([], u)) 

30604  1090 
 strip_abs_split i t = 
1091 
strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0)); 

18013  1092 

35364  1093 
fun let_codegen thy defs dep thyname brack t gr = 
1094 
(case strip_comb t of 

1095 
(t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) => 

15394  1096 
let 
35364  1097 
fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) = 
19039  1098 
(case strip_abs_split 1 u of 
15394  1099 
([p], u') => apfst (cons (p, t)) (dest_let u') 
1100 
 _ => ([], l)) 

1101 
 dest_let t = ([], t); 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1102 
fun mk_code (l, r) gr = 
15394  1103 
let 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1104 
val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1105 
val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1106 
in ((pl, pr), gr2) end 
16634  1107 
in case dest_let (t1 $ t2 $ t3) of 
15531  1108 
([], _) => NONE 
15394  1109 
 (ps, u) => 
1110 
let 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1111 
val (qs, gr1) = fold_map mk_code ps gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1112 
val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1113 
val (pargs, gr3) = fold_map 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1114 
(Codegen.invoke_codegen thy defs dep thyname true) ts gr2 
15394  1115 
in 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1116 
SOME (Codegen.mk_app brack 
32952  1117 
(Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26798
diff
changeset

1118 
(separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) => 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26798
diff
changeset

1119 
[Pretty.block [Codegen.str "val ", pl, Codegen.str " =", 
16634  1120 
Pretty.brk 1, pr]]) qs))), 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
26798
diff
changeset

1121 
Pretty.brk 1, Codegen.str "in ", pu, 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1122 
Pretty.brk 1, Codegen.str "end"])) pargs, gr3) 
15394  1123 
end 
1124 
end 

16634  1125 
 _ => NONE); 
15394  1126 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
28346
diff
changeset

1127 
fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of 
35364  1128 
(t1 as Const (@{const_name split}, _), t2 :: ts) => 
30604  1129 
let 
1130 
val ([p], u) = strip_abs_split 1 (t1 $ t2); 

1131 
val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr; 

1132 
val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1; 

1133 
val (pargs, gr3) = fold_map 

1134 
(Codegen.invoke_codegen thy defs dep thyname true) ts gr2 

1135 
in 

1136 
SOME (Codegen.mk_app brack 

1137 
(Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>", 

1138 
Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2) 

1139 
end 

16634  1140 
 _ => NONE); 
15394  1141 

21908  1142 
in 
1143 

20105  1144 
Codegen.add_codegen "let_codegen" let_codegen 
1145 
#> Codegen.add_codegen "split_codegen" split_codegen 

15394  1146 

21908  1147 
end 
15394  1148 
*} 
1149 

31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31667
diff
changeset

1150 
use "Tools/inductive_set.ML" 
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31667
diff
changeset

1151 
setup Inductive_Set.setup 
24699
c6674504103f
datatype interpretators for size and datatype_realizer
haftmann
parents:
24286
diff
changeset

1152 

10213  1153 
end 