modernized structure Prop_Logic;
authorwenzelm
Sat Jan 08 16:01:51 2011 +0100 (2011-01-08)
changeset 4147154a58904a598
parent 41470 890b25753bf7
child 41472 f6ab14e61604
modernized structure Prop_Logic;
avoid ML structure aliases;
src/HOL/Tools/Function/scnp_solve.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/prop_logic.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/sat_solver.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/Tools/Function/scnp_solve.ML	Sat Jan 08 14:32:55 2011 +0100
     1.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML	Sat Jan 08 16:01:51 2011 +0100
     1.3 @@ -51,11 +51,11 @@
     1.4  
     1.5  (** Propositional formulas **)
     1.6  
     1.7 -val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
     1.8 -val BoolVar = PropLogic.BoolVar
     1.9 +val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or
    1.10 +val BoolVar = Prop_Logic.BoolVar
    1.11  fun Implies (p, q) = Or (Not p, q)
    1.12  fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
    1.13 -val all = PropLogic.all
    1.14 +val all = Prop_Logic.all
    1.15  
    1.16  (* finite indexed quantifiers:
    1.17  
    1.18 @@ -64,7 +64,7 @@
    1.19                        0<=i<n
    1.20   *)
    1.21  fun iforall n f = all (map_range f n)
    1.22 -fun iexists n f = PropLogic.exists (map_range f n)
    1.23 +fun iexists n f = Prop_Logic.exists (map_range f n)
    1.24  fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
    1.25  
    1.26  fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
    1.27 @@ -112,7 +112,7 @@
    1.28      val ng = num_graphs gp
    1.29      val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
    1.30  
    1.31 -    fun encode_constraint_strict 0 (x, y) = PropLogic.False
    1.32 +    fun encode_constraint_strict 0 (x, y) = Prop_Logic.False
    1.33        | encode_constraint_strict k (x, y) =
    1.34          Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
    1.35              And (Equiv (TAG x (k - 1), TAG y (k - 1)),
    1.36 @@ -212,7 +212,7 @@
    1.37  fun mk_certificate bits label gp f =
    1.38    let
    1.39      val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
    1.40 -    fun assign (PropLogic.BoolVar v) = the_default false (f v)
    1.41 +    fun assign (Prop_Logic.BoolVar v) = the_default false (f v)
    1.42      fun assignTag i j =
    1.43        (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
    1.44          (bits - 1 downto 0) 0)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jan 08 14:32:55 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Sat Jan 08 16:01:51 2011 +0100
     2.3 @@ -20,8 +20,6 @@
     2.4  open Nitpick_Util
     2.5  open Nitpick_HOL
     2.6  
     2.7 -structure PL = PropLogic
     2.8 -
     2.9  datatype sign = Plus | Minus
    2.10  
    2.11  type var = int
    2.12 @@ -474,36 +472,36 @@
    2.13  val bools_from_annotation = AList.lookup (op =) bool_table #> the
    2.14  val annotation_from_bools = AList.find (op =) bool_table #> the_single
    2.15  
    2.16 -fun prop_for_bool b = if b then PL.True else PL.False
    2.17 +fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
    2.18  fun prop_for_bool_var_equality (v1, v2) =
    2.19 -  PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)),
    2.20 -           PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2))
    2.21 +  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
    2.22 +           Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2))
    2.23  fun prop_for_assign (x, a) =
    2.24    let val (b1, b2) = bools_from_annotation a in
    2.25 -    PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot,
    2.26 -             PL.BoolVar (snd_var x) |> not b2 ? PL.SNot)
    2.27 +    Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
    2.28 +             Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
    2.29    end
    2.30  fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
    2.31 -  | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a))
    2.32 +  | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a))
    2.33  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
    2.34    | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
    2.35  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
    2.36    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
    2.37    | prop_for_atom_equality (V x1, V x2) =
    2.38 -    PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
    2.39 +    Prop_Logic.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)),
    2.40               prop_for_bool_var_equality (pairself snd_var (x1, x2)))
    2.41 -val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
    2.42 +val prop_for_assign_clause = Prop_Logic.exists o map prop_for_assign_literal
    2.43  fun prop_for_exists_var_assign_literal xs a =
    2.44 -  PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
    2.45 +  Prop_Logic.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
    2.46  fun prop_for_comp (aa1, aa2, Eq, []) =
    2.47 -    PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
    2.48 +    Prop_Logic.SAnd (prop_for_comp (aa1, aa2, Leq, []),
    2.49               prop_for_comp (aa2, aa1, Leq, []))
    2.50    | prop_for_comp (aa1, aa2, Neq, []) =
    2.51 -    PL.SNot (prop_for_comp (aa1, aa2, Eq, []))
    2.52 +    Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, []))
    2.53    | prop_for_comp (aa1, aa2, Leq, []) =
    2.54 -    PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
    2.55 +    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
    2.56    | prop_for_comp (aa1, aa2, cmp, xs) =
    2.57 -    PL.SOr (prop_for_exists_var_assign_literal xs Gen,
    2.58 +    Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen,
    2.59              prop_for_comp (aa1, aa2, cmp, []))
    2.60  
    2.61  fun extract_assigns max_var assigns asgs =
    2.62 @@ -542,11 +540,11 @@
    2.63        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
    2.64      val _ = print_problem comps clauses
    2.65      val prop =
    2.66 -      PL.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
    2.67 +      Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
    2.68    in
    2.69 -    if PL.eval (K false) prop then
    2.70 +    if Prop_Logic.eval (K false) prop then
    2.71        do_assigns (K (SOME false))
    2.72 -    else if PL.eval (K true) prop then
    2.73 +    else if Prop_Logic.eval (K true) prop then
    2.74        do_assigns (K (SOME true))
    2.75      else
    2.76        let
     3.1 --- a/src/HOL/Tools/prop_logic.ML	Sat Jan 08 14:32:55 2011 +0100
     3.2 +++ b/src/HOL/Tools/prop_logic.ML	Sat Jan 08 16:01:51 2011 +0100
     3.3 @@ -42,7 +42,7 @@
     3.4    val term_of_prop_formula: prop_formula -> term
     3.5  end;
     3.6  
     3.7 -structure PropLogic : PROP_LOGIC =
     3.8 +structure Prop_Logic : PROP_LOGIC =
     3.9  struct
    3.10  
    3.11  (* ------------------------------------------------------------------------- *)
     4.1 --- a/src/HOL/Tools/refute.ML	Sat Jan 08 14:32:55 2011 +0100
     4.2 +++ b/src/HOL/Tools/refute.ML	Sat Jan 08 16:01:51 2011 +0100
     4.3 @@ -77,7 +77,7 @@
     4.4  structure Refute : REFUTE =
     4.5  struct
     4.6  
     4.7 -open PropLogic;
     4.8 +open Prop_Logic;
     4.9  
    4.10  (* We use 'REFUTE' only for internal error conditions that should    *)
    4.11  (* never occur in the first place (i.e. errors caused by bugs in our *)
    4.12 @@ -1118,8 +1118,8 @@
    4.13              (* make 'u' either true or false, and make all axioms true, and *)
    4.14              (* add the well-formedness side condition                       *)
    4.15              val fm_u = (if negate then toFalse else toTrue) (hd intrs)
    4.16 -            val fm_ax = PropLogic.all (map toTrue (tl intrs))
    4.17 -            val fm = PropLogic.all [#wellformed args, fm_ax, fm_u]
    4.18 +            val fm_ax = Prop_Logic.all (map toTrue (tl intrs))
    4.19 +            val fm = Prop_Logic.all [#wellformed args, fm_ax, fm_u]
    4.20              val _ =
    4.21                (if satsolver = "dpll" orelse satsolver = "enumerate" then
    4.22                  warning ("Using SAT solver " ^ quote satsolver ^
    4.23 @@ -1394,22 +1394,22 @@
    4.24        (case i1 of
    4.25          Leaf xs =>
    4.26            (case i2 of
    4.27 -            Leaf ys => PropLogic.dot_product (xs, ys)  (* defined and equal *)
    4.28 +            Leaf ys => Prop_Logic.dot_product (xs, ys)  (* defined and equal *)
    4.29            | Node _  => raise REFUTE ("make_equality",
    4.30              "second interpretation is higher"))
    4.31        | Node xs =>
    4.32            (case i2 of
    4.33              Leaf _  => raise REFUTE ("make_equality",
    4.34              "first interpretation is higher")
    4.35 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
    4.36 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
    4.37      (* interpretation * interpretation -> prop_formula *)
    4.38      fun not_equal (i1, i2) =
    4.39        (case i1 of
    4.40          Leaf xs =>
    4.41            (case i2 of
    4.42              (* defined and not equal *)
    4.43 -            Leaf ys => PropLogic.all ((PropLogic.exists xs)
    4.44 -            :: (PropLogic.exists ys)
    4.45 +            Leaf ys => Prop_Logic.all ((Prop_Logic.exists xs)
    4.46 +            :: (Prop_Logic.exists ys)
    4.47              :: (map (fn (x,y) => SOr (SNot x, SNot y)) (xs ~~ ys)))
    4.48            | Node _  => raise REFUTE ("make_equality",
    4.49              "second interpretation is higher"))
    4.50 @@ -1417,7 +1417,7 @@
    4.51            (case i2 of
    4.52              Leaf _  => raise REFUTE ("make_equality",
    4.53              "first interpretation is higher")
    4.54 -          | Node ys => PropLogic.exists (map not_equal (xs ~~ ys))))
    4.55 +          | Node ys => Prop_Logic.exists (map not_equal (xs ~~ ys))))
    4.56    in
    4.57      (* a value may be undefined; therefore 'not_equal' is not just the *)
    4.58      (* negation of 'equal'                                             *)
    4.59 @@ -1443,15 +1443,15 @@
    4.60          Leaf xs =>
    4.61            (case i2 of
    4.62              (* defined and equal, or both undefined *)
    4.63 -            Leaf ys => SOr (PropLogic.dot_product (xs, ys),
    4.64 -            SAnd (PropLogic.all (map SNot xs), PropLogic.all (map SNot ys)))
    4.65 +            Leaf ys => SOr (Prop_Logic.dot_product (xs, ys),
    4.66 +            SAnd (Prop_Logic.all (map SNot xs), Prop_Logic.all (map SNot ys)))
    4.67            | Node _  => raise REFUTE ("make_def_equality",
    4.68              "second interpretation is higher"))
    4.69        | Node xs =>
    4.70            (case i2 of
    4.71              Leaf _  => raise REFUTE ("make_def_equality",
    4.72              "first interpretation is higher")
    4.73 -          | Node ys => PropLogic.all (map equal (xs ~~ ys))))
    4.74 +          | Node ys => Prop_Logic.all (map equal (xs ~~ ys))))
    4.75      (* interpretation *)
    4.76      val eq = equal (i1, i2)
    4.77    in
    4.78 @@ -1499,7 +1499,7 @@
    4.79      (* interpretation -> prop_formula list *)
    4.80      fun interpretation_to_prop_formula_list (Leaf xs) = xs
    4.81        | interpretation_to_prop_formula_list (Node trees) =
    4.82 -          map PropLogic.all (pick_all
    4.83 +          map Prop_Logic.all (pick_all
    4.84              (map interpretation_to_prop_formula_list trees))
    4.85    in
    4.86      case i1 of
    4.87 @@ -1571,7 +1571,7 @@
    4.88              val intr = Leaf fms
    4.89              (* prop_formula list -> prop_formula *)
    4.90              fun one_of_two_false [] = True
    4.91 -              | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
    4.92 +              | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
    4.93                    SOr (SNot x, SNot x')) xs), one_of_two_false xs)
    4.94              (* prop_formula *)
    4.95              val wf = one_of_two_false fms
    4.96 @@ -1672,8 +1672,8 @@
    4.97            Node xs =>
    4.98              (* 3-valued logic *)
    4.99              let
   4.100 -              val fmTrue  = PropLogic.all (map toTrue xs)
   4.101 -              val fmFalse = PropLogic.exists (map toFalse xs)
   4.102 +              val fmTrue  = Prop_Logic.all (map toTrue xs)
   4.103 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
   4.104              in
   4.105                SOME (Leaf [fmTrue, fmFalse], m, a)
   4.106              end
   4.107 @@ -1701,8 +1701,8 @@
   4.108        let
   4.109          val (i1, m1, a1) = interpret ctxt model args t1
   4.110          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   4.111 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   4.112 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   4.113 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
   4.114 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
   4.115        in
   4.116          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   4.117        end
   4.118 @@ -1735,8 +1735,8 @@
   4.119            Node xs =>
   4.120              (* 3-valued logic *)
   4.121              let
   4.122 -              val fmTrue  = PropLogic.all (map toTrue xs)
   4.123 -              val fmFalse = PropLogic.exists (map toFalse xs)
   4.124 +              val fmTrue = Prop_Logic.all (map toTrue xs)
   4.125 +              val fmFalse = Prop_Logic.exists (map toFalse xs)
   4.126              in
   4.127                SOME (Leaf [fmTrue, fmFalse], m, a)
   4.128              end
   4.129 @@ -1754,8 +1754,8 @@
   4.130            Node xs =>
   4.131              (* 3-valued logic *)
   4.132              let
   4.133 -              val fmTrue  = PropLogic.exists (map toTrue xs)
   4.134 -              val fmFalse = PropLogic.all (map toFalse xs)
   4.135 +              val fmTrue = Prop_Logic.exists (map toTrue xs)
   4.136 +              val fmFalse = Prop_Logic.all (map toFalse xs)
   4.137              in
   4.138                SOME (Leaf [fmTrue, fmFalse], m, a)
   4.139              end
   4.140 @@ -1781,8 +1781,8 @@
   4.141        let
   4.142          val (i1, m1, a1) = interpret ctxt model args t1
   4.143          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   4.144 -        val fmTrue       = PropLogic.SAnd (toTrue i1, toTrue i2)
   4.145 -        val fmFalse      = PropLogic.SOr (toFalse i1, toFalse i2)
   4.146 +        val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2)
   4.147 +        val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2)
   4.148        in
   4.149          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   4.150        end
   4.151 @@ -1798,8 +1798,8 @@
   4.152        let
   4.153          val (i1, m1, a1) = interpret ctxt model args t1
   4.154          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   4.155 -        val fmTrue       = PropLogic.SOr (toTrue i1, toTrue i2)
   4.156 -        val fmFalse      = PropLogic.SAnd (toFalse i1, toFalse i2)
   4.157 +        val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2)
   4.158 +        val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2)
   4.159        in
   4.160          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   4.161        end
   4.162 @@ -1815,8 +1815,8 @@
   4.163        let
   4.164          val (i1, m1, a1) = interpret ctxt model args t1
   4.165          val (i2, m2, a2) = interpret ctxt m1 a1 t2
   4.166 -        val fmTrue       = PropLogic.SOr (toFalse i1, toTrue i2)
   4.167 -        val fmFalse      = PropLogic.SAnd (toTrue i1, toFalse i2)
   4.168 +        val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
   4.169 +        val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
   4.170        in
   4.171          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   4.172        end
   4.173 @@ -1890,7 +1890,7 @@
   4.174                      val intr     = Leaf fms
   4.175                      (* prop_formula list -> prop_formula *)
   4.176                      fun one_of_two_false [] = True
   4.177 -                      | one_of_two_false (x::xs) = SAnd (PropLogic.all (map (fn x' =>
   4.178 +                      | one_of_two_false (x::xs) = SAnd (Prop_Logic.all (map (fn x' =>
   4.179                            SOr (SNot x, SNot x')) xs), one_of_two_false xs)
   4.180                      (* prop_formula *)
   4.181                      val wf = one_of_two_false fms
   4.182 @@ -2961,7 +2961,7 @@
   4.183            strip_leading_quote x ^ string_of_int i
   4.184      (* interpretation -> int *)
   4.185      fun index_from_interpretation (Leaf xs) =
   4.186 -          find_index (PropLogic.eval assignment) xs
   4.187 +          find_index (Prop_Logic.eval assignment) xs
   4.188        | index_from_interpretation _ =
   4.189            raise REFUTE ("stlc_printer",
   4.190              "interpretation for ground type is not a leaf")
   4.191 @@ -3045,7 +3045,7 @@
   4.192                (* the index of the element in the datatype *)
   4.193                val element =
   4.194                  (case intr of
   4.195 -                  Leaf xs => find_index (PropLogic.eval assignment) xs
   4.196 +                  Leaf xs => find_index (Prop_Logic.eval assignment) xs
   4.197                  | Node _  => raise REFUTE ("IDT_printer",
   4.198                    "interpretation is not a leaf"))
   4.199              in
     5.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Jan 08 14:32:55 2011 +0100
     5.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Jan 08 16:01:51 2011 +0100
     5.3 @@ -266,13 +266,13 @@
     5.4  (*      a 'prop_formula' (just for tracing)                                  *)
     5.5  (* ------------------------------------------------------------------------- *)
     5.6  
     5.7 -fun string_of_prop_formula PropLogic.True = "True"
     5.8 -  | string_of_prop_formula PropLogic.False = "False"
     5.9 -  | string_of_prop_formula (PropLogic.BoolVar i) = "x" ^ string_of_int i
    5.10 -  | string_of_prop_formula (PropLogic.Not fm) = "~" ^ string_of_prop_formula fm
    5.11 -  | string_of_prop_formula (PropLogic.Or (fm1, fm2)) =
    5.12 +fun string_of_prop_formula Prop_Logic.True = "True"
    5.13 +  | string_of_prop_formula Prop_Logic.False = "False"
    5.14 +  | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
    5.15 +  | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
    5.16 +  | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
    5.17        "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
    5.18 -  | string_of_prop_formula (PropLogic.And (fm1, fm2)) =
    5.19 +  | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
    5.20        "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
    5.21  
    5.22  (* ------------------------------------------------------------------------- *)
    5.23 @@ -313,15 +313,15 @@
    5.24          tracing ("Sorted non-trivial clauses:\n" ^
    5.25            cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
    5.26        else ()
    5.27 -    (* translate clauses from HOL terms to PropLogic.prop_formula *)
    5.28 +    (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
    5.29      val (fms, atom_table) =
    5.30 -      fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
    5.31 +      fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
    5.32          sorted_clauses Termtab.empty
    5.33      val _ =
    5.34        if !trace_sat then
    5.35          tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
    5.36        else ()
    5.37 -    val fm = PropLogic.all fms
    5.38 +    val fm = Prop_Logic.all fms
    5.39      (* unit -> Thm.thm *)
    5.40      fun make_quick_and_dirty_thm () =
    5.41        let
     6.1 --- a/src/HOL/Tools/sat_solver.ML	Sat Jan 08 14:32:55 2011 +0100
     6.2 +++ b/src/HOL/Tools/sat_solver.ML	Sat Jan 08 16:01:51 2011 +0100
     6.3 @@ -14,16 +14,16 @@
     6.4    datatype result = SATISFIABLE of assignment
     6.5                    | UNSATISFIABLE of proof option
     6.6                    | UNKNOWN
     6.7 -  type solver     = PropLogic.prop_formula -> result
     6.8 +  type solver     = Prop_Logic.prop_formula -> result
     6.9  
    6.10    (* auxiliary functions to create external SAT solvers *)
    6.11 -  val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    6.12 -  val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    6.13 -  val read_std_result_file  : Path.T -> string * string * string -> result
    6.14 -  val make_external_solver  : string -> (PropLogic.prop_formula -> unit) ->
    6.15 -                                (unit -> result) -> solver
    6.16 +  val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit
    6.17 +  val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit
    6.18 +  val read_std_result_file : Path.T -> string * string * string -> result
    6.19 +  val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) ->
    6.20 +    (unit -> result) -> solver
    6.21  
    6.22 -  val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
    6.23 +  val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
    6.24  
    6.25    (* generic solver interface *)
    6.26    val solvers       : (string * solver) list Unsynchronized.ref
    6.27 @@ -34,7 +34,7 @@
    6.28  structure SatSolver : SAT_SOLVER =
    6.29  struct
    6.30  
    6.31 -  open PropLogic;
    6.32 +  open Prop_Logic;
    6.33  
    6.34  (* ------------------------------------------------------------------------- *)
    6.35  (* should be raised by an external SAT solver to indicate that the solver is *)
    6.36 @@ -279,8 +279,6 @@
    6.37  (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
    6.38  (* ------------------------------------------------------------------------- *)
    6.39  
    6.40 -  (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
    6.41 -
    6.42    fun make_external_solver cmd writefn readfn fm =
    6.43      (writefn fm; bash cmd; readfn ());
    6.44  
    6.45 @@ -289,8 +287,6 @@
    6.46  (*      a SAT problem given in DIMACS CNF format                             *)
    6.47  (* ------------------------------------------------------------------------- *)
    6.48  
    6.49 -  (* Path.T -> PropLogic.prop_formula *)
    6.50 -
    6.51    fun read_dimacs_cnf_file path =
    6.52    let
    6.53      (* string list -> string list *)
    6.54 @@ -323,27 +319,24 @@
    6.55          | (0::tl) => xs1 :: clauses tl
    6.56          | _       => raise Fail "SatSolver.clauses"
    6.57        end
    6.58 -    (* int -> PropLogic.prop_formula *)
    6.59      fun literal_from_int i =
    6.60        (i<>0 orelse error "variable index in DIMACS CNF file is 0";
    6.61        if i>0 then
    6.62 -        PropLogic.BoolVar i
    6.63 +        Prop_Logic.BoolVar i
    6.64        else
    6.65 -        PropLogic.Not (PropLogic.BoolVar (~i)))
    6.66 -    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
    6.67 +        Prop_Logic.Not (Prop_Logic.BoolVar (~i)))
    6.68      fun disjunction [] =
    6.69        error "empty clause in DIMACS CNF file"
    6.70        | disjunction (x::xs) =
    6.71        (case xs of
    6.72          [] => x
    6.73 -      | _  => PropLogic.Or (x, disjunction xs))
    6.74 -    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
    6.75 +      | _  => Prop_Logic.Or (x, disjunction xs))
    6.76      fun conjunction [] =
    6.77        error "no clause in DIMACS CNF file"
    6.78        | conjunction (x::xs) =
    6.79        (case xs of
    6.80          [] => x
    6.81 -      | _  => PropLogic.And (x, conjunction xs))
    6.82 +      | _  => Prop_Logic.And (x, conjunction xs))
    6.83    in
    6.84      (conjunction
    6.85      o (map disjunction)
    6.86 @@ -405,7 +398,7 @@
    6.87    fun enum_solver fm =
    6.88    let
    6.89      (* int list *)
    6.90 -    val indices = PropLogic.indices fm
    6.91 +    val indices = Prop_Logic.indices fm
    6.92      (* int list -> int list -> int list option *)
    6.93      (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
    6.94      fun next_list _ ([]:int list) =
    6.95 @@ -424,7 +417,7 @@
    6.96        member (op =) xs i
    6.97      (* int list -> SatSolver.result *)
    6.98      fun solver_loop xs =
    6.99 -      if PropLogic.eval (assignment_from_list xs) fm then
   6.100 +      if Prop_Logic.eval (assignment_from_list xs) fm then
   6.101          SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
   6.102        else
   6.103          (case next_list xs indices of
   6.104 @@ -446,16 +439,16 @@
   6.105  
   6.106  let
   6.107    local
   6.108 -    open PropLogic
   6.109 +    open Prop_Logic
   6.110    in
   6.111      fun dpll_solver fm =
   6.112      let
   6.113 -      (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
   6.114 +      (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
   6.115        (* but that sometimes leads to worse performance due to the         *)
   6.116        (* introduction of additional variables.                            *)
   6.117 -      val fm' = PropLogic.nnf fm
   6.118 +      val fm' = Prop_Logic.nnf fm
   6.119        (* int list *)
   6.120 -      val indices = PropLogic.indices fm'
   6.121 +      val indices = Prop_Logic.indices fm'
   6.122        (* int list -> int -> prop_formula *)
   6.123        fun partial_var_eval []      i = BoolVar i
   6.124          | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
   6.125 @@ -587,7 +580,7 @@
   6.126      fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   6.127      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   6.128      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   6.129 -    val cnf        = PropLogic.defcnf fm
   6.130 +    val cnf        = Prop_Logic.defcnf fm
   6.131      val result     = SatSolver.make_external_solver cmd writefn readfn cnf
   6.132      val _          = try File.rm inpath
   6.133      val _          = try File.rm outpath
   6.134 @@ -599,16 +592,16 @@
   6.135          handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
   6.136        (* representation of clauses as ordered lists of literals (with duplicates removed) *)
   6.137        (* prop_formula -> int list *)
   6.138 -      fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
   6.139 +      fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
   6.140          Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
   6.141 -        | clause_to_lit_list (PropLogic.BoolVar i) =
   6.142 +        | clause_to_lit_list (Prop_Logic.BoolVar i) =
   6.143          [i]
   6.144 -        | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
   6.145 +        | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
   6.146          [~i]
   6.147          | clause_to_lit_list _ =
   6.148          raise INVALID_PROOF "Error: invalid clause in CNF formula."
   6.149        (* prop_formula -> int *)
   6.150 -      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
   6.151 +      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   6.152          cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   6.153          | cnf_number_of_clauses _ =
   6.154          1
   6.155 @@ -617,7 +610,7 @@
   6.156        val clauses = Array.array (number_of_clauses, [])
   6.157        (* initialize the 'clauses' array *)
   6.158        (* prop_formula * int -> int *)
   6.159 -      fun init_array (PropLogic.And (fm1, fm2), n) =
   6.160 +      fun init_array (Prop_Logic.And (fm1, fm2), n) =
   6.161          init_array (fm2, init_array (fm1, n))
   6.162          | init_array (fm, n) =
   6.163          (Array.update (clauses, n, clause_to_lit_list fm); n+1)
   6.164 @@ -768,7 +761,7 @@
   6.165      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   6.166      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   6.167      val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
   6.168 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   6.169 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   6.170      fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   6.171      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   6.172      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   6.173 @@ -806,9 +799,9 @@
   6.174        (* string list *)
   6.175        val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
   6.176          handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   6.177 -      (* PropLogic.prop_formula -> int *)
   6.178 -      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   6.179 -        | cnf_number_of_clauses _                          = 1
   6.180 +      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   6.181 +            cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   6.182 +        | cnf_number_of_clauses _ = 1
   6.183        (* string -> int *)
   6.184        fun int_from_string s = (
   6.185          case Int.fromString s of
   6.186 @@ -848,7 +841,7 @@
   6.187                val _   = if !clause_offset = ~1 then clause_offset :=
   6.188                  (case Inttab.max_key (!clause_table) of
   6.189                    SOME id => id
   6.190 -                | NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
   6.191 +                | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
   6.192                  else
   6.193                    ()
   6.194                val vid = int_from_string id
   6.195 @@ -927,7 +920,7 @@
   6.196      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   6.197      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   6.198      val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
   6.199 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   6.200 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   6.201      fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   6.202      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   6.203      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   6.204 @@ -954,7 +947,7 @@
   6.205      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   6.206      val exec       = getenv "BERKMIN_EXE"
   6.207      val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
   6.208 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   6.209 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   6.210      fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   6.211      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   6.212      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   6.213 @@ -980,7 +973,7 @@
   6.214      val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   6.215      val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   6.216      val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
   6.217 -    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   6.218 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   6.219      fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   6.220      val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   6.221      val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
     7.1 --- a/src/HOL/ex/SAT_Examples.thy	Sat Jan 08 14:32:55 2011 +0100
     7.2 +++ b/src/HOL/ex/SAT_Examples.thy	Sat Jan 08 16:01:51 2011 +0100
     7.3 @@ -533,12 +533,10 @@
     7.4  fun benchmark dimacsfile =
     7.5  let
     7.6    val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
     7.7 -  fun and_to_list (PropLogic.And (fm1, fm2)) acc =
     7.8 -    and_to_list fm2 (fm1 :: acc)
     7.9 -    | and_to_list fm acc =
    7.10 -    rev (fm :: acc)
    7.11 +  fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
    7.12 +    | and_to_list fm acc = rev (fm :: acc)
    7.13    val clauses = and_to_list prop_fm []
    7.14 -  val terms   = map (HOLogic.mk_Trueprop o PropLogic.term_of_prop_formula)
    7.15 +  val terms   = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
    7.16      clauses
    7.17    val cterms  = map (Thm.cterm_of @{theory}) terms
    7.18    val timer   = start_timing ()