src/HOL/Tools/Metis/metis_reconstruct.ML
changeset 40259 c0e34371c2e2
parent 40258 2c0d8fe36c21
child 40261 7a02144874f3
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Oct 29 12:49:05 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
     1.5    val untyped_aconv : term -> term -> bool
     1.6    val replay_one_inference :
     1.7 -    Proof.context -> mode -> (string * term) list
     1.8 +    Proof.context -> mode -> (string * term) list * int Unsynchronized.ref
     1.9      -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    1.10      -> (Metis_Thm.thm * thm) list
    1.11    val discharge_skolem_premises :
    1.12 @@ -93,7 +93,7 @@
    1.13          | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
    1.14  
    1.15  (*Maps metis terms to isabelle terms*)
    1.16 -fun hol_term_from_metis_PT ctxt fol_tm =
    1.17 +fun hol_term_from_metis_PT ctxt new_skolem_var_count fol_tm =
    1.18    let val thy = ProofContext.theory_of ctxt
    1.19        val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
    1.20                                         Metis_Term.toString fol_tm)
    1.21 @@ -126,9 +126,11 @@
    1.22                      val nterms = length ts - ntypes
    1.23                      val tts = map tm_to_tt ts
    1.24                      val tys = types_of (List.take(tts,ntypes))
    1.25 +                    val j = !new_skolem_var_count + 1
    1.26 +                    val _ = new_skolem_var_count := j
    1.27                      val t =
    1.28                        if String.isPrefix new_skolem_const_prefix c then
    1.29 -                        Var (new_skolem_var_from_const c,
    1.30 +                        Var ((new_skolem_var_name_from_const c, j),
    1.31                               Type_Infer.paramify_vars (tl tys ---> hd tys))
    1.32                        else
    1.33                          Const (c, dummyT)
    1.34 @@ -162,7 +164,7 @@
    1.35    end
    1.36  
    1.37  (*Maps fully-typed metis terms to isabelle terms*)
    1.38 -fun hol_term_from_metis_FT ctxt fol_tm =
    1.39 +fun hol_term_from_metis_FT ctxt new_skolem_var_count fol_tm =
    1.40    let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
    1.41                                         Metis_Term.toString fol_tm)
    1.42        fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
    1.43 @@ -193,17 +195,17 @@
    1.44                  SOME v => Free (v, dummyT)
    1.45                | NONE => (trace_msg ctxt (fn () =>
    1.46                                        "hol_term_from_metis_FT bad const: " ^ x);
    1.47 -                         hol_term_from_metis_PT ctxt t))
    1.48 +                         hol_term_from_metis_PT ctxt new_skolem_var_count t))
    1.49          | cvt t = (trace_msg ctxt (fn () =>
    1.50                     "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    1.51 -                   hol_term_from_metis_PT ctxt t)
    1.52 +                   hol_term_from_metis_PT ctxt new_skolem_var_count t)
    1.53    in fol_tm |> cvt end
    1.54  
    1.55  fun hol_term_from_metis FT = hol_term_from_metis_FT
    1.56    | hol_term_from_metis _ = hol_term_from_metis_PT
    1.57  
    1.58 -fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
    1.59 -  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
    1.60 +fun hol_terms_from_metis ctxt mode (old_skolems, new_skolem_var_count) fol_tms =
    1.61 +  let val ts = map (hol_term_from_metis mode ctxt new_skolem_var_count) fol_tms
    1.62        val _ = trace_msg ctxt (fn () => "  calling type inference:")
    1.63        val _ = app (fn t => trace_msg ctxt
    1.64                                       (fn () => Syntax.string_of_term ctxt t)) ts
    1.65 @@ -249,17 +251,18 @@
    1.66        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
    1.67    in  cterm_instantiate substs th  end;
    1.68  
    1.69 -fun assume_inf ctxt mode old_skolems atm =
    1.70 +fun assume_inf ctxt mode skolem_params atm =
    1.71    inst_excluded_middle
    1.72        (ProofContext.theory_of ctxt)
    1.73 -      (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm))
    1.74 +      (singleton (hol_terms_from_metis ctxt mode skolem_params)
    1.75 +                 (Metis_Term.Fn atm))
    1.76  
    1.77  (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
    1.78     to reconstruct them admits new possibilities of errors, e.g. concerning
    1.79     sorts. Instead we try to arrange that new TVars are distinct and that types
    1.80     can be inferred from terms. *)
    1.81  
    1.82 -fun inst_inf ctxt mode old_skolems thpairs fsubst th =
    1.83 +fun inst_inf ctxt mode (old_skolems, new_skolem_var_count) thpairs fsubst th =
    1.84    let val thy = ProofContext.theory_of ctxt
    1.85        val i_th = lookth thpairs th
    1.86        val i_th_vars = Term.add_vars (prop_of i_th) []
    1.87 @@ -267,7 +270,7 @@
    1.88        fun subst_translation (x,y) =
    1.89          let val v = find_var x
    1.90              (* We call "reveal_old_skolem_terms" and "infer_types" below. *)
    1.91 -            val t = hol_term_from_metis mode ctxt y
    1.92 +            val t = hol_term_from_metis mode ctxt new_skolem_var_count y
    1.93          in  SOME (cterm_of thy (Var v), t)  end
    1.94          handle Option.Option =>
    1.95                 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
    1.96 @@ -375,7 +378,7 @@
    1.97  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
    1.98  val select_literal = negate_head oo make_last
    1.99  
   1.100 -fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 =
   1.101 +fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
   1.102    let
   1.103      val thy = ProofContext.theory_of ctxt
   1.104      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   1.105 @@ -390,7 +393,7 @@
   1.106      else
   1.107        let
   1.108          val i_atm =
   1.109 -          singleton (hol_terms_from_fol ctxt mode old_skolems)
   1.110 +          singleton (hol_terms_from_metis ctxt mode skolem_params)
   1.111                      (Metis_Term.Fn atm)
   1.112          val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.113          val prems_th1 = prems_of i_th1
   1.114 @@ -415,9 +418,9 @@
   1.115  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   1.116  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   1.117  
   1.118 -fun refl_inf ctxt mode old_skolems t =
   1.119 +fun refl_inf ctxt mode skolem_params t =
   1.120    let val thy = ProofContext.theory_of ctxt
   1.121 -      val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
   1.122 +      val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
   1.123        val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.124        val c_t = cterm_incr_types thy refl_idx i_t
   1.125    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   1.126 @@ -433,10 +436,10 @@
   1.127    | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
   1.128    | get_ty_arg_size _ _ = 0;
   1.129  
   1.130 -fun equality_inf ctxt mode old_skolems (pos, atm) fp fr =
   1.131 +fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
   1.132    let val thy = ProofContext.theory_of ctxt
   1.133        val m_tm = Metis_Term.Fn atm
   1.134 -      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
   1.135 +      val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
   1.136        val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.137        fun replace_item_list lx 0 (_::ls) = lx::ls
   1.138          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.139 @@ -515,17 +518,17 @@
   1.140  
   1.141  val factor = Seq.hd o distinct_subgoals_tac;
   1.142  
   1.143 -fun step ctxt mode old_skolems thpairs p =
   1.144 +fun step ctxt mode skolem_params thpairs p =
   1.145    case p of
   1.146      (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
   1.147 -  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm
   1.148 +  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
   1.149    | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   1.150 -    factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1)
   1.151 +    factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
   1.152    | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
   1.153 -    factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2)
   1.154 -  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm
   1.155 +    factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
   1.156 +  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
   1.157    | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   1.158 -    equality_inf ctxt mode old_skolems f_lit f_p f_r
   1.159 +    equality_inf ctxt mode skolem_params f_lit f_p f_r
   1.160  
   1.161  fun flexflex_first_order th =
   1.162    case Thm.tpairs_of th of
   1.163 @@ -545,12 +548,12 @@
   1.164  
   1.165  fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
   1.166  
   1.167 -fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   1.168 +fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
   1.169    let
   1.170      val _ = trace_msg ctxt (fn () => "=============================================")
   1.171      val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   1.172      val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   1.173 -    val th = step ctxt mode old_skolems thpairs (fol_th, inf)
   1.174 +    val th = step ctxt mode skolem_params thpairs (fol_th, inf)
   1.175               |> flexflex_first_order
   1.176      val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.177      val _ = trace_msg ctxt (fn () => "=============================================")