src/HOL/Tools/refute.ML
changeset 41471 54a58904a598
parent 40720 b770df486e5c
child 41472 f6ab14e61604
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 08 14:32:55 2011 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 08 16:01:51 2011 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  structure Refute : REFUTE =
     1.5  struct
     1.6  
     1.7 -open PropLogic;
     1.8 +open Prop_Logic;
     1.9  
    1.10  (* We use 'REFUTE' only for internal error conditions that should    *)
    1.11  (* never occur in the first place (i.e. errors caused by bugs in our *)
    1.12 @@ -1118,8 +1118,8 @@
    1.13              (* make 'u' either true or false, and make all axioms true, and *)
    1.14              (* add the well-formedness side condition                       *)
    1.15              val fm_u = (if negate then toFalse else toTrue) (hd intrs)
    1.16 -            val fm_ax = PropLogic.all (map toTrue (tl intrs))
    1.17 -            val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
    1.18 +            val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
    1.19 +            val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
    1.20              val _ =
    1.21                (if satsolver = "dpll" orelse satsolver = "enumerate" then
    1.22                  warning ("Using SAT solver " ^ quote satsolver ^
    1.23 @@ -1394,22 +1394,22 @@
    1.24        (case i1 of
    1.25          Leaf xs =>
    1.26            (case i2 of
    1.27 -            Leaf ys => PropLogic.dot_product (xs, ys)  (* defined and equal *)
    1.28 +            Leaf ys => Prop_Logic.dot_product (xs, ys)  (* defined and equal *)
    1.29            | Node _  => raise REFUTE ("make_equality",
    1.30              "second interpretation is higher"))
    1.31        | Node xs =>
    1.32            (case i2 of
    1.33              Leaf _  => raise REFUTE ("make_equality",
    1.34              "first interpretation is higher")
    1.35 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
    1.36 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
    1.37      (* interpretation * interpretation -> prop_formula *)
    1.38      fun not_equal (i1, i2) =
    1.39        (case i1 of
    1.40          Leaf xs =>
    1.41            (case i2 of
    1.42              (* defined and not equal *)
    1.43 -            Leaf ys => PropLogic.all ((PropLogic.exists xs)
    1.44 -            :: (PropLogic.exists ys)
    1.45 +            Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs)
    1.46 +            :: (Prop_Logic.exists ys)
    1.47              :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))
    1.48            | Node _  => raise REFUTE ("make_equality",
    1.49              "second interpretation is higher"))
    1.50 @@ -1417,7 +1417,7 @@
    1.51            (case i2 of
    1.52              Leaf _  => raise REFUTE ("make_equality",
    1.53              "first interpretation is higher")
    1.54 -          | Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
    1.55 +          | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys))))
    1.56    in
    1.57      (* a value may be undefined; therefore 'not_equal' is not just the *)
    1.58      (* negation of 'equal'                                             *)
    1.59 @@ -1443,15 +1443,15 @@
    1.60          Leaf xs =>
    1.61            (case i2 of
    1.62              (* defined and equal, or both undefined *)
    1.63 -            Leaf ys => SOr (PropLogic.dot_product (xs, ys),
    1.64 -            SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys)))
    1.65 +            Leaf ys => SOr (Prop_Logic.dot_product (xs, ys),
    1.66 +            SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys)))
    1.67            | Node _  => raise REFUTE ("make_def_equality",
    1.68              "second interpretation is higher"))
    1.69        | Node xs =>
    1.70            (case i2 of
    1.71              Leaf _  => raise REFUTE ("make_def_equality",
    1.72              "first interpretation is higher")
    1.73 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
    1.74 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
    1.75      (* interpretation *)
    1.76      val eq = equal (i1, i2)
    1.77    in
    1.78 @@ -1499,7 +1499,7 @@
    1.79      (* interpretation -> prop_formula list *)
    1.80      fun interpretation_to_prop_formula_list (Leaf xs) = xs
    1.81        | interpretation_to_prop_formula_list (Node trees) =
    1.82 -          map PropLogic.all (pick_all
    1.83 +          map Prop_Logic.all (pick_all
    1.84              (map interpretation_to_prop_formula_list trees))
    1.85    in
    1.86      case i1 of
    1.87 @@ -1571,7 +1571,7 @@
    1.88              val intr = Leaf fms
    1.89              (* prop_formula list -> prop_formula *)
    1.90              fun one_of_two_false [] = True
    1.91 -              | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
    1.92 +              | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
    1.93                    SOr (SNot x, SNot x')) xs), one_of_two_false xs)
    1.94              (* prop_formula *)
    1.95              val wf = one_of_two_false fms
    1.96 @@ -1672,8 +1672,8 @@
    1.97            Node xs =>
    1.98              (* 3-valued logic *)
    1.99              let
   1.100 -              val fmTrue  = PropLogic.all (map toTrue xs)
   1.101 -              val fmFalse = PropLogic.exists (map toFalse xs)
   1.102 +              val fmTrue  = Prop_Logic.all (map toTrue xs)
   1.103 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
   1.104              in
   1.105                SOME (Leaf [fmTrue, fmFalse], m, a)
   1.106              end
   1.107 @@ -1701,8 +1701,8 @@
   1.108        let
   1.109          val (i1, m1, a1) = interpret ctxt model args t1
   1.110          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   1.111 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   1.112 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   1.113 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
   1.114 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
   1.115        in
   1.116          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.117        end
   1.118 @@ -1735,8 +1735,8 @@
   1.119            Node xs =>
   1.120              (* 3-valued logic *)
   1.121              let
   1.122 -              val fmTrue  = PropLogic.all (map toTrue xs)
   1.123 -              val fmFalse = PropLogic.exists (map toFalse xs)
   1.124 +              val fmTrue = Prop_Logic.all (map toTrue xs)
   1.125 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
   1.126              in
   1.127                SOME (Leaf [fmTrue, fmFalse], m, a)
   1.128              end
   1.129 @@ -1754,8 +1754,8 @@
   1.130            Node xs =>
   1.131              (* 3-valued logic *)
   1.132              let
   1.133 -              val fmTrue  = PropLogic.exists (map toTrue xs)
   1.134 -              val fmFalse = PropLogic.all (map toFalse xs)
   1.135 +              val fmTrue = Prop_Logic.exists (map toTrue xs)
   1.136 +              val fmFalse = Prop_Logic.all (map toFalse xs)
   1.137              in
   1.138                SOME (Leaf [fmTrue, fmFalse], m, a)
   1.139              end
   1.140 @@ -1781,8 +1781,8 @@
   1.141        let
   1.142          val (i1, m1, a1) = interpret ctxt model args t1
   1.143          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   1.144 -        val fmTrue       = PropLogic.SAnd (toTrue i1, toTrue i2)
   1.145 -        val fmFalse      = PropLogic.SOr (toFalse i1, toFalse i2)
   1.146 +        val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2)
   1.147 +        val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2)
   1.148        in
   1.149          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.150        end
   1.151 @@ -1798,8 +1798,8 @@
   1.152        let
   1.153          val (i1, m1, a1) = interpret ctxt model args t1
   1.154          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   1.155 -        val fmTrue       = PropLogic.SOr (toTrue i1, toTrue i2)
   1.156 -        val fmFalse      = PropLogic.SAnd (toFalse i1, toFalse i2)
   1.157 +        val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2)
   1.158 +        val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2)
   1.159        in
   1.160          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.161        end
   1.162 @@ -1815,8 +1815,8 @@
   1.163        let
   1.164          val (i1, m1, a1) = interpret ctxt model args t1
   1.165          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   1.166 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   1.167 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   1.168 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
   1.169 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
   1.170        in
   1.171          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.172        end
   1.173 @@ -1890,7 +1890,7 @@
   1.174                      val intr     = Leaf fms
   1.175                      (* prop_formula list -> prop_formula *)
   1.176                      fun one_of_two_false [] = True
   1.177 -                      | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
   1.178 +                      | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
   1.179                            SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   1.180                      (* prop_formula *)
   1.181                      val wf = one_of_two_false fms
   1.182 @@ -2961,7 +2961,7 @@
   1.183            strip_leading_quote x ^ string_of_int i
   1.184      (* interpretation -> int *)
   1.185      fun index_from_interpretation (Leaf xs) =
   1.186 -          find_index (PropLogic.eval assignment) xs
   1.187 +          find_index (Prop_Logic.eval assignment) xs
   1.188        | index_from_interpretation _ =
   1.189            raise REFUTE ("stlc_printer",
   1.190              "interpretation for ground type is not a leaf")
   1.191 @@ -3045,7 +3045,7 @@
   1.192                (* the index of the element in the datatype *)
   1.193                val element =
   1.194                  (case intr of
   1.195 -                  Leaf xs => find_index (PropLogic.eval assignment) xs
   1.196 +                  Leaf xs => find_index (Prop_Logic.eval assignment) xs
   1.197                  | Node _  => raise REFUTE ("IDT_printer",
   1.198                    "interpretation is not a leaf"))
   1.199              in