trying to make single-step proofs work better, especially if they contain
abstraction functions. Uniform names for Skolem and Abstraction functions
--- a/src/HOL/Tools/res_atp.ML Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Apr 19 18:23:11 2007 +0200
@@ -718,7 +718,7 @@
(*Called by the oracle-based methods declared in res_atp_methods.ML*)
fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
let val conj_cls = make_clauses conjectures
- |> ResAxioms.assume_abstract_list true |> Meson.finish_cnf
+ |> ResAxioms.assume_abstract_list "subgoal" |> Meson.finish_cnf
val hyp_cls = cnf_hyps_thms ctxt
val goal_cls = conj_cls@hyp_cls
val goal_tms = map prop_of goal_cls
--- a/src/HOL/Tools/res_axioms.ML Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Thu Apr 19 18:23:11 2007 +0200
@@ -13,11 +13,10 @@
val meta_cnf_axiom : thm -> thm list
val pairname : thm -> string * thm
val skolem_thm : thm -> thm list
- val to_nnf : thm -> thm
val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
val meson_method_setup : theory -> theory
val setup : theory -> theory
- val assume_abstract_list: bool -> thm list -> thm list
+ val assume_abstract_list: string -> thm list -> thm list
val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
@@ -97,7 +96,7 @@
let val nref = ref 0
fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
(*Existential: declare a Skolem function, then insert into body and continue*)
- let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref))
+ let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
val args = term_frees xtp (*get the formal parameter list*)
val Ts = map type_of args
val cT = Ts ---> T
@@ -122,14 +121,16 @@
in dec_sko (prop_of th) (thy,[]) end;
(*Traverse a theorem, accumulating Skolem function definitions.*)
-fun assume_skofuns th =
- let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
+fun assume_skofuns s th =
+ let val sko_count = ref 0
+ fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
(*Existential: declare a Skolem function, then insert into body and continue*)
let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
val args = term_frees xtp \\ skos (*the formal parameters*)
val Ts = map type_of args
val cT = Ts ---> T
- val c = Free (gensym "sko_", cT)
+ val id = "sko_" ^ s ^ "_" ^ Int.toString (inc sko_count)
+ val c = Free (id, cT)
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
(*Forms a lambda-abstraction over the formal parameters*)
@@ -244,13 +245,14 @@
(*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
prefix for the constants. Resulting theory is returned in the first theorem. *)
-fun declare_absfuns th =
- let fun abstract thy ct =
+fun declare_absfuns s th =
+ let val nref = ref 0
+ fun abstract thy ct =
if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
else
case term_of ct of
Abs _ =>
- let val cname = Name.internal (gensym "abs_");
+ let val cname = Name.internal ("llabs_" ^ s ^ "_" ^ Int.toString (inc nref))
val _ = assert_eta_free ct;
val (cvs,cta) = dest_abs_list ct
val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
@@ -319,9 +321,8 @@
fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
| valid_name defs _ = false;
-(*isgoal holds if "th" is a conjecture. Then the assumption functions are counted from 1
- rather than produced using gensym, as they need to be repeatable.*)
-fun assume_absfuns isgoal th =
+(*s is the theorem name (hint) or the word "subgoal"*)
+fun assume_absfuns s th =
let val thy = theory_of_thm th
val cterm = cterm_of thy
val abs_count = ref 0
@@ -353,8 +354,7 @@
| [] =>
let val Ts = map type_of args
val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
- val id = if isgoal then "abs_" ^ Int.toString (inc abs_count)
- else gensym "abs_"
+ val id = "llabs_" ^ s ^ "_" ^ Int.toString (inc abs_count)
val c = Free (id, const_ty)
val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
|> mk_object_eq |> strip_lambdas (length args)
@@ -419,65 +419,66 @@
|> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
(*Generate Skolem functions for a theorem supplied in nnf*)
-fun skolem_of_nnf th =
- map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
+fun skolem_of_nnf s th =
+ map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
fun assert_lambda_free ths msg =
case filter (not o lambda_free o prop_of) ths of
[] => ()
- | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
+ | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths'));
-fun assume_abstract isgoal th =
+fun assume_abstract s th =
if lambda_free (prop_of th) then [th]
- else th |> Drule.eta_contraction_rule |> assume_absfuns isgoal
+ else th |> Drule.eta_contraction_rule |> assume_absfuns s
|> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
(*Replace lambdas by assumed function definitions in the theorems*)
-fun assume_abstract_list isgoal ths =
- if abstract_lambdas then List.concat (map (assume_abstract isgoal) ths)
+fun assume_abstract_list s ths =
+ if abstract_lambdas then List.concat (map (assume_abstract s) ths)
else map Drule.eta_contraction_rule ths;
(*Replace lambdas by declared function definitions in the theorems*)
-fun declare_abstract' (thy, []) = (thy, [])
- | declare_abstract' (thy, th::ths) =
+fun declare_abstract' s (thy, []) = (thy, [])
+ | declare_abstract' s (thy, th::ths) =
let val (thy', th_defs) =
if lambda_free (prop_of th) then (thy, [th])
else
th |> zero_var_indexes |> freeze_thm
- |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns
+ |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
- val (thy'', ths') = declare_abstract' (thy', ths)
+ val (thy'', ths') = declare_abstract' s (thy', ths)
in (thy'', th_defs @ ths') end;
-fun declare_abstract (thy, ths) =
- if abstract_lambdas then declare_abstract' (thy, ths)
+fun declare_abstract s (thy, ths) =
+ if abstract_lambdas then declare_abstract' s (thy, ths)
else (thy, map Drule.eta_contraction_rule ths);
-(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolem_thm th =
- let val nnfth = to_nnf th
- in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list false |> Meson.finish_cnf
- end
- handle THM _ => [];
-
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (NameSpace.explode s);
+fun fake_name th =
+ if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
+ else gensym "unknown_thm_";
+
+(*Skolemize a named theorem, with Skolem functions as additional premises.*)
+fun skolem_thm th =
+ let val nnfth = to_nnf th and s = fake_name th
+ in Meson.make_cnf (skolem_of_nnf s nnfth) nnfth |> assume_abstract_list s |> Meson.finish_cnf
+ end
+ handle THM _ => [];
+
(*Declare Skolem functions for a theorem, supplied in nnf and with its name.
It returns a modified theory, unless skolemization fails.*)
fun skolem thy th =
- let val cname = (if PureThy.has_name_hint th
- then flatten_name (PureThy.get_name_hint th) else gensym "")
- val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
- in Option.map
- (fn nnfth =>
- let val (thy',defs) = declare_skofuns cname nnfth thy
+ Option.map
+ (fn (nnfth, s) =>
+ let val _ = Output.debug (fn () => "skolemizing " ^ s ^ ": ")
+ val (thy',defs) = declare_skofuns s nnfth thy
val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
- val (thy'',cnfs') = declare_abstract (thy',cnfs)
+ val (thy'',cnfs') = declare_abstract s (thy',cnfs)
in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
end)
- (SOME (to_nnf th) handle THM _ => NONE)
- end;
+ (SOME (to_nnf th, fake_name th) handle THM _ => NONE);
structure ThmCache = TheoryDataFun
(struct
@@ -596,19 +597,33 @@
fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
-fun aconv_ct (t,u) = (Thm.term_of t) aconv (Thm.term_of u);
+(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
+fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
+ | is_absko _ = false;
+
+fun is_okdef xs (Const ("==", _) $ t $ u) = (*Definition of Free, not in certain terms*)
+ is_Free t andalso not (member (op aconv) xs t)
+ | is_okdef _ _ = false
-(*Expand all *new* definitions (presumably of abstraction or Skolem functions) in a proof state.*)
-fun expand_defs_tac ths ths' st =
- let val hyps = foldl (gen_union aconv_ct) [] (map (#hyps o crep_thm) ths)
- val remove_hyps = filter (not o member aconv_ct hyps)
- val hyps' = foldl (gen_union aconv_ct) [] (map (remove_hyps o #hyps o crep_thm) (st::ths'))
- in PRIMITIVE (LocalDefs.expand (filter (can dest_equals) hyps')) st end;
+fun expand_defs_tac st0 st =
+ let val hyps0 = #hyps (rep_thm st0)
+ val hyps = #hyps (crep_thm st)
+ val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
+ val defs = filter (is_absko o Thm.term_of) newhyps
+ val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
+ (map Thm.term_of hyps)
+ val fixed = term_frees (concl_of st) @
+ foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
+ in Output.debug (fn _ => "expand_defs_tac: " ^ string_of_thm st);
+ Output.debug (fn _ => " st0: " ^ string_of_thm st0);
+ Output.debug (fn _ => " defs: " ^ commas (map string_of_cterm defs));
+ Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st]
+ end;
-fun meson_general_tac ths i =
- let val _ = Output.debug (fn () => "Meson called with theorems " ^ cat_lines (map string_of_thm ths))
- val ths' = cnf_rules_of_ths ths
- in Meson.meson_claset_tac ths' HOL_cs i THEN expand_defs_tac ths ths' end;
+
+fun meson_general_tac ths i st0 =
+ let val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map string_of_thm ths))
+ in (Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
val meson_method_setup = Method.add_methods
[("meson", Method.thms_args (fn ths =>
@@ -633,7 +648,7 @@
it can introduce TVars, which are useless in conjecture clauses.*)
val no_tvars = null o term_tvars o prop_of;
-val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list true o make_clauses;
+val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list "subgoal" o make_clauses;
fun neg_conjecture_clauses st0 n =
let val st = Seq.hd (neg_skolemize_tac n st0)
--- a/src/HOL/Tools/res_reconstruct.ML Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Apr 19 18:23:11 2007 +0200
@@ -186,7 +186,8 @@
(*Invert the table of translations between Isabelle and ATPs*)
val const_trans_table_inv =
- Symtab.make (map swap (Symtab.dest ResClause.const_trans_table));
+ Symtab.update ("fequal", "op =")
+ (Symtab.make (map swap (Symtab.dest ResClause.const_trans_table)));
fun invert_const c =
case Symtab.lookup const_trans_table_inv c of
@@ -209,9 +210,7 @@
| Br (a,ts) =>
case strip_prefix ResClause.const_prefix a of
SOME "equal" =>
- if length ts = 2 then
- list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
- else raise STREE t (*equality needs two arguments*)
+ list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts)
| SOME b =>
let val c = invert_const b
val nterms = length ts - num_typargs thy c
@@ -376,10 +375,10 @@
(*No "real" literals means only type information*)
fun eq_types t = t aconv (HOLogic.mk_Trueprop HOLogic.true_const);
-fun replace_dep (old, new) dep = if dep=old then new else [dep];
+fun replace_dep (old:int, new) dep = if dep=old then new else [dep];
-fun replace_deps (old, new) (lno, t, deps) =
- (lno, t, List.concat (map (replace_dep (old, new)) deps));
+fun replace_deps (old:int, new) (lno, t, deps) =
+ (lno, t, foldl (op union_int) [] (map (replace_dep (old, new)) deps));
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
@@ -411,6 +410,9 @@
| add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines
and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines);
+fun bad_free (Free (a,_)) = String.isPrefix "llabs_" a orelse String.isPrefix "sko_" a
+ | bad_free _ = false;
+
(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies.
To further compress proofs, setting modulus:=n deletes every nth line, and nlines
counts the number of proof lines processed so far.
@@ -421,7 +423,8 @@
| add_wanted_prfline (line, (nlines, [])) = (nlines, [line]) (*final line must be kept*)
| add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
if eq_types t orelse not (null (term_tvars t)) orelse
- length deps < 2 orelse nlines mod !modulus <> 0
+ length deps < 2 orelse nlines mod !modulus <> 0 orelse
+ exists bad_free (term_frees t)
then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
else (nlines+1, (lno, t, deps) :: lines);
@@ -434,7 +437,7 @@
fun fix lno = if lno <= Vector.length thm_names
then SOME(Vector.sub(thm_names,lno-1))
else AList.lookup op= deps_map lno;
- in (lname, t, List.mapPartial fix deps) ::
+ in (lname, t, List.mapPartial fix (distinct (op=) deps)) ::
stringify_deps thm_names ((lno,lname)::deps_map) lines
end;
@@ -547,7 +550,7 @@
(trace ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
" num of clauses is " ^ string_of_int (Vector.length thm_names));
signal_success probfile toParent ppid
- ("Try this proof method: \n" ^ rules_to_metis (getax proofstr thm_names))
+ ("Try this command: \n apply " ^ rules_to_metis (getax proofstr thm_names))
)
handle e => (*FIXME: exn handler is too general!*)
(trace ("\nprover_lemma_list_aux: In exception handler: " ^ Toplevel.exn_message e);
--- a/src/HOL/ex/Classical.thy Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/ex/Classical.thy Thu Apr 19 18:23:11 2007 +0200
@@ -849,19 +849,19 @@
by (meson equalityI 2)
have 11: "!!U V. U \<notin> S | V \<notin> S | V = U"
by (meson 10 2)
- have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
+ have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
by (meson subsetI 11)
- have 14: "!!U V. S \<subseteq> U | S \<subseteq> V | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S V"
+ have 14: "!!U V. S \<subseteq> U | S \<subseteq> V | sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S V"
by (meson subsetI 13)
- have 29: "!!U V. S \<subseteq> U | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S {V}"
+ have 29: "!!U V. S \<subseteq> U | sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S {V}"
by (meson 1 14)
- have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+ have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
by (meson 1 29)
(*hacked here while we wait for Metis: !!U V complicates proofs.*)
- have 82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+ have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
apply (insert 58 [of U V], erule ssubst)
by (meson 58 subsetI)
- have 85: "Set_XsubsetI_sko1_ S {U} \<notin> {V}"
+ have 85: "sko_Set_XsubsetI_1_ S {U} \<notin> {V}"
by (meson 1 82)
show False
by (meson insertI1 85)
@@ -874,12 +874,12 @@
fix S :: "'a set set"
assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
- have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
+ have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
by (meson subsetI equalityI 2)
- have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+ have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
by (meson 1 subsetI 13)
(*hacked here while we wait for Metis: !!U V complicates proofs.*)
- have 82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+ have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
apply (insert 58 [of U V], erule ssubst)
by (meson 58 subsetI)
show False
@@ -893,7 +893,7 @@
fix S :: "'a set set"
assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
- have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+ have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
by (meson 1 subsetI_0 equalityI 2)
show False
by (iprover intro: subsetI_1 insertI1 1 58 elim: ssubst)