src/HOL/Tools/res_axioms.ML
changeset 22724 3002683a6e0f
parent 22691 290454649b8c
child 22731 abfdccaed085
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Apr 17 21:06:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Apr 18 11:14:09 2007 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
     1.5    val meson_method_setup : theory -> theory
     1.6    val setup : theory -> theory
     1.7 -  val assume_abstract_list: thm list -> thm list
     1.8 +  val assume_abstract_list: bool -> thm list -> thm list
     1.9    val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
    1.10    val claset_rules_of: Proof.context -> (string * thm) list   (*FIXME DELETE*)
    1.11    val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
    1.12 @@ -319,9 +319,12 @@
    1.13  fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
    1.14    | valid_name defs _ = false;
    1.15  
    1.16 -fun assume_absfuns th =
    1.17 +(*isgoal holds if "th" is a conjecture. Then the assumption functions are counted from 1
    1.18 +  rather than produced using gensym, as they need to be repeatable.*)
    1.19 +fun assume_absfuns isgoal th =
    1.20    let val thy = theory_of_thm th
    1.21        val cterm = cterm_of thy
    1.22 +      val abs_count = ref 0
    1.23        fun abstract ct =
    1.24          if lambda_free (term_of ct) then (reflexive ct, [])
    1.25          else
    1.26 @@ -350,7 +353,9 @@
    1.27                     | [] =>
    1.28                        let val Ts = map type_of args
    1.29                            val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
    1.30 -                          val c = Free (gensym "abs_", const_ty)
    1.31 +                          val id = if isgoal then "abs_" ^ Int.toString (inc abs_count)
    1.32 +                                   else gensym "abs_"
    1.33 +                          val c = Free (id, const_ty)
    1.34                            val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
    1.35                                       |> mk_object_eq |> strip_lambdas (length args)
    1.36                                       |> mk_meta_eq |> Meson.generalize
    1.37 @@ -422,14 +427,14 @@
    1.38        [] => ()
    1.39       | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
    1.40  
    1.41 -fun assume_abstract th =
    1.42 +fun assume_abstract isgoal th =
    1.43    if lambda_free (prop_of th) then [th]
    1.44 -  else th |> Drule.eta_contraction_rule |> assume_absfuns
    1.45 +  else th |> Drule.eta_contraction_rule |> assume_absfuns isgoal
    1.46            |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
    1.47  
    1.48  (*Replace lambdas by assumed function definitions in the theorems*)
    1.49 -fun assume_abstract_list ths =
    1.50 -  if abstract_lambdas then List.concat (map assume_abstract ths)
    1.51 +fun assume_abstract_list isgoal ths =
    1.52 +  if abstract_lambdas then List.concat (map (assume_abstract isgoal) ths)
    1.53    else map Drule.eta_contraction_rule ths;
    1.54  
    1.55  (*Replace lambdas by declared function definitions in the theorems*)
    1.56 @@ -451,7 +456,7 @@
    1.57  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
    1.58  fun skolem_thm th =
    1.59    let val nnfth = to_nnf th
    1.60 -  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf
    1.61 +  in  Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list false |> Meson.finish_cnf
    1.62    end
    1.63    handle THM _ => [];
    1.64  
    1.65 @@ -461,7 +466,8 @@
    1.66  (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
    1.67    It returns a modified theory, unless skolemization fails.*)
    1.68  fun skolem thy th =
    1.69 -  let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s)
    1.70 +  let val cname = (if PureThy.has_name_hint th 
    1.71 +                   then flatten_name (PureThy.get_name_hint th) else gensym "")
    1.72        val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
    1.73    in Option.map
    1.74          (fn nnfth =>
    1.75 @@ -515,7 +521,9 @@
    1.76  	 (case Thmtab.lookup (!global_clause_cache) th of
    1.77  	   NONE => 
    1.78  	     let val cls = map Goal.close_result (skolem_thm th)
    1.79 -	     in Output.debug (fn () => "inserted into cache: " ^ PureThy.get_name_hint th);
    1.80 +	     in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^ 
    1.81 +	                         (if PureThy.has_name_hint th then PureThy.get_name_hint th
    1.82 +	                          else string_of_thm th));
    1.83  		change cache (Thmtab.update (th, cls)); cls 
    1.84  	     end
    1.85  	 | SOME cls => cls)
    1.86 @@ -588,9 +596,23 @@
    1.87  
    1.88  fun cnf_rules_of_ths ths = List.concat (map cnf_axiom ths);
    1.89  
    1.90 +fun aconv_ct (t,u) = (Thm.term_of t) aconv (Thm.term_of u);
    1.91 +
    1.92 +(*Expand all *new* definitions (presumably of abstraction or Skolem functions) in a proof state.*)
    1.93 +fun expand_defs_tac ths ths' st =
    1.94 +  let val hyps = foldl (gen_union aconv_ct) [] (map (#hyps o crep_thm) ths)
    1.95 +      val remove_hyps = filter (not o member aconv_ct hyps) 
    1.96 +      val hyps' = foldl (gen_union aconv_ct) [] (map (remove_hyps o #hyps o crep_thm) (st::ths'))
    1.97 +  in  PRIMITIVE (LocalDefs.expand (filter (can dest_equals) hyps')) st  end;
    1.98 +
    1.99 +fun meson_general_tac ths i =
   1.100 + let val _ = Output.debug (fn () => "Meson called with theorems " ^ cat_lines (map string_of_thm ths))
   1.101 +     val ths' = cnf_rules_of_ths ths
   1.102 + in  Meson.meson_claset_tac ths' HOL_cs i THEN expand_defs_tac ths ths' end;
   1.103 +
   1.104  val meson_method_setup = Method.add_methods
   1.105    [("meson", Method.thms_args (fn ths =>
   1.106 -      Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
   1.107 +      Method.SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ths)),
   1.108      "MESON resolution proof procedure")];
   1.109  
   1.110  (** Attribute for converting a theorem into clauses **)
   1.111 @@ -611,7 +633,7 @@
   1.112    it can introduce TVars, which are useless in conjecture clauses.*)
   1.113  val no_tvars = null o term_tvars o prop_of;
   1.114  
   1.115 -val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list o make_clauses;
   1.116 +val neg_clausify = filter no_tvars o Meson.finish_cnf o assume_abstract_list true o make_clauses;
   1.117  
   1.118  fun neg_conjecture_clauses st0 n =
   1.119    let val st = Seq.hd (neg_skolemize_tac n st0)
   1.120 @@ -645,7 +667,7 @@
   1.121  fun skolem_attr (Context.Theory thy, th) =
   1.122        let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
   1.123        in (Context.Theory thy', conj_rule cls) end
   1.124 -  | skolem_attr (context, th) = (context, conj_rule (cnf_axiom th));
   1.125 +  | skolem_attr (context, th) = (context, th)
   1.126  
   1.127  val setup_attrs = Attrib.add_attributes
   1.128    [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),