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.45    (Haskell -)
    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 "#->")