proper setup for abstract product types;
authorwenzelm
Thu Oct 18 21:01:18 2001 +0200 (2001-10-18)
changeset 118262203c7f9ec40
parent 11825 ef7d619e2c88
child 11827 16ef206e6648
proper setup for abstract product types;
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Thu Oct 18 20:59:59 2001 +0200
     1.2 +++ b/src/HOL/Record.thy	Thu Oct 18 21:01:18 2001 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  header {* Extensible records with structural subtyping *}
     1.6  
     1.7 -theory Record = Datatype
     1.8 +theory Record = Product_Type
     1.9  files ("Tools/record_package.ML"):
    1.10  
    1.11  
    1.12 @@ -13,67 +13,118 @@
    1.13  
    1.14  constdefs
    1.15    product_type :: "('p => 'a * 'b) => ('a * 'b => 'p) =>
    1.16 -    ('a => 'b => 'p) => (('a => 'b => 'c) => 'p => 'c) => bool"
    1.17 -  "product_type Rep Abs intro elim ==
    1.18 +    ('a => 'b => 'p) => ('p \<Rightarrow> 'a) => ('p => 'b) => bool"
    1.19 +  "product_type Rep Abs pair dest1 dest2 ==
    1.20      type_definition Rep Abs UNIV \<and>
    1.21 -    intro = (\<lambda>a b. Abs (a, b)) \<and>
    1.22 -    elim = (\<lambda>f. prod_case f o Rep)"
    1.23 +    pair = (\<lambda>a b. Abs (a, b)) \<and>
    1.24 +    dest1 = (\<lambda>p. fst (Rep p)) \<and>
    1.25 +    dest2 = (\<lambda>p. snd (Rep p))"
    1.26  
    1.27  lemma product_typeI:
    1.28 -  "type_definition Rep Abs A ==> A == UNIV ==>
    1.29 -    intro == \<lambda>a b. Abs (a, b) ==> elim == \<lambda>f. prod_case f o Rep ==>
    1.30 -    product_type Rep Abs intro elim"
    1.31 +  "type_definition Rep Abs UNIV ==>
    1.32 +    pair == \<lambda>a b. Abs (a, b) ==>
    1.33 +    dest1 == (\<lambda>p. fst (Rep p)) \<Longrightarrow>
    1.34 +    dest2 == (\<lambda>p. snd (Rep p)) \<Longrightarrow>
    1.35 +    product_type Rep Abs pair dest1 dest2"
    1.36    by (simp add: product_type_def)
    1.37  
    1.38  lemma product_type_typedef:
    1.39 -    "product_type Rep Abs intro elim ==> type_definition Rep Abs UNIV"
    1.40 +    "product_type Rep Abs pair dest1 dest2 ==> type_definition Rep Abs UNIV"
    1.41    by (unfold product_type_def) blast
    1.42  
    1.43 -lemma product_type_intro:
    1.44 -    "product_type Rep Abs intro elim ==> intro = (\<lambda>a b. Abs (a, b))"
    1.45 +lemma product_type_pair:
    1.46 +    "product_type Rep Abs pair dest1 dest2 ==> pair a b = Abs (a, b)"
    1.47 +  by (unfold product_type_def) blast
    1.48 +
    1.49 +lemma product_type_dest1:
    1.50 +    "product_type Rep Abs pair dest1 dest2 ==> dest1 p = fst (Rep p)"
    1.51    by (unfold product_type_def) blast
    1.52  
    1.53 -lemma product_type_elim:
    1.54 -    "product_type Rep Abs intro elim ==> elim = (\<lambda>f. prod_case f o Rep)"
    1.55 -  by (unfold product_type_def) fast  (* FIXME blast fails!? *)
    1.56 +lemma product_type_dest2:
    1.57 +    "product_type Rep Abs pair dest1 dest2 ==> dest2 p = snd (Rep p)"
    1.58 +  by (unfold product_type_def) blast
    1.59 +
    1.60  
    1.61 -lemma product_type_inject:
    1.62 -  "product_type Rep Abs intro elim ==>
    1.63 -    (intro x y = intro x' y') = (x = x' \<and> y = y')"
    1.64 +theorem product_type_inject:
    1.65 +  "product_type Rep Abs pair dest1 dest2 ==>
    1.66 +    (pair x y = pair x' y') = (x = x' \<and> y = y')"
    1.67 +proof -
    1.68 +  case rule_context
    1.69 +  show ?thesis
    1.70 +    by (simp add: product_type_pair [OF rule_context]
    1.71 +      Abs_inject [OF product_type_typedef [OF rule_context]])
    1.72 +qed
    1.73 +
    1.74 +theorem product_type_conv1:
    1.75 +  "product_type Rep Abs pair dest1 dest2 ==> dest1 (pair x y) = x"
    1.76  proof -
    1.77    case rule_context
    1.78    show ?thesis
    1.79 -    by (simp add: product_type_intro [OF rule_context]
    1.80 -      Abs_inject [OF product_type_typedef [OF rule_context]])
    1.81 +    by (simp add: product_type_pair [OF rule_context]
    1.82 +      product_type_dest1 [OF rule_context]
    1.83 +      Abs_inverse [OF product_type_typedef [OF rule_context]])
    1.84  qed
    1.85  
    1.86 -lemma product_type_surject:
    1.87 -  "product_type Rep Abs intro elim ==>
    1.88 -    elim f (intro x y) = f x y"
    1.89 +theorem product_type_conv2:
    1.90 +  "product_type Rep Abs pair dest1 dest2 ==> dest2 (pair x y) = y"
    1.91  proof -
    1.92    case rule_context
    1.93    show ?thesis
    1.94 -    by (simp add: product_type_intro [OF rule_context]
    1.95 -      product_type_elim [OF rule_context]
    1.96 +    by (simp add: product_type_pair [OF rule_context]
    1.97 +      product_type_dest2 [OF rule_context]
    1.98        Abs_inverse [OF product_type_typedef [OF rule_context]])
    1.99  qed
   1.100  
   1.101 -lemma product_type_induct:
   1.102 -  "product_type Rep Abs intro elim ==>
   1.103 -    (!!x y. P (intro x y)) ==> P p"
   1.104 +theorem product_type_induct [induct set: product_type]:
   1.105 +  "product_type Rep Abs pair dest1 dest2 ==>
   1.106 +    (!!x y. P (pair x y)) ==> P p"
   1.107  proof -
   1.108 -  assume hyp: "!!x y. P (intro x y)"
   1.109 -  assume prod_type: "product_type Rep Abs intro elim"
   1.110 +  assume hyp: "!!x y. P (pair x y)"
   1.111 +  assume prod_type: "product_type Rep Abs pair dest1 dest2"
   1.112    show "P p"
   1.113    proof (rule Abs_induct [OF product_type_typedef [OF prod_type]])
   1.114      fix pair show "P (Abs pair)"
   1.115 -    proof (rule prod.induct)
   1.116 +    proof (rule prod_induct)
   1.117        fix x y from hyp show "P (Abs (x, y))"
   1.118 -	by (simp only: product_type_intro [OF prod_type])
   1.119 +        by (simp only: product_type_pair [OF prod_type])
   1.120      qed
   1.121    qed
   1.122  qed
   1.123  
   1.124 +theorem product_type_cases [cases set: product_type]:
   1.125 +  "product_type Rep Abs pair dest1 dest2 ==>
   1.126 +    (!!x y. p = pair x y \<Longrightarrow> C) ==> C"
   1.127 +proof -
   1.128 +  assume prod_type: "product_type Rep Abs pair dest1 dest2"
   1.129 +  assume "!!x y. p = pair x y \<Longrightarrow> C"
   1.130 +  with prod_type show C
   1.131 +    by (induct p) (simp only: product_type_inject [OF prod_type], blast)
   1.132 +qed
   1.133 +
   1.134 +theorem product_type_surjective_pairing:
   1.135 +  "product_type Rep Abs pair dest1 dest2 ==>
   1.136 +    p = pair (dest1 p) (dest2 p)"
   1.137 +proof -
   1.138 +  case rule_context
   1.139 +  thus ?thesis by (induct p)
   1.140 +    (simp add: product_type_conv1 [OF rule_context] product_type_conv2 [OF rule_context])
   1.141 +qed
   1.142 +
   1.143 +theorem product_type_split_paired_all:
   1.144 +  "product_type Rep Abs pair dest1 dest2 ==>
   1.145 +  (\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (pair a b))"
   1.146 +proof
   1.147 +  fix a b
   1.148 +  assume "!!x. PROP P x"
   1.149 +  thus "PROP P (pair a b)" .
   1.150 +next
   1.151 +  case rule_context
   1.152 +  fix x
   1.153 +  assume "!!a b. PROP P (pair a b)"
   1.154 +  hence "PROP P (pair (dest1 x) (dest2 x))" .
   1.155 +  thus "PROP P x" by (simp only: product_type_surjective_pairing [OF rule_context, symmetric])
   1.156 +qed
   1.157 +
   1.158  
   1.159  text {* \medskip Type class for record extensions. *}
   1.160  
   1.161 @@ -81,7 +132,13 @@
   1.162  instance unit :: more ..
   1.163  
   1.164  
   1.165 -subsection {* Concrete syntax of records *}
   1.166 +subsection {* Record package setup *}
   1.167 +
   1.168 +use "Tools/record_package.ML"
   1.169 +setup RecordPackage.setup
   1.170 +
   1.171 +
   1.172 +subsection {* Concrete syntax *}
   1.173  
   1.174  nonterminals
   1.175    ident field_type field_types field fields update updates
   1.176 @@ -115,11 +172,6 @@
   1.177    "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   1.178    "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
   1.179  
   1.180 -
   1.181 -subsection {* Package setup *}
   1.182 -
   1.183 -use "Tools/record_package.ML"
   1.184 -
   1.185  parse_translation {*
   1.186    let
   1.187      fun update_name_tr (Free (x, T) :: ts) =
   1.188 @@ -133,6 +185,4 @@
   1.189    in [("_update_name", update_name_tr)] end
   1.190  *}
   1.191  
   1.192 -setup RecordPackage.setup
   1.193 -
   1.194  end