src/HOL/Import/HOL4Setup.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 20326 cbf31171c147
child 31723 f5cafe803b55
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/Import/HOL4Setup.thy
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 theory HOL4Setup imports MakeEqual ImportRecorder
     7   uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     8 
     9 section {* General Setup *}
    10 
    11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    12   by auto
    13 
    14 lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
    15 proof -
    16   assume "!! bogus. P bogus"
    17   thus "ALL x. P x"
    18     ..
    19 qed
    20 
    21 consts
    22   ONE_ONE :: "('a => 'b) => bool"
    23 
    24 defs
    25   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
    26 
    27 lemma ONE_ONE_rew: "ONE_ONE f = inj_on f UNIV"
    28   by (simp add: ONE_ONE_DEF inj_on_def)
    29 
    30 lemma INFINITY_AX: "EX (f::ind \<Rightarrow> ind). (inj f & ~(surj f))"
    31 proof (rule exI,safe)
    32   show "inj Suc_Rep"
    33     by (rule inj_Suc_Rep)
    34 next
    35   assume "surj Suc_Rep"
    36   hence "ALL y. EX x. y = Suc_Rep x"
    37     by (simp add: surj_def)
    38   hence "EX x. Zero_Rep = Suc_Rep x"
    39     by (rule spec)
    40   thus False
    41   proof (rule exE)
    42     fix x
    43     assume "Zero_Rep = Suc_Rep x"
    44     hence "Suc_Rep x = Zero_Rep"
    45       ..
    46     with Suc_Rep_not_Zero_Rep
    47     show False
    48       ..
    49   qed
    50 qed
    51 
    52 lemma EXISTS_DEF: "Ex P = P (Eps P)"
    53 proof (rule iffI)
    54   assume "Ex P"
    55   thus "P (Eps P)"
    56     ..
    57 next
    58   assume "P (Eps P)"
    59   thus "Ex P"
    60     ..
    61 qed
    62 
    63 consts
    64   TYPE_DEFINITION :: "('a => bool) => ('b => 'a) => bool"
    65 
    66 defs
    67   TYPE_DEFINITION: "TYPE_DEFINITION p rep == ((ALL x y. (rep x = rep y) --> (x = y)) & (ALL x. (p x = (EX y. x = rep y))))"
    68 
    69 lemma ex_imp_nonempty: "Ex P ==> EX x. x : (Collect P)"
    70   by simp
    71 
    72 lemma light_ex_imp_nonempty: "P t ==> EX x. x : (Collect P)"
    73 proof -
    74   assume "P t"
    75   hence "EX x. P x"
    76     ..
    77   thus ?thesis
    78     by (rule ex_imp_nonempty)
    79 qed
    80 
    81 lemma light_imp_as: "[| Q --> P; P --> Q |] ==> P = Q"
    82   by blast
    83 
    84 lemma typedef_hol2hol4:
    85   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
    86   shows "EX rep. TYPE_DEFINITION P (rep::'a=>'b)"
    87 proof -
    88   from a
    89   have td: "(ALL x. P (Rep x)) & (ALL x. Abs (Rep x) = x) & (ALL y. P y \<longrightarrow> Rep (Abs y) = y)"
    90     by (simp add: type_definition_def)
    91   have ed: "TYPE_DEFINITION P Rep"
    92   proof (auto simp add: TYPE_DEFINITION)
    93     fix x y
    94     assume "Rep x = Rep y"
    95     from td have "x = Abs (Rep x)"
    96       by auto
    97     also have "Abs (Rep x) = Abs (Rep y)"
    98       by (simp add: prems)
    99     also from td have "Abs (Rep y) = y"
   100       by auto
   101     finally show "x = y" .
   102   next
   103     fix x
   104     assume "P x"
   105     with td
   106     have "Rep (Abs x) = x"
   107       by auto
   108     hence "x = Rep (Abs x)"
   109       ..
   110     thus "EX y. x = Rep y"
   111       ..
   112   next
   113     fix y
   114     from td
   115     show "P (Rep y)"
   116       by auto
   117   qed
   118   show ?thesis
   119     apply (rule exI [of _ Rep])
   120     apply (rule ed)
   121     .
   122 qed
   123 
   124 lemma typedef_hol2hollight:
   125   assumes a: "type_definition (Rep::'a=>'b) Abs (Collect P)"
   126   shows "(Abs (Rep a) = a) & (P r = (Rep (Abs r) = r))"
   127 proof
   128   from a
   129   show "Abs (Rep a) = a"
   130     by (rule type_definition.Rep_inverse)
   131 next
   132   show "P r = (Rep (Abs r) = r)"
   133   proof
   134     assume "P r"
   135     hence "r \<in> (Collect P)"
   136       by simp
   137     with a
   138     show "Rep (Abs r) = r"
   139       by (rule type_definition.Abs_inverse)
   140   next
   141     assume ra: "Rep (Abs r) = r"
   142     from a
   143     have "Rep (Abs r) \<in> (Collect P)"
   144       by (rule type_definition.Rep)
   145     thus "P r"
   146       by (simp add: ra)
   147   qed
   148 qed
   149 
   150 lemma termspec_help: "[| Ex P ; c == Eps P |] ==> P c"
   151   apply simp
   152   apply (rule someI_ex)
   153   .
   154 
   155 lemma typedef_helper: "EX x. P x \<Longrightarrow> EX x. x \<in> (Collect P)"
   156   by simp
   157 
   158 use "hol4rews.ML"
   159 
   160 setup hol4_setup
   161 parse_ast_translation smarter_trueprop_parsing
   162 
   163 use "proof_kernel.ML"
   164 use "replay.ML"
   165 use "import_package.ML"
   166 
   167 setup ImportPackage.setup
   168 
   169 end