src/HOL/Import/hol4rews.ML
author wenzelm
Sat Mar 29 19:14:03 2008 +0100 (2008-03-29)
changeset 26481 92e901171cc8
parent 22846 fb79144af9a3
child 26928 ca87aff1ad2d
permissions -rw-r--r--
simplified PureThy.store_thm;
     1 (*  Title:      HOL/Import/hol4rews.ML
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
     7 
     8 type holthm = (term * term) list * thm
     9 
    10 datatype ImportStatus =
    11 	 NoImport
    12        | Generating of string
    13        | Replaying of string
    14 
    15 structure HOL4DefThy = TheoryDataFun
    16 (
    17   type T = ImportStatus
    18   val empty = NoImport
    19   val copy = I
    20   val extend = I
    21   fun merge _ (NoImport,NoImport) = NoImport
    22     | merge _ _ = (warning "Import status set during merge"; NoImport)
    23 )
    24 
    25 structure ImportSegment = TheoryDataFun
    26 (
    27   type T = string
    28   val empty = ""
    29   val copy = I
    30   val extend = I
    31   fun merge _ ("",arg) = arg
    32     | merge _ (arg,"") = arg
    33     | merge _ (s1,s2) =
    34       if s1 = s2
    35       then s1
    36       else error "Trying to merge two different import segments"
    37 )
    38 
    39 val get_import_segment = ImportSegment.get
    40 val set_import_segment = ImportSegment.put
    41 
    42 structure HOL4UNames = TheoryDataFun
    43 (
    44   type T = string list
    45   val empty = []
    46   val copy = I
    47   val extend = I
    48   fun merge _ ([],[]) = []
    49     | merge _ _ = error "Used names not empty during merge"
    50 )
    51 
    52 structure HOL4Dump = TheoryDataFun
    53 (
    54   type T = string * string * string list
    55   val empty = ("","",[])
    56   val copy = I
    57   val extend = I
    58   fun merge _ (("","",[]),("","",[])) = ("","",[])
    59     | merge _ _ = error "Dump data not empty during merge"
    60 )
    61 
    62 structure HOL4Moves = TheoryDataFun
    63 (
    64   type T = string Symtab.table
    65   val empty = Symtab.empty
    66   val copy = I
    67   val extend = I
    68   fun merge _ : T * T -> T = Symtab.merge (K true)
    69 )
    70 
    71 structure HOL4Imports = TheoryDataFun
    72 (
    73   type T = string Symtab.table
    74   val empty = Symtab.empty
    75   val copy = I
    76   val extend = I
    77   fun merge _ : T * T -> T = Symtab.merge (K true)
    78 )
    79 
    80 fun get_segment2 thyname thy =
    81   Symtab.lookup (HOL4Imports.get thy) thyname
    82 
    83 fun set_segment thyname segname thy =
    84     let
    85 	val imps = HOL4Imports.get thy
    86 	val imps' = Symtab.update_new (thyname,segname) imps
    87     in
    88 	HOL4Imports.put imps' thy
    89     end
    90 
    91 structure HOL4CMoves = TheoryDataFun
    92 (
    93   type T = string Symtab.table
    94   val empty = Symtab.empty
    95   val copy = I
    96   val extend = I
    97   fun merge _ : T * T -> T = Symtab.merge (K true)
    98 )
    99 
   100 structure HOL4Maps = TheoryDataFun
   101 (
   102   type T = (string option) StringPair.table
   103   val empty = StringPair.empty
   104   val copy = I
   105   val extend = I
   106   fun merge _ : T * T -> T = StringPair.merge (K true)
   107 )
   108 
   109 structure HOL4Thms = TheoryDataFun
   110 (
   111   type T = holthm StringPair.table
   112   val empty = StringPair.empty
   113   val copy = I
   114   val extend = I
   115   fun merge _ : T * T -> T = StringPair.merge (K true)
   116 )
   117 
   118 structure HOL4ConstMaps = TheoryDataFun
   119 (
   120   type T = (bool * string * typ option) StringPair.table
   121   val empty = StringPair.empty
   122   val copy = I
   123   val extend = I
   124   fun merge _ : T * T -> T = StringPair.merge (K true)
   125 )
   126 
   127 structure HOL4Rename = TheoryDataFun
   128 (
   129   type T = string StringPair.table
   130   val empty = StringPair.empty
   131   val copy = I
   132   val extend = I
   133   fun merge _ : T * T -> T = StringPair.merge (K true)
   134 )
   135 
   136 structure HOL4DefMaps = TheoryDataFun
   137 (
   138   type T = string StringPair.table
   139   val empty = StringPair.empty
   140   val copy = I
   141   val extend = I
   142   fun merge _ : T * T -> T = StringPair.merge (K true)
   143 )
   144 
   145 structure HOL4TypeMaps = TheoryDataFun
   146 (
   147   type T = (bool * string) StringPair.table
   148   val empty = StringPair.empty
   149   val copy = I
   150   val extend = I
   151   fun merge _ : T * T -> T = StringPair.merge (K true)
   152 )
   153 
   154 structure HOL4Pending = TheoryDataFun
   155 (
   156   type T = ((term * term) list * thm) StringPair.table
   157   val empty = StringPair.empty
   158   val copy = I
   159   val extend = I
   160   fun merge _ : T * T -> T = StringPair.merge (K true)
   161 )
   162 
   163 structure HOL4Rewrites = TheoryDataFun
   164 (
   165   type T = thm list
   166   val empty = []
   167   val copy = I
   168   val extend = I
   169   fun merge _ = Library.gen_union Thm.eq_thm
   170 )
   171 
   172 val hol4_debug = ref false
   173 fun message s = if !hol4_debug then writeln s else ()
   174 
   175 local
   176   val eq_reflection = thm "eq_reflection"
   177 in
   178 fun add_hol4_rewrite (Context.Theory thy, th) =
   179     let
   180 	val _ = message "Adding HOL4 rewrite"
   181 	val th1 = th RS eq_reflection
   182 	val current_rews = HOL4Rewrites.get thy
   183 	val new_rews = insert Thm.eq_thm th1 current_rews
   184 	val updated_thy  = HOL4Rewrites.put new_rews thy
   185     in
   186 	(Context.Theory updated_thy,th1)
   187     end
   188   | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
   189 end
   190 
   191 fun ignore_hol4 bthy bthm thy =
   192     let
   193 	val _ = message ("Ignoring " ^ bthy ^ "." ^ bthm)
   194 	val curmaps = HOL4Maps.get thy
   195 	val newmaps = StringPair.update_new ((bthy,bthm),NONE) curmaps
   196 	val upd_thy = HOL4Maps.put newmaps thy
   197     in
   198 	upd_thy
   199     end
   200 
   201 val opt_get_output_thy = #2 o HOL4Dump.get
   202 
   203 fun get_output_thy thy =
   204     case #2 (HOL4Dump.get thy) of
   205 	"" => error "No theory file being output"
   206       | thyname => thyname
   207 
   208 val get_output_dir = #1 o HOL4Dump.get
   209 
   210 fun add_hol4_move bef aft thy =
   211     let
   212 	val curmoves = HOL4Moves.get thy
   213 	val newmoves = Symtab.update_new (bef, aft) curmoves
   214     in
   215 	HOL4Moves.put newmoves thy
   216     end
   217 
   218 fun get_hol4_move bef thy =
   219   Symtab.lookup (HOL4Moves.get thy) bef
   220 
   221 fun follow_name thmname thy =
   222     let
   223 	val moves = HOL4Moves.get thy
   224 	fun F thmname =
   225 	    case Symtab.lookup moves thmname of
   226 		SOME name => F name
   227 	      | NONE => thmname
   228     in
   229 	F thmname
   230     end
   231 
   232 fun add_hol4_cmove bef aft thy =
   233     let
   234 	val curmoves = HOL4CMoves.get thy
   235 	val newmoves = Symtab.update_new (bef, aft) curmoves
   236     in
   237 	HOL4CMoves.put newmoves thy
   238     end
   239 
   240 fun get_hol4_cmove bef thy =
   241   Symtab.lookup (HOL4CMoves.get thy) bef
   242 
   243 fun follow_cname thmname thy =
   244     let
   245 	val moves = HOL4CMoves.get thy
   246 	fun F thmname =
   247 	    case Symtab.lookup moves thmname of
   248 		SOME name => F name
   249 	      | NONE => thmname
   250     in
   251 	F thmname
   252     end
   253 
   254 fun add_hol4_mapping bthy bthm isathm thy =
   255     let	
   256        (* val _ = writeln ("Before follow_name: "^isathm)  *)
   257       val isathm = follow_name isathm thy
   258        (* val _ = writeln ("Adding theorem map: " ^ bthy ^ "." ^ bthm ^ " --> " ^ isathm)*)
   259 	val curmaps = HOL4Maps.get thy
   260 	val newmaps = StringPair.update_new ((bthy,bthm),SOME isathm) curmaps
   261 	val upd_thy = HOL4Maps.put newmaps thy
   262     in
   263 	upd_thy
   264     end;
   265 
   266 fun get_hol4_type_mapping bthy tycon thy =
   267     let
   268 	val maps = HOL4TypeMaps.get thy
   269     in
   270 	StringPair.lookup maps (bthy,tycon)
   271     end
   272 
   273 fun get_hol4_mapping bthy bthm thy =
   274     let
   275 	val curmaps = HOL4Maps.get thy
   276     in
   277 	StringPair.lookup curmaps (bthy,bthm)
   278     end;
   279 
   280 fun add_hol4_const_mapping bthy bconst internal isaconst thy =
   281     let
   282 	val thy = case opt_get_output_thy thy of
   283 		      "" => thy
   284 		    | output_thy => if internal
   285 				    then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   286 				    else thy
   287 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   288 	val curmaps = HOL4ConstMaps.get thy
   289 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,NONE)) curmaps
   290 	val upd_thy = HOL4ConstMaps.put newmaps thy
   291     in
   292 	upd_thy
   293     end;
   294 
   295 fun add_hol4_const_renaming bthy bconst newname thy =
   296     let
   297 	val currens = HOL4Rename.get thy
   298 	val _ = message ("Adding renaming " ^ bthy ^ "." ^ bconst ^ " -> " ^ newname)
   299 	val newrens = StringPair.update_new ((bthy,bconst),newname) currens
   300 	val upd_thy = HOL4Rename.put newrens thy
   301     in
   302 	upd_thy
   303     end;
   304 
   305 fun get_hol4_const_renaming bthy bconst thy =
   306     let
   307 	val currens = HOL4Rename.get thy
   308     in
   309 	StringPair.lookup currens (bthy,bconst)
   310     end;
   311 
   312 fun get_hol4_const_mapping bthy bconst thy =
   313     let
   314 	val bconst = case get_hol4_const_renaming bthy bconst thy of
   315 			 SOME name => name
   316 		       | NONE => bconst
   317 	val maps = HOL4ConstMaps.get thy
   318     in
   319 	StringPair.lookup maps (bthy,bconst)
   320     end
   321 
   322 fun add_hol4_const_wt_mapping bthy bconst internal isaconst typ thy =
   323     let
   324 	val thy = case opt_get_output_thy thy of
   325 		      "" => thy
   326 		    | output_thy => if internal
   327 				    then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
   328 				    else thy
   329 	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   330 	val curmaps = HOL4ConstMaps.get thy
   331 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst,SOME typ)) curmaps
   332 	val upd_thy = HOL4ConstMaps.put newmaps thy
   333     in
   334 	upd_thy
   335     end;
   336 
   337 fun add_hol4_type_mapping bthy bconst internal isaconst thy =
   338     let
   339 	val curmaps = HOL4TypeMaps.get thy
   340 	val _ = writeln ("Adding tmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
   341 	val newmaps = StringPair.update_new ((bthy,bconst),(internal,isaconst)) curmaps
   342                handle x => let val (internal, isaconst') = the (StringPair.lookup curmaps (bthy, bconst)) in
   343                       warning ("couldn't map type "^bthy^"."^bconst^" to "^isaconst^": already mapped to "^isaconst'); raise x end
   344         val upd_thy = HOL4TypeMaps.put newmaps thy
   345     in
   346 	upd_thy
   347     end;
   348 
   349 fun add_hol4_pending bthy bthm hth thy =
   350     let
   351 	val thmname = Sign.full_name thy bthm
   352 	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
   353 	val curpend = HOL4Pending.get thy
   354 	val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
   355 	val upd_thy = HOL4Pending.put newpend thy
   356 	val thy' = case opt_get_output_thy upd_thy of
   357 		       "" => add_hol4_mapping bthy bthm thmname upd_thy
   358 		     | output_thy =>
   359 		       let
   360 			   val new_thmname = output_thy ^ "." ^ bthy ^ "." ^ bthm
   361 		       in
   362 			   upd_thy |> add_hol4_move thmname new_thmname
   363 				   |> add_hol4_mapping bthy bthm new_thmname
   364 		       end
   365     in
   366 	thy'
   367     end;
   368 
   369 fun get_hol4_theorem thyname thmname thy =
   370   let
   371     val isathms = HOL4Thms.get thy
   372   in
   373     StringPair.lookup isathms (thyname,thmname)
   374   end;
   375 
   376 fun add_hol4_theorem thyname thmname hth =
   377   let
   378     val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
   379   in
   380     HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
   381   end;
   382 
   383 fun export_hol4_pending thy =
   384   let
   385     val rews = HOL4Rewrites.get thy;
   386     val pending = HOL4Pending.get thy;
   387     fun process ((bthy,bthm), hth as (_,thm)) thy =
   388       let
   389         val thm1 = rewrite_rule (map (Thm.transfer thy) rews) (Thm.transfer thy thm);
   390         val thm2 = standard thm1;
   391       in
   392         thy
   393         |> PureThy.store_thm (bthm, thm2)
   394         |> snd
   395         |> add_hol4_theorem bthy bthm hth
   396       end;
   397   in
   398     thy
   399     |> StringPair.fold process pending
   400     |> HOL4Pending.put StringPair.empty
   401   end;
   402 
   403 fun setup_dump (dir,thyname) thy =
   404     HOL4Dump.put (dir,thyname,["(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)"]) thy
   405 
   406 fun add_dump str thy =
   407     let
   408 	val (dir,thyname,curdump) = HOL4Dump.get thy
   409     in
   410 	HOL4Dump.put (dir,thyname,str::curdump) thy
   411     end
   412 
   413 fun flush_dump thy =
   414     let
   415 	val (dir,thyname,dumpdata) = HOL4Dump.get thy
   416 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=dir,
   417 						      file=thyname ^ ".thy"})
   418 	val _  = app (fn s => TextIO.output(os,s ^ "\n\n")) (rev dumpdata)
   419 	val  _ = TextIO.closeOut os
   420     in
   421 	HOL4Dump.put ("","",[]) thy
   422     end
   423 
   424 fun set_generating_thy thyname thy =
   425     case HOL4DefThy.get thy of
   426 	NoImport => HOL4DefThy.put (Generating thyname) thy
   427       | _ => error "Import already in progess"
   428 
   429 fun set_replaying_thy thyname thy =
   430     case HOL4DefThy.get thy of
   431 	NoImport => HOL4DefThy.put (Replaying thyname) thy
   432       | _ => error "Import already in progess"
   433 
   434 fun clear_import_thy thy =
   435     case HOL4DefThy.get thy of
   436 	NoImport => error "No import in progress"
   437       | _ => HOL4DefThy.put NoImport thy
   438 
   439 fun get_generating_thy thy =
   440     case HOL4DefThy.get thy of
   441 	Generating thyname => thyname
   442       | _ => error "No theory being generated"
   443 
   444 fun get_replaying_thy thy =
   445     case HOL4DefThy.get thy of
   446 	Replaying thyname => thyname
   447       | _ => error "No theory being replayed"
   448 
   449 fun get_import_thy thy =
   450     case HOL4DefThy.get thy of
   451 	Replaying thyname => thyname
   452       | Generating thyname => thyname
   453       | _ => error "No theory being imported"
   454 
   455 fun should_ignore thyname thy thmname =
   456     case get_hol4_mapping thyname thmname thy of
   457 	SOME NONE => true 
   458       | _ => false
   459 
   460 val trans_string =
   461     let
   462 	fun quote s = "\"" ^ s ^ "\""
   463 	fun F [] = []
   464 	  | F (#"\\" :: cs) = patch #"\\" cs
   465 	  | F (#"\"" :: cs) = patch #"\"" cs
   466 	  | F (c     :: cs) = c :: F cs
   467 	and patch c rest = #"\\" :: c :: F rest
   468     in
   469 	quote o String.implode o F o String.explode
   470     end
   471 
   472 fun dump_import_thy thyname thy =
   473     let
   474 	val output_dir = get_output_dir thy
   475 	val output_thy = get_output_thy thy
   476 	val input_thy = Context.theory_name thy
   477 	val import_segment = get_import_segment thy
   478 	val os = TextIO.openOut (OS.Path.joinDirFile {dir=output_dir,
   479 						      file=thyname ^ ".imp"})
   480 	fun out s = TextIO.output(os,s)
   481     val (ignored, mapped) = StringPair.fold
   482       (fn ((bthy, bthm), v) => fn (ign, map) =>
   483         if bthy = thyname
   484         then case v
   485          of NONE => (bthm :: ign, map)
   486           | SOME w => (ign, (bthm, w) :: map)
   487         else (ign, map)) (HOL4Maps.get thy) ([],[]);
   488     fun mk init = StringPair.fold
   489       (fn ((bthy, bthm), v) => if bthy = thyname then cons (bthm, v) else I) init [];
   490     val constmaps = mk (HOL4ConstMaps.get thy);
   491     val constrenames = mk (HOL4Rename.get thy);
   492     val typemaps = mk (HOL4TypeMaps.get thy);
   493     val defmaps = mk (HOL4DefMaps.get thy);
   494 	fun new_name internal isa =
   495 	    if internal
   496 	    then
   497 		let
   498 		    val paths = NameSpace.explode isa
   499 		    val i = Library.drop(length paths - 2,paths)
   500 		in
   501 		    case i of
   502 			[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
   503 		      | _ => error "hol4rews.dump internal error"
   504 		end
   505 	    else
   506 		isa
   507 
   508 	val _ = out "import\n\n"
   509 
   510 	val _ = out ("import_segment " ^ trans_string import_segment ^ "\n\n")
   511 	val _ = if null defmaps
   512 		then ()
   513 		else out "def_maps"
   514 	val _ = app (fn (hol,isa) =>
   515 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string isa))) defmaps
   516 	val _ = if null defmaps
   517 		then ()
   518 		else out "\n\n"
   519 
   520 	val _ = if null typemaps
   521 		then ()
   522 		else out "type_maps"
   523 	val _ = app (fn (hol,(internal,isa)) =>
   524 			out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (new_name internal isa)))) typemaps
   525 	val _ = if null typemaps
   526 		then ()
   527 		else out "\n\n"
   528 
   529 	val _ = if null constmaps
   530 		then ()
   531 		else out "const_maps"
   532 	val _ = app (fn (hol,(internal,isa,opt_ty)) =>
   533 			(out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (follow_cname isa thy)));
   534 			 case opt_ty of
   535 			     SOME ty => out (" :: \"" ^ (string_of_ctyp (ctyp_of thy ty)) ^ "\"")
   536 			   | NONE => ())) constmaps
   537 	val _ = if null constmaps
   538 		then ()
   539 		else out "\n\n"
   540 
   541 	val _ = if null constrenames
   542 		then ()
   543 		else out "const_renames"
   544 	val _ = app (fn (old,new) =>
   545 			out ("\n  " ^ (trans_string old) ^ " > " ^ (trans_string new))) constrenames
   546 	val _ = if null constrenames
   547 		then ()
   548 		else out "\n\n"
   549 
   550 	fun gen2replay in_thy out_thy s = 
   551 	    let
   552 		val ss = NameSpace.explode s
   553 	    in
   554 		if (hd ss = in_thy) then 
   555 		    NameSpace.implode (out_thy::(tl ss))
   556 		else
   557 		    s
   558 	    end 
   559 
   560 	val _ = if null mapped
   561 		then ()
   562 		else out "thm_maps"
   563 	val _ = app (fn (hol,isa) => out ("\n  " ^ (trans_string hol) ^ " > " ^ (trans_string (gen2replay input_thy output_thy isa)))) mapped
   564 	val _ = if null mapped 
   565 		then ()
   566 		else out "\n\n"
   567 
   568 	val _ = if null ignored
   569 		then ()
   570 		else out "ignore_thms"
   571 	val _ = app (fn ign => out ("\n  " ^ (trans_string ign))) ignored
   572 	val _ = if null ignored
   573 		then ()
   574 		else out "\n\n"
   575 
   576 	val _ = out "end\n"
   577 	val _ = TextIO.closeOut os
   578     in
   579 	thy
   580     end
   581 
   582 fun set_used_names names thy =
   583     let
   584 	val unames = HOL4UNames.get thy
   585     in
   586 	case unames of
   587 	    [] => HOL4UNames.put names thy
   588 	  | _ => error "hol4rews.set_used_names called on initialized data!"
   589     end
   590 
   591 val clear_used_names = HOL4UNames.put [];
   592 
   593 fun get_defmap thyname const thy =
   594     let
   595 	val maps = HOL4DefMaps.get thy
   596     in
   597 	StringPair.lookup maps (thyname,const)
   598     end
   599 
   600 fun add_defmap thyname const defname thy =
   601     let
   602 	val _ = message ("Adding defmap " ^ thyname ^ "." ^ const ^ " --> " ^ defname)
   603 	val maps = HOL4DefMaps.get thy
   604 	val maps' = StringPair.update_new ((thyname,const),defname) maps
   605 	val thy' = HOL4DefMaps.put maps' thy
   606     in
   607 	thy'
   608     end
   609 
   610 fun get_defname thyname name thy =
   611     let
   612 	val maps = HOL4DefMaps.get thy
   613 	fun F dname = (dname,add_defmap thyname name dname thy)
   614     in
   615 	case StringPair.lookup maps (thyname,name) of
   616 	    SOME thmname => (thmname,thy)
   617 	  | NONE =>
   618 	    let
   619 		val used = HOL4UNames.get thy
   620 		val defname = def_name name
   621 		val pdefname = name ^ "_primdef"
   622 	    in
   623 		if not (defname mem used)
   624 		then F defname                 (* name_def *)
   625 		else if not (pdefname mem used)
   626 		then F pdefname                (* name_primdef *)
   627 		else F (Name.variant used pdefname) (* last resort *)
   628 	    end
   629     end
   630 
   631 local
   632     fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==", _],_,_]] = x
   633       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "all", _],_]] = x
   634       | handle_meta [x as Appl[Appl[Constant "_constrain", Constant "==>", _],_,_]] = x
   635       | handle_meta [x] = Appl[Constant "Trueprop",x]
   636       | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
   637 in
   638 val smarter_trueprop_parsing = [("Trueprop",handle_meta)]
   639 end
   640 
   641 local
   642     fun initial_maps thy =
   643 	thy |> add_hol4_type_mapping "min" "bool" false "bool"
   644 	    |> add_hol4_type_mapping "min" "fun" false "fun"
   645 	    |> add_hol4_type_mapping "min" "ind" false "Nat.ind"
   646 	    |> add_hol4_const_mapping "min" "=" false "op ="
   647 	    |> add_hol4_const_mapping "min" "==>" false "op -->"
   648 	    |> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
   649 in
   650 val hol4_setup =
   651   initial_maps #>
   652   Attrib.add_attributes
   653     [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
   654 end