src/HOL/Import/import_rule.ML
author wenzelm
Fri Oct 12 21:22:35 2012 +0200 (2012-10-12)
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 50214 67fb9a168d10
permissions -rw-r--r--
discontinued typedef with alternative name;
cezarykaliszyk@47258
     1
(*  Title:      HOL/Import/import_rule.ML
cezarykaliszyk@47258
     2
    Author:     Cezary Kaliszyk, University of Innsbruck
cezarykaliszyk@47258
     3
    Author:     Alexander Krauss, QAware GmbH
cezarykaliszyk@47258
     4
cezarykaliszyk@47258
     5
Importer proof rules and processing of lines and files.
cezarykaliszyk@47258
     6
cezarykaliszyk@47258
     7
Based on earlier code by Steven Obua and Sebastian Skalberg.
cezarykaliszyk@47258
     8
*)
cezarykaliszyk@47258
     9
cezarykaliszyk@47258
    10
signature IMPORT_RULE =
cezarykaliszyk@47258
    11
sig
cezarykaliszyk@47258
    12
  val beta : cterm -> thm
cezarykaliszyk@47258
    13
  val eq_mp : thm -> thm -> thm
cezarykaliszyk@47258
    14
  val comb : thm -> thm -> thm
cezarykaliszyk@47258
    15
  val trans : thm -> thm -> thm
cezarykaliszyk@47258
    16
  val deduct : thm -> thm -> thm
cezarykaliszyk@47258
    17
  val conj1 : thm -> thm
cezarykaliszyk@47258
    18
  val conj2 : thm -> thm
cezarykaliszyk@47258
    19
  val refl : cterm -> thm
cezarykaliszyk@47258
    20
  val abs : cterm -> thm -> thm
cezarykaliszyk@47258
    21
  val mdef : string -> theory -> thm
cezarykaliszyk@47258
    22
  val def : string -> cterm -> theory -> thm * theory
cezarykaliszyk@47258
    23
  val mtydef : string -> theory -> thm
cezarykaliszyk@47258
    24
  val tydef :
cezarykaliszyk@47258
    25
    string -> string -> string -> cterm -> cterm -> thm -> theory -> thm * theory
cezarykaliszyk@47258
    26
  val inst_type : (ctyp * ctyp) list -> thm -> theory -> thm
cezarykaliszyk@47258
    27
  val inst : (cterm * cterm) list -> thm -> thm
cezarykaliszyk@47258
    28
cezarykaliszyk@47258
    29
  type state
cezarykaliszyk@47258
    30
  val init_state : state
cezarykaliszyk@47258
    31
  val process_line : string -> (theory * state) -> (theory * state)
cezarykaliszyk@47258
    32
  val process_file : Path.T -> theory -> theory
cezarykaliszyk@47258
    33
end
cezarykaliszyk@47258
    34
cezarykaliszyk@47258
    35
structure Import_Rule: IMPORT_RULE =
cezarykaliszyk@47258
    36
struct
cezarykaliszyk@47258
    37
cezarykaliszyk@47258
    38
val init_state = ((Inttab.empty, 0), (Inttab.empty, 0), (Inttab.empty, 0))
cezarykaliszyk@47258
    39
cezarykaliszyk@47258
    40
type state = (ctyp Inttab.table * int) * (cterm Inttab.table * int) * (thm Inttab.table * int)
cezarykaliszyk@47258
    41
cezarykaliszyk@47258
    42
fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
cezarykaliszyk@47258
    43
cezarykaliszyk@47258
    44
fun meta_mp th1 th2 =
cezarykaliszyk@47258
    45
  let
cezarykaliszyk@47258
    46
    val th1a = implies_elim_all th1
cezarykaliszyk@47258
    47
    val th1b = Thm.implies_intr (strip_imp_concl (cprop_of th2)) th1a
cezarykaliszyk@47258
    48
    val th2a = implies_elim_all th2
cezarykaliszyk@47258
    49
    val th3 = Thm.implies_elim th1b th2a
cezarykaliszyk@47258
    50
  in
cezarykaliszyk@47258
    51
    implies_intr_hyps th3
cezarykaliszyk@47258
    52
  end
cezarykaliszyk@47258
    53
cezarykaliszyk@47258
    54
fun meta_eq_to_obj_eq th =
cezarykaliszyk@47258
    55
  let
cezarykaliszyk@47258
    56
    val (tml, tmr) = Thm.dest_binop (strip_imp_concl (cprop_of th))
cezarykaliszyk@47258
    57
    val cty = ctyp_of_term tml
cezarykaliszyk@47258
    58
    val i = Drule.instantiate' [SOME cty] [SOME tml, SOME tmr]
