Fixes for proof reconstruction, especially involving abstractions and definitions
1.1 --- a/src/HOL/Tools/meson.ML Tue Apr 17 21:06:59 2007 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Wed Apr 18 11:14:09 2007 +0200
1.3 @@ -541,11 +541,6 @@
1.4 cut_facts_tac (map (skolemize o make_nnf) prems) THEN'
1.5 REPEAT o (etac exE);
1.6
1.7 -(*Expand all definitions (presumably of Skolem functions) in a proof state.*)
1.8 -fun expand_defs_tac st =
1.9 - let val defs = filter (can dest_equals) (#hyps (crep_thm st))
1.10 - in PRIMITIVE (LocalDefs.expand defs) st end;
1.11 -
1.12 (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
1.13 Function mkcl converts theorems to clauses.*)
1.14 fun MESON mkcl cltac i st =
1.15 @@ -553,9 +548,8 @@
1.16 (EVERY [rtac ccontr 1,
1.17 METAHYPS (fn negs =>
1.18 EVERY1 [skolemize_prems_tac negs,
1.19 - METAHYPS (cltac o mkcl)]) 1,
1.20 - expand_defs_tac]) i st
1.21 - handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.22 + METAHYPS (cltac o mkcl)]) 1]) i st
1.23 + handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
1.24
1.25 (** Best-first search versions **)
1.26
2.1 --- a/src/HOL/Tools/res_atp.ML Tue Apr 17 21:06:59 2007 +0200
2.2 +++ b/src/HOL/Tools/res_atp.ML Wed Apr 18 11:14:09 2007 +0200
2.3 @@ -718,7 +718,7 @@
2.4 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
2.5 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
2.6 let val conj_cls = make_clauses conjectures
2.7 - |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
2.8 + |> ResAxioms.assume_abstract_list true |> Meson.finish_cnf
2.9 val hyp_cls = cnf_hyps_thms ctxt
2.10 val goal_cls = conj_cls@hyp_cls
2.11 val goal_tms = map prop_of goal_cls
3.1 --- a/src/HOL/Tools/res_axioms.ML Tue Apr 17 21:06:59 2007 +0200
3.2 +++ b/src/HOL/Tools/res_axioms.ML Wed Apr 18 11:14:09 2007 +0200
3.3 @@ -17,7 +17,7 @@
3.4 val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
3.5 val meson_method_setup : theory -> theory
3.6 val setup : theory -> theory
3.7 - val assume_abstract_list: thm list -> thm list
3.8 + val assume_abstract_list: bool -> thm list -> thm list
3.9 val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
3.10 val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
3.11 val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
3.12 @@ -319,9 +319,12 @@
3.13 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
3.14 | valid_name defs _ = false;
3.15
3.16 -fun assume_absfuns th =
3.17 +(*isgoal holds if "th" is a conjecture. Then the assumption functions are counted from 1
3.18 + rather than produced using gensym, as they need to be repeatable.*)
3.19 +fun assume_absfuns isgoal th =
3.20 let val thy = theory_of_thm th
3.21 val cterm = cterm_of thy
3.22 + val abs_count = ref 0
3.23 fun abstract ct =
3.24 if lambda_free (term_of ct) then (reflexive ct, [])
3.25 else
3.26 @@ -350,7 +353,9 @@
3.27 | [] =>
3.28 let val Ts = map type_of args
3.29 val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
3.30 - val c = Free (gensym "abs_", const_ty)
3.31 + val id = if isgoal then "abs_" ^ Int.toString (inc abs_count)
3.32 + else gensym "abs_"
3.33 + val c = Free (id, const_ty)
3.34 val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
3.35 |> mk_object_eq |> strip_lambdas (length args)
3.36 |> mk_meta_eq |> Meson.generalize
3.37 @@ -422,14 +427,14 @@
3.38 [] => ()
3.39 | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
3.40
3.41 -fun assume_abstract th =
3.42 +fun assume_abstract isgoal th =
3.43 if lambda_free (prop_of th) then [th]
3.44 - else th |> Drule.eta_contraction_rule |> assume_absfuns
3.45 + else th |> Drule.eta_contraction_rule |> assume_absfuns isgoal
3.46 |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
3.47
3.48 (*Replace lambdas by assumed function definitions in the theorems*)
3.49 -fun assume_abstract_list ths =
3.50 - if abstract_lambdas then List.concat (map assume_abstract ths)
3.51 +fun assume_abstract_list isgoal ths =
3.52 + if abstract_lambdas then List.concat (map (assume_abstract isgoal) ths)
3.53 else map Drule.eta_contraction_rule ths;
3.54
3.55 (*Replace lambdas by declared function definitions in the theorems*)
3.56 @@ -451,7 +456,7 @@
3.57 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
3.58 fun skolem_thm th =
3.59 let val nnfth = to_nnf th
3.60 - in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf
3.61 + in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list false |> Meson.finish_cnf
3.62 end
3.63 handle THM _ => [];
3.64
3.65 @@ -461,7 +466,8 @@
3.66 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
3.67 It returns a modified theory, unless skolemization fails.*)
3.68 fun skolem thy th =
3.69 - let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s)
3.70 + let val cname = (if PureThy.has_name_hint th
3.71 + then flatten_name (PureThy.get_name_hint th) else gensym "")
3.72 val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
3.73 in Option.map
3.74 (fn nnfth =>
3.75 @@ -515,7 +521,9 @@
3.76 (case Thmtab.lookup (!global_clause_cache) th of
3.77 NONE =>
3.78 let val cls = map Goal.close_result (skolem_thm th)
3.79 - in Output.debug (fn () => "inserted into cache: " ^ PureThy.get_name_hint th);
3.80 + in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
3.81 + (if PureThy.has_name_hint th then PureThy.get_name_hint th
3.82 + else string_of_thm th));
3.83 change cache (Thmtab.update (th, cls)); cls
3.84 end
3.85 | SOME cls => cls)
3.86 @@ -588,9 +596,23 @@
3.87
3.88 fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
3.89
3.90 +fun aconv_ct (t,u) = (Thm.term_of t) aconv (Thm.term_of u);
3.91 +
3.92 +(*Expand all *new* definitions (presumably of abstraction or Skolem functions) in a proof state.*)
3.93 +fun expand_defs_tac ths ths' st =
3.94 + let val hyps = foldl (gen_union aconv_ct) [] (map (#hyps o crep_thm) ths)
3.95 + val remove_hyps = filter (not o member aconv_ct hyps)
3.96 + val hyps' = foldl (gen_union aconv_ct) [] (map (remove_hyps o #hyps o crep_thm) (st::ths'))
3.97 + in PRIMITIVE (LocalDefs.expand (filter (can dest_equals) hyps')) st end;
3.98 +
3.99 +fun meson_general_tac ths i =
3.100 + let val _ = Output.debug (fn () => "Meson called with theorems " ^ cat_lines (map string_of_thm ths))
3.101 + val ths' = cnf_rules_of_ths ths
3.102 + in Meson.meson_claset_tac ths' HOL_cs i THEN expand_defs_tac ths ths' end;
3.103 +
3.104 val meson_method_setup = Method.add_methods
3.105 [("meson", Method.thms_args (fn ths =>
3.106 - Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
3.107 + Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
3.108 "MESON resolution proof procedure")];
3.109
3.110 (** Attribute for converting a theorem into clauses **)
3.111 @@ -611,7 +633,7 @@
3.112 it can introduce TVars, which are useless in conjecture clauses.*)
3.113 val no_tvars = null o term_tvars o prop_of;
3.114
3.115 -val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list o make_clauses;
3.116 +val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list true o make_clauses;
3.117
3.118 fun neg_conjecture_clauses st0 n =
3.119 let val st = Seq.hd (neg_skolemize_tac n st0)
3.120 @@ -645,7 +667,7 @@
3.121 fun skolem_attr (Context.Theory thy, th) =
3.122 let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
3.123 in (Context.Theory thy', conj_rule cls) end
3.124 - | skolem_attr (context, th) = (context, conj_rule (cnf_axiom th));
3.125 + | skolem_attr (context, th) = (context, th)
3.126
3.127 val setup_attrs = Attrib.add_attributes
3.128 [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),