src/HOL/Tools/Sledgehammer/metis_translate.ML
changeset 39497 fa16349939b7
parent 39494 bf7dd4902321
child 39499 40bf0f66b994
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Thu Sep 16 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Thu Sep 16 17:30:29 2010 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (*  Title:      HOL/Tools/Sledgehammer/metis_translate.ML
     1.5      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.6 +    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
     1.7 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     1.8      Author:     Jasmin Blanchette, TU Muenchen
     1.9  
    1.10  Translation of HOL to FOL for Metis.
    1.11 @@ -28,6 +30,12 @@
    1.12      CombApp of combterm * combterm
    1.13    datatype fol_literal = FOLLiteral of bool * combterm
    1.14  
    1.15 +  datatype mode = FO | HO | FT
    1.16 +  type logic_map =
    1.17 +    {axioms: (Metis_Thm.thm * thm) list,
    1.18 +     tfrees: type_literal list,
    1.19 +     skolems: (string * term) list}
    1.20 +
    1.21    val type_wrapper_name : string
    1.22    val bound_var_prefix : string
    1.23    val schematic_var_prefix: string
    1.24 @@ -68,6 +76,10 @@
    1.25    val tfree_classes_of_terms : term list -> string list
    1.26    val tvar_classes_of_terms : term list -> string list
    1.27    val type_consts_of_terms : theory -> term list -> string list
    1.28 +  val string_of_mode : mode -> string
    1.29 +  val build_logic_map :
    1.30 +    mode -> Proof.context -> bool -> thm list -> thm list
    1.31 +    -> mode * logic_map
    1.32  end
    1.33  
    1.34  structure Metis_Translate : METIS_TRANSLATE =
    1.35 @@ -369,23 +381,23 @@
    1.36          |   stripc  x =  x
    1.37      in stripc(u,[]) end
    1.38  
    1.39 -fun type_of (Type (a, Ts)) =
    1.40 -    let val (folTypes,ts) = types_of Ts in
    1.41 +fun combtype_of (Type (a, Ts)) =
    1.42 +    let val (folTypes, ts) = combtypes_of Ts in
    1.43        (CombType (`make_fixed_type_const a, folTypes), ts)
    1.44      end
    1.45 -  | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
    1.46 -  | type_of (tp as TVar (x, _)) =
    1.47 +  | combtype_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
    1.48 +  | combtype_of (tp as TVar (x, _)) =
    1.49      (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
    1.50 -and types_of Ts =
    1.51 -    let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
    1.52 -      (folTyps, union_all ts)
    1.53 -    end
    1.54 +and combtypes_of Ts =
    1.55 +  let val (folTyps, ts) = ListPair.unzip (map combtype_of Ts) in
    1.56 +    (folTyps, union_all ts)
    1.57 +  end
    1.58  
    1.59  (* same as above, but no gathering of sort information *)
    1.60 -fun simp_type_of (Type (a, Ts)) =
    1.61 -      CombType (`make_fixed_type_const a, map simp_type_of Ts)
    1.62 -  | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
    1.63 -  | simp_type_of (TVar (x, _)) =
    1.64 +fun simple_combtype_of (Type (a, Ts)) =
    1.65 +    CombType (`make_fixed_type_const a, map simple_combtype_of Ts)
    1.66 +  | simple_combtype_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
    1.67 +  | simple_combtype_of (TVar (x, _)) =
    1.68      CombTVar (make_schematic_type_var x, string_of_indexname x)
    1.69  
    1.70  (* Converts a term (with combinators) into a combterm. Also accummulates sort
    1.71 @@ -396,27 +408,27 @@
    1.72        in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
    1.73    | combterm_from_term thy _ (Const (c, T)) =
    1.74        let
    1.75 -        val (tp, ts) = type_of T
    1.76 +        val (tp, ts) = combtype_of T
    1.77          val tvar_list =
    1.78            (if String.isPrefix skolem_theory_name c then
    1.79               [] |> Term.add_tvarsT T |> map TVar
    1.80             else
    1.81               (c, T) |> Sign.const_typargs thy)
    1.82 -          |> map simp_type_of
    1.83 +          |> map simple_combtype_of
    1.84          val c' = CombConst (`make_fixed_const c, tp, tvar_list)
    1.85        in  (c',ts)  end
    1.86    | combterm_from_term _ _ (Free (v, T)) =
    1.87 -      let val (tp,ts) = type_of T
    1.88 +      let val (tp, ts) = combtype_of T
    1.89            val v' = CombConst (`make_fixed_var v, tp, [])
    1.90        in  (v',ts)  end
    1.91    | combterm_from_term _ _ (Var (v, T)) =
    1.92 -      let val (tp,ts) = type_of T
    1.93 +      let val (tp,ts) = combtype_of T
    1.94            val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
    1.95        in  (v',ts)  end
    1.96    | combterm_from_term _ bs (Bound j) =
    1.97        let
    1.98          val (s, T) = nth bs j
    1.99 -        val (tp, ts) = type_of T
   1.100 +        val (tp, ts) = combtype_of T
   1.101          val v' = CombConst (`make_bound_var s, tp, [])
   1.102        in (v', ts) end
   1.103    | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   1.104 @@ -518,4 +530,226 @@
   1.105  fun type_consts_of_terms thy ts =
   1.106    Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   1.107  
   1.108 +(* ------------------------------------------------------------------------- *)
   1.109 +(* HOL to FOL  (Isabelle to Metis)                                           *)
   1.110 +(* ------------------------------------------------------------------------- *)
   1.111 +
   1.112 +datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
   1.113 +
   1.114 +fun string_of_mode FO = "FO"
   1.115 +  | string_of_mode HO = "HO"
   1.116 +  | string_of_mode FT = "FT"
   1.117 +
   1.118 +fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
   1.119 +  | fn_isa_to_met_sublevel x = x
   1.120 +fun fn_isa_to_met_toplevel "equal" = "="
   1.121 +  | fn_isa_to_met_toplevel x = x
   1.122 +
   1.123 +fun metis_lit b c args = (b, (c, args));
   1.124 +
   1.125 +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
   1.126 +  | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
   1.127 +  | metis_term_from_combtyp (CombType ((s, _), tps)) =
   1.128 +    Metis_Term.Fn (s, map metis_term_from_combtyp tps);
   1.129 +
   1.130 +(*These two functions insert type literals before the real literals. That is the
   1.131 +  opposite order from TPTP linkup, but maybe OK.*)
   1.132 +
   1.133 +fun hol_term_to_fol_FO tm =
   1.134 +  case strip_combterm_comb tm of
   1.135 +      (CombConst ((c, _), _, tys), tms) =>
   1.136 +        let val tyargs = map metis_term_from_combtyp tys
   1.137 +            val args   = map hol_term_to_fol_FO tms
   1.138 +        in Metis_Term.Fn (c, tyargs @ args) end
   1.139 +    | (CombVar ((v, _), _), []) => Metis_Term.Var v
   1.140 +    | _ => raise Fail "non-first-order combterm"
   1.141 +
   1.142 +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
   1.143 +      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
   1.144 +  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
   1.145 +  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
   1.146 +       Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
   1.147 +
   1.148 +(*The fully-typed translation, to avoid type errors*)
   1.149 +fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
   1.150 +
   1.151 +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
   1.152 +  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
   1.153 +      wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
   1.154 +  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
   1.155 +       wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
   1.156 +                  combtyp_of tm)
   1.157 +
   1.158 +fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
   1.159 +      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
   1.160 +          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
   1.161 +          val lits = map hol_term_to_fol_FO tms
   1.162 +      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
   1.163 +  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
   1.164 +     (case strip_combterm_comb tm of
   1.165 +          (CombConst(("equal", _), _, _), tms) =>
   1.166 +            metis_lit pos "=" (map hol_term_to_fol_HO tms)
   1.167 +        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
   1.168 +  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
   1.169 +     (case strip_combterm_comb tm of
   1.170 +          (CombConst(("equal", _), _, _), tms) =>
   1.171 +            metis_lit pos "=" (map hol_term_to_fol_FT tms)
   1.172 +        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
   1.173 +
   1.174 +fun literals_of_hol_term thy mode t =
   1.175 +      let val (lits, types_sorts) = literals_of_term thy t
   1.176 +      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
   1.177 +
   1.178 +(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
   1.179 +fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
   1.180 +    metis_lit pos s [Metis_Term.Var s']
   1.181 +  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
   1.182 +    metis_lit pos s [Metis_Term.Fn (s',[])]
   1.183 +
   1.184 +fun default_sort _ (TVar _) = false
   1.185 +  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
   1.186 +
   1.187 +fun metis_of_tfree tf =
   1.188 +  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
   1.189 +
   1.190 +fun hol_thm_to_fol is_conjecture ctxt type_lits mode j skolems th =
   1.191 +  let
   1.192 +    val thy = ProofContext.theory_of ctxt
   1.193 +    val (skolems, (mlits, types_sorts)) =
   1.194 +     th |> prop_of |> conceal_skolem_terms j skolems
   1.195 +        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
   1.196 +  in
   1.197 +    if is_conjecture then
   1.198 +      (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
   1.199 +       type_literals_for_types types_sorts, skolems)
   1.200 +    else
   1.201 +      let
   1.202 +        val tylits = filter_out (default_sort ctxt) types_sorts
   1.203 +                     |> type_literals_for_types
   1.204 +        val mtylits =
   1.205 +          if type_lits then map (metis_of_type_literals false) tylits else []
   1.206 +      in
   1.207 +        (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
   1.208 +         skolems)
   1.209 +      end
   1.210 +  end;
   1.211 +
   1.212 +val helpers =
   1.213 +  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
   1.214 +   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
   1.215 +   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
   1.216 +   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
   1.217 +   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
   1.218 +   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
   1.219 +                            @{thms fequal_imp_equal equal_imp_fequal})),
   1.220 +   ("c_True", (true, map (`I) @{thms True_or_False})),
   1.221 +   ("c_False", (true, map (`I) @{thms True_or_False})),
   1.222 +   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
   1.223 +
   1.224 +(* ------------------------------------------------------------------------- *)
   1.225 +(* Logic maps manage the interface between HOL and first-order logic.        *)
   1.226 +(* ------------------------------------------------------------------------- *)
   1.227 +
   1.228 +type logic_map =
   1.229 +  {axioms: (Metis_Thm.thm * thm) list,
   1.230 +   tfrees: type_literal list,
   1.231 +   skolems: (string * term) list}
   1.232 +
   1.233 +fun is_quasi_fol_clause thy =
   1.234 +  Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
   1.235 +
   1.236 +(*Extract TFree constraints from context to include as conjecture clauses*)
   1.237 +fun init_tfrees ctxt =
   1.238 +  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
   1.239 +    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
   1.240 +    |> type_literals_for_types
   1.241 +  end;
   1.242 +
   1.243 +(*Insert non-logical axioms corresponding to all accumulated TFrees*)
   1.244 +fun add_tfrees {axioms, tfrees, skolems} : logic_map =
   1.245 +     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
   1.246 +               axioms,
   1.247 +      tfrees = tfrees, skolems = skolems}
   1.248 +
   1.249 +(*transform isabelle type / arity clause to metis clause *)
   1.250 +fun add_type_thm [] lmap = lmap
   1.251 +  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
   1.252 +      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
   1.253 +                        skolems = skolems}
   1.254 +
   1.255 +fun const_in_metis c (pred, tm_list) =
   1.256 +  let
   1.257 +    fun in_mterm (Metis_Term.Var _) = false
   1.258 +      | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
   1.259 +      | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
   1.260 +  in  c = pred orelse exists in_mterm tm_list  end;
   1.261 +
   1.262 +(* ARITY CLAUSE *)
   1.263 +fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
   1.264 +    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
   1.265 +  | m_arity_cls (TVarLit ((c, _), (s, _))) =
   1.266 +    metis_lit false c [Metis_Term.Var s]
   1.267 +(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
   1.268 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
   1.269 +  (TrueI,
   1.270 +   Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
   1.271 +
   1.272 +(* CLASSREL CLAUSE *)
   1.273 +fun m_class_rel_cls (subclass, _) (superclass, _) =
   1.274 +  [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
   1.275 +fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
   1.276 +  (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
   1.277 +
   1.278 +fun type_ext thy tms =
   1.279 +  let val subs = tfree_classes_of_terms tms
   1.280 +      val supers = tvar_classes_of_terms tms
   1.281 +      and tycons = type_consts_of_terms thy tms
   1.282 +      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   1.283 +      val class_rel_clauses = make_class_rel_clauses thy subs supers'
   1.284 +  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
   1.285 +  end;
   1.286 +
   1.287 +(* Function to generate metis clauses, including comb and type clauses *)
   1.288 +fun build_logic_map mode0 ctxt type_lits cls ths =
   1.289 +  let val thy = ProofContext.theory_of ctxt
   1.290 +      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
   1.291 +      fun set_mode FO = FO
   1.292 +        | set_mode HO =
   1.293 +          if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
   1.294 +        | set_mode FT = FT
   1.295 +      val mode = set_mode mode0
   1.296 +      (*transform isabelle clause to metis clause *)
   1.297 +      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
   1.298 +                  : logic_map =
   1.299 +        let
   1.300 +          val (mth, tfree_lits, skolems) =
   1.301 +            hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
   1.302 +                           skolems metis_ith
   1.303 +        in
   1.304 +           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
   1.305 +            tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
   1.306 +        end;
   1.307 +      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
   1.308 +                 |> fold (add_thm true o `I) cls
   1.309 +                 |> add_tfrees
   1.310 +                 |> fold (add_thm false o `I) ths
   1.311 +      val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
   1.312 +      fun is_used c =
   1.313 +        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
   1.314 +      val lmap =
   1.315 +        if mode = FO then
   1.316 +          lmap
   1.317 +        else
   1.318 +          let
   1.319 +            val helper_ths =
   1.320 +              helpers |> filter (is_used o fst)
   1.321 +                      |> maps (fn (c, (needs_full_types, thms)) =>
   1.322 +                                  if not (is_used c) orelse
   1.323 +                                     needs_full_types andalso mode <> FT then
   1.324 +                                    []
   1.325 +                                  else
   1.326 +                                    thms)
   1.327 +          in lmap |> fold (add_thm false) helper_ths end
   1.328 +  in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
   1.329 +
   1.330  end;