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