src/HOL/Typedef.thy
author haftmann
Thu Aug 12 17:56:41 2010 +0200 (2010-08-12)
changeset 38393 7c045c03598f
parent 37863 7f113caabcf4
child 38536 7e57a0dcbd4f
permissions -rw-r--r--
group record-related ML files
     1 (*  Title:      HOL/Typedef.thy
     2     Author:     Markus Wenzel, TU Munich
     3 *)
     4 
     5 header {* HOL type definitions *}
     6 
     7 theory Typedef
     8 imports Set
     9 uses
    10   ("Tools/typedef.ML")
    11   ("Tools/typedef_codegen.ML")
    12 begin
    13 
    14 ML {*
    15 structure HOL = struct val thy = @{theory HOL} end;
    16 *}  -- "belongs to theory HOL"
    17 
    18 locale type_definition =
    19   fixes Rep and Abs and A
    20   assumes Rep: "Rep x \<in> A"
    21     and Rep_inverse: "Abs (Rep x) = x"
    22     and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y"
    23   -- {* This will be axiomatized for each typedef! *}
    24 begin
    25 
    26 lemma Rep_inject:
    27   "(Rep x = Rep y) = (x = y)"
    28 proof
    29   assume "Rep x = Rep y"
    30   then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    31   moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    32   moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
    33   ultimately show "x = y" by simp
    34 next
    35   assume "x = y"
    36   thus "Rep x = Rep y" by (simp only:)
    37 qed
    38 
    39 lemma Abs_inject:
    40   assumes x: "x \<in> A" and y: "y \<in> A"
    41   shows "(Abs x = Abs y) = (x = y)"
    42 proof
    43   assume "Abs x = Abs y"
    44   then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    45   moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse)
    46   moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    47   ultimately show "x = y" by simp
    48 next
    49   assume "x = y"
    50   thus "Abs x = Abs y" by (simp only:)
    51 qed
    52 
    53 lemma Rep_cases [cases set]:
    54   assumes y: "y \<in> A"
    55     and hyp: "!!x. y = Rep x ==> P"
    56   shows P
    57 proof (rule hyp)
    58   from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    59   thus "y = Rep (Abs y)" ..
    60 qed
    61 
    62 lemma Abs_cases [cases type]:
    63   assumes r: "!!y. x = Abs y ==> y \<in> A ==> P"
    64   shows P
    65 proof (rule r)
    66   have "Abs (Rep x) = x" by (rule Rep_inverse)
    67   thus "x = Abs (Rep x)" ..
    68   show "Rep x \<in> A" by (rule Rep)
    69 qed
    70 
    71 lemma Rep_induct [induct set]:
    72   assumes y: "y \<in> A"
    73     and hyp: "!!x. P (Rep x)"
    74   shows "P y"
    75 proof -
    76   have "P (Rep (Abs y))" by (rule hyp)
    77   moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    78   ultimately show "P y" by simp
    79 qed
    80 
    81 lemma Abs_induct [induct type]:
    82   assumes r: "!!y. y \<in> A ==> P (Abs y)"
    83   shows "P x"
    84 proof -
    85   have "Rep x \<in> A" by (rule Rep)
    86   then have "P (Abs (Rep x))" by (rule r)
    87   moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    88   ultimately show "P x" by simp
    89 qed
    90 
    91 lemma Rep_range: "range Rep = A"
    92 proof
    93   show "range Rep <= A" using Rep by (auto simp add: image_def)
    94   show "A <= range Rep"
    95   proof
    96     fix x assume "x : A"
    97     hence "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
    98     thus "x : range Rep" by (rule range_eqI)
    99   qed
   100 qed
   101 
   102 lemma Abs_image: "Abs ` A = UNIV"
   103 proof
   104   show "Abs ` A <= UNIV" by (rule subset_UNIV)
   105 next
   106   show "UNIV <= Abs ` A"
   107   proof
   108     fix x
   109     have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
   110     moreover have "Rep x : A" by (rule Rep)
   111     ultimately show "x : Abs ` A" by (rule image_eqI)
   112   qed
   113 qed
   114 
   115 end
   116 
   117 use "Tools/typedef.ML" setup Typedef.setup
   118 use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
   119 
   120 end