src/HOL/Library/refute.ML
changeset 56256 1e01c159e7d9
parent 56252 b72e0a9d62b9
child 56815 848d507584db
     1.1 --- a/src/HOL/Library/refute.ML	Sat Mar 22 19:33:39 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 22 20:42:16 2014 +0100
     1.3 @@ -4,11 +4,6 @@
     1.4  Finite model generation for HOL formulas, using a SAT solver.
     1.5  *)
     1.6  
     1.7 -(* ------------------------------------------------------------------------- *)
     1.8 -(* Declares the 'REFUTE' signature as well as a structure 'Refute'.          *)
     1.9 -(* Documentation is available in the Isabelle/Isar theory 'HOL/Refute.thy'.  *)
    1.10 -(* ------------------------------------------------------------------------- *)
    1.11 -
    1.12  signature REFUTE =
    1.13  sig
    1.14  
    1.15 @@ -638,6 +633,16 @@
    1.16  (* To avoid collecting the same axiom multiple times, we use an           *)
    1.17  (* accumulator 'axs' which contains all axioms collected so far.          *)
    1.18  
    1.19 +local
    1.20 +
    1.21 +fun get_axiom thy xname =
    1.22 +  Name_Space.check (Context.Theory thy) (Theory.axiom_table thy) (xname, Position.none);
    1.23 +
    1.24 +val the_eq_trivial = get_axiom @{theory HOL} "the_eq_trivial";
    1.25 +val someI = get_axiom @{theory Hilbert_Choice} "someI";
    1.26 +
    1.27 +in
    1.28 +
    1.29  fun collect_axioms ctxt t =
    1.30    let
    1.31      val thy = Proof_Context.theory_of ctxt
    1.32 @@ -724,17 +729,15 @@
    1.33        | Const (@{const_name undefined}, T) => collect_type_axioms T axs
    1.34        | Const (@{const_name The}, T) =>
    1.35            let
    1.36 -            val ax = specialize_type thy (@{const_name The}, T)
    1.37 -              (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
    1.38 +            val ax = specialize_type thy (@{const_name The}, T) (#2 the_eq_trivial)
    1.39            in
    1.40 -            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
    1.41 +            collect_this_axiom (#1 the_eq_trivial, ax) axs
    1.42            end
    1.43        | Const (@{const_name Hilbert_Choice.Eps}, T) =>
    1.44            let
    1.45 -            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T)
    1.46 -              (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
    1.47 +            val ax = specialize_type thy (@{const_name Hilbert_Choice.Eps}, T) (#2 someI)
    1.48            in
    1.49 -            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
    1.50 +            collect_this_axiom (#1 someI, ax) axs
    1.51            end
    1.52        | Const (@{const_name All}, T) => collect_type_axioms T axs
    1.53        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
    1.54 @@ -806,6 +809,8 @@
    1.55      result
    1.56    end;
    1.57  
    1.58 +end;
    1.59 +
    1.60  (* ------------------------------------------------------------------------- *)
    1.61  (* ground_types: collects all ground types in a term (including argument     *)
    1.62  (*               types of other types), suppressing duplicates.  Does not    *)
    1.63 @@ -3032,7 +3037,7 @@
    1.64  (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
    1.65  (*       subterms that are then passed to other interpreters!                *)
    1.66  (* ------------------------------------------------------------------------- *)
    1.67 -
    1.68 +(* FIXME formal @{const_name} for some entries (!??) *)
    1.69  val setup =
    1.70     add_interpreter "stlc"    stlc_interpreter #>
    1.71     add_interpreter "Pure"    Pure_interpreter #>