--- a/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 10:27:12 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Aug 19 11:02:14 2010 +0200
@@ -93,19 +93,19 @@
val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-fun is_atom (Const ("False", _)) = false
- | is_atom (Const ("True", _)) = false
- | is_atom (Const ("op &", _) $ _ $ _) = false
- | is_atom (Const ("op |", _) $ _ $ _) = false
- | is_atom (Const ("op -->", _) $ _ $ _) = false
- | is_atom (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
- | is_atom (Const ("Not", _) $ _) = false
+fun is_atom (Const (@{const_name "False"}, _)) = false
+ | is_atom (Const (@{const_name "True"}, _)) = false
+ | is_atom (Const (@{const_name "op &"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op |"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op -->"}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name "Not"}, _) $ _) = false
| is_atom _ = true;
-fun is_literal (Const ("Not", _) $ x) = is_atom x
+fun is_literal (Const (@{const_name "Not"}, _) $ x) = is_atom x
| is_literal x = is_atom x;
-fun is_clause (Const ("op |", _) $ x $ y) = is_clause x andalso is_clause y
+fun is_clause (Const (@{const_name "op |"}, _) $ x $ y) = is_clause x andalso is_clause y
| is_clause x = is_literal x;
(* ------------------------------------------------------------------------- *)
@@ -118,7 +118,7 @@
fun clause_is_trivial c =
let
(* Term.term -> Term.term *)
- fun dual (Const ("Not", _) $ x) = x
+ fun dual (Const (@{const_name "Not"}, _) $ x) = x
| dual x = HOLogic.Not $ x
(* Term.term list -> bool *)
fun has_duals [] = false
@@ -184,28 +184,28 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun make_nnf_thm thy (Const ("op &", _) $ x $ y) =
+fun make_nnf_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
conj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op |", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy y
in
disj_cong OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op -->", _) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op -->"}, _) $ x $ y) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy y
in
make_nnf_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
+ | make_nnf_thm thy (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -214,32 +214,32 @@
in
make_nnf_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ Const ("False", _)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "False"}, _)) =
make_nnf_not_false
- | make_nnf_thm thy (Const ("Not", _) $ Const ("True", _)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ Const (@{const_name "True"}, _)) =
make_nnf_not_true
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op &", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op &"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_conj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op |", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op |"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_disj OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op -->", _) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op -->"}, _) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
in
make_nnf_not_imp OF [thm1, thm2]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("op =", Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "op ="}, Type ("fun", Type ("bool", []) :: _)) $ x $ y)) =
let
val thm1 = make_nnf_thm thy x
val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
@@ -248,7 +248,7 @@
in
make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
end
- | make_nnf_thm thy (Const ("Not", _) $ (Const ("Not", _) $ x)) =
+ | make_nnf_thm thy (Const (@{const_name "Not"}, _) $ (Const (@{const_name "Not"}, _) $ x)) =
let
val thm1 = make_nnf_thm thy x
in
@@ -276,7 +276,7 @@
(* Theory.theory -> Term.term -> Thm.thm *)
-fun simp_True_False_thm thy (Const ("op &", _) $ x $ y) =
+fun simp_True_False_thm thy (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -298,7 +298,7 @@
conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
end
end
- | simp_True_False_thm thy (Const ("op |", _) $ x $ y) =
+ | simp_True_False_thm thy (Const (@{const_name "op |"}, _) $ x $ y) =
let
val thm1 = simp_True_False_thm thy x
val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
@@ -334,24 +334,24 @@
fun make_cnf_thm thy t =
let
(* Term.term -> Thm.thm *)
- fun make_cnf_thm_from_nnf (Const ("op &", _) $ x $ y) =
+ fun make_cnf_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
val thm2 = make_cnf_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnf_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnf_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnf_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnf_disj_thm x1 y'
val thm2 = make_cnf_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnf_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnf_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnf_disj_thm x' y1
val thm2 = make_cnf_disj_thm x' y2
@@ -403,34 +403,34 @@
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
+ fun make_cnfx_thm_from_nnf (Const (@{const_name "op &"}, _) $ x $ y) : thm =
let
val thm1 = make_cnfx_thm_from_nnf x
val thm2 = make_cnfx_thm_from_nnf y
in
conj_cong OF [thm1, thm2]
end
- | make_cnfx_thm_from_nnf (Const ("op |", _) $ x $ y) =
+ | make_cnfx_thm_from_nnf (Const (@{const_name "op |"}, _) $ x $ y) =
if is_clause x andalso is_clause y then
inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
else if is_literal y orelse is_literal x then let
(* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
(* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const ("op &", _) $ x1 $ x2) y' =
+ fun make_cnfx_disj_thm (Const (@{const_name "op &"}, _) $ x1 $ x2) y' =
let
val thm1 = make_cnfx_disj_thm x1 y'
val thm2 = make_cnfx_disj_thm x2 y'
in
make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
end
- | make_cnfx_disj_thm x' (Const ("op &", _) $ y1 $ y2) =
+ | make_cnfx_disj_thm x' (Const (@{const_name "op &"}, _) $ y1 $ y2) =
let
val thm1 = make_cnfx_disj_thm x' y1
val thm2 = make_cnfx_disj_thm x' y2
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const ("Ex", _) $ x') y' =
+ | make_cnfx_disj_thm (Const (@{const_name "Ex"}, _) $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const ("Ex", _) $ y') =
+ | make_cnfx_disj_thm x' (Const (@{const_name "Ex"}, _) $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()