(*  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 Unsynchronized.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 Unsynchronized.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)

(* 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 Delimfix (Syntax.escape c)

fun quotename c =

  if Syntax.is_identifier c andalso not (Keyword.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 (

        Print_Mode.setmp [] (

        setmp_CRITICAL show_brackets false (

        setmp_CRITICAL show_all_types true (

        setmp_CRITICAL Syntax.ambiguity_is_error false (

        setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))

        ct)

    end

exception SMART_STRING

fun smart_string_of_cterm ct =

    let

        val thy = Thm.theory_of_cterm ct

        val ctxt = ProofContext.init_global 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 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)

          | G 1 = setmp_CRITICAL show_brackets true (G 0)

          | G 2 = setmp_CRITICAL show_all_types true (G 0)

          | G 3 = setmp_CRITICAL show_brackets true (G 2)

          | G _ = raise SMART_STRING

        fun F n =

            let

                val str =

                  setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct

                val u = Syntax.parse_term ctxt str

                  |> Type_Infer.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 (Syntax.string_of_term ctxt o term_of) ct)

    in

      Print_Mode.setmp [] (setmp_CRITICAL 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 (Print_Mode.setmp [] Display.string_of_thm_without_context th);

fun prin t = writeln (Print_Mode.setmp []

  (fn () => Syntax.string_of_term (ML_Context.the_local_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 = Unsynchronized.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

infix mem;

fun i mem L =

    let fun itr [] = false

          | itr (a::rst) = i=a orelse itr rst

    in itr L end;

infix union;

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 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 = Unsynchronized.ref (Symtab.empty:string Symtab.table)

val invented_isavar = Unsynchronized.ref 0

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

fun valid_boundvarname s =

  can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();

fun valid_varname s =

  can (fn () => Syntax.read_term_global @{theory Main} 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 _ = Unsynchronized.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 _ = Unsynchronized.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(the (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(the (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

        val import_segment =

            case get_segment2 thyname thy of

                SOME seg => seg

              | NONE => get_import_segment thy

        val path = space_explode ":" (getenv "HOL4_PROOFS")

        fun find [] = NONE

          | find (p::ps) =

            (let

                 val dir = OS.Path.joinDirFile {dir = p,file=import_segment}

             in

                 if OS.FileSys.isDir dir

                 then SOME dir

                 else find ps

             end) handle OS.SysErr _ => find ps

    in

        Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)

    end

fun proof_file_name thyname thmname thy =

    let

        val path = case get_proof_dir thyname thy of

                       SOME p => p

                     | NONE => error "Cannot find proof files"

        val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()

    in

        OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}

    end

fun xml_to_proof thyname types terms prf thy =

    let

        val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types

        val xml_to_term = TermNet.get_term_from_xml thy thyname types terms

        fun index_to_term is =

            TermNet.get_term_from_index thy thyname types terms is

        fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is))

          | x2p (Elem("pinstt",[],p::lambda)) =

            let

                val p = x2p p

                val lambda = implode_subst (map xml_to_hol_type lambda)

            in

                mk_proof (PInstT(p,lambda))

            end

          | x2p (Elem("psubst",[("i",is)],prf::prfs)) =

            let

                val tm = index_to_term is

                val prf = x2p prf

                val prfs = map x2p prfs

            in

                mk_proof (PSubst(prfs,tm,prf))

            end

          | x2p (Elem("pabs",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val t = index_to_term is

            in

                mk_proof (PAbs (p,t))

            end

          | x2p (Elem("pdisch",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val t = index_to_term is

            in

                mk_proof (PDisch (p,t))

            end

          | x2p (Elem("pmp",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PMp(p1,p2))

            end

          | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is))

          | x2p (Elem("paxiom",[("n",n),("i",is)],[])) =

            mk_proof (PAxm(n,index_to_term is))

          | x2p (Elem("pfact",atts,[])) =

            let

                val thyname = get_segment thyname atts

                val thmname = protect_factname (get_name atts)

                val p = mk_proof PDisk

                val _  = set_disk_info_of p thyname thmname

            in

                p

            end

          | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =

            mk_proof (PDef(seg,protect_constname name,index_to_term is))

          | x2p (Elem("ptmspec",[("s",seg)],p::names)) =

            let

                val names = map (fn Elem("name",[("n",name)],[]) => name

                                  | _ => raise ERR "x2p" "Bad proof (ptmspec)") names

            in

                mk_proof (PTmSpec(seg,names,x2p p))

            end

          | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) =

            let

                val P = xml_to_term xP

                val t = xml_to_term xt

            in

                mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))

            end

          | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =

            mk_proof (PTyDef(seg,protect_tyname name,x2p p))

          | x2p (xml as Elem("poracle",[],chldr)) =

            let

                val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr

                val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles

                val (c,asl) = case terms of

                                  [] => raise ERR "x2p" "Bad oracle description"

                                | (hd::tl) => (hd,tl)

                val tg = fold_rev (Tag.merge o Tag.read) ors Tag.empty_tag

            in

                mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))

            end

          | x2p (Elem("pspec",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val tm = index_to_term is

            in

                mk_proof (PSpec(p,tm))

            end

          | x2p (Elem("pinst",[],p::theta)) =

            let

                val p = x2p p

                val theta = implode_subst (map xml_to_term theta)

            in

                mk_proof (PInst(p,theta))

            end

          | x2p (Elem("pgen",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val tm = index_to_term is

            in

                mk_proof (PGen(p,tm))

            end

          | x2p (Elem("pgenabs",[],prf::tms)) =

            let

                val p = x2p prf

                val tml = map xml_to_term tms

            in

                mk_proof (PGenAbs(p,NONE,tml))

            end

          | x2p (Elem("pgenabs",[("i",is)],prf::tms)) =

            let

                val p = x2p prf

                val tml = map xml_to_term tms

            in

                mk_proof (PGenAbs(p,SOME (index_to_term is),tml))

            end

          | x2p (Elem("pimpas",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PImpAS(p1,p2))

            end

          | x2p (Elem("psym",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PSym p)

            end

          | x2p (Elem("ptrans",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PTrans(p1,p2))

            end

          | x2p (Elem("pcomb",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PComb(p1,p2))

            end

          | x2p (Elem("peqmp",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PEqMp(p1,p2))

            end

          | x2p (Elem("peqimp",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PEqImp p)

            end

          | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) =

            let

                val p = x2p prf

                val ex = index_to_term ise

                val w = index_to_term isw

            in

                mk_proof (PExists(p,ex,w))

            end

          | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) =

            let

                val v  = index_to_term is

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PChoose(v,p1,p2))

            end

          | x2p (Elem("pconj",[],[prf1,prf2])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

            in

                mk_proof (PConj(p1,p2))

            end

          | x2p (Elem("pconjunct1",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PConjunct1 p)

            end

          | x2p (Elem("pconjunct2",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PConjunct2 p)

            end

          | x2p (Elem("pdisj1",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val t = index_to_term is

            in

                mk_proof (PDisj1 (p,t))

            end

          | x2p (Elem("pdisj2",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val t = index_to_term is

            in

                mk_proof (PDisj2 (p,t))

            end

          | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) =

            let

                val p1 = x2p prf1

                val p2 = x2p prf2

                val p3 = x2p prf3

            in

                mk_proof (PDisjCases(p1,p2,p3))

            end

          | x2p (Elem("pnoti",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PNotI p)

            end

          | x2p (Elem("pnote",[],[prf])) =

            let

                val p = x2p prf

            in

                mk_proof (PNotE p)

            end

          | x2p (Elem("pcontr",[("i",is)],[prf])) =

            let

                val p = x2p prf

                val t = index_to_term is

            in

                mk_proof (PContr (p,t))

            end

          | x2p xml = raise ERR "x2p" "Bad proof"

    in

        x2p prf

    end

fun import_proof_concl thyname thmname thy =

    let

        val is = TextIO.openIn(proof_file_name thyname thmname thy)

        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)

        val _ = TextIO.closeIn is

    in

        case proof_xml of

            Elem("proof",[],xtypes::xterms::prf::rest) =>

            let

                val types = TypeNet.input_types thyname xtypes

                val terms = TermNet.input_terms thyname types xterms

                fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm

            in

                case rest of

                    [] => NONE

                  | [xtm] => SOME (f xtm)

                  | _ => raise ERR "import_proof" "Bad argument list"

            end

          | _ => raise ERR "import_proof" "Bad proof"

    end

fun import_proof thyname thmname thy =

    let

        val is = TextIO.openIn(proof_file_name thyname thmname thy)

        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)

        val _ = TextIO.closeIn is

    in

        case proof_xml of

            Elem("proof",[],xtypes::xterms::prf::rest) =>

            let

                val types = TypeNet.input_types thyname xtypes

                val terms = TermNet.input_terms thyname types xterms

            in

                (case rest of

                     [] => NONE

                   | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm)

                   | _ => raise ERR "import_proof" "Bad argument list",

                 xml_to_proof thyname types terms prf)

            end

          | _ => raise ERR "import_proof" "Bad proof"

    end

fun uniq_compose m th i st =

    let

        val res = Thm.bicompose false (false,th,m) i st

    in

        case Seq.pull res of

            SOME (th,rest) => (case Seq.pull rest of

                                   SOME _ => raise ERR "uniq_compose" "Not unique!"

                                 | NONE => th)

          | NONE => raise ERR "uniq_compose" "No result"

    end

val reflexivity_thm = thm "refl"

val substitution_thm = thm "subst"

val mp_thm = thm "mp"

val imp_antisym_thm = thm "light_imp_as"

val disch_thm = thm "impI"

val ccontr_thm = thm "ccontr"

val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq"