110 val new_specification : string -> string -> string list -> thm -> theory -> theory * thm |
110 val new_specification : string -> string -> string list -> thm -> theory -> theory * thm |
111 val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm |
111 val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm |
112 val new_axiom : string -> term -> theory -> theory * thm |
112 val new_axiom : string -> term -> theory -> theory * thm |
113 |
113 |
114 val prin : term -> unit |
114 val prin : term -> unit |
115 val protect_factname : string -> string |
115 val protect_factname : string -> string |
|
116 val replay_protect_varname : string -> string -> unit |
116 end |
117 end |
117 |
118 |
118 structure ProofKernel :> ProofKernel = |
119 structure ProofKernel :> ProofKernel = |
119 struct |
120 struct |
120 type hol_type = Term.typ |
121 type hol_type = Term.typ |
478 SOME t => t |
479 SOME t => t |
479 | NONE => |
480 | NONE => |
480 let |
481 let |
481 val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) |
482 val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) |
482 val t = "u_"^(IntInf.toString (!invented_isavar)) |
483 val t = "u_"^(IntInf.toString (!invented_isavar)) |
|
484 val _ = ImportRecorder.protect_varname s t |
483 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) |
485 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) |
484 in |
486 in |
485 t |
487 t |
486 end |
488 end |
487 |
489 |
|
490 exception REPLAY_PROTECT_VARNAME of string*string*string |
|
491 |
|
492 fun replay_protect_varname s t = |
|
493 case Symtab.lookup (!protected_varnames) s of |
|
494 SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') |
|
495 | NONE => |
|
496 let |
|
497 val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) |
|
498 val t = "u_"^(IntInf.toString (!invented_isavar)) |
|
499 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) |
|
500 in |
|
501 () |
|
502 end |
|
503 |
488 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u" |
504 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u" |
489 |
505 |
490 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
506 fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
491 | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
507 | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) |
492 | mk_lambda v t = raise TERM ("lambda", [v, t]); |
508 | mk_lambda v t = raise TERM ("lambda", [v, t]); |