# HG changeset patch # User blanchet # Date 1292408788 -3600 # Node ID cb1cbae54dbf48cee208eb387d04ab52345381fa # Parent eb80538166b6c6c02482decdb48f57a78e5875c1 add Metis support for higher-order propositional reasoning diff -r eb80538166b6 -r cb1cbae54dbf src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Dec 15 11:26:28 2010 +0100 @@ -81,7 +81,13 @@ fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) -fun smart_invert_const "fequal" = @{const_name HOL.eq} +fun smart_invert_const "fFalse" = @{const_name False} + | smart_invert_const "fTrue" = @{const_name True} + | smart_invert_const "fNot" = @{const_name Not} + | smart_invert_const "fconj" = @{const_name conj} + | smart_invert_const "fdisj" = @{const_name disj} + | smart_invert_const "fimplies" = @{const_name implies} + | smart_invert_const "fequal" = @{const_name HOL.eq} | smart_invert_const s = invert_const s fun hol_type_from_metis_term _ (Metis_Term.Var v) = @@ -378,7 +384,8 @@ (* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing double-negations. *) -val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] +val negate_head = + fold (rewrite_rule o single) [@{thm atomize_not}, not_not RS eq_reflection] (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) val select_literal = negate_head oo make_last diff -r eb80538166b6 -r cb1cbae54dbf src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Dec 15 11:26:28 2010 +0100 @@ -82,7 +82,7 @@ structure Metis_Translate : METIS_TRANSLATE = struct -val type_tag_name = "ty" +val type_tag_name = "ti" val bound_var_prefix = "B_" val schematic_var_prefix = "V_" @@ -102,23 +102,30 @@ fun union_all xss = fold (union (op =)) xss [] (* Readable names for the more common symbolic functions. Do not mess with the - last nine entries of the table unless you know what you are doing. *) + table unless you know what you are doing. *) val const_trans_table = Symtab.make [(@{type_name Product_Type.prod}, "prod"), (@{type_name Sum_Type.sum}, "sum"), + (@{const_name False}, "False"), + (@{const_name True}, "True"), + (@{const_name Not}, "Not"), + (@{const_name conj}, "conj"), + (@{const_name disj}, "disj"), + (@{const_name implies}, "implies"), (@{const_name HOL.eq}, "equal"), - (@{const_name HOL.conj}, "and"), - (@{const_name HOL.disj}, "or"), - (@{const_name HOL.implies}, "implies"), (@{const_name Set.member}, "member"), + (@{const_name Metis.fFalse}, "fFalse"), + (@{const_name Metis.fTrue}, "fTrue"), + (@{const_name Metis.fNot}, "fNot"), + (@{const_name Metis.fconj}, "fconj"), + (@{const_name Metis.fdisj}, "fdisj"), + (@{const_name Metis.fimplies}, "fimplies"), (@{const_name Metis.fequal}, "fequal"), (@{const_name Meson.COMBI}, "COMBI"), (@{const_name Meson.COMBK}, "COMBK"), (@{const_name Meson.COMBB}, "COMBB"), (@{const_name Meson.COMBC}, "COMBC"), (@{const_name Meson.COMBS}, "COMBS"), - (@{const_name True}, "True"), - (@{const_name False}, "False"), (@{const_name If}, "If")] (* Invert the table of translations between Isabelle and ATPs. *) @@ -550,6 +557,12 @@ | string_of_mode FT = "FT" fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *) + | fn_isa_to_met_sublevel "c_False" = "c_fFalse" + | fn_isa_to_met_sublevel "c_True" = "c_fTrue" + | fn_isa_to_met_sublevel "c_Not" = "c_fNot" + | fn_isa_to_met_sublevel "c_conj" = "c_fconj" + | fn_isa_to_met_sublevel "c_disj" = "c_fdisj" + | fn_isa_to_met_sublevel "c_implies" = "c_fimplies" | fn_isa_to_met_sublevel x = x fun fn_isa_to_met_toplevel "equal" = "=" | fn_isa_to_met_toplevel x = x @@ -648,16 +661,41 @@ end; val helpers = - [("c_COMBI", (false, map (`I) @{thms Meson.COMBI_def})), - ("c_COMBK", (false, map (`I) @{thms Meson.COMBK_def})), - ("c_COMBB", (false, map (`I) @{thms Meson.COMBB_def})), - ("c_COMBC", (false, map (`I) @{thms Meson.COMBC_def})), - ("c_COMBS", (false, map (`I) @{thms Meson.COMBS_def})), - ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) - @{thms fequal_imp_equal equal_imp_fequal})), - ("c_True", (true, map (`I) @{thms True_or_False})), - ("c_False", (true, map (`I) @{thms True_or_False})), - ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))] + [("c_COMBI", (false, @{thms Meson.COMBI_def})), + ("c_COMBK", (false, @{thms Meson.COMBK_def})), + ("c_COMBB", (false, @{thms Meson.COMBB_def})), + ("c_COMBC", (false, @{thms Meson.COMBC_def})), + ("c_COMBS", (false, @{thms Meson.COMBS_def})), + ("c_fequal", + (false, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), + ("c_fFalse", (true, [@{lemma "x = fTrue | x = fFalse" + by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), + ("c_fFalse", (false, [@{lemma "~ fFalse" + by (unfold Metis.fFalse_def) fast}])), + ("c_fTrue", (true, [@{lemma "x = fTrue | x = fFalse" + by (unfold Metis.fFalse_def Metis.fTrue_def) fast}])), + ("c_fTrue", (false, [@{lemma "fTrue" + by (unfold Metis.fTrue_def) fast}])), + ("c_fNot", + (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] + fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), + ("c_fconj", + (false, @{lemma "~ P | ~ Q | Metis.fconj P Q" + "~ Metis.fconj P Q | P" + "~ Metis.fconj P Q | Q" + by (unfold Metis.fconj_def) fast+})), + ("c_fdisj", + (false, @{lemma "~ P | Metis.fdisj P Q" + "~ Q | Metis.fdisj P Q" + "~ Metis.fdisj P Q | P | Q" + by (unfold Metis.fdisj_def) fast+})), + ("c_fimplies", + (false, @{lemma "P | Metis.fimplies P Q" + "~ Q | Metis.fimplies P Q" + "~ Metis.fimplies P Q | ~ P | Q" + by (unfold Metis.fimplies_def) fast+})), + ("c_If", (true, @{thms if_True if_False True_or_False})) (* FIXME *)] (* ------------------------------------------------------------------------- *) (* Logic maps manage the interface between HOL and first-order logic. *) @@ -733,20 +771,20 @@ | set_mode FT = FT val mode = set_mode mode0 (*transform isabelle clause to metis clause *) - fun add_thm is_conjecture (metis_ith, isa_ith) + fun add_thm is_conjecture (isa_ith, metis_ith) {axioms, tfrees, old_skolems} : metis_problem = let val (mth, tfree_lits, old_skolems) = hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms) old_skolems metis_ith in - {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, + {axioms = (mth, isa_ith) :: axioms, tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} end; val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} - |> fold (add_thm true o `I) cls + |> fold (add_thm true o `Meson.make_meta_clause) cls |> add_tfrees - |> fold (fold (add_thm false o `I)) thss + |> fold (fold (add_thm false o `Meson.make_meta_clause)) thss val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) fun is_used c = exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists @@ -755,14 +793,18 @@ lmap else let + val fdefs = @{thms Metis.fFalse_def Metis.fTrue_def Metis.fNot_def + Metis.fconj_def Metis.fdisj_def + Metis.fimplies_def Metis.fequal_def} + val prepare_helper = + zero_var_indexes + #> `(Meson.make_meta_clause + #> rewrite_rule (map safe_mk_meta_eq fdefs)) val helper_ths = helpers |> filter (is_used o fst) |> maps (fn (c, (needs_full_types, thms)) => - if not (is_used c) orelse - needs_full_types andalso mode <> FT then - [] - else - thms) + if needs_full_types andalso mode <> FT then [] + else map prepare_helper thms) in lmap |> fold (add_thm false) helper_ths end in (mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)