# HG changeset patch # User paulson # Date 1176999791 -7200 # Node ID abfdccaed08531e0e504b6bb8481f6c89e70f18b # Parent 8bcc8809ed3b55b15fc1cd6705991b892b2343bd trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions diff -r 8bcc8809ed3b -r abfdccaed085 src/HOL/Tools/res_atp.ML --- 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 diff -r 8bcc8809ed3b -r abfdccaed085 src/HOL/Tools/res_axioms.ML --- 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) diff -r 8bcc8809ed3b -r abfdccaed085 src/HOL/Tools/res_reconstruct.ML --- 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); diff -r 8bcc8809ed3b -r abfdccaed085 src/HOL/ex/Classical.thy --- 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 \ S | V \ S | V = U" by (meson 10 2) - have 13: "!!U V. U \ S | S \ V | U = Set_XsubsetI_sko1_ S V" + have 13: "!!U V. U \ S | S \ V | U = sko_Set_XsubsetI_1_ S V" by (meson subsetI 11) - have 14: "!!U V. S \ U | S \ V | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S V" + have 14: "!!U V. S \ U | S \ V | sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S V" by (meson subsetI 13) - have 29: "!!U V. S \ U | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S {V}" + have 29: "!!U V. S \ 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} \ {V} | S \ {V}" + have 82: "sko_Set_XsubsetI_1_ S {U} \ {V} | S \ {V}" apply (insert 58 [of U V], erule ssubst) by (meson 58 subsetI) - have 85: "Set_XsubsetI_sko1_ S {U} \ {V}" + have 85: "sko_Set_XsubsetI_1_ S {U} \ {V}" by (meson 1 82) show False by (meson insertI1 85) @@ -874,12 +874,12 @@ fix S :: "'a set set" assume 1: "\Z. ~ (S \ {Z})" and 2: "\X Y. X \ S | Y \ S | X \ Y" - have 13: "!!U V. U \ S | S \ V | U = Set_XsubsetI_sko1_ S V" + have 13: "!!U V. U \ S | S \ 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} \ {V} | S \ {V}" + have 82: "sko_Set_XsubsetI_1_ S {U} \ {V} | S \ {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: "\Z. ~ (S \ {Z})" and 2: "\X Y. X \ S | Y \ S | X \ 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)