src/HOL/Typedef.thy
author wenzelm
Sun Oct 28 22:59:12 2001 +0100 (2001-10-28)
changeset 11979 0a3dace545c5
parent 11770 b6bb7a853dd2
child 11982 65e2822d83dd
permissions -rw-r--r--
converted theory "Set";
     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 lemma Least_mono: 
    12   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
    13     ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
    14     -- {* Courtesy of Stephan Merz *}
    15   apply clarify
    16   apply (erule_tac P = "%x. x : S" in LeastI2)
    17    apply fast
    18   apply (rule LeastI2)
    19   apply (auto elim: monoD intro!: order_antisym)
    20   done
    21 
    22 
    23 subsection {* HOL type definitions *}
    24 
    25 constdefs
    26   type_definition :: "('a => 'b) => ('b => 'a) => 'b set => bool"
    27   "type_definition Rep Abs A ==
    28     (\<forall>x. Rep x \<in> A) \<and>
    29     (\<forall>x. Abs (Rep x) = x) \<and>
    30     (\<forall>y \<in> A. Rep (Abs y) = y)"
    31   -- {* This will be stated as an axiom for each typedef! *}
    32 
    33 lemma type_definitionI [intro]:
    34   "(!!x. Rep x \<in> A) ==>
    35     (!!x. Abs (Rep x) = x) ==>
    36     (!!y. y \<in> A ==> Rep (Abs y) = y) ==>
    37     type_definition Rep Abs A"
    38   by (unfold type_definition_def) blast
    39 
    40 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A"
    41   by (unfold type_definition_def) blast
    42 
    43 theorem Rep_inverse: "type_definition Rep Abs A ==> Abs (Rep x) = x"
    44   by (unfold type_definition_def) blast
    45 
    46 theorem Abs_inverse: "type_definition Rep Abs A ==> y \<in> A ==> Rep (Abs y) = y"
    47   by (unfold type_definition_def) blast
    48 
    49 theorem Rep_inject: "type_definition Rep Abs A ==> (Rep x = Rep y) = (x = y)"
    50 proof -
    51   assume tydef: "type_definition Rep Abs A"
    52   show ?thesis
    53   proof
    54     assume "Rep x = Rep y"
    55     hence "Abs (Rep x) = Abs (Rep y)" by (simp only:)
    56     thus "x = y" by (simp only: Rep_inverse [OF tydef])
    57   next
    58     assume "x = y"
    59     thus "Rep x = Rep y" by simp
    60   qed
    61 qed
    62 
    63 theorem Abs_inject:
    64   "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
    65 proof -
    66   assume tydef: "type_definition Rep Abs A"
    67   assume x: "x \<in> A" and y: "y \<in> A"
    68   show ?thesis
    69   proof
    70     assume "Abs x = Abs y"
    71     hence "Rep (Abs x) = Rep (Abs y)" by simp
    72     moreover from x have "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
    73     moreover from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    74     ultimately show "x = y" by (simp only:)
    75   next
    76     assume "x = y"
    77     thus "Abs x = Abs y" by simp
    78   qed
    79 qed
    80 
    81 theorem Rep_cases:
    82   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
    83 proof -
    84   assume tydef: "type_definition Rep Abs A"
    85   assume y: "y \<in> A" and r: "(!!x. y = Rep x ==> P)"
    86   show P
    87   proof (rule r)
    88     from y have "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
    89     thus "y = Rep (Abs y)" ..
    90   qed
    91 qed
    92 
    93 theorem Abs_cases:
    94   "type_definition Rep Abs A ==> (!!y. x = Abs y ==> y \<in> A ==> P) ==> P"
    95 proof -
    96   assume tydef: "type_definition Rep Abs A"
    97   assume r: "!!y. x = Abs y ==> y \<in> A ==> P"
    98   show P
    99   proof (rule r)
   100     have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   101     thus "x = Abs (Rep x)" ..
   102     show "Rep x \<in> A" by (rule Rep [OF tydef])
   103   qed
   104 qed
   105 
   106 theorem Rep_induct:
   107   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
   108 proof -
   109   assume tydef: "type_definition Rep Abs A"
   110   assume "!!x. P (Rep x)" hence "P (Rep (Abs y))" .
   111   moreover assume "y \<in> A" hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
   112   ultimately show "P y" by (simp only:)
   113 qed
   114 
   115 theorem Abs_induct:
   116   "type_definition Rep Abs A ==> (!!y. y \<in> A ==> P (Abs y)) ==> P x"
   117 proof -
   118   assume tydef: "type_definition Rep Abs A"
   119   assume r: "!!y. y \<in> A ==> P (Abs y)"
   120   have "Rep x \<in> A" by (rule Rep [OF tydef])
   121   hence "P (Abs (Rep x))" by (rule r)
   122   moreover have "Abs (Rep x) = x" by (rule Rep_inverse [OF tydef])
   123   ultimately show "P x" by (simp only:)
   124 qed
   125 
   126 use "Tools/typedef_package.ML"
   127 
   128 end