src/HOL/Import/proof_kernel.ML

simplified method setup;

(*  Title:      HOL/Import/proof_kernel.ML
    Author:     Sebastian Skalberg and Steven Obua, TU Muenchen
*)

signature ProofKernel =
sig
    type hol_type
    type tag
    type term
    type thm
    type ('a,'b) subst

    type proof_info
    datatype proof = Proof of proof_info * proof_content
         and proof_content
           = PRefl of term
           | PInstT of proof * (hol_type,hol_type) subst
           | PSubst of proof list * term * proof
           | PAbs of proof * term
           | PDisch of proof * term
           | PMp of proof * proof
           | PHyp of term
           | PAxm of string * term
           | PDef of string * string * term
           | PTmSpec of string * string list * proof
           | PTyDef of string * string * proof
           | PTyIntro of string * string * string * string * term * term * proof
           | POracle of tag * term list * term
           | PDisk
           | PSpec of proof * term
           | PInst of proof * (term,term) subst
           | PGen of proof * term
           | PGenAbs of proof * term option * term list
           | PImpAS of proof * proof
           | PSym of proof
           | PTrans of proof * proof
           | PComb of proof * proof
           | PEqMp of proof * proof
           | PEqImp of proof
           | PExists of proof * term * term
           | PChoose of term * proof * proof
           | PConj of proof * proof
           | PConjunct1 of proof
           | PConjunct2 of proof
           | PDisj1 of proof * term
           | PDisj2 of proof * term
           | PDisjCases of proof * proof * proof
           | PNotI of proof
           | PNotE of proof
           | PContr of proof * term

    exception PK of string * string

    val get_proof_dir: string -> theory -> string option
    val disambiguate_frees : Thm.thm -> Thm.thm
    val debug : bool ref
    val disk_info_of : proof -> (string * string) option
    val set_disk_info_of : proof -> string -> string -> unit
    val mk_proof : proof_content -> proof
    val content_of : proof -> proof_content
    val import_proof : string -> string -> theory -> (theory -> term) option * (theory -> proof)

    val rewrite_hol4_term: Term.term -> theory -> Thm.thm

    val type_of : term -> hol_type

    val get_thm  : string -> string         -> theory -> (theory * thm option)
    val get_def  : string -> string -> term -> theory -> (theory * thm option)
    val get_axiom: string -> string         -> theory -> (theory * thm option)

    val store_thm : string -> string -> thm -> theory -> theory * thm

    val to_isa_thm : thm -> (term * term) list * Thm.thm
    val to_isa_term: term -> Term.term
    val to_hol_thm : Thm.thm -> thm

    val REFL : term -> theory -> theory * thm
    val ASSUME : term -> theory -> theory * thm
    val INST_TYPE : (hol_type,hol_type) subst -> thm -> theory -> theory * thm
    val INST : (term,term)subst -> thm -> theory -> theory * thm
    val EQ_MP : thm -> thm -> theory -> theory * thm
    val EQ_IMP_RULE : thm -> theory -> theory * thm
    val SUBST : thm list -> term -> thm -> theory -> theory * thm
    val DISJ_CASES : thm -> thm -> thm -> theory -> theory * thm
    val DISJ1: thm -> term -> theory -> theory * thm
    val DISJ2: term -> thm -> theory -> theory * thm
    val IMP_ANTISYM: thm -> thm -> theory -> theory * thm
    val SYM : thm -> theory -> theory * thm
    val MP : thm -> thm -> theory -> theory * thm
    val GEN : term -> thm -> theory -> theory * thm
    val CHOOSE : term -> thm -> thm -> theory -> theory * thm
    val EXISTS : term -> term -> thm -> theory -> theory * thm
    val ABS : term -> thm -> theory -> theory * thm
    val GEN_ABS : term option -> term list -> thm -> theory -> theory * thm
    val TRANS : thm -> thm -> theory -> theory * thm
    val CCONTR : term -> thm -> theory -> theory * thm
    val CONJ : thm -> thm -> theory -> theory * thm
    val CONJUNCT1: thm -> theory -> theory * thm
    val CONJUNCT2: thm -> theory -> theory * thm
    val NOT_INTRO: thm -> theory -> theory * thm
    val NOT_ELIM : thm -> theory -> theory * thm
    val SPEC : term -> thm -> theory -> theory * thm
    val COMB : thm -> thm -> theory -> theory * thm
    val DISCH: term -> thm -> theory -> theory * thm

    val type_introduction: string -> string -> string -> string -> string -> term * term -> thm -> theory -> theory * thm

    val new_definition : string -> string -> term -> theory -> theory * thm
    val new_specification : string -> string -> string list -> thm -> theory -> theory * thm
    val new_type_definition : string -> string -> string -> thm -> theory -> theory * thm
    val new_axiom : string -> term -> theory -> theory * thm

    val prin : term -> unit
    val protect_factname : string -> string
    val replay_protect_varname : string -> string -> unit
    val replay_add_dump : string -> theory -> theory
