# HG changeset patch # User wenzelm # Date 1565195012 -7200 # Node ID 1dc3514c1719344abe4f0d3a89dda05b997ebd3e # Parent b203aaf373cf33ccdb07620c2aa0e50317d03a6c prefer named lemmas -- more compact proofterms; diff -r b203aaf373cf -r 1dc3514c1719 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Aug 07 17:43:48 2019 +0200 +++ b/src/HOL/HOL.thy Wed Aug 07 18:23:32 2019 +0200 @@ -1735,6 +1735,51 @@ val trans = @{thm trans} \ +locale cnf +begin + +lemma clause2raw_notE: "\P; \P\ \ False" by auto +lemma clause2raw_not_disj: "\\ P; \ Q\ \ \ (P \ Q)" by auto +lemma clause2raw_not_not: "P \ \\ P" by auto + +lemma iff_refl: "(P::bool) = P" by auto +lemma iff_trans: "[| (P::bool) = Q; Q = R |] ==> P = R" by auto +lemma conj_cong: "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto +lemma disj_cong: "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto + +lemma make_nnf_imp: "[| (\P) = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto +lemma make_nnf_iff: "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (P = Q) = ((P' \ NQ) \ (NP \ Q'))" by auto +lemma make_nnf_not_false: "(\False) = True" by auto +lemma make_nnf_not_true: "(\True) = False" by auto +lemma make_nnf_not_conj: "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto +lemma make_nnf_not_disj: "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto +lemma make_nnf_not_imp: "[| P = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto +lemma make_nnf_not_iff: "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (\(P = Q)) = ((P' \ Q') \ (NP \ NQ))" by auto +lemma make_nnf_not_not: "P = P' ==> (\\P) = P'" by auto + +lemma simp_TF_conj_True_l: "[| P = True; Q = Q' |] ==> (P \ Q) = Q'" by auto +lemma simp_TF_conj_True_r: "[| P = P'; Q = True |] ==> (P \ Q) = P'" by auto +lemma simp_TF_conj_False_l: "P = False ==> (P \ Q) = False" by auto +lemma simp_TF_conj_False_r: "Q = False ==> (P \ Q) = False" by auto +lemma simp_TF_disj_True_l: "P = True ==> (P \ Q) = True" by auto +lemma simp_TF_disj_True_r: "Q = True ==> (P \ Q) = True" by auto +lemma simp_TF_disj_False_l: "[| P = False; Q = Q' |] ==> (P \ Q) = Q'" by auto +lemma simp_TF_disj_False_r: "[| P = P'; Q = False |] ==> (P \ Q) = P'" by auto + +lemma make_cnf_disj_conj_l: "[| (P \ R) = PR; (Q \ R) = QR |] ==> ((P \ Q) \ R) = (PR \ QR)" by auto +lemma make_cnf_disj_conj_r: "[| (P \ Q) = PQ; (P \ R) = PR |] ==> (P \ (Q \ R)) = (PQ \ PR)" by auto + +lemma make_cnfx_disj_ex_l: "((\(x::bool). P x) \ Q) = (\x. P x \ Q)" by auto +lemma make_cnfx_disj_ex_r: "(P \ (\(x::bool). Q x)) = (\x. P \ Q x)" by auto +lemma make_cnfx_newlit: "(P \ Q) = (\x. (P \ x) \ (Q \ \x))" by auto +lemma make_cnfx_ex_cong: "(\(x::bool). P x = Q x) \ (\x. P x) = (\x. Q x)" by auto + +lemma weakening_thm: "[| P; Q |] ==> Q" by auto + +lemma cnftac_eq_imp: "[| P = Q; P |] ==> Q" by auto + +end + ML_file \Tools/cnf.ML\ diff -r b203aaf373cf -r 1dc3514c1719 src/HOL/Tools/cnf.ML --- a/src/HOL/Tools/cnf.ML Wed Aug 07 17:43:48 2019 +0200 +++ b/src/HOL/Tools/cnf.ML Wed Aug 07 18:23:32 2019 +0200 @@ -54,46 +54,6 @@ structure CNF : CNF = struct -val clause2raw_notE = @{lemma "\P; \P\ \ False" by auto}; -val clause2raw_not_disj = @{lemma "\\ P; \ Q\ \ \ (P \ Q)" by auto}; -val clause2raw_not_not = @{lemma "P \ \\ P" by auto}; - -val iff_refl = @{lemma "(P::bool) = P" by auto}; -val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto}; -val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; -val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; - -val make_nnf_imp = @{lemma "[| (\P) = P'; Q = Q' |] ==> (P \ Q) = (P' \ Q')" by auto}; -val make_nnf_iff = @{lemma "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (P = Q) = ((P' \ NQ) \ (NP \ Q'))" by auto}; -val make_nnf_not_false = @{lemma "(\False) = True" by auto}; -val make_nnf_not_true = @{lemma "(\True) = False" by auto}; -val make_nnf_not_conj = @{lemma "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_disj = @{lemma "[| (\P) = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_imp = @{lemma "[| P = P'; (\Q) = Q' |] ==> (\(P \ Q)) = (P' \ Q')" by auto}; -val make_nnf_not_iff = @{lemma "[| P = P'; (\P) = NP; Q = Q'; (\Q) = NQ |] ==> (\(P = Q)) = ((P' \ Q') \ (NP \ NQ))" by auto}; -val make_nnf_not_not = @{lemma "P = P' ==> (\\P) = P'" by auto}; - -val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P \ Q) = Q'" by auto}; -val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P \ Q) = P'" by auto}; -val simp_TF_conj_False_l = @{lemma "P = False ==> (P \ Q) = False" by auto}; -val simp_TF_conj_False_r = @{lemma "Q = False ==> (P \ Q) = False" by auto}; -val simp_TF_disj_True_l = @{lemma "P = True ==> (P \ Q) = True" by auto}; -val simp_TF_disj_True_r = @{lemma "Q = True ==> (P \ Q) = True" by auto}; -val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P \ Q) = Q'" by auto}; -val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P \ Q) = P'" by auto}; - -val make_cnf_disj_conj_l = @{lemma "[| (P \ R) = PR; (Q \ R) = QR |] ==> ((P \ Q) \ R) = (PR \ QR)" by auto}; -val make_cnf_disj_conj_r = @{lemma "[| (P \ Q) = PQ; (P \ R) = PR |] ==> (P \ (Q \ R)) = (PQ \ PR)" by auto}; - -val make_cnfx_disj_ex_l = @{lemma "((\(x::bool). P x) \ Q) = (\x. P x \ Q)" by auto}; -val make_cnfx_disj_ex_r = @{lemma "(P \ (\(x::bool). Q x)) = (\x. P \ Q x)" by auto}; -val make_cnfx_newlit = @{lemma "(P \ Q) = (\x. (P \ x) \ (Q \ \x))" by auto}; -val make_cnfx_ex_cong = @{lemma "(\(x::bool). P x = Q x) \ (\x. P x) = (\x. Q x)" by auto}; - -val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto}; - -val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto}; - fun is_atom (Const (\<^const_name>\False\, _)) = false | is_atom (Const (\<^const_name>\True\, _)) = false | is_atom (Const (\<^const_name>\HOL.conj\, _) $ _ $ _) = false @@ -141,7 +101,7 @@ thm else not_disj_to_prem (i+1) - (Seq.hd (REPEAT_DETERM (resolve_tac ctxt [clause2raw_not_disj] i) thm)) + (Seq.hd (REPEAT_DETERM (resolve_tac ctxt @{thms cnf.clause2raw_not_disj} i) thm)) (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *) (* becomes "[..., A1, ..., An] |- B" *) fun prems_to_hyps thm = @@ -149,11 +109,11 @@ Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm in (* [...] |- ~(x1 | ... | xn) ==> False *) - (clause2raw_notE OF [clause]) + (@{thm cnf.clause2raw_notE} OF [clause]) (* [...] |- ~x1 ==> ... ==> ~xn ==> False *) |> not_disj_to_prem 1 (* [...] |- x1' ==> ... ==> xn' ==> False *) - |> Seq.hd o TRYALL (resolve_tac ctxt [clause2raw_not_not]) + |> Seq.hd o TRYALL (resolve_tac ctxt @{thms cnf.clause2raw_not_not}) (* [..., x1', ..., xn'] |- False *) |> prems_to_hyps end; @@ -181,21 +141,21 @@ val thm1 = make_nnf_thm thy x val thm2 = make_nnf_thm thy y in - conj_cong OF [thm1, thm2] + @{thm cnf.conj_cong} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\HOL.disj\, _) $ x $ y) = let val thm1 = make_nnf_thm thy x val thm2 = make_nnf_thm thy y in - disj_cong OF [thm1, thm2] + @{thm cnf.disj_cong} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\HOL.implies\, _) $ 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] + @{thm cnf.make_nnf_imp} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\HOL.eq\, Type ("fun", \<^typ>\bool\ :: _)) $ x $ y) = let @@ -204,25 +164,25 @@ 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] + @{thm cnf.make_nnf_iff} OF [thm1, thm2, thm3, thm4] end | make_nnf_thm _ (Const (\<^const_name>\Not\, _) $ Const (\<^const_name>\False\, _)) = - make_nnf_not_false + @{thm cnf.make_nnf_not_false} | make_nnf_thm _ (Const (\<^const_name>\Not\, _) $ Const (\<^const_name>\True\, _)) = - make_nnf_not_true + @{thm cnf.make_nnf_not_true} | make_nnf_thm thy (Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\HOL.conj\, _) $ 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] + @{thm cnf.make_nnf_not_conj} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\HOL.disj\, _) $ 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] + @{thm cnf.make_nnf_not_disj} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\Not\, _) $ (Const (\<^const_name>\HOL.implies\, _) $ x $ y)) = @@ -230,7 +190,7 @@ val thm1 = make_nnf_thm thy x val thm2 = make_nnf_thm thy (HOLogic.Not $ y) in - make_nnf_not_imp OF [thm1, thm2] + @{thm cnf.make_nnf_not_imp} OF [thm1, thm2] end | make_nnf_thm thy (Const (\<^const_name>\Not\, _) $ @@ -241,15 +201,15 @@ 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] + @{thm cnf.make_nnf_not_iff} OF [thm1, thm2, thm3, thm4] end | 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] + @{thm cnf.make_nnf_not_not} OF [thm1] end - | make_nnf_thm thy t = inst_thm thy [t] iff_refl; + | make_nnf_thm thy t = inst_thm thy [t] @{thm cnf.iff_refl}; fun make_under_quantifiers ctxt make t = let @@ -287,20 +247,20 @@ val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 in if x' = \<^term>\False\ then - simp_TF_conj_False_l OF [thm1] (* (x & y) = False *) + @{thm cnf.simp_TF_conj_False_l} OF [thm1] (* (x & y) = False *) else let val thm2 = simp_True_False_thm thy y val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm2 in if x' = \<^term>\True\ then - simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *) + @{thm cnf.simp_TF_conj_True_l} OF [thm1, thm2] (* (x & y) = y' *) else if y' = \<^term>\False\ then - simp_TF_conj_False_r OF [thm2] (* (x & y) = False *) + @{thm cnf.simp_TF_conj_False_r} OF [thm2] (* (x & y) = False *) else if y' = \<^term>\True\ then - simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *) + @{thm cnf.simp_TF_conj_True_r} OF [thm1, thm2] (* (x & y) = x' *) else - conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *) + @{thm cnf.conj_cong} OF [thm1, thm2] (* (x & y) = (x' & y') *) end end | simp_True_False_thm thy (Const (\<^const_name>\HOL.disj\, _) $ x $ y) = @@ -309,23 +269,23 @@ val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 in if x' = \<^term>\True\ then - simp_TF_disj_True_l OF [thm1] (* (x | y) = True *) + @{thm cnf.simp_TF_disj_True_l} OF [thm1] (* (x | y) = True *) else let val thm2 = simp_True_False_thm thy y val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm2 in if x' = \<^term>\False\ then - simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *) + @{thm cnf.simp_TF_disj_False_l} OF [thm1, thm2] (* (x | y) = y' *) else if y' = \<^term>\True\ then - simp_TF_disj_True_r OF [thm2] (* (x | y) = True *) + @{thm cnf.simp_TF_disj_True_r} OF [thm2] (* (x | y) = True *) else if y' = \<^term>\False\ then - simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *) + @{thm cnf.simp_TF_disj_False_r} OF [thm1, thm2] (* (x | y) = x' *) else - disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + @{thm cnf.disj_cong} OF [thm1, thm2] (* (x | y) = (x' | y') *) end end - | simp_True_False_thm thy t = inst_thm thy [t] iff_refl; (* t = t *) + | simp_True_False_thm thy t = inst_thm thy [t] @{thm cnf.iff_refl}; (* t = t *) (* ------------------------------------------------------------------------- *) (* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *) @@ -341,7 +301,7 @@ val thm1 = make_cnf_thm_from_nnf x val thm2 = make_cnf_thm_from_nnf y in - conj_cong OF [thm1, thm2] + @{thm cnf.conj_cong} OF [thm1, thm2] end | make_cnf_thm_from_nnf (Const (\<^const_name>\HOL.disj\, _) $ x $ y) = let @@ -351,26 +311,26 @@ 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')') *) + @{thm cnf.make_cnf_disj_conj_l} OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) end | make_cnf_disj_thm x' (Const (\<^const_name>\HOL.conj\, _) $ 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)') *) + @{thm cnf.make_cnf_disj_conj_r} OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) end | make_cnf_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + inst_thm thy [HOLogic.mk_disj (x', y')] @{thm cnf.iff_refl} (* (x' | y') = (x' | y') *) val thm1 = make_cnf_thm_from_nnf x val thm2 = make_cnf_thm_from_nnf y val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + val disj_thm = @{thm cnf.disj_cong} OF [thm1, thm2] (* (x | y) = (x' | y') *) in - iff_trans OF [disj_thm, make_cnf_disj_thm x' y'] + @{thm cnf.iff_trans} OF [disj_thm, make_cnf_disj_thm x' y'] end - | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl + | make_cnf_thm_from_nnf t = inst_thm thy [t] @{thm cnf.iff_refl} (* convert 't' to NNF first *) val nnf_thm = make_nnf_thm_under_quantifiers ctxt t (*### @@ -386,7 +346,7 @@ val cnf_thm = make_cnf_thm_from_nnf simp *) in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm] + @{thm cnf.iff_trans} OF [@{thm cnf.iff_trans} OF [nnf_thm, simp_thm], cnf_thm] end; (* ------------------------------------------------------------------------- *) @@ -414,11 +374,11 @@ val thm1 = make_cnfx_thm_from_nnf x val thm2 = make_cnfx_thm_from_nnf y in - conj_cong OF [thm1, thm2] + @{thm cnf.conj_cong} OF [thm1, thm2] end | make_cnfx_thm_from_nnf (Const (\<^const_name>\HOL.disj\, _) $ x $ y) = if is_clause x andalso is_clause y then - inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl + inst_thm thy [HOLogic.mk_disj (x, y)] @{thm cnf.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 *) @@ -428,60 +388,60 @@ 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')') *) + @{thm cnf.make_cnf_disj_conj_l} OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *) end | make_cnfx_disj_thm x' (Const (\<^const_name>\HOL.conj\, _) $ 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)') *) + @{thm cnf.make_cnf_disj_conj_r} OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *) end | make_cnfx_disj_thm (\<^term>\Ex :: (bool \ bool) \ bool\ $ x') y' = let - val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *) + val thm1 = inst_thm thy [x', y'] @{thm cnf.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 (Thm.global_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') *) + val thm5 = Thm.strip_shyps (thm4 RS @{thm cnf.make_cnfx_ex_cong}) (* (EX v. (x' | y')) = (EX v. body') *) in - iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) + @{thm cnf.iff_trans} OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *) end | make_cnfx_disj_thm x' (\<^term>\Ex :: (bool \ bool) \ bool\ $ y') = let - val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *) + val thm1 = inst_thm thy [x', y'] @{thm cnf.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 (Thm.global_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') *) + val thm5 = Thm.strip_shyps (thm4 RS @{thm cnf.make_cnfx_ex_cong}) (* (EX v. (x' | y')) = (EX v. body') *) in - iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) + @{thm cnf.iff_trans} OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *) end | make_cnfx_disj_thm x' y' = - inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *) + inst_thm thy [HOLogic.mk_disj (x', y')] @{thm cnf.iff_refl} (* (x' | y') = (x' | y') *) val thm1 = make_cnfx_thm_from_nnf x val thm2 = make_cnfx_thm_from_nnf y val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm1 val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm2 - val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *) + val disj_thm = @{thm cnf.disj_cong} OF [thm1, thm2] (* (x | y) = (x' | y') *) in - iff_trans OF [disj_thm, make_cnfx_disj_thm x' y'] + @{thm cnf.iff_trans} OF [disj_thm, make_cnfx_disj_thm x' y'] end else let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *) - val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *) + val thm1 = inst_thm thy [x, y] @{thm cnf.make_cnfx_newlit} (* (x | y) = EX v. (x | v) & (y | ~v) *) val var = new_free () val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var)) val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *) val thm3 = Thm.forall_intr (Thm.global_cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *) val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *) - val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) + val thm5 = Thm.strip_shyps (thm4 RS @{thm cnf.make_cnfx_ex_cong}) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *) in - iff_trans OF [thm1, thm5] + @{thm cnf.iff_trans} OF [thm1, thm5] end - | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl + | make_cnfx_thm_from_nnf t = inst_thm thy [t] @{thm cnf.iff_refl} (* convert 't' to NNF first *) val nnf_thm = make_nnf_thm_under_quantifiers ctxt t (* ### @@ -509,7 +469,7 @@ val cnfx_thm = make_cnfx_thm_from_nnf simp *) in - iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm] + @{thm cnf.iff_trans} OF [@{thm cnf.iff_trans} OF [nnf_thm, simp_thm], cnfx_thm] end; (* ------------------------------------------------------------------------- *) @@ -521,7 +481,7 @@ (* ------------------------------------------------------------------------- *) fun weakening_tac ctxt i = - dresolve_tac ctxt [weakening_thm] i THEN assume_tac ctxt (i+1); + dresolve_tac ctxt @{thms cnf.weakening_thm} i THEN assume_tac ctxt (i+1); (* ------------------------------------------------------------------------- *) (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *) @@ -534,7 +494,7 @@ Subgoal.FOCUS (fn {prems, context = ctxt', ...} => let val cnf_thms = map (make_cnf_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems - val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems) + val cut_thms = map (fn (th, pr) => @{thm cnf.cnftac_eq_imp} OF [th, pr]) (cnf_thms ~~ prems) in cut_facts_tac cut_thms 1 end) ctxt i @@ -556,7 +516,7 @@ Subgoal.FOCUS (fn {prems, context = ctxt', ...} => let val cnfx_thms = map (make_cnfx_thm ctxt' o HOLogic.dest_Trueprop o Thm.prop_of) prems - val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems) + val cut_thms = map (fn (th, pr) => @{thm cnf.cnftac_eq_imp} OF [th, pr]) (cnfx_thms ~~ prems) in cut_facts_tac cut_thms 1 end) ctxt i