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