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