# HG changeset patch # User blanchet # Date 1285799377 -7200 # Node ID 25a339e1ff9bf0be8a7a2448f99eb773a7f1618c # Parent 699a20afc5bd54ca69dffb9a05135d4f1a3595ee move functions closer to where they're used diff -r 699a20afc5bd -r 25a339e1ff9b src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 30 00:12:11 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Thu Sep 30 00:29:37 2010 +0200 @@ -352,6 +352,21 @@ get (n+1) xs in get 1 end +(* Permute a rule's premises to move the i-th premise to the last position. *) +fun make_last i th = + let val n = nprems_of th + in if 1 <= i andalso i <= n + then Thm.permute_prems (i-1) 1 th + else raise THM("select_literal", i, [th]) + end; + +(* 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] + +(* 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_inf ctxt mode old_skolems thpairs atm th1 th2 = let val thy = ProofContext.theory_of ctxt @@ -378,8 +393,7 @@ handle Empty => raise Fail "Failed to find literal in th2" val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) in - resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2 - i_th2 + resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 end end; @@ -502,7 +516,17 @@ | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => equality_inf ctxt mode old_skolems f_lit f_p f_r -fun is_real_literal (_, (c, _)) = not (String.isPrefix class_prefix c) +fun flexflex_first_order th = + case Thm.tpairs_of th of + [] => th + | pairs => + let val thy = theory_of_thm th + val (_, tenv) = + fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) + val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) + val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th + in th' end + handle THM _ => th; fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = let @@ -510,7 +534,7 @@ val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) val th = step ctxt mode old_skolems thpairs (fol_th, inf) - |> Meson.flexflex_first_order + |> flexflex_first_order val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) val _ = trace_msg (fn () => "=============================================") in (fol_th, th) :: thpairs end diff -r 699a20afc5bd -r 25a339e1ff9b src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Sep 30 00:12:11 2010 +0200 +++ b/src/HOL/Tools/meson.ML Thu Sep 30 00:29:37 2010 +0200 @@ -9,7 +9,6 @@ sig val trace: bool Unsynchronized.ref val term_pair_of: indexname * (typ * 'a) -> term * 'a - val flexflex_first_order: thm -> thm val size_of_subgoals: thm -> int val has_too_many_clauses: Proof.context -> term -> bool val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context @@ -37,9 +36,6 @@ val make_meta_clause: thm -> thm val make_meta_clauses: thm list -> thm list val meson_tac: Proof.context -> thm list -> int -> tactic - val negate_head: thm -> thm - val select_literal: int -> thm -> thm - val skolemize_tac: Proof.context -> int -> tactic val setup: theory -> theory end @@ -110,18 +106,6 @@ SOME th => th | NONE => raise THM ("first_order_resolve", 0, [thA, thB])) -fun flexflex_first_order th = - case Thm.tpairs_of th of - [] => th - | pairs => - let val thy = theory_of_thm th - val (_, tenv) = - fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - val t_pairs = map term_pair_of (Vartab.dest tenv) - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th - in th' end - handle THM _ => th; - (*Forward proof while preserving bound variables names*) fun rename_bvs_RS th rl = let val th' = th RS rl @@ -694,37 +678,4 @@ name_thms "MClause#" (distinct Thm.eq_thm_prop (map make_meta_clause ths)); -(*Permute a rule's premises to move the i-th premise to the last position.*) -fun make_last i th = - let val n = nprems_of th - in if 1 <= i andalso i <= n - then Thm.permute_prems (i-1) 1 th - else raise THM("select_literal", i, [th]) - end; - -(*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]; - -(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*) -fun select_literal i cl = negate_head (make_last i cl); - - -(*Top-level Skolemization. Allows part of the conversion to clauses to be - expressed as a tactic (or Isar method). Each assumption of the selected - goal is converted to NNF and then its existential quantifiers are pulled - to the front. Finally, all existential quantifiers are eliminated, - leaving !!-quantified variables. Perhaps Safe_tac should follow, but it - might generate many subgoals.*) - -fun skolemize_tac ctxt = SUBGOAL (fn (goal, i) => - let val ts = Logic.strip_assums_hyp goal - in - EVERY' - [Misc_Legacy.METAHYPS (fn hyps => - (cut_facts_tac (skolemize_nnf_list ctxt hyps) 1 - THEN REPEAT (etac exE 1))), - REPEAT_DETERM_N (length ts) o (etac thin_rl)] i - end); - end;