src/HOL/Record.thy
changeset 13412 666137b488a4
parent 11956 b814360b0267
child 13421 8fcdf4a26468
     1.1 --- a/src/HOL/Record.thy	Wed Jul 24 00:09:44 2002 +0200
     1.2 +++ b/src/HOL/Record.thy	Wed Jul 24 00:10:52 2002 +0200
     1.3 @@ -11,118 +11,57 @@
     1.4  
     1.5  subsection {* Abstract product types *}
     1.6  
     1.7 -constdefs
     1.8 -  product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
     1.9 -    ('a => 'b => 'p) => ('p => 'a) => ('p => 'b) => bool"
    1.10 -  "product_type Rep Abs pair dest1 dest2 ==
    1.11 -    type_definition Rep Abs UNIV \<and>
    1.12 -    pair = (\<lambda>a b. Abs (a, b)) \<and>
    1.13 -    dest1 = (\<lambda>p. fst (Rep p)) \<and>
    1.14 -    dest2 = (\<lambda>p. snd (Rep p))"
    1.15 -
    1.16 -lemma product_typeI:
    1.17 -  "type_definition Rep Abs UNIV ==>
    1.18 -    pair == \<lambda>a b. Abs (a, b) ==>
    1.19 -    dest1 == (\<lambda>p. fst (Rep p)) ==>
    1.20 -    dest2 == (\<lambda>p. snd (Rep p)) ==>
    1.21 -    product_type Rep Abs pair dest1 dest2"
    1.22 -  by (simp add: product_type_def)
    1.23 +locale product_type =
    1.24 +  fixes Rep and Abs and pair and dest1 and dest2
    1.25 +  assumes "typedef": "type_definition Rep Abs UNIV"
    1.26 +    and pair: "pair == (\<lambda>a b. Abs (a, b))"
    1.27 +    and dest1: "dest1 == (\<lambda>p. fst (Rep p))"
    1.28 +    and dest2: "dest2 == (\<lambda>p. snd (Rep p))"
    1.29  
    1.30 -lemma product_type_typedef:
    1.31 -    "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
    1.32 -  by (unfold product_type_def) blast
    1.33 -
    1.34 -lemma product_type_pair:
    1.35 -    "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
    1.36 -  by (unfold product_type_def) blast
    1.37 +lemmas product_typeI =
    1.38 +  product_type.intro [OF product_type_axioms.intro]
    1.39  
    1.40 -lemma product_type_dest1:
    1.41 -    "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
    1.42 -  by (unfold product_type_def) blast
    1.43 -
    1.44 -lemma product_type_dest2:
    1.45 -    "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
    1.46 -  by (unfold product_type_def) blast
    1.47 -
    1.48 +lemma (in product_type)
    1.49 +    "inject": "(pair x y = pair x' y') = (x = x' \<and> y = y')"
    1.50 +  by (simp add: pair type_definition.Abs_inject [OF "typedef"])
    1.51  
    1.52 -theorem product_type_inject:
    1.53 -  "product_type Rep Abs pair dest1 dest2 ==>
    1.54 -    (pair x y = pair x' y') = (x = x' \<and> y = y')"
    1.55 -proof -
    1.56 -  case rule_context
    1.57 -  show ?thesis
    1.58 -    by (simp add: product_type_pair [OF rule_context]
    1.59 -      Abs_inject [OF product_type_typedef [OF rule_context]])
    1.60 -qed
    1.61 +lemma (in product_type) conv1: "dest1 (pair x y) = x"
    1.62 +  by (simp add: pair dest1 type_definition.Abs_inverse [OF "typedef"])
    1.63  
    1.64 -theorem product_type_conv1:
    1.65 -  "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
    1.66 -proof -
    1.67 -  case rule_context
    1.68 -  show ?thesis
    1.69 -    by (simp add: product_type_pair [OF rule_context]
    1.70 -      product_type_dest1 [OF rule_context]
    1.71 -      Abs_inverse [OF product_type_typedef [OF rule_context]])
    1.72 -qed
    1.73 +lemma (in product_type) conv2: "dest2 (pair x y) = y"
    1.74 +  by (simp add: pair dest2 type_definition.Abs_inverse [OF "typedef"])
    1.75  
    1.76 -theorem product_type_conv2:
    1.77 -  "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
    1.78 -proof -
    1.79 -  case rule_context
    1.80 -  show ?thesis
    1.81 -    by (simp add: product_type_pair [OF rule_context]
    1.82 -      product_type_dest2 [OF rule_context]
    1.83 -      Abs_inverse [OF product_type_typedef [OF rule_context]])
    1.84 -qed
    1.85 -
    1.86 -theorem product_type_induct [induct set: product_type]:
    1.87 -  "product_type Rep Abs pair dest1 dest2 ==>
    1.88 -    (!!x y. P (pair x y)) ==> P p"
    1.89 -proof -
    1.90 -  assume hyp: "!!x y. P (pair x y)"
    1.91 -  assume prod_type: "product_type Rep Abs pair dest1 dest2"
    1.92 -  show "P p"
    1.93 -  proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
    1.94 -    fix pair show "P (Abs pair)"
    1.95 -    proof (rule prod_induct)
    1.96 -      fix x y from hyp show "P (Abs (x, y))"
    1.97 -        by (simp only: product_type_pair [OF prod_type])
    1.98 -    qed
    1.99 +lemma (in product_type) induct [induct type]:
   1.100 +  assumes hyp: "!!x y. P (pair x y)"
   1.101 +  shows "P p"
   1.102 +proof (rule type_definition.Abs_induct [OF "typedef"])
   1.103 +  fix q show "P (Abs q)"
   1.104 +  proof (induct q)
   1.105 +    fix x y have "P (pair x y)" by (rule hyp)
   1.106 +    also have "pair x y = Abs (x, y)" by (simp only: pair)
   1.107 +    finally show "P (Abs (x, y))" .
   1.108    qed
   1.109  qed
   1.110  
   1.111 -theorem product_type_cases [cases set: product_type]:
   1.112 -  "product_type Rep Abs pair dest1 dest2 ==>
   1.113 -    (!!x y. p = pair x y ==> C) ==> C"
   1.114 -proof -
   1.115 -  assume prod_type: "product_type Rep Abs pair dest1 dest2"
   1.116 -  assume "!!x y. p = pair x y ==> C"
   1.117 -  with prod_type show C
   1.118 -    by (induct p) (simp only: product_type_inject [OF prod_type], blast)
   1.119 -qed
   1.120 +lemma (in product_type) cases [cases type]:
   1.121 +    "(!!x y. p = pair x y ==> C) ==> C"
   1.122 +  by (induct p) (auto simp add: "inject")
   1.123  
   1.124 -theorem product_type_surjective_pairing:
   1.125 -  "product_type Rep Abs pair dest1 dest2 ==>
   1.126 -    p = pair (dest1 p) (dest2 p)"
   1.127 -proof -
   1.128 -  case rule_context
   1.129 -  thus ?thesis by (induct p)
   1.130 -    (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
   1.131 -qed
   1.132 +lemma (in product_type) surjective_pairing:
   1.133 +    "p = pair (dest1 p) (dest2 p)"
   1.134 +  by (induct p) (simp only: conv1 conv2)
   1.135  
   1.136 -theorem product_type_split_paired_all:
   1.137 -  "product_type Rep Abs pair dest1 dest2 ==>
   1.138 -  (!!x. PROP P x) == (!!a b. PROP P (pair a b))"
   1.139 +lemma (in product_type) split_paired_all:
   1.140 +  "(!!x. PROP P x) == (!!a b. PROP P (pair a b))"
   1.141  proof
   1.142    fix a b
   1.143    assume "!!x. PROP P x"
   1.144    thus "PROP P (pair a b)" .
   1.145  next
   1.146 -  case rule_context
   1.147    fix x
   1.148    assume "!!a b. PROP P (pair a b)"
   1.149    hence "PROP P (pair (dest1 x) (dest2 x))" .
   1.150 -  thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
   1.151 +  thus "PROP P x" by (simp only: surjective_pairing [symmetric])
   1.152  qed
   1.153  
   1.154