Reconstruction bug fix
authorpaulson
Fri Aug 24 14:15:58 2007 +0200 (2007-08-24)
changeset 2442490500d3b5b5d
parent 24423 ae9cd0e92423
child 24425 ca97c6f3d9cd
Reconstruction bug fix
src/HOL/Tools/metis_tools.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Fri Aug 24 14:14:20 2007 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Fri Aug 24 14:15:58 2007 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  structure MetisTools: METIS_TOOLS =
     1.5  struct
     1.6  
     1.7 -  structure Rc = ResReconstruct;
     1.8 +  structure Recon = ResReconstruct;
     1.9  
    1.10    val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
    1.11  
    1.12 @@ -163,7 +163,7 @@
    1.13    let val thy = ProofContext.theory_of ctxt
    1.14        and (types, sorts) = Variable.constraints_of ctxt
    1.15        val declaredT = Consts.the_constraint (Sign.consts_of thy) c
    1.16 -      val t = Rc.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts)))
    1.17 +      val t = Recon.fix_sorts sorts (Const(c, Sign.const_instance thy (c,Ts)))
    1.18    in
    1.19        Sign.typ_match thy (declaredT, type_of t) Vartab.empty;
    1.20        t
    1.21 @@ -190,10 +190,10 @@
    1.22      let val thy = ProofContext.theory_of ctxt
    1.23          val _ = Output.debug (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
    1.24          fun tm_to_tt (Metis.Term.Var v) =
    1.25 -               (case Rc.strip_prefix ResClause.tvar_prefix v of
    1.26 -                    SOME w => Type (Rc.make_tvar w)
    1.27 +               (case Recon.strip_prefix ResClause.tvar_prefix v of
    1.28 +                    SOME w => Type (Recon.make_tvar w)
    1.29                    | NONE =>
    1.30 -                case Rc.strip_prefix ResClause.schematic_var_prefix v of
    1.31 +                case Recon.strip_prefix ResClause.schematic_var_prefix v of
    1.32                      SOME w => Term (mk_var w)
    1.33                    | NONE   => Term (mk_var v) )
    1.34                        (*Var from Metis with a name like _nnn; possibly a type variable*)
    1.35 @@ -210,14 +210,14 @@
    1.36          and applic_to_tt ("=",ts) =
    1.37                Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
    1.38            | applic_to_tt (a,ts) =
    1.39 -              case Rc.strip_prefix ResClause.const_prefix a of
    1.40 +              case Recon.strip_prefix ResClause.const_prefix a of
    1.41                    SOME b =>
    1.42 -                    let val c = Rc.invert_const b
    1.43 -                        val ntypes = Rc.num_typargs thy c
    1.44 +                    let val c = Recon.invert_const b
    1.45 +                        val ntypes = Recon.num_typargs thy c
    1.46                          val nterms = length ts - ntypes
    1.47                          val tts = map tm_to_tt ts
    1.48                          val tys = types_of (List.take(tts,ntypes))
    1.49 -                        val ntyargs = Rc.num_typargs thy c
    1.50 +                        val ntyargs = Recon.num_typargs thy c
    1.51                      in if length tys = ntyargs then
    1.52                             apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes))
    1.53                         else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
    1.54 @@ -228,13 +228,13 @@
    1.55                                     space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
    1.56                         end
    1.57                  | NONE => (*Not a constant. Is it a type constructor?*)
    1.58 -              case Rc.strip_prefix ResClause.tconst_prefix a of
    1.59 -                  SOME b => Type (Term.Type(Rc.invert_type_const b, types_of (map tm_to_tt ts)))
    1.60 +              case Recon.strip_prefix ResClause.tconst_prefix a of
    1.61 +                  SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts)))
    1.62                  | NONE => (*Maybe a TFree. Should then check that ts=[].*)
    1.63 -              case Rc.strip_prefix ResClause.tfree_prefix a of
    1.64 +              case Recon.strip_prefix ResClause.tfree_prefix a of
    1.65                    SOME b => Type (mk_tfree ctxt b)
    1.66                  | NONE => (*a fixed variable? They are Skolem functions.*)
    1.67 -              case Rc.strip_prefix ResClause.fixed_var_prefix a of
    1.68 +              case Recon.strip_prefix ResClause.fixed_var_prefix a of
    1.69                    SOME b =>
    1.70                      let val opr = Term.Free(b, HOLogic.typeT)
    1.71                      in  apply_list opr (length ts) (map tm_to_tt ts)  end
    1.72 @@ -301,9 +301,9 @@
    1.73                in  SOME (cterm_of thy v, t)  end
    1.74                handle Option => NONE (*List.find failed for the variable.*)
    1.75          fun remove_typeinst (a, t) =
    1.76 -              case Rc.strip_prefix ResClause.schematic_var_prefix a of
    1.77 +              case Recon.strip_prefix ResClause.schematic_var_prefix a of
    1.78                    SOME b => SOME (b, t)
    1.79 -                | NONE   => case Rc.strip_prefix ResClause.tvar_prefix a of
    1.80 +                | NONE   => case Recon.strip_prefix ResClause.tvar_prefix a of
    1.81                    SOME _ => NONE          (*type instantiations are forbidden!*)
    1.82                  | NONE   => SOME (a,t)    (*internal Metis var?*)
    1.83          val _ = Output.debug (fn () => "  isa th: " ^ string_of_thm i_th)
    1.84 @@ -319,6 +319,18 @@
    1.85      in  cterm_instantiate substs' i_th  end;
    1.86  
    1.87    (* INFERENCE RULE: RESOLVE *)
    1.88 +  
    1.89 +  (*Like RSN, but we rename apart only the type variables. Vars here typically have an index
    1.90 +    of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
    1.91 +    could then fail. See comment on mk_var.*)
    1.92 +  fun resolve_inc_tyvars(tha,i,thb) =
    1.93 +    let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
    1.94 +	val ths = Seq.list_of (bicompose false (false,tha,nprems_of tha) i thb)
    1.95 +    in  
    1.96 +	case distinct Thm.eq_thm ths of
    1.97 +	  [th] => th
    1.98 +	| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
    1.99 +    end;
   1.100  
   1.101    fun resolve_inf ctxt thpairs atm th1 th2 =
   1.102      let
   1.103 @@ -341,7 +353,7 @@
   1.104            val index_th2 = get_index i_atm prems_th2
   1.105                  handle Empty => error "Failed to find literal in th2"
   1.106            val _ = Output.debug (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.107 -      in  (Meson.select_literal index_th1 i_th1) RSN (index_th2, i_th2)  end
   1.108 +      in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
   1.109      end;
   1.110  
   1.111    (* INFERENCE RULE: REFL *)
   1.112 @@ -352,7 +364,7 @@
   1.113      in  cterm_instantiate [(cterm_of thy v_x, cterm_of thy i_lit)] REFL_THM  end;
   1.114  
   1.115    fun get_ty_arg_size thy (Const("op =",_)) = 0  (*equality has no type arguments*)
   1.116 -    | get_ty_arg_size thy (Const(c,_))      = (Rc.num_typargs thy c handle TYPE _ => 0)
   1.117 +    | get_ty_arg_size thy (Const(c,_))      = (Recon.num_typargs thy c handle TYPE _ => 0)
   1.118      | get_ty_arg_size thy _      = 0;
   1.119  
   1.120    (* INFERENCE RULE: EQUALITY *)
   1.121 @@ -427,9 +439,9 @@
   1.122              val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
   1.123              val _ = Output.debug (fn () => "ISABELLE THM: " ^ string_of_thm th)
   1.124              val _ = Output.debug (fn () => "=============================================")
   1.125 +            val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
   1.126          in
   1.127 -            if nprems_of th =
   1.128 -        length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) then ()
   1.129 +            if nprems_of th = n_metis_lits then ()
   1.130              else error "Metis: proof reconstruction has gone wrong";
   1.131              translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
   1.132          end;