src/HOL/Product_Type.thy
 changeset 37678 0040bafffdef parent 37591 d3daea901123 child 37704 c6161bee8486
```     1.1 --- a/src/HOL/Product_Type.thy	Thu Jul 01 16:54:42 2010 +0200
1.2 +++ b/src/HOL/Product_Type.thy	Thu Jul 01 16:54:44 2010 +0200
1.3 @@ -129,7 +129,7 @@
1.4  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
1.5    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
1.6
1.7 -typedef (prod) ('a, 'b) "*" (infixr "*" 20)
1.8 +typedef ('a, 'b) prod (infixr "*" 20)
1.9    = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
1.10  proof
1.11    fix a b show "Pair_Rep a b \<in> ?prod"
1.12 @@ -137,14 +137,14 @@
1.13  qed
1.14
1.15  type_notation (xsymbols)
1.16 -  "*"  ("(_ \<times>/ _)" [21, 20] 20)
1.17 +  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
1.18  type_notation (HTML output)
1.19 -  "*"  ("(_ \<times>/ _)" [21, 20] 20)
1.20 +  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
1.21
1.22  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
1.23    "Pair a b = Abs_prod (Pair_Rep a b)"
1.24
1.25 -rep_datatype (prod) Pair proof -
1.26 +rep_datatype Pair proof -
1.27    fix P :: "'a \<times> 'b \<Rightarrow> bool" and p
1.28    assume "\<And>a b. P (Pair a b)"
1.29    then show "P p" by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
1.30 @@ -263,7 +263,7 @@
1.31
1.32  subsubsection {* Code generator setup *}
1.33
1.34 -code_type *
1.35 +code_type prod
1.36    (SML infix 2 "*")
1.37    (OCaml infix 2 "*")
1.38    (Haskell "!((_),/ (_))")
1.39 @@ -275,19 +275,19 @@
1.40    (Haskell "!((_),/ (_))")
1.41    (Scala "!((_),/ (_))")
1.42
1.43 -code_instance * :: eq
1.44 +code_instance prod :: eq
1.46
1.47  code_const "eq_class.eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
1.48    (Haskell infixl 4 "==")
1.49
1.50  types_code
1.51 -  "*"     ("(_ */ _)")
1.52 +  "prod"     ("(_ */ _)")
1.53  attach (term_of) {*
1.54 -fun term_of_id_42 aF aT bF bT (x, y) = HOLogic.pair_const aT bT \$ aF x \$ bF y;
1.55 +fun term_of_prod aF aT bF bT (x, y) = HOLogic.pair_const aT bT \$ aF x \$ bF y;
1.56  *}
1.57  attach (test) {*
1.58 -fun gen_id_42 aG aT bG bT i =
1.59 +fun term_of_prod aG aT bG bT i =
1.60    let
1.61      val (x, t) = aG i;
1.62      val (y, u) = bG i
1.63 @@ -438,7 +438,7 @@
1.64
1.65  lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
1.66    -- {* Prevents simplification of @{term c}: much faster *}
1.67 -  by (erule arg_cong)
1.68 +  by (fact weak_case_cong)
1.69
1.70  lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
1.71    by (simp add: split_eta)
1.72 @@ -689,19 +689,18 @@
1.73  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
1.74
1.75  lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
1.76 -  by auto
1.77 +  by (fact splitI2)
1.78
1.79  lemma prod_caseI2': "!!p. [| !!a b. (a, b) = p ==> c a b x |] ==> prod_case c p x"
1.80 -  by (auto simp: split_tupled_all)
1.81 +  by (fact splitI2')
1.82
1.83  lemma prod_caseE: "prod_case c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
1.84 -  by (induct p) auto
1.85 +  by (fact splitE)
1.86
1.87  lemma prod_caseE': "prod_case c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
1.88 -  by (induct p) auto
1.89 +  by (fact splitE')
1.90
1.91 -declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
1.92 -declare prod_caseE' [elim!] prod_caseE [elim!]
1.93 +declare prod_caseI [intro!]
1.94
1.95  lemma prod_case_beta:
1.96    "prod_case f p = f (fst p) (snd p)"
1.97 @@ -795,8 +794,11 @@
1.98  definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "o\<rightarrow>" 60) where
1.99    "f o\<rightarrow> g = (\<lambda>x. split g (f x))"
1.100
1.101 +lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
1.102 +  by (simp add: expand_fun_eq scomp_def split_def)
1.103 +
1.104  lemma scomp_apply:  "(f o\<rightarrow> g) x = split g (f x)"
1.105 -  by (simp add: scomp_def)
1.106 +  by (simp add: scomp_unfold split_def)
1.107
1.108  lemma Pair_scomp: "Pair x o\<rightarrow> f = f x"
1.109    by (simp add: expand_fun_eq scomp_apply)
1.110 @@ -805,13 +807,13 @@
1.111    by (simp add: expand_fun_eq scomp_apply)
1.112
1.113  lemma scomp_scomp: "(f o\<rightarrow> g) o\<rightarrow> h = f o\<rightarrow> (\<lambda>x. g x o\<rightarrow> h)"
1.114 -  by (simp add: expand_fun_eq split_twice scomp_def)
1.115 +  by (simp add: expand_fun_eq scomp_unfold)
1.116
1.117  lemma scomp_fcomp: "(f o\<rightarrow> g) o> h = f o\<rightarrow> (\<lambda>x. g x o> h)"
1.118 -  by (simp add: expand_fun_eq scomp_apply fcomp_def split_def)
1.119 +  by (simp add: expand_fun_eq scomp_unfold fcomp_def)
1.120
1.121  lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
1.122 -  by (simp add: expand_fun_eq scomp_apply fcomp_apply)
1.123 +  by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
1.124
1.125  code_const scomp
1.126    (Eval infixl 3 "#->")
```