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