--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Thu Sep 30 20:44:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 10:39:51 2010 +0200
@@ -12,7 +12,9 @@
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
- val cnf_axiom : theory -> bool -> int -> thm -> thm option * thm list
+ val cluster_for_zapped_var_name : string -> int * bool
+ val cnf_axiom :
+ theory -> bool -> int -> thm -> (thm * term) option * thm list
val meson_general_tac : Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
@@ -227,13 +229,17 @@
val eqth = eqth RS @{thm TruepropI}
in Thm.equal_elim eqth th end
-fun zapped_var_name ax_no (skolem, cluster_no) s =
+fun zapped_var_name ax_no (cluster_no, skolem) s =
(if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
+fun cluster_for_zapped_var_name s =
+ (nth (space_explode "_" s) 1 |> Int.fromString |> the,
+ String.isPrefix new_skolem_var_prefix s)
+
fun zap_quantifiers ax_no =
let
- fun conv (cluster as (cluster_skolem, cluster_no)) pos ct =
+ fun conv (cluster as (cluster_no, cluster_skolem)) pos ct =
ct |> (case term_of ct of
Const (s, _) $ Abs (s', _, _) =>
if s = @{const_name all} orelse s = @{const_name All} orelse
@@ -242,7 +248,7 @@
val skolem = (pos = (s = @{const_name Ex}))
val cluster =
if skolem = cluster_skolem then cluster
- else (skolem, cluster_no |> cluster_skolem ? Integer.add 1)
+ else (cluster_no |> cluster_skolem ? Integer.add 1, skolem)
in
Thm.dest_comb #> snd
#> Thm.dest_abs (SOME (zapped_var_name ax_no cluster s'))
@@ -270,7 +276,7 @@
Conv.all_conv
| _ => Conv.all_conv)
in
- conv (true, 0) true #> Drule.export_without_context
+ conv (0, true) true #> Drule.export_without_context
#> cprop_of #> Thm.dest_equals #> snd
end
@@ -329,7 +335,6 @@
|> (fn ([], _) =>
clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
| p => p)
- val export = Variable.export ctxt ctxt0
fun intr_imp ct th =
Thm.instantiate ([], map (pairself (cterm_of @{theory}))
[(Var (("i", 1), @{typ nat}),
@@ -337,10 +342,12 @@
@{thm skolem_COMBK_D}
RS Thm.implies_intr ct th
in
- (opt |> Option.map (singleton export o fst),
+ (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
+ ##> (term_of #> HOLogic.dest_Trueprop
+ #> singleton (Variable.export_terms ctxt ctxt0))),
cnf_ths |> map (introduce_combinators_in_theorem
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
- |> export
+ |> Variable.export ctxt ctxt0
|> Meson.finish_cnf
|> map Thm.close_derivation)
end
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 30 20:44:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Oct 01 10:39:51 2010 +0200
@@ -59,11 +59,11 @@
horribly because of the mildly higher-order nature of the unification
problems. Typical constraints are of the form "?x a b =?= b", where "a" and
"b" are goal parameters. *)
-fun unify_one_prem_with_concl thy i th =
+fun unify_prem_with_concl thy i th =
let
val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
- val prems = Logic.strip_assums_hyp goal
- val concl = Logic.strip_assums_concl goal
+ val prem = goal |> Logic.strip_assums_hyp |> the_single
+ val concl = goal |> Logic.strip_assums_concl
fun add_types Tp instT =
if exists (curry (op =) Tp) instT then instT
else Tp :: map (apsnd (typ_subst_atomic [Tp])) instT
@@ -108,47 +108,62 @@
| (Var _, _) => add_terms (t, u)
| (_, Var _) => add_terms (u, t)
| _ => if untyped_aconv t u then I else raise TERM ("unify_terms", [t, u])
- fun unify_prem prem =
- let
- val inst = [] |> unify_terms (prem, concl)
- val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
- Syntax.string_of_term @{context} t ^ " |-> " ^
- Syntax.string_of_term @{context} u) inst))
- val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
- handle TERM _ => I) inst []
- val inst = inst |> map (pairself (subst_atomic_types instT))
- val cinstT = instT |> map (pairself (ctyp_of thy))
- val cinst = inst |> map (pairself (cterm_of thy))
- in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
- in
- case prems of
- [prem] => unify_prem prem
- | _ =>
- case fold (fn prem => fn th as SOME _ => th
- | NONE => try unify_prem prem) prems NONE of
- SOME th => th
- | NONE => raise Fail "unify_one_prem_with_concl"
- end
+
+ val inst = [] |> unify_terms (prem, concl)
+ val _ = trace_msg (fn () => cat_lines (map (fn (t, u) =>
+ Syntax.string_of_term @{context} t ^ " |-> " ^
+ Syntax.string_of_term @{context} u) inst))
+ val instT = fold (fn Tp => unify_types (pairself fastype_of Tp)
+ handle TERM _ => I) inst []
+ val inst = inst |> map (pairself (subst_atomic_types instT))
+ val cinstT = instT |> map (pairself (ctyp_of thy))
+ val cinst = inst |> map (pairself (cterm_of thy))
+ in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
+ handle Empty => th (* ### FIXME *)
(* Attempts to derive the theorem "False" from a theorem of the form
"P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
must be eliminated first. *)
-fun discharge_skolem_premises ctxt axioms premises_imp_false =
- if prop_of premises_imp_false aconv @{prop False} then
- premises_imp_false
- else
- let val thy = ProofContext.theory_of ctxt in
+fun discharge_skolem_premises ctxt axioms prems_imp_false =
+ case prop_of prems_imp_false of
+ @{prop False} => prems_imp_false
+ | prems_imp_false_prop =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun match_term p =
+ let
+ val (tyenv, tenv) =
+ Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
+ val tsubst =
+ tenv |> Vartab.dest
+ |> sort (prod_ord int_ord bool_ord
+ o pairself (Meson_Clausify.cluster_for_zapped_var_name
+ o fst o fst))
+ |> map (Meson.term_pair_of
+ #> pairself (Envir.subst_term_types tyenv))
+ in (tyenv, tsubst) end
+ fun subst_info_for_prem assm_no prem =
+ case prem of
+ _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
+ let val ax_no = num |> HOLogic.dest_number |> snd in
+ (ax_no, (assm_no, match_term (nth axioms ax_no |> snd, t)))
+ end
+ | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
+ [prem])
+ val prems = Logic.strip_imp_prems prems_imp_false_prop
+ val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems
+ in
Goal.prove ctxt [] [] @{prop False}
- (K (cut_rules_tac axioms 1
+ (K (cut_rules_tac (map fst axioms) 1
THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
(* two copies are better than one (FIXME) *)
THEN etac @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} 1
THEN TRY (REPEAT_ALL_NEW (etac @{thm allE}) 1)
- THEN match_tac [premises_imp_false] 1
+ THEN match_tac [prems_imp_false] 1
THEN DETERM_UNTIL_SOLVED
(rtac @{thm skolem_COMBK_I} 1
- THEN PRIMITIVE (unify_one_prem_with_concl thy 1)
+ THEN PRIMITIVE (unify_prem_with_concl thy 1)
THEN assume_tac 1)))
end