cezarykaliszyk@47258
    59
      @{thm meta_eq_to_obj_eq}
cezarykaliszyk@47258
    60
  in
cezarykaliszyk@47258
    61
    Thm.implies_elim i th
cezarykaliszyk@47258
    62
  end
cezarykaliszyk@47258
    63
cezarykaliszyk@47258
    64
fun beta ct = meta_eq_to_obj_eq (Thm.beta_conversion false ct)
cezarykaliszyk@47258
    65
cezarykaliszyk@47258
    66
fun eq_mp th1 th2 =
cezarykaliszyk@47258
    67
  let
cezarykaliszyk@47258
    68
    val (tm1l, tm1r) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (cprop_of th1)))
cezarykaliszyk@47258
    69
    val i1 = Drule.instantiate' [] [SOME tm1l, SOME tm1r] @{thm iffD1}
cezarykaliszyk@47258
    70
    val i2 = meta_mp i1 th1
cezarykaliszyk@47258
    71
  in
cezarykaliszyk@47258
    72
    meta_mp i2 th2
cezarykaliszyk@47258
    73
  end
cezarykaliszyk@47258
    74
cezarykaliszyk@47258
    75
fun comb th1 th2 =
cezarykaliszyk@47258
    76
  let
cezarykaliszyk@47258
    77
    val t1c = Thm.dest_arg (strip_imp_concl (cprop_of th1))
cezarykaliszyk@47258
    78
    val t2c = Thm.dest_arg (strip_imp_concl (cprop_of th2))
cezarykaliszyk@47258
    79
    val (cf, cg) = Thm.dest_binop t1c
cezarykaliszyk@47258
    80
    val (cx, cy) = Thm.dest_binop t2c
cezarykaliszyk@47258
    81
    val [fd, fr] = Thm.dest_ctyp (ctyp_of_term cf)
cezarykaliszyk@47258
    82
    val i1 = Drule.instantiate' [SOME fd, SOME fr]
cezarykaliszyk@47258
    83
      [SOME cf, SOME cg, SOME cx, SOME cy] @{thm cong}
cezarykaliszyk@47258
    84
    val i2 = meta_mp i1 th1
cezarykaliszyk@47258
    85
  in
cezarykaliszyk@47258
    86
    meta_mp i2 th2
cezarykaliszyk@47258
    87
  end
cezarykaliszyk@47258
    88
cezarykaliszyk@47258
    89
fun trans th1 th2 =
cezarykaliszyk@47258
    90
  let
cezarykaliszyk@47258
    91
    val t1c = Thm.dest_arg (strip_imp_concl (cprop_of th1))
cezarykaliszyk@47258
    92
    val t2c = Thm.dest_arg (strip_imp_concl (cprop_of th2))
cezarykaliszyk@47258
    93
    val (r, s) = Thm.dest_binop t1c
cezarykaliszyk@47258
    94
    val (_, t) = Thm.dest_binop t2c
cezarykaliszyk@47258
    95
    val ty = ctyp_of_term r
cezarykaliszyk@47258
    96
    val i1 = Drule.instantiate' [SOME ty] [SOME r, SOME s, SOME t] @{thm trans}
cezarykaliszyk@47258
    97
    val i2 = meta_mp i1 th1
cezarykaliszyk@47258
    98
  in
cezarykaliszyk@47258
    99
    meta_mp i2 th2
cezarykaliszyk@47258
   100
  end
cezarykaliszyk@47258
   101
cezarykaliszyk@47258
   102
fun deduct th1 th2 =
cezarykaliszyk@47258
   103
  let
cezarykaliszyk@47258
   104
    val th1c = strip_imp_concl (cprop_of th1)
cezarykaliszyk@47258
   105
    val th2c = strip_imp_concl (cprop_of th2)
cezarykaliszyk@47258
   106
    val th1a = implies_elim_all th1
cezarykaliszyk@47258
   107
    val th2a = implies_elim_all th2
cezarykaliszyk@47258
   108
    val th1b = Thm.implies_intr th2c th1a
cezarykaliszyk@47258
   109
    val th2b = Thm.implies_intr th1c th2a
cezarykaliszyk@47258
   110
    val i = Drule.instantiate' []
