52 exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) |
52 exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) |
53 |
53 |
54 (*Determining which axiom clauses are actually used*) |
54 (*Determining which axiom clauses are actually used*) |
55 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
55 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
56 | used_axioms _ _ = NONE |
56 | used_axioms _ _ = NONE |
|
57 |
|
58 fun cterm_from_metis ctxt sym_tab tm = |
|
59 let val thy = Proof_Context.theory_of ctxt in |
|
60 tm |> hol_term_from_metis MX sym_tab ctxt |
|
61 |> Syntax.check_term |
|
62 (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |
|
63 |> cterm_of thy |
|
64 end |
|
65 |
|
66 (* Lightweight predicate type information comes in two flavors, "t = t'" and |
|
67 "t => t'", where "t" and "t'" are the same term modulo type tags. |
|
68 In Isabelle, type tags are stripped away, so we are left with "t = t" or |
|
69 "t => t". *) |
|
70 fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth = |
|
71 (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of |
|
72 [(true, (_, [_, tm]))] => |
|
73 tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive |
|
74 RS @{thm meta_eq_to_obj_eq} |
|
75 | [_, (_, tm)] => |
|
76 tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume |
|
77 | _ => raise Fail "unexpected tags sym clause") |
|
78 |> Meson.make_meta_clause |
57 |
79 |
58 val clause_params = |
80 val clause_params = |
59 {ordering = Metis_KnuthBendixOrder.default, |
81 {ordering = Metis_KnuthBendixOrder.default, |
60 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
82 orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
61 orderTerms = true} |
83 orderTerms = true} |
86 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
108 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
87 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
109 val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
88 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
110 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
89 val (mode, sym_tab, {axioms, old_skolems, ...}) = |
111 val (mode, sym_tab, {axioms, old_skolems, ...}) = |
90 prepare_metis_problem ctxt mode type_sys cls ths |
112 prepare_metis_problem ctxt mode type_sys cls ths |
|
113 val axioms = |
|
114 axioms |> map |
|
115 (fn (mth, SOME th) => (mth, th) |
|
116 | (mth, NONE) => |
|
117 (mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth)) |
91 val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") |
118 val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") |
92 val thms = map #1 axioms |
119 val thms = map #1 axioms |
93 val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms |
120 val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms |
94 val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) |
121 val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) |
95 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
122 val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |