# HG changeset patch # User haftmann # Date 1206011094 -3600 # Node ID d6a508c1690874f3a82bda1f84a4cf684c1c05bf # Parent 19b153ebda0b274d85a24b16575a4d63c503623b Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned diff -r 19b153ebda0b -r d6a508c16908 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Mar 20 12:04:53 2008 +0100 +++ b/src/HOL/Product_Type.thy Thu Mar 20 12:04:54 2008 +0100 @@ -36,6 +36,7 @@ code_instance bool :: eq (Haskell -) + subsection {* Unit *} typedef unit = "{True}" @@ -88,22 +89,53 @@ by (rule ext) simp +text {* code generator setup *} + +instance unit :: eq .. + +lemma [code func]: + "(u\unit) = v \ True" unfolding unit_eq [of u] unit_eq [of v] by rule+ + +code_type unit + (SML "unit") + (OCaml "unit") + (Haskell "()") + +code_instance unit :: eq + (Haskell -) + +code_const "op = \ unit \ unit \ bool" + (Haskell infixl 4 "==") + +code_const Unity + (SML "()") + (OCaml "()") + (Haskell "()") + +code_reserved SML + unit + +code_reserved OCaml + unit + + subsection {* Pairs *} -subsubsection {* Type definition *} +subsubsection {* Product type, basic operations and concrete syntax *} -constdefs - Pair_Rep :: "['a, 'b] => ['a, 'b] => bool" - "Pair_Rep == (%a b. %x y. x=a & y=b)" +definition + Pair_Rep :: "'a \ 'b \ 'a \ 'b \ bool" +where + "Pair_Rep a b = (\x y. x = a \ y = b)" global typedef (Prod) ('a, 'b) "*" (infixr "*" 20) - = "{f. EX a b. f = Pair_Rep (a::'a) (b::'b)}" + = "{f. \a b. f = Pair_Rep (a\'a) (b\'b)}" proof - fix a b show "Pair_Rep a b : ?Prod" - by blast + fix a b show "Pair_Rep a b \ ?Prod" + by rule+ qed syntax (xsymbols) @@ -111,20 +143,12 @@ syntax (HTML output) "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) -local - -subsubsection {* Definitions *} - -global - consts - fst :: "'a * 'b => 'a" - snd :: "'a * 'b => 'b" - split :: "[['a, 'b] => 'c, 'a * 'b] => 'c" - curry :: "['a * 'b => 'c, 'a, 'b] => 'c" - prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd" - Pair :: "['a, 'b] => 'a * 'b" - Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set" + Pair :: "'a \ 'b \ 'a \ 'b" + fst :: "'a \ 'b \ 'a" + snd :: "'a \ 'b \ 'b" + split :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" + curry :: "('a \ 'b \ 'c) \ 'a \ 'b \ 'c" local @@ -134,22 +158,6 @@ snd_def: "snd p == THE b. EX a. p = Pair a b" split_def: "split == (%c p. c (fst p) (snd p))" curry_def: "curry == (%c x y. c (Pair x y))" - prod_fun_def: "prod_fun f g == split (%x y. Pair (f x) (g y))" - Sigma_def [code func]: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" - -abbreviation - Times :: "['a set, 'b set] => ('a * 'b) set" - (infixr "<*>" 80) where - "A <*> B == Sigma A (%_. B)" - -notation (xsymbols) - Times (infixr "\" 80) - -notation (HTML output) - Times (infixr "\" 80) - - -subsubsection {* Concrete syntax *} text {* Patterns -- extends pre-defined type @{typ pttrn} used in @@ -166,7 +174,6 @@ "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')") "" :: "pttrn => patterns" ("_") "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _") - "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) translations "(x, y)" == "Pair x y" @@ -176,7 +183,6 @@ "_abs (Pair x y) t" => "%(x,y).t" (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) - "SIGMA x:A. B" == "Sigma A (%x. B)" (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*) (* works best with enclosing "let", if "let" does not avoid eta-contraction *) @@ -232,15 +238,29 @@ *} -subsubsection {* Lemmas and proof tool setup *} +text {* Towards a datatype declaration *} -lemma ProdI: "Pair_Rep a b : Prod" - unfolding Prod_def by blast +lemma surj_pair [simp]: "EX x y. p = (x, y)" + apply (unfold Pair_def) + apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) + apply (erule exE, erule exE, rule exI, rule exI) + apply (rule Rep_Prod_inverse [symmetric, THEN trans]) + apply (erule arg_cong) + done -lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' ==> a = a' & b = b'" - apply (unfold Pair_Rep_def) - apply (drule fun_cong [THEN fun_cong], blast) - done +lemma PairE [cases type: *]: + obtains x y where "p = (x, y)" + using surj_pair [of p] by blast + + +lemma prod_induct [induct type: *]: "(\a b. P (a, b)) \ P x" + by (cases x) simp + +lemma ProdI: "Pair_Rep a b \ Prod" + unfolding Prod_def by rule+ + +lemma Pair_Rep_inject: "Pair_Rep a b = Pair_Rep a' b' \ a = a' \ b = b'" + unfolding Pair_Rep_def by (drule fun_cong, drule fun_cong) blast lemma inj_on_Abs_Prod: "inj_on Abs_Prod Prod" apply (rule inj_on_inverseI) @@ -265,42 +285,23 @@ lemma snd_conv [simp, code]: "snd (a, b) = b" unfolding snd_def by blast +rep_datatype prod + inject Pair_eq + induction prod_induct + + +subsubsection {* Basic rules and proof tools *} + lemma fst_eqD: "fst (x, y) = a ==> x = a" by simp lemma snd_eqD: "snd (x, y) = a ==> y = a" by simp -lemma PairE_lemma: "EX x y. p = (x, y)" - apply (unfold Pair_def) - apply (rule Rep_Prod [unfolded Prod_def, THEN CollectE]) - apply (erule exE, erule exE, rule exI, rule exI) - apply (rule Rep_Prod_inverse [symmetric, THEN trans]) - apply (erule arg_cong) - done - -lemma PairE [cases type: *]: "(!!x y. p = (x, y) ==> Q) ==> Q" - using PairE_lemma [of p] by blast - -ML {* - local val PairE = thm "PairE" in - fun pair_tac s = - EVERY' [res_inst_tac [("p", s)] PairE, hyp_subst_tac, K prune_params_tac]; - end; -*} - -lemma surjective_pairing: "p = (fst p, snd p)" - -- {* Do not add as rewrite rule: invalidates some proofs in IMP *} +lemma pair_collapse [simp]: "(fst p, snd p) = p" by (cases p) simp -lemmas pair_collapse = surjective_pairing [symmetric] -declare pair_collapse [simp] - -lemma surj_pair [simp]: "EX x y. z = (x, y)" - apply (rule exI) - apply (rule exI) - apply (rule surjective_pairing) - done +lemmas surjective_pairing = pair_collapse [symmetric] lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))" proof @@ -313,8 +314,6 @@ from `PROP P (fst x, snd x)` show "PROP P x" by simp qed -lemmas split_tupled_all = split_paired_all unit_all_eq2 - text {* The rule @{thm [source] split_paired_all} does not work with the Simplifier because it also affects premises in congrence rules, @@ -322,7 +321,9 @@ ?P(a, b)"} which cannot be solved by reflexivity. *} -ML {* +lemmas split_tupled_all = split_paired_all unit_all_eq2 + +ML_setup {* (* replace parameters of product type by individual component parameters *) val safe_full_simp_tac = generic_simp_tac true (true, false, false); local (* filtering with exists_paired_all is an essential optimization *) @@ -352,71 +353,71 @@ -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} by fast +lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" + by fast + +lemma Pair_fst_snd_eq: "s = t \ fst s = fst t \ snd s = snd t" + by (cases s, cases t) simp + +lemma prod_eqI [intro?]: "fst p = fst q \ snd p = snd q \ p = q" + by (simp add: Pair_fst_snd_eq) + + +subsubsection {* @{text split} and @{text curry} *} + +lemma split_conv [simp, code func]: "split f (a, b) = f a b" + by (simp add: split_def) + +lemma curry_conv [simp, code func]: "curry f a b = f (a, b)" + by (simp add: curry_def) + +lemmas split = split_conv -- {* for backwards compatibility *} + +lemma splitI: "f a b \ split f (a, b)" + by (rule split_conv [THEN iffD2]) + +lemma splitD: "split f (a, b) \ f a b" + by (rule split_conv [THEN iffD1]) + +lemma curryI [intro!]: "f (a, b) \ curry f a b" + by (simp add: curry_def) + +lemma curryD [dest!]: "curry f a b \ f (a, b)" + by (simp add: curry_def) + +lemma curryE: "curry f a b \ (f (a, b) \ Q) \ Q" + by (simp add: curry_def) + lemma curry_split [simp]: "curry (split f) = f" by (simp add: curry_def split_def) lemma split_curry [simp]: "split (curry f) = f" by (simp add: curry_def split_def) -lemma curryI [intro!]: "f (a,b) ==> curry f a b" - by (simp add: curry_def) - -lemma curryD [dest!]: "curry f a b ==> f (a,b)" - by (simp add: curry_def) - -lemma curryE: "[| curry f a b ; f (a,b) ==> Q |] ==> Q" - by (simp add: curry_def) - -lemma curry_conv [simp, code func]: "curry f a b = f (a,b)" - by (simp add: curry_def) - -lemma prod_induct [induct type: *]: "!!x. (!!a b. P (a, b)) ==> P x" - by fast +lemma split_Pair [simp]: "(\(x, y). (x, y)) = id" + by (simp add: split_def id_def) -rep_datatype prod - inject Pair_eq - induction prod_induct - -lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))" - by fast - -lemma split_conv [simp, code func]: "split c (a, b) = c a b" - by (simp add: split_def) +lemma split_eta: "(\(x, y). f (x, y)) = f" + -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} + by (rule ext) auto -lemmas split = split_conv -- {* for backwards compatibility *} - -lemmas splitI = split_conv [THEN iffD2, standard] -lemmas splitD = split_conv [THEN iffD1, standard] +lemma split_comp: "split (f \ g) x = f (g (fst x)) (snd x)" + by (cases x) simp -lemma split_Pair_apply: "split (%x y. f (x, y)) = f" - -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} - apply (rule ext) - apply (tactic {* pair_tac "x" 1 *}, simp) - done +lemma split_twice: "split f (split g p) = split (\x y. split f (g x y)) p" + unfolding split_def .. lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))" -- {* Can't be added to simpset: loops! *} - by (simp add: split_Pair_apply) + by (simp add: split_eta) lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))" by (simp add: split_def) -lemma Pair_fst_snd_eq: "!!s t. (s = t) = (fst s = fst t & snd s = snd t)" -by (simp only: split_tupled_all, simp) - -lemma prod_eqI [intro?]: "fst p = fst q ==> snd p = snd q ==> p = q" - by (simp add: Pair_fst_snd_eq) - -lemma split_weak_cong: "p = q ==> split c p = split c q" +lemma split_weak_cong: "p = q \ split c p = split c q" -- {* Prevents simplification of @{term c}: much faster *} by (erule arg_cong) -lemma split_eta: "(%(x, y). f (x, y)) = f" - apply (rule ext) - apply (simp only: split_tupled_all) - apply (rule split_conv) - done - lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g" by (simp add: split_eta) @@ -425,7 +426,8 @@ @{thm [source] split_eta} as a rewrite rule is not general enough, and using @{thm [source] cond_split_eta} directly would render some existing proofs very inefficient; similarly for @{text - split_beta}. *} + split_beta}. +*} ML_setup {* @@ -581,6 +583,11 @@ shows "(%u. f (g (fst u)) (snd u)) = (split (%x. f (g x)))" by (rule ext) auto +lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" + apply (rule_tac x = "(a, b)" in image_eqI) + apply auto + done + lemma The_split_eq [simp]: "(THE (x',y'). x = x' & y = y') = (x, y)" by blast @@ -597,192 +604,6 @@ qed "The_split_eq"; *) -lemma injective_fst_snd: "!!x y. [|fst x = fst y; snd x = snd y|] ==> x = y" - by auto - - -text {* - \bigskip @{term prod_fun} --- action of the product functor upon - functions. -*} - -lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)" - by (simp add: prod_fun_def) - -lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" - apply (rule ext) - apply (tactic {* pair_tac "x" 1 *}, simp) - done - -lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" - apply (rule ext) - apply (tactic {* pair_tac "z" 1 *}, simp) - done - -lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" - apply (rule image_eqI) - apply (rule prod_fun [symmetric], assumption) - done - -lemma prod_fun_imageE [elim!]: - assumes major: "c: (prod_fun f g)`r" - and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P" - shows P - apply (rule major [THEN imageE]) - apply (rule_tac p = x in PairE) - apply (rule cases) - apply (blast intro: prod_fun) - apply blast - done - - -definition - upd_fst :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" -where - [code func del]: "upd_fst f = prod_fun f id" - -definition - upd_snd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" -where - [code func del]: "upd_snd f = prod_fun id f" - -lemma upd_fst_conv [simp, code]: - "upd_fst f (x, y) = (f x, y)" - by (simp add: upd_fst_def) - -lemma upd_snd_conv [simp, code]: - "upd_snd f (x, y) = (x, f y)" - by (simp add: upd_snd_def) - -text {* - \bigskip Disjoint union of a family of sets -- Sigma. -*} - -lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" - by (unfold Sigma_def) blast - -lemma SigmaE [elim!]: - "[| c: Sigma A B; - !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P - |] ==> P" - -- {* The general elimination rule. *} - by (unfold Sigma_def) blast - -text {* - Elimination of @{term "(a, b) : A \ B"} -- introduces no - eigenvariables. -*} - -lemma SigmaD1: "(a, b) : Sigma A B ==> a : A" - by blast - -lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a" - by blast - -lemma SigmaE2: - "[| (a, b) : Sigma A B; - [| a:A; b:B(a) |] ==> P - |] ==> P" - by blast - -lemma Sigma_cong: - "\A = B; !!x. x \ B \ C x = D x\ - \ (SIGMA x: A. C x) = (SIGMA x: B. D x)" - by auto - -lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D" - by blast - -lemma Sigma_empty1 [simp]: "Sigma {} B = {}" - by blast - -lemma Sigma_empty2 [simp]: "A <*> {} = {}" - by blast - -lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV" - by auto - -lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)" - by auto - -lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV" - by auto - -lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))" - by blast - -lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)" - by blast - -lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)" - by (blast elim: equalityE) - -lemma SetCompr_Sigma_eq: - "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))" - by blast - -text {* - \bigskip Complex rules for Sigma. -*} - -lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q" - by blast - -lemma UN_Times_distrib: - "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" - -- {* Suggested by Pierre Chartier *} - by blast - -lemma split_paired_Ball_Sigma [simp,noatp]: - "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" - by blast - -lemma split_paired_Bex_Sigma [simp,noatp]: - "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" - by blast - -lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" - by blast - -lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))" - by blast - -lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))" - by blast - -lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))" - by blast - -lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))" - by blast - -lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))" - by blast - -lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)" - by blast - -text {* - Non-dependent versions are needed to avoid the need for higher-order - matching, especially when the rules are re-oriented. -*} - -lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" - by blast - -lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" - by blast - -lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" - by blast - - -lemma pair_imageI [intro]: "(a, b) : A ==> f a b : (%(a, b). f a b) ` A" - apply (rule_tac x = "(a, b)" in image_eqI) - apply auto - done - - text {* Setup of internal @{text split_rule}. *} @@ -800,8 +621,6 @@ use "Tools/split_rule.ML" setup SplitRule.setup - - lemmas prod_caseI = prod.cases [THEN iffD2, standard] lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p" @@ -874,45 +693,234 @@ by (cases x) blast -subsection {* Further lemmas *} +subsubsection {* Derived operations *} + +text {* + The composition-uncurry combinator. +*} + +definition + mbind :: "('a \ 'b \ 'c) \ ('b \ 'c \ 'd) \ 'a \ 'd" (infixl "o->" 60) +where + "f o-> g = (\x. split g (f x))" + +notation (xsymbols) + mbind (infixl "\\" 60) + +notation (HTML output) + mbind (infixl "\\" 60) + +lemma mbind_apply: "(f \\ g) x = split g (f x)" + by (simp add: mbind_def) + +lemma Pair_mbind: "Pair x \\ f = f x" + by (simp add: expand_fun_eq mbind_apply) + +lemma mbind_Pair: "x \\ Pair = x" + by (simp add: expand_fun_eq mbind_apply) + +lemma mbind_mbind: "(f \\ g) \\ h = f \\ (\x. g x \\ h)" + by (simp add: expand_fun_eq split_twice mbind_def) + +lemma mbind_fcomp: "(f \\ g) \> h = f \\ (\x. g x \> h)" + by (simp add: expand_fun_eq mbind_apply fcomp_def split_def) + +lemma fcomp_mbind: "(f \> g) \\ h = f \> (g \\ h)" + by (simp add: expand_fun_eq mbind_apply fcomp_apply) + + +text {* + @{term prod_fun} --- action of the product functor upon + functions. +*} -lemma - split_Pair: "split Pair x = x" - unfolding split_def by auto +definition prod_fun :: "('a \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where + [code func del]: "prod_fun f g = (\(x, y). (f x, g y))" + +lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)" + by (simp add: prod_fun_def) + +lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)" + by (rule ext) auto + +lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)" + by (rule ext) auto + +lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r" + apply (rule image_eqI) + apply (rule prod_fun [symmetric], assumption) + done -lemma - split_comp: "split (f \ g) x = f (g (fst x)) (snd x)" - by (cases x, simp) +lemma prod_fun_imageE [elim!]: + assumes major: "c: (prod_fun f g)`r" + and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P" + shows P + apply (rule major [THEN imageE]) + apply (rule_tac p = x in PairE) + apply (rule cases) + apply (blast intro: prod_fun) + apply blast + done + +definition + apfst :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" +where + [code func del]: "apfst f = prod_fun f id" + +definition + apsnd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" +where + [code func del]: "apsnd f = prod_fun id f" + +lemma apfst_conv [simp, code]: + "apfst f (x, y) = (f x, y)" + by (simp add: apfst_def) + +lemma upd_snd_conv [simp, code]: + "apsnd f (x, y) = (x, f y)" + by (simp add: apsnd_def) -subsection {* Code generator setup *} +text {* + Disjoint union of a family of sets -- Sigma. +*} + +definition Sigma :: "['a set, 'a => 'b set] => ('a \ 'b) set" where + Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}" + +abbreviation + Times :: "['a set, 'b set] => ('a * 'b) set" + (infixr "<*>" 80) where + "A <*> B == Sigma A (%_. B)" + +notation (xsymbols) + Times (infixr "\" 80) -instance unit :: eq .. +notation (HTML output) + Times (infixr "\" 80) + +syntax + "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10) + +translations + "SIGMA x:A. B" == "Product_Type.Sigma A (%x. B)" + +lemma SigmaI [intro!]: "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B" + by (unfold Sigma_def) blast + +lemma SigmaE [elim!]: + "[| c: Sigma A B; + !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P + |] ==> P" + -- {* The general elimination rule. *} + by (unfold Sigma_def) blast -lemma [code func]: - "(u\unit) = v \ True" unfolding unit_eq [of u] unit_eq [of v] by rule+ +text {* + Elimination of @{term "(a, b) : A \ B"} -- introduces no + eigenvariables. +*} + +lemma SigmaD1: "(a, b) : Sigma A B ==> a : A" + by blast + +lemma SigmaD2: "(a, b) : Sigma A B ==> b : B a" + by blast + +lemma SigmaE2: + "[| (a, b) : Sigma A B; + [| a:A; b:B(a) |] ==> P + |] ==> P" + by blast -code_type unit - (SML "unit") - (OCaml "unit") - (Haskell "()") +lemma Sigma_cong: + "\A = B; !!x. x \ B \ C x = D x\ + \ (SIGMA x: A. C x) = (SIGMA x: B. D x)" + by auto + +lemma Sigma_mono: "[| A <= C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D" + by blast + +lemma Sigma_empty1 [simp]: "Sigma {} B = {}" + by blast + +lemma Sigma_empty2 [simp]: "A <*> {} = {}" + by blast + +lemma UNIV_Times_UNIV [simp]: "UNIV <*> UNIV = UNIV" + by auto -code_instance unit :: eq - (Haskell -) +lemma Compl_Times_UNIV1 [simp]: "- (UNIV <*> A) = UNIV <*> (-A)" + by auto + +lemma Compl_Times_UNIV2 [simp]: "- (A <*> UNIV) = (-A) <*> UNIV" + by auto + +lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))" + by blast + +lemma Times_subset_cancel2: "x:C ==> (A <*> C <= B <*> C) = (A <= B)" + by blast + +lemma Times_eq_cancel2: "x:C ==> (A <*> C = B <*> C) = (A = B)" + by (blast elim: equalityE) -code_const "op = \ unit \ unit \ bool" - (Haskell infixl 4 "==") +lemma SetCompr_Sigma_eq: + "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))" + by blast + +lemma Collect_split [simp]: "{(a,b). P a & Q b} = Collect P <*> Collect Q" + by blast + +lemma UN_Times_distrib: + "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)" + -- {* Suggested by Pierre Chartier *} + by blast + +lemma split_paired_Ball_Sigma [simp,noatp]: + "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))" + by blast + +lemma split_paired_Bex_Sigma [simp,noatp]: + "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))" + by blast -code_const Unity - (SML "()") - (OCaml "()") - (Haskell "()") +lemma Sigma_Un_distrib1: "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))" + by blast + +lemma Sigma_Un_distrib2: "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))" + by blast + +lemma Sigma_Int_distrib1: "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))" + by blast + +lemma Sigma_Int_distrib2: "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))" + by blast + +lemma Sigma_Diff_distrib1: "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))" + by blast + +lemma Sigma_Diff_distrib2: "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))" + by blast -code_reserved SML - unit +lemma Sigma_Union: "Sigma (Union X) B = (UN A:X. Sigma A B)" + by blast + +text {* + Non-dependent versions are needed to avoid the need for higher-order + matching, especially when the rules are re-oriented. +*} -code_reserved OCaml - unit +lemma Times_Un_distrib1: "(A Un B) <*> C = (A <*> C) Un (B <*> C)" + by blast + +lemma Times_Int_distrib1: "(A Int B) <*> C = (A <*> C) Int (B <*> C)" + by blast + +lemma Times_Diff_distrib1: "(A - B) <*> C = (A <*> C) - (B <*> C)" + by blast + + +subsubsection {* Code generator setup *} instance * :: (eq, eq) eq .. @@ -1044,12 +1052,10 @@ val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2"; val PairE = thm "PairE"; -val PairE_lemma = thm "PairE_lemma"; val Pair_Rep_inject = thm "Pair_Rep_inject"; val Pair_def = thm "Pair_def"; val Pair_eq = thm "Pair_eq"; val Pair_fst_snd_eq = thm "Pair_fst_snd_eq"; -val Pair_inject = thm "Pair_inject"; val ProdI = thm "ProdI"; val SetCompr_Sigma_eq = thm "SetCompr_Sigma_eq"; val SigmaD1 = thm "SigmaD1"; @@ -1084,7 +1090,6 @@ val fst_def = thm "fst_def"; val fst_eqD = thm "fst_eqD"; val inj_on_Abs_Prod = thm "inj_on_Abs_Prod"; -val injective_fst_snd = thm "injective_fst_snd"; val mem_Sigma_iff = thm "mem_Sigma_iff"; val mem_splitE = thm "mem_splitE"; val mem_splitI = thm "mem_splitI"; @@ -1109,7 +1114,6 @@ val splitI = thm "splitI"; val splitI2 = thm "splitI2"; val splitI2' = thm "splitI2'"; -val split_Pair_apply = thm "split_Pair_apply"; val split_beta = thm "split_beta"; val split_conv = thm "split_conv"; val split_def = thm "split_def"; @@ -1133,7 +1137,6 @@ val unit_all_eq1 = thm "unit_all_eq1"; val unit_all_eq2 = thm "unit_all_eq2"; val unit_eq = thm "unit_eq"; -val unit_induct = thm "unit_induct"; *}