1(* Title: HOL/Product_Type.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section \<open>Cartesian products\<close> 7 8theory Product_Type 9 imports Typedef Inductive Fun 10 keywords "inductive_set" "coinductive_set" :: thy_decl 11begin 12 13subsection \<open>@{typ bool} is a datatype\<close> 14 15free_constructors (discs_sels) case_bool for True | False 16 by auto 17 18text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 19 20setup \<open>Sign.mandatory_path "old"\<close> 21 22old_rep_datatype True False by (auto intro: bool_induct) 23 24setup \<open>Sign.parent_path\<close> 25 26text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 27 28setup \<open>Sign.mandatory_path "bool"\<close> 29 30lemmas induct = old.bool.induct 31lemmas inducts = old.bool.inducts 32lemmas rec = old.bool.rec 33lemmas simps = bool.distinct bool.case bool.rec 34 35setup \<open>Sign.parent_path\<close> 36 37declare case_split [cases type: bool] 38 \<comment> \<open>prefer plain propositional version\<close> 39 40lemma [code]: "HOL.equal False P \<longleftrightarrow> \<not> P" 41 and [code]: "HOL.equal True P \<longleftrightarrow> P" 42 and [code]: "HOL.equal P False \<longleftrightarrow> \<not> P" 43 and [code]: "HOL.equal P True \<longleftrightarrow> P" 44 and [code nbe]: "HOL.equal P P \<longleftrightarrow> True" 45 by (simp_all add: equal) 46 47lemma If_case_cert: 48 assumes "CASE \<equiv> (\<lambda>b. If b f g)" 49 shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)" 50 using assms by simp_all 51 52setup \<open>Code.declare_case_global @{thm If_case_cert}\<close> 53 54code_printing 55 constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "==" 56| class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) - 57 58 59subsection \<open>The \<open>unit\<close> type\<close> 60 61typedef unit = "{True}" 62 by auto 63 64definition Unity :: unit ("'(')") 65 where "() = Abs_unit True" 66 67lemma unit_eq [no_atp]: "u = ()" 68 by (induct u) (simp add: Unity_def) 69 70text \<open> 71 Simplification procedure for @{thm [source] unit_eq}. Cannot use 72 this rule directly --- it loops! 73\<close> 74 75simproc_setup unit_eq ("x::unit") = \<open> 76 fn _ => fn _ => fn ct => 77 if HOLogic.is_unit (Thm.term_of ct) then NONE 78 else SOME (mk_meta_eq @{thm unit_eq}) 79\<close> 80 81free_constructors case_unit for "()" 82 by auto 83 84text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 85 86setup \<open>Sign.mandatory_path "old"\<close> 87 88old_rep_datatype "()" by simp 89 90setup \<open>Sign.parent_path\<close> 91 92text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 93 94setup \<open>Sign.mandatory_path "unit"\<close> 95 96lemmas induct = old.unit.induct 97lemmas inducts = old.unit.inducts 98lemmas rec = old.unit.rec 99lemmas simps = unit.case unit.rec 100 101setup \<open>Sign.parent_path\<close> 102 103lemma unit_all_eq1: "(\<And>x::unit. PROP P x) \<equiv> PROP P ()" 104 by simp 105 106lemma unit_all_eq2: "(\<And>x::unit. PROP P) \<equiv> PROP P" 107 by (rule triv_forall_equality) 108 109text \<open> 110 This rewrite counters the effect of simproc \<open>unit_eq\<close> on @{term 111 [source] "\<lambda>u::unit. f u"}, replacing it by @{term [source] 112 f} rather than by @{term [source] "\<lambda>u. f ()"}. 113\<close> 114 115lemma unit_abs_eta_conv [simp]: "(\<lambda>u::unit. f ()) = f" 116 by (rule ext) simp 117 118lemma UNIV_unit: "UNIV = {()}" 119 by auto 120 121instantiation unit :: default 122begin 123 124definition "default = ()" 125 126instance .. 127 128end 129 130instantiation unit :: "{complete_boolean_algebra,complete_linorder,wellorder}" 131begin 132 133definition less_eq_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" 134 where "(_::unit) \<le> _ \<longleftrightarrow> True" 135 136lemma less_eq_unit [iff]: "u \<le> v" for u v :: unit 137 by (simp add: less_eq_unit_def) 138 139definition less_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" 140 where "(_::unit) < _ \<longleftrightarrow> False" 141 142lemma less_unit [iff]: "\<not> u < v" for u v :: unit 143 by (simp_all add: less_eq_unit_def less_unit_def) 144 145definition bot_unit :: unit 146 where [code_unfold]: "\<bottom> = ()" 147 148definition top_unit :: unit 149 where [code_unfold]: "\<top> = ()" 150 151definition inf_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit" 152 where [simp]: "_ \<sqinter> _ = ()" 153 154definition sup_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit" 155 where [simp]: "_ \<squnion> _ = ()" 156 157definition Inf_unit :: "unit set \<Rightarrow> unit" 158 where [simp]: "\<Sqinter>_ = ()" 159 160definition Sup_unit :: "unit set \<Rightarrow> unit" 161 where [simp]: "\<Squnion>_ = ()" 162 163definition uminus_unit :: "unit \<Rightarrow> unit" 164 where [simp]: "- _ = ()" 165 166declare less_eq_unit_def [abs_def, code_unfold] 167 less_unit_def [abs_def, code_unfold] 168 inf_unit_def [abs_def, code_unfold] 169 sup_unit_def [abs_def, code_unfold] 170 Inf_unit_def [abs_def, code_unfold] 171 Sup_unit_def [abs_def, code_unfold] 172 uminus_unit_def [abs_def, code_unfold] 173 174instance 175 by intro_classes auto 176 177end 178 179lemma [code]: "HOL.equal u v \<longleftrightarrow> True" for u v :: unit 180 unfolding equal unit_eq [of u] unit_eq [of v] by rule+ 181 182code_printing 183 type_constructor unit \<rightharpoonup> 184 (SML) "unit" 185 and (OCaml) "unit" 186 and (Haskell) "()" 187 and (Scala) "Unit" 188| constant Unity \<rightharpoonup> 189 (SML) "()" 190 and (OCaml) "()" 191 and (Haskell) "()" 192 and (Scala) "()" 193| class_instance unit :: equal \<rightharpoonup> 194 (Haskell) - 195| constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup> 196 (Haskell) infix 4 "==" 197 198code_reserved SML 199 unit 200 201code_reserved OCaml 202 unit 203 204code_reserved Scala 205 Unit 206 207 208subsection \<open>The product type\<close> 209 210subsubsection \<open>Type definition\<close> 211 212definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" 213 where "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)" 214 215definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}" 216 217typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set" 218 unfolding prod_def by auto 219 220type_notation (ASCII) 221 prod (infixr "*" 20) 222 223definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" 224 where "Pair a b = Abs_prod (Pair_Rep a b)" 225 226lemma prod_cases: "(\<And>a b. P (Pair a b)) \<Longrightarrow> P p" 227 by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) 228 229free_constructors case_prod for Pair fst snd 230proof - 231 fix P :: bool and p :: "'a \<times> 'b" 232 show "(\<And>x1 x2. p = Pair x1 x2 \<Longrightarrow> P) \<Longrightarrow> P" 233 by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def) 234next 235 fix a c :: 'a and b d :: 'b 236 have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d" 237 by (auto simp add: Pair_Rep_def fun_eq_iff) 238 moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod" 239 by (auto simp add: prod_def) 240 ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d" 241 by (simp add: Pair_def Abs_prod_inject) 242qed 243 244text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close> 245 246setup \<open>Sign.mandatory_path "old"\<close> 247 248old_rep_datatype Pair 249 by (erule prod_cases) (rule prod.inject) 250 251setup \<open>Sign.parent_path\<close> 252 253text \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close> 254 255setup \<open>Sign.mandatory_path "prod"\<close> 256 257declare old.prod.inject [iff del] 258 259lemmas induct = old.prod.induct 260lemmas inducts = old.prod.inducts 261lemmas rec = old.prod.rec 262lemmas simps = prod.inject prod.case prod.rec 263 264setup \<open>Sign.parent_path\<close> 265 266declare prod.case [nitpick_simp del] 267declare old.prod.case_cong_weak [cong del] 268declare prod.case_eq_if [mono] 269declare prod.split [no_atp] 270declare prod.split_asm [no_atp] 271 272text \<open> 273 @{thm [source] prod.split} could be declared as \<open>[split]\<close> 274 done after the Splitter has been speeded up significantly; 275 precompute the constants involved and don't do anything unless the 276 current goal contains one of those constants. 277\<close> 278 279 280subsubsection \<open>Tuple syntax\<close> 281 282text \<open> 283 Patterns -- extends pre-defined type @{typ pttrn} used in 284 abstractions. 285\<close> 286 287nonterminal tuple_args and patterns 288syntax 289 "_tuple" :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b" ("(1'(_,/ _'))") 290 "_tuple_arg" :: "'a \<Rightarrow> tuple_args" ("_") 291 "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args" ("_,/ _") 292 "_pattern" :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn" ("'(_,/ _')") 293 "" :: "pttrn \<Rightarrow> patterns" ("_") 294 "_patterns" :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns" ("_,/ _") 295 "_unit" :: pttrn ("'(')") 296translations 297 "(x, y)" \<rightleftharpoons> "CONST Pair x y" 298 "_pattern x y" \<rightleftharpoons> "CONST Pair x y" 299 "_patterns x y" \<rightleftharpoons> "CONST Pair x y" 300 "_tuple x (_tuple_args y z)" \<rightleftharpoons> "_tuple x (_tuple_arg (_tuple y z))" 301 "\<lambda>(x, y, zs). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x (y, zs). b)" 302 "\<lambda>(x, y). b" \<rightleftharpoons> "CONST case_prod (\<lambda>x y. b)" 303 "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t" 304 \<comment> \<open>This rule accommodates tuples in \<open>case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>\<close>: 305 The \<open>(x, y)\<close> is parsed as \<open>Pair x y\<close> because it is \<open>logic\<close>, 306 not \<open>pttrn\<close>.\<close> 307 "\<lambda>(). b" \<rightleftharpoons> "CONST case_unit b" 308 "_abs (CONST Unity) t" \<rightharpoonup> "\<lambda>(). t" 309 310text \<open>print @{term "case_prod f"} as @{term "\<lambda>(x, y). f x y"} and 311 @{term "case_prod (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close> 312 313typed_print_translation \<open> 314 let 315 fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match 316 | case_prod_guess_names_tr' T [Abs (x, xT, t)] = 317 (case (head_of t) of 318 Const (@{const_syntax case_prod}, _) => raise Match 319 | _ => 320 let 321 val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; 322 val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); 323 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); 324 in 325 Syntax.const @{syntax_const "_abs"} $ 326 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 327 end) 328 | case_prod_guess_names_tr' T [t] = 329 (case head_of t of 330 Const (@{const_syntax case_prod}, _) => raise Match 331 | _ => 332 let 333 val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; 334 val (y, t') = 335 Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); 336 val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); 337 in 338 Syntax.const @{syntax_const "_abs"} $ 339 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 340 end) 341 | case_prod_guess_names_tr' _ _ = raise Match; 342 in [(@{const_syntax case_prod}, K case_prod_guess_names_tr')] end 343\<close> 344 345text \<open>Reconstruct pattern from (nested) @{const case_prod}s, 346 avoiding eta-contraction of body; required for enclosing "let", 347 if "let" does not avoid eta-contraction, which has been observed to occur.\<close> 348 349print_translation \<open> 350 let 351 fun case_prod_tr' [Abs (x, T, t as (Abs abs))] = 352 (* case_prod (\<lambda>x y. t) \<Rightarrow> \<lambda>(x, y) t *) 353 let 354 val (y, t') = Syntax_Trans.atomic_abs_tr' abs; 355 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); 356 in 357 Syntax.const @{syntax_const "_abs"} $ 358 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' 359 end 360 | case_prod_tr' [Abs (x, T, (s as Const (@{const_syntax case_prod}, _) $ t))] = 361 (* case_prod (\<lambda>x. (case_prod (\<lambda>y z. t))) \<Rightarrow> \<lambda>(x, y, z). t *) 362 let 363 val Const (@{syntax_const "_abs"}, _) $ 364 (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = 365 case_prod_tr' [t]; 366 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); 367 in 368 Syntax.const @{syntax_const "_abs"} $ 369 (Syntax.const @{syntax_const "_pattern"} $ x' $ 370 (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t'' 371 end 372 | case_prod_tr' [Const (@{const_syntax case_prod}, _) $ t] = 373 (* case_prod (case_prod (\<lambda>x y z. t)) \<Rightarrow> \<lambda>((x, y), z). t *) 374 case_prod_tr' [(case_prod_tr' [t])] 375 (* inner case_prod_tr' creates next pattern *) 376 | case_prod_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = 377 (* case_prod (\<lambda>pttrn z. t) \<Rightarrow> \<lambda>(pttrn, z). t *) 378 let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in 379 Syntax.const @{syntax_const "_abs"} $ 380 (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t 381 end 382 | case_prod_tr' _ = raise Match; 383 in [(@{const_syntax case_prod}, K case_prod_tr')] end 384\<close> 385 386 387subsubsection \<open>Code generator setup\<close> 388 389code_printing 390 type_constructor prod \<rightharpoonup> 391 (SML) infix 2 "*" 392 and (OCaml) infix 2 "*" 393 and (Haskell) "!((_),/ (_))" 394 and (Scala) "((_),/ (_))" 395| constant Pair \<rightharpoonup> 396 (SML) "!((_),/ (_))" 397 and (OCaml) "!((_),/ (_))" 398 and (Haskell) "!((_),/ (_))" 399 and (Scala) "!((_),/ (_))" 400| class_instance prod :: equal \<rightharpoonup> 401 (Haskell) - 402| constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup> 403 (Haskell) infix 4 "==" 404| constant fst \<rightharpoonup> (Haskell) "fst" 405| constant snd \<rightharpoonup> (Haskell) "snd" 406 407 408subsubsection \<open>Fundamental operations and properties\<close> 409 410lemma Pair_inject: "(a, b) = (a', b') \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R" 411 by simp 412 413lemma surj_pair [simp]: "\<exists>x y. p = (x, y)" 414 by (cases p) simp 415 416lemma fst_eqD: "fst (x, y) = a \<Longrightarrow> x = a" 417 by simp 418 419lemma snd_eqD: "snd (x, y) = a \<Longrightarrow> y = a" 420 by simp 421 422lemma case_prod_unfold [nitpick_unfold]: "case_prod = (\<lambda>c p. c (fst p) (snd p))" 423 by (simp add: fun_eq_iff split: prod.split) 424 425lemma case_prod_conv [simp, code]: "(case (a, b) of (c, d) \<Rightarrow> f c d) = f a b" 426 by (fact prod.case) 427 428lemmas surjective_pairing = prod.collapse [symmetric] 429 430lemma prod_eq_iff: "s = t \<longleftrightarrow> fst s = fst t \<and> snd s = snd t" 431 by (cases s, cases t) simp 432 433lemma prod_eqI [intro?]: "fst p = fst q \<Longrightarrow> snd p = snd q \<Longrightarrow> p = q" 434 by (simp add: prod_eq_iff) 435 436lemma case_prodI: "f a b \<Longrightarrow> case (a, b) of (c, d) \<Rightarrow> f c d" 437 by (rule prod.case [THEN iffD2]) 438 439lemma case_prodD: "(case (a, b) of (c, d) \<Rightarrow> f c d) \<Longrightarrow> f a b" 440 by (rule prod.case [THEN iffD1]) 441 442lemma case_prod_Pair [simp]: "case_prod Pair = id" 443 by (simp add: fun_eq_iff split: prod.split) 444 445lemma case_prod_eta: "(\<lambda>(x, y). f (x, y)) = f" 446 \<comment> \<open>Subsumes the old \<open>split_Pair\<close> when @{term f} is the identity function.\<close> 447 by (simp add: fun_eq_iff split: prod.split) 448 449(* This looks like a sensible simp-rule but appears to do more harm than good: 450lemma case_prod_const [simp]: "(\<lambda>(_,_). c) = (\<lambda>_. c)" 451by(rule case_prod_eta) 452*) 453 454lemma case_prod_comp: "(case x of (a, b) \<Rightarrow> (f \<circ> g) a b) = f (g (fst x)) (snd x)" 455 by (cases x) simp 456 457lemma The_case_prod: "The (case_prod P) = (THE xy. P (fst xy) (snd xy))" 458 by (simp add: case_prod_unfold) 459 460lemma cond_case_prod_eta: "(\<And>x y. f x y = g (x, y)) \<Longrightarrow> (\<lambda>(x, y). f x y) = g" 461 by (simp add: case_prod_eta) 462 463lemma split_paired_all [no_atp]: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" 464proof 465 fix a b 466 assume "\<And>x. PROP P x" 467 then show "PROP P (a, b)" . 468next 469 fix x 470 assume "\<And>a b. PROP P (a, b)" 471 from \<open>PROP P (fst x, snd x)\<close> show "PROP P x" by simp 472qed 473 474text \<open> 475 The rule @{thm [source] split_paired_all} does not work with the 476 Simplifier because it also affects premises in congrence rules, 477 where this can lead to premises of the form \<open>\<And>a b. \<dots> = ?P(a, b)\<close> 478 which cannot be solved by reflexivity. 479\<close> 480 481lemmas split_tupled_all = split_paired_all unit_all_eq2 482 483ML \<open> 484 (* replace parameters of product type by individual component parameters *) 485 local (* filtering with exists_paired_all is an essential optimization *) 486 fun exists_paired_all (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = 487 can HOLogic.dest_prodT T orelse exists_paired_all t 488 | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u 489 | exists_paired_all (Abs (_, _, t)) = exists_paired_all t 490 | exists_paired_all _ = false; 491 val ss = 492 simpset_of 493 (put_simpset HOL_basic_ss @{context} 494 addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] 495 addsimprocs [@{simproc unit_eq}]); 496 in 497 fun split_all_tac ctxt = SUBGOAL (fn (t, i) => 498 if exists_paired_all t then safe_full_simp_tac (put_simpset ss ctxt) i else no_tac); 499 500 fun unsafe_split_all_tac ctxt = SUBGOAL (fn (t, i) => 501 if exists_paired_all t then full_simp_tac (put_simpset ss ctxt) i else no_tac); 502 503 fun split_all ctxt th = 504 if exists_paired_all (Thm.prop_of th) 505 then full_simplify (put_simpset ss ctxt) th else th; 506 end; 507\<close> 508 509setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close> 510 511lemma split_paired_All [simp, no_atp]: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>a b. P (a, b))" 512 \<comment> \<open>\<open>[iff]\<close> is not a good idea because it makes \<open>blast\<close> loop\<close> 513 by fast 514 515lemma split_paired_Ex [simp, no_atp]: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>a b. P (a, b))" 516 by fast 517 518lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))" 519 \<comment> \<open>Can't be added to simpset: loops!\<close> 520 by (simp add: case_prod_eta) 521 522text \<open> 523 Simplification procedure for @{thm [source] cond_case_prod_eta}. Using 524 @{thm [source] case_prod_eta} as a rewrite rule is not general enough, 525 and using @{thm [source] cond_case_prod_eta} directly would render some 526 existing proofs very inefficient; similarly for \<open>prod.case_eq_if\<close>. 527\<close> 528 529ML \<open> 530local 531 val cond_case_prod_eta_ss = 532 simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms cond_case_prod_eta}); 533 fun Pair_pat k 0 (Bound m) = (m = k) 534 | Pair_pat k i (Const (@{const_name Pair}, _) $ Bound m $ t) = 535 i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t 536 | Pair_pat _ _ _ = false; 537 fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t 538 | no_args k i (t $ u) = no_args k i t andalso no_args k i u 539 | no_args k i (Bound m) = m < k orelse m > k + i 540 | no_args _ _ _ = true; 541 fun split_pat tp i (Abs (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE 542 | split_pat tp i (Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t 543 | split_pat tp i _ = NONE; 544 fun metaeq ctxt lhs rhs = mk_meta_eq (Goal.prove ctxt [] [] 545 (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) 546 (K (simp_tac (put_simpset cond_case_prod_eta_ss ctxt) 1))); 547 548 fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t 549 | beta_term_pat k i (t $ u) = 550 Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u) 551 | beta_term_pat k i t = no_args k i t; 552 fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg 553 | eta_term_pat _ _ _ = false; 554 fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t) 555 | subst arg k i (t $ u) = 556 if Pair_pat k i (t $ u) then incr_boundvars k arg 557 else (subst arg k i t $ subst arg k i u) 558 | subst arg k i t = t; 559in 560 fun beta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t) $ arg) = 561 (case split_pat beta_term_pat 1 t of 562 SOME (i, f) => SOME (metaeq ctxt s (subst arg 0 i f)) 563 | NONE => NONE) 564 | beta_proc _ _ = NONE; 565 fun eta_proc ctxt (s as Const (@{const_name case_prod}, _) $ Abs (_, _, t)) = 566 (case split_pat eta_term_pat 1 t of 567 SOME (_, ft) => SOME (metaeq ctxt s (let val f $ _ = ft in f end)) 568 | NONE => NONE) 569 | eta_proc _ _ = NONE; 570end; 571\<close> 572simproc_setup case_prod_beta ("case_prod f z") = 573 \<open>fn _ => fn ctxt => fn ct => beta_proc ctxt (Thm.term_of ct)\<close> 574simproc_setup case_prod_eta ("case_prod f") = 575 \<open>fn _ => fn ctxt => fn ct => eta_proc ctxt (Thm.term_of ct)\<close> 576 577lemma case_prod_beta': "(\<lambda>(x,y). f x y) = (\<lambda>x. f (fst x) (snd x))" 578 by (auto simp: fun_eq_iff) 579 580text \<open> 581 \<^medskip> @{const case_prod} used as a logical connective or set former. 582 583 \<^medskip> These rules are for use with \<open>blast\<close>; could instead 584 call \<open>simp\<close> using @{thm [source] prod.split} as rewrite.\<close> 585 586lemma case_prodI2: 587 "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> c a b) \<Longrightarrow> case p of (a, b) \<Rightarrow> c a b" 588 by (simp add: split_tupled_all) 589 590lemma case_prodI2': 591 "\<And>p. (\<And>a b. (a, b) = p \<Longrightarrow> c a b x) \<Longrightarrow> (case p of (a, b) \<Rightarrow> c a b) x" 592 by (simp add: split_tupled_all) 593 594lemma case_prodE [elim!]: 595 "(case p of (a, b) \<Rightarrow> c a b) \<Longrightarrow> (\<And>x y. p = (x, y) \<Longrightarrow> c x y \<Longrightarrow> Q) \<Longrightarrow> Q" 596 by (induct p) simp 597 598lemma case_prodE' [elim!]: 599 "(case p of (a, b) \<Rightarrow> c a b) z \<Longrightarrow> (\<And>x y. p = (x, y) \<Longrightarrow> c x y z \<Longrightarrow> Q) \<Longrightarrow> Q" 600 by (induct p) simp 601 602lemma case_prodE2: 603 assumes q: "Q (case z of (a, b) \<Rightarrow> P a b)" 604 and r: "\<And>x y. z = (x, y) \<Longrightarrow> Q (P x y) \<Longrightarrow> R" 605 shows R 606proof (rule r) 607 show "z = (fst z, snd z)" by simp 608 then show "Q (P (fst z) (snd z))" 609 using q by (simp add: case_prod_unfold) 610qed 611 612lemma case_prodD': "(case (a, b) of (c, d) \<Rightarrow> R c d) c \<Longrightarrow> R a b c" 613 by simp 614 615lemma mem_case_prodI: "z \<in> c a b \<Longrightarrow> z \<in> (case (a, b) of (d, e) \<Rightarrow> c d e)" 616 by simp 617 618lemma mem_case_prodI2 [intro!]: 619 "\<And>p. (\<And>a b. p = (a, b) \<Longrightarrow> z \<in> c a b) \<Longrightarrow> z \<in> (case p of (a, b) \<Rightarrow> c a b)" 620 by (simp only: split_tupled_all) simp 621 622declare mem_case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close> 623declare case_prodI2' [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close> 624declare case_prodI2 [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close> 625declare case_prodI [intro!] \<comment> \<open>postponed to maintain traditional declaration order!\<close> 626 627lemma mem_case_prodE [elim!]: 628 assumes "z \<in> case_prod c p" 629 obtains x y where "p = (x, y)" and "z \<in> c x y" 630 using assms by (rule case_prodE2) 631 632ML \<open> 633local (* filtering with exists_p_split is an essential optimization *) 634 fun exists_p_split (Const (@{const_name case_prod},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true 635 | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u 636 | exists_p_split (Abs (_, _, t)) = exists_p_split t 637 | exists_p_split _ = false; 638in 639 fun split_conv_tac ctxt = SUBGOAL (fn (t, i) => 640 if exists_p_split t 641 then safe_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms case_prod_conv}) i 642 else no_tac); 643end; 644\<close> 645 646(* This prevents applications of splitE for already splitted arguments leading 647 to quite time-consuming computations (in particular for nested tuples) *) 648setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac))\<close> 649 650lemma split_eta_SetCompr [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P (x, y)) = P" 651 by (rule ext) fast 652 653lemma split_eta_SetCompr2 [simp, no_atp]: "(\<lambda>u. \<exists>x y. u = (x, y) \<and> P x y) = case_prod P" 654 by (rule ext) fast 655 656lemma split_part [simp]: "(\<lambda>(a,b). P \<and> Q a b) = (\<lambda>ab. P \<and> case_prod Q ab)" 657 \<comment> \<open>Allows simplifications of nested splits in case of independent predicates.\<close> 658 by (rule ext) blast 659 660(* Do NOT make this a simp rule as it 661 a) only helps in special situations 662 b) can lead to nontermination in the presence of split_def 663*) 664lemma split_comp_eq: 665 fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" 666 and g :: "'d \<Rightarrow> 'a" 667 shows "(\<lambda>u. f (g (fst u)) (snd u)) = case_prod (\<lambda>x. f (g x))" 668 by (rule ext) auto 669 670lemma pair_imageI [intro]: "(a, b) \<in> A \<Longrightarrow> f a b \<in> (\<lambda>(a, b). f a b) ` A" 671 by (rule image_eqI [where x = "(a, b)"]) auto 672 673lemma Collect_const_case_prod[simp]: "{(a,b). P} = (if P then UNIV else {})" 674by auto 675 676lemma The_split_eq [simp]: "(THE (x',y'). x = x' \<and> y = y') = (x, y)" 677 by blast 678 679(* 680the following would be slightly more general, 681but cannot be used as rewrite rule: 682### Cannot add premise as rewrite rule because it contains (type) unknowns: 683### ?y = .x 684Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)" 685by (rtac some_equality 1) 686by ( Simp_tac 1) 687by (split_all_tac 1) 688by (Asm_full_simp_tac 1) 689qed "The_split_eq"; 690*) 691 692lemma case_prod_beta: "case_prod f p = f (fst p) (snd p)" 693 by (fact prod.case_eq_if) 694 695lemma prod_cases3 [cases type]: 696 obtains (fields) a b c where "y = (a, b, c)" 697 by (cases y, case_tac b) blast 698 699lemma prod_induct3 [case_names fields, induct type]: 700 "(\<And>a b c. P (a, b, c)) \<Longrightarrow> P x" 701 by (cases x) blast 702 703lemma prod_cases4 [cases type]: 704 obtains (fields) a b c d where "y = (a, b, c, d)" 705 by (cases y, case_tac c) blast 706 707lemma prod_induct4 [case_names fields, induct type]: 708 "(\<And>a b c d. P (a, b, c, d)) \<Longrightarrow> P x" 709 by (cases x) blast 710 711lemma prod_cases5 [cases type]: 712 obtains (fields) a b c d e where "y = (a, b, c, d, e)" 713 by (cases y, case_tac d) blast 714 715lemma prod_induct5 [case_names fields, induct type]: 716 "(\<And>a b c d e. P (a, b, c, d, e)) \<Longrightarrow> P x" 717 by (cases x) blast 718 719lemma prod_cases6 [cases type]: 720 obtains (fields) a b c d e f where "y = (a, b, c, d, e, f)" 721 by (cases y, case_tac e) blast 722 723lemma prod_induct6 [case_names fields, induct type]: 724 "(\<And>a b c d e f. P (a, b, c, d, e, f)) \<Longrightarrow> P x" 725 by (cases x) blast 726 727lemma prod_cases7 [cases type]: 728 obtains (fields) a b c d e f g where "y = (a, b, c, d, e, f, g)" 729 by (cases y, case_tac f) blast 730 731lemma prod_induct7 [case_names fields, induct type]: 732 "(\<And>a b c d e f g. P (a, b, c, d, e, f, g)) \<Longrightarrow> P x" 733 by (cases x) blast 734 735definition internal_case_prod :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" 736 where "internal_case_prod \<equiv> case_prod" 737 738lemma internal_case_prod_conv: "internal_case_prod c (a, b) = c a b" 739 by (simp only: internal_case_prod_def case_prod_conv) 740 741ML_file "Tools/split_rule.ML" 742 743hide_const internal_case_prod 744 745 746subsubsection \<open>Derived operations\<close> 747 748definition curry :: "('a \<times> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'c" 749 where "curry = (\<lambda>c x y. c (x, y))" 750 751lemma curry_conv [simp, code]: "curry f a b = f (a, b)" 752 by (simp add: curry_def) 753 754lemma curryI [intro!]: "f (a, b) \<Longrightarrow> curry f a b" 755 by (simp add: curry_def) 756 757lemma curryD [dest!]: "curry f a b \<Longrightarrow> f (a, b)" 758 by (simp add: curry_def) 759 760lemma curryE: "curry f a b \<Longrightarrow> (f (a, b) \<Longrightarrow> Q) \<Longrightarrow> Q" 761 by (simp add: curry_def) 762 763lemma curry_case_prod [simp]: "curry (case_prod f) = f" 764 by (simp add: curry_def case_prod_unfold) 765 766lemma case_prod_curry [simp]: "case_prod (curry f) = f" 767 by (simp add: curry_def case_prod_unfold) 768 769lemma curry_K: "curry (\<lambda>x. c) = (\<lambda>x y. c)" 770 by (simp add: fun_eq_iff) 771 772text \<open>The composition-uncurry combinator.\<close> 773 774notation fcomp (infixl "\<circ>>" 60) 775 776definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60) 777 where "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))" 778 779lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))" 780 by (simp add: fun_eq_iff scomp_def case_prod_unfold) 781 782lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = case_prod g (f x)" 783 by (simp add: scomp_unfold case_prod_unfold) 784 785lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x" 786 by (simp add: fun_eq_iff) 787 788lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x" 789 by (simp add: fun_eq_iff) 790 791lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)" 792 by (simp add: fun_eq_iff scomp_unfold) 793 794lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)" 795 by (simp add: fun_eq_iff scomp_unfold fcomp_def) 796 797lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)" 798 by (simp add: fun_eq_iff scomp_unfold) 799 800code_printing 801 constant scomp \<rightharpoonup> (Eval) infixl 3 "#->" 802 803no_notation fcomp (infixl "\<circ>>" 60) 804no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 805 806text \<open> 807 @{term map_prod} --- action of the product functor upon functions. 808\<close> 809 810definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" 811 where "map_prod f g = (\<lambda>(x, y). (f x, g y))" 812 813lemma map_prod_simp [simp, code]: "map_prod f g (a, b) = (f a, g b)" 814 by (simp add: map_prod_def) 815 816functor map_prod: map_prod 817 by (auto simp add: split_paired_all) 818 819lemma fst_map_prod [simp]: "fst (map_prod f g x) = f (fst x)" 820 by (cases x) simp_all 821 822lemma snd_map_prod [simp]: "snd (map_prod f g x) = g (snd x)" 823 by (cases x) simp_all 824 825lemma fst_comp_map_prod [simp]: "fst \<circ> map_prod f g = f \<circ> fst" 826 by (rule ext) simp_all 827 828lemma snd_comp_map_prod [simp]: "snd \<circ> map_prod f g = g \<circ> snd" 829 by (rule ext) simp_all 830 831lemma map_prod_compose: "map_prod (f1 \<circ> f2) (g1 \<circ> g2) = (map_prod f1 g1 \<circ> map_prod f2 g2)" 832 by (rule ext) (simp add: map_prod.compositionality comp_def) 833 834lemma map_prod_ident [simp]: "map_prod (\<lambda>x. x) (\<lambda>y. y) = (\<lambda>z. z)" 835 by (rule ext) (simp add: map_prod.identity) 836 837lemma map_prod_imageI [intro]: "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R" 838 by (rule image_eqI) simp_all 839 840lemma prod_fun_imageE [elim!]: 841 assumes major: "c \<in> map_prod f g ` R" 842 and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P" 843 shows P 844 apply (rule major [THEN imageE]) 845 apply (case_tac x) 846 apply (rule cases) 847 apply simp_all 848 done 849 850definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" 851 where "apfst f = map_prod f id" 852 853definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" 854 where "apsnd f = map_prod id f" 855 856lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" 857 by (simp add: apfst_def) 858 859lemma apsnd_conv [simp, code]: "apsnd f (x, y) = (x, f y)" 860 by (simp add: apsnd_def) 861 862lemma fst_apfst [simp]: "fst (apfst f x) = f (fst x)" 863 by (cases x) simp 864 865lemma fst_comp_apfst [simp]: "fst \<circ> apfst f = f \<circ> fst" 866 by (simp add: fun_eq_iff) 867 868lemma fst_apsnd [simp]: "fst (apsnd f x) = fst x" 869 by (cases x) simp 870 871lemma fst_comp_apsnd [simp]: "fst \<circ> apsnd f = fst" 872 by (simp add: fun_eq_iff) 873 874lemma snd_apfst [simp]: "snd (apfst f x) = snd x" 875 by (cases x) simp 876 877lemma snd_comp_apfst [simp]: "snd \<circ> apfst f = snd" 878 by (simp add: fun_eq_iff) 879 880lemma snd_apsnd [simp]: "snd (apsnd f x) = f (snd x)" 881 by (cases x) simp 882 883lemma snd_comp_apsnd [simp]: "snd \<circ> apsnd f = f \<circ> snd" 884 by (simp add: fun_eq_iff) 885 886lemma apfst_compose: "apfst f (apfst g x) = apfst (f \<circ> g) x" 887 by (cases x) simp 888 889lemma apsnd_compose: "apsnd f (apsnd g x) = apsnd (f \<circ> g) x" 890 by (cases x) simp 891 892lemma apfst_apsnd [simp]: "apfst f (apsnd g x) = (f (fst x), g (snd x))" 893 by (cases x) simp 894 895lemma apsnd_apfst [simp]: "apsnd f (apfst g x) = (g (fst x), f (snd x))" 896 by (cases x) simp 897 898lemma apfst_id [simp]: "apfst id = id" 899 by (simp add: fun_eq_iff) 900 901lemma apsnd_id [simp]: "apsnd id = id" 902 by (simp add: fun_eq_iff) 903 904lemma apfst_eq_conv [simp]: "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)" 905 by (cases x) simp 906 907lemma apsnd_eq_conv [simp]: "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)" 908 by (cases x) simp 909 910lemma apsnd_apfst_commute: "apsnd f (apfst g p) = apfst g (apsnd f p)" 911 by simp 912 913context 914begin 915 916local_setup \<open>Local_Theory.map_background_naming (Name_Space.mandatory_path "prod")\<close> 917 918definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a" 919 where "swap p = (snd p, fst p)" 920 921end 922 923lemma swap_simp [simp]: "prod.swap (x, y) = (y, x)" 924 by (simp add: prod.swap_def) 925 926lemma swap_swap [simp]: "prod.swap (prod.swap p) = p" 927 by (cases p) simp 928 929lemma swap_comp_swap [simp]: "prod.swap \<circ> prod.swap = id" 930 by (simp add: fun_eq_iff) 931 932lemma pair_in_swap_image [simp]: "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A" 933 by (auto intro!: image_eqI) 934 935lemma inj_swap [simp]: "inj_on prod.swap A" 936 by (rule inj_onI) auto 937 938lemma swap_inj_on: "inj_on (\<lambda>(i, j). (j, i)) A" 939 by (rule inj_onI) auto 940 941lemma surj_swap [simp]: "surj prod.swap" 942 by (rule surjI [of _ prod.swap]) simp 943 944lemma bij_swap [simp]: "bij prod.swap" 945 by (simp add: bij_def) 946 947lemma case_swap [simp]: "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)" 948 by (cases p) simp 949 950lemma fst_swap [simp]: "fst (prod.swap x) = snd x" 951 by (cases x) simp 952 953lemma snd_swap [simp]: "snd (prod.swap x) = fst x" 954 by (cases x) simp 955 956text \<open>Disjoint union of a family of sets -- Sigma.\<close> 957 958definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set" 959 where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}" 960 961abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr "\<times>" 80) 962 where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)" 963 964hide_const (open) Times 965 966bundle no_Set_Product_syntax begin 967no_notation Product_Type.Times (infixr "\<times>" 80) 968end 969bundle Set_Product_syntax begin 970notation Product_Type.Times (infixr "\<times>" 80) 971end 972 973syntax 974 "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) 975translations 976 "SIGMA x:A. B" \<rightleftharpoons> "CONST Sigma A (\<lambda>x. B)" 977 978lemma SigmaI [intro!]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> (a, b) \<in> Sigma A B" 979 unfolding Sigma_def by blast 980 981lemma SigmaE [elim!]: "c \<in> Sigma A B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> B x \<Longrightarrow> c = (x, y) \<Longrightarrow> P) \<Longrightarrow> P" 982 \<comment> \<open>The general elimination rule.\<close> 983 unfolding Sigma_def by blast 984 985text \<open> 986 Elimination of @{term "(a, b) \<in> A \<times> B"} -- introduces no 987 eigenvariables. 988\<close> 989 990lemma SigmaD1: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A" 991 by blast 992 993lemma SigmaD2: "(a, b) \<in> Sigma A B \<Longrightarrow> b \<in> B a" 994 by blast 995 996lemma SigmaE2: "(a, b) \<in> Sigma A B \<Longrightarrow> (a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> P) \<Longrightarrow> P" 997 by blast 998 999lemma Sigma_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (SIGMA x:A. C x) = (SIGMA x:B. D x)" 1000 by auto 1001 1002lemma Sigma_mono: "A \<subseteq> C \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> D x) \<Longrightarrow> Sigma A B \<subseteq> Sigma C D" 1003 by blast 1004 1005lemma Sigma_empty1 [simp]: "Sigma {} B = {}" 1006 by blast 1007 1008lemma Sigma_empty2 [simp]: "A \<times> {} = {}" 1009 by blast 1010 1011lemma UNIV_Times_UNIV [simp]: "UNIV \<times> UNIV = UNIV" 1012 by auto 1013 1014lemma Compl_Times_UNIV1 [simp]: "- (UNIV \<times> A) = UNIV \<times> (-A)" 1015 by auto 1016 1017lemma Compl_Times_UNIV2 [simp]: "- (A \<times> UNIV) = (-A) \<times> UNIV" 1018 by auto 1019 1020lemma mem_Sigma_iff [iff]: "(a, b) \<in> Sigma A B \<longleftrightarrow> a \<in> A \<and> b \<in> B a" 1021 by blast 1022 1023lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B" 1024 by (induct x) simp 1025 1026lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})" 1027 by auto 1028 1029lemma Times_subset_cancel2: "x \<in> C \<Longrightarrow> A \<times> C \<subseteq> B \<times> C \<longleftrightarrow> A \<subseteq> B" 1030 by blast 1031 1032lemma Times_eq_cancel2: "x \<in> C \<Longrightarrow> A \<times> C = B \<times> C \<longleftrightarrow> A = B" 1033 by (blast elim: equalityE) 1034 1035lemma Collect_case_prod_Sigma: "{(x, y). P x \<and> Q x y} = (SIGMA x:Collect P. Collect (Q x))" 1036 by blast 1037 1038lemma Collect_case_prod [simp]: "{(a, b). P a \<and> Q b} = Collect P \<times> Collect Q " 1039 by (fact Collect_case_prod_Sigma) 1040 1041lemma Collect_case_prodD: "x \<in> Collect (case_prod A) \<Longrightarrow> A (fst x) (snd x)" 1042 by auto 1043 1044lemma Collect_case_prod_mono: "A \<le> B \<Longrightarrow> Collect (case_prod A) \<subseteq> Collect (case_prod B)" 1045 by auto (auto elim!: le_funE) 1046 1047lemma Collect_split_mono_strong: 1048 "X = fst ` A \<Longrightarrow> Y = snd ` A \<Longrightarrow> \<forall>a\<in>X. \<forall>b \<in> Y. P a b \<longrightarrow> Q a b 1049 \<Longrightarrow> A \<subseteq> Collect (case_prod P) \<Longrightarrow> A \<subseteq> Collect (case_prod Q)" 1050 by fastforce 1051 1052lemma UN_Times_distrib: "(\<Union>(a, b)\<in>A \<times> B. E a \<times> F b) = UNION A E \<times> UNION B F" 1053 \<comment> \<open>Suggested by Pierre Chartier\<close> 1054 by blast 1055 1056lemma split_paired_Ball_Sigma [simp, no_atp]: "(\<forall>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B x. P (x, y))" 1057 by blast 1058 1059lemma split_paired_Bex_Sigma [simp, no_atp]: "(\<exists>z\<in>Sigma A B. P z) \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B x. P (x, y))" 1060 by blast 1061 1062lemma Sigma_Un_distrib1: "Sigma (I \<union> J) C = Sigma I C \<union> Sigma J C" 1063 by blast 1064 1065lemma Sigma_Un_distrib2: "(SIGMA i:I. A i \<union> B i) = Sigma I A \<union> Sigma I B" 1066 by blast 1067 1068lemma Sigma_Int_distrib1: "Sigma (I \<inter> J) C = Sigma I C \<inter> Sigma J C" 1069 by blast 1070 1071lemma Sigma_Int_distrib2: "(SIGMA i:I. A i \<inter> B i) = Sigma I A \<inter> Sigma I B" 1072 by blast 1073 1074lemma Sigma_Diff_distrib1: "Sigma (I - J) C = Sigma I C - Sigma J C" 1075 by blast 1076 1077lemma Sigma_Diff_distrib2: "(SIGMA i:I. A i - B i) = Sigma I A - Sigma I B" 1078 by blast 1079 1080lemma Sigma_Union: "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)" 1081 by blast 1082 1083lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})" 1084 by auto 1085 1086text \<open> 1087 Non-dependent versions are needed to avoid the need for higher-order 1088 matching, especially when the rules are re-oriented. 1089\<close> 1090 1091lemma Times_Un_distrib1: "(A \<union> B) \<times> C = A \<times> C \<union> B \<times> C " 1092 by (fact Sigma_Un_distrib1) 1093 1094lemma Times_Int_distrib1: "(A \<inter> B) \<times> C = A \<times> C \<inter> B \<times> C " 1095 by (fact Sigma_Int_distrib1) 1096 1097lemma Times_Diff_distrib1: "(A - B) \<times> C = A \<times> C - B \<times> C " 1098 by (fact Sigma_Diff_distrib1) 1099 1100lemma Times_empty [simp]: "A \<times> B = {} \<longleftrightarrow> A = {} \<or> B = {}" 1101 by auto 1102 1103lemma times_eq_iff: "A \<times> B = C \<times> D \<longleftrightarrow> A = C \<and> B = D \<or> (A = {} \<or> B = {}) \<and> (C = {} \<or> D = {})" 1104 by auto 1105 1106lemma fst_image_times [simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)" 1107 by force 1108 1109lemma snd_image_times [simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)" 1110 by force 1111 1112lemma fst_image_Sigma: "fst ` (Sigma A B) = {x \<in> A. B(x) \<noteq> {}}" 1113 by force 1114 1115lemma snd_image_Sigma: "snd ` (Sigma A B) = (\<Union> x \<in> A. B x)" 1116 by force 1117 1118lemma vimage_fst: "fst -` A = A \<times> UNIV" 1119 by auto 1120 1121lemma vimage_snd: "snd -` A = UNIV \<times> A" 1122 by auto 1123 1124lemma insert_times_insert [simp]: 1125 "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)" 1126 by blast 1127 1128lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B" 1129proof (rule set_eqI) 1130 show "x \<in> f -` (A \<times> B) \<longleftrightarrow> x \<in> (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B" for x 1131 by (cases "f x") (auto split: prod.split) 1132qed 1133 1134lemma times_Int_times: "A \<times> B \<inter> C \<times> D = (A \<inter> C) \<times> (B \<inter> D)" 1135 by auto 1136 1137lemma product_swap: "prod.swap ` (A \<times> B) = B \<times> A" 1138 by (auto simp add: set_eq_iff) 1139 1140lemma swap_product: "(\<lambda>(i, j). (j, i)) ` (A \<times> B) = B \<times> A" 1141 by (auto simp add: set_eq_iff) 1142 1143lemma image_split_eq_Sigma: "(\<lambda>x. (f x, g x)) ` A = Sigma (f ` A) (\<lambda>x. g ` (f -` {x} \<inter> A))" 1144proof (safe intro!: imageI) 1145 fix a b 1146 assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" 1147 show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" 1148 using * eq[symmetric] by auto 1149qed simp_all 1150 1151lemma subset_fst_snd: "A \<subseteq> (fst ` A \<times> snd ` A)" 1152 by force 1153 1154lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A" 1155 by (auto simp add: inj_on_def) 1156 1157lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f" 1158 using inj_on_apfst[of f UNIV] by simp 1159 1160lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A" 1161 by (auto simp add: inj_on_def) 1162 1163lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f" 1164 using inj_on_apsnd[of f UNIV] by simp 1165 1166context 1167begin 1168 1169qualified definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" 1170 where [code_abbrev]: "product A B = A \<times> B" 1171 1172lemma member_product: "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B" 1173 by (simp add: product_def) 1174 1175end 1176 1177text \<open>The following @{const map_prod} lemmas are due to Joachim Breitner:\<close> 1178 1179lemma map_prod_inj_on: 1180 assumes "inj_on f A" 1181 and "inj_on g B" 1182 shows "inj_on (map_prod f g) (A \<times> B)" 1183proof (rule inj_onI) 1184 fix x :: "'a \<times> 'c" 1185 fix y :: "'a \<times> 'c" 1186 assume "x \<in> A \<times> B" 1187 then have "fst x \<in> A" and "snd x \<in> B" by auto 1188 assume "y \<in> A \<times> B" 1189 then have "fst y \<in> A" and "snd y \<in> B" by auto 1190 assume "map_prod f g x = map_prod f g y" 1191 then have "fst (map_prod f g x) = fst (map_prod f g y)" by auto 1192 then have "f (fst x) = f (fst y)" by (cases x, cases y) auto 1193 with \<open>inj_on f A\<close> and \<open>fst x \<in> A\<close> and \<open>fst y \<in> A\<close> have "fst x = fst y" 1194 by (auto dest: inj_onD) 1195 moreover from \<open>map_prod f g x = map_prod f g y\<close> 1196 have "snd (map_prod f g x) = snd (map_prod f g y)" by auto 1197 then have "g (snd x) = g (snd y)" by (cases x, cases y) auto 1198 with \<open>inj_on g B\<close> and \<open>snd x \<in> B\<close> and \<open>snd y \<in> B\<close> have "snd x = snd y" 1199 by (auto dest: inj_onD) 1200 ultimately show "x = y" by (rule prod_eqI) 1201qed 1202 1203lemma map_prod_surj: 1204 fixes f :: "'a \<Rightarrow> 'b" 1205 and g :: "'c \<Rightarrow> 'd" 1206 assumes "surj f" and "surj g" 1207 shows "surj (map_prod f g)" 1208 unfolding surj_def 1209proof 1210 fix y :: "'b \<times> 'd" 1211 from \<open>surj f\<close> obtain a where "fst y = f a" 1212 by (auto elim: surjE) 1213 moreover 1214 from \<open>surj g\<close> obtain b where "snd y = g b" 1215 by (auto elim: surjE) 1216 ultimately have "(fst y, snd y) = map_prod f g (a,b)" 1217 by auto 1218 then show "\<exists>x. y = map_prod f g x" 1219 by auto 1220qed 1221 1222lemma map_prod_surj_on: 1223 assumes "f ` A = A'" and "g ` B = B'" 1224 shows "map_prod f g ` (A \<times> B) = A' \<times> B'" 1225 unfolding image_def 1226proof (rule set_eqI, rule iffI) 1227 fix x :: "'a \<times> 'c" 1228 assume "x \<in> {y::'a \<times> 'c. \<exists>x::'b \<times> 'd\<in>A \<times> B. y = map_prod f g x}" 1229 then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y" 1230 by blast 1231 from \<open>image f A = A'\<close> and \<open>y \<in> A \<times> B\<close> have "f (fst y) \<in> A'" 1232 by auto 1233 moreover from \<open>image g B = B'\<close> and \<open>y \<in> A \<times> B\<close> have "g (snd y) \<in> B'" 1234 by auto 1235 ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" 1236 by auto 1237 with \<open>x = map_prod f g y\<close> show "x \<in> A' \<times> B'" 1238 by (cases y) auto 1239next 1240 fix x :: "'a \<times> 'c" 1241 assume "x \<in> A' \<times> B'" 1242 then have "fst x \<in> A'" and "snd x \<in> B'" 1243 by auto 1244 from \<open>image f A = A'\<close> and \<open>fst x \<in> A'\<close> have "fst x \<in> image f A" 1245 by auto 1246 then obtain a where "a \<in> A" and "fst x = f a" 1247 by (rule imageE) 1248 moreover from \<open>image g B = B'\<close> and \<open>snd x \<in> B'\<close> obtain b where "b \<in> B" and "snd x = g b" 1249 by auto 1250 ultimately have "(fst x, snd x) = map_prod f g (a, b)" 1251 by auto 1252 moreover from \<open>a \<in> A\<close> and \<open>b \<in> B\<close> have "(a , b) \<in> A \<times> B" 1253 by auto 1254 ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y" 1255 by auto 1256 then show "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}" 1257 by auto 1258qed 1259 1260 1261subsection \<open>Simproc for rewriting a set comprehension into a pointfree expression\<close> 1262 1263ML_file "Tools/set_comprehension_pointfree.ML" 1264 1265setup \<open> 1266 Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs 1267 [Simplifier.make_simproc @{context} "set comprehension" 1268 {lhss = [@{term "Collect P"}], 1269 proc = K Set_Comprehension_Pointfree.code_simproc}]) 1270\<close> 1271 1272 1273subsection \<open>Inductively defined sets\<close> 1274 1275(* simplify {(x1, ..., xn). (x1, ..., xn) : S} to S *) 1276simproc_setup Collect_mem ("Collect t") = \<open> 1277 fn _ => fn ctxt => fn ct => 1278 (case Thm.term_of ct of 1279 S as Const (@{const_name Collect}, Type (@{type_name fun}, [_, T])) $ t => 1280 let val (u, _, ps) = HOLogic.strip_ptupleabs t in 1281 (case u of 1282 (c as Const (@{const_name Set.member}, _)) $ q $ S' => 1283 (case try (HOLogic.strip_ptuple ps) q of 1284 NONE => NONE 1285 | SOME ts => 1286 if not (Term.is_open S') andalso 1287 ts = map Bound (length ps downto 0) 1288 then 1289 let val simp = 1290 full_simp_tac (put_simpset HOL_basic_ss ctxt 1291 addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1 1292 in 1293 SOME (Goal.prove ctxt [] [] 1294 (Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S') 1295 (K (EVERY 1296 [resolve_tac ctxt [eq_reflection] 1, 1297 resolve_tac ctxt @{thms subset_antisym} 1, 1298 resolve_tac ctxt @{thms subsetI} 1, 1299 dresolve_tac ctxt @{thms CollectD} 1, simp, 1300 resolve_tac ctxt @{thms subsetI} 1, 1301 resolve_tac ctxt @{thms CollectI} 1, simp]))) 1302 end 1303 else NONE) 1304 | _ => NONE) 1305 end 1306 | _ => NONE) 1307\<close> 1308 1309ML_file "Tools/inductive_set.ML" 1310 1311 1312subsection \<open>Legacy theorem bindings and duplicates\<close> 1313 1314lemmas fst_conv = prod.sel(1) 1315lemmas snd_conv = prod.sel(2) 1316lemmas split_def = case_prod_unfold 1317lemmas split_beta' = case_prod_beta' 1318lemmas split_beta = prod.case_eq_if 1319lemmas split_conv = case_prod_conv 1320lemmas split = case_prod_conv 1321 1322hide_const (open) prod 1323 1324end 1325