1.1 --- a/src/HOL/Import/proof_kernel.ML Thu Apr 10 20:54:18 2008 +0200
1.2 +++ b/src/HOL/Import/proof_kernel.ML Sat Apr 12 17:00:35 2008 +0200
1.3 @@ -13,42 +13,42 @@
1.4
1.5 type proof_info
1.6 datatype proof = Proof of proof_info * proof_content
1.7 - and proof_content
1.8 - = PRefl of term
1.9 - | PInstT of proof * (hol_type,hol_type) subst
1.10 - | PSubst of proof list * term * proof
1.11 - | PAbs of proof * term
1.12 - | PDisch of proof * term
1.13 - | PMp of proof * proof
1.14 - | PHyp of term
1.15 - | PAxm of string * term
1.16 - | PDef of string * string * term
1.17 - | PTmSpec of string * string list * proof
1.18 - | PTyDef of string * string * proof
1.19 - | PTyIntro of string * string * string * string * term * term * proof
1.20 - | POracle of tag * term list * term
1.21 - | PDisk
1.22 - | PSpec of proof * term
1.23 - | PInst of proof * (term,term) subst
1.24 - | PGen of proof * term
1.25 - | PGenAbs of proof * term option * term list
1.26 - | PImpAS of proof * proof
1.27 - | PSym of proof
1.28 - | PTrans of proof * proof
1.29 - | PComb of proof * proof
1.30 - | PEqMp of proof * proof
1.31 - | PEqImp of proof
1.32 - | PExists of proof * term * term
1.33 - | PChoose of term * proof * proof
1.34 - | PConj of proof * proof
1.35 - | PConjunct1 of proof
1.36 - | PConjunct2 of proof
1.37 - | PDisj1 of proof * term
1.38 - | PDisj2 of proof * term
1.39 - | PDisjCases of proof * proof * proof
1.40 - | PNotI of proof
1.41 - | PNotE of proof
1.42 - | PContr of proof * term
1.43 + and proof_content
1.44 + = PRefl of term
1.45 + | PInstT of proof * (hol_type,hol_type) subst
1.46 + | PSubst of proof list * term * proof
1.47 + | PAbs of proof * term
1.48 + | PDisch of proof * term
1.49 + | PMp of proof * proof
1.50 + | PHyp of term
1.51 + | PAxm of string * term
1.52 + | PDef of string * string * term
1.53 + | PTmSpec of string * string list * proof
1.54 + | PTyDef of string * string * proof
1.55 + | PTyIntro of string * string * string * string * term * term * proof
1.56 + | POracle of tag * term list * term
1.57 + | PDisk
1.58 + | PSpec of proof * term
1.59 + | PInst of proof * (term,term) subst
1.60 + | PGen of proof * term
1.61 + | PGenAbs of proof * term option * term list
1.62 + | PImpAS of proof * proof
1.63 + | PSym of proof
1.64 + | PTrans of proof * proof
1.65 + | PComb of proof * proof
1.66 + | PEqMp of proof * proof
1.67 + | PEqImp of proof
1.68 + | PExists of proof * term * term
1.69 + | PChoose of term * proof * proof
1.70 + | PConj of proof * proof
1.71 + | PConjunct1 of proof
1.72 + | PConjunct2 of proof
1.73 + | PDisj1 of proof * term
1.74 + | PDisj2 of proof * term
1.75 + | PDisjCases of proof * proof * proof
1.76 + | PNotI of proof
1.77 + | PNotE of proof
1.78 + | PContr of proof * term
1.79
1.80 exception PK of string * string
1.81
1.82 @@ -178,7 +178,7 @@
1.83
1.84 fun print_exn e =
1.85 case e of
1.86 - PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
1.87 + PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e)
1.88 | _ => OldGoals.print_exn e
1.89
1.90 (* Compatibility. *)
1.91 @@ -194,47 +194,49 @@
1.92
1.93 fun simple_smart_string_of_cterm ct =
1.94 let
1.95 - val {thy,t,T,...} = rep_cterm ct
1.96 - (* Hack to avoid parse errors with Trueprop *)
1.97 - val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
1.98 - handle TERM _ => ct)
1.99 + val thy = Thm.theory_of_cterm ct;
1.100 + val {t,T,...} = rep_cterm ct
1.101 + (* Hack to avoid parse errors with Trueprop *)
1.102 + val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
1.103 + handle TERM _ => ct)
1.104 in
1.105 - quote(
1.106 - PrintMode.setmp [] (
1.107 - Library.setmp show_brackets false (
1.108 - Library.setmp show_all_types true (
1.109 - Library.setmp Syntax.ambiguity_is_error false (
1.110 - Library.setmp show_sorts true string_of_cterm))))
1.111 - ct)
1.112 + quote(
1.113 + PrintMode.setmp [] (
1.114 + Library.setmp show_brackets false (
1.115 + Library.setmp show_all_types true (
1.116 + Library.setmp Syntax.ambiguity_is_error false (
1.117 + Library.setmp show_sorts true string_of_cterm))))
1.118 + ct)
1.119 end
1.120
1.121 exception SMART_STRING
1.122
1.123 fun smart_string_of_cterm ct =
1.124 let
1.125 - val {thy,t,T,...} = rep_cterm ct
1.126 + val thy = Thm.theory_of_cterm ct
1.127 val ctxt = ProofContext.init thy
1.128 + val {t,T,...} = rep_cterm ct
1.129 (* Hack to avoid parse errors with Trueprop *)
1.130 - val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
1.131 - handle TERM _ => ct)
1.132 - fun match u = t aconv u
1.133 - fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
1.134 - | G 1 = Library.setmp show_brackets true (G 0)
1.135 - | G 2 = Library.setmp show_all_types true (G 0)
1.136 - | G 3 = Library.setmp show_brackets true (G 2)
1.137 + val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
1.138 + handle TERM _ => ct)
1.139 + fun match u = t aconv u
1.140 + fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
1.141 + | G 1 = Library.setmp show_brackets true (G 0)
1.142 + | G 2 = Library.setmp show_all_types true (G 0)
1.143 + | G 3 = Library.setmp show_brackets true (G 2)
1.144 | G _ = raise SMART_STRING
1.145 - fun F n =
1.146 - let
1.147 - val str = Library.setmp show_brackets false (G n string_of_cterm) ct
1.148 - val u = Syntax.parse_term ctxt str
1.149 + fun F n =
1.150 + let
1.151 + val str = Library.setmp show_brackets false (G n string_of_cterm) ct
1.152 + val u = Syntax.parse_term ctxt str
1.153 |> TypeInfer.constrain T |> Syntax.check_term ctxt
1.154 - in
1.155 - if match u
1.156 - then quote str
1.157 - else F (n+1)
1.158 - end
1.159 - handle ERROR mesg => F (n+1)
1.160 - | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
1.161 + in
1.162 + if match u
1.163 + then quote str
1.164 + else F (n+1)
1.165 + end
1.166 + handle ERROR mesg => F (n+1)
1.167 + | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct))
1.168 in
1.169 PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
1.170 end
1.171 @@ -247,11 +249,11 @@
1.172 fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
1.173 fun pth (HOLThm(ren,thm)) =
1.174 let
1.175 - (*val _ = writeln "Renaming:"
1.176 - val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
1.177 - val _ = prth thm
1.178 + (*val _ = writeln "Renaming:"
1.179 + val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*)
1.180 + val _ = prth thm
1.181 in
1.182 - ()
1.183 + ()
1.184 end
1.185
1.186 fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info
1.187 @@ -267,16 +269,16 @@
1.188
1.189 fun assoc x =
1.190 let
1.191 - fun F [] = raise PK("Lib.assoc","Not found")
1.192 - | F ((x',y)::rest) = if x = x'
1.193 - then y
1.194 - else F rest
1.195 + fun F [] = raise PK("Lib.assoc","Not found")
1.196 + | F ((x',y)::rest) = if x = x'
1.197 + then y
1.198 + else F rest
1.199 in
1.200 - F
1.201 + F
1.202 end
1.203 fun i mem L =
1.204 let fun itr [] = false
1.205 - | itr (a::rst) = i=a orelse itr rst
1.206 + | itr (a::rst) = i=a orelse itr rst
1.207 in itr L end;
1.208
1.209 fun insert i L = if i mem L then L else i::L
1.210 @@ -305,7 +307,7 @@
1.211 (* Actual code. *)
1.212
1.213 fun get_segment thyname l = (Lib.assoc "s" l
1.214 - handle PK _ => thyname)
1.215 + handle PK _ => thyname)
1.216 val get_name : (string * string) list -> string = Lib.assoc "n"
1.217
1.218 local
1.219 @@ -333,43 +335,43 @@
1.220
1.221 fun scan_string str c =
1.222 let
1.223 - fun F [] toks = (c,toks)
1.224 - | F (c::cs) toks =
1.225 - case LazySeq.getItem toks of
1.226 - SOME(c',toks') =>
1.227 - if c = c'
1.228 - then F cs toks'
1.229 - else raise SyntaxError
1.230 - | NONE => raise SyntaxError
1.231 + fun F [] toks = (c,toks)
1.232 + | F (c::cs) toks =
1.233 + case LazySeq.getItem toks of
1.234 + SOME(c',toks') =>
1.235 + if c = c'
1.236 + then F cs toks'
1.237 + else raise SyntaxError
1.238 + | NONE => raise SyntaxError
1.239 in
1.240 - F (String.explode str)
1.241 + F (String.explode str)
1.242 end
1.243
1.244 local
1.245 val scan_entity =
1.246 - (scan_string "amp;" #"&")
1.247 - || scan_string "quot;" #"\""
1.248 - || scan_string "gt;" #">"
1.249 - || scan_string "lt;" #"<"
1.250 + (scan_string "amp;" #"&")
1.251 + || scan_string "quot;" #"\""
1.252 + || scan_string "gt;" #">"
1.253 + || scan_string "lt;" #"<"
1.254 || scan_string "apos;" #"'"
1.255 in
1.256 fun scan_nonquote toks =
1.257 case LazySeq.getItem toks of
1.258 - SOME (c,toks') =>
1.259 - (case c of
1.260 - #"\"" => raise SyntaxError
1.261 - | #"&" => scan_entity toks'
1.262 - | c => (c,toks'))
1.263 + SOME (c,toks') =>
1.264 + (case c of
1.265 + #"\"" => raise SyntaxError
1.266 + | #"&" => scan_entity toks'
1.267 + | c => (c,toks'))
1.268 | NONE => raise SyntaxError
1.269 end
1.270
1.271 val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
1.272 - String.implode
1.273 + String.implode
1.274
1.275 val scan_attribute = scan_id -- $$ #"=" |-- scan_string
1.276
1.277 val scan_start_of_tag = $$ #"<" |-- scan_id --
1.278 - repeat ($$ #" " |-- scan_attribute)
1.279 + repeat ($$ #" " |-- scan_attribute)
1.280
1.281 (* The evaluation delay introduced through the 'toks' argument is needed
1.282 for the sake of the SML/NJ (110.9.1) compiler. Either that or an explicit
1.283 @@ -379,15 +381,15 @@
1.284 val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
1.285
1.286 fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
1.287 - (fn (chldr,id') => if id = id'
1.288 - then chldr
1.289 - else raise XML "Tag mismatch")
1.290 + (fn (chldr,id') => if id = id'
1.291 + then chldr
1.292 + else raise XML "Tag mismatch")
1.293 and scan_tag toks =
1.294 let
1.295 - val ((id,atts),toks2) = scan_start_of_tag toks
1.296 - val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
1.297 + val ((id,atts),toks2) = scan_start_of_tag toks
1.298 + val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
1.299 in
1.300 - (Elem (id,atts,chldr),toks3)
1.301 + (Elem (id,atts,chldr),toks3)
1.302 end
1.303 end
1.304
1.305 @@ -398,28 +400,28 @@
1.306
1.307 fun mk_defeq name rhs thy =
1.308 let
1.309 - val ty = type_of rhs
1.310 + val ty = type_of rhs
1.311 in
1.312 - Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
1.313 + Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs)
1.314 end
1.315
1.316 fun mk_teq name rhs thy =
1.317 let
1.318 - val ty = type_of rhs
1.319 + val ty = type_of rhs
1.320 in
1.321 - HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
1.322 + HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs)
1.323 end
1.324
1.325 fun intern_const_name thyname const thy =
1.326 case get_hol4_const_mapping thyname const thy of
1.327 - SOME (_,cname,_) => cname
1.328 + SOME (_,cname,_) => cname
1.329 | NONE => (case get_hol4_const_renaming thyname const thy of
1.330 - SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
1.331 - | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
1.332 + SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname)
1.333 + | NONE => Sign.intern_const thy (thyname ^ "." ^ const))
1.334
1.335 fun intern_type_name thyname const thy =
1.336 case get_hol4_type_mapping thyname const thy of
1.337 - SOME (_,cname) => cname
1.338 + SOME (_,cname) => cname
1.339 | NONE => Sign.intern_const thy (thyname ^ "." ^ const)
1.340
1.341 fun mk_vartype name = TFree(name,["HOL.type"])
1.342 @@ -454,16 +456,16 @@
1.343 (* Needed for HOL Light *)
1.344 fun protect_tyvarname s =
1.345 let
1.346 - fun no_quest s =
1.347 - if Char.contains s #"?"
1.348 - then String.translate (fn #"?" => "q_" | c => Char.toString c) s
1.349 - else s
1.350 - fun beg_prime s =
1.351 - if String.isPrefix "'" s
1.352 - then s
1.353 - else "'" ^ s
1.354 + fun no_quest s =
1.355 + if Char.contains s #"?"
1.356 + then String.translate (fn #"?" => "q_" | c => Char.toString c) s
1.357 + else s
1.358 + fun beg_prime s =
1.359 + if String.isPrefix "'" s
1.360 + then s
1.361 + else "'" ^ s
1.362 in
1.363 - s |> no_quest |> beg_prime
1.364 + s |> no_quest |> beg_prime
1.365 end
1.366
1.367 val protected_varnames = ref (Symtab.empty:string Symtab.table)
1.368 @@ -485,26 +487,26 @@
1.369 SOME t => t
1.370 | NONE =>
1.371 let
1.372 - val _ = inc invented_isavar
1.373 - val t = "u_" ^ string_of_int (!invented_isavar)
1.374 - val _ = ImportRecorder.protect_varname s t
1.375 + val _ = inc invented_isavar
1.376 + val t = "u_" ^ string_of_int (!invented_isavar)
1.377 + val _ = ImportRecorder.protect_varname s t
1.378 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
1.379 in
1.380 - t
1.381 + t
1.382 end
1.383
1.384 exception REPLAY_PROTECT_VARNAME of string*string*string
1.385
1.386 fun replay_protect_varname s t =
1.387 - case Symtab.lookup (!protected_varnames) s of
1.388 - SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
1.389 - | NONE =>
1.390 + case Symtab.lookup (!protected_varnames) s of
1.391 + SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t')
1.392 + | NONE =>
1.393 let
1.394 - val _ = inc invented_isavar
1.395 - val t = "u_" ^ string_of_int (!invented_isavar)
1.396 + val _ = inc invented_isavar
1.397 + val t = "u_" ^ string_of_int (!invented_isavar)
1.398 val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
1.399 in
1.400 - ()
1.401 + ()
1.402 end
1.403
1.404 fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u"
1.405 @@ -554,46 +556,46 @@
1.406
1.407 fun get_type_from_index thy thyname types is =
1.408 case Int.fromString is of
1.409 - SOME i => (case Array.sub(types,i) of
1.410 - FullType ty => ty
1.411 - | XMLty xty =>
1.412 - let
1.413 - val ty = get_type_from_xml thy thyname types xty
1.414 - val _ = Array.update(types,i,FullType ty)
1.415 - in
1.416 - ty
1.417 - end)
1.418 + SOME i => (case Array.sub(types,i) of
1.419 + FullType ty => ty
1.420 + | XMLty xty =>
1.421 + let
1.422 + val ty = get_type_from_xml thy thyname types xty
1.423 + val _ = Array.update(types,i,FullType ty)
1.424 + in
1.425 + ty
1.426 + end)
1.427 | NONE => raise ERR "get_type_from_index" "Bad index"
1.428 and get_type_from_xml thy thyname types =
1.429 let
1.430 - fun gtfx (Elem("tyi",[("i",iS)],[])) =
1.431 - get_type_from_index thy thyname types iS
1.432 - | gtfx (Elem("tyc",atts,[])) =
1.433 - mk_thy_type thy
1.434 - (get_segment thyname atts)
1.435 - (protect_tyname (get_name atts))
1.436 - []
1.437 - | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
1.438 - | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
1.439 - mk_thy_type thy
1.440 - (get_segment thyname atts)
1.441 - (protect_tyname (get_name atts))
1.442 - (map gtfx tys)
1.443 - | gtfx _ = raise ERR "get_type" "Bad type"
1.444 + fun gtfx (Elem("tyi",[("i",iS)],[])) =
1.445 + get_type_from_index thy thyname types iS
1.446 + | gtfx (Elem("tyc",atts,[])) =
1.447 + mk_thy_type thy
1.448 + (get_segment thyname atts)
1.449 + (protect_tyname (get_name atts))
1.450 + []
1.451 + | gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s)
1.452 + | gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) =
1.453 + mk_thy_type thy
1.454 + (get_segment thyname atts)
1.455 + (protect_tyname (get_name atts))
1.456 + (map gtfx tys)
1.457 + | gtfx _ = raise ERR "get_type" "Bad type"
1.458 in
1.459 - gtfx
1.460 + gtfx
1.461 end
1.462
1.463 fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
1.464 let
1.465 - val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
1.466 - fun IT _ [] = ()
1.467 - | IT n (xty::xtys) =
1.468 - (Array.update(types,n,XMLty xty);
1.469 - IT (n+1) xtys)
1.470 - val _ = IT 0 xtys
1.471 + val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
1.472 + fun IT _ [] = ()
1.473 + | IT n (xty::xtys) =
1.474 + (Array.update(types,n,XMLty xty);
1.475 + IT (n+1) xtys)
1.476 + val _ = IT 0 xtys
1.477 in
1.478 - types
1.479 + types
1.480 end
1.481 | input_types _ _ = raise ERR "input_types" "Bad type list"
1.482 end
1.483 @@ -603,392 +605,392 @@
1.484
1.485 fun get_term_from_index thy thyname types terms is =
1.486 case Int.fromString is of
1.487 - SOME i => (case Array.sub(terms,i) of
1.488 - FullTerm tm => tm
1.489 - | XMLtm xtm =>
1.490 - let
1.491 - val tm = get_term_from_xml thy thyname types terms xtm
1.492 - val _ = Array.update(terms,i,FullTerm tm)
1.493 - in
1.494 - tm
1.495 - end)
1.496 + SOME i => (case Array.sub(terms,i) of
1.497 + FullTerm tm => tm
1.498 + | XMLtm xtm =>
1.499 + let
1.500 + val tm = get_term_from_xml thy thyname types terms xtm
1.501 + val _ = Array.update(terms,i,FullTerm tm)
1.502 + in
1.503 + tm
1.504 + end)
1.505 | NONE => raise ERR "get_term_from_index" "Bad index"
1.506 and get_term_from_xml thy thyname types terms =
1.507 let
1.508 - fun get_type [] = NONE
1.509 - | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
1.510 - | get_type _ = raise ERR "get_term" "Bad type"
1.511 + fun get_type [] = NONE
1.512 + | get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty)
1.513 + | get_type _ = raise ERR "get_term" "Bad type"
1.514
1.515 - fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
1.516 - mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
1.517 - | gtfx (Elem("tmc",atts,[])) =
1.518 - let
1.519 - val segment = get_segment thyname atts
1.520 - val name = protect_constname(get_name atts)
1.521 - in
1.522 - mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
1.523 - handle PK _ => prim_mk_const thy segment name
1.524 - end
1.525 - | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) =
1.526 - let
1.527 - val f = get_term_from_index thy thyname types terms tmf
1.528 - val a = get_term_from_index thy thyname types terms tma
1.529 - in
1.530 - mk_comb(f,a)
1.531 - end
1.532 - | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
1.533 - let
1.534 + fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) =
1.535 + mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi)
1.536 + | gtfx (Elem("tmc",atts,[])) =
1.537 + let
1.538 + val segment = get_segment thyname atts
1.539 + val name = protect_constname(get_name atts)
1.540 + in
1.541 + mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts))
1.542 + handle PK _ => prim_mk_const thy segment name
1.543 + end
1.544 + | gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) =
1.545 + let
1.546 + val f = get_term_from_index thy thyname types terms tmf
1.547 + val a = get_term_from_index thy thyname types terms tma
1.548 + in
1.549 + mk_comb(f,a)
1.550 + end
1.551 + | gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) =
1.552 + let
1.553 val x = get_term_from_index thy thyname types terms tmx
1.554 val a = get_term_from_index thy thyname types terms tma
1.555 - in
1.556 - mk_lambda x a
1.557 - end
1.558 - | gtfx (Elem("tmi",[("i",iS)],[])) =
1.559 - get_term_from_index thy thyname types terms iS
1.560 - | gtfx (Elem(tag,_,_)) =
1.561 - raise ERR "get_term" ("Not a term: "^tag)
1.562 + in
1.563 + mk_lambda x a
1.564 + end
1.565 + | gtfx (Elem("tmi",[("i",iS)],[])) =
1.566 + get_term_from_index thy thyname types terms iS
1.567 + | gtfx (Elem(tag,_,_)) =
1.568 + raise ERR "get_term" ("Not a term: "^tag)
1.569 in
1.570 - gtfx
1.571 + gtfx
1.572 end
1.573
1.574 fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
1.575 let
1.576 - val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
1.577 + val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
1.578
1.579 - fun IT _ [] = ()
1.580 - | IT n (xtm::xtms) =
1.581 - (Array.update(terms,n,XMLtm xtm);
1.582 - IT (n+1) xtms)
1.583 - val _ = IT 0 xtms
1.584 + fun IT _ [] = ()
1.585 + | IT n (xtm::xtms) =
1.586 + (Array.update(terms,n,XMLtm xtm);
1.587 + IT (n+1) xtms)
1.588 + val _ = IT 0 xtms
1.589 in
1.590 - terms
1.591 + terms
1.592 end
1.593 | input_terms _ _ _ = raise ERR "input_terms" "Bad term list"
1.594 end
1.595
1.596 fun get_proof_dir (thyname:string) thy =
1.597 let
1.598 - val import_segment =
1.599 - case get_segment2 thyname thy of
1.600 - SOME seg => seg
1.601 - | NONE => get_import_segment thy
1.602 - val path = space_explode ":" (getenv "HOL4_PROOFS")
1.603 - fun find [] = NONE
1.604 - | find (p::ps) =
1.605 - (let
1.606 - val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
1.607 - in
1.608 - if OS.FileSys.isDir dir
1.609 - then SOME dir
1.610 - else find ps
1.611 - end) handle OS.SysErr _ => find ps
1.612 + val import_segment =
1.613 + case get_segment2 thyname thy of
1.614 + SOME seg => seg
1.615 + | NONE => get_import_segment thy
1.616 + val path = space_explode ":" (getenv "HOL4_PROOFS")
1.617 + fun find [] = NONE
1.618 + | find (p::ps) =
1.619 + (let
1.620 + val dir = OS.Path.joinDirFile {dir = p,file=import_segment}
1.621 + in
1.622 + if OS.FileSys.isDir dir
1.623 + then SOME dir
1.624 + else find ps
1.625 + end) handle OS.SysErr _ => find ps
1.626 in
1.627 - Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
1.628 + Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path)
1.629 end
1.630
1.631 fun proof_file_name thyname thmname thy =
1.632 let
1.633 - val path = case get_proof_dir thyname thy of
1.634 - SOME p => p
1.635 - | NONE => error "Cannot find proof files"
1.636 - val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
1.637 + val path = case get_proof_dir thyname thy of
1.638 + SOME p => p
1.639 + | NONE => error "Cannot find proof files"
1.640 + val _ = OS.FileSys.mkDir path handle OS.SysErr _ => ()
1.641 in
1.642 - OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
1.643 + OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}}
1.644 end
1.645
1.646 fun xml_to_proof thyname types terms prf thy =
1.647 let
1.648 - val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
1.649 - val xml_to_term = TermNet.get_term_from_xml thy thyname types terms
1.650 + val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types
1.651 + val xml_to_term = TermNet.get_term_from_xml thy thyname types terms
1.652
1.653 - fun index_to_term is =
1.654 - TermNet.get_term_from_index thy thyname types terms is
1.655 + fun index_to_term is =
1.656 + TermNet.get_term_from_index thy thyname types terms is
1.657
1.658 - fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is))
1.659 - | x2p (Elem("pinstt",[],p::lambda)) =
1.660 - let
1.661 - val p = x2p p
1.662 - val lambda = implode_subst (map xml_to_hol_type lambda)
1.663 - in
1.664 - mk_proof (PInstT(p,lambda))
1.665 - end
1.666 - | x2p (Elem("psubst",[("i",is)],prf::prfs)) =
1.667 - let
1.668 - val tm = index_to_term is
1.669 - val prf = x2p prf
1.670 - val prfs = map x2p prfs
1.671 - in
1.672 - mk_proof (PSubst(prfs,tm,prf))
1.673 - end
1.674 - | x2p (Elem("pabs",[("i",is)],[prf])) =
1.675 - let
1.676 - val p = x2p prf
1.677 - val t = index_to_term is
1.678 - in
1.679 - mk_proof (PAbs (p,t))
1.680 - end
1.681 - | x2p (Elem("pdisch",[("i",is)],[prf])) =
1.682 - let
1.683 - val p = x2p prf
1.684 - val t = index_to_term is
1.685 - in
1.686 - mk_proof (PDisch (p,t))
1.687 - end
1.688 - | x2p (Elem("pmp",[],[prf1,prf2])) =
1.689 - let
1.690 - val p1 = x2p prf1
1.691 - val p2 = x2p prf2
1.692 - in
1.693 - mk_proof (PMp(p1,p2))
1.694 - end
1.695 - | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is))
1.696 - | x2p (Elem("paxiom",[("n",n),("i",is)],[])) =
1.697 - mk_proof (PAxm(n,index_to_term is))
1.698 - | x2p (Elem("pfact",atts,[])) =
1.699 - let
1.700 - val thyname = get_segment thyname atts
1.701 - val thmname = protect_factname (get_name atts)
1.702 - val p = mk_proof PDisk
1.703 - val _ = set_disk_info_of p thyname thmname
1.704 - in
1.705 - p
1.706 - end
1.707 - | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
1.708 - mk_proof (PDef(seg,protect_constname name,index_to_term is))
1.709 - | x2p (Elem("ptmspec",[("s",seg)],p::names)) =
1.710 - let
1.711 - val names = map (fn Elem("name",[("n",name)],[]) => name
1.712 - | _ => raise ERR "x2p" "Bad proof (ptmspec)") names
1.713 - in
1.714 - mk_proof (PTmSpec(seg,names,x2p p))
1.715 - end
1.716 - | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) =
1.717 - let
1.718 - val P = xml_to_term xP
1.719 - val t = xml_to_term xt
1.720 - in
1.721 - mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
1.722 - end
1.723 - | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
1.724 - mk_proof (PTyDef(seg,protect_tyname name,x2p p))
1.725 - | x2p (xml as Elem("poracle",[],chldr)) =
1.726 - let
1.727 - val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
1.728 - val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
1.729 - val (c,asl) = case terms of
1.730 - [] => raise ERR "x2p" "Bad oracle description"
1.731 - | (hd::tl) => (hd,tl)
1.732 - val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
1.733 - in
1.734 - mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
1.735 - end
1.736 - | x2p (Elem("pspec",[("i",is)],[prf])) =
1.737 - let
1.738 - val p = x2p prf
1.739 - val tm = index_to_term is
1.740 - in
1.741 - mk_proof (PSpec(p,tm))
1.742 - end
1.743 - | x2p (Elem("pinst",[],p::theta)) =
1.744 - let
1.745 - val p = x2p p
1.746 - val theta = implode_subst (map xml_to_term theta)
1.747 - in
1.748 - mk_proof (PInst(p,theta))
1.749 - end
1.750 - | x2p (Elem("pgen",[("i",is)],[prf])) =
1.751 - let
1.752 - val p = x2p prf
1.753 - val tm = index_to_term is
1.754 - in
1.755 - mk_proof (PGen(p,tm))
1.756 - end
1.757 - | x2p (Elem("pgenabs",[],prf::tms)) =
1.758 - let
1.759 - val p = x2p prf
1.760 - val tml = map xml_to_term tms
1.761 - in
1.762 - mk_proof (PGenAbs(p,NONE,tml))
1.763 - end
1.764 - | x2p (Elem("pgenabs",[("i",is)],prf::tms)) =
1.765 - let
1.766 - val p = x2p prf
1.767 - val tml = map xml_to_term tms
1.768 - in
1.769 - mk_proof (PGenAbs(p,SOME (index_to_term is),tml))
1.770 - end
1.771 - | x2p (Elem("pimpas",[],[prf1,prf2])) =
1.772 - let
1.773 - val p1 = x2p prf1
1.774 - val p2 = x2p prf2
1.775 - in
1.776 - mk_proof (PImpAS(p1,p2))
1.777 - end
1.778 - | x2p (Elem("psym",[],[prf])) =
1.779 - let
1.780 - val p = x2p prf
1.781 - in
1.782 - mk_proof (PSym p)
1.783 - end
1.784 - | x2p (Elem("ptrans",[],[prf1,prf2])) =
1.785 - let
1.786 - val p1 = x2p prf1
1.787 - val p2 = x2p prf2
1.788 - in
1.789 - mk_proof (PTrans(p1,p2))
1.790 - end
1.791 - | x2p (Elem("pcomb",[],[prf1,prf2])) =
1.792 - let
1.793 - val p1 = x2p prf1
1.794 - val p2 = x2p prf2
1.795 - in
1.796 - mk_proof (PComb(p1,p2))
1.797 - end
1.798 - | x2p (Elem("peqmp",[],[prf1,prf2])) =
1.799 - let
1.800 - val p1 = x2p prf1
1.801 - val p2 = x2p prf2
1.802 - in
1.803 - mk_proof (PEqMp(p1,p2))
1.804 - end
1.805 - | x2p (Elem("peqimp",[],[prf])) =
1.806 - let
1.807 - val p = x2p prf
1.808 - in
1.809 - mk_proof (PEqImp p)
1.810 - end
1.811 - | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) =
1.812 - let
1.813 - val p = x2p prf
1.814 - val ex = index_to_term ise
1.815 - val w = index_to_term isw
1.816 - in
1.817 - mk_proof (PExists(p,ex,w))
1.818 - end
1.819 - | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) =
1.820 - let
1.821 - val v = index_to_term is
1.822 - val p1 = x2p prf1
1.823 - val p2 = x2p prf2
1.824 - in
1.825 - mk_proof (PChoose(v,p1,p2))
1.826 - end
1.827 - | x2p (Elem("pconj",[],[prf1,prf2])) =
1.828 - let
1.829 - val p1 = x2p prf1
1.830 - val p2 = x2p prf2
1.831 - in
1.832 - mk_proof (PConj(p1,p2))
1.833 - end
1.834 - | x2p (Elem("pconjunct1",[],[prf])) =
1.835 - let
1.836 - val p = x2p prf
1.837 - in
1.838 - mk_proof (PConjunct1 p)
1.839 - end
1.840 - | x2p (Elem("pconjunct2",[],[prf])) =
1.841 - let
1.842 - val p = x2p prf
1.843 - in
1.844 - mk_proof (PConjunct2 p)
1.845 - end
1.846 - | x2p (Elem("pdisj1",[("i",is)],[prf])) =
1.847 - let
1.848 - val p = x2p prf
1.849 - val t = index_to_term is
1.850 - in
1.851 - mk_proof (PDisj1 (p,t))
1.852 - end
1.853 - | x2p (Elem("pdisj2",[("i",is)],[prf])) =
1.854 - let
1.855 - val p = x2p prf
1.856 - val t = index_to_term is
1.857 - in
1.858 - mk_proof (PDisj2 (p,t))
1.859 - end
1.860 - | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) =
1.861 - let
1.862 - val p1 = x2p prf1
1.863 - val p2 = x2p prf2
1.864 - val p3 = x2p prf3
1.865 - in
1.866 - mk_proof (PDisjCases(p1,p2,p3))
1.867 - end
1.868 - | x2p (Elem("pnoti",[],[prf])) =
1.869 - let
1.870 - val p = x2p prf
1.871 - in
1.872 - mk_proof (PNotI p)
1.873 - end
1.874 - | x2p (Elem("pnote",[],[prf])) =
1.875 - let
1.876 - val p = x2p prf
1.877 - in
1.878 - mk_proof (PNotE p)
1.879 - end
1.880 - | x2p (Elem("pcontr",[("i",is)],[prf])) =
1.881 - let
1.882 - val p = x2p prf
1.883 - val t = index_to_term is
1.884 - in
1.885 - mk_proof (PContr (p,t))
1.886 - end
1.887 - | x2p xml = raise ERR "x2p" "Bad proof"
1.888 + fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is))
1.889 + | x2p (Elem("pinstt",[],p::lambda)) =
1.890 + let
1.891 + val p = x2p p
1.892 + val lambda = implode_subst (map xml_to_hol_type lambda)
1.893 + in
1.894 + mk_proof (PInstT(p,lambda))
1.895 + end
1.896 + | x2p (Elem("psubst",[("i",is)],prf::prfs)) =
1.897 + let
1.898 + val tm = index_to_term is
1.899 + val prf = x2p prf
1.900 + val prfs = map x2p prfs
1.901 + in
1.902 + mk_proof (PSubst(prfs,tm,prf))
1.903 + end
1.904 + | x2p (Elem("pabs",[("i",is)],[prf])) =
1.905 + let
1.906 + val p = x2p prf
1.907 + val t = index_to_term is
1.908 + in
1.909 + mk_proof (PAbs (p,t))
1.910 + end
1.911 + | x2p (Elem("pdisch",[("i",is)],[prf])) =
1.912 + let
1.913 + val p = x2p prf
1.914 + val t = index_to_term is
1.915 + in
1.916 + mk_proof (PDisch (p,t))
1.917 + end
1.918 + | x2p (Elem("pmp",[],[prf1,prf2])) =
1.919 + let
1.920 + val p1 = x2p prf1
1.921 + val p2 = x2p prf2
1.922 + in
1.923 + mk_proof (PMp(p1,p2))
1.924 + end
1.925 + | x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is))
1.926 + | x2p (Elem("paxiom",[("n",n),("i",is)],[])) =
1.927 + mk_proof (PAxm(n,index_to_term is))
1.928 + | x2p (Elem("pfact",atts,[])) =
1.929 + let
1.930 + val thyname = get_segment thyname atts
1.931 + val thmname = protect_factname (get_name atts)
1.932 + val p = mk_proof PDisk
1.933 + val _ = set_disk_info_of p thyname thmname
1.934 + in
1.935 + p
1.936 + end
1.937 + | x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) =
1.938 + mk_proof (PDef(seg,protect_constname name,index_to_term is))
1.939 + | x2p (Elem("ptmspec",[("s",seg)],p::names)) =
1.940 + let
1.941 + val names = map (fn Elem("name",[("n",name)],[]) => name
1.942 + | _ => raise ERR "x2p" "Bad proof (ptmspec)") names
1.943 + in
1.944 + mk_proof (PTmSpec(seg,names,x2p p))
1.945 + end
1.946 + | x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) =
1.947 + let
1.948 + val P = xml_to_term xP
1.949 + val t = xml_to_term xt
1.950 + in
1.951 + mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p))
1.952 + end
1.953 + | x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) =
1.954 + mk_proof (PTyDef(seg,protect_tyname name,x2p p))
1.955 + | x2p (xml as Elem("poracle",[],chldr)) =
1.956 + let
1.957 + val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true | _ => false) chldr
1.958 + val ors = map (fn (Elem("oracle",[("n",name)],[])) => name | xml => raise ERR "x2p" "bad oracle") oracles
1.959 + val (c,asl) = case terms of
1.960 + [] => raise ERR "x2p" "Bad oracle description"
1.961 + | (hd::tl) => (hd,tl)
1.962 + val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
1.963 + in
1.964 + mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
1.965 + end
1.966 + | x2p (Elem("pspec",[("i",is)],[prf])) =
1.967 + let
1.968 + val p = x2p prf
1.969 + val tm = index_to_term is
1.970 + in
1.971 + mk_proof (PSpec(p,tm))
1.972 + end
1.973 + | x2p (Elem("pinst",[],p::theta)) =
1.974 + let
1.975 + val p = x2p p
1.976 + val theta = implode_subst (map xml_to_term theta)
1.977 + in
1.978 + mk_proof (PInst(p,theta))
1.979 + end
1.980 + | x2p (Elem("pgen",[("i",is)],[prf])) =
1.981 + let
1.982 + val p = x2p prf
1.983 + val tm = index_to_term is
1.984 + in
1.985 + mk_proof (PGen(p,tm))
1.986 + end
1.987 + | x2p (Elem("pgenabs",[],prf::tms)) =
1.988 + let
1.989 + val p = x2p prf
1.990 + val tml = map xml_to_term tms
1.991 + in
1.992 + mk_proof (PGenAbs(p,NONE,tml))
1.993 + end
1.994 + | x2p (Elem("pgenabs",[("i",is)],prf::tms)) =
1.995 + let
1.996 + val p = x2p prf
1.997 + val tml = map xml_to_term tms
1.998 + in
1.999 + mk_proof (PGenAbs(p,SOME (index_to_term is),tml))
1.1000 + end
1.1001 + | x2p (Elem("pimpas",[],[prf1,prf2])) =
1.1002 + let
1.1003 + val p1 = x2p prf1
1.1004 + val p2 = x2p prf2
1.1005 + in
1.1006 + mk_proof (PImpAS(p1,p2))
1.1007 + end
1.1008 + | x2p (Elem("psym",[],[prf])) =
1.1009 + let
1.1010 + val p = x2p prf
1.1011 + in
1.1012 + mk_proof (PSym p)
1.1013 + end
1.1014 + | x2p (Elem("ptrans",[],[prf1,prf2])) =
1.1015 + let
1.1016 + val p1 = x2p prf1
1.1017 + val p2 = x2p prf2
1.1018 + in
1.1019 + mk_proof (PTrans(p1,p2))
1.1020 + end
1.1021 + | x2p (Elem("pcomb",[],[prf1,prf2])) =
1.1022 + let
1.1023 + val p1 = x2p prf1
1.1024 + val p2 = x2p prf2
1.1025 + in
1.1026 + mk_proof (PComb(p1,p2))
1.1027 + end
1.1028 + | x2p (Elem("peqmp",[],[prf1,prf2])) =
1.1029 + let
1.1030 + val p1 = x2p prf1
1.1031 + val p2 = x2p prf2
1.1032 + in
1.1033 + mk_proof (PEqMp(p1,p2))
1.1034 + end
1.1035 + | x2p (Elem("peqimp",[],[prf])) =
1.1036 + let
1.1037 + val p = x2p prf
1.1038 + in
1.1039 + mk_proof (PEqImp p)
1.1040 + end
1.1041 + | x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) =
1.1042 + let
1.1043 + val p = x2p prf
1.1044 + val ex = index_to_term ise
1.1045 + val w = index_to_term isw
1.1046 + in
1.1047 + mk_proof (PExists(p,ex,w))
1.1048 + end
1.1049 + | x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) =
1.1050 + let
1.1051 + val v = index_to_term is
1.1052 + val p1 = x2p prf1
1.1053 + val p2 = x2p prf2
1.1054 + in
1.1055 + mk_proof (PChoose(v,p1,p2))
1.1056 + end
1.1057 + | x2p (Elem("pconj",[],[prf1,prf2])) =
1.1058 + let
1.1059 + val p1 = x2p prf1
1.1060 + val p2 = x2p prf2
1.1061 + in
1.1062 + mk_proof (PConj(p1,p2))
1.1063 + end
1.1064 + | x2p (Elem("pconjunct1",[],[prf])) =
1.1065 + let
1.1066 + val p = x2p prf
1.1067 + in
1.1068 + mk_proof (PConjunct1 p)
1.1069 + end
1.1070 + | x2p (Elem("pconjunct2",[],[prf])) =
1.1071 + let
1.1072 + val p = x2p prf
1.1073 + in
1.1074 + mk_proof (PConjunct2 p)
1.1075 + end
1.1076 + | x2p (Elem("pdisj1",[("i",is)],[prf])) =
1.1077 + let
1.1078 + val p = x2p prf
1.1079 + val t = index_to_term is
1.1080 + in
1.1081 + mk_proof (PDisj1 (p,t))
1.1082 + end
1.1083 + | x2p (Elem("pdisj2",[("i",is)],[prf])) =
1.1084 + let
1.1085 + val p = x2p prf
1.1086 + val t = index_to_term is
1.1087 + in
1.1088 + mk_proof (PDisj2 (p,t))
1.1089 + end
1.1090 + | x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) =
1.1091 + let
1.1092 + val p1 = x2p prf1
1.1093 + val p2 = x2p prf2
1.1094 + val p3 = x2p prf3
1.1095 + in
1.1096 + mk_proof (PDisjCases(p1,p2,p3))
1.1097 + end
1.1098 + | x2p (Elem("pnoti",[],[prf])) =
1.1099 + let
1.1100 + val p = x2p prf
1.1101 + in
1.1102 + mk_proof (PNotI p)
1.1103 + end
1.1104 + | x2p (Elem("pnote",[],[prf])) =
1.1105 + let
1.1106 + val p = x2p prf
1.1107 + in
1.1108 + mk_proof (PNotE p)
1.1109 + end
1.1110 + | x2p (Elem("pcontr",[("i",is)],[prf])) =
1.1111 + let
1.1112 + val p = x2p prf
1.1113 + val t = index_to_term is
1.1114 + in
1.1115 + mk_proof (PContr (p,t))
1.1116 + end
1.1117 + | x2p xml = raise ERR "x2p" "Bad proof"
1.1118 in
1.1119 - x2p prf
1.1120 + x2p prf
1.1121 end
1.1122
1.1123 fun import_proof_concl thyname thmname thy =
1.1124 let
1.1125 - val is = TextIO.openIn(proof_file_name thyname thmname thy)
1.1126 - val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
1.1127 - val _ = TextIO.closeIn is
1.1128 + val is = TextIO.openIn(proof_file_name thyname thmname thy)
1.1129 + val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
1.1130 + val _ = TextIO.closeIn is
1.1131 in
1.1132 - case proof_xml of
1.1133 - Elem("proof",[],xtypes::xterms::prf::rest) =>
1.1134 - let
1.1135 - val types = TypeNet.input_types thyname xtypes
1.1136 - val terms = TermNet.input_terms thyname types xterms
1.1137 + case proof_xml of
1.1138 + Elem("proof",[],xtypes::xterms::prf::rest) =>
1.1139 + let
1.1140 + val types = TypeNet.input_types thyname xtypes
1.1141 + val terms = TermNet.input_terms thyname types xterms
1.1142 fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm
1.1143 - in
1.1144 - case rest of
1.1145 - [] => NONE
1.1146 - | [xtm] => SOME (f xtm)
1.1147 - | _ => raise ERR "import_proof" "Bad argument list"
1.1148 - end
1.1149 - | _ => raise ERR "import_proof" "Bad proof"
1.1150 + in
1.1151 + case rest of
1.1152 + [] => NONE
1.1153 + | [xtm] => SOME (f xtm)
1.1154 + | _ => raise ERR "import_proof" "Bad argument list"
1.1155 + end
1.1156 + | _ => raise ERR "import_proof" "Bad proof"
1.1157 end
1.1158
1.1159 fun import_proof thyname thmname thy =
1.1160 let
1.1161 - val is = TextIO.openIn(proof_file_name thyname thmname thy)
1.1162 - val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
1.1163 - val _ = TextIO.closeIn is
1.1164 + val is = TextIO.openIn(proof_file_name thyname thmname thy)
1.1165 + val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
1.1166 + val _ = TextIO.closeIn is
1.1167 in
1.1168 - case proof_xml of
1.1169 - Elem("proof",[],xtypes::xterms::prf::rest) =>
1.1170 - let
1.1171 - val types = TypeNet.input_types thyname xtypes
1.1172 - val terms = TermNet.input_terms thyname types xterms
1.1173 - in
1.1174 - (case rest of
1.1175 - [] => NONE
1.1176 - | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm)
1.1177 - | _ => raise ERR "import_proof" "Bad argument list",
1.1178 - xml_to_proof thyname types terms prf)
1.1179 - end
1.1180 - | _ => raise ERR "import_proof" "Bad proof"
1.1181 + case proof_xml of
1.1182 + Elem("proof",[],xtypes::xterms::prf::rest) =>
1.1183 + let
1.1184 + val types = TypeNet.input_types thyname xtypes
1.1185 + val terms = TermNet.input_terms thyname types xterms
1.1186 + in
1.1187 + (case rest of
1.1188 + [] => NONE
1.1189 + | [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm)
1.1190 + | _ => raise ERR "import_proof" "Bad argument list",
1.1191 + xml_to_proof thyname types terms prf)
1.1192 + end
1.1193 + | _ => raise ERR "import_proof" "Bad proof"
1.1194 end
1.1195
1.1196 fun uniq_compose m th i st =
1.1197 let
1.1198 - val res = bicompose false (false,th,m) i st
1.1199 + val res = bicompose false (false,th,m) i st
1.1200 in
1.1201 - case Seq.pull res of
1.1202 - SOME (th,rest) => (case Seq.pull rest of
1.1203 - SOME _ => raise ERR "uniq_compose" "Not unique!"
1.1204 - | NONE => th)
1.1205 - | NONE => raise ERR "uniq_compose" "No result"
1.1206 + case Seq.pull res of
1.1207 + SOME (th,rest) => (case Seq.pull rest of
1.1208 + SOME _ => raise ERR "uniq_compose" "Not unique!"
1.1209 + | NONE => th)
1.1210 + | NONE => raise ERR "uniq_compose" "No result"
1.1211 end
1.1212
1.1213 val reflexivity_thm = thm "refl"
1.1214 @@ -1033,10 +1035,10 @@
1.1215
1.1216 fun beta_eta_thm th =
1.1217 let
1.1218 - val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th
1.1219 - val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1
1.1220 + val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th
1.1221 + val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1
1.1222 in
1.1223 - th2
1.1224 + th2
1.1225 end
1.1226
1.1227 fun implies_elim_all th =
1.1228 @@ -1049,38 +1051,38 @@
1.1229
1.1230 fun mk_GEN v th sg =
1.1231 let
1.1232 - val c = HOLogic.dest_Trueprop (concl_of th)
1.1233 - val cv = cterm_of sg v
1.1234 - val lc = Term.lambda v c
1.1235 - val clc = Thm.cterm_of sg lc
1.1236 - val cvty = ctyp_of_term cv
1.1237 - val th1 = implies_elim_all th
1.1238 - val th2 = beta_eta_thm (forall_intr cv th1)
1.1239 - val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
1.1240 - val c = prop_of th3
1.1241 - val vname = fst(dest_Free v)
1.1242 - val (cold,cnew) = case c of
1.1243 - tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
1.1244 - (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
1.1245 - | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
1.1246 - | _ => raise ERR "mk_GEN" "Unknown conclusion"
1.1247 - val th4 = Thm.rename_boundvars cold cnew th3
1.1248 - val res = implies_intr_hyps th4
1.1249 + val c = HOLogic.dest_Trueprop (concl_of th)
1.1250 + val cv = cterm_of sg v
1.1251 + val lc = Term.lambda v c
1.1252 + val clc = Thm.cterm_of sg lc
1.1253 + val cvty = ctyp_of_term cv
1.1254 + val th1 = implies_elim_all th
1.1255 + val th2 = beta_eta_thm (forall_intr cv th1)
1.1256 + val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm))
1.1257 + val c = prop_of th3
1.1258 + val vname = fst(dest_Free v)
1.1259 + val (cold,cnew) = case c of
1.1260 + tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) =>
1.1261 + (Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0))
1.1262 + | tpc $ (Const("All",allT) $ rest) => (tpc,tpc)
1.1263 + | _ => raise ERR "mk_GEN" "Unknown conclusion"
1.1264 + val th4 = Thm.rename_boundvars cold cnew th3
1.1265 + val res = implies_intr_hyps th4
1.1266 in
1.1267 - res
1.1268 + res
1.1269 end
1.1270
1.1271 val permute_prems = Thm.permute_prems
1.1272
1.1273 fun rearrange sg tm th =
1.1274 let
1.1275 - val tm' = Envir.beta_eta_contract tm
1.1276 - fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
1.1277 - | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
1.1278 - then permute_prems n 1 th
1.1279 - else find ps (n+1)
1.1280 + val tm' = Envir.beta_eta_contract tm
1.1281 + fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th)
1.1282 + | find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p)
1.1283 + then permute_prems n 1 th
1.1284 + else find ps (n+1)
1.1285 in
1.1286 - find (prems_of th) 0
1.1287 + find (prems_of th) 0
1.1288 end
1.1289
1.1290 fun zip (x::xs) (y::ys) = (x,y)::(zip xs ys)
1.1291 @@ -1093,17 +1095,17 @@
1.1292
1.1293 val collect_vars =
1.1294 let
1.1295 - fun F vars (Bound _) = vars
1.1296 - | F vars (tm as Free _) =
1.1297 - if tm mem vars
1.1298 - then vars
1.1299 - else (tm::vars)
1.1300 - | F vars (Const _) = vars
1.1301 - | F vars (tm1 $ tm2) = F (F vars tm1) tm2
1.1302 - | F vars (Abs(_,_,body)) = F vars body
1.1303 - | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found"
1.1304 + fun F vars (Bound _) = vars
1.1305 + | F vars (tm as Free _) =
1.1306 + if tm mem vars
1.1307 + then vars
1.1308 + else (tm::vars)
1.1309 + | F vars (Const _) = vars
1.1310 + | F vars (tm1 $ tm2) = F (F vars tm1) tm2
1.1311 + | F vars (Abs(_,_,body)) = F vars body
1.1312 + | F vars (Var _) = raise ERR "collect_vars" "Schematic variable found"
1.1313 in
1.1314 - F []
1.1315 + F []
1.1316 end
1.1317
1.1318 (* Code for disambiguating variablenames (wrt. types) *)
1.1319 @@ -1122,9 +1124,9 @@
1.1320 fun has_ren (HOLThm _) = false
1.1321
1.1322 fun prinfo {vars,rens} = (writeln "Vars:";
1.1323 - app prin vars;
1.1324 - writeln "Renaming:";
1.1325 - app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens)
1.1326 + app prin vars;
1.1327 + writeln "Renaming:";
1.1328 + app (fn(x,y)=>(prin x; writeln " -->"; prin y)) rens)
1.1329
1.1330 fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm)
1.1331
1.1332 @@ -1202,119 +1204,119 @@
1.1333
1.1334 fun get_hol4_thm thyname thmname thy =
1.1335 case get_hol4_theorem thyname thmname thy of
1.1336 - SOME hth => SOME (HOLThm hth)
1.1337 + SOME hth => SOME (HOLThm hth)
1.1338 | NONE =>
1.1339 - let
1.1340 - val pending = HOL4Pending.get thy
1.1341 - in
1.1342 - case StringPair.lookup pending (thyname,thmname) of
1.1343 - SOME hth => SOME (HOLThm hth)
1.1344 - | NONE => NONE
1.1345 - end
1.1346 + let
1.1347 + val pending = HOL4Pending.get thy
1.1348 + in
1.1349 + case StringPair.lookup pending (thyname,thmname) of
1.1350 + SOME hth => SOME (HOLThm hth)
1.1351 + | NONE => NONE
1.1352 + end
1.1353
1.1354 fun non_trivial_term_consts tm =
1.1355 List.filter (fn c => not (c = "Trueprop" orelse
1.1356 - c = "All" orelse
1.1357 - c = "op -->" orelse
1.1358 - c = "op &" orelse
1.1359 - c = "op =")) (Term.term_consts tm)
1.1360 + c = "All" orelse
1.1361 + c = "op -->" orelse
1.1362 + c = "op &" orelse
1.1363 + c = "op =")) (Term.term_consts tm)
1.1364
1.1365 fun match_consts t (* th *) =
1.1366 let
1.1367 - fun add_consts (Const (c, _), cs) =
1.1368 - (case c of
1.1369 - "op =" => Library.insert (op =) "==" cs
1.1370 - | "op -->" => Library.insert (op =) "==>" cs
1.1371 - | "All" => cs
1.1372 - | "all" => cs
1.1373 - | "op &" => cs
1.1374 - | "Trueprop" => cs
1.1375 - | _ => Library.insert (op =) c cs)
1.1376 - | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
1.1377 - | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
1.1378 - | add_consts (_, cs) = cs
1.1379 - val t_consts = add_consts(t,[])
1.1380 + fun add_consts (Const (c, _), cs) =
1.1381 + (case c of
1.1382 + "op =" => Library.insert (op =) "==" cs
1.1383 + | "op -->" => Library.insert (op =) "==>" cs
1.1384 + | "All" => cs
1.1385 + | "all" => cs
1.1386 + | "op &" => cs
1.1387 + | "Trueprop" => cs
1.1388 + | _ => Library.insert (op =) c cs)
1.1389 + | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
1.1390 + | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
1.1391 + | add_consts (_, cs) = cs
1.1392 + val t_consts = add_consts(t,[])
1.1393 in
1.1394 - fn th => eq_set(t_consts,add_consts(prop_of th,[]))
1.1395 + fn th => eq_set(t_consts,add_consts(prop_of th,[]))
1.1396 end
1.1397
1.1398 fun split_name str =
1.1399 let
1.1400 - val sub = Substring.full str
1.1401 - val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
1.1402 - val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
1.1403 + val sub = Substring.full str
1.1404 + val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
1.1405 + val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
1.1406 in
1.1407 - if not (idx = "") andalso u = "_"
1.1408 - then SOME (newstr,valOf(Int.fromString idx))
1.1409 - else NONE
1.1410 + if not (idx = "") andalso u = "_"
1.1411 + then SOME (newstr,valOf(Int.fromString idx))
1.1412 + else NONE
1.1413 end
1.1414 handle _ => NONE
1.1415
1.1416 fun rewrite_hol4_term t thy =
1.1417 let
1.1418 - val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
1.1419 - val hol4ss = Simplifier.theory_context thy empty_ss
1.1420 + val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
1.1421 + val hol4ss = Simplifier.theory_context thy empty_ss
1.1422 setmksimps single addsimps hol4rews1
1.1423 in
1.1424 - Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
1.1425 + Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
1.1426 end
1.1427
1.1428 fun get_isabelle_thm thyname thmname hol4conc thy =
1.1429 let
1.1430 - val (info,hol4conc') = disamb_term hol4conc
1.1431 - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
1.1432 - val isaconc =
1.1433 - case concl_of i2h_conc of
1.1434 - Const("==",_) $ lhs $ _ => lhs
1.1435 - | _ => error "get_isabelle_thm" "Bad rewrite rule"
1.1436 - val _ = (message "Original conclusion:";
1.1437 - if_debug prin hol4conc';
1.1438 - message "Modified conclusion:";
1.1439 - if_debug prin isaconc)
1.1440 + val (info,hol4conc') = disamb_term hol4conc
1.1441 + val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
1.1442 + val isaconc =
1.1443 + case concl_of i2h_conc of
1.1444 + Const("==",_) $ lhs $ _ => lhs
1.1445 + | _ => error "get_isabelle_thm" "Bad rewrite rule"
1.1446 + val _ = (message "Original conclusion:";
1.1447 + if_debug prin hol4conc';
1.1448 + message "Modified conclusion:";
1.1449 + if_debug prin isaconc)
1.1450
1.1451 - fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
1.1452 + fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th)
1.1453 in
1.1454 - case get_hol4_mapping thyname thmname thy of
1.1455 - SOME (SOME thmname) =>
1.1456 - let
1.1457 - val th1 = (SOME (PureThy.get_thm thy thmname)
1.1458 - handle ERROR _ =>
1.1459 - (case split_name thmname of
1.1460 - SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
1.1461 - handle _ => NONE)
1.1462 - | NONE => NONE))
1.1463 - in
1.1464 - case th1 of
1.1465 - SOME th2 =>
1.1466 - (case Shuffler.set_prop thy isaconc [(thmname,th2)] of
1.1467 - SOME (_,th) => (message "YES";(thy, SOME (mk_res th)))
1.1468 - | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping"))
1.1469 - | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping")
1.1470 - end
1.1471 - | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
1.1472 - | NONE =>
1.1473 - let
1.1474 - val _ = (message "Looking for conclusion:";
1.1475 - if_debug prin isaconc)
1.1476 - val cs = non_trivial_term_consts isaconc
1.1477 - val _ = (message "Looking for consts:";
1.1478 - message (commas cs))
1.1479 - val pot_thms = Shuffler.find_potential thy isaconc
1.1480 - val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
1.1481 - in
1.1482 - case Shuffler.set_prop thy isaconc pot_thms of
1.1483 - SOME (isaname,th) =>
1.1484 - let
1.1485 - val hth as HOLThm args = mk_res th
1.1486 - val thy' = thy |> add_hol4_theorem thyname thmname args
1.1487 - |> add_hol4_mapping thyname thmname isaname
1.1488 - val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
1.1489 - val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
1.1490 - in
1.1491 - (thy',SOME hth)
1.1492 - end
1.1493 - | NONE => (thy,NONE)
1.1494 - end
1.1495 + case get_hol4_mapping thyname thmname thy of
1.1496 + SOME (SOME thmname) =>
1.1497 + let
1.1498 + val th1 = (SOME (PureThy.get_thm thy thmname)
1.1499 + handle ERROR _ =>
1.1500 + (case split_name thmname of
1.1501 + SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
1.1502 + handle _ => NONE)
1.1503 + | NONE => NONE))
1.1504 + in
1.1505 + case th1 of
1.1506 + SOME th2 =>
1.1507 + (case Shuffler.set_prop thy isaconc [(thmname,th2)] of
1.1508 + SOME (_,th) => (message "YES";(thy, SOME (mk_res th)))
1.1509 + | NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping"))
1.1510 + | NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping")
1.1511 + end
1.1512 + | SOME NONE => error ("Trying to access ignored theorem " ^ thmname)
1.1513 + | NONE =>
1.1514 + let
1.1515 + val _ = (message "Looking for conclusion:";
1.1516 + if_debug prin isaconc)
1.1517 + val cs = non_trivial_term_consts isaconc
1.1518 + val _ = (message "Looking for consts:";
1.1519 + message (commas cs))
1.1520 + val pot_thms = Shuffler.find_potential thy isaconc
1.1521 + val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems")
1.1522 + in
1.1523 + case Shuffler.set_prop thy isaconc pot_thms of
1.1524 + SOME (isaname,th) =>
1.1525 + let
1.1526 + val hth as HOLThm args = mk_res th
1.1527 + val thy' = thy |> add_hol4_theorem thyname thmname args
1.1528 + |> add_hol4_mapping thyname thmname isaname
1.1529 + val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
1.1530 + val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
1.1531 + in
1.1532 + (thy',SOME hth)
1.1533 + end
1.1534 + | NONE => (thy,NONE)
1.1535 + end
1.1536 end
1.1537 handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE))
1.1538
1.1539 @@ -1323,658 +1325,658 @@
1.1540 val (a, b) = get_isabelle_thm thyname thmname hol4conc thy
1.1541 fun warn () =
1.1542 let
1.1543 - val (info,hol4conc') = disamb_term hol4conc
1.1544 - val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
1.1545 - in
1.1546 - case concl_of i2h_conc of
1.1547 - Const("==",_) $ lhs $ _ =>
1.1548 - (warning ("Failed lookup of theorem '"^thmname^"':");
1.1549 - writeln "Original conclusion:";
1.1550 - prin hol4conc';
1.1551 - writeln "Modified conclusion:";
1.1552 - prin lhs)
1.1553 - | _ => ()
1.1554 - end
1.1555 + val (info,hol4conc') = disamb_term hol4conc
1.1556 + val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy)
1.1557 + in
1.1558 + case concl_of i2h_conc of
1.1559 + Const("==",_) $ lhs $ _ =>
1.1560 + (warning ("Failed lookup of theorem '"^thmname^"':");
1.1561 + writeln "Original conclusion:";
1.1562 + prin hol4conc';
1.1563 + writeln "Modified conclusion:";
1.1564 + prin lhs)
1.1565 + | _ => ()
1.1566 + end
1.1567 in
1.1568 case b of
1.1569 - NONE => (warn () handle _ => (); (a,b))
1.1570 - | _ => (a, b)
1.1571 + NONE => (warn () handle _ => (); (a,b))
1.1572 + | _ => (a, b)
1.1573 end
1.1574
1.1575 fun get_thm thyname thmname thy =
1.1576 case get_hol4_thm thyname thmname thy of
1.1577 - SOME hth => (thy,SOME hth)
1.1578 + SOME hth => (thy,SOME hth)
1.1579 | NONE => ((case import_proof_concl thyname thmname thy of
1.1580 - SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
1.1581 - | NONE => (message "No conclusion"; (thy,NONE)))
1.1582 - handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
1.1583 - | e as PK _ => (message "PK exception"; (thy,NONE)))
1.1584 + SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy
1.1585 + | NONE => (message "No conclusion"; (thy,NONE)))
1.1586 + handle e as IO.Io _ => (message "IO exception"; (thy,NONE))
1.1587 + | e as PK _ => (message "PK exception"; (thy,NONE)))
1.1588
1.1589 fun rename_const thyname thy name =
1.1590 case get_hol4_const_renaming thyname name thy of
1.1591 - SOME cname => cname
1.1592 + SOME cname => cname
1.1593 | NONE => name
1.1594
1.1595 fun get_def thyname constname rhs thy =
1.1596 let
1.1597 - val constname = rename_const thyname thy constname
1.1598 - val (thmname,thy') = get_defname thyname constname thy
1.1599 - val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname)
1.1600 + val constname = rename_const thyname thy constname
1.1601 + val (thmname,thy') = get_defname thyname constname thy
1.1602 + val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname)
1.1603 in
1.1604 - get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
1.1605 + get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy'
1.1606 end
1.1607
1.1608 fun get_axiom thyname axname thy =
1.1609 case get_thm thyname axname thy of
1.1610 - arg as (_,SOME _) => arg
1.1611 + arg as (_,SOME _) => arg
1.1612 | _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")")
1.1613
1.1614 fun intern_store_thm gen_output thyname thmname hth thy =
1.1615 let
1.1616 - val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
1.1617 - val rew = rewrite_hol4_term (concl_of th) thy
1.1618 - val th = equal_elim rew th
1.1619 - val thy' = add_hol4_pending thyname thmname args thy
1.1620 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.1621 + val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth
1.1622 + val rew = rewrite_hol4_term (concl_of th) thy
1.1623 + val th = equal_elim rew th
1.1624 + val thy' = add_hol4_pending thyname thmname args thy
1.1625 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.1626 val th = disambiguate_frees th
1.1627 - val thy2 = if gen_output
1.1628 - then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
1.1629 + val thy2 = if gen_output
1.1630 + then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^
1.1631 (smart_string_of_thm th) ^ "\n by (import " ^
1.1632 thyname ^ " " ^ (quotename thmname) ^ ")") thy'
1.1633 - else thy'
1.1634 + else thy'
1.1635 in
1.1636 - (thy2,hth')
1.1637 + (thy2,hth')
1.1638 end
1.1639
1.1640 val store_thm = intern_store_thm true
1.1641
1.1642 fun mk_REFL ctm =
1.1643 let
1.1644 - val cty = Thm.ctyp_of_term ctm
1.1645 + val cty = Thm.ctyp_of_term ctm
1.1646 in
1.1647 - Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm
1.1648 + Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm
1.1649 end
1.1650
1.1651 fun REFL tm thy =
1.1652 let
1.1653 - val _ = message "REFL:"
1.1654 - val (info,tm') = disamb_term tm
1.1655 - val ctm = Thm.cterm_of thy tm'
1.1656 - val res = HOLThm(rens_of info,mk_REFL ctm)
1.1657 - val _ = if_debug pth res
1.1658 + val _ = message "REFL:"
1.1659 + val (info,tm') = disamb_term tm
1.1660 + val ctm = Thm.cterm_of thy tm'
1.1661 + val res = HOLThm(rens_of info,mk_REFL ctm)
1.1662 + val _ = if_debug pth res
1.1663 in
1.1664 - (thy,res)
1.1665 + (thy,res)
1.1666 end
1.1667
1.1668 fun ASSUME tm thy =
1.1669 let
1.1670 - val _ = message "ASSUME:"
1.1671 - val (info,tm') = disamb_term tm
1.1672 - val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm')
1.1673 - val th = Thm.trivial ctm
1.1674 - val res = HOLThm(rens_of info,th)
1.1675 - val _ = if_debug pth res
1.1676 + val _ = message "ASSUME:"
1.1677 + val (info,tm') = disamb_term tm
1.1678 + val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm')
1.1679 + val th = Thm.trivial ctm
1.1680 + val res = HOLThm(rens_of info,th)
1.1681 + val _ = if_debug pth res
1.1682 in
1.1683 - (thy,res)
1.1684 + (thy,res)
1.1685 end
1.1686
1.1687 fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy =
1.1688 let
1.1689 - val _ = message "INST_TYPE:"
1.1690 - val _ = if_debug pth hth
1.1691 - val tys_before = add_term_tfrees (prop_of th,[])
1.1692 - val th1 = Thm.varifyT th
1.1693 - val tys_after = add_term_tvars (prop_of th1,[])
1.1694 - val tyinst = map (fn (bef, iS) =>
1.1695 - (case try (Lib.assoc (TFree bef)) lambda of
1.1696 - SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
1.1697 - | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
1.1698 - ))
1.1699 - (zip tys_before tys_after)
1.1700 - val res = Drule.instantiate (tyinst,[]) th1
1.1701 - val hth = HOLThm([],res)
1.1702 - val res = norm_hthm thy hth
1.1703 - val _ = message "RESULT:"
1.1704 - val _ = if_debug pth res
1.1705 + val _ = message "INST_TYPE:"
1.1706 + val _ = if_debug pth hth
1.1707 + val tys_before = add_term_tfrees (prop_of th,[])
1.1708 + val th1 = Thm.varifyT th
1.1709 + val tys_after = add_term_tvars (prop_of th1,[])
1.1710 + val tyinst = map (fn (bef, iS) =>
1.1711 + (case try (Lib.assoc (TFree bef)) lambda of
1.1712 + SOME ty => (ctyp_of thy (TVar iS), ctyp_of thy ty)
1.1713 + | NONE => (ctyp_of thy (TVar iS), ctyp_of thy (TFree bef))
1.1714 + ))
1.1715 + (zip tys_before tys_after)
1.1716 + val res = Drule.instantiate (tyinst,[]) th1
1.1717 + val hth = HOLThm([],res)
1.1718 + val res = norm_hthm thy hth
1.1719 + val _ = message "RESULT:"
1.1720 + val _ = if_debug pth res
1.1721 in
1.1722 - (thy,res)
1.1723 + (thy,res)
1.1724 end
1.1725
1.1726 fun INST sigma hth thy =
1.1727 let
1.1728 - val _ = message "INST:"
1.1729 - val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
1.1730 - val _ = if_debug pth hth
1.1731 - val (sdom,srng) = ListPair.unzip (rev sigma)
1.1732 - val th = hthm2thm hth
1.1733 - val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th
1.1734 - val res = HOLThm([],th1)
1.1735 - val _ = message "RESULT:"
1.1736 - val _ = if_debug pth res
1.1737 + val _ = message "INST:"
1.1738 + val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
1.1739 + val _ = if_debug pth hth
1.1740 + val (sdom,srng) = ListPair.unzip (rev sigma)
1.1741 + val th = hthm2thm hth
1.1742 + val th1 = mk_INST (map (cterm_of thy) sdom) (map (cterm_of thy) srng) th
1.1743 + val res = HOLThm([],th1)
1.1744 + val _ = message "RESULT:"
1.1745 + val _ = if_debug pth res
1.1746 in
1.1747 - (thy,res)
1.1748 + (thy,res)
1.1749 end
1.1750
1.1751 fun EQ_IMP_RULE (hth as HOLThm(rens,th)) thy =
1.1752 let
1.1753 - val _ = message "EQ_IMP_RULE:"
1.1754 - val _ = if_debug pth hth
1.1755 - val res = HOLThm(rens,th RS eqimp_thm)
1.1756 - val _ = message "RESULT:"
1.1757 - val _ = if_debug pth res
1.1758 + val _ = message "EQ_IMP_RULE:"
1.1759 + val _ = if_debug pth hth
1.1760 + val res = HOLThm(rens,th RS eqimp_thm)
1.1761 + val _ = message "RESULT:"
1.1762 + val _ = if_debug pth res
1.1763 in
1.1764 - (thy,res)
1.1765 + (thy,res)
1.1766 end
1.1767
1.1768 fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm
1.1769
1.1770 fun EQ_MP hth1 hth2 thy =
1.1771 let
1.1772 - val _ = message "EQ_MP:"
1.1773 - val _ = if_debug pth hth1
1.1774 - val _ = if_debug pth hth2
1.1775 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.1776 - val res = HOLThm(rens_of info,mk_EQ_MP th1 th2)
1.1777 - val _ = message "RESULT:"
1.1778 - val _ = if_debug pth res
1.1779 + val _ = message "EQ_MP:"
1.1780 + val _ = if_debug pth hth1
1.1781 + val _ = if_debug pth hth2
1.1782 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.1783 + val res = HOLThm(rens_of info,mk_EQ_MP th1 th2)
1.1784 + val _ = message "RESULT:"
1.1785 + val _ = if_debug pth res
1.1786 in
1.1787 - (thy,res)
1.1788 + (thy,res)
1.1789 end
1.1790
1.1791 fun mk_COMB th1 th2 thy =
1.1792 let
1.1793 - val (f,g) = case concl_of th1 of
1.1794 - _ $ (Const("op =",_) $ f $ g) => (f,g)
1.1795 - | _ => raise ERR "mk_COMB" "First theorem not an equality"
1.1796 - val (x,y) = case concl_of th2 of
1.1797 - _ $ (Const("op =",_) $ x $ y) => (x,y)
1.1798 - | _ => raise ERR "mk_COMB" "Second theorem not an equality"
1.1799 - val fty = type_of f
1.1800 - val (fd,fr) = dom_rng fty
1.1801 - val comb_thm' = Drule.instantiate'
1.1802 - [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
1.1803 - [SOME (cterm_of thy f),SOME (cterm_of thy g),
1.1804 - SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm
1.1805 + val (f,g) = case concl_of th1 of
1.1806 + _ $ (Const("op =",_) $ f $ g) => (f,g)
1.1807 + | _ => raise ERR "mk_COMB" "First theorem not an equality"
1.1808 + val (x,y) = case concl_of th2 of
1.1809 + _ $ (Const("op =",_) $ x $ y) => (x,y)
1.1810 + | _ => raise ERR "mk_COMB" "Second theorem not an equality"
1.1811 + val fty = type_of f
1.1812 + val (fd,fr) = dom_rng fty
1.1813 + val comb_thm' = Drule.instantiate'
1.1814 + [SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
1.1815 + [SOME (cterm_of thy f),SOME (cterm_of thy g),
1.1816 + SOME (cterm_of thy x),SOME (cterm_of thy y)] comb_thm
1.1817 in
1.1818 - [th1,th2] MRS comb_thm'
1.1819 + [th1,th2] MRS comb_thm'
1.1820 end
1.1821
1.1822 fun SUBST rews ctxt hth thy =
1.1823 let
1.1824 - val _ = message "SUBST:"
1.1825 - val _ = if_debug (app pth) rews
1.1826 - val _ = if_debug prin ctxt
1.1827 - val _ = if_debug pth hth
1.1828 - val (info,th) = disamb_thm hth
1.1829 - val (info1,ctxt') = disamb_term_from info ctxt
1.1830 - val (info2,rews') = disamb_thms_from info1 rews
1.1831 + val _ = message "SUBST:"
1.1832 + val _ = if_debug (app pth) rews
1.1833 + val _ = if_debug prin ctxt
1.1834 + val _ = if_debug pth hth
1.1835 + val (info,th) = disamb_thm hth
1.1836 + val (info1,ctxt') = disamb_term_from info ctxt
1.1837 + val (info2,rews') = disamb_thms_from info1 rews
1.1838
1.1839 - val cctxt = cterm_of thy ctxt'
1.1840 - fun subst th [] = th
1.1841 - | subst th (rew::rews) = subst (mk_COMB th rew thy) rews
1.1842 - val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th)
1.1843 - val _ = message "RESULT:"
1.1844 - val _ = if_debug pth res
1.1845 + val cctxt = cterm_of thy ctxt'
1.1846 + fun subst th [] = th
1.1847 + | subst th (rew::rews) = subst (mk_COMB th rew thy) rews
1.1848 + val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th)
1.1849 + val _ = message "RESULT:"
1.1850 + val _ = if_debug pth res
1.1851 in
1.1852 - (thy,res)
1.1853 + (thy,res)
1.1854 end
1.1855
1.1856 fun DISJ_CASES hth hth1 hth2 thy =
1.1857 let
1.1858 - val _ = message "DISJ_CASES:"
1.1859 - val _ = if_debug (app pth) [hth,hth1,hth2]
1.1860 - val (info,th) = disamb_thm hth
1.1861 - val (info1,th1) = disamb_thm_from info hth1
1.1862 - val (info2,th2) = disamb_thm_from info1 hth2
1.1863 - val th1 = norm_hyps th1
1.1864 - val th2 = norm_hyps th2
1.1865 - val (l,r) = case concl_of th of
1.1866 - _ $ (Const("op |",_) $ l $ r) => (l,r)
1.1867 - | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
1.1868 - val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
1.1869 - val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
1.1870 - val res1 = th RS disj_cases_thm
1.1871 - val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1
1.1872 - val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2
1.1873 - val res = HOLThm(rens_of info2,res3)
1.1874 - val _ = message "RESULT:"
1.1875 - val _ = if_debug pth res
1.1876 + val _ = message "DISJ_CASES:"
1.1877 + val _ = if_debug (app pth) [hth,hth1,hth2]
1.1878 + val (info,th) = disamb_thm hth
1.1879 + val (info1,th1) = disamb_thm_from info hth1
1.1880 + val (info2,th2) = disamb_thm_from info1 hth2
1.1881 + val th1 = norm_hyps th1
1.1882 + val th2 = norm_hyps th2
1.1883 + val (l,r) = case concl_of th of
1.1884 + _ $ (Const("op |",_) $ l $ r) => (l,r)
1.1885 + | _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction"
1.1886 + val th1' = rearrange thy (HOLogic.mk_Trueprop l) th1
1.1887 + val th2' = rearrange thy (HOLogic.mk_Trueprop r) th2
1.1888 + val res1 = th RS disj_cases_thm
1.1889 + val res2 = uniq_compose ((nprems_of th1')-1) th1' ((nprems_of th)+1) res1
1.1890 + val res3 = uniq_compose ((nprems_of th2')-1) th2' (nprems_of res2) res2
1.1891 + val res = HOLThm(rens_of info2,res3)
1.1892 + val _ = message "RESULT:"
1.1893 + val _ = if_debug pth res
1.1894 in
1.1895 - (thy,res)
1.1896 + (thy,res)
1.1897 end
1.1898
1.1899 fun DISJ1 hth tm thy =
1.1900 let
1.1901 - val _ = message "DISJ1:"
1.1902 - val _ = if_debug pth hth
1.1903 - val _ = if_debug prin tm
1.1904 - val (info,th) = disamb_thm hth
1.1905 - val (info',tm') = disamb_term_from info tm
1.1906 - val ct = Thm.cterm_of thy tm'
1.1907 - val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm
1.1908 - val res = HOLThm(rens_of info',th RS disj1_thm')
1.1909 - val _ = message "RESULT:"
1.1910 - val _ = if_debug pth res
1.1911 + val _ = message "DISJ1:"
1.1912 + val _ = if_debug pth hth
1.1913 + val _ = if_debug prin tm
1.1914 + val (info,th) = disamb_thm hth
1.1915 + val (info',tm') = disamb_term_from info tm
1.1916 + val ct = Thm.cterm_of thy tm'
1.1917 + val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm
1.1918 + val res = HOLThm(rens_of info',th RS disj1_thm')
1.1919 + val _ = message "RESULT:"
1.1920 + val _ = if_debug pth res
1.1921 in
1.1922 - (thy,res)
1.1923 + (thy,res)
1.1924 end
1.1925
1.1926 fun DISJ2 tm hth thy =
1.1927 let
1.1928 - val _ = message "DISJ1:"
1.1929 - val _ = if_debug prin tm
1.1930 - val _ = if_debug pth hth
1.1931 - val (info,th) = disamb_thm hth
1.1932 - val (info',tm') = disamb_term_from info tm
1.1933 - val ct = Thm.cterm_of thy tm'
1.1934 - val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm
1.1935 - val res = HOLThm(rens_of info',th RS disj2_thm')
1.1936 - val _ = message "RESULT:"
1.1937 - val _ = if_debug pth res
1.1938 + val _ = message "DISJ1:"
1.1939 + val _ = if_debug prin tm
1.1940 + val _ = if_debug pth hth
1.1941 + val (info,th) = disamb_thm hth
1.1942 + val (info',tm') = disamb_term_from info tm
1.1943 + val ct = Thm.cterm_of thy tm'
1.1944 + val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm
1.1945 + val res = HOLThm(rens_of info',th RS disj2_thm')
1.1946 + val _ = message "RESULT:"
1.1947 + val _ = if_debug pth res
1.1948 in
1.1949 - (thy,res)
1.1950 + (thy,res)
1.1951 end
1.1952
1.1953 fun IMP_ANTISYM hth1 hth2 thy =
1.1954 let
1.1955 - val _ = message "IMP_ANTISYM:"
1.1956 - val _ = if_debug pth hth1
1.1957 - val _ = if_debug pth hth2
1.1958 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.1959 - val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm
1.1960 - val res = HOLThm(rens_of info,th)
1.1961 - val _ = message "RESULT:"
1.1962 - val _ = if_debug pth res
1.1963 + val _ = message "IMP_ANTISYM:"
1.1964 + val _ = if_debug pth hth1
1.1965 + val _ = if_debug pth hth2
1.1966 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.1967 + val th = [beta_eta_thm th1,beta_eta_thm th2] MRS imp_antisym_thm
1.1968 + val res = HOLThm(rens_of info,th)
1.1969 + val _ = message "RESULT:"
1.1970 + val _ = if_debug pth res
1.1971 in
1.1972 - (thy,res)
1.1973 + (thy,res)
1.1974 end
1.1975
1.1976 fun SYM (hth as HOLThm(rens,th)) thy =
1.1977 let
1.1978 - val _ = message "SYM:"
1.1979 - val _ = if_debug pth hth
1.1980 - val th = th RS symmetry_thm
1.1981 - val res = HOLThm(rens,th)
1.1982 - val _ = message "RESULT:"
1.1983 - val _ = if_debug pth res
1.1984 + val _ = message "SYM:"
1.1985 + val _ = if_debug pth hth
1.1986 + val th = th RS symmetry_thm
1.1987 + val res = HOLThm(rens,th)
1.1988 + val _ = message "RESULT:"
1.1989 + val _ = if_debug pth res
1.1990 in
1.1991 - (thy,res)
1.1992 + (thy,res)
1.1993 end
1.1994
1.1995 fun MP hth1 hth2 thy =
1.1996 let
1.1997 - val _ = message "MP:"
1.1998 - val _ = if_debug pth hth1
1.1999 - val _ = if_debug pth hth2
1.2000 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2001 - val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm
1.2002 - val res = HOLThm(rens_of info,th)
1.2003 - val _ = message "RESULT:"
1.2004 - val _ = if_debug pth res
1.2005 + val _ = message "MP:"
1.2006 + val _ = if_debug pth hth1
1.2007 + val _ = if_debug pth hth2
1.2008 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2009 + val th = [beta_eta_thm th1,beta_eta_thm th2] MRS mp_thm
1.2010 + val res = HOLThm(rens_of info,th)
1.2011 + val _ = message "RESULT:"
1.2012 + val _ = if_debug pth res
1.2013 in
1.2014 - (thy,res)
1.2015 + (thy,res)
1.2016 end
1.2017
1.2018 fun CONJ hth1 hth2 thy =
1.2019 let
1.2020 - val _ = message "CONJ:"
1.2021 - val _ = if_debug pth hth1
1.2022 - val _ = if_debug pth hth2
1.2023 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2024 - val th = [th1,th2] MRS conj_thm
1.2025 - val res = HOLThm(rens_of info,th)
1.2026 - val _ = message "RESULT:"
1.2027 - val _ = if_debug pth res
1.2028 + val _ = message "CONJ:"
1.2029 + val _ = if_debug pth hth1
1.2030 + val _ = if_debug pth hth2
1.2031 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2032 + val th = [th1,th2] MRS conj_thm
1.2033 + val res = HOLThm(rens_of info,th)
1.2034 + val _ = message "RESULT:"
1.2035 + val _ = if_debug pth res
1.2036 in
1.2037 - (thy,res)
1.2038 + (thy,res)
1.2039 end
1.2040
1.2041 fun CONJUNCT1 (hth as HOLThm(rens,th)) thy =
1.2042 let
1.2043 - val _ = message "CONJUNCT1:"
1.2044 - val _ = if_debug pth hth
1.2045 - val res = HOLThm(rens,th RS conjunct1_thm)
1.2046 - val _ = message "RESULT:"
1.2047 - val _ = if_debug pth res
1.2048 + val _ = message "CONJUNCT1:"
1.2049 + val _ = if_debug pth hth
1.2050 + val res = HOLThm(rens,th RS conjunct1_thm)
1.2051 + val _ = message "RESULT:"
1.2052 + val _ = if_debug pth res
1.2053 in
1.2054 - (thy,res)
1.2055 + (thy,res)
1.2056 end
1.2057
1.2058 fun CONJUNCT2 (hth as HOLThm(rens,th)) thy =
1.2059 let
1.2060 - val _ = message "CONJUNCT1:"
1.2061 - val _ = if_debug pth hth
1.2062 - val res = HOLThm(rens,th RS conjunct2_thm)
1.2063 - val _ = message "RESULT:"
1.2064 - val _ = if_debug pth res
1.2065 + val _ = message "CONJUNCT1:"
1.2066 + val _ = if_debug pth hth
1.2067 + val res = HOLThm(rens,th RS conjunct2_thm)
1.2068 + val _ = message "RESULT:"
1.2069 + val _ = if_debug pth res
1.2070 in
1.2071 - (thy,res)
1.2072 + (thy,res)
1.2073 end
1.2074
1.2075 fun EXISTS ex wit hth thy =
1.2076 let
1.2077 - val _ = message "EXISTS:"
1.2078 - val _ = if_debug prin ex
1.2079 - val _ = if_debug prin wit
1.2080 - val _ = if_debug pth hth
1.2081 - val (info,th) = disamb_thm hth
1.2082 - val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
1.2083 - val cwit = cterm_of thy wit'
1.2084 - val cty = ctyp_of_term cwit
1.2085 - val a = case ex' of
1.2086 - (Const("Ex",_) $ a) => a
1.2087 - | _ => raise ERR "EXISTS" "Argument not existential"
1.2088 - val ca = cterm_of thy a
1.2089 - val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
1.2090 - val th1 = beta_eta_thm th
1.2091 - val th2 = implies_elim_all th1
1.2092 - val th3 = th2 COMP exists_thm'
1.2093 - val th = implies_intr_hyps th3
1.2094 - val res = HOLThm(rens_of info',th)
1.2095 - val _ = message "RESULT:"
1.2096 - val _ = if_debug pth res
1.2097 + val _ = message "EXISTS:"
1.2098 + val _ = if_debug prin ex
1.2099 + val _ = if_debug prin wit
1.2100 + val _ = if_debug pth hth
1.2101 + val (info,th) = disamb_thm hth
1.2102 + val (info',[ex',wit']) = disamb_terms_from info [ex,wit]
1.2103 + val cwit = cterm_of thy wit'
1.2104 + val cty = ctyp_of_term cwit
1.2105 + val a = case ex' of
1.2106 + (Const("Ex",_) $ a) => a
1.2107 + | _ => raise ERR "EXISTS" "Argument not existential"
1.2108 + val ca = cterm_of thy a
1.2109 + val exists_thm' = beta_eta_thm (Drule.instantiate' [SOME cty] [SOME ca,SOME cwit] exists_thm)
1.2110 + val th1 = beta_eta_thm th
1.2111 + val th2 = implies_elim_all th1
1.2112 + val th3 = th2 COMP exists_thm'
1.2113 + val th = implies_intr_hyps th3
1.2114 + val res = HOLThm(rens_of info',th)
1.2115 + val _ = message "RESULT:"
1.2116 + val _ = if_debug pth res
1.2117 in
1.2118 - (thy,res)
1.2119 + (thy,res)
1.2120 end
1.2121
1.2122 fun CHOOSE v hth1 hth2 thy =
1.2123 let
1.2124 - val _ = message "CHOOSE:"
1.2125 - val _ = if_debug prin v
1.2126 - val _ = if_debug pth hth1
1.2127 - val _ = if_debug pth hth2
1.2128 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2129 - val (info',v') = disamb_term_from info v
1.2130 - fun strip 0 _ th = th
1.2131 - | strip n (p::ps) th =
1.2132 - strip (n-1) ps (implies_elim th (assume p))
1.2133 - | strip _ _ _ = raise ERR "CHOOSE" "strip error"
1.2134 - val cv = cterm_of thy v'
1.2135 - val th2 = norm_hyps th2
1.2136 - val cvty = ctyp_of_term cv
1.2137 - val c = HOLogic.dest_Trueprop (concl_of th2)
1.2138 - val cc = cterm_of thy c
1.2139 - val a = case concl_of th1 of
1.2140 - _ $ (Const("Ex",_) $ a) => a
1.2141 - | _ => raise ERR "CHOOSE" "Conclusion not existential"
1.2142 - val ca = cterm_of (theory_of_thm th1) a
1.2143 - val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
1.2144 - val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
1.2145 - val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
1.2146 - val th23 = beta_eta_thm (forall_intr cv th22)
1.2147 - val th11 = implies_elim_all (beta_eta_thm th1)
1.2148 - val th' = th23 COMP (th11 COMP choose_thm')
1.2149 - val th = implies_intr_hyps th'
1.2150 - val res = HOLThm(rens_of info',th)
1.2151 - val _ = message "RESULT:"
1.2152 - val _ = if_debug pth res
1.2153 + val _ = message "CHOOSE:"
1.2154 + val _ = if_debug prin v
1.2155 + val _ = if_debug pth hth1
1.2156 + val _ = if_debug pth hth2
1.2157 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2158 + val (info',v') = disamb_term_from info v
1.2159 + fun strip 0 _ th = th
1.2160 + | strip n (p::ps) th =
1.2161 + strip (n-1) ps (implies_elim th (assume p))
1.2162 + | strip _ _ _ = raise ERR "CHOOSE" "strip error"
1.2163 + val cv = cterm_of thy v'
1.2164 + val th2 = norm_hyps th2
1.2165 + val cvty = ctyp_of_term cv
1.2166 + val c = HOLogic.dest_Trueprop (concl_of th2)
1.2167 + val cc = cterm_of thy c
1.2168 + val a = case concl_of th1 of
1.2169 + _ $ (Const("Ex",_) $ a) => a
1.2170 + | _ => raise ERR "CHOOSE" "Conclusion not existential"
1.2171 + val ca = cterm_of (theory_of_thm th1) a
1.2172 + val choose_thm' = beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME ca,SOME cc] choose_thm)
1.2173 + val th21 = rearrange thy (HOLogic.mk_Trueprop (a $ v')) th2
1.2174 + val th22 = strip ((nprems_of th21)-1) (cprems_of th21) th21
1.2175 + val th23 = beta_eta_thm (forall_intr cv th22)
1.2176 + val th11 = implies_elim_all (beta_eta_thm th1)
1.2177 + val th' = th23 COMP (th11 COMP choose_thm')
1.2178 + val th = implies_intr_hyps th'
1.2179 + val res = HOLThm(rens_of info',th)
1.2180 + val _ = message "RESULT:"
1.2181 + val _ = if_debug pth res
1.2182 in
1.2183 - (thy,res)
1.2184 + (thy,res)
1.2185 end
1.2186
1.2187 fun GEN v hth thy =
1.2188 let
1.2189 val _ = message "GEN:"
1.2190 - val _ = if_debug prin v
1.2191 - val _ = if_debug pth hth
1.2192 - val (info,th) = disamb_thm hth
1.2193 - val (info',v') = disamb_term_from info v
1.2194 - val res = HOLThm(rens_of info',mk_GEN v' th thy)
1.2195 - val _ = message "RESULT:"
1.2196 - val _ = if_debug pth res
1.2197 + val _ = if_debug prin v
1.2198 + val _ = if_debug pth hth
1.2199 + val (info,th) = disamb_thm hth
1.2200 + val (info',v') = disamb_term_from info v
1.2201 + val res = HOLThm(rens_of info',mk_GEN v' th thy)
1.2202 + val _ = message "RESULT:"
1.2203 + val _ = if_debug pth res
1.2204 in
1.2205 - (thy,res)
1.2206 + (thy,res)
1.2207 end
1.2208
1.2209 fun SPEC tm hth thy =
1.2210 let
1.2211 - val _ = message "SPEC:"
1.2212 - val _ = if_debug prin tm
1.2213 - val _ = if_debug pth hth
1.2214 - val (info,th) = disamb_thm hth
1.2215 - val (info',tm') = disamb_term_from info tm
1.2216 - val ctm = Thm.cterm_of thy tm'
1.2217 - val cty = Thm.ctyp_of_term ctm
1.2218 - val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm
1.2219 - val th = th RS spec'
1.2220 - val res = HOLThm(rens_of info',th)
1.2221 - val _ = message "RESULT:"
1.2222 - val _ = if_debug pth res
1.2223 + val _ = message "SPEC:"
1.2224 + val _ = if_debug prin tm
1.2225 + val _ = if_debug pth hth
1.2226 + val (info,th) = disamb_thm hth
1.2227 + val (info',tm') = disamb_term_from info tm
1.2228 + val ctm = Thm.cterm_of thy tm'
1.2229 + val cty = Thm.ctyp_of_term ctm
1.2230 + val spec' = Drule.instantiate' [SOME cty] [NONE,SOME ctm] spec_thm
1.2231 + val th = th RS spec'
1.2232 + val res = HOLThm(rens_of info',th)
1.2233 + val _ = message "RESULT:"
1.2234 + val _ = if_debug pth res
1.2235 in
1.2236 - (thy,res)
1.2237 + (thy,res)
1.2238 end
1.2239
1.2240 fun COMB hth1 hth2 thy =
1.2241 let
1.2242 - val _ = message "COMB:"
1.2243 - val _ = if_debug pth hth1
1.2244 - val _ = if_debug pth hth2
1.2245 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2246 - val res = HOLThm(rens_of info,mk_COMB th1 th2 thy)
1.2247 - val _ = message "RESULT:"
1.2248 - val _ = if_debug pth res
1.2249 + val _ = message "COMB:"
1.2250 + val _ = if_debug pth hth1
1.2251 + val _ = if_debug pth hth2
1.2252 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2253 + val res = HOLThm(rens_of info,mk_COMB th1 th2 thy)
1.2254 + val _ = message "RESULT:"
1.2255 + val _ = if_debug pth res
1.2256 in
1.2257 - (thy,res)
1.2258 + (thy,res)
1.2259 end
1.2260
1.2261 fun TRANS hth1 hth2 thy =
1.2262 let
1.2263 - val _ = message "TRANS:"
1.2264 - val _ = if_debug pth hth1
1.2265 - val _ = if_debug pth hth2
1.2266 - val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2267 - val th = [th1,th2] MRS trans_thm
1.2268 - val res = HOLThm(rens_of info,th)
1.2269 - val _ = message "RESULT:"
1.2270 - val _ = if_debug pth res
1.2271 + val _ = message "TRANS:"
1.2272 + val _ = if_debug pth hth1
1.2273 + val _ = if_debug pth hth2
1.2274 + val (info,[th1,th2]) = disamb_thms [hth1,hth2]
1.2275 + val th = [th1,th2] MRS trans_thm
1.2276 + val res = HOLThm(rens_of info,th)
1.2277 + val _ = message "RESULT:"
1.2278 + val _ = if_debug pth res
1.2279 in
1.2280 - (thy,res)
1.2281 + (thy,res)
1.2282 end
1.2283
1.2284
1.2285 fun CCONTR tm hth thy =
1.2286 let
1.2287 - val _ = message "SPEC:"
1.2288 - val _ = if_debug prin tm
1.2289 - val _ = if_debug pth hth
1.2290 - val (info,th) = disamb_thm hth
1.2291 - val (info',tm') = disamb_term_from info tm
1.2292 - val th = norm_hyps th
1.2293 - val ct = cterm_of thy tm'
1.2294 - val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
1.2295 - val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
1.2296 - val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
1.2297 - val res = HOLThm(rens_of info',res1)
1.2298 - val _ = message "RESULT:"
1.2299 - val _ = if_debug pth res
1.2300 + val _ = message "SPEC:"
1.2301 + val _ = if_debug prin tm
1.2302 + val _ = if_debug pth hth
1.2303 + val (info,th) = disamb_thm hth
1.2304 + val (info',tm') = disamb_term_from info tm
1.2305 + val th = norm_hyps th
1.2306 + val ct = cterm_of thy tm'
1.2307 + val th1 = rearrange thy (HOLogic.mk_Trueprop (Const("Not",boolT-->boolT) $ tm')) th
1.2308 + val ccontr_thm' = Drule.instantiate' [] [SOME ct] ccontr_thm
1.2309 + val res1 = uniq_compose ((nprems_of th1) - 1) th1 1 ccontr_thm'
1.2310 + val res = HOLThm(rens_of info',res1)
1.2311 + val _ = message "RESULT:"
1.2312 + val _ = if_debug pth res
1.2313 in
1.2314 - (thy,res)
1.2315 + (thy,res)
1.2316 end
1.2317
1.2318 fun mk_ABS v th thy =
1.2319 let
1.2320 - val cv = cterm_of thy v
1.2321 - val th1 = implies_elim_all (beta_eta_thm th)
1.2322 - val (f,g) = case concl_of th1 of
1.2323 - _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
1.2324 - | _ => raise ERR "mk_ABS" "Bad conclusion"
1.2325 - val (fd,fr) = dom_rng (type_of f)
1.2326 - 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
1.2327 - val th2 = forall_intr cv th1
1.2328 - val th3 = th2 COMP abs_thm'
1.2329 - val res = implies_intr_hyps th3
1.2330 + val cv = cterm_of thy v
1.2331 + val th1 = implies_elim_all (beta_eta_thm th)
1.2332 + val (f,g) = case concl_of th1 of
1.2333 + _ $ (Const("op =",_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
1.2334 + | _ => raise ERR "mk_ABS" "Bad conclusion"
1.2335 + val (fd,fr) = dom_rng (type_of f)
1.2336 + 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
1.2337 + val th2 = forall_intr cv th1
1.2338 + val th3 = th2 COMP abs_thm'
1.2339 + val res = implies_intr_hyps th3
1.2340 in
1.2341 - res
1.2342 + res
1.2343 end
1.2344
1.2345 fun ABS v hth thy =
1.2346 let
1.2347 - val _ = message "ABS:"
1.2348 - val _ = if_debug prin v
1.2349 - val _ = if_debug pth hth
1.2350 - val (info,th) = disamb_thm hth
1.2351 - val (info',v') = disamb_term_from info v
1.2352 - val res = HOLThm(rens_of info',mk_ABS v' th thy)
1.2353 - val _ = message "RESULT:"
1.2354 - val _ = if_debug pth res
1.2355 + val _ = message "ABS:"
1.2356 + val _ = if_debug prin v
1.2357 + val _ = if_debug pth hth
1.2358 + val (info,th) = disamb_thm hth
1.2359 + val (info',v') = disamb_term_from info v
1.2360 + val res = HOLThm(rens_of info',mk_ABS v' th thy)
1.2361 + val _ = message "RESULT:"
1.2362 + val _ = if_debug pth res
1.2363 in
1.2364 - (thy,res)
1.2365 + (thy,res)
1.2366 end
1.2367
1.2368 fun GEN_ABS copt vlist hth thy =
1.2369 let
1.2370 - val _ = message "GEN_ABS:"
1.2371 - val _ = case copt of
1.2372 - SOME c => if_debug prin c
1.2373 - | NONE => ()
1.2374 - val _ = if_debug (app prin) vlist
1.2375 - val _ = if_debug pth hth
1.2376 - val (info,th) = disamb_thm hth
1.2377 - val (info',vlist') = disamb_terms_from info vlist
1.2378 - val th1 =
1.2379 - case copt of
1.2380 - SOME (c as Const(cname,cty)) =>
1.2381 - let
1.2382 - fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!"
1.2383 - | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty
1.2384 - then ty2
1.2385 - else ty
1.2386 - | inst_type ty1 ty2 (ty as Type(name,tys)) =
1.2387 - Type(name,map (inst_type ty1 ty2) tys)
1.2388 - in
1.2389 - foldr (fn (v,th) =>
1.2390 - let
1.2391 - val cdom = fst (dom_rng (fst (dom_rng cty)))
1.2392 - val vty = type_of v
1.2393 - val newcty = inst_type cdom vty cty
1.2394 - val cc = cterm_of thy (Const(cname,newcty))
1.2395 - in
1.2396 - mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
1.2397 - end) th vlist'
1.2398 - end
1.2399 - | SOME _ => raise ERR "GEN_ABS" "Bad constant"
1.2400 - | NONE =>
1.2401 - foldr (fn (v,th) => mk_ABS v th thy) th vlist'
1.2402 - val res = HOLThm(rens_of info',th1)
1.2403 - val _ = message "RESULT:"
1.2404 - val _ = if_debug pth res
1.2405 + val _ = message "GEN_ABS:"
1.2406 + val _ = case copt of
1.2407 + SOME c => if_debug prin c
1.2408 + | NONE => ()
1.2409 + val _ = if_debug (app prin) vlist
1.2410 + val _ = if_debug pth hth
1.2411 + val (info,th) = disamb_thm hth
1.2412 + val (info',vlist') = disamb_terms_from info vlist
1.2413 + val th1 =
1.2414 + case copt of
1.2415 + SOME (c as Const(cname,cty)) =>
1.2416 + let
1.2417 + fun inst_type ty1 ty2 (TVar _) = raise ERR "GEN_ABS" "Type variable found!"
1.2418 + | inst_type ty1 ty2 (ty as TFree _) = if ty1 = ty
1.2419 + then ty2
1.2420 + else ty
1.2421 + | inst_type ty1 ty2 (ty as Type(name,tys)) =
1.2422 + Type(name,map (inst_type ty1 ty2) tys)
1.2423 + in
1.2424 + foldr (fn (v,th) =>
1.2425 + let
1.2426 + val cdom = fst (dom_rng (fst (dom_rng cty)))
1.2427 + val vty = type_of v
1.2428 + val newcty = inst_type cdom vty cty
1.2429 + val cc = cterm_of thy (Const(cname,newcty))
1.2430 + in
1.2431 + mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
1.2432 + end) th vlist'
1.2433 + end
1.2434 + | SOME _ => raise ERR "GEN_ABS" "Bad constant"
1.2435 + | NONE =>
1.2436 + foldr (fn (v,th) => mk_ABS v th thy) th vlist'
1.2437 + val res = HOLThm(rens_of info',th1)
1.2438 + val _ = message "RESULT:"
1.2439 + val _ = if_debug pth res
1.2440 in
1.2441 - (thy,res)
1.2442 + (thy,res)
1.2443 end
1.2444
1.2445 fun NOT_INTRO (hth as HOLThm(rens,th)) thy =
1.2446 let
1.2447 - val _ = message "NOT_INTRO:"
1.2448 - val _ = if_debug pth hth
1.2449 - val th1 = implies_elim_all (beta_eta_thm th)
1.2450 - val a = case concl_of th1 of
1.2451 - _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
1.2452 - | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
1.2453 - val ca = cterm_of thy a
1.2454 - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
1.2455 - val res = HOLThm(rens,implies_intr_hyps th2)
1.2456 - val _ = message "RESULT:"
1.2457 - val _ = if_debug pth res
1.2458 + val _ = message "NOT_INTRO:"
1.2459 + val _ = if_debug pth hth
1.2460 + val th1 = implies_elim_all (beta_eta_thm th)
1.2461 + val a = case concl_of th1 of
1.2462 + _ $ (Const("op -->",_) $ a $ Const("False",_)) => a
1.2463 + | _ => raise ERR "NOT_INTRO" "Conclusion of bad form"
1.2464 + val ca = cterm_of thy a
1.2465 + val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_intro_thm) th1
1.2466 + val res = HOLThm(rens,implies_intr_hyps th2)
1.2467 + val _ = message "RESULT:"
1.2468 + val _ = if_debug pth res
1.2469 in
1.2470 - (thy,res)
1.2471 + (thy,res)
1.2472 end
1.2473
1.2474 fun NOT_ELIM (hth as HOLThm(rens,th)) thy =
1.2475 let
1.2476 - val _ = message "NOT_INTRO:"
1.2477 - val _ = if_debug pth hth
1.2478 - val th1 = implies_elim_all (beta_eta_thm th)
1.2479 - val a = case concl_of th1 of
1.2480 - _ $ (Const("Not",_) $ a) => a
1.2481 - | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
1.2482 - val ca = cterm_of thy a
1.2483 - val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
1.2484 - val res = HOLThm(rens,implies_intr_hyps th2)
1.2485 - val _ = message "RESULT:"
1.2486 - val _ = if_debug pth res
1.2487 + val _ = message "NOT_INTRO:"
1.2488 + val _ = if_debug pth hth
1.2489 + val th1 = implies_elim_all (beta_eta_thm th)
1.2490 + val a = case concl_of th1 of
1.2491 + _ $ (Const("Not",_) $ a) => a
1.2492 + | _ => raise ERR "NOT_ELIM" "Conclusion of bad form"
1.2493 + val ca = cterm_of thy a
1.2494 + val th2 = equal_elim (Drule.instantiate' [] [SOME ca] not_elim_thm) th1
1.2495 + val res = HOLThm(rens,implies_intr_hyps th2)
1.2496 + val _ = message "RESULT:"
1.2497 + val _ = if_debug pth res
1.2498 in
1.2499 - (thy,res)
1.2500 + (thy,res)
1.2501 end
1.2502
1.2503 fun DISCH tm hth thy =
1.2504 let
1.2505 - val _ = message "DISCH:"
1.2506 - val _ = if_debug prin tm
1.2507 - val _ = if_debug pth hth
1.2508 - val (info,th) = disamb_thm hth
1.2509 - val (info',tm') = disamb_term_from info tm
1.2510 - val prems = prems_of th
1.2511 - val th1 = beta_eta_thm th
1.2512 - val th2 = implies_elim_all th1
1.2513 - val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
1.2514 - val th4 = th3 COMP disch_thm
1.2515 - val res = HOLThm(rens_of info',implies_intr_hyps th4)
1.2516 - val _ = message "RESULT:"
1.2517 - val _ = if_debug pth res
1.2518 + val _ = message "DISCH:"
1.2519 + val _ = if_debug prin tm
1.2520 + val _ = if_debug pth hth
1.2521 + val (info,th) = disamb_thm hth
1.2522 + val (info',tm') = disamb_term_from info tm
1.2523 + val prems = prems_of th
1.2524 + val th1 = beta_eta_thm th
1.2525 + val th2 = implies_elim_all th1
1.2526 + val th3 = implies_intr (cterm_of thy (HOLogic.mk_Trueprop tm')) th2
1.2527 + val th4 = th3 COMP disch_thm
1.2528 + val res = HOLThm(rens_of info',implies_intr_hyps th4)
1.2529 + val _ = message "RESULT:"
1.2530 + val _ = if_debug pth res
1.2531 in
1.2532 - (thy,res)
1.2533 + (thy,res)
1.2534 end
1.2535
1.2536 val spaces = String.concat o separate " "
1.2537
1.2538 fun new_definition thyname constname rhs thy =
1.2539 let
1.2540 - val constname = rename_const thyname thy constname
1.2541 + val constname = rename_const thyname thy constname
1.2542 val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
1.2543 - val _ = warning ("Introducing constant " ^ constname)
1.2544 - val (thmname,thy) = get_defname thyname constname thy
1.2545 - val (info,rhs') = disamb_term rhs
1.2546 - val ctype = type_of rhs'
1.2547 - val csyn = mk_syn thy constname
1.2548 - val thy1 = case HOL4DefThy.get thy of
1.2549 - Replaying _ => thy
1.2550 - | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
1.2551 - val eq = mk_defeq constname rhs' thy1
1.2552 - val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
1.2553 - val _ = ImportRecorder.add_defs thmname eq
1.2554 - val def_thm = hd thms
1.2555 - val thm' = def_thm RS meta_eq_to_obj_eq_thm
1.2556 - val (thy',th) = (thy2, thm')
1.2557 - val fullcname = Sign.intern_const thy' constname
1.2558 - val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
1.2559 - val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
1.2560 - val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
1.2561 - val rew = rewrite_hol4_term eq thy''
1.2562 - val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
1.2563 - val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
1.2564 - then
1.2565 - let
1.2566 - val p1 = quotename constname
1.2567 - val p2 = string_of_ctyp (ctyp_of thy'' ctype)
1.2568 - val p3 = string_of_mixfix csyn
1.2569 - val p4 = smart_string_of_cterm crhs
1.2570 - in
1.2571 - add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
1.2572 - end
1.2573 - else
1.2574 - (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
1.2575 - "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
1.2576 - thy'')
1.2577 - val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
1.2578 - SOME (_,res) => HOLThm(rens_of linfo,res)
1.2579 - | NONE => raise ERR "new_definition" "Bad conclusion"
1.2580 - val fullname = Sign.full_name thy22 thmname
1.2581 - val thy22' = case opt_get_output_thy thy22 of
1.2582 - "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
1.2583 - add_hol4_mapping thyname thmname fullname thy22)
1.2584 - | output_thy =>
1.2585 - let
1.2586 - val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
1.2587 - val _ = ImportRecorder.add_hol_move fullname moved_thmname
1.2588 - val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
1.2589 - in
1.2590 - thy22 |> add_hol4_move fullname moved_thmname
1.2591 - |> add_hol4_mapping thyname thmname moved_thmname
1.2592 - end
1.2593 - val _ = message "new_definition:"
1.2594 - val _ = if_debug pth hth
1.2595 + val _ = warning ("Introducing constant " ^ constname)
1.2596 + val (thmname,thy) = get_defname thyname constname thy
1.2597 + val (info,rhs') = disamb_term rhs
1.2598 + val ctype = type_of rhs'
1.2599 + val csyn = mk_syn thy constname
1.2600 + val thy1 = case HOL4DefThy.get thy of
1.2601 + Replaying _ => thy
1.2602 + | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
1.2603 + val eq = mk_defeq constname rhs' thy1
1.2604 + val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
1.2605 + val _ = ImportRecorder.add_defs thmname eq
1.2606 + val def_thm = hd thms
1.2607 + val thm' = def_thm RS meta_eq_to_obj_eq_thm
1.2608 + val (thy',th) = (thy2, thm')
1.2609 + val fullcname = Sign.intern_const thy' constname
1.2610 + val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
1.2611 + val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
1.2612 + val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
1.2613 + val rew = rewrite_hol4_term eq thy''
1.2614 + val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
1.2615 + val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
1.2616 + then
1.2617 + let
1.2618 + val p1 = quotename constname
1.2619 + val p2 = string_of_ctyp (ctyp_of thy'' ctype)
1.2620 + val p3 = string_of_mixfix csyn
1.2621 + val p4 = smart_string_of_cterm crhs
1.2622 + in
1.2623 + add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy''
1.2624 + end
1.2625 + else
1.2626 + (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^
1.2627 + "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs))
1.2628 + thy'')
1.2629 + val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
1.2630 + SOME (_,res) => HOLThm(rens_of linfo,res)
1.2631 + | NONE => raise ERR "new_definition" "Bad conclusion"
1.2632 + val fullname = Sign.full_name thy22 thmname
1.2633 + val thy22' = case opt_get_output_thy thy22 of
1.2634 + "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
1.2635 + add_hol4_mapping thyname thmname fullname thy22)
1.2636 + | output_thy =>
1.2637 + let
1.2638 + val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
1.2639 + val _ = ImportRecorder.add_hol_move fullname moved_thmname
1.2640 + val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
1.2641 + in
1.2642 + thy22 |> add_hol4_move fullname moved_thmname
1.2643 + |> add_hol4_mapping thyname thmname moved_thmname
1.2644 + end
1.2645 + val _ = message "new_definition:"
1.2646 + val _ = if_debug pth hth
1.2647 in
1.2648 - (thy22',hth)
1.2649 + (thy22',hth)
1.2650 end
1.2651 handle e => (message "exception in new_definition"; print_exn e)
1.2652
1.2653 @@ -1983,81 +1985,81 @@
1.2654 in
1.2655 fun new_specification thyname thmname names hth thy =
1.2656 case HOL4DefThy.get thy of
1.2657 - Replaying _ => (thy,hth)
1.2658 + Replaying _ => (thy,hth)
1.2659 | _ =>
1.2660 - let
1.2661 - val _ = message "NEW_SPEC:"
1.2662 - val _ = if_debug pth hth
1.2663 - val names = map (rename_const thyname thy) names
1.2664 - val _ = warning ("Introducing constants " ^ commas names)
1.2665 - val (HOLThm(rens,th)) = norm_hthm thy hth
1.2666 - val thy1 = case HOL4DefThy.get thy of
1.2667 - Replaying _ => thy
1.2668 - | _ =>
1.2669 - let
1.2670 - fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
1.2671 - | dest_eta_abs body =
1.2672 - let
1.2673 - val (dT,rT) = dom_rng (type_of body)
1.2674 - in
1.2675 - ("x",dT,body $ Bound 0)
1.2676 - end
1.2677 - handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
1.2678 - fun dest_exists (Const("Ex",_) $ abody) =
1.2679 - dest_eta_abs abody
1.2680 - | dest_exists tm =
1.2681 - raise ERR "new_specification" "Bad existential formula"
1.2682 + let
1.2683 + val _ = message "NEW_SPEC:"
1.2684 + val _ = if_debug pth hth
1.2685 + val names = map (rename_const thyname thy) names
1.2686 + val _ = warning ("Introducing constants " ^ commas names)
1.2687 + val (HOLThm(rens,th)) = norm_hthm thy hth
1.2688 + val thy1 = case HOL4DefThy.get thy of
1.2689 + Replaying _ => thy
1.2690 + | _ =>
1.2691 + let
1.2692 + fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
1.2693 + | dest_eta_abs body =
1.2694 + let
1.2695 + val (dT,rT) = dom_rng (type_of body)
1.2696 + in
1.2697 + ("x",dT,body $ Bound 0)
1.2698 + end
1.2699 + handle TYPE _ => raise ERR "new_specification" "not an abstraction type"
1.2700 + fun dest_exists (Const("Ex",_) $ abody) =
1.2701 + dest_eta_abs abody
1.2702 + | dest_exists tm =
1.2703 + raise ERR "new_specification" "Bad existential formula"
1.2704
1.2705 - val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
1.2706 - let
1.2707 - val (_,cT,p) = dest_exists ex
1.2708 - in
1.2709 - ((cname,cT,mk_syn thy cname)::cs,p)
1.2710 - end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
1.2711 - val str = Library.foldl (fn (acc,(c,T,csyn)) =>
1.2712 - acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
1.2713 - val thy' = add_dump str thy
1.2714 - val _ = ImportRecorder.add_consts consts
1.2715 - in
1.2716 - Sign.add_consts_i consts thy'
1.2717 - end
1.2718 + val (consts,_) = Library.foldl (fn ((cs,ex),cname) =>
1.2719 + let
1.2720 + val (_,cT,p) = dest_exists ex
1.2721 + in
1.2722 + ((cname,cT,mk_syn thy cname)::cs,p)
1.2723 + end) (([],HOLogic.dest_Trueprop (concl_of th)),names)
1.2724 + val str = Library.foldl (fn (acc,(c,T,csyn)) =>
1.2725 + acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts)
1.2726 + val thy' = add_dump str thy
1.2727 + val _ = ImportRecorder.add_consts consts
1.2728 + in
1.2729 + Sign.add_consts_i consts thy'
1.2730 + end
1.2731
1.2732 - val thy1 = foldr (fn(name,thy)=>
1.2733 - snd (get_defname thyname name thy)) thy1 names
1.2734 - fun new_name name = fst (get_defname thyname name thy1)
1.2735 - val names' = map (fn name => (new_name name,name,false)) names
1.2736 - val (thy',res) = SpecificationPackage.add_specification NONE
1.2737 - names'
1.2738 - (thy1,th)
1.2739 - val _ = ImportRecorder.add_specification names' th
1.2740 - val res' = Thm.unvarify res
1.2741 - val hth = HOLThm(rens,res')
1.2742 - val rew = rewrite_hol4_term (concl_of res') thy'
1.2743 - val th = equal_elim rew res'
1.2744 - fun handle_const (name,thy) =
1.2745 - let
1.2746 - val defname = def_name name
1.2747 - val (newname,thy') = get_defname thyname name thy
1.2748 - in
1.2749 - (if defname = newname
1.2750 - then quotename name
1.2751 - else (quotename newname) ^ ": " ^ (quotename name),thy')
1.2752 - end
1.2753 - val (new_names,thy') = foldr (fn(name,(names,thy)) =>
1.2754 - let
1.2755 - val (name',thy') = handle_const (name,thy)
1.2756 - in
1.2757 - (name'::names,thy')
1.2758 - end) ([],thy') names
1.2759 - val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
1.2760 - "\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
1.2761 - thy'
1.2762 - val _ = message "RESULT:"
1.2763 - val _ = if_debug pth hth
1.2764 - in
1.2765 - intern_store_thm false thyname thmname hth thy''
1.2766 - end
1.2767 - handle e => (message "exception in new_specification"; print_exn e)
1.2768 + val thy1 = foldr (fn(name,thy)=>
1.2769 + snd (get_defname thyname name thy)) thy1 names
1.2770 + fun new_name name = fst (get_defname thyname name thy1)
1.2771 + val names' = map (fn name => (new_name name,name,false)) names
1.2772 + val (thy',res) = SpecificationPackage.add_specification NONE
1.2773 + names'
1.2774 + (thy1,th)
1.2775 + val _ = ImportRecorder.add_specification names' th
1.2776 + val res' = Thm.unvarify res
1.2777 + val hth = HOLThm(rens,res')
1.2778 + val rew = rewrite_hol4_term (concl_of res') thy'
1.2779 + val th = equal_elim rew res'
1.2780 + fun handle_const (name,thy) =
1.2781 + let
1.2782 + val defname = def_name name
1.2783 + val (newname,thy') = get_defname thyname name thy
1.2784 + in
1.2785 + (if defname = newname
1.2786 + then quotename name
1.2787 + else (quotename newname) ^ ": " ^ (quotename name),thy')
1.2788 + end
1.2789 + val (new_names,thy') = foldr (fn(name,(names,thy)) =>
1.2790 + let
1.2791 + val (name',thy') = handle_const (name,thy)
1.2792 + in
1.2793 + (name'::names,thy')
1.2794 + end) ([],thy') names
1.2795 + val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
1.2796 + "\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
1.2797 + thy'
1.2798 + val _ = message "RESULT:"
1.2799 + val _ = if_debug pth hth
1.2800 + in
1.2801 + intern_store_thm false thyname thmname hth thy''
1.2802 + end
1.2803 + handle e => (message "exception in new_specification"; print_exn e)
1.2804
1.2805 end
1.2806
1.2807 @@ -2065,9 +2067,9 @@
1.2808
1.2809 fun to_isa_thm (hth as HOLThm(_,th)) =
1.2810 let
1.2811 - val (HOLThm args) = norm_hthm (theory_of_thm th) hth
1.2812 + val (HOLThm args) = norm_hthm (theory_of_thm th) hth
1.2813 in
1.2814 - apsnd strip_shyps args
1.2815 + apsnd strip_shyps args
1.2816 end
1.2817
1.2818 fun to_isa_term tm = tm
1.2819 @@ -2080,74 +2082,74 @@
1.2820 in
1.2821 fun new_type_definition thyname thmname tycname hth thy =
1.2822 case HOL4DefThy.get thy of
1.2823 - Replaying _ => (thy,hth)
1.2824 + Replaying _ => (thy,hth)
1.2825 | _ =>
1.2826 - let
1.2827 - val _ = message "TYPE_DEF:"
1.2828 - val _ = if_debug pth hth
1.2829 - val _ = warning ("Introducing type " ^ tycname)
1.2830 - val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.2831 - val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
1.2832 - val c = case concl_of th2 of
1.2833 - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
1.2834 - | _ => raise ERR "new_type_definition" "Bad type definition theorem"
1.2835 - val tfrees = term_tfrees c
1.2836 - val tnames = map fst tfrees
1.2837 - val tsyn = mk_syn thy tycname
1.2838 - val typ = (tycname,tnames,tsyn)
1.2839 - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
1.2840 + let
1.2841 + val _ = message "TYPE_DEF:"
1.2842 + val _ = if_debug pth hth
1.2843 + val _ = warning ("Introducing type " ^ tycname)
1.2844 + val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.2845 + val th2 = beta_eta_thm (td_th RS ex_imp_nonempty)
1.2846 + val c = case concl_of th2 of
1.2847 + _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
1.2848 + | _ => raise ERR "new_type_definition" "Bad type definition theorem"
1.2849 + val tfrees = term_tfrees c
1.2850 + val tnames = map fst tfrees
1.2851 + val tsyn = mk_syn thy tycname
1.2852 + val typ = (tycname,tnames,tsyn)
1.2853 + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
1.2854 val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
1.2855
1.2856 - val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
1.2857 + val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
1.2858
1.2859 - val fulltyname = Sign.intern_type thy' tycname
1.2860 - val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
1.2861 - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
1.2862 + val fulltyname = Sign.intern_type thy' tycname
1.2863 + val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
1.2864 + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
1.2865
1.2866 - val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
1.2867 - val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
1.2868 - else ()
1.2869 - val thy4 = add_hol4_pending thyname thmname args thy''
1.2870 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.2871 + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
1.2872 + val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
1.2873 + else ()
1.2874 + val thy4 = add_hol4_pending thyname thmname args thy''
1.2875 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.2876
1.2877 - val rew = rewrite_hol4_term (concl_of td_th) thy4
1.2878 - val th = equal_elim rew (Thm.transfer thy4 td_th)
1.2879 - val c = case HOLogic.dest_Trueprop (prop_of th) of
1.2880 - Const("Ex",exT) $ P =>
1.2881 - let
1.2882 - val PT = domain_type exT
1.2883 - in
1.2884 - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
1.2885 - end
1.2886 - | _ => error "Internal error in ProofKernel.new_typedefinition"
1.2887 - val tnames_string = if null tnames
1.2888 - then ""
1.2889 - else "(" ^ commas tnames ^ ") "
1.2890 - val proc_prop = if null tnames
1.2891 - then smart_string_of_cterm
1.2892 - else Library.setmp show_all_types true smart_string_of_cterm
1.2893 - val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
1.2894 - ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
1.2895 + val rew = rewrite_hol4_term (concl_of td_th) thy4
1.2896 + val th = equal_elim rew (Thm.transfer thy4 td_th)
1.2897 + val c = case HOLogic.dest_Trueprop (prop_of th) of
1.2898 + Const("Ex",exT) $ P =>
1.2899 + let
1.2900 + val PT = domain_type exT
1.2901 + in
1.2902 + Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P
1.2903 + end
1.2904 + | _ => error "Internal error in ProofKernel.new_typedefinition"
1.2905 + val tnames_string = if null tnames
1.2906 + then ""
1.2907 + else "(" ^ commas tnames ^ ") "
1.2908 + val proc_prop = if null tnames
1.2909 + then smart_string_of_cterm
1.2910 + else Library.setmp show_all_types true smart_string_of_cterm
1.2911 + val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
1.2912 + ^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
1.2913
1.2914 - val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
1.2915 + val thy6 = add_dump ("lemmas " ^ thmname ^ " = typedef_hol2hol4 [OF type_definition_" ^ tycname ^ "]") thy5
1.2916
1.2917 - val _ = message "RESULT:"
1.2918 - val _ = if_debug pth hth'
1.2919 - in
1.2920 - (thy6,hth')
1.2921 - end
1.2922 - handle e => (message "exception in new_type_definition"; print_exn e)
1.2923 + val _ = message "RESULT:"
1.2924 + val _ = if_debug pth hth'
1.2925 + in
1.2926 + (thy6,hth')
1.2927 + end
1.2928 + handle e => (message "exception in new_type_definition"; print_exn e)
1.2929
1.2930 fun add_dump_constdefs thy defname constname rhs ty =
1.2931 let
1.2932 - val n = quotename constname
1.2933 - val t = string_of_ctyp (ctyp_of thy ty)
1.2934 - val syn = string_of_mixfix (mk_syn thy constname)
1.2935 - (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
1.2936 + val n = quotename constname
1.2937 + val t = string_of_ctyp (ctyp_of thy ty)
1.2938 + val syn = string_of_mixfix (mk_syn thy constname)
1.2939 + (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*)
1.2940 val eq = quote (constname ^ " == "^rhs)
1.2941 - val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
1.2942 + val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : "
1.2943 in
1.2944 - add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
1.2945 + add_dump ("constdefs\n " ^ n ^ " :: \"" ^ t ^ "\" " ^ syn ^ "\n " ^ d ^ eq) thy
1.2946 end
1.2947
1.2948 fun add_dump_syntax thy name =
1.2949 @@ -2160,85 +2162,85 @@
1.2950
1.2951 fun type_introduction thyname thmname tycname abs_name rep_name (P,t) hth thy =
1.2952 case HOL4DefThy.get thy of
1.2953 - Replaying _ => (thy,
1.2954 + Replaying _ => (thy,
1.2955 HOLThm([], PureThy.get_thm thy (thmname^"_@intern")) handle ERROR _ => hth)
1.2956 | _ =>
1.2957 - let
1.2958 + let
1.2959 val _ = message "TYPE_INTRO:"
1.2960 - val _ = if_debug pth hth
1.2961 - val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
1.2962 - val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.2963 - val tT = type_of t
1.2964 - val light_nonempty' =
1.2965 - Drule.instantiate' [SOME (ctyp_of thy tT)]
1.2966 - [SOME (cterm_of thy P),
1.2967 - SOME (cterm_of thy t)] light_nonempty
1.2968 - val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
1.2969 - val c = case concl_of th2 of
1.2970 - _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
1.2971 - | _ => raise ERR "type_introduction" "Bad type definition theorem"
1.2972 - val tfrees = term_tfrees c
1.2973 - val tnames = sort string_ord (map fst tfrees)
1.2974 - val tsyn = mk_syn thy tycname
1.2975 - val typ = (tycname,tnames,tsyn)
1.2976 - val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
1.2977 - val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
1.2978 - val fulltyname = Sign.intern_type thy' tycname
1.2979 - val aty = Type (fulltyname, map mk_vartype tnames)
1.2980 - val abs_ty = tT --> aty
1.2981 - val rep_ty = aty --> tT
1.2982 + val _ = if_debug pth hth
1.2983 + val _ = warning ("Introducing type " ^ tycname ^ " (with morphisms " ^ abs_name ^ " and " ^ rep_name ^ ")")
1.2984 + val (HOLThm(rens,td_th)) = norm_hthm thy hth
1.2985 + val tT = type_of t
1.2986 + val light_nonempty' =
1.2987 + Drule.instantiate' [SOME (ctyp_of thy tT)]
1.2988 + [SOME (cterm_of thy P),
1.2989 + SOME (cterm_of thy t)] light_nonempty
1.2990 + val th2 = beta_eta_thm (td_th RS (beta_eta_thm light_nonempty'))
1.2991 + val c = case concl_of th2 of
1.2992 + _ $ (Const("Ex",_) $ Abs(_,_,Const("op :",_) $ _ $ c)) => c
1.2993 + | _ => raise ERR "type_introduction" "Bad type definition theorem"
1.2994 + val tfrees = term_tfrees c
1.2995 + val tnames = sort string_ord (map fst tfrees)
1.2996 + val tsyn = mk_syn thy tycname
1.2997 + val typ = (tycname,tnames,tsyn)
1.2998 + val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
1.2999 + val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
1.3000 + val fulltyname = Sign.intern_type thy' tycname
1.3001 + val aty = Type (fulltyname, map mk_vartype tnames)
1.3002 + val abs_ty = tT --> aty
1.3003 + val rep_ty = aty --> tT
1.3004 val typedef_hol2hollight' =
1.3005 - Drule.instantiate'
1.3006 - [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
1.3007 - [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
1.3008 + Drule.instantiate'
1.3009 + [SOME (ctyp_of thy' aty), SOME (ctyp_of thy' tT)]
1.3010 + [NONE, NONE, NONE, SOME (cterm_of thy' (Free ("a", aty))), SOME (cterm_of thy' (Free ("r", tT)))]
1.3011 typedef_hol2hollight
1.3012 - val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
1.3013 + val th4 = (#type_definition typedef_info) RS typedef_hol2hollight'
1.3014 val _ = null (Thm.fold_terms Term.add_tvars th4 []) orelse
1.3015 raise ERR "type_introduction" "no type variables expected any more"
1.3016 val _ = null (Thm.fold_terms Term.add_vars th4 []) orelse
1.3017 raise ERR "type_introduction" "no term variables expected any more"
1.3018 - val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
1.3019 + val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
1.3020 val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
1.3021 - val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
1.3022 + val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
1.3023 val _ = message "step 4"
1.3024 - val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
1.3025 - val thy4 = add_hol4_pending thyname thmname args thy''
1.3026 - val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.3027 + val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
1.3028 + val thy4 = add_hol4_pending thyname thmname args thy''
1.3029 + val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
1.3030
1.3031 - val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
1.3032 - val c =
1.3033 - let
1.3034 - val PT = type_of P'
1.3035 - in
1.3036 - Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
1.3037 - end
1.3038 + val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
1.3039 + val c =
1.3040 + let
1.3041 + val PT = type_of P'
1.3042 + in
1.3043 + Const("Collect",PT-->HOLogic.mk_setT (domain_type PT)) $ P'
1.3044 + end
1.3045
1.3046 - val tnames_string = if null tnames
1.3047 - then ""
1.3048 - else "(" ^ commas tnames ^ ") "
1.3049 - val proc_prop = if null tnames
1.3050 - then smart_string_of_cterm
1.3051 - else Library.setmp show_all_types true smart_string_of_cterm
1.3052 - val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
1.3053 + val tnames_string = if null tnames
1.3054 + then ""
1.3055 + else "(" ^ commas tnames ^ ") "
1.3056 + val proc_prop = if null tnames
1.3057 + then smart_string_of_cterm
1.3058 + else Library.setmp show_all_types true smart_string_of_cterm
1.3059 + val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
1.3060 " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
1.3061 - (string_of_mixfix tsyn) ^ " morphisms "^
1.3062 + (string_of_mixfix tsyn) ^ " morphisms "^
1.3063 (quote rep_name)^" "^(quote abs_name)^"\n"^
1.3064 - (" apply (rule light_ex_imp_nonempty[where t="^
1.3065 + (" apply (rule light_ex_imp_nonempty[where t="^
1.3066 (proc_prop (cterm_of thy4 t))^"])\n"^
1.3067 - (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
1.3068 - val str_aty = string_of_ctyp (ctyp_of thy aty)
1.3069 + (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4
1.3070 + val str_aty = string_of_ctyp (ctyp_of thy aty)
1.3071 val thy = add_dump_syntax thy rep_name
1.3072 val thy = add_dump_syntax thy abs_name
1.3073 - val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
1.3074 + val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^
1.3075 " = typedef_hol2hollight \n"^
1.3076 " [where a=\"a :: "^str_aty^"\" and r=r" ^
1.3077 - " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
1.3078 - val _ = message "RESULT:"
1.3079 - val _ = if_debug pth hth'
1.3080 - in
1.3081 - (thy,hth')
1.3082 - end
1.3083 - handle e => (message "exception in type_introduction"; print_exn e)
1.3084 + " ,\n OF "^(quotename ("type_definition_" ^ tycname)) ^ "]") thy
1.3085 + val _ = message "RESULT:"
1.3086 + val _ = if_debug pth hth'
1.3087 + in
1.3088 + (thy,hth')
1.3089 + end
1.3090 + handle e => (message "exception in type_introduction"; print_exn e)
1.3091 end
1.3092
1.3093 val prin = prin
2.1 --- a/src/HOL/Tools/TFL/dcterm.ML Thu Apr 10 20:54:18 2008 +0200
2.2 +++ b/src/HOL/Tools/TFL/dcterm.ML Sat Apr 12 17:00:35 2008 +0200
2.3 @@ -187,7 +187,10 @@
2.4 *---------------------------------------------------------------------------*)
2.5
2.6 fun mk_prop ctm =
2.7 - let val {t, thy, ...} = Thm.rep_cterm ctm in
2.8 + let
2.9 + val thy = Thm.theory_of_cterm ctm;
2.10 + val t = Thm.term_of ctm;
2.11 + in
2.12 if can HOLogic.dest_Trueprop t then ctm
2.13 else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
2.14 end
3.1 --- a/src/HOL/Tools/TFL/post.ML Thu Apr 10 20:54:18 2008 +0200
3.2 +++ b/src/HOL/Tools/TFL/post.ML Sat Apr 12 17:00:35 2008 +0200
3.3 @@ -93,7 +93,7 @@
3.4 fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
3.5
3.6 fun join_assums th =
3.7 - let val {thy,...} = rep_thm th
3.8 + let val thy = Thm.theory_of_thm th
3.9 val tych = cterm_of thy
3.10 val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
3.11 val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
4.1 --- a/src/HOL/Tools/TFL/rules.ML Thu Apr 10 20:54:18 2008 +0200
4.2 +++ b/src/HOL/Tools/TFL/rules.ML Sat Apr 12 17:00:35 2008 +0200
4.3 @@ -171,7 +171,8 @@
4.4 (*----------------------------------------------------------------------------
4.5 * Disjunction
4.6 *---------------------------------------------------------------------------*)
4.7 -local val {prop,thy,...} = rep_thm disjI1
4.8 +local val thy = Thm.theory_of_thm disjI1
4.9 + val prop = Thm.prop_of disjI1
4.10 val [P,Q] = term_vars prop
4.11 val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
4.12 in
4.13 @@ -179,7 +180,8 @@
4.14 handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
4.15 end;
4.16
4.17 -local val {prop,thy,...} = rep_thm disjI2
4.18 +local val thy = Thm.theory_of_thm disjI2
4.19 + val prop = Thm.prop_of disjI2
4.20 val [P,Q] = term_vars prop
4.21 val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
4.22 in
4.23 @@ -274,17 +276,15 @@
4.24 * Universals
4.25 *---------------------------------------------------------------------------*)
4.26 local (* this is fragile *)
4.27 - val {prop,thy,...} = rep_thm spec
4.28 + val thy = Thm.theory_of_thm spec
4.29 + val prop = Thm.prop_of spec
4.30 val x = hd (tl (term_vars prop))
4.31 val cTV = ctyp_of thy (type_of x)
4.32 val gspec = forall_intr (cterm_of thy x) spec
4.33 in
4.34 fun SPEC tm thm =
4.35 - let val {thy,T,...} = rep_cterm tm
4.36 - val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec
4.37 - in
4.38 - thm RS (forall_elim tm gspec')
4.39 - end
4.40 + let val gspec' = instantiate ([(cTV, Thm.ctyp_of_term tm)], []) gspec
4.41 + in thm RS (forall_elim tm gspec') end
4.42 end;
4.43
4.44 fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
4.45 @@ -293,7 +293,8 @@
4.46 val ISPECL = fold ISPEC;
4.47
4.48 (* Not optimized! Too complicated. *)
4.49 -local val {prop,thy,...} = rep_thm allI
4.50 +local val thy = Thm.theory_of_thm allI
4.51 + val prop = Thm.prop_of allI
4.52 val [P] = add_term_vars (prop, [])
4.53 fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
4.54 fun ctm_theta s = map (fn (i, (_, tm2)) =>
4.55 @@ -306,12 +307,13 @@
4.56 in
4.57 fun GEN v th =
4.58 let val gth = forall_intr v th
4.59 - val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth
4.60 + val thy = Thm.theory_of_thm gth
4.61 + val Const("all",_)$Abs(x,ty,rst) = Thm.prop_of gth
4.62 val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
4.63 val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
4.64 val allI2 = instantiate (certify thy theta) allI
4.65 val thm = Thm.implies_elim allI2 gth
4.66 - val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm
4.67 + val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
4.68 val prop' = tp $ (A $ Abs(x,ty,M))
4.69 in ALPHA thm (cterm_of thy prop')
4.70 end
4.71 @@ -320,7 +322,8 @@
4.72 val GENL = fold_rev GEN;
4.73
4.74 fun GEN_ALL thm =
4.75 - let val {prop,thy,...} = rep_thm thm
4.76 + let val thy = Thm.theory_of_thm thm
4.77 + val prop = Thm.prop_of thm
4.78 val tycheck = cterm_of thy
4.79 val vlist = map tycheck (add_term_vars (prop, []))
4.80 in GENL vlist thm
4.81 @@ -352,18 +355,21 @@
4.82 let
4.83 val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
4.84 val redex = D.capply lam fvar
4.85 - val {thy, t = t$u,...} = Thm.rep_cterm redex
4.86 + val thy = Thm.theory_of_cterm redex
4.87 + val t$u = Thm.term_of redex
4.88 val residue = Thm.cterm_of thy (Term.betapply (t, u))
4.89 in
4.90 GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
4.91 handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
4.92 end;
4.93
4.94 -local val {prop,thy,...} = rep_thm exI
4.95 +local val thy = Thm.theory_of_thm exI
4.96 + val prop = Thm.prop_of exI
4.97 val [P,x] = term_vars prop
4.98 in
4.99 fun EXISTS (template,witness) thm =
4.100 - let val {prop,thy,...} = rep_thm thm
4.101 + let val thy = Thm.theory_of_thm thm
4.102 + val prop = Thm.prop_of thm
4.103 val P' = cterm_of thy P
4.104 val x' = cterm_of thy x
4.105 val abstr = #2 (D.dest_comb template)
4.106 @@ -396,16 +402,15 @@
4.107 (* Could be improved, but needs "subst_free" for certified terms *)
4.108
4.109 fun IT_EXISTS blist th =
4.110 - let val {thy,...} = rep_thm th
4.111 + let val thy = Thm.theory_of_thm th
4.112 val tych = cterm_of thy
4.113 - val detype = #t o rep_cterm
4.114 - val blist' = map (fn (x,y) => (detype x, detype y)) blist
4.115 + val blist' = map (pairself Thm.term_of) blist
4.116 fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
4.117
4.118 in
4.119 fold_rev (fn (b as (r1,r2)) => fn thm =>
4.120 EXISTS(ex r2 (subst_free [b]
4.121 - (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1)
4.122 + (HOLogic.dest_Trueprop(Thm.prop_of thm))), tych r1)
4.123 thm)
4.124 blist' th
4.125 end;
4.126 @@ -451,13 +456,10 @@
4.127
4.128 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
4.129 fun is_cong thm =
4.130 - let val {prop, ...} = rep_thm thm
4.131 - in case prop
4.132 + case (Thm.prop_of thm)
4.133 of (Const("==>",_)$(Const("Trueprop",_)$ _) $
4.134 (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false
4.135 - | _ => true
4.136 - end;
4.137 -
4.138 + | _ => true;
4.139
4.140
4.141 fun dest_equal(Const ("==",_) $
4.142 @@ -521,9 +523,9 @@
4.143
4.144 (* Note: rename_params_rule counts from 1, not 0 *)
4.145 fun rename thm =
4.146 - let val {prop,thy,...} = rep_thm thm
4.147 + let val thy = Thm.theory_of_thm thm
4.148 val tych = cterm_of thy
4.149 - val ants = Logic.strip_imp_prems prop
4.150 + val ants = Logic.strip_imp_prems (Thm.prop_of thm)
4.151 val news = get (ants,1,[])
4.152 in
4.153 fold rename_params_rule news thm
4.154 @@ -745,12 +747,12 @@
4.155 end end
4.156
4.157 fun eliminate thm =
4.158 - case (rep_thm thm)
4.159 - of {prop = (Const("==>",_) $ imp $ _), thy, ...} =>
4.160 + case Thm.prop_of thm
4.161 + of Const("==>",_) $ imp $ _ =>
4.162 eliminate
4.163 (if not(is_all imp)
4.164 - then uq_eliminate (thm,imp,thy)
4.165 - else q_eliminate (thm,imp,thy))
4.166 + then uq_eliminate (thm, imp, Thm.theory_of_thm thm)
4.167 + else q_eliminate (thm, imp, Thm.theory_of_thm thm))
4.168 (* Assume that the leading constant is ==, *)
4.169 | _ => thm (* if it is not a ==> *)
4.170 in SOME(eliminate (rename thm)) end
4.171 @@ -760,8 +762,8 @@
4.172 let val dummy = say "restrict_prover:"
4.173 val cntxt = rev(MetaSimplifier.prems_of_ss ss)
4.174 val dummy = print_thms "cntxt:" cntxt
4.175 - val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
4.176 - thy,...} = rep_thm thm
4.177 + val thy = Thm.theory_of_thm thm
4.178 + val Const("==>",_) $ (Const("Trueprop",_) $ A) $ _ = Thm.prop_of thm
4.179 fun genl tm = let val vlist = subtract (op aconv) globals
4.180 (add_term_frees(tm,[]))
4.181 in fold_rev Forall vlist tm
4.182 @@ -814,7 +816,8 @@
4.183
4.184 fun prove strict (ptm, tac) =
4.185 let
4.186 - val {thy, t, ...} = Thm.rep_cterm ptm;
4.187 + val thy = Thm.theory_of_cterm ptm;
4.188 + val t = Thm.term_of ptm;
4.189 val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
4.190 in
4.191 if strict then Goal.prove ctxt [] [] t (K tac)
5.1 --- a/src/HOL/Tools/datatype_realizer.ML Thu Apr 10 20:54:18 2008 +0200
5.2 +++ b/src/HOL/Tools/datatype_realizer.ML Sat Apr 12 17:00:35 2008 +0200
5.3 @@ -27,8 +27,7 @@
5.4 in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
5.5
5.6 fun prf_of thm =
5.7 - let val {thy, prop, der = (_, prf), ...} = rep_thm thm
5.8 - in Reconstruct.reconstruct_proof thy prop prf end;
5.9 + Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
5.10
5.11 fun prf_subst_vars inst =
5.12 Proofterm.map_proof_terms (subst_vars ([], inst)) I;
6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 10 20:54:18 2008 +0200
6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sat Apr 12 17:00:35 2008 +0200
6.3 @@ -359,7 +359,8 @@
6.4
6.5 fun mk_funs_inv thm =
6.6 let
6.7 - val {thy, prop, ...} = rep_thm thm;
6.8 + val thy = Thm.theory_of_thm thm;
6.9 + val prop = Thm.prop_of thm;
6.10 val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
6.11 (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
6.12 val used = add_term_tfree_names (a, []);
7.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Apr 10 20:54:18 2008 +0200
7.2 +++ b/src/HOL/Tools/inductive_realizer.ML Sat Apr 12 17:00:35 2008 +0200
7.3 @@ -24,8 +24,10 @@
7.4 val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
7.5
7.6 fun prf_of thm =
7.7 - let val {thy, prop, der = (_, prf), ...} = rep_thm thm
7.8 - in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
7.9 + let
7.10 + val thy = Thm.theory_of_thm thm;
7.11 + val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
7.12 + in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
7.13
7.14 fun forall_intr_prf (t, prf) =
7.15 let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
8.1 --- a/src/HOL/Tools/record_package.ML Thu Apr 10 20:54:18 2008 +0200
8.2 +++ b/src/HOL/Tools/record_package.ML Sat Apr 12 17:00:35 2008 +0200
8.3 @@ -1740,7 +1740,8 @@
8.4
8.5 fun meta_to_obj_all thm =
8.6 let
8.7 - val {thy, prop, ...} = rep_thm thm;
8.8 + val thy = Thm.theory_of_thm thm;
8.9 + val prop = Thm.prop_of thm;
8.10 val params = Logic.strip_params prop;
8.11 val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
8.12 val ct = cterm_of thy
9.1 --- a/src/HOLCF/Tools/adm_tac.ML Thu Apr 10 20:54:18 2008 +0200
9.2 +++ b/src/HOLCF/Tools/adm_tac.ML Sat Apr 12 17:00:35 2008 +0200
9.3 @@ -110,8 +110,9 @@
9.4 (*** instantiation of adm_subst theorem (a bit tricky) ***)
9.5
9.6 fun inst_adm_subst_thm state i params s T subt t paths =
9.7 - let val {thy = sign, maxidx, ...} = rep_thm state;
9.8 - val j = maxidx+1;
9.9 + let
9.10 + val sign = Thm.theory_of_thm state;
9.11 + val j = Thm.maxidx_of state + 1;
9.12 val parTs = map snd (rev params);
9.13 val rule = Thm.lift_rule (Thm.cprem_of state i) @{thm adm_subst};
9.14 val types = valOf o (fst (types_sorts rule));
10.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 10 20:54:18 2008 +0200
10.2 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 12 17:00:35 2008 +0200
10.3 @@ -564,7 +564,8 @@
10.4 NONE =>
10.5 let
10.6 val (ctxt, (_, thm)) = Proof.get_goal state;
10.7 - val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
10.8 + val thy = ProofContext.theory_of ctxt;
10.9 + val prf = Thm.proof_of thm;
10.10 val prop = Thm.full_prop_of thm;
10.11 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
10.12 in
11.1 --- a/src/Pure/Proof/extraction.ML Thu Apr 10 20:54:18 2008 +0200
11.2 +++ b/src/Pure/Proof/extraction.ML Sat Apr 12 17:00:35 2008 +0200
11.3 @@ -711,7 +711,9 @@
11.4
11.5 fun prep_thm (thm, vs) =
11.6 let
11.7 - val {prop, der = (_, prf), thy, ...} = rep_thm thm;
11.8 + val thy = Thm.theory_of_thm thm;
11.9 + val prop = Thm.prop_of thm;
11.10 + val prf = Thm.proof_of thm;
11.11 val name = Thm.get_name thm;
11.12 val _ = name <> "" orelse error "extraction: unnamed theorem";
11.13 val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
12.1 --- a/src/Pure/Proof/proof_syntax.ML Thu Apr 10 20:54:18 2008 +0200
12.2 +++ b/src/Pure/Proof/proof_syntax.ML Sat Apr 12 17:00:35 2008 +0200
12.3 @@ -259,8 +259,9 @@
12.4
12.5 fun proof_of full thm =
12.6 let
12.7 - val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
12.8 + val thy = Thm.theory_of_thm thm;
12.9 val prop = Thm.full_prop_of thm;
12.10 + val prf = Thm.proof_of thm;
12.11 val prf' = (case strip_combt (fst (strip_combP prf)) of
12.12 (PThm (_, prf', prop', _), _) => if prop = prop' then prf' else prf
12.13 | _ => prf)
13.1 --- a/src/Pure/codegen.ML Thu Apr 10 20:54:18 2008 +0200
13.2 +++ b/src/Pure/codegen.ML Sat Apr 12 17:00:35 2008 +0200
13.3 @@ -1074,8 +1074,8 @@
13.4 Logic.mk_equals (t, eval_term thy t);
13.5
13.6 fun evaluation_conv ct =
13.7 - let val {thy, t, ...} = rep_cterm ct
13.8 - in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
13.9 + let val thy = Thm.theory_of_cterm ct
13.10 + in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation (Thm.term_of ct)) end;
13.11
13.12 val _ = Context.>> (Context.map_theory
13.13 (Theory.add_oracle ("evaluation", evaluation_oracle)));
14.1 --- a/src/Pure/display.ML Thu Apr 10 20:54:18 2008 +0200
14.2 +++ b/src/Pure/display.ML Sat Apr 12 17:00:35 2008 +0200
14.3 @@ -109,20 +109,12 @@
14.4
14.5 (* other printing commands *)
14.6
14.7 -fun pretty_ctyp cT =
14.8 - let val {thy, T, ...} = rep_ctyp cT in Sign.pretty_typ thy T end;
14.9 -
14.10 -fun string_of_ctyp cT =
14.11 - let val {thy, T, ...} = rep_ctyp cT in Sign.string_of_typ thy T end;
14.12 -
14.13 +fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
14.14 +fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
14.15 val print_ctyp = writeln o string_of_ctyp;
14.16
14.17 -fun pretty_cterm ct =
14.18 - let val {thy, t, ...} = rep_cterm ct in Sign.pretty_term thy t end;
14.19 -
14.20 -fun string_of_cterm ct =
14.21 - let val {thy, t, ...} = rep_cterm ct in Sign.string_of_term thy t end;
14.22 -
14.23 +fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
14.24 +fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
14.25 val print_cterm = writeln o string_of_cterm;
14.26
14.27
15.1 --- a/src/Pure/meta_simplifier.ML Thu Apr 10 20:54:18 2008 +0200
15.2 +++ b/src/Pure/meta_simplifier.ML Sat Apr 12 17:00:35 2008 +0200
15.3 @@ -458,7 +458,8 @@
15.4
15.5 fun decomp_simp thm =
15.6 let
15.7 - val {thy, prop, ...} = Thm.rep_thm thm;
15.8 + val thy = Thm.theory_of_thm thm;
15.9 + val prop = Thm.prop_of thm;
15.10 val prems = Logic.strip_imp_prems prop;
15.11 val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
15.12 val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
15.13 @@ -833,7 +834,10 @@
15.14 (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
15.15 in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
15.16 handle THM _ =>
15.17 - let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
15.18 + let
15.19 + val thy = Thm.theory_of_thm thm;
15.20 + val _ $ _ $ prop0 = Thm.prop_of thm;
15.21 + in
15.22 trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
15.23 trace_term false (fn () => "Should have proved:") ss thy prop0;
15.24 NONE
15.25 @@ -897,7 +901,8 @@
15.26 val eta_t = term_of eta_t';
15.27 fun rew {thm, name, lhs, elhs, extra, fo, perm} =
15.28 let
15.29 - val {thy, prop, maxidx, ...} = rep_thm thm;
15.30 + val thy = Thm.theory_of_thm thm;
15.31 + val {prop, maxidx, ...} = rep_thm thm;
15.32 val (rthm, elhs') =
15.33 if maxt = ~1 orelse not extra then (thm, elhs)
15.34 else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
15.35 @@ -1233,8 +1238,9 @@
15.36
15.37 fun rewrite_cterm mode prover raw_ss raw_ct =
15.38 let
15.39 + val thy = Thm.theory_of_cterm raw_ct;
15.40 val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
15.41 - val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
15.42 + val {t, maxidx, ...} = Thm.rep_cterm ct;
15.43 val ss = inc_simp_depth (activate_context thy raw_ss);
15.44 val depth = simp_depth ss;
15.45 val _ =
16.1 --- a/src/Pure/old_goals.ML Thu Apr 10 20:54:18 2008 +0200
16.2 +++ b/src/Pure/old_goals.ML Sat Apr 12 17:00:35 2008 +0200
16.3 @@ -151,7 +151,8 @@
16.4 fun prepare_proof atomic rths chorn =
16.5 let
16.6 val _ = legacy_feature "Old goal command";
16.7 - val {thy, t=horn,...} = rep_cterm chorn;
16.8 + val thy = Thm.theory_of_cterm chorn;
16.9 + val horn = Thm.term_of chorn;
16.10 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
16.11 val (As, B) = Logic.strip_horn horn;
16.12 val atoms = atomic andalso
16.13 @@ -170,7 +171,8 @@
16.14 val ngoals = nprems_of state
16.15 val ath = implies_intr_list cAs state
16.16 val th = Goal.conclude ath
16.17 - val {hyps,prop,thy=thy',...} = rep_thm th
16.18 + val thy' = Thm.theory_of_thm th
16.19 + val {hyps, prop, ...} = Thm.rep_thm th
16.20 val final_th = standard th
16.21 in if not check then final_th
16.22 else if not (eq_thy(thy,thy')) then !result_error_fn state
16.23 @@ -229,7 +231,7 @@
16.24 SOME(st,_) => st
16.25 | _ => error ("prove_goal: tactic failed"))
16.26 in mkresult (check, cond_timeit (!Output.timing) "" statef) end
16.27 - handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
16.28 + handle e => (print_sign_exn_unit (Thm.theory_of_cterm chorn) e;
16.29 writeln ("The exception above was raised for\n" ^
16.30 Display.string_of_cterm chorn); raise e);
16.31
17.1 --- a/src/Pure/pure_thy.ML Thu Apr 10 20:54:18 2008 +0200
17.2 +++ b/src/Pure/pure_thy.ML Sat Apr 12 17:00:35 2008 +0200
17.3 @@ -337,7 +337,8 @@
17.4
17.5 fun forall_elim_vars_aux strip_vars i th =
17.6 let
17.7 - val {thy, tpairs, prop, ...} = Thm.rep_thm th;
17.8 + val thy = Thm.theory_of_thm th;
17.9 + val {tpairs, prop, ...} = Thm.rep_thm th;
17.10 val add_used = Term.fold_aterms
17.11 (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
17.12 val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
18.1 --- a/src/Pure/tactic.ML Thu Apr 10 20:54:18 2008 +0200
18.2 +++ b/src/Pure/tactic.ML Sat Apr 12 17:00:35 2008 +0200
18.3 @@ -263,15 +263,19 @@
18.4 i.e. Tinsts is not applied to insts.
18.5 *)
18.6 fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
18.7 -let val {maxidx,thy,...} = rep_thm st
18.8 +let
18.9 + val thy = Thm.theory_of_thm st
18.10 + val cert = Thm.cterm_of thy
18.11 + val certT = Thm.ctyp_of thy
18.12 + val maxidx = Thm.maxidx_of st
18.13 val paramTs = map #2 (params_of_state i st)
18.14 - and inc = maxidx+1
18.15 + val inc = maxidx+1
18.16 fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
18.17 (*lift only Var, not term, which must be lifted already*)
18.18 - fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
18.19 + fun liftpair (v,t) = (cert (liftvar v), cert t)
18.20 fun liftTpair (((a, i), S), T) =
18.21 - (ctyp_of thy (TVar ((a, i + inc), S)),
18.22 - ctyp_of thy (Logic.incr_tvar inc T))
18.23 + (certT (TVar ((a, i + inc), S)),
18.24 + certT (Logic.incr_tvar inc T))
18.25 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
18.26 (Thm.lift_rule (Thm.cprem_of st i) rule)
18.27 end;
19.1 --- a/src/Pure/tctical.ML Thu Apr 10 20:54:18 2008 +0200
19.2 +++ b/src/Pure/tctical.ML Sat Apr 12 17:00:35 2008 +0200
19.3 @@ -425,8 +425,8 @@
19.4
19.5 fun metahyps_aux_tac tacf (prem,gno) state =
19.6 let val (insts,params,hyps,concl) = metahyps_split_prem prem
19.7 - val {thy = sign,maxidx,...} = rep_thm state
19.8 - val cterm = cterm_of sign
19.9 + val maxidx = Thm.maxidx_of state
19.10 + val cterm = Thm.cterm_of (Thm.theory_of_thm state)
19.11 val chyps = map cterm hyps
19.12 val hypths = map assume chyps
19.13 val subprems = map (forall_elim_vars 0) hypths
20.1 --- a/src/Tools/Compute_Oracle/compute.ML Thu Apr 10 20:54:18 2008 +0200
20.2 +++ b/src/Tools/Compute_Oracle/compute.ML Sat Apr 12 17:00:35 2008 +0200
20.3 @@ -43,7 +43,7 @@
20.4
20.5 open Report;
20.6
20.7 -datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
20.8 +datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML
20.9
20.10 (* Terms are mapped to integer codes *)
20.11 structure Encode :>
20.12 @@ -52,10 +52,10 @@
20.13 val empty : encoding
20.14 val insert : term -> encoding -> int * encoding
20.15 val lookup_code : term -> encoding -> int option
20.16 - val lookup_term : int -> encoding -> term option
20.17 + val lookup_term : int -> encoding -> term option
20.18 val remove_code : int -> encoding -> encoding
20.19 val remove_term : term -> encoding -> encoding
20.20 - val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a
20.21 + val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a
20.22 end
20.23 =
20.24 struct
20.25 @@ -66,7 +66,7 @@
20.26
20.27 fun insert t (e as (count, term2int, int2term)) =
20.28 (case Termtab.lookup term2int t of
20.29 - NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
20.30 + NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term))
20.31 | SOME code => (code, e))
20.32
20.33 fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t
20.34 @@ -88,29 +88,29 @@
20.35
20.36 local
20.37 fun make_constant t ty encoding =
20.38 - let
20.39 - val (code, encoding) = Encode.insert t encoding
20.40 - in
20.41 - (encoding, AbstractMachine.Const code)
20.42 - end
20.43 + let
20.44 + val (code, encoding) = Encode.insert t encoding
20.45 + in
20.46 + (encoding, AbstractMachine.Const code)
20.47 + end
20.48 in
20.49
20.50 fun remove_types encoding t =
20.51 case t of
20.52 - Var (_, ty) => make_constant t ty encoding
20.53 + Var (_, ty) => make_constant t ty encoding
20.54 | Free (_, ty) => make_constant t ty encoding
20.55 | Const (_, ty) => make_constant t ty encoding
20.56 | Abs (_, ty, t') =>
20.57 - let val (encoding, t'') = remove_types encoding t' in
20.58 - (encoding, AbstractMachine.Abs t'')
20.59 - end
20.60 + let val (encoding, t'') = remove_types encoding t' in
20.61 + (encoding, AbstractMachine.Abs t'')
20.62 + end
20.63 | a $ b =>
20.64 - let
20.65 - val (encoding, a) = remove_types encoding a
20.66 - val (encoding, b) = remove_types encoding b
20.67 - in
20.68 - (encoding, AbstractMachine.App (a,b))
20.69 - end
20.70 + let
20.71 + val (encoding, a) = remove_types encoding a
20.72 + val (encoding, b) = remove_types encoding b
20.73 + in
20.74 + (encoding, AbstractMachine.App (a,b))
20.75 + end
20.76 | Bound b => (encoding, AbstractMachine.Var b)
20.77 end
20.78
20.79 @@ -123,23 +123,23 @@
20.80 fun infer_types naming encoding =
20.81 let
20.82 fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v))
20.83 - | infer_types _ bounds _ (AbstractMachine.Const code) =
20.84 - let
20.85 - val c = the (Encode.lookup_term code encoding)
20.86 - in
20.87 - (c, type_of c)
20.88 - end
20.89 - | infer_types level bounds _ (AbstractMachine.App (a, b)) =
20.90 - let
20.91 - val (a, aty) = infer_types level bounds NONE a
20.92 - val (adom, arange) =
20.93 + | infer_types _ bounds _ (AbstractMachine.Const code) =
20.94 + let
20.95 + val c = the (Encode.lookup_term code encoding)
20.96 + in
20.97 + (c, type_of c)
20.98 + end
20.99 + | infer_types level bounds _ (AbstractMachine.App (a, b)) =
20.100 + let
20.101 + val (a, aty) = infer_types level bounds NONE a
20.102 + val (adom, arange) =
20.103 case aty of
20.104 Type ("fun", [dom, range]) => (dom, range)
20.105 | _ => sys_error "infer_types: function type expected"
20.106 val (b, bty) = infer_types level bounds (SOME adom) b
20.107 - in
20.108 - (a $ b, arange)
20.109 - end
20.110 + in
20.111 + (a $ b, arange)
20.112 + end
20.113 | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) =
20.114 let
20.115 val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m
20.116 @@ -160,7 +160,7 @@
20.117 end
20.118
20.119 datatype prog =
20.120 - ProgBarras of AM_Interpreter.program
20.121 + ProgBarras of AM_Interpreter.program
20.122 | ProgBarrasC of AM_Compiler.program
20.123 | ProgHaskell of AM_GHC.program
20.124 | ProgSML of AM_SML.program
20.125 @@ -198,26 +198,26 @@
20.126
20.127 fun thm2cthm th =
20.128 let
20.129 - val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
20.130 - val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
20.131 + val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th
20.132 + val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else ()
20.133 in
20.134 - ComputeThm (hyps, shyps, prop)
20.135 + ComputeThm (hyps, shyps, prop)
20.136 end
20.137
20.138 fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths =
20.139 let
20.140 - fun transfer (x:thm) = Thm.transfer thy x
20.141 - val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
20.142 + fun transfer (x:thm) = Thm.transfer thy x
20.143 + val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths
20.144
20.145 fun make_pattern encoding n vars (var as AbstractMachine.Abs _) =
20.146 - raise (Make "no lambda abstractions allowed in pattern")
20.147 - | make_pattern encoding n vars (var as AbstractMachine.Var _) =
20.148 - raise (Make "no bound variables allowed in pattern")
20.149 - | make_pattern encoding n vars (AbstractMachine.Const code) =
20.150 - (case the (Encode.lookup_term code encoding) of
20.151 - Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
20.152 - handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
20.153 - | _ => (n, vars, AbstractMachine.PConst (code, [])))
20.154 + raise (Make "no lambda abstractions allowed in pattern")
20.155 + | make_pattern encoding n vars (var as AbstractMachine.Var _) =
20.156 + raise (Make "no bound variables allowed in pattern")
20.157 + | make_pattern encoding n vars (AbstractMachine.Const code) =
20.158 + (case the (Encode.lookup_term code encoding) of
20.159 + Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar)
20.160 + handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed"))
20.161 + | _ => (n, vars, AbstractMachine.PConst (code, [])))
20.162 | make_pattern encoding n vars (AbstractMachine.App (a, b)) =
20.163 let
20.164 val (n, vars, pa) = make_pattern encoding n vars a
20.165 @@ -232,26 +232,26 @@
20.166
20.167 fun thm2rule (encoding, hyptable, shyptable) th =
20.168 let
20.169 - val (ComputeThm (hyps, shyps, prop)) = th
20.170 - val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
20.171 - val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
20.172 - val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
20.173 + val (ComputeThm (hyps, shyps, prop)) = th
20.174 + val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable
20.175 + val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable
20.176 + val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop)
20.177 val (a, b) = Logic.dest_equals prop
20.178 handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)")
20.179 - val a = Envir.eta_contract a
20.180 - val b = Envir.eta_contract b
20.181 - val prems = map Envir.eta_contract prems
20.182 + val a = Envir.eta_contract a
20.183 + val b = Envir.eta_contract b
20.184 + val prems = map Envir.eta_contract prems
20.185
20.186 val (encoding, left) = remove_types encoding a
20.187 - val (encoding, right) = remove_types encoding b
20.188 + val (encoding, right) = remove_types encoding b
20.189 fun remove_types_of_guard encoding g =
20.190 - (let
20.191 - val (t1, t2) = Logic.dest_equals g
20.192 - val (encoding, t1) = remove_types encoding t1
20.193 - val (encoding, t2) = remove_types encoding t2
20.194 - in
20.195 - (encoding, AbstractMachine.Guard (t1, t2))
20.196 - end handle TERM _ => raise (Make "guards must be meta-level equations"))
20.197 + (let
20.198 + val (t1, t2) = Logic.dest_equals g
20.199 + val (encoding, t1) = remove_types encoding t1
20.200 + val (encoding, t2) = remove_types encoding t2
20.201 + in
20.202 + (encoding, AbstractMachine.Guard (t1, t2))
20.203 + end handle TERM _ => raise (Make "guards must be meta-level equations"))
20.204 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, [])
20.205
20.206 (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule.
20.207 @@ -263,24 +263,24 @@
20.208 AbstractMachine.PVar =>
20.209 raise (Make "patterns may not start with a variable")
20.210 (* | AbstractMachine.PConst (_, []) =>
20.211 - (print th; raise (Make "no parameter rewrite found"))*)
20.212 - | _ => ())
20.213 + (print th; raise (Make "no parameter rewrite found"))*)
20.214 + | _ => ())
20.215
20.216 (* finally, provide a function for renaming the
20.217 pattern bound variables on the right hand side *)
20.218
20.219 fun rename level vars (var as AbstractMachine.Var _) = var
20.220 - | rename level vars (c as AbstractMachine.Const code) =
20.221 - (case Inttab.lookup vars code of
20.222 - NONE => c
20.223 - | SOME n => AbstractMachine.Var (vcount-n-1+level))
20.224 + | rename level vars (c as AbstractMachine.Const code) =
20.225 + (case Inttab.lookup vars code of
20.226 + NONE => c
20.227 + | SOME n => AbstractMachine.Var (vcount-n-1+level))
20.228 | rename level vars (AbstractMachine.App (a, b)) =
20.229 AbstractMachine.App (rename level vars a, rename level vars b)
20.230 | rename level vars (AbstractMachine.Abs m) =
20.231 AbstractMachine.Abs (rename (level+1) vars m)
20.232 -
20.233 - fun rename_guard (AbstractMachine.Guard (a,b)) =
20.234 - AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
20.235 +
20.236 + fun rename_guard (AbstractMachine.Guard (a,b)) =
20.237 + AbstractMachine.Guard (rename 0 vars a, rename 0 vars b)
20.238 in
20.239 ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right))
20.240 end
20.241 @@ -293,35 +293,35 @@
20.242 ths ((encoding, Termtab.empty, Sorttab.empty), [])
20.243
20.244 fun make_cache_pattern t (encoding, cache_patterns) =
20.245 - let
20.246 - val (encoding, a) = remove_types encoding t
20.247 - val (_,_,p) = make_pattern encoding 0 Inttab.empty a
20.248 - in
20.249 - (encoding, p::cache_patterns)
20.250 - end
20.251 -
20.252 - val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
20.253 + let
20.254 + val (encoding, a) = remove_types encoding t
20.255 + val (_,_,p) = make_pattern encoding 0 Inttab.empty a
20.256 + in
20.257 + (encoding, p::cache_patterns)
20.258 + end
20.259 +
20.260 + val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, [])
20.261
20.262 - fun arity (Type ("fun", [a,b])) = 1 + arity b
20.263 - | arity _ = 0
20.264 + fun arity (Type ("fun", [a,b])) = 1 + arity b
20.265 + | arity _ = 0
20.266
20.267 - fun make_arity (Const (s, _), i) tab =
20.268 - (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
20.269 - | make_arity _ tab = tab
20.270 + fun make_arity (Const (s, _), i) tab =
20.271 + (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab)
20.272 + | make_arity _ tab = tab
20.273
20.274 - val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
20.275 - fun const_arity x = Inttab.lookup const_arity_tab x
20.276 + val const_arity_tab = Encode.fold make_arity encoding Inttab.empty
20.277 + fun const_arity x = Inttab.lookup const_arity_tab x
20.278
20.279 val prog =
20.280 - case machine of
20.281 - BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
20.282 - | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
20.283 - | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
20.284 - | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
20.285 + case machine of
20.286 + BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules)
20.287 + | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules)
20.288 + | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules)
20.289 + | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules)
20.290
20.291 fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
20.292
20.293 - val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
20.294 + val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable
20.295
20.296 in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end
20.297
20.298 @@ -331,32 +331,32 @@
20.299
20.300 fun update_with_cache computer cache_patterns raw_thms =
20.301 let
20.302 - val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer)
20.303 - (encoding_of computer) cache_patterns raw_thms
20.304 - val _ = (ref_of computer) := SOME c
20.305 + val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer)
20.306 + (encoding_of computer) cache_patterns raw_thms
20.307 + val _ = (ref_of computer) := SOME c
20.308 in
20.309 - ()
20.310 + ()
20.311 end
20.312
20.313 fun update computer raw_thms = update_with_cache computer [] raw_thms
20.314
20.315 fun discard computer =
20.316 let
20.317 - val _ =
20.318 - case prog_of computer of
20.319 - ProgBarras p => AM_Interpreter.discard p
20.320 - | ProgBarrasC p => AM_Compiler.discard p
20.321 - | ProgHaskell p => AM_GHC.discard p
20.322 - | ProgSML p => AM_SML.discard p
20.323 - val _ = (ref_of computer) := NONE
20.324 + val _ =
20.325 + case prog_of computer of
20.326 + ProgBarras p => AM_Interpreter.discard p
20.327 + | ProgBarrasC p => AM_Compiler.discard p
20.328 + | ProgHaskell p => AM_GHC.discard p
20.329 + | ProgSML p => AM_SML.discard p
20.330 + val _ = (ref_of computer) := NONE
20.331 in
20.332 - ()
20.333 + ()
20.334 end
20.335 -
20.336 +
20.337 fun runprog (ProgBarras p) = AM_Interpreter.run p
20.338 | runprog (ProgBarrasC p) = AM_Compiler.run p
20.339 | runprog (ProgHaskell p) = AM_GHC.run p
20.340 - | runprog (ProgSML p) = AM_SML.run p
20.341 + | runprog (ProgSML p) = AM_SML.run p
20.342
20.343 (* ------------------------------------------------------------------------------------- *)
20.344 (* An oracle for exporting theorems; must only be accessible from inside this structure! *)
20.345 @@ -377,15 +377,15 @@
20.346
20.347 fun export_oracle (thy, ExportThm (hyps, shyps, prop)) =
20.348 let
20.349 - val shyptab = add_shyps shyps Sorttab.empty
20.350 - fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
20.351 - fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
20.352 - fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
20.353 - val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
20.354 - val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
20.355 - val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
20.356 + val shyptab = add_shyps shyps Sorttab.empty
20.357 + fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
20.358 + fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
20.359 + fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))
20.360 + val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab
20.361 + val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab)
20.362 + val _ = if not (null shyps) then raise Compute ("dangling sort hypotheses: "^(makestring shyps)) else ()
20.363 in
20.364 - fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
20.365 + fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop
20.366 end
20.367 | export_oracle _ = raise Match
20.368
20.369 @@ -393,24 +393,25 @@
20.370
20.371 fun export_thm thy hyps shyps prop =
20.372 let
20.373 - val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
20.374 - val hyps = map (fn h => assume (cterm_of thy h)) hyps
20.375 + val th = invoke_oracle_i thy "Compute_Oracle.compute" (thy, ExportThm (hyps, shyps, prop))
20.376 + val hyps = map (fn h => assume (cterm_of thy h)) hyps
20.377 in
20.378 - fold (fn h => fn p => implies_elim p h) hyps th
20.379 + fold (fn h => fn p => implies_elim p h) hyps th
20.380 end
20.381 -
20.382 +
20.383 (* --------- Rewrite ----------- *)
20.384
20.385 fun rewrite computer ct =
20.386 let
20.387 - val {t=t',T=ty,thy=thy,...} = rep_cterm ct
20.388 - val _ = Theory.assert_super (theory_of computer) thy
20.389 - val naming = naming_of computer
20.390 + val thy = Thm.theory_of_cterm ct
20.391 + val {t=t',T=ty,...} = rep_cterm ct
20.392 + val _ = Theory.assert_super (theory_of computer) thy
20.393 + val naming = naming_of computer
20.394 val (encoding, t) = remove_types (encoding_of computer) t'
20.395 - (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
20.396 + (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*)
20.397 val t = runprog (prog_of computer) t
20.398 val t = infer_types naming encoding ty t
20.399 - val eq = Logic.mk_equals (t', t)
20.400 + val eq = Logic.mk_equals (t', t)
20.401 in
20.402 export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq
20.403 end
20.404 @@ -418,7 +419,7 @@
20.405 (* --------- Simplify ------------ *)
20.406
20.407 datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int
20.408 - | Prem of AbstractMachine.term
20.409 + | Prem of AbstractMachine.term
20.410 datatype theorem = Theorem of theory_ref * unit ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table
20.411 * prem list * AbstractMachine.term * term list * sort list
20.412
20.413 @@ -439,46 +440,46 @@
20.414 | collect_vars (Const _) tab = tab
20.415 | collect_vars (Free _) tab = tab
20.416 | collect_vars (Var ((s, i), ty)) tab =
20.417 - if List.find (fn x => x=s) vars = NONE then
20.418 - tab
20.419 - else
20.420 - (case Symtab.lookup tab s of
20.421 - SOME ((s',i'),ty') =>
20.422 - if s' <> s orelse i' <> i orelse ty <> ty' then
20.423 - raise Compute ("make_theorem: variable name '"^s^"' is not unique")
20.424 - else
20.425 - tab
20.426 - | NONE => Symtab.update (s, ((s, i), ty)) tab)
20.427 + if List.find (fn x => x=s) vars = NONE then
20.428 + tab
20.429 + else
20.430 + (case Symtab.lookup tab s of
20.431 + SOME ((s',i'),ty') =>
20.432 + if s' <> s orelse i' <> i orelse ty <> ty' then
20.433 + raise Compute ("make_theorem: variable name '"^s^"' is not unique")
20.434 + else
20.435 + tab
20.436 + | NONE => Symtab.update (s, ((s, i), ty)) tab)
20.437 val vartab = collect_vars prop Symtab.empty
20.438 fun encodevar (s, t as (_, ty)) (encoding, tab) =
20.439 - let
20.440 - val (x, encoding) = Encode.insert (Var t) encoding
20.441 - in
20.442 - (encoding, Symtab.update (s, (x, ty)) tab)
20.443 - end
20.444 - val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)
20.445 + let
20.446 + val (x, encoding) = Encode.insert (Var t) encoding
20.447 + in
20.448 + (encoding, Symtab.update (s, (x, ty)) tab)
20.449 + end
20.450 + val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty)
20.451 val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab))
20.452
20.453 (* make the premises and the conclusion *)
20.454 fun mk_prem encoding t =
20.455 - (let
20.456 - val (a, b) = Logic.dest_equals t
20.457 - val ty = type_of a
20.458 - val (encoding, a) = remove_types encoding a
20.459 - val (encoding, b) = remove_types encoding b
20.460 - val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding
20.461 - in
20.462 - (encoding, EqPrem (a, b, ty, eq))
20.463 - end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
20.464 + (let
20.465 + val (a, b) = Logic.dest_equals t
20.466 + val ty = type_of a
20.467 + val (encoding, a) = remove_types encoding a
20.468 + val (encoding, b) = remove_types encoding b
20.469 + val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding
20.470 + in
20.471 + (encoding, EqPrem (a, b, ty, eq))
20.472 + end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end)
20.473 val (encoding, prems) =
20.474 - (fold_rev (fn t => fn (encoding, l) =>
20.475 - case mk_prem encoding t of
20.476 + (fold_rev (fn t => fn (encoding, l) =>
20.477 + case mk_prem encoding t of
20.478 (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, []))
20.479 val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop)
20.480 val _ = set_encoding computer encoding
20.481 in
20.482 Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst,
20.483 - prems, concl, hyps, shyps)
20.484 + prems, concl, hyps, shyps)
20.485 end
20.486
20.487 fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy
20.488 @@ -498,7 +499,7 @@
20.489
20.490 fun check_compatible computer th s =
20.491 if stamp_of computer <> stamp_of_theorem th then
20.492 - raise Compute (s^": computer and theorem are incompatible")
20.493 + raise Compute (s^": computer and theorem are incompatible")
20.494 else ()
20.495
20.496 fun instantiate computer insts th =
20.497 @@ -511,49 +512,49 @@
20.498
20.499 fun rewrite computer t =
20.500 let
20.501 - val naming = naming_of computer
20.502 + val naming = naming_of computer
20.503 val (encoding, t) = remove_types (encoding_of computer) t
20.504 val t = runprog (prog_of computer) t
20.505 - val _ = set_encoding computer encoding
20.506 + val _ = set_encoding computer encoding
20.507 in
20.508 t
20.509 end
20.510
20.511 fun assert_varfree vs t =
20.512 - if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
20.513 - ()
20.514 - else
20.515 - raise Compute "instantiate: assert_varfree failed"
20.516 + if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then
20.517 + ()
20.518 + else
20.519 + raise Compute "instantiate: assert_varfree failed"
20.520
20.521 fun assert_closed t =
20.522 - if AbstractMachine.closed t then
20.523 - ()
20.524 - else
20.525 - raise Compute "instantiate: not a closed term"
20.526 + if AbstractMachine.closed t then
20.527 + ()
20.528 + else
20.529 + raise Compute "instantiate: not a closed term"
20.530
20.531 fun compute_inst (s, ct) vs =
20.532 - let
20.533 - val _ = Theory.assert_super (theory_of_cterm ct) thy
20.534 - val ty = typ_of (ctyp_of_term ct)
20.535 - in
20.536 - (case Symtab.lookup vartab s of
20.537 - NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
20.538 - | SOME (x, ty') =>
20.539 - (case Inttab.lookup vs x of
20.540 - SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
20.541 - | SOME NONE =>
20.542 - if ty <> ty' then
20.543 - raise Compute ("instantiate: wrong type for variable '"^s^"'")
20.544 - else
20.545 - let
20.546 - val t = rewrite computer (term_of ct)
20.547 - val _ = assert_varfree vs t
20.548 - val _ = assert_closed t
20.549 - in
20.550 - Inttab.update (x, SOME t) vs
20.551 - end
20.552 - | NONE => raise Compute "instantiate: internal error"))
20.553 - end
20.554 + let
20.555 + val _ = Theory.assert_super (theory_of_cterm ct) thy
20.556 + val ty = typ_of (ctyp_of_term ct)
20.557 + in
20.558 + (case Symtab.lookup vartab s of
20.559 + NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem")
20.560 + | SOME (x, ty') =>
20.561 + (case Inttab.lookup vs x of
20.562 + SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated")
20.563 + | SOME NONE =>
20.564 + if ty <> ty' then
20.565 + raise Compute ("instantiate: wrong type for variable '"^s^"'")
20.566 + else
20.567 + let
20.568 + val t = rewrite computer (term_of ct)
20.569 + val _ = assert_varfree vs t
20.570 + val _ = assert_closed t
20.571 + in
20.572 + Inttab.update (x, SOME t) vs
20.573 + end
20.574 + | NONE => raise Compute "instantiate: internal error"))
20.575 + end
20.576
20.577 val vs = fold compute_inst insts (varsubst_of_theorem th)
20.578 in
20.579 @@ -561,39 +562,39 @@
20.580 end
20.581
20.582 fun match_aterms subst =
20.583 - let
20.584 - exception no_match
20.585 - open AbstractMachine
20.586 - fun match subst (b as (Const c)) a =
20.587 - if a = b then subst
20.588 - else
20.589 - (case Inttab.lookup subst c of
20.590 - SOME (SOME a') => if a=a' then subst else raise no_match
20.591 - | SOME NONE => if AbstractMachine.closed a then
20.592 - Inttab.update (c, SOME a) subst
20.593 - else raise no_match
20.594 - | NONE => raise no_match)
20.595 - | match subst (b as (Var _)) a = if a=b then subst else raise no_match
20.596 - | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
20.597 - | match subst (Abs u) (Abs u') = match subst u u'
20.598 - | match subst _ _ = raise no_match
20.599 + let
20.600 + exception no_match
20.601 + open AbstractMachine
20.602 + fun match subst (b as (Const c)) a =
20.603 + if a = b then subst
20.604 + else
20.605 + (case Inttab.lookup subst c of
20.606 + SOME (SOME a') => if a=a' then subst else raise no_match
20.607 + | SOME NONE => if AbstractMachine.closed a then
20.608 + Inttab.update (c, SOME a) subst
20.609 + else raise no_match
20.610 + | NONE => raise no_match)
20.611 + | match subst (b as (Var _)) a = if a=b then subst else raise no_match
20.612 + | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v'
20.613 + | match subst (Abs u) (Abs u') = match subst u u'
20.614 + | match subst _ _ = raise no_match
20.615 in
20.616 - fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
20.617 + fn b => fn a => (SOME (match subst b a) handle no_match => NONE)
20.618 end
20.619
20.620 fun apply_subst vars_allowed subst =
20.621 let
20.622 - open AbstractMachine
20.623 - fun app (t as (Const c)) =
20.624 - (case Inttab.lookup subst c of
20.625 - NONE => t
20.626 - | SOME (SOME t) => Computed t
20.627 - | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
20.628 - | app (t as (Var _)) = t
20.629 - | app (App (u, v)) = App (app u, app v)
20.630 - | app (Abs m) = Abs (app m)
20.631 + open AbstractMachine
20.632 + fun app (t as (Const c)) =
20.633 + (case Inttab.lookup subst c of
20.634 + NONE => t
20.635 + | SOME (SOME t) => Computed t
20.636 + | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed")
20.637 + | app (t as (Var _)) = t
20.638 + | app (App (u, v)) = App (app u, app v)
20.639 + | app (Abs m) = Abs (app m)
20.640 in
20.641 - app
20.642 + app
20.643 end
20.644
20.645 fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1)
20.646 @@ -604,27 +605,27 @@
20.647 val prems = prems_of_theorem th
20.648 val varsubst = varsubst_of_theorem th
20.649 fun run vars_allowed t =
20.650 - runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
20.651 + runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
20.652 in
20.653 case List.nth (prems, prem_no) of
20.654 - Prem _ => raise Compute "evaluate_prem: no equality premise"
20.655 - | EqPrem (a, b, ty, _) =>
20.656 - let
20.657 - val a' = run false a
20.658 - val b' = run true b
20.659 - in
20.660 - case match_aterms varsubst b' a' of
20.661 - NONE =>
20.662 - let
20.663 - fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
20.664 - val left = "computed left side: "^(mk a')
20.665 - val right = "computed right side: "^(mk b')
20.666 - in
20.667 - raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
20.668 - end
20.669 - | SOME varsubst =>
20.670 - update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
20.671 - end
20.672 + Prem _ => raise Compute "evaluate_prem: no equality premise"
20.673 + | EqPrem (a, b, ty, _) =>
20.674 + let
20.675 + val a' = run false a
20.676 + val b' = run true b
20.677 + in
20.678 + case match_aterms varsubst b' a' of
20.679 + NONE =>
20.680 + let
20.681 + fun mk s = makestring (infer_types (naming_of computer) (encoding_of computer) ty s)
20.682 + val left = "computed left side: "^(mk a')
20.683 + val right = "computed right side: "^(mk b')
20.684 + in
20.685 + raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n")
20.686 + end
20.687 + | SOME varsubst =>
20.688 + update_prems (splicein prem_no [] prems) (update_varsubst varsubst th)
20.689 + end
20.690 end
20.691
20.692 fun prem2term (Prem t) = t
20.693 @@ -635,33 +636,33 @@
20.694 let
20.695 val _ = check_compatible computer th
20.696 val thy =
20.697 - let
20.698 - val thy1 = theory_of_theorem th
20.699 - val thy2 = theory_of_thm th'
20.700 - in
20.701 - if Context.subthy (thy1, thy2) then thy2
20.702 - else if Context.subthy (thy2, thy1) then thy1 else
20.703 - raise Compute "modus_ponens: theorems are not compatible with each other"
20.704 - end
20.705 + let
20.706 + val thy1 = theory_of_theorem th
20.707 + val thy2 = theory_of_thm th'
20.708 + in
20.709 + if Context.subthy (thy1, thy2) then thy2
20.710 + else if Context.subthy (thy2, thy1) then thy1 else
20.711 + raise Compute "modus_ponens: theorems are not compatible with each other"
20.712 + end
20.713 val th' = make_theorem computer th' []
20.714 val varsubst = varsubst_of_theorem th
20.715 fun run vars_allowed t =
20.716 - runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
20.717 + runprog (prog_of computer) (apply_subst vars_allowed varsubst t)
20.718 val prems = prems_of_theorem th
20.719 val prem = run true (prem2term (List.nth (prems, prem_no)))
20.720 val concl = run false (concl_of_theorem th')
20.721 in
20.722 case match_aterms varsubst prem concl of
20.723 - NONE => raise Compute "modus_ponens: conclusion does not match premise"
20.724 + NONE => raise Compute "modus_ponens: conclusion does not match premise"
20.725 | SOME varsubst =>
20.726 - let
20.727 - val th = update_varsubst varsubst th
20.728 - val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
20.729 - val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
20.730 - val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
20.731 - in
20.732 - update_theory thy th
20.733 - end
20.734 + let
20.735 + val th = update_varsubst varsubst th
20.736 + val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th
20.737 + val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th
20.738 + val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th
20.739 + in
20.740 + update_theory thy th
20.741 + end
20.742 end
20.743
20.744 fun simplify computer th =
21.1 --- a/src/Tools/induct.ML Thu Apr 10 20:54:18 2008 +0200
21.2 +++ b/src/Tools/induct.ML Sat Apr 12 17:00:35 2008 +0200
21.3 @@ -280,10 +280,11 @@
21.4 fun prep_var (x, SOME t) =
21.5 let
21.6 val cx = cert x;
21.7 - val {T = xT, thy, ...} = Thm.rep_cterm cx;
21.8 + val xT = #T (Thm.rep_cterm cx);
21.9 val ct = cert (tune t);
21.10 + val tT = Thm.ctyp_of_term ct;
21.11 in
21.12 - if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
21.13 + if Type.could_unify (Thm.typ_of tT, xT) then SOME (cx, ct)
21.14 else error (Pretty.string_of (Pretty.block
21.15 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
21.16 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
21.17 @@ -432,7 +433,8 @@
21.18
21.19 fun guess_instance rule i st =
21.20 let
21.21 - val {thy, maxidx, ...} = Thm.rep_thm st;
21.22 + val thy = Thm.theory_of_thm st;
21.23 + val maxidx = Thm.maxidx_of st;
21.24 val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*)
21.25 val params = rev (rename_wrt_term goal (Logic.strip_params goal));
21.26 in