src/HOL/Tools/cnf_funcs.ML

 
 val weakening_thm        = @{lemma "[| P; Q |] ==> Q" by auto};
 
 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;
 
 (* ------------------------------------------------------------------------- *)
 (* clause_is_trivial: a clause is trivially true if it contains both an atom *)
 (*      and the atom's negation                                              *)

 (* Term.term -> bool *)
 
 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
 		  | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
 	in

 (*      eliminated (possibly causing an exponential blowup)                  *)
 (* ------------------------------------------------------------------------- *)
 
 (* 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)
 		val thm3 = make_nnf_thm thy y
 		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
 	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)
 		val thm3 = make_nnf_thm thy y
 		val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
 	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
 		make_nnf_not_not OF [thm1]
 	end

 (*      (True, respectively).                                                *)
 (* ------------------------------------------------------------------------- *)
 
 (* 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
 	in
 		if x' = HOLogic.false_const then

 					simp_TF_conj_True_r OF [thm1, thm2]  (* (x & y) = x' *)
 				else
 					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
 	in
 		if x' = HOLogic.true_const then

 (* Theory.theory -> Term.term -> Thm.thm *)
 
 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
 				in
 					make_cnf_disj_conj_r OF [thm1, thm2]  (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)

 fun make_cnfx_thm thy t =
 let
 	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 ()
 					val thm2 = make_cnfx_disj_thm (betapply (x', var)) y'  (* (x' | y') = body' *)
 					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)
 					val thm4 = Thm.strip_shyps (thm3 COMP allI)            (* ALL v. (x' | y') = body' *)
 					val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
 				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 ()
 					val thm2 = make_cnfx_disj_thm x' (betapply (y', var))  (* (x' | y') = body' *)
 					val thm3 = Thm.forall_intr (cterm_of thy var) thm2     (* !!v. (x' | y') = body' *)