cezarykaliszyk@47258
   111
      [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
cezarykaliszyk@47258
   112
    val i1 = Thm.implies_elim i (Thm.assume (cprop_of th2b))
cezarykaliszyk@47258
   113
    val i2 = Thm.implies_elim i1 th1b
cezarykaliszyk@47258
   114
    val i3 = Thm.implies_intr (cprop_of th2b) i2
cezarykaliszyk@47258
   115
    val i4 = Thm.implies_elim i3 th2b
cezarykaliszyk@47258
   116
  in
cezarykaliszyk@47258
   117
    implies_intr_hyps i4
cezarykaliszyk@47258
   118
  end
cezarykaliszyk@47258
   119
cezarykaliszyk@47258
   120
fun conj1 th =
cezarykaliszyk@47258
   121
  let
cezarykaliszyk@47258
   122
    val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (cprop_of th)))
cezarykaliszyk@47258
   123
    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct1}
cezarykaliszyk@47258
   124
  in
cezarykaliszyk@47258
   125
    meta_mp i th
cezarykaliszyk@47258
   126
  end
cezarykaliszyk@47258
   127
cezarykaliszyk@47258
   128
fun conj2 th =
cezarykaliszyk@47258
   129
  let
cezarykaliszyk@47258
   130
    val (tml, tmr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (cprop_of th)))
cezarykaliszyk@47258
   131
    val i = Drule.instantiate' [] [SOME tml, SOME tmr] @{thm conjunct2}
cezarykaliszyk@47258
   132
  in
cezarykaliszyk@47258
   133
    meta_mp i th
cezarykaliszyk@47258
   134
  end
cezarykaliszyk@47258
   135
cezarykaliszyk@47258
   136
fun refl ctm =
cezarykaliszyk@47258
   137
  let
cezarykaliszyk@47258
   138
    val cty = Thm.ctyp_of_term ctm
cezarykaliszyk@47258
   139
  in
cezarykaliszyk@47258
   140
    Drule.instantiate' [SOME cty] [SOME ctm] @{thm refl}
cezarykaliszyk@47258
   141
  end
cezarykaliszyk@47258
   142
cezarykaliszyk@47258
   143
fun abs cv th =
cezarykaliszyk@47258
   144
  let
cezarykaliszyk@47258
   145
    val th1 = implies_elim_all th
cezarykaliszyk@47258
   146
    val (tl, tr) = Thm.dest_binop (Thm.dest_arg (strip_imp_concl (cprop_of th1)))
cezarykaliszyk@47258
   147
    val (ll, lr) = (Thm.lambda cv tl, Thm.lambda cv tr)
cezarykaliszyk@47258
   148
    val (al, ar) = (Thm.apply ll cv, Thm.apply lr cv)
cezarykaliszyk@47258
   149
    val bl = beta al
cezarykaliszyk@47258
   150
    val br = meta_eq_to_obj_eq (Thm.symmetric (Thm.beta_conversion false ar))
cezarykaliszyk@47258
   151
    val th2 = trans (trans bl th1) br
cezarykaliszyk@47258
   152
    val th3 = implies_elim_all th2
cezarykaliszyk@47258
   153
    val th4 = Thm.forall_intr cv th3
cezarykaliszyk@47258
   154
    val i = Drule.instantiate' [SOME (ctyp_of_term cv), SOME (ctyp_of_term tl)]
cezarykaliszyk@47258
   155
      [SOME ll, SOME lr] @{thm ext2}
cezarykaliszyk@47258
   156
  in
cezarykaliszyk@47258
   157
    meta_mp i th4
cezarykaliszyk@47258
   158
  end
cezarykaliszyk@47258
   159
cezarykaliszyk@47258
   160
fun freezeT thm =
cezarykaliszyk@47258
   161
  let
cezarykaliszyk@47258
   162
    val tvars = Term.add_tvars (prop_of thm) []
cezarykaliszyk@47258
   163
    val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
cezarykaliszyk@47258
   164
    val tvars = map TVar tvars
cezarykaliszyk@47258
   165
    val thy = Thm.theory_of_thm thm
cezarykaliszyk@47258
   166
    fun inst ty = ctyp_of thy ty
cezarykaliszyk@47258
   167
  in
cezarykaliszyk@47258
   168
    Thm.instantiate ((map inst tvars ~~ map inst tfrees), []) thm
cezarykaliszyk@47258
   169
  end
cezarykaliszyk@47258
   170
cezarykaliszyk@47258
   171
fun def' constname rhs thy =
cezarykaliszyk@47258
   172
  let
cezarykaliszyk@47258
   173
    val rhs = term_of rhs
cezarykaliszyk@47258
   174
    val typ = type_of rhs
cezarykaliszyk@47258
   175
    val thy1 = Sign.add_consts_i [(Binding.name constname, typ, NoSyn)] thy
cezarykaliszyk@47258
   176
    val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs)
cezarykaliszyk@47258
   177
    val (thms, thy2) = Global_Theory.add_defs false
