# HG changeset patch # User paulson # Date 1187957758 -7200 # Node ID 90500d3b5b5dcf6eea708515e006e5cdb2fbfdfd # Parent ae9cd0e9242351579dce4d6690f012e8c2acf5f7 Reconstruction bug fix diff -r ae9cd0e92423 -r 90500d3b5b5d src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Fri Aug 24 14:14:20 2007 +0200 +++ b/src/HOL/Tools/metis_tools.ML Fri Aug 24 14:15:58 2007 +0200 @@ -17,7 +17,7 @@ structure MetisTools: METIS_TOOLS = struct - structure Rc = ResReconstruct; + structure Recon = ResReconstruct; val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; @@ -163,7 +163,7 @@ let val thy = ProofContext.theory_of ctxt and (types, sorts) = Variable.constraints_of ctxt val declaredT = Consts.the_constraint (Sign.consts_of thy) c - val t = Rc.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts))) + val t = Recon.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts))) in Sign.typ_match thy (declaredT, type_of t) Vartab.empty; t @@ -190,10 +190,10 @@ let val thy = ProofContext.theory_of ctxt val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case Rc.strip_prefix ResClause.tvar_prefix v of - SOME w => Type (Rc.make_tvar w) + (case Recon.strip_prefix ResClause.tvar_prefix v of + SOME w => Type (Recon.make_tvar w) | NONE => - case Rc.strip_prefix ResClause.schematic_var_prefix v of + case Recon.strip_prefix ResClause.schematic_var_prefix v of SOME w => Term (mk_var w) | NONE => Term (mk_var v) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -210,14 +210,14 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case Rc.strip_prefix ResClause.const_prefix a of + case Recon.strip_prefix ResClause.const_prefix a of SOME b => - let val c = Rc.invert_const b - val ntypes = Rc.num_typargs thy c + let val c = Recon.invert_const b + val ntypes = Recon.num_typargs thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = Rc.num_typargs thy c + val ntyargs = Recon.num_typargs thy c in if length tys = ntyargs then apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes)) else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ @@ -228,13 +228,13 @@ space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case Rc.strip_prefix ResClause.tconst_prefix a of - SOME b => Type (Term.Type(Rc.invert_type_const b, types_of (map tm_to_tt ts))) + case Recon.strip_prefix ResClause.tconst_prefix a of + SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case Rc.strip_prefix ResClause.tfree_prefix a of + case Recon.strip_prefix ResClause.tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case Rc.strip_prefix ResClause.fixed_var_prefix a of + case Recon.strip_prefix ResClause.fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -301,9 +301,9 @@ in SOME (cterm_of thy v, t) end handle Option => NONE (*List.find failed for the variable.*) fun remove_typeinst (a, t) = - case Rc.strip_prefix ResClause.schematic_var_prefix a of + case Recon.strip_prefix ResClause.schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case Rc.strip_prefix ResClause.tvar_prefix a of + | NONE => case Recon.strip_prefix ResClause.tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = Output.debug (fn () => " isa th: " ^ string_of_thm i_th) @@ -319,6 +319,18 @@ in cterm_instantiate substs' i_th end; (* INFERENCE RULE: RESOLVE *) + + (*Like RSN, but we rename apart only the type variables. Vars here typically have an index + of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars + could then fail. See comment on mk_var.*) + fun resolve_inc_tyvars(tha,i,thb) = + let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha + val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb) + in + case distinct Thm.eq_thm ths of + [th] => th + | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) + end; fun resolve_inf ctxt thpairs atm th1 th2 = let @@ -341,7 +353,7 @@ val index_th2 = get_index i_atm prems_th2 handle Empty => error "Failed to find literal in th2" val _ = Output.debug (fn () => " index_th2: " ^ Int.toString index_th2) - in (Meson.select_literal index_th1 i_th1) RSN (index_th2, i_th2) end + in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end end; (* INFERENCE RULE: REFL *) @@ -352,7 +364,7 @@ in cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM end; fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const(c,_)) = (Rc.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy (Const(c,_)) = (Recon.num_typargs thy c handle TYPE _ => 0) | get_ty_arg_size thy _ = 0; (* INFERENCE RULE: EQUALITY *) @@ -427,9 +439,9 @@ val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf))) val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th) val _ = Output.debug (fn () => "=============================================") + val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) in - if nprems_of th = - length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) then () + if nprems_of th = n_metis_lits then () else error "Metis: proof reconstruction has gone wrong"; translate isFO ctxt ((fol_th, th) :: thpairs) infpairs end;