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