cezarykaliszyk@47258
   178
      [((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1
cezarykaliszyk@47258
   179
    val def_thm = freezeT (hd thms)
cezarykaliszyk@47258
   180
  in
cezarykaliszyk@47258
   181
    (meta_eq_to_obj_eq def_thm, thy2)
cezarykaliszyk@47258
   182
  end
cezarykaliszyk@47258
   183
cezarykaliszyk@47258
   184
fun mdef name thy =
cezarykaliszyk@47258
   185
  case Import_Data.get_const_def name thy of
cezarykaliszyk@47258
   186
    SOME th => th
cezarykaliszyk@47258
   187
  | NONE => error ("constant mapped but no definition: " ^ name)
cezarykaliszyk@47258
   188
cezarykaliszyk@47258
   189
fun def constname rhs thy =
cezarykaliszyk@47258
   190
  case Import_Data.get_const_def constname thy of
cezarykaliszyk@47258
   191
    SOME _ =>
cezarykaliszyk@47258
   192
      let
cezarykaliszyk@47258
   193
        val () = warning ("Const mapped but def provided: " ^ constname)
cezarykaliszyk@47258
   194
      in
cezarykaliszyk@47258
   195
        (mdef constname thy, thy)
cezarykaliszyk@47258
   196
      end
cezarykaliszyk@47258
   197
  | NONE => def' constname rhs thy
cezarykaliszyk@47258
   198
cezarykaliszyk@47258
   199
fun typedef_hollight th thy =
cezarykaliszyk@47258
   200
  let
cezarykaliszyk@47258
   201
    val (th_s, cn) = Thm.dest_comb (Thm.dest_arg (cprop_of th))
cezarykaliszyk@47258
   202
    val (th_s, abst) = Thm.dest_comb th_s
cezarykaliszyk@47258
   203
    val rept = Thm.dest_arg th_s
cezarykaliszyk@47258
   204
    val P = Thm.dest_arg cn
cezarykaliszyk@47258
   205
    val [nty, oty] = Thm.dest_ctyp (ctyp_of_term rept)
cezarykaliszyk@47258
   206
  in
cezarykaliszyk@47258
   207
    Drule.instantiate' [SOME nty, SOME oty] [SOME rept, SOME abst, SOME P,
cezarykaliszyk@47258
   208
      SOME (cterm_of thy (Free ("a", typ_of nty))),
cezarykaliszyk@47258
   209
      SOME (cterm_of thy (Free ("r", typ_of oty)))] @{thm typedef_hol2hollight}
cezarykaliszyk@47258
   210
  end
cezarykaliszyk@47258
   211
cezarykaliszyk@47258
   212
fun tydef' tycname abs_name rep_name cP ct td_th thy =
cezarykaliszyk@47258
   213
  let
cezarykaliszyk@47258
   214
    val ctT = ctyp_of_term ct
cezarykaliszyk@47258
   215
    val nonempty = Drule.instantiate' [SOME ctT] [SOME cP, SOME ct] @{thm light_ex_imp_nonempty}
cezarykaliszyk@47258
   216
    val th2 = meta_mp nonempty td_th
cezarykaliszyk@47258
   217
    val c = case concl_of th2 of
cezarykaliszyk@47258
   218
        _ $ (Const(@{const_name Ex},_) $ Abs(_,_,Const(@{const_name Set.member},_) $ _ $ c)) => c
cezarykaliszyk@47258
   219
      | _ => error "type_introduction: bad type definition theorem"
cezarykaliszyk@47258
   220
    val tfrees = Term.add_tfrees c []
cezarykaliszyk@47258
   221
    val tnames = sort_strings (map fst tfrees)
cezarykaliszyk@47258
   222
    val ((_, typedef_info), thy') =
wenzelm@49835
   223
     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
wenzelm@49835
   224
       (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
cezarykaliszyk@47258
   225
    val aty = #abs_type (#1 typedef_info)
cezarykaliszyk@47258
   226
    val th = freezeT (#type_definition (#2 typedef_info))
cezarykaliszyk@47258
   227
    val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th))
cezarykaliszyk@47258
   228
    val (th_s, abst) = Thm.dest_comb th_s
cezarykaliszyk@47258
   229
    val rept = Thm.dest_arg th_s
cezarykaliszyk@47258
   230
    val [nty, oty] = Thm.dest_ctyp (ctyp_of_term rept)
cezarykaliszyk@47258
   231
    val typedef_th =
cezarykaliszyk@47258
   232
       Drule.instantiate'
cezarykaliszyk@47258
   233
          [SOME nty, SOME oty]
cezarykaliszyk@47258
   234
          [SOME rept, SOME abst, SOME cP, SOME (cterm_of thy' (Free ("a", aty))),
cezarykaliszyk@47258
   235
             SOME (cterm_of thy' (Free ("r", typ_of ctT)))]
cezarykaliszyk@47258
   236
          @{thm typedef_hol2hollight}
cezarykaliszyk@47363
   237
    val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
cezarykaliszyk@47258
   238
  in
cezarykaliszyk@47258
   239
    (th4, thy')
cezarykaliszyk@47258
   240
  end
cezarykaliszyk@47258
   241
cezarykaliszyk@47258
   242
fun mtydef name thy =
cezarykaliszyk@47258
   243
  case Import_Data.get_typ_def name thy of
cezarykaliszyk@47258
   244
    SOME thn => meta_mp (typedef_hollight thn thy) thn
cezarykaliszyk@47258
   245
  | NONE => error ("type mapped but no tydef thm registered: " ^ name)
cezarykaliszyk@47258
   246
cezarykaliszyk@47258
   247
fun tydef tycname abs_name rep_name P t td_th thy =
cezarykaliszyk@47258
   248
  case Import_Data.get_typ_def tycname thy of
cezarykaliszyk@47258
   249
    SOME _ =>
cezarykaliszyk@47258
   250
      let
cezarykaliszyk@47258
   251
        val () = warning ("Type mapped but proofs provided: " ^ tycname)
cezarykaliszyk@47258
   252
      in
cezarykaliszyk@47258
   253
        (mtydef tycname thy, thy)
cezarykaliszyk@47258
   254
      end
cezarykaliszyk@47258
   255
  | NONE => tydef' tycname abs_name rep_name P t td_th thy
cezarykaliszyk@47258
   256
cezarykaliszyk@47258
   257
fun inst_type lambda th thy =
cezarykaliszyk@47258
   258
  let
cezarykaliszyk@47258
   259
    fun assoc _ [] = error "assoc"
cezarykaliszyk@47258
   260
      | assoc x ((x',y)::rest) = if x = x' then y else assoc x rest
cezarykaliszyk@47258
   261
    val lambda = map (fn (a, b) => (typ_of a, b)) lambda
cezarykaliszyk@47258
   262
    val tys_before = Term.add_tfrees (prop_of th) []
cezarykaliszyk@47258
   263
    val th1 = Thm.varifyT_global th
cezarykaliszyk@47258
   264
    val tys_after = Term.add_tvars (prop_of th1) []
cezarykaliszyk@47258
   265
    val tyinst = map2 (fn bef => fn iS =>
cezarykaliszyk@47258
   266
       (case try (assoc (TFree bef)) lambda of
cezarykaliszyk@47258
   267
              SOME cty => (ctyp_of thy (TVar iS), cty)
cezarykaliszyk@47258
   268
            | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
cezarykaliszyk@47258
   269
       )) tys_before tys_after
cezarykaliszyk@47258
   270
  in
cezarykaliszyk@47258
   271
    Thm.instantiate (tyinst,[]) th1
cezarykaliszyk@47258
   272
  end
cezarykaliszyk@47258
   273
cezarykaliszyk@47258
   274
fun inst sigma th =
cezarykaliszyk@47258
   275
  let
cezarykaliszyk@47258
   276
    val (dom, rng) = ListPair.unzip (rev sigma)
cezarykaliszyk@47258
   277
  in
cezarykaliszyk@47258
   278
    th |> forall_intr_list dom
cezarykaliszyk@47258
   279
       |> forall_elim_list rng
cezarykaliszyk@47258
   280
  end
cezarykaliszyk@47258
   281
cezarykaliszyk@47258
   282
fun transl_dotc #"." = "dot"
cezarykaliszyk@47258
   283
  | transl_dotc c = Char.toString c
cezarykaliszyk@47258
   284
val transl_dot = String.translate transl_dotc
cezarykaliszyk@47258
   285
cezarykaliszyk@47258
   286
fun transl_qmc #"?" = "t"
cezarykaliszyk@47258
   287
  | transl_qmc c = Char.toString c
cezarykaliszyk@47258
   288
val transl_qm = String.translate transl_qmc
cezarykaliszyk@47258
   289
cezarykaliszyk@47258
   290
fun getconstname s thy =
cezarykaliszyk@47258
   291
  case Import_Data.get_const_map s thy of
cezarykaliszyk@47258
   292
      SOME s => s
cezarykaliszyk@47258
   293
    | NONE => Sign.full_name thy (Binding.name (transl_dot s))
cezarykaliszyk@47258
   294
fun gettyname s thy =
cezarykaliszyk@47258
   295
  case Import_Data.get_typ_map s thy of
cezarykaliszyk@47258
   296
    SOME s => s
cezarykaliszyk@47258
   297
  | NONE => Sign.full_name thy (Binding.name s)
cezarykaliszyk@47258
   298
cezarykaliszyk@47258
   299
fun get (map, no) s =
cezarykaliszyk@47258
   300
  case Int.fromString s of
cezarykaliszyk@47258
   301
    NONE => error "Import_Rule.get: not a number"
cezarykaliszyk@47258
   302
  | SOME i => (case Inttab.lookup map (Int.abs i) of
cezarykaliszyk@47258
   303
      NONE => error "Import_Rule.get: lookup failed"
cezarykaliszyk@47258
   304
    | SOME res => (res, (if i < 0 then Inttab.delete (Int.abs i) map else map, no)))
cezarykaliszyk@47258
   305
cezarykaliszyk@47258
   306
fun getty i (thy, (tyi, tmi, thi)) = let val (i, tyi) = (get tyi i) in (i, (thy, (tyi, tmi, thi))) end
cezarykaliszyk@47258
   307
fun gettm i (thy, (tyi, tmi, thi)) = let val (i, tmi) = (get tmi i) in (i, (thy, (tyi, tmi, thi))) end
cezarykaliszyk@47258
   308
fun getth i (thy, (tyi, tmi, thi)) = let val (i, thi) = (get thi i) in (i, (thy, (tyi, tmi, thi))) end
cezarykaliszyk@47258
   309
fun set (map, no) v = (Inttab.update_new (no + 1, v) map, no + 1)
cezarykaliszyk@47258
   310
fun setty v (thy, (tyi, tmi, thi)) = (thy, (set tyi v, tmi, thi))
cezarykaliszyk@47258
   311
fun settm v (thy, (tyi, tmi, thi)) = (thy, (tyi, set tmi v, thi))
cezarykaliszyk@47258
   312
fun setth v (thy, (tyi, tmi, thi)) = (thy, (tyi, tmi, set thi v))
cezarykaliszyk@47258
   313
cezarykaliszyk@47258
   314
fun last_thm (_, _, (map, no)) =
cezarykaliszyk@47258
   315
  case Inttab.lookup map no of
cezarykaliszyk@47258
   316
    NONE => error "Import_Rule.last_thm: lookup failed"
cezarykaliszyk@47258
   317
  | SOME thm => thm
cezarykaliszyk@47258
   318
cezarykaliszyk@47258
   319
fun listLast (h1 :: (h2 :: t)) = apfst (fn t => h1 :: h2 :: t) (listLast t)
cezarykaliszyk@47258
   320
  | listLast [p] = ([], p)
cezarykaliszyk@47258
   321
  | listLast [] = error "listLast: empty"
cezarykaliszyk@47258
   322
cezarykaliszyk@47258
   323
fun pairList (h1 :: (h2 :: t)) = ((h1, h2) :: pairList t)
cezarykaliszyk@47258
   324
  | pairList [] = []
cezarykaliszyk@47258
   325
  | pairList _ = error "pairList: odd list length"
cezarykaliszyk@47258
   326
cezarykaliszyk@47258
   327
fun store_thm binding thm thy =
cezarykaliszyk@47258
   328
  let
cezarykaliszyk@47258
   329
    val thm = Drule.export_without_context_open thm
cezarykaliszyk@47258
   330
    val tvs = Term.add_tvars (prop_of thm) []
cezarykaliszyk@47258
   331
    val tns = map (fn (_, _) => "'") tvs
cezarykaliszyk@47258
   332
    val nms = fst (fold_map Name.variant tns (Variable.names_of (Proof_Context.init_global thy)))
cezarykaliszyk@47258
   333
    val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
cezarykaliszyk@47258
   334
    val cvs = map (ctyp_of thy) vs
cezarykaliszyk@47258
   335
    val ctvs = map (ctyp_of thy) (map TVar tvs)
cezarykaliszyk@47258
   336
    val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
cezarykaliszyk@47258
   337
  in
cezarykaliszyk@47258
   338
    snd (Global_Theory.add_thm ((binding, thm'), []) thy)
cezarykaliszyk@47258
   339
  end
cezarykaliszyk@47258
   340
krauss@47371
   341
fun log_timestamp () =
krauss@47371
   342
  let
krauss@47371
   343
    val time = Time.now ()
krauss@47371
   344
    val millis = nth (space_explode "." (Time.fmt 3 time)) 1
krauss@47371
   345
  in
krauss@47371
   346
    Date.fmt "%d.%m.%Y %H:%M:%S." (Date.fromTimeLocal time) ^ millis
krauss@47371
   347
  end
krauss@47371
   348
cezarykaliszyk@47258
   349
fun process_line str tstate =
cezarykaliszyk@47258
   350
  let
cezarykaliszyk@47258
   351
    fun process tstate (#"R", [t]) = gettm t tstate |>> refl |-> setth
cezarykaliszyk@47258
   352
      | process tstate (#"B", [t]) = gettm t tstate |>> beta |-> setth
cezarykaliszyk@47258
   353
      | process tstate (#"1", [th]) = getth th tstate |>> conj1 |-> setth
cezarykaliszyk@47258
   354
      | process tstate (#"2", [th]) = getth th tstate |>> conj2 |-> setth
cezarykaliszyk@47258
   355
      | process tstate (#"H", [t]) =
cezarykaliszyk@47258
   356
          gettm t tstate |>> Thm.apply @{cterm Trueprop} |>> Thm.trivial |-> setth
cezarykaliszyk@47258
   357
      | process tstate (#"A", [_, t]) =
cezarykaliszyk@47258
   358
          gettm t tstate |>> Thm.apply @{cterm Trueprop} |>> Skip_Proof.make_thm_cterm |-> setth
cezarykaliszyk@47258
   359
      | process tstate (#"C", [th1, th2]) =
cezarykaliszyk@47258
   360
          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => comb t1 t2) |-> setth
cezarykaliszyk@47258
   361
      | process tstate (#"T", [th1, th2]) =
cezarykaliszyk@47258
   362
          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => trans t1 t2) |-> setth
cezarykaliszyk@47258
   363
      | process tstate (#"E", [th1, th2]) =
cezarykaliszyk@47258
   364
          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => eq_mp t1 t2) |-> setth
cezarykaliszyk@47258
   365
      | process tstate (#"D", [th1, th2]) =
cezarykaliszyk@47258
   366
          getth th1 tstate ||>> getth th2 |>> (fn (t1, t2) => deduct t1 t2) |-> setth
cezarykaliszyk@47258
   367
      | process tstate (#"L", [t, th]) =
cezarykaliszyk@47258
   368
          gettm t tstate ||>> (fn ti => getth th ti) |>> (fn (tm, th) => abs tm th) |-> setth
cezarykaliszyk@47258
   369
      | process (thy, state) (#"M", [s]) =
cezarykaliszyk@47258
   370
          let
cezarykaliszyk@47258
   371
            val ctxt = Variable.set_body false (Proof_Context.init_global thy)
cezarykaliszyk@47258
   372
            val thm = freezeT (Global_Theory.get_thm thy s)
cezarykaliszyk@47258
   373
            val ((_, [th']), _) = Variable.import true [thm] ctxt
cezarykaliszyk@47258
   374
          in
cezarykaliszyk@47258
   375
            setth th' (thy, state)
cezarykaliszyk@47258
   376
          end
cezarykaliszyk@47258
   377
      | process (thy, state) (#"Q", l) =
cezarykaliszyk@47258
   378
          let
cezarykaliszyk@47258
   379
            val (tys, th) = listLast l
cezarykaliszyk@47258
   380
            val (th, tstate) = getth th (thy, state)
cezarykaliszyk@47258
   381
            val (tys, tstate) = fold_map getty tys tstate
cezarykaliszyk@47258
   382
          in
cezarykaliszyk@47258
   383
            setth (inst_type (pairList tys) th thy) tstate
cezarykaliszyk@47258
   384
          end
cezarykaliszyk@47258
   385
      | process tstate (#"S", l) =
cezarykaliszyk@47258
   386
          let
cezarykaliszyk@47258
   387
            val (tms, th) = listLast l
cezarykaliszyk@47258
   388
            val (th, tstate) = getth th tstate
cezarykaliszyk@47258
   389
            val (tms, tstate) = fold_map gettm tms tstate
cezarykaliszyk@47258
   390
          in
cezarykaliszyk@47258
   391
            setth (inst (pairList tms) th) tstate
cezarykaliszyk@47258
   392
          end
cezarykaliszyk@47258
   393
      | process tstate (#"F", [name, t]) =
cezarykaliszyk@47258
   394
          let
cezarykaliszyk@47258
   395
            val (tm, (thy, state)) = gettm t tstate
cezarykaliszyk@47258
   396
            val (th, thy) = def (transl_dot name) tm thy
cezarykaliszyk@47258
   397
          in
cezarykaliszyk@47258
   398
            setth th (thy, state)
cezarykaliszyk@47258
   399
          end
cezarykaliszyk@47258
   400
      | process (thy, state) (#"F", [name]) = setth (mdef name thy) (thy, state)
cezarykaliszyk@47258
   401
      | process tstate (#"Y", [name, absname, repname, t1, t2, th]) =
cezarykaliszyk@47258
   402
          let
cezarykaliszyk@47258
   403
            val (th, tstate) = getth th tstate
cezarykaliszyk@47258
   404
            val (t1, tstate) = gettm t1 tstate
cezarykaliszyk@47258
   405
            val (t2, (thy, state)) = gettm t2 tstate
cezarykaliszyk@47258
   406
            val (th, thy) = tydef name absname repname t1 t2 th thy
cezarykaliszyk@47258
   407
          in
cezarykaliszyk@47258
   408
            setth th (thy, state)
cezarykaliszyk@47258
   409
          end
cezarykaliszyk@47258
   410
      | process (thy, state) (#"Y", [name, _, _]) = setth (mtydef name thy) (thy, state)
cezarykaliszyk@47258
   411
      | process (thy, state) (#"t", [n]) =
cezarykaliszyk@47258
   412
          setty (ctyp_of thy (TFree ("'" ^ (transl_qm n), ["HOL.type"]))) (thy, state)
cezarykaliszyk@47258
   413
      | process (thy, state) (#"a", n :: l) =
cezarykaliszyk@47258
   414
          fold_map getty l (thy, state) |>>
cezarykaliszyk@47258
   415
            (fn tys => ctyp_of thy (Type (gettyname n thy, map typ_of tys))) |-> setty
cezarykaliszyk@47258
   416
      | process (thy, state) (#"v", [n, ty]) =
cezarykaliszyk@47258
   417
          getty ty (thy, state) |>> (fn ty => cterm_of thy (Free (transl_dot n, typ_of ty))) |-> settm
cezarykaliszyk@47258
   418
      | process (thy, state) (#"c", [n, ty]) =
cezarykaliszyk@47258
   419
          getty ty (thy, state) |>> (fn ty => cterm_of thy (Const (getconstname n thy, typ_of ty))) |-> settm
cezarykaliszyk@47258
   420
      | process tstate (#"f", [t1, t2]) =
cezarykaliszyk@47258
   421
          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.apply t1 t2) |-> settm
cezarykaliszyk@47258
   422
      | process tstate (#"l", [t1, t2]) =
cezarykaliszyk@47258
   423
          gettm t1 tstate ||>> gettm t2 |>> (fn (t1, t2) => Thm.lambda t1 t2) |-> settm
cezarykaliszyk@47258
   424
      | process (thy, state) (#"+", [s]) =
cezarykaliszyk@47258
   425
          let
krauss@47371
   426
            val _ = tracing ("NOTING " ^ log_timestamp () ^ ": " ^ s)
cezarykaliszyk@47258
   427
          in
cezarykaliszyk@47258
   428
            (store_thm (Binding.name (transl_dot s)) (last_thm state) thy, state)
cezarykaliszyk@47258
   429
          end
cezarykaliszyk@47258
   430
      | process _ (c, _) = error ("process: unknown command: " ^ String.implode [c])
cezarykaliszyk@47258
   431
cezarykaliszyk@47258
   432
    fun parse_line s =
cezarykaliszyk@47258
   433
        case String.tokens (fn x => (x = #"\n" orelse x = #" ")) s of
cezarykaliszyk@47258
   434
          [] => error "parse_line: empty"
cezarykaliszyk@47258
   435
        | h :: t => (case String.explode h of
cezarykaliszyk@47258
   436
            [] => error "parse_line: empty command"
cezarykaliszyk@47258
   437
          | sh :: st => (sh, (String.implode st) :: t))
cezarykaliszyk@47258
   438
  in
cezarykaliszyk@47258
   439
    process tstate (parse_line str)
cezarykaliszyk@47258
   440
  end
cezarykaliszyk@47258
   441
cezarykaliszyk@47258
   442
fun process_file path thy =
cezarykaliszyk@47258
   443
  (thy, init_state) |> File.fold_lines process_line path |> fst
cezarykaliszyk@47258
   444
cezarykaliszyk@47258
   445
val _ = Outer_Syntax.command @{command_spec "import_file"}
wenzelm@48881
   446
  "Import a recorded proof file"
wenzelm@48881
   447
  (Parse.path >> (fn name => Toplevel.theory (fn thy => process_file (Path.explode name) thy)))
cezarykaliszyk@47258
   448
cezarykaliszyk@47258
   449
cezarykaliszyk@47258
   450
end