src/HOL/Import/HOL4Setup.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17801 30cbd2685e73
child 19064 bf19cc5a7899
permissions -rw-r--r--
adaptions to codegen_package
     1 (*  Title:      HOL/Import/HOL4Setup.thy
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 theory HOL4Setup imports MakeEqual
     7   uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
     8     ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     9 
    10 section {* General Setup *}
    11 
    12 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    13   by auto
    14 
    15 lemma HOLallI: "(!! bogus. P bogus) \<Longrightarrow> (ALL bogus. P bogus)"
    16 proof -
    17   assume "!! bogus. P bogus"
    18   thus "ALL x. P x"
    19     ..
    20 qed
    21 
    22 consts
    23   ONE_ONE :: "('a => 'b) => bool"
    24   ONTO    :: "('a => 'b) => bool"
    25 
    26 defs
    27   ONE_ONE_DEF: "ONE_ONE f == ALL x y. f x = f y --> x = y"
    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 & ~(surj f))"
    33 proof (rule exI,safe)
    34   show "inj Suc_Rep"
    35     by (rule inj_Suc_Rep)
    36 next
    37   assume "surj Suc_Rep"
    38   hence "ALL y. EX x. y = Suc_Rep x"
    39     by (simp add: 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