src/HOL/Typedef.thy
author wenzelm
Mon Dec 07 10:38:04 2015 +0100 (2015-12-07)
changeset 61799 4cf66f21b764
parent 61102 0ec9fd8d8119
child 63434 c956d995bec6
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/Typedef.thy
     2     Author:     Markus Wenzel, TU Munich
     3 *)
     4 
     5 section \<open>HOL type definitions\<close>
     6 
     7 theory Typedef
     8 imports Set
     9 keywords "typedef" :: thy_goal and "morphisms"
    10 begin
    11 
    12 locale type_definition =
    13   fixes Rep and Abs and A
    14   assumes Rep: "Rep x \<in> A"
    15     and Rep_inverse: "Abs (Rep x) = x"
    16     and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y"
    17   \<comment> \<open>This will be axiomatized for each typedef!\<close>
    18 begin
    19 
    20 lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"
    21 proof
    22   assume "Rep x = Rep y"
    23   then have "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    24   moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    25   moreover have "Abs (Rep y) = y" by (rule Rep_inverse)
    26   ultimately show "x = y" by simp
    27 next
    28   assume "x = y"
    29   then show "Rep x = Rep y" by (simp only:)
    30 qed
    31 
    32 lemma Abs_inject:
    33   assumes "x \<in> A" and "y \<in> A"
    34   shows "Abs x = Abs y \<longleftrightarrow> x = y"
    35 proof
    36   assume "Abs x = Abs y"
    37   then have "Rep (Abs x) = Rep (Abs y)" by (simp only:)
    38   moreover from \<open>x \<in> A\<close> have "Rep (Abs x) = x" by (rule Abs_inverse)
    39   moreover from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
    40   ultimately show "x = y" by simp
    41 next
    42   assume "x = y"
    43   then show "Abs x = Abs y" by (simp only:)
    44 qed
    45 
    46 lemma Rep_cases [cases set]:
    47   assumes "y \<in> A"
    48     and hyp: "\<And>x. y = Rep x \<Longrightarrow> P"
    49   shows P
    50 proof (rule hyp)
    51   from \<open>y \<in> A\<close> have "Rep (Abs y) = y" by (rule Abs_inverse)
    52   then show "y = Rep (Abs y)" ..
    53 qed
    54 
    55 lemma Abs_cases [cases type]:
    56   assumes r: "\<And>y. x = Abs y \<Longrightarrow> y \<in> A \<Longrightarrow> P"
    57   shows P
    58 proof (rule r)
    59   have "Abs (Rep x) = x" by (rule Rep_inverse)
    60   then show "x = Abs (Rep x)" ..
    61   show "Rep x \<in> A" by (rule Rep)
    62 qed
    63 
    64 lemma Rep_induct [induct set]:
    65   assumes y: "y \<in> A"
    66     and hyp: "\<And>x. P (Rep x)"
    67   shows "P y"
    68 proof -
    69   have "P (Rep (Abs y))" by (rule hyp)
    70   moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse)
    71   ultimately show "P y" by simp
    72 qed
    73 
    74 lemma Abs_induct [induct type]:
    75   assumes r: "\<And>y. y \<in> A \<Longrightarrow> P (Abs y)"
    76   shows "P x"
    77 proof -
    78   have "Rep x \<in> A" by (rule Rep)
    79   then have "P (Abs (Rep x))" by (rule r)
    80   moreover have "Abs (Rep x) = x" by (rule Rep_inverse)
    81   ultimately show "P x" by simp
    82 qed
    83 
    84 lemma Rep_range: "range Rep = A"
    85 proof
    86   show "range Rep \<subseteq> A" using Rep by (auto simp add: image_def)
    87   show "A \<subseteq> range Rep"
    88   proof
    89     fix x assume "x \<in> A"
    90     then have "x = Rep (Abs x)" by (rule Abs_inverse [symmetric])
    91     then show "x \<in> range Rep" by (rule range_eqI)
    92   qed
    93 qed
    94 
    95 lemma Abs_image: "Abs ` A = UNIV"
    96 proof
    97   show "Abs ` A \<subseteq> UNIV" by (rule subset_UNIV)
    98   show "UNIV \<subseteq> Abs ` A"
    99   proof
   100     fix x
   101     have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
   102     moreover have "Rep x \<in> A" by (rule Rep)
   103     ultimately show "x \<in> Abs ` A" by (rule image_eqI)
   104   qed
   105 qed
   106 
   107 end
   108 
   109 ML_file "Tools/typedef.ML"
   110 
   111 end