src/HOL/Tools/res_axioms.ML
changeset 28544 26743a1591f5
parent 28262 aa7ca36d67fd
child 28674 08a77c495dc1
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 09 20:53:10 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 09 20:53:11 2008 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
     1.5    | type_has_empty_sort _ = false;
     1.6  
     1.7 +
     1.8  (**** Transformation of Elimination Rules into First-Order Formulas****)
     1.9  
    1.10  val cfalse = cterm_of HOL.thy HOLogic.false_const;
    1.11 @@ -54,6 +55,7 @@
    1.12  (*To enforce single-threading*)
    1.13  exception Clausify_failure of theory;
    1.14  
    1.15 +
    1.16  (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
    1.17  
    1.18  fun rhs_extra_types lhsT rhs =
    1.19 @@ -76,9 +78,6 @@
    1.20              val args0 = term_frees xtp  (*get the formal parameter list*)
    1.21              val Ts = map type_of args0
    1.22              val extraTs = rhs_extra_types (Ts ---> T) xtp
    1.23 -            val _ = if null extraTs then () else
    1.24 -              warning ("Skolemization: extra type vars: " ^
    1.25 -                commas_quote (map (Syntax.string_of_typ_global thy) extraTs))
    1.26              val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
    1.27              val args = argsx @ args0
    1.28              val cT = extraTs ---> Ts ---> T
    1.29 @@ -165,9 +164,9 @@
    1.30  
    1.31  (*FIXME: requires more use of cterm constructors*)
    1.32  fun abstract ct =
    1.33 -  let val _ = Output.debug (fn()=>"  abstraction: " ^ Display.string_of_cterm ct)
    1.34 +  let
    1.35 +      val thy = theory_of_cterm ct
    1.36        val Abs(x,_,body) = term_of ct
    1.37 -      val thy = theory_of_cterm ct
    1.38        val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
    1.39        val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
    1.40        fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
    1.41 @@ -209,7 +208,7 @@
    1.42    end;
    1.43  
    1.44  (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
    1.45 -  prefix for the constants. Resulting theory is returned in the first theorem. *)
    1.46 +  prefix for the constants.*)
    1.47  fun combinators_aux ct =
    1.48    if lambda_free (term_of ct) then reflexive ct
    1.49    else
    1.50 @@ -217,13 +216,10 @@
    1.51        Abs _ =>
    1.52          let val (cv,cta) = Thm.dest_abs NONE ct
    1.53              val (v,Tv) = (dest_Free o term_of) cv
    1.54 -            val _ = Output.debug (fn()=>"  recursion: " ^ Display.string_of_cterm cta);
    1.55              val u_th = combinators_aux cta
    1.56 -            val _ = Output.debug (fn()=>"  returned " ^ Display.string_of_thm u_th);
    1.57              val cu = Thm.rhs_of u_th
    1.58              val comb_eq = abstract (Thm.cabs cv cu)
    1.59 -        in Output.debug (fn()=>"  abstraction result: " ^ Display.string_of_thm comb_eq);
    1.60 -           (transitive (abstract_rule v cv u_th) comb_eq) end
    1.61 +        in transitive (abstract_rule v cv u_th) comb_eq end
    1.62      | t1 $ t2 =>
    1.63          let val (ct1,ct2) = Thm.dest_comb ct
    1.64          in  combination (combinators_aux ct1) (combinators_aux ct2)  end;
    1.65 @@ -231,10 +227,8 @@
    1.66  fun combinators th =
    1.67    if lambda_free (prop_of th) then th
    1.68    else
    1.69 -    let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th);
    1.70 -        val th = Drule.eta_contraction_rule th
    1.71 +    let val th = Drule.eta_contraction_rule th
    1.72          val eqth = combinators_aux (cprop_of th)
    1.73 -        val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth);
    1.74      in  equal_elim eqth th   end
    1.75      handle THM (msg,_,_) =>
    1.76        (warning ("Error in the combinator translation of " ^ Display.string_of_thm th);
    1.77 @@ -359,29 +353,12 @@
    1.78      in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
    1.79      handle THM _ => [];
    1.80  
    1.81 -(*Declare Skolem functions for a theorem, supplied in nnf and with its name.
    1.82 -  It returns a modified theory, unless skolemization fails.*)
    1.83 -fun skolem (name, th0) thy =
    1.84 -  let
    1.85 -    val th = Thm.transfer thy th0
    1.86 -    val ctxt0 = Variable.thm_context th
    1.87 -  in
    1.88 -    try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) =>
    1.89 -      let
    1.90 -        val s = flatten_name name
    1.91 -        val (defs, thy') = declare_skofuns s nnfth thy
    1.92 -        val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
    1.93 -        val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0
    1.94 -                         |> Meson.finish_cnf |> map Thm.close_derivation
    1.95 -      in (cnfs', thy') end)
    1.96 -  end;
    1.97 -
    1.98  (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
    1.99    Skolem functions.*)
   1.100  structure ThmCache = TheoryDataFun
   1.101  (
   1.102 -  type T = thm list Thmtab.table * unit Symtab.table
   1.103 -  val empty = (Thmtab.empty, Symtab.empty)
   1.104 +  type T = thm list Thmtab.table * unit Symtab.table;
   1.105 +  val empty = (Thmtab.empty, Symtab.empty);
   1.106    val copy = I;
   1.107    val extend = I;
   1.108    fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
   1.109 @@ -411,19 +388,12 @@
   1.110    let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
   1.111        val intros = safeIs @ hazIs
   1.112        val elims  = map Classical.classical_rule (safeEs @ hazEs)
   1.113 -  in
   1.114 -     Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^
   1.115 -            " elims: " ^ Int.toString(length elims));
   1.116 -     map pairname (intros @ elims)
   1.117 -  end;
   1.118 +  in map pairname (intros @ elims) end;
   1.119  
   1.120  fun rules_of_simpset ss =
   1.121    let val ({rules,...}, _) = rep_ss ss
   1.122        val simps = Net.entries rules
   1.123 -  in
   1.124 -    Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps));
   1.125 -    map (fn r => (#name r, #thm r)) simps
   1.126 -  end;
   1.127 +  in map (fn r => (#name r, #thm r)) simps end;
   1.128  
   1.129  fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
   1.130  fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
   1.131 @@ -448,28 +418,51 @@
   1.132  
   1.133  (**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****)
   1.134  
   1.135 -(*Populate the clause cache using the supplied theorem. Return the clausal form
   1.136 -  and modified theory.*)
   1.137 -fun skolem_cache_thm name (i, th) thy =
   1.138 -  if bad_for_atp th then thy
   1.139 -  else
   1.140 -    (case lookup_cache thy th of
   1.141 -      SOME _ => thy
   1.142 -    | NONE =>
   1.143 -        (case skolem (name ^ "_" ^ string_of_int (i + 1), th) thy of
   1.144 -          NONE => thy
   1.145 -        | SOME (cls, thy') => update_cache (th, cls) thy'));
   1.146 +local
   1.147 +
   1.148 +fun skolem_def (name, th) thy =
   1.149 +  let val ctxt0 = Variable.thm_context th in
   1.150 +    (case try (to_nnf th) ctxt0 of
   1.151 +      NONE => (NONE, thy)
   1.152 +    | SOME (nnfth, ctxt1) =>
   1.153 +        let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy
   1.154 +        in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end)
   1.155 +  end;
   1.156  
   1.157 -fun skolem_cache_fact (name, ths) (changed, thy) =
   1.158 -  if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name
   1.159 -  then (changed, thy)
   1.160 -  else (true, thy |> mark_seen name |> fold_index (skolem_cache_thm name) ths);
   1.161 +fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) =
   1.162 +  let
   1.163 +    val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1;
   1.164 +    val cnfs' = cnfs
   1.165 +      |> map combinators
   1.166 +      |> Variable.export ctxt2 ctxt0
   1.167 +      |> Meson.finish_cnf
   1.168 +      |> map Thm.close_derivation;
   1.169 +    in (th, cnfs') end;
   1.170 +
   1.171 +in
   1.172  
   1.173  fun saturate_skolem_cache thy =
   1.174 -  (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of
   1.175 -    (false, _) => NONE
   1.176 -  | (true, thy') => SOME thy');
   1.177 +  let
   1.178 +    val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
   1.179 +      if already_seen thy name then I else cons (name, ths));
   1.180 +    val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
   1.181 +      if member (op =) multi_base_blacklist (Sign.base_name name) then I
   1.182 +      else fold_index (fn (i, th) =>
   1.183 +        if bad_for_atp th orelse is_some (lookup_cache thy th) then I
   1.184 +        else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
   1.185 +  in
   1.186 +    if null new_facts then NONE
   1.187 +    else
   1.188 +      let
   1.189 +        val (defs, thy') = thy
   1.190 +          |> fold (mark_seen o #1) new_facts
   1.191 +          |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
   1.192 +          |>> map_filter I;
   1.193 +        val cache_entries = ParList.map skolem_cnfs defs;
   1.194 +      in SOME (fold update_cache cache_entries thy') end
   1.195 +  end;
   1.196  
   1.197 +end;
   1.198  
   1.199  val suppress_endtheory = ref false;
   1.200  
   1.201 @@ -484,7 +477,7 @@
   1.202  
   1.203  (*** meson proof methods ***)
   1.204  
   1.205 -(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*)
   1.206 +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
   1.207  fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a
   1.208    | is_absko _ = false;
   1.209  
   1.210 @@ -504,17 +497,12 @@
   1.211                                        (map Thm.term_of hyps)
   1.212        val fixed = term_frees (concl_of st) @
   1.213                    foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps)
   1.214 -  in  Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st);
   1.215 -      Output.debug (fn _ => "  st0: " ^ Display.string_of_thm st0);
   1.216 -      Output.debug (fn _ => "  defs: " ^ commas (map Display.string_of_cterm defs));
   1.217 -      Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st]
   1.218 -  end;
   1.219 +  in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
   1.220  
   1.221  
   1.222  fun meson_general_tac ths i st0 =
   1.223    let
   1.224      val thy = Thm.theory_of_thm st0
   1.225 -    val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths))
   1.226    in  (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end;
   1.227  
   1.228  val meson_method_setup = Method.add_methods
   1.229 @@ -577,4 +565,3 @@
   1.230    Theory.at_end clause_cache_endtheory;
   1.231  
   1.232  end;
   1.233 -