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