# HG changeset patch # User blanchet # Date 1282234607 -7200 # Node ID 3003ddbd46d96070e0a86e3cde62613ab04e6a93 # Parent 970ee38495e417a2eb0aed064e6b35d68d9abbba encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Aug 19 14:39:31 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Aug 19 18:16:47 2010 +0200 @@ -31,28 +31,31 @@ [no_atp]: "skolem_id = (\x. x)" definition COMBI :: "'a \ 'a" where -[no_atp]: "COMBI P \ P" +[no_atp]: "COMBI P = P" definition COMBK :: "'a \ 'b \ 'a" where -[no_atp]: "COMBK P Q \ P" +[no_atp]: "COMBK P Q = P" definition COMBB :: "('b => 'c) \ ('a => 'b) \ 'a \ 'c" where [no_atp]: -"COMBB P Q R \ P (Q R)" +"COMBB P Q R = P (Q R)" definition COMBC :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where -[no_atp]: "COMBC P Q R \ P R Q" +[no_atp]: "COMBC P Q R = P R Q" definition COMBS :: "('a \ 'b \ 'c) \ ('a \ 'b) \ 'a \ 'c" where -[no_atp]: "COMBS P Q R \ P R (Q R)" +[no_atp]: "COMBS P Q R = P R (Q R)" definition fequal :: "'a \ 'a \ bool" where [no_atp]: -"fequal X Y \ (X = Y)" +"fequal X Y \ (X = Y)" + +lemma fequal_imp_equal [no_atp]: "\ fequal X Y \ X = Y" +by (simp add: fequal_def) -lemma fequal_imp_equal [no_atp]: "fequal X Y \ X = Y" - by (simp add: fequal_def) +lemma equal_imp_fequal [no_atp]: "\ X = Y \ fequal X Y" +by (simp add: fequal_def) -lemma equal_imp_fequal [no_atp]: "X = Y \ fequal X Y" - by (simp add: fequal_def) +lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y" +by auto text{*Theorems for translation to combinators*} diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 19 14:39:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Aug 19 18:16:47 2010 +0200 @@ -66,8 +66,10 @@ (* HOL to FOL (Isabelle to Metis) *) (* ------------------------------------------------------------------------- *) -fun fn_isa_to_met "equal" = "=" - | fn_isa_to_met x = x; +fun fn_isa_to_met_sublevel "equal" = "c_fequal" + | fn_isa_to_met_sublevel x = x +fun fn_isa_to_met_toplevel "equal" = "=" + | fn_isa_to_met_toplevel x = x fun metis_lit b c args = (b, (c, args)); @@ -89,7 +91,7 @@ | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm") fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = - Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist) + Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist) | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); @@ -99,7 +101,7 @@ fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty) | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = - wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) + wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty) | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), combtyp_of tm) @@ -108,7 +110,7 @@ let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys val lits = map hol_term_to_fol_FO tms - in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end + in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = (case strip_combterm_comb tm of (CombConst(("equal", _), _, _), tms) => @@ -224,13 +226,16 @@ fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) +fun smart_invert_const "fequal" = @{const_name "op ="} + | smart_invert_const s = invert_const s + fun hol_type_from_metis_term _ (Metis.Term.Var v) = (case strip_prefix_and_undo_ascii tvar_prefix v of SOME w => make_tvar w | NONE => make_tvar v) | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = (case strip_prefix_and_undo_ascii type_const_prefix x of - SOME tc => Term.Type (invert_const tc, + SOME tc => Term.Type (smart_invert_const tc, map (hol_type_from_metis_term ctxt) tys) | NONE => case strip_prefix_and_undo_ascii tfree_prefix x of @@ -265,7 +270,7 @@ | applic_to_tt (a,ts) = case strip_prefix_and_undo_ascii const_prefix a of SOME b => - let val c = invert_const b + let val c = smart_invert_const b val ntypes = num_type_args thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts @@ -283,7 +288,7 @@ | NONE => (*Not a constant. Is it a type constructor?*) case strip_prefix_and_undo_ascii type_const_prefix a of SOME b => - Type (Term.Type (invert_const b, types_of (map tm_to_tt ts))) + Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) case strip_prefix_and_undo_ascii tfree_prefix a of SOME b => Type (mk_tfree ctxt b) @@ -311,7 +316,7 @@ Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = (case strip_prefix_and_undo_ascii const_prefix x of - SOME c => Const (invert_const c, dummyT) + SOME c => Const (smart_invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_undo_ascii fixed_var_prefix x of SOME v => Free (v, hol_type_from_metis_term ctxt ty) @@ -325,7 +330,7 @@ list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = (case strip_prefix_and_undo_ascii const_prefix x of - SOME c => Const (invert_const c, dummyT) + SOME c => Const (smart_invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_undo_ascii fixed_var_prefix x of SOME v => Free (v, dummyT) @@ -598,9 +603,6 @@ (* Translation of HO Clauses *) (* ------------------------------------------------------------------------- *) -fun cnf_helper_theorem thy raw th = - if raw then th else the_single (Clausifier.cnf_axiom thy th) - fun type_ext thy tms = let val subs = tfree_classes_of_terms tms val supers = tvar_classes_of_terms tms @@ -650,15 +652,16 @@ | string_of_mode FT = "FT" val helpers = - [("c_COMBI", (false, @{thms COMBI_def})), - ("c_COMBK", (false, @{thms COMBK_def})), - ("c_COMBB", (false, @{thms COMBB_def})), - ("c_COMBC", (false, @{thms COMBC_def})), - ("c_COMBS", (false, @{thms COMBS_def})), - ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})), - ("c_True", (true, @{thms True_or_False})), - ("c_False", (true, @{thms True_or_False})), - ("c_If", (true, @{thms if_True if_False True_or_False}))] + [("c_COMBI", (false, map (`I) @{thms COMBI_def})), + ("c_COMBK", (false, map (`I) @{thms COMBK_def})), + ("c_COMBB", (false, map (`I) @{thms COMBB_def})), + ("c_COMBC", (false, map (`I) @{thms COMBC_def})), + ("c_COMBS", (false, map (`I) @{thms 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}))] fun is_quasi_fol_clause thy = Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of @@ -673,18 +676,20 @@ | set_mode FT = FT val mode = set_mode mode0 (*transform isabelle clause to metis clause *) - fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map = + fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems} + : logic_map = let val (mth, tfree_lits, skolems) = - hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith + hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems + metis_ith in - {axioms = (mth, Meson.make_meta_clause ith) :: axioms, + {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms, tfrees = union (op =) tfree_lits tfrees, skolems = skolems} end; val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []} - |> fold (add_thm true) cls + |> fold (add_thm true o `I) cls |> add_tfrees - |> fold (add_thm false) ths + |> fold (add_thm false o `I) ths 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 @@ -695,11 +700,12 @@ let val helper_ths = helpers |> filter (is_used o fst) - |> maps (fn (_, (raw, thms)) => - if mode = FT orelse not raw then - map (cnf_helper_theorem @{theory} raw) thms + |> maps (fn (c, (needs_full_types, thms)) => + if not (is_used c) orelse + needs_full_types andalso mode <> FT then + [] else - []) + thms) in lmap |> fold (add_thm false) helper_ths end in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 19 14:39:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 19 18:16:47 2010 +0200 @@ -82,9 +82,9 @@ (*Pairs a constant with the list of its type instantiations (using const_typ)*) fun const_with_typ thy (c,typ) = - let val tvars = Sign.const_typargs thy (c,typ) - in (c, map const_typ_of tvars) end - handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*) + let val tvars = Sign.const_typargs thy (c,typ) in + (c, map const_typ_of tvars) end + handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*) (*Add a const/type pair to the table, but a [] entry means a standard connective, which we ignore.*) @@ -95,7 +95,8 @@ val fresh_prefix = "Sledgehammer.Fresh." val flip = Option.map not (* These are typically simplified away by "Meson.presimplify". *) -val boring_consts = [@{const_name If}, @{const_name Let}] +val boring_consts = + [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)] fun get_consts_typs thy pos ts = let @@ -104,9 +105,8 @@ introduce a fresh constant to simulate the effect of Skolemization. *) fun do_term t = case t of - Const (@{const_name Let}, _) => I - | Const x => add_const_type_to_table (const_with_typ thy x) - | Free x => add_const_type_to_table (const_with_typ thy x) + Const x => add_const_type_to_table (const_with_typ thy x) + | Free (s, _) => add_const_type_to_table (s, []) | t1 $ t2 => do_term t1 #> do_term t2 | Abs (_, _, t) => (* Abstractions lead to combinators, so we add a penalty for them. *) @@ -198,7 +198,7 @@ fun count_axiom_consts theory_relevant thy (_, th) = let fun do_const (a, T) = - let val (c, cts) = const_with_typ thy (a,T) in + let val (c, cts) = const_with_typ thy (a, T) in (* Two-dimensional table update. Constant maps to types maps to count. *) CTtab.map_default (cts, 0) (Integer.add 1) diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 19 14:39:31 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 19 18:16:47 2010 +0200 @@ -209,7 +209,7 @@ val optional_typed_helpers = [(["c_True", "c_False"], @{thms True_or_False}), (["c_If"], @{thms if_True if_False True_or_False})] -val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} +val mandatory_helpers = @{thms fequal_def} val init_counters = Symtab.make (maps (maps (map (rpair 0) o fst)) diff -r 970ee38495e4 -r 3003ddbd46d9 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Aug 19 14:39:31 2010 +0200 +++ b/src/HOL/Tools/meson.ML Thu Aug 19 18:16:47 2010 +0200 @@ -527,7 +527,8 @@ which are needed to avoid the various one-point theorems from generating junk clauses.*) val nnf_simps = @{thms simp_implies_def Ex1_def Ball_def Bex_def if_True if_False if_cancel - if_eq_cancel cases_simp} + if_eq_cancel cases_simp (* TODO: mem_def_raw Collect_def_raw *)} +(* TODO: @ [@{lemma "{} = (%x. False)" by (rule ext) auto}] *) val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms} val nnf_ss = @@ -539,8 +540,7 @@ #> simplify nnf_ss fun make_nnf ctxt th = case prems_of th of - [] => th |> presimplify - |> make_nnf1 ctxt + [] => th |> presimplify |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]); (*Pull existential quantifiers to front. This accomplishes Skolemization for