src/HOL/Typedef.thy
author wenzelm
Thu Sep 27 22:26:00 2001 +0200 (2001-09-27)
changeset 11608 c760ea8154ee
child 11654 53d18ab990f6
permissions -rw-r--r--
renamed theory "subset" to "Typedef";
     1 (*  Title:      HOL/Typedef.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Munich
     4 
     5 Misc set-theory lemmas and HOL type definitions.
     6 *)
     7 
     8 theory Typedef = Set
     9 files "subset.ML" "equalities.ML" "mono.ML"
    10   "Tools/induct_attrib.ML" ("Tools/typedef_package.ML"):
    11 
    12 (** belongs to theory Ord **)
    13   
    14 theorems linorder_cases [case_names less equal greater] =
    15   linorder_less_split
    16 
    17 (* Courtesy of Stephan Merz *)
    18 lemma Least_mono: 
    19   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    20     ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    21   apply clarify
    22   apply (erule_tac P = "%x. x : S" in LeastI2)
    23    apply fast
    24   apply (rule LeastI2)
    25   apply (auto elim: monoD intro!: order_antisym)
    26   done
    27 
    28 
    29 (*belongs to theory Set*)
    30 setup Rulify.setup
    31 
    32 
    33 section {* HOL type definitions *}
    34 
    35 constdefs
    36   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    37   "type_definition Rep Abs A ==
    38     (\<forall>x. Rep x \<in> A) \<and>
    39     (\<forall>x. Abs (Rep x) = x) \<and>
    40     (\<forall>y \<in> A. Rep (Abs y) = y)"
    41   -- {* This will be stated as an axiom for each typedef! *}
    42 
    43 lemma type_definitionI [intro]:
    44   "(!!x. Rep x \<in> A) ==>
    45     (!!x. Abs (Rep x) = x) ==>
    46     (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    47     type_definition Rep Abs A"
    48   by (unfold type_definition_def) blast
    49 
    50 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    51   by (unfold type_definition_def) blast
    52 
    53 theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    54   by (unfold type_definition_def) blast
    55 
    56 theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    57   by (unfold type_definition_def) blast
    58 
    59 theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    60 proof -
    61   assume tydef: "type_definition Rep Abs A"
    62   show ?thesis
    63   proof
    64     assume "Rep x = Rep y"
    65     hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    66     thus "x = y" by (simp only: Rep_inverse [OF tydef])
    67   next
    68     assume "x = y"
    69     thus "Rep x = Rep y" by simp
    70   qed
    71 qed
    72 
    73 theorem Abs_inject:
    74   "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    75 proof -
    76   assume tydef: "type_definition Rep Abs A"
    77   assume x: "x \<in> A" and y: "y \<in> A"
    78   show ?thesis
    79   proof
    80     assume "Abs x = Abs y"
    81     hence "Rep (Abs x) = Rep (Abs y)" by simp
    82     moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    83     moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    84     ultimately show "x = y" by (simp only:)
    85   next
    86     assume "x = y"
    87     thus "Abs x = Abs y" by simp
    88   qed
    89 qed
    90 
    91 theorem Rep_cases:
    92   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    93 proof -
    94   assume tydef: "type_definition Rep Abs A"
    95   assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
    96   show P
    97   proof (rule r)
    98     from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    99     thus "y = Rep (Abs y)" ..
   100   qed
   101 qed
   102 
   103 theorem Abs_cases:
   104   "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
   105 proof -
   106   assume tydef: "type_definition Rep Abs A"
   107   assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
   108   show P
   109   proof (rule r)
   110     have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   111     thus "x = Abs (Rep x)" ..
   112     show "Rep x \<in> A" by (rule Rep [OF tydef])
   113   qed
   114 qed
   115 
   116 theorem Rep_induct:
   117   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   118 proof -
   119   assume tydef: "type_definition Rep Abs A"
   120   assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   121   moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   122   ultimately show "P y" by (simp only:)
   123 qed
   124 
   125 theorem Abs_induct:
   126   "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   127 proof -
   128   assume tydef: "type_definition Rep Abs A"
   129   assume r: "!!y. y \<in> A ==> P (Abs y)"
   130   have "Rep x \<in> A" by (rule Rep [OF tydef])
   131   hence "P (Abs (Rep x))" by (rule r)
   132   moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   133   ultimately show "P x" by (simp only:)
   134 qed
   135 
   136 setup InductAttrib.setup
   137 use "Tools/typedef_package.ML"
   138 
   139 end