--- a/src/HOL/Tools/prop_logic.ML Fri Jan 07 16:11:02 2011 +0100
+++ b/src/HOL/Tools/prop_logic.ML Fri Jan 07 17:07:00 2011 +0100
@@ -7,39 +7,39 @@
signature PROP_LOGIC =
sig
- datatype prop_formula =
- True
- | False
- | BoolVar of int (* NOTE: only use indices >= 1 *)
- | Not of prop_formula
- | Or of prop_formula * prop_formula
- | And of prop_formula * prop_formula
+ datatype prop_formula =
+ True
+ | False
+ | BoolVar of int (* NOTE: only use indices >= 1 *)
+ | Not of prop_formula
+ | Or of prop_formula * prop_formula
+ | And of prop_formula * prop_formula
- val SNot : prop_formula -> prop_formula
- val SOr : prop_formula * prop_formula -> prop_formula
- val SAnd : prop_formula * prop_formula -> prop_formula
- val simplify : prop_formula -> prop_formula (* eliminates True/False and double-negation *)
+ val SNot: prop_formula -> prop_formula
+ val SOr: prop_formula * prop_formula -> prop_formula
+ val SAnd: prop_formula * prop_formula -> prop_formula
+ val simplify: prop_formula -> prop_formula (* eliminates True/False and double-negation *)
- val indices : prop_formula -> int list (* set of all variable indices *)
- val maxidx : prop_formula -> int (* maximal variable index *)
+ val indices: prop_formula -> int list (* set of all variable indices *)
+ val maxidx: prop_formula -> int (* maximal variable index *)
- val exists : prop_formula list -> prop_formula (* finite disjunction *)
- val all : prop_formula list -> prop_formula (* finite conjunction *)
- val dot_product : prop_formula list * prop_formula list -> prop_formula
+ val exists: prop_formula list -> prop_formula (* finite disjunction *)
+ val all: prop_formula list -> prop_formula (* finite conjunction *)
+ val dot_product: prop_formula list * prop_formula list -> prop_formula
- val is_nnf : prop_formula -> bool (* returns true iff the formula is in negation normal form *)
- val is_cnf : prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *)
+ val is_nnf: prop_formula -> bool (* returns true iff the formula is in negation normal form *)
+ val is_cnf: prop_formula -> bool (* returns true iff the formula is in conjunctive normal form *)
- val nnf : prop_formula -> prop_formula (* negation normal form *)
- val cnf : prop_formula -> prop_formula (* conjunctive normal form *)
- val defcnf : prop_formula -> prop_formula (* definitional cnf *)
+ val nnf: prop_formula -> prop_formula (* negation normal form *)
+ val cnf: prop_formula -> prop_formula (* conjunctive normal form *)
+ val defcnf: prop_formula -> prop_formula (* definitional cnf *)
- val eval : (int -> bool) -> prop_formula -> bool (* semantics *)
+ val eval: (int -> bool) -> prop_formula -> bool (* semantics *)
- (* propositional representation of HOL terms *)
- val prop_formula_of_term : term -> int Termtab.table -> prop_formula * int Termtab.table
- (* HOL term representation of propositional formulae *)
- val term_of_prop_formula : prop_formula -> term
+ (* propositional representation of HOL terms *)
+ val prop_formula_of_term: term -> int Termtab.table -> prop_formula * int Termtab.table
+ (* HOL term representation of propositional formulae *)
+ val term_of_prop_formula: prop_formula -> term
end;
structure PropLogic : PROP_LOGIC =
@@ -51,13 +51,13 @@
(* not/or/and *)
(* ------------------------------------------------------------------------- *)
- datatype prop_formula =
- True
- | False
- | BoolVar of int (* NOTE: only use indices >= 1 *)
- | Not of prop_formula
- | Or of prop_formula * prop_formula
- | And of prop_formula * prop_formula;
+datatype prop_formula =
+ True
+ | False
+ | BoolVar of int (* NOTE: only use indices >= 1 *)
+ | Not of prop_formula
+ | Or of prop_formula * prop_formula
+ | And of prop_formula * prop_formula;
(* ------------------------------------------------------------------------- *)
(* The following constructor functions make sure that True and False do not *)
@@ -65,114 +65,93 @@
(* perform double-negation elimination. *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun SNot True = False
- | SNot False = True
- | SNot (Not fm) = fm
- | SNot fm = Not fm;
-
- (* prop_formula * prop_formula -> prop_formula *)
+fun SNot True = False
+ | SNot False = True
+ | SNot (Not fm) = fm
+ | SNot fm = Not fm;
- fun SOr (True, _) = True
- | SOr (_, True) = True
- | SOr (False, fm) = fm
- | SOr (fm, False) = fm
- | SOr (fm1, fm2) = Or (fm1, fm2);
+fun SOr (True, _) = True
+ | SOr (_, True) = True
+ | SOr (False, fm) = fm
+ | SOr (fm, False) = fm
+ | SOr (fm1, fm2) = Or (fm1, fm2);
- (* prop_formula * prop_formula -> prop_formula *)
-
- fun SAnd (True, fm) = fm
- | SAnd (fm, True) = fm
- | SAnd (False, _) = False
- | SAnd (_, False) = False
- | SAnd (fm1, fm2) = And (fm1, fm2);
+fun SAnd (True, fm) = fm
+ | SAnd (fm, True) = fm
+ | SAnd (False, _) = False
+ | SAnd (_, False) = False
+ | SAnd (fm1, fm2) = And (fm1, fm2);
(* ------------------------------------------------------------------------- *)
(* simplify: eliminates True/False below other connectives, and double- *)
(* negation *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun simplify (Not fm) = SNot (simplify fm)
- | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2)
- | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
- | simplify fm = fm;
+fun simplify (Not fm) = SNot (simplify fm)
+ | simplify (Or (fm1, fm2)) = SOr (simplify fm1, simplify fm2)
+ | simplify (And (fm1, fm2)) = SAnd (simplify fm1, simplify fm2)
+ | simplify fm = fm;
(* ------------------------------------------------------------------------- *)
(* indices: collects all indices of Boolean variables that occur in a *)
(* propositional formula 'fm'; no duplicates *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> int list *)
-
- fun indices True = []
- | indices False = []
- | indices (BoolVar i) = [i]
- | indices (Not fm) = indices fm
- | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2)
- | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
+fun indices True = []
+ | indices False = []
+ | indices (BoolVar i) = [i]
+ | indices (Not fm) = indices fm
+ | indices (Or (fm1, fm2)) = union (op =) (indices fm1) (indices fm2)
+ | indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
(* ------------------------------------------------------------------------- *)
(* maxidx: computes the maximal variable index occuring in a formula of *)
(* propositional logic 'fm'; 0 if 'fm' contains no variable *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> int *)
-
- fun maxidx True = 0
- | maxidx False = 0
- | maxidx (BoolVar i) = i
- | maxidx (Not fm) = maxidx fm
- | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2)
- | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
+fun maxidx True = 0
+ | maxidx False = 0
+ | maxidx (BoolVar i) = i
+ | maxidx (Not fm) = maxidx fm
+ | maxidx (Or (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2)
+ | maxidx (And (fm1, fm2)) = Int.max (maxidx fm1, maxidx fm2);
(* ------------------------------------------------------------------------- *)
(* exists: computes the disjunction over a list 'xs' of propositional *)
(* formulas *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula list -> prop_formula *)
-
- fun exists xs = Library.foldl SOr (False, xs);
+fun exists xs = Library.foldl SOr (False, xs);
(* ------------------------------------------------------------------------- *)
(* all: computes the conjunction over a list 'xs' of propositional formulas *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula list -> prop_formula *)
-
- fun all xs = Library.foldl SAnd (True, xs);
+fun all xs = Library.foldl SAnd (True, xs);
(* ------------------------------------------------------------------------- *)
(* dot_product: ([x1,...,xn], [y1,...,yn]) -> x1*y1+...+xn*yn *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula list * prop_formula list -> prop_formula *)
-
- fun dot_product (xs,ys) = exists (map SAnd (xs~~ys));
+fun dot_product (xs, ys) = exists (map SAnd (xs ~~ ys));
(* ------------------------------------------------------------------------- *)
(* is_nnf: returns 'true' iff the formula is in negation normal form (i.e., *)
(* only variables may be negated, but not subformulas). *)
(* ------------------------------------------------------------------------- *)
- local
- fun is_literal (BoolVar _) = true
- | is_literal (Not (BoolVar _)) = true
- | is_literal _ = false
- fun is_conj_disj (Or (fm1, fm2)) =
- is_conj_disj fm1 andalso is_conj_disj fm2
- | is_conj_disj (And (fm1, fm2)) =
- is_conj_disj fm1 andalso is_conj_disj fm2
- | is_conj_disj fm =
- is_literal fm
- in
- fun is_nnf True = true
- | is_nnf False = true
- | is_nnf fm = is_conj_disj fm
- end;
+local
+ fun is_literal (BoolVar _) = true
+ | is_literal (Not (BoolVar _)) = true
+ | is_literal _ = false
+ fun is_conj_disj (Or (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
+ | is_conj_disj (And (fm1, fm2)) = is_conj_disj fm1 andalso is_conj_disj fm2
+ | is_conj_disj fm = is_literal fm
+in
+ fun is_nnf True = true
+ | is_nnf False = true
+ | is_nnf fm = is_conj_disj fm
+end;
(* ------------------------------------------------------------------------- *)
(* is_cnf: returns 'true' iff the formula is in conjunctive normal form *)
@@ -180,19 +159,19 @@
(* implies 'is_nnf'. *)
(* ------------------------------------------------------------------------- *)
- local
- fun is_literal (BoolVar _) = true
- | is_literal (Not (BoolVar _)) = true
- | is_literal _ = false
- fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
- | is_disj fm = is_literal fm
- fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
- | is_conj fm = is_disj fm
- in
- fun is_cnf True = true
- | is_cnf False = true
- | is_cnf fm = is_conj fm
- end;
+local
+ fun is_literal (BoolVar _) = true
+ | is_literal (Not (BoolVar _)) = true
+ | is_literal _ = false
+ fun is_disj (Or (fm1, fm2)) = is_disj fm1 andalso is_disj fm2
+ | is_disj fm = is_literal fm
+ fun is_conj (And (fm1, fm2)) = is_conj fm1 andalso is_conj fm2
+ | is_conj fm = is_disj fm
+in
+ fun is_cnf True = true
+ | is_cnf False = true
+ | is_cnf fm = is_conj fm
+end;
(* ------------------------------------------------------------------------- *)
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
@@ -202,35 +181,31 @@
(* 'fm' if (and only if) 'is_nnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun nnf fm =
- let
- fun
- (* constants *)
- nnf_aux True = True
- | nnf_aux False = False
- (* variables *)
- | nnf_aux (BoolVar i) = (BoolVar i)
- (* 'or' and 'and' as outermost connectives are left untouched *)
- | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2)
- | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2)
- (* 'not' + constant *)
- | nnf_aux (Not True) = False
- | nnf_aux (Not False) = True
- (* 'not' + variable *)
- | nnf_aux (Not (BoolVar i)) = Not (BoolVar i)
- (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
- | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
- | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
- (* double-negation elimination *)
- | nnf_aux (Not (Not fm)) = nnf_aux fm
- in
- if is_nnf fm then
- fm
- else
- nnf_aux fm
- end;
+fun nnf fm =
+ let
+ fun
+ (* constants *)
+ nnf_aux True = True
+ | nnf_aux False = False
+ (* variables *)
+ | nnf_aux (BoolVar i) = (BoolVar i)
+ (* 'or' and 'and' as outermost connectives are left untouched *)
+ | nnf_aux (Or (fm1, fm2)) = SOr (nnf_aux fm1, nnf_aux fm2)
+ | nnf_aux (And (fm1, fm2)) = SAnd (nnf_aux fm1, nnf_aux fm2)
+ (* 'not' + constant *)
+ | nnf_aux (Not True) = False
+ | nnf_aux (Not False) = True
+ (* 'not' + variable *)
+ | nnf_aux (Not (BoolVar i)) = Not (BoolVar i)
+ (* pushing 'not' inside of 'or'/'and' using de Morgan's laws *)
+ | nnf_aux (Not (Or (fm1, fm2))) = SAnd (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+ | nnf_aux (Not (And (fm1, fm2))) = SOr (nnf_aux (SNot fm1), nnf_aux (SNot fm2))
+ (* double-negation elimination *)
+ | nnf_aux (Not (Not fm)) = nnf_aux fm
+ in
+ if is_nnf fm then fm
+ else nnf_aux fm
+ end;
(* ------------------------------------------------------------------------- *)
(* cnf: computes the conjunctive normal form (i.e., a conjunction of *)
@@ -241,35 +216,30 @@
(* 'fm' if (and only if) 'is_cnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun cnf fm =
- let
- (* function to push an 'Or' below 'And's, using distributive laws *)
- fun cnf_or (And (fm11, fm12), fm2) =
- And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
- | cnf_or (fm1, And (fm21, fm22)) =
- And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
- (* neither subformula contains 'And' *)
- | cnf_or (fm1, fm2) =
- Or (fm1, fm2)
- fun cnf_from_nnf True = True
- | cnf_from_nnf False = False
- | cnf_from_nnf (BoolVar i) = BoolVar i
- (* 'fm' must be a variable since the formula is in NNF *)
- | cnf_from_nnf (Not fm) = Not fm
- (* 'Or' may need to be pushed below 'And' *)
- | cnf_from_nnf (Or (fm1, fm2)) =
- cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
- (* 'And' as outermost connective is left untouched *)
- | cnf_from_nnf (And (fm1, fm2)) =
- And (cnf_from_nnf fm1, cnf_from_nnf fm2)
- in
- if is_cnf fm then
- fm
- else
- (cnf_from_nnf o nnf) fm
- end;
+fun cnf fm =
+ let
+ (* function to push an 'Or' below 'And's, using distributive laws *)
+ fun cnf_or (And (fm11, fm12), fm2) =
+ And (cnf_or (fm11, fm2), cnf_or (fm12, fm2))
+ | cnf_or (fm1, And (fm21, fm22)) =
+ And (cnf_or (fm1, fm21), cnf_or (fm1, fm22))
+ (* neither subformula contains 'And' *)
+ | cnf_or (fm1, fm2) = Or (fm1, fm2)
+ fun cnf_from_nnf True = True
+ | cnf_from_nnf False = False
+ | cnf_from_nnf (BoolVar i) = BoolVar i
+ (* 'fm' must be a variable since the formula is in NNF *)
+ | cnf_from_nnf (Not fm) = Not fm
+ (* 'Or' may need to be pushed below 'And' *)
+ | cnf_from_nnf (Or (fm1, fm2)) =
+ cnf_or (cnf_from_nnf fm1, cnf_from_nnf fm2)
+ (* 'And' as outermost connective is left untouched *)
+ | cnf_from_nnf (And (fm1, fm2)) =
+ And (cnf_from_nnf fm1, cnf_from_nnf fm2)
+ in
+ if is_cnf fm then fm
+ else (cnf_from_nnf o nnf) fm
+ end;
(* ------------------------------------------------------------------------- *)
(* defcnf: computes a definitional conjunctive normal form of a formula 'fm' *)
@@ -282,86 +252,80 @@
(* 'is_cnf fm' returns 'true'. *)
(* ------------------------------------------------------------------------- *)
- (* prop_formula -> prop_formula *)
-
- fun defcnf fm =
- if is_cnf fm then
- fm
- else
- let
- val fm' = nnf fm
- (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
- (* int ref *)
- val new = Unsynchronized.ref (maxidx fm' + 1)
- (* unit -> int *)
- fun new_idx () = let val idx = !new in new := idx+1; idx end
- (* replaces 'And' by an auxiliary variable (and its definition) *)
- (* prop_formula -> prop_formula * prop_formula list *)
- fun defcnf_or (And x) =
- let
- val i = new_idx ()
- in
- (* Note that definitions are in NNF, but not CNF. *)
- (BoolVar i, [Or (Not (BoolVar i), And x)])
- end
- | defcnf_or (Or (fm1, fm2)) =
- let
- val (fm1', defs1) = defcnf_or fm1
- val (fm2', defs2) = defcnf_or fm2
- in
- (Or (fm1', fm2'), defs1 @ defs2)
- end
- | defcnf_or fm =
- (fm, [])
- (* prop_formula -> prop_formula *)
- fun defcnf_from_nnf True = True
- | defcnf_from_nnf False = False
- | defcnf_from_nnf (BoolVar i) = BoolVar i
- (* 'fm' must be a variable since the formula is in NNF *)
- | defcnf_from_nnf (Not fm) = Not fm
- (* 'Or' may need to be pushed below 'And' *)
- (* 'Or' of literal and 'And': use distributivity *)
- | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
- And (defcnf_from_nnf (Or (BoolVar i, fm1)),
- defcnf_from_nnf (Or (BoolVar i, fm2)))
- | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
- And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
- defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
- | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
- And (defcnf_from_nnf (Or (fm1, BoolVar i)),
- defcnf_from_nnf (Or (fm2, BoolVar i)))
- | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
- And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
- defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
- (* all other cases: turn the formula into a disjunction of literals, *)
- (* adding definitions as necessary *)
- | defcnf_from_nnf (Or x) =
- let
- val (fm, defs) = defcnf_or (Or x)
- val cnf_defs = map defcnf_from_nnf defs
- in
- all (fm :: cnf_defs)
- end
- (* 'And' as outermost connective is left untouched *)
- | defcnf_from_nnf (And (fm1, fm2)) =
- And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
- in
- defcnf_from_nnf fm'
- end;
+fun defcnf fm =
+ if is_cnf fm then fm
+ else
+ let
+ val fm' = nnf fm
+ (* 'new' specifies the next index that is available to introduce an auxiliary variable *)
+ (* int ref *)
+ val new = Unsynchronized.ref (maxidx fm' + 1)
+ (* unit -> int *)
+ fun new_idx () = let val idx = !new in new := idx+1; idx end
+ (* replaces 'And' by an auxiliary variable (and its definition) *)
+ (* prop_formula -> prop_formula * prop_formula list *)
+ fun defcnf_or (And x) =
+ let
+ val i = new_idx ()
+ in
+ (* Note that definitions are in NNF, but not CNF. *)
+ (BoolVar i, [Or (Not (BoolVar i), And x)])
+ end
+ | defcnf_or (Or (fm1, fm2)) =
+ let
+ val (fm1', defs1) = defcnf_or fm1
+ val (fm2', defs2) = defcnf_or fm2
+ in
+ (Or (fm1', fm2'), defs1 @ defs2)
+ end
+ | defcnf_or fm = (fm, [])
+ (* prop_formula -> prop_formula *)
+ fun defcnf_from_nnf True = True
+ | defcnf_from_nnf False = False
+ | defcnf_from_nnf (BoolVar i) = BoolVar i
+ (* 'fm' must be a variable since the formula is in NNF *)
+ | defcnf_from_nnf (Not fm) = Not fm
+ (* 'Or' may need to be pushed below 'And' *)
+ (* 'Or' of literal and 'And': use distributivity *)
+ | defcnf_from_nnf (Or (BoolVar i, And (fm1, fm2))) =
+ And (defcnf_from_nnf (Or (BoolVar i, fm1)),
+ defcnf_from_nnf (Or (BoolVar i, fm2)))
+ | defcnf_from_nnf (Or (Not (BoolVar i), And (fm1, fm2))) =
+ And (defcnf_from_nnf (Or (Not (BoolVar i), fm1)),
+ defcnf_from_nnf (Or (Not (BoolVar i), fm2)))
+ | defcnf_from_nnf (Or (And (fm1, fm2), BoolVar i)) =
+ And (defcnf_from_nnf (Or (fm1, BoolVar i)),
+ defcnf_from_nnf (Or (fm2, BoolVar i)))
+ | defcnf_from_nnf (Or (And (fm1, fm2), Not (BoolVar i))) =
+ And (defcnf_from_nnf (Or (fm1, Not (BoolVar i))),
+ defcnf_from_nnf (Or (fm2, Not (BoolVar i))))
+ (* all other cases: turn the formula into a disjunction of literals, *)
+ (* adding definitions as necessary *)
+ | defcnf_from_nnf (Or x) =
+ let
+ val (fm, defs) = defcnf_or (Or x)
+ val cnf_defs = map defcnf_from_nnf defs
+ in
+ all (fm :: cnf_defs)
+ end
+ (* 'And' as outermost connective is left untouched *)
+ | defcnf_from_nnf (And (fm1, fm2)) =
+ And (defcnf_from_nnf fm1, defcnf_from_nnf fm2)
+ in
+ defcnf_from_nnf fm'
+ end;
(* ------------------------------------------------------------------------- *)
(* eval: given an assignment 'a' of Boolean values to variable indices, the *)
(* truth value of a propositional formula 'fm' is computed *)
(* ------------------------------------------------------------------------- *)
- (* (int -> bool) -> prop_formula -> bool *)
-
- fun eval a True = true
- | eval a False = false
- | eval a (BoolVar i) = (a i)
- | eval a (Not fm) = not (eval a fm)
- | eval a (Or (fm1,fm2)) = (eval a fm1) orelse (eval a fm2)
- | eval a (And (fm1,fm2)) = (eval a fm1) andalso (eval a fm2);
+fun eval a True = true
+ | eval a False = false
+ | eval a (BoolVar i) = (a i)
+ | eval a (Not fm) = not (eval a fm)
+ | eval a (Or (fm1, fm2)) = (eval a fm1) orelse (eval a fm2)
+ | eval a (And (fm1, fm2)) = (eval a fm1) andalso (eval a fm2);
(* ------------------------------------------------------------------------- *)
(* prop_formula_of_term: returns the propositional structure of a HOL term, *)
@@ -378,52 +342,47 @@
(* so that it does not have to be recomputed (by folding over the *)
(* table) for each invocation. *)
- (* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
- fun prop_formula_of_term t table =
- let
- val next_idx_is_valid = Unsynchronized.ref false
- val next_idx = Unsynchronized.ref 0
- fun get_next_idx () =
- if !next_idx_is_valid then
- Unsynchronized.inc next_idx
- else (
- next_idx := Termtab.fold (Integer.max o snd) table 0;
- next_idx_is_valid := true;
- Unsynchronized.inc next_idx
- )
- fun aux (Const (@{const_name True}, _)) table =
- (True, table)
- | aux (Const (@{const_name False}, _)) table =
- (False, table)
- | aux (Const (@{const_name Not}, _) $ x) table =
- apfst Not (aux x table)
- | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
- let
- val (fm1, table1) = aux x table
- val (fm2, table2) = aux y table1
- in
- (Or (fm1, fm2), table2)
- end
- | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
- let
- val (fm1, table1) = aux x table
- val (fm2, table2) = aux y table1
- in
- (And (fm1, fm2), table2)
- end
- | aux x table =
- (case Termtab.lookup table x of
- SOME i =>
- (BoolVar i, table)
- | NONE =>
- let
- val i = get_next_idx ()
- in
- (BoolVar i, Termtab.update (x, i) table)
- end)
- in
- aux t table
- end;
+fun prop_formula_of_term t table =
+ let
+ val next_idx_is_valid = Unsynchronized.ref false
+ val next_idx = Unsynchronized.ref 0
+ fun get_next_idx () =
+ if !next_idx_is_valid then
+ Unsynchronized.inc next_idx
+ else (
+ next_idx := Termtab.fold (Integer.max o snd) table 0;
+ next_idx_is_valid := true;
+ Unsynchronized.inc next_idx
+ )
+ fun aux (Const (@{const_name True}, _)) table = (True, table)
+ | aux (Const (@{const_name False}, _)) table = (False, table)
+ | aux (Const (@{const_name Not}, _) $ x) table = apfst Not (aux x table)
+ | aux (Const (@{const_name HOL.disj}, _) $ x $ y) table =
+ let
+ val (fm1, table1) = aux x table
+ val (fm2, table2) = aux y table1
+ in
+ (Or (fm1, fm2), table2)
+ end
+ | aux (Const (@{const_name HOL.conj}, _) $ x $ y) table =
+ let
+ val (fm1, table1) = aux x table
+ val (fm2, table2) = aux y table1
+ in
+ (And (fm1, fm2), table2)
+ end
+ | aux x table =
+ (case Termtab.lookup table x of
+ SOME i => (BoolVar i, table)
+ | NONE =>
+ let
+ val i = get_next_idx ()
+ in
+ (BoolVar i, Termtab.update (x, i) table)
+ end)
+ in
+ aux t table
+ end;
(* ------------------------------------------------------------------------- *)
(* term_of_prop_formula: returns a HOL term that corresponds to a *)
@@ -435,18 +394,13 @@
(* Boolean variables in the formula, similar to 'prop_formula_of_term' *)
(* (but the other way round). *)
- (* prop_formula -> Term.term *)
- fun term_of_prop_formula True =
- HOLogic.true_const
- | term_of_prop_formula False =
- HOLogic.false_const
- | term_of_prop_formula (BoolVar i) =
- Free ("v" ^ Int.toString i, HOLogic.boolT)
- | term_of_prop_formula (Not fm) =
- HOLogic.mk_not (term_of_prop_formula fm)
- | term_of_prop_formula (Or (fm1, fm2)) =
- HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
- | term_of_prop_formula (And (fm1, fm2)) =
- HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
+fun term_of_prop_formula True = HOLogic.true_const
+ | term_of_prop_formula False = HOLogic.false_const
+ | term_of_prop_formula (BoolVar i) = Free ("v" ^ Int.toString i, HOLogic.boolT)
+ | term_of_prop_formula (Not fm) = HOLogic.mk_not (term_of_prop_formula fm)
+ | term_of_prop_formula (Or (fm1, fm2)) =
+ HOLogic.mk_disj (term_of_prop_formula fm1, term_of_prop_formula fm2)
+ | term_of_prop_formula (And (fm1, fm2)) =
+ HOLogic.mk_conj (term_of_prop_formula fm1, term_of_prop_formula fm2);
end;