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