# HG changeset patch # User blanchet # Date 1307386566 -7200 # Node ID 050a03afe0241979e967fbf8b70ac83bc2f44536 # Parent 77c432fe28ffcc3ace9e8ab5873f5ef241e67160 Metis code cleanup diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Metis_Examples/Proxies.thy --- a/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jun 06 20:56:06 2011 +0200 @@ -24,24 +24,24 @@ lemma "inc \ (\y. 0)" sledgehammer [expect = some] (inc_def plus_1_not_0) -by (new_metis_exhaust inc_def plus_1_not_0) +by (metis_exhaust inc_def plus_1_not_0) lemma "inc = (\y. y + 1)" sledgehammer [expect = some] (inc_def) -by (new_metis_exhaust inc_def) +by (metis_exhaust inc_def) definition add_swap :: "nat \ nat \ nat" where "add_swap = (\x y. y + x)" lemma "add_swap m n = n + m" sledgehammer [expect = some] (add_swap_def) -by (new_metis_exhaust add_swap_def) +by (metis_exhaust add_swap_def) definition "A = {xs\'a list. True}" lemma "xs \ A" sledgehammer [expect = some] -by (new_metis_exhaust A_def Collect_def mem_def) +by (metis_exhaust A_def Collect_def mem_def) definition "B (y::int) \ y \ 0" definition "C (y::int) \ y \ 1" @@ -51,7 +51,7 @@ lemma "B \ C" sledgehammer [type_sys = poly_args, max_relevant = 200, expect = some] -by (new_metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) +by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I) text {* Proxies for logical constants *} @@ -78,7 +78,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "\ id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -90,7 +90,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "x = id True \ x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -102,7 +102,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id x = id True \ id x = id False" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -114,7 +114,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "P True \ P False \ P x" sledgehammer [type_sys = erased, expect = none] () @@ -139,7 +139,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (\ \ a) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -151,7 +151,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (\ (id (\ a))) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -163,7 +163,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (a \ b) \ id a" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -175,7 +175,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (a \ b) \ id b" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -187,7 +187,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id a \ id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -199,7 +199,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id a \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -211,7 +211,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id b \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -223,7 +223,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (\ a) \ id (\ b) \ id (\ (a \ b))" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -235,7 +235,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (\ a) \ id (a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -247,7 +247,7 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) lemma "id (a \ b) \ id (\ a \ b)" sledgehammer [type_sys = erased, expect = some] (id_apply) @@ -259,6 +259,6 @@ sledgehammer [type_sys = mangled_tags, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds?, expect = some] (id_apply) sledgehammer [type_sys = mangled_preds, expect = some] (id_apply) -by (new_metis_exhaust id_apply) +by (metis_exhaust id_apply) end diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Mon Jun 06 20:56:06 2011 +0200 @@ -69,47 +69,47 @@ "mangled_tags_heavy!", "simple!"] -fun new_metis_exhaust_tac ctxt ths = +fun metis_exhaust_tac ctxt ths = let fun tac [] st = all_tac st | tac (type_sys :: type_syss) st = st (* |> tap (fn _ => tracing (PolyML.makestring type_sys)) *) |> ((if null type_syss then all_tac else rtac @{thm fork} 1) - THEN Metis_Tactics.new_metis_tac [type_sys] ctxt ths 1 + THEN Metis_Tactics.metis_tac [type_sys] ctxt ths 1 THEN COND (has_fewer_prems 2) all_tac no_tac THEN tac type_syss) in tac end *} -method_setup new_metis_exhaust = {* +method_setup metis_exhaust = {* Attrib.thms >> - (fn ths => fn ctxt => SIMPLE_METHOD (new_metis_exhaust_tac ctxt ths type_syss)) + (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_syss)) *} "exhaustively run the new Metis with all type encodings" text {* Miscellaneous tests *} lemma "x = y \ y = x" -by new_metis_exhaust +by metis_exhaust lemma "[a] = [1 + 1] \ a = 1 + (1::int)" -by (new_metis_exhaust last.simps) +by (metis_exhaust last.simps) lemma "map Suc [0] = [Suc 0]" -by (new_metis_exhaust map.simps) +by (metis_exhaust map.simps) lemma "map Suc [1 + 1] = [Suc 2]" -by (new_metis_exhaust map.simps nat_1_add_1) +by (metis_exhaust map.simps nat_1_add_1) lemma "map Suc [2] = [Suc (1 + 1)]" -by (new_metis_exhaust map.simps nat_1_add_1) +by (metis_exhaust map.simps nat_1_add_1) definition "null xs = (xs = [])" lemma "P (null xs) \ null xs \ xs = []" -by (new_metis_exhaust null_def) +by (metis_exhaust null_def) lemma "(0::nat) + 0 = 0" -by (new_metis_exhaust arithmetic_simps(38)) +by (metis_exhaust arithmetic_simps(38)) end diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Jun 06 20:56:06 2011 +0200 @@ -18,7 +18,7 @@ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) - fun metis ctxt = Metis_Tactics.new_metis_tac [] ctxt (thms @ facts) + fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> prefix (metis_tag id) diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 06 20:56:06 2011 +0200 @@ -542,9 +542,9 @@ else if !reconstructor = "smt" then SMT_Solver.smt_tac else if full orelse !reconstructor = "metisFT" then - Metis_Tactics.new_metisFT_tac + Metis_Tactics.metisFT_tac else - Metis_Tactics.new_metis_tac []) ctxt thms + Metis_Tactics.metis_tac []) ctxt thms fun apply_reconstructor thms = Mirabelle.can_apply timeout (do_reconstructor thms) st diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Mon Jun 06 20:56:06 2011 +0200 @@ -427,7 +427,10 @@ fun term_from_atp ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt - (* see also "mk_var" in "Metis_Reconstruct" *) + (* For Metis, we use 1 rather than 0 because variable references in clauses + may otherwise conflict with variable constraints in the goal. At least, + type inference often fails otherwise. See also "axiom_inference" in + "Metis_Reconstruct". *) val var_index = if textual then 0 else 1 fun do_term extra_ts opt_T u = case u of diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:56:06 2011 +0200 @@ -9,8 +9,6 @@ signature METIS_RECONSTRUCT = sig - type mode = Metis_Translate.mode - exception METIS of string * string val trace : bool Config.T @@ -23,7 +21,7 @@ val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term * term -> bool val replay_one_inference : - Proof.context -> mode -> (string * term) list -> int Symtab.table + Proof.context -> (string * term) list -> int Symtab.table -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : @@ -65,154 +63,6 @@ | types_of (SomeTerm _ :: tts) = types_of tts | types_of (SomeType T :: tts) = T :: types_of tts -fun apply_list rator nargs rands = - let val trands = terms_of rands - in if length trands = nargs then SomeTerm (list_comb(rator, trands)) - else raise Fail - ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ - " expected " ^ string_of_int nargs ^ - " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) - end; - -fun infer_types ctxt = - Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) - -(* We use 1 rather than 0 because variable references in clauses may otherwise - conflict with variable constraints in the goal...at least, type inference - often fails otherwise. See also "axiom_inference" below. *) -fun make_var (w, T) = Var ((w, 1), T) - -(*Remove the "apply" operator from an HO term*) -fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t - | strip_happ args x = (x, args) - -fun hol_type_from_metis_term _ (Metis_Term.Var v) = - (case strip_prefix_and_unascii 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_unascii type_const_prefix x of - SOME tc => Type (invert_const tc, - map (hol_type_from_metis_term ctxt) tys) - | NONE => - case strip_prefix_and_unascii tfree_prefix x of - SOME tf => make_tfree ctxt tf - | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); - -(*Maps metis terms to isabelle terms*) -fun hol_term_from_metis_PT ctxt fol_tm = - let val thy = Proof_Context.theory_of ctxt - val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) - fun tm_to_tt (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => SomeType (make_tvar w) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => SomeTerm (make_var (w, HOLogic.typeT)) - | NONE => SomeTerm (make_var (v, HOLogic.typeT))) - (*Var from Metis with a name like _nnn; possibly a type variable*) - | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) - | tm_to_tt (t as Metis_Term.Fn (".", _)) = - let val (rator,rands) = strip_happ [] t in - case rator of - Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) - | _ => case tm_to_tt rator of - SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) - | _ => raise Fail "tm_to_tt: HO application" - end - | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) - and applic_to_tt ("=",ts) = - SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) - | applic_to_tt (a,ts) = - case strip_prefix_and_unascii const_prefix a of - SOME b => - let - val c = b |> invert_const |> unproxify_const - val ntypes = num_type_args thy c - val nterms = length ts - ntypes - val tts = map tm_to_tt ts - val tys = types_of (List.take(tts,ntypes)) - val t = - if String.isPrefix new_skolem_const_prefix c then - Var ((new_skolem_var_name_from_const c, 1), - Type_Infer.paramify_vars (tl tys ---> hd tys)) - else - Const (c, dummyT) - in if length tys = ntypes then - apply_list t nterms (List.drop(tts,ntypes)) - else - raise Fail ("Constant " ^ c ^ " expects " ^ string_of_int ntypes ^ - " but gets " ^ string_of_int (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) - end - | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix_and_unascii type_const_prefix a of - SOME b => - SomeType (Type (invert_const b, types_of (map tm_to_tt ts))) - | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix_and_unascii tfree_prefix a of - SOME b => SomeType (make_tfree ctxt b) - | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix_and_unascii fixed_var_prefix a of - SOME b => - let val opr = Free (b, HOLogic.typeT) - in apply_list opr (length ts) (map tm_to_tt ts) end - | NONE => raise Fail ("unexpected metis function: " ^ a) - in - case tm_to_tt fol_tm of - SomeTerm t => t - | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) - end - -(*Maps fully-typed metis terms to isabelle terms*) -fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) - fun do_const c = - let val c = c |> invert_const |> unproxify_const in - if String.isPrefix new_skolem_const_prefix c then - Var ((new_skolem_var_name_from_const c, 1), dummyT) - else - Const (c, dummyT) - end - fun cvt (Metis_Term.Fn (":", [Metis_Term.Var v, _])) = - (case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => make_var (w, dummyT) - | NONE => make_var (v, dummyT)) - | cvt (Metis_Term.Fn (":", [Metis_Term.Fn ("=",[]), _])) = - Const (@{const_name HOL.eq}, HOLogic.typeT) - | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (x,[]), ty])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => do_const c - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, hol_type_from_metis_term ctxt ty) - | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) - | cvt (Metis_Term.Fn (":", [Metis_Term.Fn (".", [tm1,tm2]), _])) = - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) - | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = - list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) - | cvt (t as Metis_Term.Fn (x, [])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => do_const c - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, dummyT) - | NONE => (trace_msg ctxt (fn () => - "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg ctxt (fn () => - "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) - in fol_tm |> cvt end - fun atp_name_from_metis s = case find_first (fn (_, (s', _)) => s' = s) metis_name_table of SOME ((s, _), (_, swap)) => (s, swap) @@ -223,15 +73,8 @@ end | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, []) -fun hol_term_from_metis_MX ctxt sym_tab = - atp_term_from_metis - #> term_from_atp ctxt false sym_tab NONE - -fun hol_term_from_metis ctxt FO _ = hol_term_from_metis_PT ctxt - | hol_term_from_metis ctxt HO _ = hol_term_from_metis_PT ctxt - | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt - | hol_term_from_metis ctxt (Type_Sys _) sym_tab = - hol_term_from_metis_MX ctxt sym_tab +fun hol_term_from_metis ctxt sym_tab = + atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE fun atp_literal_from_metis (pos, atom) = atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot @@ -241,7 +84,7 @@ fun reveal_old_skolems_and_infer_types ctxt old_skolems = map (reveal_old_skolem_terms old_skolems) - #> infer_types ctxt + #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt) fun hol_clause_from_metis ctxt sym_tab old_skolems = Metis_Thm.clause @@ -250,8 +93,8 @@ #> prop_from_atp ctxt false sym_tab #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems) -fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms = - let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms +fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms = + let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms val _ = trace_msg ctxt (fn () => " calling type inference:") val _ = app (fn t => trace_msg ctxt (fn () => Syntax.string_of_term ctxt t)) ts @@ -284,9 +127,9 @@ (* INFERENCE RULE: AXIOM *) -(* This causes variables to have an index of 1 by default. See also "make_var" - above. *) -fun axiom_inference th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th) +(* This causes variables to have an index of 1 by default. See also + "term_from_atp" in "ATP_Reconstruct". *) +val axiom_inference = Thm.incr_indexes 1 oo lookth (* INFERENCE RULE: ASSUME *) @@ -298,10 +141,10 @@ val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)] in cterm_instantiate substs th end; -fun assume_inference ctxt mode old_skolems sym_tab atom = +fun assume_inference ctxt old_skolems sym_tab atom = inst_excluded_middle (Proof_Context.theory_of ctxt) - (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) + (singleton (hol_terms_from_metis ctxt old_skolems sym_tab) (Metis_Term.Fn atom)) (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying @@ -309,7 +152,7 @@ sorts. Instead we try to arrange that new TVars are distinct and that types can be inferred from terms. *) -fun inst_inference ctxt mode old_skolems sym_tab th_pairs fsubst th = +fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th = let val thy = Proof_Context.theory_of ctxt val i_th = lookth th_pairs th val i_th_vars = Term.add_vars (prop_of i_th) [] @@ -317,7 +160,7 @@ fun subst_translation (x,y) = let val v = find_var x (* We call "reveal_old_skolems_and_infer_types" below. *) - val t = hol_term_from_metis ctxt mode sym_tab y + val t = hol_term_from_metis ctxt sym_tab y in SOME (cterm_of thy (Var v), t) end handle Option.Option => (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ @@ -441,7 +284,7 @@ (* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) val select_literal = negate_head oo make_last -fun resolve_inference ctxt mode old_skolems sym_tab th_pairs atom th1 th2 = +fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 = let val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) val _ = trace_msg ctxt (fn () => @@ -457,7 +300,7 @@ let val thy = Proof_Context.theory_of ctxt val i_atom = - singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) + singleton (hol_terms_from_metis ctxt old_skolems sym_tab) (Metis_Term.Fn atom) val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atom) @@ -486,10 +329,10 @@ val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); val refl_idx = 1 + Thm.maxidx_of REFL_THM; -fun refl_inference ctxt mode old_skolems sym_tab t = +fun refl_inference ctxt old_skolems sym_tab t = let val thy = Proof_Context.theory_of ctxt - val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t + val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end @@ -499,19 +342,11 @@ val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} -val metis_eq = Metis_Term.Fn ("=", []); - -(* Equality has no type arguments *) -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 - | get_ty_arg_size thy (Const (s, _)) = - (num_type_args thy s handle TYPE _ => 0) - | get_ty_arg_size _ _ = 0 - -fun equality_inference ctxt mode old_skolems sym_tab (pos, atom) fp fr = +fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr = let val thy = Proof_Context.theory_of ctxt val m_tm = Metis_Term.Fn atom val [i_atom, i_tm] = - hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr] + hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr] val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos) fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls @@ -522,53 +357,24 @@ (case t of SOME t => " fol-term: " ^ Metis_Term.toString t | NONE => "")) - fun path_finder_FO tm [] = (tm, Bound 0) - | path_finder_FO tm (p::ps) = - let val (tm1,args) = strip_comb tm - val adjustment = get_ty_arg_size thy tm1 - val p' = if adjustment > p then p else p - adjustment - val tm_p = nth args p' - handle Subscript => - raise METIS ("equality_inference", - string_of_int p ^ " adj " ^ - string_of_int adjustment ^ " term " ^ - Syntax.string_of_term ctxt tm) - val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^ - " " ^ Syntax.string_of_term ctxt tm_p) - val (r,t) = path_finder_FO tm_p ps - in - (r, list_comb (tm1, replace_item_list t p' args)) - end - fun path_finder_HO tm [] = (tm, Bound 0) - | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) - | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) - | path_finder_HO tm ps = path_finder_fail tm ps NONE - fun path_finder_FT tm [] _ = (tm, Bound 0) - | path_finder_FT tm (0::ps) (Metis_Term.Fn (":", [t1, _])) = - path_finder_FT tm ps t1 - | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = - (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) - | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = - (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = path_finder_fail tm ps (SOME t) - fun path_finder_MX tm [] _ = (tm, Bound 0) - | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = + fun path_finder tm [] _ = (tm, Bound 0) + | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) = let val s = s |> perhaps (try (strip_prefix_and_unascii const_prefix #> the #> unmangled_const_name)) in if s = metis_predicator orelse s = predicator_name orelse s = metis_type_tag orelse s = type_tag_name then - path_finder_MX tm ps (nth ts p) + path_finder tm ps (nth ts p) else if s = metis_app_op orelse s = app_op_name then let val (tm1, tm2) = dest_comb tm val p' = p - (length ts - 2) in if p' = 0 then - path_finder_MX tm1 ps (nth ts p) ||> (fn y => y $ tm2) + path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2) else - path_finder_MX tm2 ps (nth ts p) ||> (fn y => tm1 $ y) + path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y) end else let @@ -581,31 +387,11 @@ val _ = trace_msg ctxt (fn () => "path_finder: " ^ string_of_int p ^ " " ^ Syntax.string_of_term ctxt tm_p) - val (r, t) = path_finder_MX tm_p ps (nth ts p) + val (r, t) = path_finder tm_p ps (nth ts p) in (r, list_comb (tm1, replace_item_list t p' args)) end end - | path_finder_MX tm ps t = path_finder_fail tm ps (SOME t) - fun path_finder FO tm ps _ = path_finder_FO tm ps - | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) - else path_finder_HO tm (p::ps) (*1 selects second operand*) - | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = - path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) - | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) - (Metis_Term.Fn ("=", [t1,t2])) = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_FT tm (0::1::ps) - (Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2])) - (*select first operand*) - else path_finder_FT tm (p::ps) - (Metis_Term.Fn (metis_app_op, [metis_eq, t2])) - (*1 selects second operand*) - | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 - (*if not equality, ignore head to skip the hBOOL predicate*) - | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - | path_finder (Type_Sys _) tm ps t = path_finder_MX tm ps t - val (tm_subst, body) = path_finder mode i_atom fp m_tm + | path_finder tm ps t = path_finder_fail tm ps (SOME t) + val (tm_subst, body) = path_finder i_atom fp m_tm val tm_abs = Abs ("x", type_of tm_subst, body) val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) @@ -619,21 +405,21 @@ val factor = Seq.hd o distinct_subgoals_tac -fun one_step ctxt mode old_skolems sym_tab th_pairs p = +fun one_step ctxt old_skolems sym_tab th_pairs p = case p of (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atom) => - assume_inference ctxt mode old_skolems sym_tab f_atom + assume_inference ctxt old_skolems sym_tab f_atom | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - inst_inference ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 + inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1 |> factor | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) => - resolve_inference ctxt mode old_skolems sym_tab th_pairs f_atom f_th1 f_th2 + resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2 |> factor | (_, Metis_Proof.Refl f_tm) => - refl_inference ctxt mode old_skolems sym_tab f_tm + refl_inference ctxt old_skolems sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inference ctxt mode old_skolems sym_tab f_lit f_p f_r + equality_inference ctxt old_skolems sym_tab f_lit f_p f_r fun flexflex_first_order th = case Thm.tpairs_of th of @@ -684,7 +470,7 @@ end end -fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs = +fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs = if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then (* Isabelle sometimes identifies literals (premises) that are distinct in @@ -699,7 +485,7 @@ (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf) + val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf) |> flexflex_first_order |> resynchronize ctxt fol_th val _ = trace_msg ctxt diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:56:06 2011 +0200 @@ -16,11 +16,8 @@ val trace : bool Config.T val verbose : bool Config.T val new_skolemizer : bool Config.T - val old_metis_tac : Proof.context -> thm list -> int -> tactic - val old_metisF_tac : Proof.context -> thm list -> int -> tactic - val old_metisFT_tac : Proof.context -> thm list -> int -> tactic - val new_metis_tac : string list -> Proof.context -> thm list -> int -> tactic - val new_metisFT_tac : Proof.context -> thm list -> int -> tactic + val metis_tac : string list -> Proof.context -> thm list -> int -> tactic + val metisFT_tac : Proof.context -> thm list -> int -> tactic val setup : theory -> theory end @@ -38,15 +35,12 @@ val default_unsound_type_sys = "poly_args" val default_sound_type_sys = "poly_preds_heavy_query" -fun method_call_for_mode HO = (@{binding old_metis}, "") - | method_call_for_mode FO = (@{binding metisF}, "") - | method_call_for_mode FT = (@{binding old_metisFT}, "") - | method_call_for_mode (Type_Sys type_sys) = - if type_sys = default_sound_type_sys then - (@{binding metisFT}, "") - else - (@{binding metis}, - if type_sys = default_unsound_type_sys then "" else type_sys) +fun method_call_for_type_sys type_sys = + if type_sys = default_sound_type_sys then + (@{binding metisFT}, "") + else + (@{binding metis}, + if type_sys = default_unsound_type_sys then "" else type_sys) val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) @@ -92,13 +86,8 @@ val resolution_params = {active = active_params, waiting = waiting_params} (* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 = +fun FOL_SOLVE (type_sys :: fallback_type_syss) ctxt cls ths0 = let val thy = Proof_Context.theory_of ctxt - val _ = - if mode = FO then - legacy_feature "Old 'metisF' command -- use 'metis' instead" - else - () val new_skolemizer = Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) val th_cls_pairs = @@ -112,8 +101,8 @@ val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths - val (mode, sym_tab, {axioms, old_skolems, ...}) = - prepare_metis_problem ctxt mode cls ths + val (sym_tab, axioms, old_skolems) = + prepare_metis_problem ctxt type_sys cls ths fun get_isa_thm mth Isa_Reflexive_or_Trivial = reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth | get_isa_thm _ (Isa_Raw ith) = ith @@ -121,7 +110,7 @@ val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = axioms |> map fst val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms - val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) + val _ = trace_msg ctxt (fn () => "type_sys = " ^ type_sys) val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") in case filter (fn t => prop_of t aconv @{prop False}) cls of @@ -136,8 +125,8 @@ (*add constraints arising from converting goal to clause form*) val proof = Metis_Proof.proof mth val result = - fold (replay_one_inference ctxt' mode old_skolems sym_tab) - proof axioms + axioms + |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof val used = map_filter (used_axioms axioms) proof val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used @@ -166,7 +155,7 @@ end | Metis_Resolution.Satisfiable _ => (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); - if null fallback_modes then + if null fallback_type_syss then () else raise METIS ("FOL_SOLVE", @@ -174,17 +163,17 @@ []) end handle METIS (loc, msg) => - case fallback_modes of + case fallback_type_syss of [] => error ("Failed to replay Metis proof in Isabelle." ^ (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg else "")) - | mode :: _ => - let val (binding, arg) = method_call_for_mode mode in + | type_sys :: _ => + let val (binding, arg) = method_call_for_type_sys type_sys in (verbose_warning ctxt ("Falling back on " ^ quote (Binding.qualified_name_of binding ^ (arg |> arg <> "" ? enclose " (" ")")) ^ "..."); - FOL_SOLVE fallback_modes ctxt cls ths0) + FOL_SOLVE fallback_type_syss ctxt cls ths0) end val neg_clausify = @@ -204,12 +193,12 @@ val type_has_top_sort = exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) -fun generic_metis_tac modes ctxt ths i st0 = +fun generic_metis_tac type_syss ctxt ths i st0 = let val _ = trace_msg ctxt (fn () => "Metis called with theorems\n" ^ cat_lines (map (Display.string_of_thm ctxt) ths)) - fun tac clause = resolve_tac (FOL_SOLVE modes ctxt clause ths) 1 + fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 in if exists_type type_has_top_sort (prop_of st0) then (verbose_warning ctxt "Proof state contains the universal sort {}"; @@ -218,19 +207,12 @@ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 end -val old_metis_modes = [HO, FT] -val old_metisF_modes = [FO, FT] -val old_metisFT_modes = [FT] -val new_metis_default_modes = - map Type_Sys [default_unsound_type_sys, default_sound_type_sys] -val new_metisFT_modes = [Type_Sys default_sound_type_sys] +val metis_default_type_syss = [default_unsound_type_sys, default_sound_type_sys] +val metisFT_type_syss = [default_sound_type_sys] -val old_metis_tac = generic_metis_tac old_metis_modes -val old_metisF_tac = generic_metis_tac old_metisF_modes -val old_metisFT_tac = generic_metis_tac old_metisFT_modes -fun new_metis_tac [] = generic_metis_tac new_metis_default_modes - | new_metis_tac type_syss = generic_metis_tac (map Type_Sys type_syss) -val new_metisFT_tac = generic_metis_tac new_metisFT_modes +fun metis_tac [] = generic_metis_tac metis_default_type_syss + | metis_tac type_syss = generic_metis_tac type_syss +val metisFT_tac = generic_metis_tac metisFT_type_syss (* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. @@ -240,33 +222,30 @@ val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of -fun method modes (type_sys, ths) ctxt facts = +fun method type_syss (type_sys, ths) ctxt facts = let val (schem_facts, nonschem_facts) = List.partition has_tvar facts - val modes = type_sys |> Option.map (single o Type_Sys) |> the_default modes + val type_syss = type_sys |> Option.map single |> the_default type_syss in HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP o generic_metis_tac modes ctxt (schem_facts @ ths)) + CHANGED_PROP + o generic_metis_tac type_syss ctxt (schem_facts @ ths)) end -fun setup_method (modes as mode :: _) = - (if modes = new_metis_default_modes then +fun setup_method (type_syss as type_sys :: _) = + (if type_syss = metis_default_type_syss then (Args.parens Parse.short_ident >> (fn s => if s = full_typesN then default_sound_type_sys else s)) |> Scan.option |> Scan.lift else Scan.succeed NONE) - -- Attrib.thms >> (METHOD oo method modes) - |> Method.setup (fst (method_call_for_mode mode)) + -- Attrib.thms >> (METHOD oo method type_syss) + |> Method.setup (fst (method_call_for_type_sys type_sys)) val setup = - [(old_metis_modes, "Metis for FOL and HOL problems"), - (old_metisF_modes, "Metis for FOL problems (legacy)"), - (old_metisFT_modes, - "Metis for FOL/HOL problems with fully-typed translation"), - (new_metis_default_modes, "Metis for FOL and HOL problems (experimental)"), - (new_metisFT_modes, - "Metis for FOL/HOL problems with fully-typed translation (experimental)")] + [(metis_default_type_syss, "Metis for FOL and HOL problems"), + (metisFT_type_syss, + "Metis for FOL/HOL problems with fully-typed translation")] |> fold (uncurry setup_method) end; diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:56:06 2011 +0200 @@ -11,17 +11,10 @@ sig type type_literal = ATP_Translate.type_literal - datatype mode = FO | HO | FT | Type_Sys of string - datatype isa_thm = Isa_Reflexive_or_Trivial | Isa_Raw of thm - type metis_problem = - {axioms : (Metis_Thm.thm * isa_thm) list, - tfrees : type_literal list, - old_skolems : (string * term) list} - val metis_equal : string val metis_predicator : string val metis_app_op : string @@ -29,10 +22,9 @@ val metis_generated_var_prefix : string val metis_name_table : ((string * int) * (string * bool)) list val reveal_old_skolem_terms : (string * term) list -> term -> term - val string_of_mode : mode -> string val prepare_metis_problem : - Proof.context -> mode -> thm list -> thm list - -> mode * int Symtab.table * metis_problem + Proof.context -> string -> thm list -> thm list + -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list end structure Metis_Translate : METIS_TRANSLATE = @@ -54,20 +46,6 @@ ((prefixed_app_op_name, 2), (metis_app_op, false)), ((prefixed_type_tag_name, 2), (metis_type_tag, true))] -fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos) - | predicate_of thy (t, pos) = - (combterm_from_term thy [] (Envir.eta_contract t), pos) - -fun literals_of_term1 args thy (@{const Trueprop} $ P) = - literals_of_term1 args thy P - | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) = - literals_of_term1 (literals_of_term1 args thy P) thy Q - | literals_of_term1 (lits, ts) thy P = - let val ((pred, ts'), pol) = predicate_of thy (P, true) in - ((pol, pred) :: lits, union (op =) ts ts') - end -val literals_of_term = literals_of_term1 ([], []) - fun old_skolem_const_name i j num_T_args = old_skolem_const_prefix ^ Long_Name.separator ^ (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args])) @@ -114,127 +92,6 @@ (* ------------------------------------------------------------------------- *) -(* HOL to FOL (Isabelle to Metis) *) -(* ------------------------------------------------------------------------- *) - -(* first-order, higher-order, fully-typed, ATP type system *) -datatype mode = FO | HO | FT | Type_Sys of string - -fun string_of_mode FO = "FO" - | string_of_mode HO = "HO" - | string_of_mode FT = "FT" - | string_of_mode (Type_Sys type_sys) = "Type_Sys " ^ type_sys - -fun fn_isa_to_met_sublevel "equal" = "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" = metis_equal - | fn_isa_to_met_toplevel x = x - -fun metis_lit b c args = (b, (c, args)); - -fun metis_term_from_typ (Type (s, Ts)) = - Metis_Term.Fn (make_fixed_type_const s, map metis_term_from_typ Ts) - | metis_term_from_typ (TFree (s, _)) = - Metis_Term.Fn (make_fixed_type_var s, []) - | metis_term_from_typ (TVar (x, _)) = - Metis_Term.Var (make_schematic_type_var x) - -(*These two functions insert type literals before the real literals. That is the - opposite order from TPTP linkup, but maybe OK.*) - -fun hol_term_to_fol_FO tm = - case strip_combterm_comb tm of - (CombConst ((c, _), _, Ts), tms) => - let val tyargs = map metis_term_from_typ Ts - val args = map hol_term_to_fol_FO tms - in Metis_Term.Fn (c, tyargs @ args) end - | (CombVar ((v, _), _), []) => Metis_Term.Var v - | _ => raise Fail "non-first-order combterm" - -fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) = - Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts) - | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s - | hol_term_to_fol_HO (CombApp (tm1, tm2)) = - Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2]) - -(*The fully-typed translation, to avoid type errors*) -fun tag_with_type tm T = - Metis_Term.Fn (metis_type_tag, [tm, metis_term_from_typ T]) - -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = - tag_with_type (Metis_Term.Var s) ty - | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) = - tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty - | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) = - tag_with_type - (Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2])) - (combtyp_of tm) - -fun hol_literal_to_fol FO (pos, tm) = - let - val (CombConst((p, _), _, Ts), tms) = strip_combterm_comb tm - val tylits = if p = "equal" then [] else map metis_term_from_typ Ts - val lits = map hol_term_to_fol_FO tms - in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end - | hol_literal_to_fol HO (pos, tm) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos metis_equal (map hol_term_to_fol_HO tms) - | _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm]) - | hol_literal_to_fol FT (pos, tm) = - (case strip_combterm_comb tm of - (CombConst(("equal", _), _, _), tms) => - metis_lit pos metis_equal (map hol_term_to_fol_FT tms) - | _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm]) - -fun literals_of_hol_term thy mode t = - let val (lits, types_sorts) = literals_of_term thy t in - (map (hol_literal_to_fol mode) lits, types_sorts) - end - -(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) -fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) = - metis_lit pos s [Metis_Term.Var s'] - | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) = - metis_lit pos s [Metis_Term.Fn (s',[])] - -fun has_default_sort _ (TVar _) = false - | has_default_sort ctxt (TFree (x, s)) = - (s = the_default [] (Variable.def_sort ctxt (x, ~1))); - -fun metis_of_tfree tf = - Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf)); - -fun hol_thm_to_fol is_conjecture ctxt mode j old_skolems th = - let - val thy = Proof_Context.theory_of ctxt - val (old_skolems, (mlits, types_sorts)) = - th |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms j old_skolems - ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) - in - if is_conjecture then - (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits), - raw_type_literals_for_types types_sorts, old_skolems) - else - let - val tylits = types_sorts |> filter_out (has_default_sort ctxt) - |> raw_type_literals_for_types - val mtylits = map (metis_of_type_literals false) tylits - in - (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [], - old_skolems) - end - end; - -(* ------------------------------------------------------------------------- *) (* Logic maps manage the interface between HOL and first-order logic. *) (* ------------------------------------------------------------------------- *) @@ -242,56 +99,6 @@ Isa_Reflexive_or_Trivial | Isa_Raw of thm -type metis_problem = - {axioms : (Metis_Thm.thm * isa_thm) list, - tfrees : type_literal list, - old_skolems : (string * term) list} - -fun is_quasi_fol_clause thy = - Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of - -(*Extract TFree constraints from context to include as conjecture clauses*) -fun init_tfrees ctxt = - let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in - Vartab.fold add (#2 (Variable.constraints_of ctxt)) [] - |> raw_type_literals_for_types - end; - -fun const_in_metis c (pred, tm_list) = - let - fun in_mterm (Metis_Term.Var _) = false - | in_mterm (Metis_Term.Fn (nm, tm_list)) = - c = nm orelse exists in_mterm tm_list - in c = pred orelse exists in_mterm tm_list end - -(* ARITY CLAUSE *) -fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = - metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] - | m_arity_cls (TVarLit ((c, _), (s, _))) = - metis_lit false c [Metis_Term.Var s] -(* TrueI is returned as the Isabelle counterpart because there isn't any. *) -fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) = - (TrueI, - Metis_Thm.axiom (Metis_LiteralSet.fromList - (map m_arity_cls (concl_lits :: prem_lits)))); - -(* CLASSREL CLAUSE *) -fun m_class_rel_cls (subclass, _) (superclass, _) = - [metis_lit false subclass [Metis_Term.Var "T"], - metis_lit true superclass [Metis_Term.Var "T"]] -fun class_rel_cls ({subclass, superclass, ...} : class_rel_clause) = - (TrueI, m_class_rel_cls subclass superclass - |> Metis_LiteralSet.fromList |> Metis_Thm.axiom) - -fun type_ext thy tms = - let - val subs = tfree_classes_of_terms tms - val supers = tvar_classes_of_terms tms - val tycons = type_constrs_of_terms thy tms - val (supers', arity_clauses) = make_arity_clauses thy tycons supers - val class_rel_clauses = make_class_rel_clauses thy subs supers' - in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end - val proxy_defs = map (fst o snd o snd) proxy_table val prepare_helper = Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs) @@ -346,92 +153,39 @@ | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem ctxt (mode as Type_Sys type_sys) conj_clauses - fact_clauses = - let - val type_sys = type_sys_from_string type_sys - val explicit_apply = NONE - val clauses = - conj_clauses @ fact_clauses - |> (if polymorphism_of_type_sys type_sys = Polymorphic then - I - else - map (pair 0) - #> rpair ctxt - #-> Monomorph.monomorph Monomorph.all_schematic_consts_of - #> fst #> maps (map (zero_var_indexes o snd))) - val (old_skolems, props) = - fold_rev (fn clause => fn (old_skolems, props) => - clause |> prop_of |> Logic.strip_imp_concl - |> conceal_old_skolem_terms (length clauses) - old_skolems - ||> (fn prop => prop :: props)) - clauses ([], []) +fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses = + let + val type_sys = type_sys_from_string type_sys + val explicit_apply = NONE + val clauses = + conj_clauses @ fact_clauses + |> (if polymorphism_of_type_sys type_sys = Polymorphic then + I + else + map (pair 0) + #> rpair ctxt + #-> Monomorph.monomorph Monomorph.all_schematic_consts_of + #> fst #> maps (map (zero_var_indexes o snd))) + val (old_skolems, props) = + fold_rev (fn clause => fn (old_skolems, props) => + clause |> prop_of |> Logic.strip_imp_concl + |> conceal_old_skolem_terms (length clauses) + old_skolems + ||> (fn prop => prop :: props)) + clauses ([], []) (* val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) *) - val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply - false false props @{prop False} [] + val (atp_problem, _, _, _, _, _, sym_tab) = + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply + false false props @{prop False} [] (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem)) *) - (* "rev" is for compatibility *) - val axioms = - atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) - |> rev - in - (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems}) - end - | prepare_metis_problem ctxt mode conj_clauses fact_clauses = - let - val thy = Proof_Context.theory_of ctxt - (* The modes FO and FT are sticky. HO can be downgraded to FO. *) - val mode = - if mode = HO andalso - forall (forall (is_quasi_fol_clause thy)) - [conj_clauses, fact_clauses] then - FO - else - mode - 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 mode (length axioms) old_skolems - metis_ith - in - {axioms = (mth, Isa_Raw isa_ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} - end; - fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = - {axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees, - old_skolems = old_skolems} - fun add_tfrees {axioms, tfrees, old_skolems} = - {axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree) - (distinct (op =) tfrees) @ axioms, - tfrees = tfrees, old_skolems = old_skolems} - val problem = - {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []} - |> fold (add_thm true o `Meson.make_meta_clause) conj_clauses - |> add_tfrees - |> fold (add_thm false o `Meson.make_meta_clause) fact_clauses - val clause_lists = map (Metis_Thm.clause o #1) (#axioms problem) - fun is_used c = - exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists - val problem = - if mode = FO then - problem - else - let - val helper_ths = - helper_table - |> filter (is_used o prefix const_prefix o fst o fst) - |> maps (fn ((_, needs_full_types), thms) => - if needs_full_types andalso mode <> FT then [] - else map (`prepare_helper) thms) - in problem |> fold (add_thm false) helper_ths end - val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses)) - in (mode, Symtab.empty, fold add_type_thm type_ths problem) end + (* "rev" is for compatibility *) + val axioms = + atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd) + |> rev + in (sym_tab, axioms, old_skolems) end end; diff -r 77c432fe28ff -r 050a03afe024 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 06 20:56:06 2011 +0200 @@ -417,8 +417,8 @@ in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor Metis = - Metis_Tactics.new_metis_tac [Metis_Tactics.default_unsound_type_sys] - | tac_for_reconstructor MetisFT = Metis_Tactics.new_metisFT_tac + Metis_Tactics.metis_tac [Metis_Tactics.default_unsound_type_sys] + | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac | tac_for_reconstructor _ = raise Fail "unexpected reconstructor" fun timed_reconstructor reconstructor debug timeout ths = diff -r 77c432fe28ff -r 050a03afe024 src/HOL/ex/CASC_Setup.thy --- a/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/ex/CASC_Setup.thy Mon Jun 06 20:56:06 2011 +0200 @@ -52,7 +52,7 @@ THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" - (ALLGOALS (Metis_Tactics.new_metis_tac [] ctxt [])) + (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) ORELSE diff -r 77c432fe28ff -r 050a03afe024 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:36:36 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Mon Jun 06 20:56:06 2011 +0200 @@ -70,7 +70,7 @@ in case run_atp false timeout i i ctxt th atp of SOME facts => - Metis_Tactics.new_metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th + Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty end