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