# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID b0b30df60056772828c49c0d47a0a2826cea9eab # Parent f6331d78512832d2c638489ce25f107264a0b8b6 tuning diff -r f6331d785128 -r b0b30df60056 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200 @@ -85,7 +85,7 @@ val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss val (mode, {axioms, tfrees, old_skolems}) = - prepare_metis_problem mode ctxt cls thss + prepare_metis_problem ctxt mode cls thss val _ = if null tfrees then () else (trace_msg ctxt (fn () => "TFREE CLAUSES"); app (fn TyLitFree ((s, _), (s', _)) => diff -r f6331d785128 -r b0b30df60056 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200 @@ -25,7 +25,7 @@ val reveal_old_skolem_terms : (string * term) list -> term -> term val string_of_mode : mode -> string val prepare_metis_problem : - mode -> Proof.context -> thm list -> thm list list -> mode * metis_problem + Proof.context -> mode -> thm list -> thm list list -> mode * metis_problem end structure Metis_Translate : METIS_TRANSLATE = @@ -247,18 +247,6 @@ |> raw_type_literals_for_types end; -(*Insert non-logical axioms corresponding to all accumulated TFrees*) -fun add_tfrees {axioms, tfrees, old_skolems} : metis_problem = - {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ - axioms, - tfrees = tfrees, old_skolems = old_skolems} - -(*transform isabelle type / arity clause to metis clause *) -fun add_type_thm [] lmap = lmap - | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, old_skolems} = - add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees, - old_skolems = old_skolems} - fun const_in_metis c (pred, tm_list) = let fun in_mterm (Metis_Term.Var _) = false @@ -279,33 +267,39 @@ (* 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"]]; + [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, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass))); + (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_consts_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; + let + val subs = tfree_classes_of_terms tms + val supers = tvar_classes_of_terms tms + val tycons = type_consts_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 (* Function to generate metis clauses, including comb and type clauses *) -fun prepare_metis_problem New ctxt cls thss = - error "Not implemented yet" - | prepare_metis_problem mode ctxt cls thss = +fun prepare_metis_problem ctxt New conj_clauses fact_clausess = + let + val x = 1 + in + error "Not implemented yet" + end + | prepare_metis_problem ctxt mode conj_clauses fact_clausess = 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)) (cls :: thss) then + forall (forall (is_quasi_fol_clause thy)) + (conj_clauses :: fact_clausess) then FO else mode - (*transform isabelle clause to metis clause *) fun add_thm is_conjecture (isa_ith, metis_ith) {axioms, tfrees, old_skolems} : metis_problem = let @@ -313,19 +307,27 @@ hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems metis_ith in - {axioms = (mth, isa_ith) :: axioms, - tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems} + {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 `Meson.make_meta_clause) cls - |> add_tfrees - |> fold (fold (add_thm false o `Meson.make_meta_clause)) thss - val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap) + fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} = + {axioms = (mth, ith) :: axioms, tfrees = tfrees, + old_skolems = old_skolems} + fun add_tfrees {axioms, tfrees, old_skolems} = + {axioms = + map (rpair 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 (fold (add_thm false o `Meson.make_meta_clause)) fact_clausess + 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 lmap = + val problem = if mode = FO then - lmap + problem else let val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def @@ -340,10 +342,9 @@ |> maps (fn (_, (needs_full_types, 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) - end + in problem |> fold (add_thm false) helper_ths end + val type_ths = + type_ext thy (maps (map prop_of) (conj_clauses :: fact_clausess)) + in (mode, fold add_type_thm type_ths problem) end end;