src/HOL/Typedef.thy
author wenzelm
Tue Oct 30 13:43:26 2001 +0100 (2001-10-30)
changeset 11982 65e2822d83dd
parent 11979 0a3dace545c5
child 12023 d982f98e0f0d
permissions -rw-r--r--
lemma Least_mono moved from Typedef.thy to Set.thy;
     1 (*  Title:      HOL/Typedef.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Munich
     4 *)
     5 
     6 header {* HOL type definitions *}
     7 
     8 theory Typedef = Set
     9 files ("Tools/typedef_package.ML"):
    10 
    11 subsection {* HOL type definitions *}
    12 
    13 constdefs
    14   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    15   "type_definition Rep Abs A ==
    16     (\<forall>x. Rep x \<in> A) \<and>
    17     (\<forall>x. Abs (Rep x) = x) \<and>
    18     (\<forall>y \<in> A. Rep (Abs y) = y)"
    19   -- {* This will be stated as an axiom for each typedef! *}
    20 
    21 lemma type_definitionI [intro]:
    22   "(!!x. Rep x \<in> A) ==>
    23     (!!x. Abs (Rep x) = x) ==>
    24     (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    25     type_definition Rep Abs A"
    26   by (unfold type_definition_def) blast
    27 
    28 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    29   by (unfold type_definition_def) blast
    30 
    31 theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    32   by (unfold type_definition_def) blast
    33 
    34 theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    35   by (unfold type_definition_def) blast
    36 
    37 theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    38 proof -
    39   assume tydef: "type_definition Rep Abs A"
    40   show ?thesis
    41   proof
    42     assume "Rep x = Rep y"
    43     hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    44     thus "x = y" by (simp only: Rep_inverse [OF tydef])
    45   next
    46     assume "x = y"
    47     thus "Rep x = Rep y" by simp
    48   qed
    49 qed
    50 
    51 theorem Abs_inject:
    52   "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    53 proof -
    54   assume tydef: "type_definition Rep Abs A"
    55   assume x: "x \<in> A" and y: "y \<in> A"
    56   show ?thesis
    57   proof
    58     assume "Abs x = Abs y"
    59     hence "Rep (Abs x) = Rep (Abs y)" by simp
    60     moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    61     moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    62     ultimately show "x = y" by (simp only:)
    63   next
    64     assume "x = y"
    65     thus "Abs x = Abs y" by simp
    66   qed
    67 qed
    68 
    69 theorem Rep_cases:
    70   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    71 proof -
    72   assume tydef: "type_definition Rep Abs A"
    73   assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
    74   show P
    75   proof (rule r)
    76     from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    77     thus "y = Rep (Abs y)" ..
    78   qed
    79 qed
    80 
    81 theorem Abs_cases:
    82   "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
    83 proof -
    84   assume tydef: "type_definition Rep Abs A"
    85   assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
    86   show P
    87   proof (rule r)
    88     have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
    89     thus "x = Abs (Rep x)" ..
    90     show "Rep x \<in> A" by (rule Rep [OF tydef])
    91   qed
    92 qed
    93 
    94 theorem Rep_induct:
    95   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
    96 proof -
    97   assume tydef: "type_definition Rep Abs A"
    98   assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
    99   moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   100   ultimately show "P y" by (simp only:)
   101 qed
   102 
   103 theorem Abs_induct:
   104   "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   105 proof -
   106   assume tydef: "type_definition Rep Abs A"
   107   assume r: "!!y. y \<in> A ==> P (Abs y)"
   108   have "Rep x \<in> A" by (rule Rep [OF tydef])
   109   hence "P (Abs (Rep x))" by (rule r)
   110   moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   111   ultimately show "P x" by (simp only:)
   112 qed
   113 
   114 use "Tools/typedef_package.ML"
   115 
   116 end