end

structure ProofKernel :> ProofKernel =
struct
type hol_type = Term.typ
type term = Term.term
datatype tag = Tag of string list
type ('a,'b) subst = ('a * 'b) list
datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm

fun hthm2thm (HOLThm (_, th)) = th

fun to_hol_thm th = HOLThm ([], th)

val replay_add_dump = add_dump
fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)

datatype proof_info
  = Info of {disk_info: (string * string) option ref}

datatype proof = Proof of proof_info * proof_content
     and proof_content
       = PRefl of term
       | PInstT of proof * (hol_type,hol_type) subst
       | PSubst of proof list * term * proof
       | PAbs of proof * term
       | PDisch of proof * term
       | PMp of proof * proof
       | PHyp of term
       | PAxm of string * term
       | PDef of string * string * term
       | PTmSpec of string * string list * proof
       | PTyDef of string * string * proof
       | PTyIntro of string * string * string * string * term * term * proof
       | POracle of tag * term list * term
       | PDisk
       | PSpec of proof * term
       | PInst of proof * (term,term) subst
       | PGen of proof * term
       | PGenAbs of proof * term option * term list
       | PImpAS of proof * proof
       | PSym of proof
       | PTrans of proof * proof
       | PComb of proof * proof
       | PEqMp of proof * proof
       | PEqImp of proof
       | PExists of proof * term * term
       | PChoose of term * proof * proof
       | PConj of proof * proof
       | PConjunct1 of proof
       | PConjunct2 of proof
       | PDisj1 of proof * term
       | PDisj2 of proof * term
       | PDisjCases of proof * proof * proof
       | PNotI of proof
       | PNotE of proof
       | PContr of proof * term

exception PK of string * string
fun ERR f mesg = PK (f,mesg)

fun print_exn e =
    case e of
        PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
      | _ => OldGoals.print_exn e

(* Compatibility. *)

val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix;

fun mk_syn thy c =
  if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
  else Syntax.literal c

fun quotename c =
  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c

fun simple_smart_string_of_cterm ct =
    let
        val thy = Thm.theory_of_cterm ct;
        val {t,T,...} = rep_cterm ct
        (* Hack to avoid parse errors with Trueprop *)
        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
                           handle TERM _ => ct)
    in
        quote(
        PrintMode.setmp [] (
        Library.setmp show_brackets false (
        Library.setmp show_all_types true (
        Library.setmp Syntax.ambiguity_is_error false (
        Library.setmp show_sorts true Display.string_of_cterm))))
        ct)
    end

exception SMART_STRING

fun smart_string_of_cterm ct =
    let
        val thy = Thm.theory_of_cterm ct
        val ctxt = ProofContext.init thy
        val {t,T,...} = rep_cterm ct
        (* Hack to avoid parse errors with Trueprop *)
        val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
                   handle TERM _ => ct)
        fun match u = t aconv u
        fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
          | G 1 = Library.setmp show_brackets true (G 0)
          | G 2 = Library.setmp show_all_types true (G 0)
          | G 3 = Library.setmp show_brackets true (G 2)
          | G _ = raise SMART_STRING
        fun F n =
            let
                val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct
                val u = Syntax.parse_term ctxt str
                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
            in
                if match u
                then quote str
                else F (n+1)
            end
            handle ERROR mesg => F (n+1)
                 | SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct))
    in
      PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    end
    handle ERROR mesg => simple_smart_string_of_cterm ct

val smart_string_of_thm = smart_string_of_cterm o cprop_of

fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
fun pth (HOLThm(ren,thm)) =
    let
        (*val _ = writeln "Renaming:"
        val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
        val _ = prth thm
    in
        ()
    end

fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
fun mk_proof p = Proof(Info{disk_info = ref NONE},p)
fun content_of (Proof(_,p)) = p

fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname =
    disk_info := SOME(thyname,thmname)

structure Lib =
struct

fun assoc x =
    let
        fun F [] = raise PK("Lib.assoc","Not found")
          | F ((x',y)::rest) = if x = x'
                               then y
                               else F rest
    in
        F
    end
fun i mem L =
    let fun itr [] = false
          | itr (a::rst) = i=a orelse itr rst
    in itr L end;

fun [] union S = S
  | S union [] = S
  | (a::rst) union S2 = rst union (insert (op =) a S2)

fun implode_subst [] = []
  | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
  | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"

end
open Lib

structure Tag =
struct
val empty_tag = Tag []
fun read name = Tag [name]
fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2))
end

(* Actual code. *)

fun get_segment thyname l = (Lib.assoc "s" l
                             handle PK _ => thyname)
val get_name : (string * string) list -> string = Lib.assoc "n"

local
    open LazyScan
    infix 7 |-- --|
    infix 5 :-- -- ^^
    infix 3 >>
    infix 0 ||
in
exception XML of string

datatype xml = Elem of string * (string * string) list * xml list
datatype XMLtype = XMLty of xml | FullType of hol_type
datatype XMLterm = XMLtm of xml | FullTerm of term

fun pair x y = (x,y)

fun scan_id toks =
    let
        val (x,toks2) = one Char.isAlpha toks
        val (xs,toks3) = any Char.isAlphaNum toks2
    in
        (String.implode (x::xs),toks3)
    end

fun scan_string str c =
    let
        fun F [] toks = (c,toks)
          | F (c::cs) toks =
            case LazySeq.getItem toks of
                SOME(c',toks') =>
                if c = c'
                then F cs toks'
                else raise SyntaxError
              | NONE => raise SyntaxError
    in
        F (String.explode str)
    end

local
    val scan_entity =
        (scan_string "amp;" #"&")
            || scan_string "quot;" #"\""
            || scan_string "gt;" #">"
            || scan_string "lt;" #"<"
            || scan_string "apos;" #"'"
in
fun scan_nonquote toks =
    case LazySeq.getItem toks of
        SOME (c,toks') =>
        (case c of
             #"\"" => raise SyntaxError
           | #"&" => scan_entity toks'
           | c => (c,toks'))
      | NONE => raise SyntaxError
end

val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
                     String.implode

val scan_attribute = scan_id -- $$ #"=" |-- scan_string

val scan_start_of_tag = $$ #"<" |-- scan_id --
                           repeat ($$ #" " |-- scan_attribute)

(* The evaluation delay introduced through the 'toks' argument is needed
for the sake of the SML/NJ (110.9.1) compiler.  Either that or an explicit
type :-( *)
fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks

val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"

fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
                       (fn (chldr,id') => if id = id'
                                          then chldr
                                          else raise XML "Tag mismatch")
and scan_tag toks =
    let
        val ((id,atts),toks2) = scan_start_of_tag toks
        val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
    in
        (Elem (id,atts,chldr),toks3)
    end
end

val type_of = Term.type_of

val boolT = Type("bool",[])
val propT = Type("prop",[])

fun mk_defeq name rhs thy =
    let
        val ty = type_of rhs
    in
        Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
    end

fun mk_teq name rhs thy =
    let
        val ty = type_of rhs
    in
        HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
    end

fun intern_const_name thyname const thy =
    case get_hol4_const_mapping thyname const thy of
        SOME (_,cname,_) => cname
      | NONE => (case get_hol4_const_renaming thyname const thy of
                     SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
                   | NONE => Sign.intern_const thy (thyname ^ "." ^ const))

fun intern_type_name thyname const thy =
    case get_hol4_type_mapping thyname const thy of
        SOME (_,cname) => cname
      | NONE => Sign.intern_const thy (thyname ^ "." ^ const)

fun mk_vartype name = TFree(name,["HOL.type"])
fun mk_thy_type thy Thy Tyop Args = Type(intern_type_name Thy Tyop thy,Args)

val mk_var = Free

fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
  | dom_rng _ = raise ERR "dom_rng" "Not a functional type"

fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)

local
  fun get_const sg thyname name =
    (case Sign.const_type sg name of
      SOME ty => Const (name, ty)
    | NONE => raise ERR "get_type" (name ^ ": No such constant"))
in
fun prim_mk_const thy Thy Nam =
    let
      val name = intern_const_name Thy Nam thy
      val cmaps = HOL4ConstMaps.get thy
    in
      case StringPair.lookup cmaps (Thy,Nam) of
        SOME(_,_,SOME ty) => Const(name,ty)
      | _ => get_const thy Thy name
    end
end

fun mk_comb(f,a) = f $ a

(* Needed for HOL Light *)
fun protect_tyvarname s =
    let
        fun no_quest s =
            if Char.contains s #"?"
            then String.translate (fn #"?" => "q_" | c => Char.toString c) s
            else s
        fun beg_prime s =
            if String.isPrefix "'" s
            then s
            else "'" ^ s
    in
        s |> no_quest |> beg_prime
    end

val protected_varnames = ref (Symtab.empty:string Symtab.table)
val invented_isavar = ref 0

fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)

val check_name_thy = theory "Main"

fun valid_boundvarname s =
  can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) ();

fun valid_varname s =
  can (fn () => Syntax.read_term_global check_name_thy s) ();

fun protect_varname s =
    if innocent_varname s andalso valid_varname s then s else
    case Symtab.lookup (!protected_varnames) s of
      SOME t => t
    | NONE =>
      let
          val _ = inc invented_isavar
          val t = "u_" ^ string_of_int (!invented_isavar)
          val _ = ImportRecorder.protect_varname s t
          val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
      in
          t
      end

exception REPLAY_PROTECT_VARNAME of string*string*string

fun replay_protect_varname s t =
        case Symtab.lookup (!protected_varnames) s of
          SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
        | NONE =>
          let
              val _ = inc invented_isavar
              val t = "u_" ^ string_of_int (!invented_isavar)
              val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
          in
              ()
          end

fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"

fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
  | mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t))
  | mk_lambda v t = raise TERM ("lambda", [v, t]);

fun replacestr x y s =
let
  val xl = explode x
  val yl = explode y
  fun isprefix [] ys = true
    | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
    | isprefix _ _ = false
  fun isp s = isprefix xl s
  fun chg s = yl@(List.drop (s, List.length xl))
  fun r [] = []
    | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
in
  implode(r (explode s))
end

fun protect_factname s = replacestr "." "_dot_" s
fun unprotect_factname s = replacestr "_dot_" "." s

val ty_num_prefix = "N_"

fun startsWithDigit s = Char.isDigit (hd (String.explode s))

fun protect_tyname tyn =
  let
    val tyn' =
      if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else
      (if startsWithDigit tyn then ty_num_prefix^tyn else tyn)
  in
    tyn'
  end

fun protect_constname tcn = tcn
 (* if tcn = ".." then "dotdot"
  else if tcn = "==" then "eqeq"
  else tcn*)

structure TypeNet =
struct

fun get_type_from_index thy thyname types is =
    case Int.fromString is of
        SOME i => (case Array.sub(types,i) of
                       FullType ty => ty
                     | XMLty xty =>
                       let
                           val ty = get_type_from_xml thy thyname types xty
                           val _  = Array.update(types,i,FullType ty)
                       in
                           ty
                       end)
      | NONE => raise ERR "get_type_from_index" "Bad index"
and get_type_from_xml thy thyname types =
    let
        fun gtfx (Elem("tyi",[("i",iS)],[])) =
                 get_type_from_index thy thyname types iS
          | gtfx (Elem("tyc",atts,[])) =
            mk_thy_type thy
                        (get_segment thyname atts)
                        (protect_tyname (get_name atts))
                        []
          | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
          | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
            mk_thy_type thy
                        (get_segment thyname atts)
                        (protect_tyname (get_name atts))
                        (map gtfx tys)
          | gtfx _ = raise ERR "get_type" "Bad type"
    in
        gtfx
    end

fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
    let
        val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
        fun IT _ [] = ()
          | IT n (xty::xtys) =
            (Array.update(types,n,XMLty xty);
             IT (n+1) xtys)
        val _ = IT 0 xtys
    in
        types
    end
  | input_types _ _ = raise ERR "input_types" "Bad type list"
end

structure TermNet =
struct

fun get_term_from_index thy thyname types terms is =
    case Int.fromString is of
        SOME i => (case Array.sub(terms,i) of
                       FullTerm tm => tm
                     | XMLtm xtm =>
                       let
                           val tm = get_term_from_xml thy thyname types terms xtm
                           val _  = Array.update(terms,i,FullTerm tm)
                       in
                           tm
                       end)
      | NONE => raise ERR "get_term_from_index" "Bad index"
and get_term_from_xml thy thyname types terms =
    let
        fun get_type [] = NONE
          | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
          | get_type _ = raise ERR "get_term" "Bad type"

        fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
            mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
          | gtfx (Elem("tmc",atts,[])) =
            let
                val segment = get_segment thyname atts
                val name = protect_constname(get_name atts)
            in
                mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
                handle PK _ => prim_mk_const thy segment name
            end
          | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) =
            let
                val f = get_term_from_index thy thyname types terms tmf
                val a = get_term_from_index thy thyname types terms tma
            in
                mk_comb(f,a)
            end
          | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
            let
                val x = get_term_from_index thy thyname types terms tmx
                val a = get_term_from_index thy thyname types terms tma
            in
                mk_lambda x a
            end
          | gtfx (Elem("tmi",[("i",iS)],[])) =
            get_term_from_index thy thyname types terms iS
          | gtfx (Elem(tag,_,_)) =
            raise ERR "get_term" ("Not a term: "^tag)
    in
        gtfx
    end

fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
    let
        val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))

        fun IT _ [] = ()
          | IT n (xtm::xtms) =
            (Array.update(terms,n,XMLtm xtm);
             IT (n+1) xtms)
        val _ = IT 0 xtms
    in
        terms
    end
  | input_terms _ _ _ = raise ERR "input_terms" "Bad term list"
end

fun get_proof_dir (thyname:string) thy =
    let