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