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