# HG changeset patch
# User webertj
# Date 1156985948 -7200
# Node ID 04621ea9440eeace4c0b837fcae922bb7ef24772
# Parent  a9034285b96b8a7c4caad99b97e9c7b21e710ae3
term_of_prop_formula added

diff -r a9034285b96b -r 04621ea9440e src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Thu Aug 31 02:22:05 2006 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Thu Aug 31 02:59:08 2006 +0200
@@ -35,8 +35,10 @@
 
 	val eval : (int -> bool) -> prop_formula -> bool  (* semantics *)
 
+	(* propositional representation of HOL terms *)
 	val prop_formula_of_term : Term.term -> int Termtab.table -> prop_formula * int Termtab.table
-		(* propositional representation of HOL terms *)
+	(* HOL term representation of propositional formulae *)
+	val term_of_prop_formula : prop_formula -> Term.term
 end;
 
 structure PropLogic : PROP_LOGIC =
@@ -486,4 +488,28 @@
 		aux t table
 	end;
 
+(* ------------------------------------------------------------------------- *)
+(* term_of_prop_formula: returns a HOL term that corresponds to a            *)
+(*      propositional formula, with Boolean variables replaced by Free's     *)
+(* ------------------------------------------------------------------------- *)
+
+(* Note: A more generic implementation should take another argument of type  *)
+(*       Term.term Inttab.table (or so) that specifies HOL terms for some    *)
+(*       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);
+
 end;