# HG changeset patch # User wenzelm # Date 1208012435 -7200 # Node ID c6231d64d264ff6c7a790d5f12e6bf0b71f88234 # Parent e0cc4169626e2b9f55297ce24a3a3c6160ce2453 rep_cterm/rep_thm: no longer dereference theory_ref; diff -r e0cc4169626e -r c6231d64d264 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Import/proof_kernel.ML Sat Apr 12 17:00:35 2008 +0200 @@ -13,42 +13,42 @@ 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 + 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 @@ -178,7 +178,7 @@ fun print_exn e = case e of - PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e) + PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e) | _ => OldGoals.print_exn e (* Compatibility. *) @@ -194,47 +194,49 @@ fun simple_smart_string_of_cterm ct = let - val {thy,t,T,...} = rep_cterm ct - (* Hack to avoid parse errors with Trueprop *) - val ct = (cterm_of thy (HOLogic.dest_Trueprop t) - handle TERM _ => ct) + 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 string_of_cterm)))) - ct) + 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 string_of_cterm)))) + ct) end exception SMART_STRING fun smart_string_of_cterm ct = let - val {thy,t,T,...} = rep_cterm ct + 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) + 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 string_of_cterm) ct - val u = Syntax.parse_term ctxt str + fun F n = + let + val str = Library.setmp show_brackets false (G n 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 => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct)) + in + if match u + then quote str + else F (n+1) + end + handle ERROR mesg => F (n+1) + | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct)) in PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 end @@ -247,11 +249,11 @@ fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (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 + (*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 @@ -267,16 +269,16 @@ fun assoc x = let - fun F [] = raise PK("Lib.assoc","Not found") - | F ((x',y)::rest) = if x = x' - then y - else F rest + fun F [] = raise PK("Lib.assoc","Not found") + | F ((x',y)::rest) = if x = x' + then y + else F rest in - F + F end fun i mem L = let fun itr [] = false - | itr (a::rst) = i=a orelse itr rst + | itr (a::rst) = i=a orelse itr rst in itr L end; fun insert i L = if i mem L then L else i::L @@ -305,7 +307,7 @@ (* Actual code. *) fun get_segment thyname l = (Lib.assoc "s" l - handle PK _ => thyname) + handle PK _ => thyname) val get_name : (string * string) list -> string = Lib.assoc "n" local @@ -333,43 +335,43 @@ 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 + 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) + F (String.explode str) end local val scan_entity = - (scan_string "amp;" #"&") - || scan_string "quot;" #"\"" - || scan_string "gt;" #">" - || scan_string "lt;" #"<" + (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')) + 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 + String.implode val scan_attribute = scan_id -- $$ #"=" |-- scan_string val scan_start_of_tag = $$ #"<" |-- scan_id -- - repeat ($$ #" " |-- scan_attribute) + 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 @@ -379,15 +381,15 @@ 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") + (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 + 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) + (Elem (id,atts,chldr),toks3) end end @@ -398,28 +400,28 @@ fun mk_defeq name rhs thy = let - val ty = type_of rhs + val ty = type_of rhs in - Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs) + Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs) end fun mk_teq name rhs thy = let - val ty = type_of rhs + val ty = type_of rhs in - HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs) + 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 + 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)) + 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 + SOME (_,cname) => cname | NONE => Sign.intern_const thy (thyname ^ "." ^ const) fun mk_vartype name = TFree(name,["HOL.type"]) @@ -454,16 +456,16 @@ (* 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 + 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 + s |> no_quest |> beg_prime end val protected_varnames = ref (Symtab.empty:string Symtab.table) @@ -485,26 +487,26 @@ SOME t => t | NONE => let - val _ = inc invented_isavar - val t = "u_" ^ string_of_int (!invented_isavar) - val _ = ImportRecorder.protect_varname s t + 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 + 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 => + 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 _ = 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" @@ -554,46 +556,46 @@ 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) + 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" + 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 + 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 + 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 + types end | input_types _ _ = raise ERR "input_types" "Bad type list" end @@ -603,392 +605,392 @@ 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) + 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 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 + 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 + 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 + gtfx end fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) = let - val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[]))) + 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 + fun IT _ [] = () + | IT n (xtm::xtms) = + (Array.update(terms,n,XMLtm xtm); + IT (n+1) xtms) + val _ = IT 0 xtms in - terms + 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 + 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) + 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 _ => () + 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"}} + 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 + 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 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 = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors - 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" + 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 = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors + 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 + 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 + 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 + 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" + 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 + 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" + 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 = bicompose false (false,th,m) i st + val res = 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" + 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" @@ -1033,10 +1035,10 @@ fun beta_eta_thm th = let - val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th - val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1 + val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th + val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1 in - th2 + th2 end fun implies_elim_all th = @@ -1049,38 +1051,38 @@ fun mk_GEN v th sg = let - val c = HOLogic.dest_Trueprop (concl_of th) - val cv = cterm_of sg v - val lc = Term.lambda v c - val clc = Thm.cterm_of sg lc - val cvty = ctyp_of_term cv - val th1 = implies_elim_all th - val th2 = beta_eta_thm (forall_intr cv th1) - val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) - val c = prop_of th3 - val vname = fst(dest_Free v) - val (cold,cnew) = case c of - tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) => - (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0)) - | tpc $ (Const("All",allT) $ rest) => (tpc,tpc) - | _ => raise ERR "mk_GEN" "Unknown conclusion" - val th4 = Thm.rename_boundvars cold cnew th3 - val res = implies_intr_hyps th4 + val c = HOLogic.dest_Trueprop (concl_of th) + val cv = cterm_of sg v + val lc = Term.lambda v c + val clc = Thm.cterm_of sg lc + val cvty = ctyp_of_term cv + val th1 = implies_elim_all th + val th2 = beta_eta_thm (forall_intr cv th1) + val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) + val c = prop_of th3 + val vname = fst(dest_Free v) + val (cold,cnew) = case c of + tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) => + (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0)) + | tpc $ (Const("All",allT) $ rest) => (tpc,tpc) + | _ => raise ERR "mk_GEN" "Unknown conclusion" + val th4 = Thm.rename_boundvars cold cnew th3 + val res = implies_intr_hyps th4 in - res + res end val permute_prems = Thm.permute_prems fun rearrange sg tm th = let - val tm' = Envir.beta_eta_contract tm - fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th) - | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) - then permute_prems n 1 th - else find ps (n+1) + val tm' = Envir.beta_eta_contract tm + fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th) + | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) + then permute_prems n 1 th + else find ps (n+1) in - find (prems_of th) 0 + find (prems_of th) 0 end fun zip (x::xs) (y::ys) = (x,y)::(zip xs ys) @@ -1093,17 +1095,17 @@ val collect_vars = let - fun F vars (Bound _) = vars - | F vars (tm as Free _) = - if tm mem vars - then vars - else (tm::vars) - | F vars (Const _) = vars - | F vars (tm1 $ tm2) = F (F vars tm1) tm2 - | F vars (Abs(_,_,body)) = F vars body - | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found" + fun F vars (Bound _) = vars + | F vars (tm as Free _) = + if tm mem vars + then vars + else (tm::vars) + | F vars (Const _) = vars + | F vars (tm1 $ tm2) = F (F vars tm1) tm2 + | F vars (Abs(_,_,body)) = F vars body + | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found" in - F [] + F [] end (* Code for disambiguating variablenames (wrt. types) *) @@ -1122,9 +1124,9 @@ fun has_ren (HOLThm _) = false fun prinfo {vars,rens} = (writeln "Vars:"; - app prin vars; - writeln "Renaming:"; - app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens) + app prin vars; + writeln "Renaming:"; + app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens) fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) @@ -1202,119 +1204,119 @@ fun get_hol4_thm thyname thmname thy = case get_hol4_theorem thyname thmname thy of - SOME hth => SOME (HOLThm hth) + SOME hth => SOME (HOLThm hth) | NONE => - let - val pending = HOL4Pending.get thy - in - case StringPair.lookup pending (thyname,thmname) of - SOME hth => SOME (HOLThm hth) - | NONE => NONE - end + let + val pending = HOL4Pending.get thy + in + case StringPair.lookup pending (thyname,thmname) of + SOME hth => SOME (HOLThm hth) + | NONE => NONE + end fun non_trivial_term_consts tm = List.filter (fn c => not (c = "Trueprop" orelse - c = "All" orelse - c = "op -->" orelse - c = "op &" orelse - c = "op =")) (Term.term_consts tm) + c = "All" orelse + c = "op -->" orelse + c = "op &" orelse + c = "op =")) (Term.term_consts tm) fun match_consts t (* th *) = let - fun add_consts (Const (c, _), cs) = - (case c of - "op =" => Library.insert (op =) "==" cs - | "op -->" => Library.insert (op =) "==>" cs - | "All" => cs - | "all" => cs - | "op &" => cs - | "Trueprop" => cs - | _ => Library.insert (op =) c cs) - | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) - | add_consts (Abs (_, _, t), cs) = add_consts (t, cs) - | add_consts (_, cs) = cs - val t_consts = add_consts(t,[]) + fun add_consts (Const (c, _), cs) = + (case c of + "op =" => Library.insert (op =) "==" cs + | "op -->" => Library.insert (op =) "==>" cs + | "All" => cs + | "all" => cs + | "op &" => cs + | "Trueprop" => cs + | _ => Library.insert (op =) c cs) + | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) + | add_consts (Abs (_, _, t), cs) = add_consts (t, cs) + | add_consts (_, cs) = cs + val t_consts = add_consts(t,[]) in - fn th => eq_set(t_consts,add_consts(prop_of th,[])) + fn th => eq_set(t_consts,add_consts(prop_of th,[])) end fun split_name str = let - val sub = Substring.full str - val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) - val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) + val sub = Substring.full str + val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) + val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) in - if not (idx = "") andalso u = "_" - then SOME (newstr,valOf(Int.fromString idx)) - else NONE + if not (idx = "") andalso u = "_" + then SOME (newstr,valOf(Int.fromString idx)) + else NONE end handle _ => NONE fun rewrite_hol4_term t thy = let - val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) - val hol4ss = Simplifier.theory_context thy empty_ss + val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) + val hol4ss = Simplifier.theory_context thy empty_ss setmksimps single addsimps hol4rews1 in - Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t)) + Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t)) end fun get_isabelle_thm thyname thmname hol4conc thy = let - val (info,hol4conc') = disamb_term hol4conc - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) - val isaconc = - case concl_of i2h_conc of - Const("==",_) $ lhs $ _ => lhs - | _ => error "get_isabelle_thm" "Bad rewrite rule" - val _ = (message "Original conclusion:"; - if_debug prin hol4conc'; - message "Modified conclusion:"; - if_debug prin isaconc) + val (info,hol4conc') = disamb_term hol4conc + val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) + val isaconc = + case concl_of i2h_conc of + Const("==",_) $ lhs $ _ => lhs + | _ => error "get_isabelle_thm" "Bad rewrite rule" + val _ = (message "Original conclusion:"; + if_debug prin hol4conc'; + message "Modified conclusion:"; + if_debug prin isaconc) - fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th) + fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th) in - case get_hol4_mapping thyname thmname thy of - SOME (SOME thmname) => - let - val th1 = (SOME (PureThy.get_thm thy thmname) - handle ERROR _ => - (case split_name thmname of - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1)) - handle _ => NONE) - | NONE => NONE)) - in - case th1 of - SOME th2 => - (case Shuffler.set_prop thy isaconc [(thmname,th2)] of - SOME (_,th) => (message "YES";(thy, SOME (mk_res th))) - | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping")) - | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping") - end - | SOME NONE => error ("Trying to access ignored theorem " ^ thmname) - | NONE => - let - val _ = (message "Looking for conclusion:"; - if_debug prin isaconc) - val cs = non_trivial_term_consts isaconc - val _ = (message "Looking for consts:"; - message (commas cs)) - val pot_thms = Shuffler.find_potential thy isaconc - val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") - in - case Shuffler.set_prop thy isaconc pot_thms of - SOME (isaname,th) => - let - val hth as HOLThm args = mk_res th - val thy' = thy |> add_hol4_theorem thyname thmname args - |> add_hol4_mapping thyname thmname isaname - val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args) - val _ = ImportRecorder.add_hol_mapping thyname thmname isaname - in - (thy',SOME hth) - end - | NONE => (thy,NONE) - end + case get_hol4_mapping thyname thmname thy of + SOME (SOME thmname) => + let + val th1 = (SOME (PureThy.get_thm thy thmname) + handle ERROR _ => + (case split_name thmname of + SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1)) + handle _ => NONE) + | NONE => NONE)) + in + case th1 of + SOME th2 => + (case Shuffler.set_prop thy isaconc [(thmname,th2)] of + SOME (_,th) => (message "YES";(thy, SOME (mk_res th))) + | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping")) + | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping") + end + | SOME NONE => error ("Trying to access ignored theorem " ^ thmname) + | NONE => + let + val _ = (message "Looking for conclusion:"; + if_debug prin isaconc) + val cs = non_trivial_term_consts isaconc + val _ = (message "Looking for consts:"; + message (commas cs)) + val pot_thms = Shuffler.find_potential thy isaconc + val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") + in + case Shuffler.set_prop thy isaconc pot_thms of + SOME (isaname,th) => + let + val hth as HOLThm args = mk_res th + val thy' = thy |> add_hol4_theorem thyname thmname args + |> add_hol4_mapping thyname thmname isaname + val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args) + val _ = ImportRecorder.add_hol_mapping thyname thmname isaname + in + (thy',SOME hth) + end + | NONE => (thy,NONE) + end end handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE)) @@ -1323,658 +1325,658 @@ val (a, b) = get_isabelle_thm thyname thmname hol4conc thy fun warn () = let - val (info,hol4conc') = disamb_term hol4conc - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) - in - case concl_of i2h_conc of - Const("==",_) $ lhs $ _ => - (warning ("Failed lookup of theorem '"^thmname^"':"); - writeln "Original conclusion:"; - prin hol4conc'; - writeln "Modified conclusion:"; - prin lhs) - | _ => () - end + val (info,hol4conc') = disamb_term hol4conc + val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) + in + case concl_of i2h_conc of + Const("==",_) $ lhs $ _ => + (warning ("Failed lookup of theorem '"^thmname^"':"); + writeln "Original conclusion:"; + prin hol4conc'; + writeln "Modified conclusion:"; + prin lhs) + | _ => () + end in case b of - NONE => (warn () handle _ => (); (a,b)) - | _ => (a, b) + NONE => (warn () handle _ => (); (a,b)) + | _ => (a, b) end fun get_thm thyname thmname thy = case get_hol4_thm thyname thmname thy of - SOME hth => (thy,SOME hth) + SOME hth => (thy,SOME hth) | NONE => ((case import_proof_concl thyname thmname thy of - SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy - | NONE => (message "No conclusion"; (thy,NONE))) - handle e as IO.Io _ => (message "IO exception"; (thy,NONE)) - | e as PK _ => (message "PK exception"; (thy,NONE))) + SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy + | NONE => (message "No conclusion"; (thy,NONE))) + handle e as IO.Io _ => (message "IO exception"; (thy,NONE)) + | e as PK _ => (message "PK exception"; (thy,NONE))) fun rename_const thyname thy name = case get_hol4_const_renaming thyname name thy of - SOME cname => cname + SOME cname => cname | NONE => name fun get_def thyname constname rhs thy = let - val constname = rename_const thyname thy constname - val (thmname,thy') = get_defname thyname constname thy - val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname) + val constname = rename_const thyname thy constname + val (thmname,thy') = get_defname thyname constname thy + val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname) in - get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' + get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' end fun get_axiom thyname axname thy = case get_thm thyname axname thy of - arg as (_,SOME _) => arg + arg as (_,SOME _) => arg | _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")") fun intern_store_thm gen_output thyname thmname hth thy = let - val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth - val rew = rewrite_hol4_term (concl_of th) thy - val th = equal_elim rew th - val thy' = add_hol4_pending thyname thmname args thy - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') + val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth + val rew = rewrite_hol4_term (concl_of th) thy + val th = equal_elim rew th + val thy' = add_hol4_pending thyname thmname args thy + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') val th = disambiguate_frees th - val thy2 = if gen_output - then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ + val thy2 = if gen_output + then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ (smart_string_of_thm th) ^ "\n by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")") thy' - else thy' + else thy' in - (thy2,hth') + (thy2,hth') end val store_thm = intern_store_thm true fun mk_REFL ctm = let - val cty = Thm.ctyp_of_term ctm + val cty = Thm.ctyp_of_term ctm in - Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm + Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm end fun REFL tm thy = let - val _ = message "REFL:" - val (info,tm') = disamb_term tm - val ctm = Thm.cterm_of thy tm' - val res = HOLThm(rens_of info,mk_REFL ctm) - val _ = if_debug pth res + val _ = message "REFL:" + val (info,tm') = disamb_term tm + val ctm = Thm.cterm_of thy tm' + val res = HOLThm(rens_of info,mk_REFL ctm) + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun ASSUME tm thy = let - val _ = message "ASSUME:" - val (info,tm') = disamb_term tm - val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm') - val th = Thm.trivial ctm - val res = HOLThm(rens_of info,th) - val _ = if_debug pth res + val _ = message "ASSUME:" + val (info,tm') = disamb_term tm + val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm') + val th = Thm.trivial ctm + val res = HOLThm(rens_of info,th) + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy = let - val _ = message "INST_TYPE:" - val _ = if_debug pth hth - val tys_before = add_term_tfrees (prop_of th,[]) - val th1 = Thm.varifyT th - val tys_after = add_term_tvars (prop_of th1,[]) - val tyinst = map (fn (bef, iS) => - (case try (Lib.assoc (TFree bef)) lambda of - SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty) - | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef)) - )) - (zip tys_before tys_after) - val res = Drule.instantiate (tyinst,[]) th1 - val hth = HOLThm([],res) - val res = norm_hthm thy hth - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "INST_TYPE:" + val _ = if_debug pth hth + val tys_before = add_term_tfrees (prop_of th,[]) + val th1 = Thm.varifyT th + val tys_after = add_term_tvars (prop_of th1,[]) + val tyinst = map (fn (bef, iS) => + (case try (Lib.assoc (TFree bef)) lambda of + SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty) + | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef)) + )) + (zip tys_before tys_after) + val res = Drule.instantiate (tyinst,[]) th1 + val hth = HOLThm([],res) + val res = norm_hthm thy hth + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun INST sigma hth thy = let - val _ = message "INST:" - val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma - val _ = if_debug pth hth - val (sdom,srng) = ListPair.unzip (rev sigma) - val th = hthm2thm hth - val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th - val res = HOLThm([],th1) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "INST:" + val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma + val _ = if_debug pth hth + val (sdom,srng) = ListPair.unzip (rev sigma) + val th = hthm2thm hth + val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th + val res = HOLThm([],th1) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun EQ_IMP_RULE (hth as HOLThm(rens,th)) thy = let - val _ = message "EQ_IMP_RULE:" - val _ = if_debug pth hth - val res = HOLThm(rens,th RS eqimp_thm) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "EQ_IMP_RULE:" + val _ = if_debug pth hth + val res = HOLThm(rens,th RS eqimp_thm) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm fun EQ_MP hth1 hth2 thy = let - val _ = message "EQ_MP:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val res = HOLThm(rens_of info,mk_EQ_MP th1 th2) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "EQ_MP:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val res = HOLThm(rens_of info,mk_EQ_MP th1 th2) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun mk_COMB th1 th2 thy = let - val (f,g) = case concl_of th1 of - _ $ (Const("op =",_) $ f $ g) => (f,g) - | _ => raise ERR "mk_COMB" "First theorem not an equality" - val (x,y) = case concl_of th2 of - _ $ (Const("op =",_) $ x $ y) => (x,y) - | _ => raise ERR "mk_COMB" "Second theorem not an equality" - val fty = type_of f - val (fd,fr) = dom_rng fty - val comb_thm' = Drule.instantiate' - [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)] - [SOME (cterm_of thy f),SOME (cterm_of thy g), - SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm + val (f,g) = case concl_of th1 of + _ $ (Const("op =",_) $ f $ g) => (f,g) + | _ => raise ERR "mk_COMB" "First theorem not an equality" + val (x,y) = case concl_of th2 of + _ $ (Const("op =",_) $ x $ y) => (x,y) + | _ => raise ERR "mk_COMB" "Second theorem not an equality" + val fty = type_of f + val (fd,fr) = dom_rng fty + val comb_thm' = Drule.instantiate' + [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)] + [SOME (cterm_of thy f),SOME (cterm_of thy g), + SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm in - [th1,th2] MRS comb_thm' + [th1,th2] MRS comb_thm' end fun SUBST rews ctxt hth thy = let - val _ = message "SUBST:" - val _ = if_debug (app pth) rews - val _ = if_debug prin ctxt - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info1,ctxt') = disamb_term_from info ctxt - val (info2,rews') = disamb_thms_from info1 rews + val _ = message "SUBST:" + val _ = if_debug (app pth) rews + val _ = if_debug prin ctxt + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info1,ctxt') = disamb_term_from info ctxt + val (info2,rews') = disamb_thms_from info1 rews - val cctxt = cterm_of thy ctxt' - fun subst th [] = th - | subst th (rew::rews) = subst (mk_COMB th rew thy) rews - val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th) - val _ = message "RESULT:" - val _ = if_debug pth res + val cctxt = cterm_of thy ctxt' + fun subst th [] = th + | subst th (rew::rews) = subst (mk_COMB th rew thy) rews + val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun DISJ_CASES hth hth1 hth2 thy = let - val _ = message "DISJ_CASES:" - val _ = if_debug (app pth) [hth,hth1,hth2] - val (info,th) = disamb_thm hth - val (info1,th1) = disamb_thm_from info hth1 - val (info2,th2) = disamb_thm_from info1 hth2 - val th1 = norm_hyps th1 - val th2 = norm_hyps th2 - val (l,r) = case concl_of th of - _ $ (Const("op |",_) $ l $ r) => (l,r) - | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction" - val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1 - val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2 - val res1 = th RS disj_cases_thm - val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1 - val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2 - val res = HOLThm(rens_of info2,res3) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "DISJ_CASES:" + val _ = if_debug (app pth) [hth,hth1,hth2] + val (info,th) = disamb_thm hth + val (info1,th1) = disamb_thm_from info hth1 + val (info2,th2) = disamb_thm_from info1 hth2 + val th1 = norm_hyps th1 + val th2 = norm_hyps th2 + val (l,r) = case concl_of th of + _ $ (Const("op |",_) $ l $ r) => (l,r) + | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction" + val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1 + val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2 + val res1 = th RS disj_cases_thm + val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1 + val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2 + val res = HOLThm(rens_of info2,res3) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun DISJ1 hth tm thy = let - val _ = message "DISJ1:" - val _ = if_debug pth hth - val _ = if_debug prin tm - val (info,th) = disamb_thm hth - val (info',tm') = disamb_term_from info tm - val ct = Thm.cterm_of thy tm' - val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm - val res = HOLThm(rens_of info',th RS disj1_thm') - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "DISJ1:" + val _ = if_debug pth hth + val _ = if_debug prin tm + val (info,th) = disamb_thm hth + val (info',tm') = disamb_term_from info tm + val ct = Thm.cterm_of thy tm' + val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm + val res = HOLThm(rens_of info',th RS disj1_thm') + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun DISJ2 tm hth thy = let - val _ = message "DISJ1:" - val _ = if_debug prin tm - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',tm') = disamb_term_from info tm - val ct = Thm.cterm_of thy tm' - val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm - val res = HOLThm(rens_of info',th RS disj2_thm') - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "DISJ1:" + val _ = if_debug prin tm + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',tm') = disamb_term_from info tm + val ct = Thm.cterm_of thy tm' + val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm + val res = HOLThm(rens_of info',th RS disj2_thm') + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun IMP_ANTISYM hth1 hth2 thy = let - val _ = message "IMP_ANTISYM:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm - val res = HOLThm(rens_of info,th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "IMP_ANTISYM:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm + val res = HOLThm(rens_of info,th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun SYM (hth as HOLThm(rens,th)) thy = let - val _ = message "SYM:" - val _ = if_debug pth hth - val th = th RS symmetry_thm - val res = HOLThm(rens,th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "SYM:" + val _ = if_debug pth hth + val th = th RS symmetry_thm + val res = HOLThm(rens,th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun MP hth1 hth2 thy = let - val _ = message "MP:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm - val res = HOLThm(rens_of info,th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "MP:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm + val res = HOLThm(rens_of info,th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun CONJ hth1 hth2 thy = let - val _ = message "CONJ:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val th = [th1,th2] MRS conj_thm - val res = HOLThm(rens_of info,th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "CONJ:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val th = [th1,th2] MRS conj_thm + val res = HOLThm(rens_of info,th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun CONJUNCT1 (hth as HOLThm(rens,th)) thy = let - val _ = message "CONJUNCT1:" - val _ = if_debug pth hth - val res = HOLThm(rens,th RS conjunct1_thm) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "CONJUNCT1:" + val _ = if_debug pth hth + val res = HOLThm(rens,th RS conjunct1_thm) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun CONJUNCT2 (hth as HOLThm(rens,th)) thy = let - val _ = message "CONJUNCT1:" - val _ = if_debug pth hth - val res = HOLThm(rens,th RS conjunct2_thm) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "CONJUNCT1:" + val _ = if_debug pth hth + val res = HOLThm(rens,th RS conjunct2_thm) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun EXISTS ex wit hth thy = let - val _ = message "EXISTS:" - val _ = if_debug prin ex - val _ = if_debug prin wit - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',[ex',wit']) = disamb_terms_from info [ex,wit] - val cwit = cterm_of thy wit' - val cty = ctyp_of_term cwit - val a = case ex' of - (Const("Ex",_) $ a) => a - | _ => raise ERR "EXISTS" "Argument not existential" - val ca = cterm_of thy a - val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm) - val th1 = beta_eta_thm th - val th2 = implies_elim_all th1 - val th3 = th2 COMP exists_thm' - val th = implies_intr_hyps th3 - val res = HOLThm(rens_of info',th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "EXISTS:" + val _ = if_debug prin ex + val _ = if_debug prin wit + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',[ex',wit']) = disamb_terms_from info [ex,wit] + val cwit = cterm_of thy wit' + val cty = ctyp_of_term cwit + val a = case ex' of + (Const("Ex",_) $ a) => a + | _ => raise ERR "EXISTS" "Argument not existential" + val ca = cterm_of thy a + val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm) + val th1 = beta_eta_thm th + val th2 = implies_elim_all th1 + val th3 = th2 COMP exists_thm' + val th = implies_intr_hyps th3 + val res = HOLThm(rens_of info',th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun CHOOSE v hth1 hth2 thy = let - val _ = message "CHOOSE:" - val _ = if_debug prin v - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val (info',v') = disamb_term_from info v - fun strip 0 _ th = th - | strip n (p::ps) th = - strip (n-1) ps (implies_elim th (assume p)) - | strip _ _ _ = raise ERR "CHOOSE" "strip error" - val cv = cterm_of thy v' - val th2 = norm_hyps th2 - val cvty = ctyp_of_term cv - val c = HOLogic.dest_Trueprop (concl_of th2) - val cc = cterm_of thy c - val a = case concl_of th1 of - _ $ (Const("Ex",_) $ a) => a - | _ => raise ERR "CHOOSE" "Conclusion not existential" - val ca = cterm_of (theory_of_thm th1) a - val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm) - val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2 - val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21 - val th23 = beta_eta_thm (forall_intr cv th22) - val th11 = implies_elim_all (beta_eta_thm th1) - val th' = th23 COMP (th11 COMP choose_thm') - val th = implies_intr_hyps th' - val res = HOLThm(rens_of info',th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "CHOOSE:" + val _ = if_debug prin v + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val (info',v') = disamb_term_from info v + fun strip 0 _ th = th + | strip n (p::ps) th = + strip (n-1) ps (implies_elim th (assume p)) + | strip _ _ _ = raise ERR "CHOOSE" "strip error" + val cv = cterm_of thy v' + val th2 = norm_hyps th2 + val cvty = ctyp_of_term cv + val c = HOLogic.dest_Trueprop (concl_of th2) + val cc = cterm_of thy c + val a = case concl_of th1 of + _ $ (Const("Ex",_) $ a) => a + | _ => raise ERR "CHOOSE" "Conclusion not existential" + val ca = cterm_of (theory_of_thm th1) a + val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm) + val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2 + val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21 + val th23 = beta_eta_thm (forall_intr cv th22) + val th11 = implies_elim_all (beta_eta_thm th1) + val th' = th23 COMP (th11 COMP choose_thm') + val th = implies_intr_hyps th' + val res = HOLThm(rens_of info',th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun GEN v hth thy = let val _ = message "GEN:" - val _ = if_debug prin v - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',v') = disamb_term_from info v - val res = HOLThm(rens_of info',mk_GEN v' th thy) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = if_debug prin v + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',v') = disamb_term_from info v + val res = HOLThm(rens_of info',mk_GEN v' th thy) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun SPEC tm hth thy = let - val _ = message "SPEC:" - val _ = if_debug prin tm - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',tm') = disamb_term_from info tm - val ctm = Thm.cterm_of thy tm' - val cty = Thm.ctyp_of_term ctm - val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm - val th = th RS spec' - val res = HOLThm(rens_of info',th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "SPEC:" + val _ = if_debug prin tm + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',tm') = disamb_term_from info tm + val ctm = Thm.cterm_of thy tm' + val cty = Thm.ctyp_of_term ctm + val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm + val th = th RS spec' + val res = HOLThm(rens_of info',th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun COMB hth1 hth2 thy = let - val _ = message "COMB:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val res = HOLThm(rens_of info,mk_COMB th1 th2 thy) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "COMB:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val res = HOLThm(rens_of info,mk_COMB th1 th2 thy) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun TRANS hth1 hth2 thy = let - val _ = message "TRANS:" - val _ = if_debug pth hth1 - val _ = if_debug pth hth2 - val (info,[th1,th2]) = disamb_thms [hth1,hth2] - val th = [th1,th2] MRS trans_thm - val res = HOLThm(rens_of info,th) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "TRANS:" + val _ = if_debug pth hth1 + val _ = if_debug pth hth2 + val (info,[th1,th2]) = disamb_thms [hth1,hth2] + val th = [th1,th2] MRS trans_thm + val res = HOLThm(rens_of info,th) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun CCONTR tm hth thy = let - val _ = message "SPEC:" - val _ = if_debug prin tm - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',tm') = disamb_term_from info tm - val th = norm_hyps th - val ct = cterm_of thy tm' - val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th - val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm - val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm' - val res = HOLThm(rens_of info',res1) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "SPEC:" + val _ = if_debug prin tm + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',tm') = disamb_term_from info tm + val th = norm_hyps th + val ct = cterm_of thy tm' + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th + val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm + val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm' + val res = HOLThm(rens_of info',res1) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun mk_ABS v th thy = let - val cv = cterm_of thy v - val th1 = implies_elim_all (beta_eta_thm th) - val (f,g) = case concl_of th1 of - _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g) - | _ => raise ERR "mk_ABS" "Bad conclusion" - val (fd,fr) = dom_rng (type_of f) - val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm - val th2 = forall_intr cv th1 - val th3 = th2 COMP abs_thm' - val res = implies_intr_hyps th3 + val cv = cterm_of thy v + val th1 = implies_elim_all (beta_eta_thm th) + val (f,g) = case concl_of th1 of + _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g) + | _ => raise ERR "mk_ABS" "Bad conclusion" + val (fd,fr) = dom_rng (type_of f) + val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm + val th2 = forall_intr cv th1 + val th3 = th2 COMP abs_thm' + val res = implies_intr_hyps th3 in - res + res end fun ABS v hth thy = let - val _ = message "ABS:" - val _ = if_debug prin v - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',v') = disamb_term_from info v - val res = HOLThm(rens_of info',mk_ABS v' th thy) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "ABS:" + val _ = if_debug prin v + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',v') = disamb_term_from info v + val res = HOLThm(rens_of info',mk_ABS v' th thy) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun GEN_ABS copt vlist hth thy = let - val _ = message "GEN_ABS:" - val _ = case copt of - SOME c => if_debug prin c - | NONE => () - val _ = if_debug (app prin) vlist - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',vlist') = disamb_terms_from info vlist - val th1 = - case copt of - SOME (c as Const(cname,cty)) => - let - fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!" - | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty - then ty2 - else ty - | inst_type ty1 ty2 (ty as Type(name,tys)) = - Type(name,map (inst_type ty1 ty2) tys) - in - foldr (fn (v,th) => - let - val cdom = fst (dom_rng (fst (dom_rng cty))) - val vty = type_of v - val newcty = inst_type cdom vty cty - val cc = cterm_of thy (Const(cname,newcty)) - in - mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy - end) th vlist' - end - | SOME _ => raise ERR "GEN_ABS" "Bad constant" - | NONE => - foldr (fn (v,th) => mk_ABS v th thy) th vlist' - val res = HOLThm(rens_of info',th1) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "GEN_ABS:" + val _ = case copt of + SOME c => if_debug prin c + | NONE => () + val _ = if_debug (app prin) vlist + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',vlist') = disamb_terms_from info vlist + val th1 = + case copt of + SOME (c as Const(cname,cty)) => + let + fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!" + | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty + then ty2 + else ty + | inst_type ty1 ty2 (ty as Type(name,tys)) = + Type(name,map (inst_type ty1 ty2) tys) + in + foldr (fn (v,th) => + let + val cdom = fst (dom_rng (fst (dom_rng cty))) + val vty = type_of v + val newcty = inst_type cdom vty cty + val cc = cterm_of thy (Const(cname,newcty)) + in + mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy + end) th vlist' + end + | SOME _ => raise ERR "GEN_ABS" "Bad constant" + | NONE => + foldr (fn (v,th) => mk_ABS v th thy) th vlist' + val res = HOLThm(rens_of info',th1) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun NOT_INTRO (hth as HOLThm(rens,th)) thy = let - val _ = message "NOT_INTRO:" - val _ = if_debug pth hth - val th1 = implies_elim_all (beta_eta_thm th) - val a = case concl_of th1 of - _ $ (Const("op -->",_) $ a $ Const("False",_)) => a - | _ => raise ERR "NOT_INTRO" "Conclusion of bad form" - val ca = cterm_of thy a - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 - val res = HOLThm(rens,implies_intr_hyps th2) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "NOT_INTRO:" + val _ = if_debug pth hth + val th1 = implies_elim_all (beta_eta_thm th) + val a = case concl_of th1 of + _ $ (Const("op -->",_) $ a $ Const("False",_)) => a + | _ => raise ERR "NOT_INTRO" "Conclusion of bad form" + val ca = cterm_of thy a + val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1 + val res = HOLThm(rens,implies_intr_hyps th2) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun NOT_ELIM (hth as HOLThm(rens,th)) thy = let - val _ = message "NOT_INTRO:" - val _ = if_debug pth hth - val th1 = implies_elim_all (beta_eta_thm th) - val a = case concl_of th1 of - _ $ (Const("Not",_) $ a) => a - | _ => raise ERR "NOT_ELIM" "Conclusion of bad form" - val ca = cterm_of thy a - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 - val res = HOLThm(rens,implies_intr_hyps th2) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "NOT_INTRO:" + val _ = if_debug pth hth + val th1 = implies_elim_all (beta_eta_thm th) + val a = case concl_of th1 of + _ $ (Const("Not",_) $ a) => a + | _ => raise ERR "NOT_ELIM" "Conclusion of bad form" + val ca = cterm_of thy a + val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1 + val res = HOLThm(rens,implies_intr_hyps th2) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end fun DISCH tm hth thy = let - val _ = message "DISCH:" - val _ = if_debug prin tm - val _ = if_debug pth hth - val (info,th) = disamb_thm hth - val (info',tm') = disamb_term_from info tm - val prems = prems_of th - val th1 = beta_eta_thm th - val th2 = implies_elim_all th1 - val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 - val th4 = th3 COMP disch_thm - val res = HOLThm(rens_of info',implies_intr_hyps th4) - val _ = message "RESULT:" - val _ = if_debug pth res + val _ = message "DISCH:" + val _ = if_debug prin tm + val _ = if_debug pth hth + val (info,th) = disamb_thm hth + val (info',tm') = disamb_term_from info tm + val prems = prems_of th + val th1 = beta_eta_thm th + val th2 = implies_elim_all th1 + val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2 + val th4 = th3 COMP disch_thm + val res = HOLThm(rens_of info',implies_intr_hyps th4) + val _ = message "RESULT:" + val _ = if_debug pth res in - (thy,res) + (thy,res) end val spaces = String.concat o separate " " fun new_definition thyname constname rhs thy = let - val constname = rename_const thyname thy constname + val constname = rename_const thyname thy constname val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname)); - val _ = warning ("Introducing constant " ^ constname) - val (thmname,thy) = get_defname thyname constname thy - val (info,rhs') = disamb_term rhs - val ctype = type_of rhs' - val csyn = mk_syn thy constname - val thy1 = case HOL4DefThy.get thy of - Replaying _ => thy - | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy) - val eq = mk_defeq constname rhs' thy1 - val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1 - val _ = ImportRecorder.add_defs thmname eq - val def_thm = hd thms - val thm' = def_thm RS meta_eq_to_obj_eq_thm - val (thy',th) = (thy2, thm') - val fullcname = Sign.intern_const thy' constname - val thy'' = add_hol4_const_mapping thyname constname true fullcname thy' - val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname - val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'') - val rew = rewrite_hol4_term eq thy'' - val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) - val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn - then - let - val p1 = quotename constname - val p2 = string_of_ctyp (ctyp_of thy'' ctype) - val p3 = string_of_mixfix csyn - val p4 = smart_string_of_cterm crhs - in - add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' - end - else - (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ - "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) - thy'') - val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of - SOME (_,res) => HOLThm(rens_of linfo,res) - | NONE => raise ERR "new_definition" "Bad conclusion" - val fullname = Sign.full_name thy22 thmname - val thy22' = case opt_get_output_thy thy22 of - "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; - add_hol4_mapping thyname thmname fullname thy22) - | output_thy => - let - val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname - val _ = ImportRecorder.add_hol_move fullname moved_thmname - val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname - in - thy22 |> add_hol4_move fullname moved_thmname - |> add_hol4_mapping thyname thmname moved_thmname - end - val _ = message "new_definition:" - val _ = if_debug pth hth + val _ = warning ("Introducing constant " ^ constname) + val (thmname,thy) = get_defname thyname constname thy + val (info,rhs') = disamb_term rhs + val ctype = type_of rhs' + val csyn = mk_syn thy constname + val thy1 = case HOL4DefThy.get thy of + Replaying _ => thy + | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy) + val eq = mk_defeq constname rhs' thy1 + val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1 + val _ = ImportRecorder.add_defs thmname eq + val def_thm = hd thms + val thm' = def_thm RS meta_eq_to_obj_eq_thm + val (thy',th) = (thy2, thm') + val fullcname = Sign.intern_const thy' constname + val thy'' = add_hol4_const_mapping thyname constname true fullcname thy' + val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname + val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'') + val rew = rewrite_hol4_term eq thy'' + val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) + val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn + then + let + val p1 = quotename constname + val p2 = string_of_ctyp (ctyp_of thy'' ctype) + val p3 = string_of_mixfix csyn + val p4 = smart_string_of_cterm crhs + in + add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' + end + else + (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ + "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) + thy'') + val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of + SOME (_,res) => HOLThm(rens_of linfo,res) + | NONE => raise ERR "new_definition" "Bad conclusion" + val fullname = Sign.full_name thy22 thmname + val thy22' = case opt_get_output_thy thy22 of + "" => (ImportRecorder.add_hol_mapping thyname thmname fullname; + add_hol4_mapping thyname thmname fullname thy22) + | output_thy => + let + val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname + val _ = ImportRecorder.add_hol_move fullname moved_thmname + val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname + in + thy22 |> add_hol4_move fullname moved_thmname + |> add_hol4_mapping thyname thmname moved_thmname + end + val _ = message "new_definition:" + val _ = if_debug pth hth in - (thy22',hth) + (thy22',hth) end handle e => (message "exception in new_definition"; print_exn e) @@ -1983,81 +1985,81 @@ in fun new_specification thyname thmname names hth thy = case HOL4DefThy.get thy of - Replaying _ => (thy,hth) + Replaying _ => (thy,hth) | _ => - let - val _ = message "NEW_SPEC:" - val _ = if_debug pth hth - val names = map (rename_const thyname thy) names - val _ = warning ("Introducing constants " ^ commas names) - val (HOLThm(rens,th)) = norm_hthm thy hth - val thy1 = case HOL4DefThy.get thy of - Replaying _ => thy - | _ => - let - fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body) - | dest_eta_abs body = - let - val (dT,rT) = dom_rng (type_of body) - in - ("x",dT,body $ Bound 0) - end - handle TYPE _ => raise ERR "new_specification" "not an abstraction type" - fun dest_exists (Const("Ex",_) $ abody) = - dest_eta_abs abody - | dest_exists tm = - raise ERR "new_specification" "Bad existential formula" + let + val _ = message "NEW_SPEC:" + val _ = if_debug pth hth + val names = map (rename_const thyname thy) names + val _ = warning ("Introducing constants " ^ commas names) + val (HOLThm(rens,th)) = norm_hthm thy hth + val thy1 = case HOL4DefThy.get thy of + Replaying _ => thy + | _ => + let + fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body) + | dest_eta_abs body = + let + val (dT,rT) = dom_rng (type_of body) + in + ("x",dT,body $ Bound 0) + end + handle TYPE _ => raise ERR "new_specification" "not an abstraction type" + fun dest_exists (Const("Ex",_) $ abody) = + dest_eta_abs abody + | dest_exists tm = + raise ERR "new_specification" "Bad existential formula" - val (consts,_) = Library.foldl (fn ((cs,ex),cname) => - let - val (_,cT,p) = dest_exists ex - in - ((cname,cT,mk_syn thy cname)::cs,p) - end) (([],HOLogic.dest_Trueprop (concl_of th)),names) - val str = Library.foldl (fn (acc,(c,T,csyn)) => - acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) - val thy' = add_dump str thy - val _ = ImportRecorder.add_consts consts - in - Sign.add_consts_i consts thy' - end + val (consts,_) = Library.foldl (fn ((cs,ex),cname) => + let + val (_,cT,p) = dest_exists ex + in + ((cname,cT,mk_syn thy cname)::cs,p) + end) (([],HOLogic.dest_Trueprop (concl_of th)),names) + val str = Library.foldl (fn (acc,(c,T,csyn)) => + acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) + val thy' = add_dump str thy + val _ = ImportRecorder.add_consts consts + in + Sign.add_consts_i consts thy' + end - val thy1 = foldr (fn(name,thy)=> - snd (get_defname thyname name thy)) thy1 names - fun new_name name = fst (get_defname thyname name thy1) - val names' = map (fn name => (new_name name,name,false)) names - val (thy',res) = SpecificationPackage.add_specification NONE - names' - (thy1,th) - val _ = ImportRecorder.add_specification names' th - val res' = Thm.unvarify res - val hth = HOLThm(rens,res') - val rew = rewrite_hol4_term (concl_of res') thy' - val th = equal_elim rew res' - fun handle_const (name,thy) = - let - val defname = def_name name - val (newname,thy') = get_defname thyname name thy - in - (if defname = newname - then quotename name - else (quotename newname) ^ ": " ^ (quotename name),thy') - end - val (new_names,thy') = foldr (fn(name,(names,thy)) => - let - val (name',thy') = handle_const (name,thy) - in - (name'::names,thy') - end) ([],thy') names - val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^ - "\n by (import " ^ thyname ^ " " ^ thmname ^ ")") - thy' - val _ = message "RESULT:" - val _ = if_debug pth hth - in - intern_store_thm false thyname thmname hth thy'' - end - handle e => (message "exception in new_specification"; print_exn e) + val thy1 = foldr (fn(name,thy)=> + snd (get_defname thyname name thy)) thy1 names + fun new_name name = fst (get_defname thyname name thy1) + val names' = map (fn name => (new_name name,name,false)) names + val (thy',res) = SpecificationPackage.add_specification NONE + names' + (thy1,th) + val _ = ImportRecorder.add_specification names' th + val res' = Thm.unvarify res + val hth = HOLThm(rens,res') + val rew = rewrite_hol4_term (concl_of res') thy' + val th = equal_elim rew res' + fun handle_const (name,thy) = + let + val defname = def_name name + val (newname,thy') = get_defname thyname name thy + in + (if defname = newname + then quotename name + else (quotename newname) ^ ": " ^ (quotename name),thy') + end + val (new_names,thy') = foldr (fn(name,(names,thy)) => + let + val (name',thy') = handle_const (name,thy) + in + (name'::names,thy') + end) ([],thy') names + val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^ + "\n by (import " ^ thyname ^ " " ^ thmname ^ ")") + thy' + val _ = message "RESULT:" + val _ = if_debug pth hth + in + intern_store_thm false thyname thmname hth thy'' + end + handle e => (message "exception in new_specification"; print_exn e) end @@ -2065,9 +2067,9 @@ fun to_isa_thm (hth as HOLThm(_,th)) = let - val (HOLThm args) = norm_hthm (theory_of_thm th) hth + val (HOLThm args) = norm_hthm (theory_of_thm th) hth in - apsnd strip_shyps args + apsnd strip_shyps args end fun to_isa_term tm = tm @@ -2080,74 +2082,74 @@ in fun new_type_definition thyname thmname tycname hth thy = case HOL4DefThy.get thy of - Replaying _ => (thy,hth) + Replaying _ => (thy,hth) | _ => - let - val _ = message "TYPE_DEF:" - val _ = if_debug pth hth - val _ = warning ("Introducing type " ^ tycname) - val (HOLThm(rens,td_th)) = norm_hthm thy hth - val th2 = beta_eta_thm (td_th RS ex_imp_nonempty) - val c = case concl_of th2 of - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c - | _ => raise ERR "new_type_definition" "Bad type definition theorem" - val tfrees = term_tfrees c - val tnames = map fst tfrees - val tsyn = mk_syn thy tycname - val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy + let + val _ = message "TYPE_DEF:" + val _ = if_debug pth hth + val _ = warning ("Introducing type " ^ tycname) + val (HOLThm(rens,td_th)) = norm_hthm thy hth + val th2 = beta_eta_thm (td_th RS ex_imp_nonempty) + val c = case concl_of th2 of + _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c + | _ => raise ERR "new_type_definition" "Bad type definition theorem" + val tfrees = term_tfrees c + val tnames = map fst tfrees + val tsyn = mk_syn thy tycname + val typ = (tycname,tnames,tsyn) + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 - val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 + val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 - val fulltyname = Sign.intern_type thy' tycname - val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname + val fulltyname = Sign.intern_type thy' tycname + val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname - val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3)) - val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") - else () - val thy4 = add_hol4_pending thyname thmname args thy'' - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3)) + val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating") + else () + val thy4 = add_hol4_pending thyname thmname args thy'' + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') - val rew = rewrite_hol4_term (concl_of td_th) thy4 - val th = equal_elim rew (Thm.transfer thy4 td_th) - val c = case HOLogic.dest_Trueprop (prop_of th) of - Const("Ex",exT) $ P => - let - val PT = domain_type exT - in - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P - end - | _ => error "Internal error in ProofKernel.new_typedefinition" - val tnames_string = if null tnames - then "" - else "(" ^ commas tnames ^ ") " - val proc_prop = if null tnames - then smart_string_of_cterm - else Library.setmp show_all_types true smart_string_of_cterm - val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " - ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4 + val rew = rewrite_hol4_term (concl_of td_th) thy4 + val th = equal_elim rew (Thm.transfer thy4 td_th) + val c = case HOLogic.dest_Trueprop (prop_of th) of + Const("Ex",exT) $ P => + let + val PT = domain_type exT + in + Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P + end + | _ => error "Internal error in ProofKernel.new_typedefinition" + val tnames_string = if null tnames + then "" + else "(" ^ commas tnames ^ ") " + val proc_prop = if null tnames + then smart_string_of_cterm + else Library.setmp show_all_types true smart_string_of_cterm + val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " + ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4 - val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5 + val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5 - val _ = message "RESULT:" - val _ = if_debug pth hth' - in - (thy6,hth') - end - handle e => (message "exception in new_type_definition"; print_exn e) + val _ = message "RESULT:" + val _ = if_debug pth hth' + in + (thy6,hth') + end + handle e => (message "exception in new_type_definition"; print_exn e) fun add_dump_constdefs thy defname constname rhs ty = let - val n = quotename constname - val t = string_of_ctyp (ctyp_of thy ty) - val syn = string_of_mixfix (mk_syn thy constname) - (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) + val n = quotename constname + val t = string_of_ctyp (ctyp_of thy ty) + val syn = string_of_mixfix (mk_syn thy constname) + (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) val eq = quote (constname ^ " == "^rhs) - val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " + val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " in - add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy + add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy end fun add_dump_syntax thy name = @@ -2160,85 +2162,85 @@ fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy = case HOL4DefThy.get thy of - Replaying _ => (thy, + Replaying _ => (thy, HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth) | _ => - let + let val _ = message "TYPE_INTRO:" - val _ = if_debug pth hth - val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")") - val (HOLThm(rens,td_th)) = norm_hthm thy hth - val tT = type_of t - val light_nonempty' = - Drule.instantiate' [SOME (ctyp_of thy tT)] - [SOME (cterm_of thy P), - SOME (cterm_of thy t)] light_nonempty - val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty')) - val c = case concl_of th2 of - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c - | _ => raise ERR "type_introduction" "Bad type definition theorem" - val tfrees = term_tfrees c - val tnames = sort string_ord (map fst tfrees) - val tsyn = mk_syn thy tycname - val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy - val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 - val fulltyname = Sign.intern_type thy' tycname - val aty = Type (fulltyname, map mk_vartype tnames) - val abs_ty = tT --> aty - val rep_ty = aty --> tT + val _ = if_debug pth hth + val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")") + val (HOLThm(rens,td_th)) = norm_hthm thy hth + val tT = type_of t + val light_nonempty' = + Drule.instantiate' [SOME (ctyp_of thy tT)] + [SOME (cterm_of thy P), + SOME (cterm_of thy t)] light_nonempty + val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty')) + val c = case concl_of th2 of + _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c + | _ => raise ERR "type_introduction" "Bad type definition theorem" + val tfrees = term_tfrees c + val tnames = sort string_ord (map fst tfrees) + val tsyn = mk_syn thy tycname + val typ = (tycname,tnames,tsyn) + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy + val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 + val fulltyname = Sign.intern_type thy' tycname + val aty = Type (fulltyname, map mk_vartype tnames) + val abs_ty = tT --> aty + val rep_ty = aty --> tT val typedef_hol2hollight' = - Drule.instantiate' - [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] - [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] + Drule.instantiate' + [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)] + [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))] typedef_hol2hollight - val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' + val th4 = (#type_definition typedef_info) RS typedef_hol2hollight' val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse raise ERR "type_introduction" "no type variables expected any more" val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse raise ERR "type_introduction" "no term variables expected any more" - val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) + val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname) val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy' - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname val _ = message "step 4" - val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) - val thy4 = add_hol4_pending thyname thmname args thy'' - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4)) + val thy4 = add_hol4_pending thyname thmname args thy'' + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') - val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *) - val c = - let - val PT = type_of P' - in - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P' - end + val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *) + val c = + let + val PT = type_of P' + in + Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P' + end - val tnames_string = if null tnames - then "" - else "(" ^ commas tnames ^ ") " - val proc_prop = if null tnames - then smart_string_of_cterm - else Library.setmp show_all_types true smart_string_of_cterm - val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ + val tnames_string = if null tnames + then "" + else "(" ^ commas tnames ^ ") " + val proc_prop = if null tnames + then smart_string_of_cterm + else Library.setmp show_all_types true smart_string_of_cterm + val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^ - (string_of_mixfix tsyn) ^ " morphisms "^ + (string_of_mixfix tsyn) ^ " morphisms "^ (quote rep_name)^" "^(quote abs_name)^"\n"^ - (" apply (rule light_ex_imp_nonempty[where t="^ + (" apply (rule light_ex_imp_nonempty[where t="^ (proc_prop (cterm_of thy4 t))^"])\n"^ - (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 - val str_aty = string_of_ctyp (ctyp_of thy aty) + (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 + val str_aty = string_of_ctyp (ctyp_of thy aty) val thy = add_dump_syntax thy rep_name val thy = add_dump_syntax thy abs_name - val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ + val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ " = typedef_hol2hollight \n"^ " [where a=\"a :: "^str_aty^"\" and r=r" ^ - " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy - val _ = message "RESULT:" - val _ = if_debug pth hth' - in - (thy,hth') - end - handle e => (message "exception in type_introduction"; print_exn e) + " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy + val _ = message "RESULT:" + val _ = if_debug pth hth' + in + (thy,hth') + end + handle e => (message "exception in type_introduction"; print_exn e) end val prin = prin diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/TFL/dcterm.ML --- a/src/HOL/Tools/TFL/dcterm.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/TFL/dcterm.ML Sat Apr 12 17:00:35 2008 +0200 @@ -187,7 +187,10 @@ *---------------------------------------------------------------------------*) fun mk_prop ctm = - let val {t, thy, ...} = Thm.rep_cterm ctm in + let + val thy = Thm.theory_of_cterm ctm; + val t = Thm.term_of ctm; + in if can HOLogic.dest_Trueprop t then ctm else Thm.cterm_of thy (HOLogic.mk_Trueprop t) end diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/TFL/post.ML Sat Apr 12 17:00:35 2008 +0200 @@ -93,7 +93,7 @@ fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L)) fun join_assums th = - let val {thy,...} = rep_thm th + let val thy = Thm.theory_of_thm th val tych = cterm_of thy val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/TFL/rules.ML Sat Apr 12 17:00:35 2008 +0200 @@ -171,7 +171,8 @@ (*---------------------------------------------------------------------------- * Disjunction *---------------------------------------------------------------------------*) -local val {prop,thy,...} = rep_thm disjI1 +local val thy = Thm.theory_of_thm disjI1 + val prop = Thm.prop_of disjI1 val [P,Q] = term_vars prop val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1 in @@ -179,7 +180,8 @@ handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; end; -local val {prop,thy,...} = rep_thm disjI2 +local val thy = Thm.theory_of_thm disjI2 + val prop = Thm.prop_of disjI2 val [P,Q] = term_vars prop val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2 in @@ -274,17 +276,15 @@ * Universals *---------------------------------------------------------------------------*) local (* this is fragile *) - val {prop,thy,...} = rep_thm spec + val thy = Thm.theory_of_thm spec + val prop = Thm.prop_of spec val x = hd (tl (term_vars prop)) val cTV = ctyp_of thy (type_of x) val gspec = forall_intr (cterm_of thy x) spec in fun SPEC tm thm = - let val {thy,T,...} = rep_cterm tm - val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec - in - thm RS (forall_elim tm gspec') - end + let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec + in thm RS (forall_elim tm gspec') end end; fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm; @@ -293,7 +293,8 @@ val ISPECL = fold ISPEC; (* Not optimized! Too complicated. *) -local val {prop,thy,...} = rep_thm allI +local val thy = Thm.theory_of_thm allI + val prop = Thm.prop_of allI val [P] = add_term_vars (prop, []) fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty)) fun ctm_theta s = map (fn (i, (_, tm2)) => @@ -306,12 +307,13 @@ in fun GEN v th = let val gth = forall_intr v th - val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth + val thy = Thm.theory_of_thm gth + val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); val allI2 = instantiate (certify thy theta) allI val thm = Thm.implies_elim allI2 gth - val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm + val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm val prop' = tp $ (A $ Abs(x,ty,M)) in ALPHA thm (cterm_of thy prop') end @@ -320,7 +322,8 @@ val GENL = fold_rev GEN; fun GEN_ALL thm = - let val {prop,thy,...} = rep_thm thm + let val thy = Thm.theory_of_thm thm + val prop = Thm.prop_of thm val tycheck = cterm_of thy val vlist = map tycheck (add_term_vars (prop, [])) in GENL vlist thm @@ -352,18 +355,21 @@ let val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) val redex = D.capply lam fvar - val {thy, t = t$u,...} = Thm.rep_cterm redex + val thy = Thm.theory_of_cterm redex + val t$u = Thm.term_of redex val residue = Thm.cterm_of thy (Term.betapply (t, u)) in GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg end; -local val {prop,thy,...} = rep_thm exI +local val thy = Thm.theory_of_thm exI + val prop = Thm.prop_of exI val [P,x] = term_vars prop in fun EXISTS (template,witness) thm = - let val {prop,thy,...} = rep_thm thm + let val thy = Thm.theory_of_thm thm + val prop = Thm.prop_of thm val P' = cterm_of thy P val x' = cterm_of thy x val abstr = #2 (D.dest_comb template) @@ -396,16 +402,15 @@ (* Could be improved, but needs "subst_free" for certified terms *) fun IT_EXISTS blist th = - let val {thy,...} = rep_thm th + let val thy = Thm.theory_of_thm th val tych = cterm_of thy - val detype = #t o rep_cterm - val blist' = map (fn (x,y) => (detype x, detype y)) blist + val blist' = map (pairself Thm.term_of) blist fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M}) in fold_rev (fn (b as (r1,r2)) => fn thm => EXISTS(ex r2 (subst_free [b] - (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) + (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1) thm) blist' th end; @@ -451,13 +456,10 @@ (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) fun is_cong thm = - let val {prop, ...} = rep_thm thm - in case prop + case (Thm.prop_of thm) of (Const("==>",_)$(Const("Trueprop",_)$ _) $ (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false - | _ => true - end; - + | _ => true; fun dest_equal(Const ("==",_) $ @@ -521,9 +523,9 @@ (* Note: rename_params_rule counts from 1, not 0 *) fun rename thm = - let val {prop,thy,...} = rep_thm thm + let val thy = Thm.theory_of_thm thm val tych = cterm_of thy - val ants = Logic.strip_imp_prems prop + val ants = Logic.strip_imp_prems (Thm.prop_of thm) val news = get (ants,1,[]) in fold rename_params_rule news thm @@ -745,12 +747,12 @@ end end fun eliminate thm = - case (rep_thm thm) - of {prop = (Const("==>",_) $ imp $ _), thy, ...} => + case Thm.prop_of thm + of Const("==>",_) $ imp $ _ => eliminate (if not(is_all imp) - then uq_eliminate (thm,imp,thy) - else q_eliminate (thm,imp,thy)) + then uq_eliminate (thm, imp, Thm.theory_of_thm thm) + else q_eliminate (thm, imp, Thm.theory_of_thm thm)) (* Assume that the leading constant is ==, *) | _ => thm (* if it is not a ==> *) in SOME(eliminate (rename thm)) end @@ -760,8 +762,8 @@ let val dummy = say "restrict_prover:" val cntxt = rev(MetaSimplifier.prems_of_ss ss) val dummy = print_thms "cntxt:" cntxt - val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, - thy,...} = rep_thm thm + val thy = Thm.theory_of_thm thm + val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm fun genl tm = let val vlist = subtract (op aconv) globals (add_term_frees(tm,[])) in fold_rev Forall vlist tm @@ -814,7 +816,8 @@ fun prove strict (ptm, tac) = let - val {thy, t, ...} = Thm.rep_cterm ptm; + val thy = Thm.theory_of_cterm ptm; + val t = Thm.term_of ptm; val ctxt = ProofContext.init thy |> Variable.auto_fixes t; in if strict then Goal.prove ctxt [] [] t (K tac) diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Sat Apr 12 17:00:35 2008 +0200 @@ -27,8 +27,7 @@ in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end; fun prf_of thm = - let val {thy, prop, der = (_, prf), ...} = rep_thm thm - in Reconstruct.reconstruct_proof thy prop prf end; + Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); fun prf_subst_vars inst = Proofterm.map_proof_terms (subst_vars ([], inst)) I; diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Apr 12 17:00:35 2008 +0200 @@ -359,7 +359,8 @@ fun mk_funs_inv thm = let - val {thy, prop, ...} = rep_thm thm; + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $ (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop; val used = add_term_tfree_names (a, []); diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Apr 12 17:00:35 2008 +0200 @@ -24,8 +24,10 @@ val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps"); fun prf_of thm = - let val {thy, prop, der = (_, prf), ...} = rep_thm thm - in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *) + let + val thy = Thm.theory_of_thm thm; + val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm); + in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *) fun forall_intr_prf (t, prf) = let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p) diff -r e0cc4169626e -r c6231d64d264 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOL/Tools/record_package.ML Sat Apr 12 17:00:35 2008 +0200 @@ -1740,7 +1740,8 @@ fun meta_to_obj_all thm = let - val {thy, prop, ...} = rep_thm thm; + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; val params = Logic.strip_params prop; val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop); val ct = cterm_of thy diff -r e0cc4169626e -r c6231d64d264 src/HOLCF/Tools/adm_tac.ML --- a/src/HOLCF/Tools/adm_tac.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/HOLCF/Tools/adm_tac.ML Sat Apr 12 17:00:35 2008 +0200 @@ -110,8 +110,9 @@ (*** instantiation of adm_subst theorem (a bit tricky) ***) fun inst_adm_subst_thm state i params s T subt t paths = - let val {thy = sign, maxidx, ...} = rep_thm state; - val j = maxidx+1; + let + val sign = Thm.theory_of_thm state; + val j = Thm.maxidx_of state + 1; val parTs = map snd (rev params); val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst}; val types = valOf o (fst (types_sorts rule)); diff -r e0cc4169626e -r c6231d64d264 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 12 17:00:35 2008 +0200 @@ -564,7 +564,8 @@ NONE => let val (ctxt, (_, thm)) = Proof.get_goal state; - val {thy, der = (_, prf), ...} = Thm.rep_thm thm; + val thy = ProofContext.theory_of ctxt; + val prf = Thm.proof_of thm; val prop = Thm.full_prop_of thm; val prf' = Proofterm.rewrite_proof_notypes ([], []) prf in diff -r e0cc4169626e -r c6231d64d264 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/Proof/extraction.ML Sat Apr 12 17:00:35 2008 +0200 @@ -711,7 +711,9 @@ fun prep_thm (thm, vs) = let - val {prop, der = (_, prf), thy, ...} = rep_thm thm; + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; + val prf = Thm.proof_of thm; val name = Thm.get_name thm; val _ = name <> "" orelse error "extraction: unnamed theorem"; val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^ diff -r e0cc4169626e -r c6231d64d264 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 12 17:00:35 2008 +0200 @@ -259,8 +259,9 @@ fun proof_of full thm = let - val {thy, der = (_, prf), ...} = Thm.rep_thm thm; + val thy = Thm.theory_of_thm thm; val prop = Thm.full_prop_of thm; + val prf = Thm.proof_of thm; val prf' = (case strip_combt (fst (strip_combP prf)) of (PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf | _ => prf) diff -r e0cc4169626e -r c6231d64d264 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/codegen.ML Sat Apr 12 17:00:35 2008 +0200 @@ -1074,8 +1074,8 @@ Logic.mk_equals (t, eval_term thy t); fun evaluation_conv ct = - let val {thy, t, ...} = rep_cterm ct - in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end; + let val thy = Thm.theory_of_cterm ct + in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end; val _ = Context.>> (Context.map_theory (Theory.add_oracle ("evaluation", evaluation_oracle))); diff -r e0cc4169626e -r c6231d64d264 src/Pure/display.ML --- a/src/Pure/display.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/display.ML Sat Apr 12 17:00:35 2008 +0200 @@ -109,20 +109,12 @@ (* other printing commands *) -fun pretty_ctyp cT = - let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end; - -fun string_of_ctyp cT = - let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end; - +fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT); +fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT); val print_ctyp = writeln o string_of_ctyp; -fun pretty_cterm ct = - let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end; - -fun string_of_cterm ct = - let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end; - +fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct); +fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct); val print_cterm = writeln o string_of_cterm; diff -r e0cc4169626e -r c6231d64d264 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/meta_simplifier.ML Sat Apr 12 17:00:35 2008 +0200 @@ -458,7 +458,8 @@ fun decomp_simp thm = let - val {thy, prop, ...} = Thm.rep_thm thm; + val thy = Thm.theory_of_thm thm; + val prop = Thm.prop_of thm; val prems = Logic.strip_imp_prems prop; val concl = Drule.strip_imp_concl (Thm.cprop_of thm); val (lhs, rhs) = Thm.dest_equals concl handle TERM _ => @@ -833,7 +834,10 @@ (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm') in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end handle THM _ => - let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in + let + val thy = Thm.theory_of_thm thm; + val _ $ _ $ prop0 = Thm.prop_of thm; + in trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; trace_term false (fn () => "Should have proved:") ss thy prop0; NONE @@ -897,7 +901,8 @@ val eta_t = term_of eta_t'; fun rew {thm, name, lhs, elhs, extra, fo, perm} = let - val {thy, prop, maxidx, ...} = rep_thm thm; + val thy = Thm.theory_of_thm thm; + val {prop, maxidx, ...} = rep_thm thm; val (rthm, elhs') = if maxt = ~1 orelse not extra then (thm, elhs) else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs); @@ -1233,8 +1238,9 @@ fun rewrite_cterm mode prover raw_ss raw_ct = let + val thy = Thm.theory_of_cterm raw_ct; val ct = Thm.adjust_maxidx_cterm ~1 raw_ct; - val {thy, t, maxidx, ...} = Thm.rep_cterm ct; + val {t, maxidx, ...} = Thm.rep_cterm ct; val ss = inc_simp_depth (activate_context thy raw_ss); val depth = simp_depth ss; val _ = diff -r e0cc4169626e -r c6231d64d264 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/old_goals.ML Sat Apr 12 17:00:35 2008 +0200 @@ -151,7 +151,8 @@ fun prepare_proof atomic rths chorn = let val _ = legacy_feature "Old goal command"; - val {thy, t=horn,...} = rep_cterm chorn; + val thy = Thm.theory_of_cterm chorn; + val horn = Thm.term_of chorn; val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; val (As, B) = Logic.strip_horn horn; val atoms = atomic andalso @@ -170,7 +171,8 @@ val ngoals = nprems_of state val ath = implies_intr_list cAs state val th = Goal.conclude ath - val {hyps,prop,thy=thy',...} = rep_thm th + val thy' = Thm.theory_of_thm th + val {hyps, prop, ...} = Thm.rep_thm th val final_th = standard th in if not check then final_th else if not (eq_thy(thy,thy')) then !result_error_fn state @@ -229,7 +231,7 @@ SOME(st,_) => st | _ => error ("prove_goal: tactic failed")) in mkresult (check, cond_timeit (!Output.timing) "" statef) end - handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e; + handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e; writeln ("The exception above was raised for\n" ^ Display.string_of_cterm chorn); raise e); diff -r e0cc4169626e -r c6231d64d264 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/pure_thy.ML Sat Apr 12 17:00:35 2008 +0200 @@ -337,7 +337,8 @@ fun forall_elim_vars_aux strip_vars i th = let - val {thy, tpairs, prop, ...} = Thm.rep_thm th; + val thy = Thm.theory_of_thm th; + val {tpairs, prop, ...} = Thm.rep_thm th; val add_used = Term.fold_aterms (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I); val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []); diff -r e0cc4169626e -r c6231d64d264 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/tactic.ML Sat Apr 12 17:00:35 2008 +0200 @@ -263,15 +263,19 @@ i.e. Tinsts is not applied to insts. *) fun term_lift_inst_rule (st, i, Tinsts, insts, rule) = -let val {maxidx,thy,...} = rep_thm st +let + val thy = Thm.theory_of_thm st + val cert = Thm.cterm_of thy + val certT = Thm.ctyp_of thy + val maxidx = Thm.maxidx_of st val paramTs = map #2 (params_of_state i st) - and inc = maxidx+1 + val inc = maxidx+1 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T) (*lift only Var, not term, which must be lifted already*) - fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t) + fun liftpair (v,t) = (cert (liftvar v), cert t) fun liftTpair (((a, i), S), T) = - (ctyp_of thy (TVar ((a, i + inc), S)), - ctyp_of thy (Logic.incr_tvar inc T)) + (certT (TVar ((a, i + inc), S)), + certT (Logic.incr_tvar inc T)) in Drule.instantiate (map liftTpair Tinsts, map liftpair insts) (Thm.lift_rule (Thm.cprem_of st i) rule) end; diff -r e0cc4169626e -r c6231d64d264 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Pure/tctical.ML Sat Apr 12 17:00:35 2008 +0200 @@ -425,8 +425,8 @@ fun metahyps_aux_tac tacf (prem,gno) state = let val (insts,params,hyps,concl) = metahyps_split_prem prem - val {thy = sign,maxidx,...} = rep_thm state - val cterm = cterm_of sign + val maxidx = Thm.maxidx_of state + val cterm = Thm.cterm_of (Thm.theory_of_thm state) val chyps = map cterm hyps val hypths = map assume chyps val subprems = map (forall_elim_vars 0) hypths diff -r e0cc4169626e -r c6231d64d264 src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Sat Apr 12 17:00:35 2008 +0200 @@ -43,7 +43,7 @@ open Report; -datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML +datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML (* Terms are mapped to integer codes *) structure Encode :> @@ -52,10 +52,10 @@ val empty : encoding val insert : term -> encoding -> int * encoding val lookup_code : term -> encoding -> int option - val lookup_term : int -> encoding -> term option + val lookup_term : int -> encoding -> term option val remove_code : int -> encoding -> encoding val remove_term : term -> encoding -> encoding - val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a + val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a end = struct @@ -66,7 +66,7 @@ fun insert t (e as (count, term2int, int2term)) = (case Termtab.lookup term2int t of - NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term)) + NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term)) | SOME code => (code, e)) fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t @@ -88,29 +88,29 @@ local fun make_constant t ty encoding = - let - val (code, encoding) = Encode.insert t encoding - in - (encoding, AbstractMachine.Const code) - end + let + val (code, encoding) = Encode.insert t encoding + in + (encoding, AbstractMachine.Const code) + end in fun remove_types encoding t = case t of - Var (_, ty) => make_constant t ty encoding + Var (_, ty) => make_constant t ty encoding | Free (_, ty) => make_constant t ty encoding | Const (_, ty) => make_constant t ty encoding | Abs (_, ty, t') => - let val (encoding, t'') = remove_types encoding t' in - (encoding, AbstractMachine.Abs t'') - end + let val (encoding, t'') = remove_types encoding t' in + (encoding, AbstractMachine.Abs t'') + end | a $ b => - let - val (encoding, a) = remove_types encoding a - val (encoding, b) = remove_types encoding b - in - (encoding, AbstractMachine.App (a,b)) - end + let + val (encoding, a) = remove_types encoding a + val (encoding, b) = remove_types encoding b + in + (encoding, AbstractMachine.App (a,b)) + end | Bound b => (encoding, AbstractMachine.Var b) end @@ -123,23 +123,23 @@ fun infer_types naming encoding = let fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v)) - | infer_types _ bounds _ (AbstractMachine.Const code) = - let - val c = the (Encode.lookup_term code encoding) - in - (c, type_of c) - end - | infer_types level bounds _ (AbstractMachine.App (a, b)) = - let - val (a, aty) = infer_types level bounds NONE a - val (adom, arange) = + | infer_types _ bounds _ (AbstractMachine.Const code) = + let + val c = the (Encode.lookup_term code encoding) + in + (c, type_of c) + end + | infer_types level bounds _ (AbstractMachine.App (a, b)) = + let + val (a, aty) = infer_types level bounds NONE a + val (adom, arange) = case aty of Type ("fun", [dom, range]) => (dom, range) | _ => sys_error "infer_types: function type expected" val (b, bty) = infer_types level bounds (SOME adom) b - in - (a $ b, arange) - end + in + (a $ b, arange) + end | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) = let val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m @@ -160,7 +160,7 @@ end datatype prog = - ProgBarras of AM_Interpreter.program + ProgBarras of AM_Interpreter.program | ProgBarrasC of AM_Compiler.program | ProgHaskell of AM_GHC.program | ProgSML of AM_SML.program @@ -198,26 +198,26 @@ fun thm2cthm th = let - val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th - val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () + val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th + val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () in - ComputeThm (hyps, shyps, prop) + ComputeThm (hyps, shyps, prop) end fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths = let - fun transfer (x:thm) = Thm.transfer thy x - val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths + fun transfer (x:thm) = Thm.transfer thy x + val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths fun make_pattern encoding n vars (var as AbstractMachine.Abs _) = - raise (Make "no lambda abstractions allowed in pattern") - | make_pattern encoding n vars (var as AbstractMachine.Var _) = - raise (Make "no bound variables allowed in pattern") - | make_pattern encoding n vars (AbstractMachine.Const code) = - (case the (Encode.lookup_term code encoding) of - Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar) - handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed")) - | _ => (n, vars, AbstractMachine.PConst (code, []))) + raise (Make "no lambda abstractions allowed in pattern") + | make_pattern encoding n vars (var as AbstractMachine.Var _) = + raise (Make "no bound variables allowed in pattern") + | make_pattern encoding n vars (AbstractMachine.Const code) = + (case the (Encode.lookup_term code encoding) of + Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar) + handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed")) + | _ => (n, vars, AbstractMachine.PConst (code, []))) | make_pattern encoding n vars (AbstractMachine.App (a, b)) = let val (n, vars, pa) = make_pattern encoding n vars a @@ -232,26 +232,26 @@ fun thm2rule (encoding, hyptable, shyptable) th = let - val (ComputeThm (hyps, shyps, prop)) = th - val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable - val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable - val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) + val (ComputeThm (hyps, shyps, prop)) = th + val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable + val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable + val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) val (a, b) = Logic.dest_equals prop handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)") - val a = Envir.eta_contract a - val b = Envir.eta_contract b - val prems = map Envir.eta_contract prems + val a = Envir.eta_contract a + val b = Envir.eta_contract b + val prems = map Envir.eta_contract prems val (encoding, left) = remove_types encoding a - val (encoding, right) = remove_types encoding b + val (encoding, right) = remove_types encoding b fun remove_types_of_guard encoding g = - (let - val (t1, t2) = Logic.dest_equals g - val (encoding, t1) = remove_types encoding t1 - val (encoding, t2) = remove_types encoding t2 - in - (encoding, AbstractMachine.Guard (t1, t2)) - end handle TERM _ => raise (Make "guards must be meta-level equations")) + (let + val (t1, t2) = Logic.dest_equals g + val (encoding, t1) = remove_types encoding t1 + val (encoding, t2) = remove_types encoding t2 + in + (encoding, AbstractMachine.Guard (t1, t2)) + end handle TERM _ => raise (Make "guards must be meta-level equations")) val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, []) (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule. @@ -263,24 +263,24 @@ AbstractMachine.PVar => raise (Make "patterns may not start with a variable") (* | AbstractMachine.PConst (_, []) => - (print th; raise (Make "no parameter rewrite found"))*) - | _ => ()) + (print th; raise (Make "no parameter rewrite found"))*) + | _ => ()) (* finally, provide a function for renaming the pattern bound variables on the right hand side *) fun rename level vars (var as AbstractMachine.Var _) = var - | rename level vars (c as AbstractMachine.Const code) = - (case Inttab.lookup vars code of - NONE => c - | SOME n => AbstractMachine.Var (vcount-n-1+level)) + | rename level vars (c as AbstractMachine.Const code) = + (case Inttab.lookup vars code of + NONE => c + | SOME n => AbstractMachine.Var (vcount-n-1+level)) | rename level vars (AbstractMachine.App (a, b)) = AbstractMachine.App (rename level vars a, rename level vars b) | rename level vars (AbstractMachine.Abs m) = AbstractMachine.Abs (rename (level+1) vars m) - - fun rename_guard (AbstractMachine.Guard (a,b)) = - AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) + + fun rename_guard (AbstractMachine.Guard (a,b)) = + AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) in ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right)) end @@ -293,35 +293,35 @@ ths ((encoding, Termtab.empty, Sorttab.empty), []) fun make_cache_pattern t (encoding, cache_patterns) = - let - val (encoding, a) = remove_types encoding t - val (_,_,p) = make_pattern encoding 0 Inttab.empty a - in - (encoding, p::cache_patterns) - end - - val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) + let + val (encoding, a) = remove_types encoding t + val (_,_,p) = make_pattern encoding 0 Inttab.empty a + in + (encoding, p::cache_patterns) + end + + val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) - fun arity (Type ("fun", [a,b])) = 1 + arity b - | arity _ = 0 + fun arity (Type ("fun", [a,b])) = 1 + arity b + | arity _ = 0 - fun make_arity (Const (s, _), i) tab = - (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab) - | make_arity _ tab = tab + fun make_arity (Const (s, _), i) tab = + (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab) + | make_arity _ tab = tab - val const_arity_tab = Encode.fold make_arity encoding Inttab.empty - fun const_arity x = Inttab.lookup const_arity_tab x + val const_arity_tab = Encode.fold make_arity encoding Inttab.empty + fun const_arity x = Inttab.lookup const_arity_tab x val prog = - case machine of - BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules) - | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules) - | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules) - | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules) + case machine of + BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules) + | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules) + | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules) + | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules) fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable + val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end @@ -331,32 +331,32 @@ fun update_with_cache computer cache_patterns raw_thms = let - val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) - (encoding_of computer) cache_patterns raw_thms - val _ = (ref_of computer) := SOME c + val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) + (encoding_of computer) cache_patterns raw_thms + val _ = (ref_of computer) := SOME c in - () + () end fun update computer raw_thms = update_with_cache computer [] raw_thms fun discard computer = let - val _ = - case prog_of computer of - ProgBarras p => AM_Interpreter.discard p - | ProgBarrasC p => AM_Compiler.discard p - | ProgHaskell p => AM_GHC.discard p - | ProgSML p => AM_SML.discard p - val _ = (ref_of computer) := NONE + val _ = + case prog_of computer of + ProgBarras p => AM_Interpreter.discard p + | ProgBarrasC p => AM_Compiler.discard p + | ProgHaskell p => AM_GHC.discard p + | ProgSML p => AM_SML.discard p + val _ = (ref_of computer) := NONE in - () + () end - + fun runprog (ProgBarras p) = AM_Interpreter.run p | runprog (ProgBarrasC p) = AM_Compiler.run p | runprog (ProgHaskell p) = AM_GHC.run p - | runprog (ProgSML p) = AM_SML.run p + | runprog (ProgSML p) = AM_SML.run p (* ------------------------------------------------------------------------------------- *) (* An oracle for exporting theorems; must only be accessible from inside this structure! *) @@ -377,15 +377,15 @@ fun export_oracle (thy, ExportThm (hyps, shyps, prop)) = let - val shyptab = add_shyps shyps Sorttab.empty - fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab - fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab - fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) - val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab - val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) - val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else () + val shyptab = add_shyps shyps Sorttab.empty + fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab + fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab + fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) + val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab + val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) + val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else () in - fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop + fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop end | export_oracle _ = raise Match @@ -393,24 +393,25 @@ fun export_thm thy hyps shyps prop = let - val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop)) - val hyps = map (fn h => assume (cterm_of thy h)) hyps + val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop)) + val hyps = map (fn h => assume (cterm_of thy h)) hyps in - fold (fn h => fn p => implies_elim p h) hyps th + fold (fn h => fn p => implies_elim p h) hyps th end - + (* --------- Rewrite ----------- *) fun rewrite computer ct = let - val {t=t',T=ty,thy=thy,...} = rep_cterm ct - val _ = Theory.assert_super (theory_of computer) thy - val naming = naming_of computer + val thy = Thm.theory_of_cterm ct + val {t=t',T=ty,...} = rep_cterm ct + val _ = Theory.assert_super (theory_of computer) thy + val naming = naming_of computer val (encoding, t) = remove_types (encoding_of computer) t' - (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) + (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) val t = runprog (prog_of computer) t val t = infer_types naming encoding ty t - val eq = Logic.mk_equals (t', t) + val eq = Logic.mk_equals (t', t) in export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq end @@ -418,7 +419,7 @@ (* --------- Simplify ------------ *) datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int - | Prem of AbstractMachine.term + | Prem of AbstractMachine.term datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table * prem list * AbstractMachine.term * term list * sort list @@ -439,46 +440,46 @@ | collect_vars (Const _) tab = tab | collect_vars (Free _) tab = tab | collect_vars (Var ((s, i), ty)) tab = - if List.find (fn x => x=s) vars = NONE then - tab - else - (case Symtab.lookup tab s of - SOME ((s',i'),ty') => - if s' <> s orelse i' <> i orelse ty <> ty' then - raise Compute ("make_theorem: variable name '"^s^"' is not unique") - else - tab - | NONE => Symtab.update (s, ((s, i), ty)) tab) + if List.find (fn x => x=s) vars = NONE then + tab + else + (case Symtab.lookup tab s of + SOME ((s',i'),ty') => + if s' <> s orelse i' <> i orelse ty <> ty' then + raise Compute ("make_theorem: variable name '"^s^"' is not unique") + else + tab + | NONE => Symtab.update (s, ((s, i), ty)) tab) val vartab = collect_vars prop Symtab.empty fun encodevar (s, t as (_, ty)) (encoding, tab) = - let - val (x, encoding) = Encode.insert (Var t) encoding - in - (encoding, Symtab.update (s, (x, ty)) tab) - end - val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) + let + val (x, encoding) = Encode.insert (Var t) encoding + in + (encoding, Symtab.update (s, (x, ty)) tab) + end + val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab)) (* make the premises and the conclusion *) fun mk_prem encoding t = - (let - val (a, b) = Logic.dest_equals t - val ty = type_of a - val (encoding, a) = remove_types encoding a - val (encoding, b) = remove_types encoding b - val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding - in - (encoding, EqPrem (a, b, ty, eq)) - end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) + (let + val (a, b) = Logic.dest_equals t + val ty = type_of a + val (encoding, a) = remove_types encoding a + val (encoding, b) = remove_types encoding b + val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding + in + (encoding, EqPrem (a, b, ty, eq)) + end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) val (encoding, prems) = - (fold_rev (fn t => fn (encoding, l) => - case mk_prem encoding t of + (fold_rev (fn t => fn (encoding, l) => + case mk_prem encoding t of (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, [])) val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) val _ = set_encoding computer encoding in Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, - prems, concl, hyps, shyps) + prems, concl, hyps, shyps) end fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy @@ -498,7 +499,7 @@ fun check_compatible computer th s = if stamp_of computer <> stamp_of_theorem th then - raise Compute (s^": computer and theorem are incompatible") + raise Compute (s^": computer and theorem are incompatible") else () fun instantiate computer insts th = @@ -511,49 +512,49 @@ fun rewrite computer t = let - val naming = naming_of computer + val naming = naming_of computer val (encoding, t) = remove_types (encoding_of computer) t val t = runprog (prog_of computer) t - val _ = set_encoding computer encoding + val _ = set_encoding computer encoding in t end fun assert_varfree vs t = - if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then - () - else - raise Compute "instantiate: assert_varfree failed" + if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then + () + else + raise Compute "instantiate: assert_varfree failed" fun assert_closed t = - if AbstractMachine.closed t then - () - else - raise Compute "instantiate: not a closed term" + if AbstractMachine.closed t then + () + else + raise Compute "instantiate: not a closed term" fun compute_inst (s, ct) vs = - let - val _ = Theory.assert_super (theory_of_cterm ct) thy - val ty = typ_of (ctyp_of_term ct) - in - (case Symtab.lookup vartab s of - NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") - | SOME (x, ty') => - (case Inttab.lookup vs x of - SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") - | SOME NONE => - if ty <> ty' then - raise Compute ("instantiate: wrong type for variable '"^s^"'") - else - let - val t = rewrite computer (term_of ct) - val _ = assert_varfree vs t - val _ = assert_closed t - in - Inttab.update (x, SOME t) vs - end - | NONE => raise Compute "instantiate: internal error")) - end + let + val _ = Theory.assert_super (theory_of_cterm ct) thy + val ty = typ_of (ctyp_of_term ct) + in + (case Symtab.lookup vartab s of + NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") + | SOME (x, ty') => + (case Inttab.lookup vs x of + SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") + | SOME NONE => + if ty <> ty' then + raise Compute ("instantiate: wrong type for variable '"^s^"'") + else + let + val t = rewrite computer (term_of ct) + val _ = assert_varfree vs t + val _ = assert_closed t + in + Inttab.update (x, SOME t) vs + end + | NONE => raise Compute "instantiate: internal error")) + end val vs = fold compute_inst insts (varsubst_of_theorem th) in @@ -561,39 +562,39 @@ end fun match_aterms subst = - let - exception no_match - open AbstractMachine - fun match subst (b as (Const c)) a = - if a = b then subst - else - (case Inttab.lookup subst c of - SOME (SOME a') => if a=a' then subst else raise no_match - | SOME NONE => if AbstractMachine.closed a then - Inttab.update (c, SOME a) subst - else raise no_match - | NONE => raise no_match) - | match subst (b as (Var _)) a = if a=b then subst else raise no_match - | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' - | match subst (Abs u) (Abs u') = match subst u u' - | match subst _ _ = raise no_match + let + exception no_match + open AbstractMachine + fun match subst (b as (Const c)) a = + if a = b then subst + else + (case Inttab.lookup subst c of + SOME (SOME a') => if a=a' then subst else raise no_match + | SOME NONE => if AbstractMachine.closed a then + Inttab.update (c, SOME a) subst + else raise no_match + | NONE => raise no_match) + | match subst (b as (Var _)) a = if a=b then subst else raise no_match + | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' + | match subst (Abs u) (Abs u') = match subst u u' + | match subst _ _ = raise no_match in - fn b => fn a => (SOME (match subst b a) handle no_match => NONE) + fn b => fn a => (SOME (match subst b a) handle no_match => NONE) end fun apply_subst vars_allowed subst = let - open AbstractMachine - fun app (t as (Const c)) = - (case Inttab.lookup subst c of - NONE => t - | SOME (SOME t) => Computed t - | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") - | app (t as (Var _)) = t - | app (App (u, v)) = App (app u, app v) - | app (Abs m) = Abs (app m) + open AbstractMachine + fun app (t as (Const c)) = + (case Inttab.lookup subst c of + NONE => t + | SOME (SOME t) => Computed t + | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") + | app (t as (Var _)) = t + | app (App (u, v)) = App (app u, app v) + | app (Abs m) = Abs (app m) in - app + app end fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1) @@ -604,27 +605,27 @@ val prems = prems_of_theorem th val varsubst = varsubst_of_theorem th fun run vars_allowed t = - runprog (prog_of computer) (apply_subst vars_allowed varsubst t) + runprog (prog_of computer) (apply_subst vars_allowed varsubst t) in case List.nth (prems, prem_no) of - Prem _ => raise Compute "evaluate_prem: no equality premise" - | EqPrem (a, b, ty, _) => - let - val a' = run false a - val b' = run true b - in - case match_aterms varsubst b' a' of - NONE => - let - fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s) - val left = "computed left side: "^(mk a') - val right = "computed right side: "^(mk b') - in - raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") - end - | SOME varsubst => - update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) - end + Prem _ => raise Compute "evaluate_prem: no equality premise" + | EqPrem (a, b, ty, _) => + let + val a' = run false a + val b' = run true b + in + case match_aterms varsubst b' a' of + NONE => + let + fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s) + val left = "computed left side: "^(mk a') + val right = "computed right side: "^(mk b') + in + raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") + end + | SOME varsubst => + update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) + end end fun prem2term (Prem t) = t @@ -635,33 +636,33 @@ let val _ = check_compatible computer th val thy = - let - val thy1 = theory_of_theorem th - val thy2 = theory_of_thm th' - in - if Context.subthy (thy1, thy2) then thy2 - else if Context.subthy (thy2, thy1) then thy1 else - raise Compute "modus_ponens: theorems are not compatible with each other" - end + let + val thy1 = theory_of_theorem th + val thy2 = theory_of_thm th' + in + if Context.subthy (thy1, thy2) then thy2 + else if Context.subthy (thy2, thy1) then thy1 else + raise Compute "modus_ponens: theorems are not compatible with each other" + end val th' = make_theorem computer th' [] val varsubst = varsubst_of_theorem th fun run vars_allowed t = - runprog (prog_of computer) (apply_subst vars_allowed varsubst t) + runprog (prog_of computer) (apply_subst vars_allowed varsubst t) val prems = prems_of_theorem th val prem = run true (prem2term (List.nth (prems, prem_no))) val concl = run false (concl_of_theorem th') in case match_aterms varsubst prem concl of - NONE => raise Compute "modus_ponens: conclusion does not match premise" + NONE => raise Compute "modus_ponens: conclusion does not match premise" | SOME varsubst => - let - val th = update_varsubst varsubst th - val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th - val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th - val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th - in - update_theory thy th - end + let + val th = update_varsubst varsubst th + val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th + val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th + val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th + in + update_theory thy th + end end fun simplify computer th = diff -r e0cc4169626e -r c6231d64d264 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Apr 10 20:54:18 2008 +0200 +++ b/src/Tools/induct.ML Sat Apr 12 17:00:35 2008 +0200 @@ -280,10 +280,11 @@ fun prep_var (x, SOME t) = let val cx = cert x; - val {T = xT, thy, ...} = Thm.rep_cterm cx; + val xT = #T (Thm.rep_cterm cx); val ct = cert (tune t); + val tT = Thm.ctyp_of_term ct; in - if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) + if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct) else error (Pretty.string_of (Pretty.block [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, @@ -432,7 +433,8 @@ fun guess_instance rule i st = let - val {thy, maxidx, ...} = Thm.rep_thm st; + val thy = Thm.theory_of_thm st; + val maxidx = Thm.maxidx_of st; val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*) val params = rev (rename_wrt_term goal (Logic.strip_params goal)); in