(* Title: HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
Author: Nik Sultana, Cambridge University Computer Laboratory
Unit tests for proof reconstruction module.
*)
theory TPTP_Proof_Reconstruction_Test_Units
imports TPTP_Test TPTP_Proof_Reconstruction
begin
declare [[ML_exception_trace, ML_print_depth = 200]]
declare [[tptp_trace_reconstruction = true]]
lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \ ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
oops
lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \ ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
apply (rule allI)+
apply (tactic \<open>nominal_inst_parametermatch_tac @{context} @{thm allE} 1\<close>)+
oops
(*Could test bind_tac further with NUM667^1 inode43*)
(*
(* SEU581^2.p_nux *)
(* (Annotated_step ("inode1", "bind"), *)
lemma "\(SV5::TPTP_Interpret.ind \ bool)
SV6::TPTP_Interpret.ind.
(bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
(bnd_powerset bnd_sK1_A) =
bnd_in (bnd_dsetconstr SV6 SV5)
(bnd_powerset SV6)) =
False \<Longrightarrow>
(bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
(bnd_powerset bnd_sK1_A) =
bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
(bnd_powerset bnd_sK1_A)) =
False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;
val binds =
[Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))), Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))])))]
(* |> TPTP_Reconstruct.permute *)
(*
val binds =
[Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))),
Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))
]
*)
val tec =
(*
map (bind_tac @{context} (hd prob_names)) binds
|> FIRST
*)
bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done
(* (Annotated_step ("inode2", "bind"), *)
lemma "\(SV7::TPTP_Interpret.ind) SV8::TPTP_Interpret.ind.
(bnd_subset SV8 SV7 =
bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
bnd_sK1_A) =
False \<or>
bnd_in SV8 (bnd_powerset SV7) = False \<Longrightarrow>
(bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
bnd_sK1_A =
bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
bnd_sK1_A) =
False \<or>
bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
(bnd_powerset bnd_sK1_A) =
False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;
val binds =
[Bind ("SV8", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "dsetconstr", []))), Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))]), Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))])), Bind ("SV7", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))]
(* |> TPTP_Reconstruct.permute *)
val tec =
(*
map (bind_tac @{context} (hd prob_names)) binds
|> FIRST
*)
bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done
*)
(*
from SEU897^5
lemma "
\<forall>SV9 SV10 SV11 SV12 SV13 SV14.
(((((bnd_sK5_SY14 SV14 SV13 SV12 = SV11) = False \<or>
(bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 SV11)) =
False) \<or>
bnd_cR SV14 = False) \<or>
(SV12 = SV13 SV14) = False) \<or>
bnd_cR SV9 = False) \<or>
(SV11 = SV10 SV9) = False \<Longrightarrow>
\<forall>SV14 SV13 SV12 SV10 SV9.
(((((bnd_sK5_SY14 SV14 SV13 SV12 =
bnd_sK5_SY14 SV14 SV13 SV12) =
False \<or>
(bnd_sK4_SX0 =
SV10
(bnd_sK5_SY14 SV9 SV10
(bnd_sK5_SY14 SV14 SV13 SV12))) =
False) \<or>
bnd_cR SV14 = False) \<or>
(SV12 = SV13 SV14) = False) \<or>
bnd_cR SV9 = False) \<or>
(bnd_sK5_SY14 SV14 SV13 SV12 = SV10 SV9) = False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;
val binds =
[Bind ("SV11", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK5_SY14", []))), Atom (THF_Atom_term (Term_Var "SV14"))]), Atom (THF_Atom_term (Term_Var "SV13"))]), Atom (THF_Atom_term (Term_Var "SV12"))]))]
val tec = bind_tac @{context} (hd prob_names) binds
*}
apply (tactic {*tec*})
done
*)
subsection "Interpreting the inferences"
(*from SET598^5
lemma "(bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
(\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
(\<forall>SY27.
(\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
(\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
(\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30))) =
False \<Longrightarrow>
(\<not> (bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
(\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
(\<forall>SY27.
(\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
(\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
(\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)))) =
True"
apply (tactic {*polarity_switch_tac @{context}*})
done
lemma "
(((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
(\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
(\<forall>SY27.
(\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
(\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
(\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17)) =
False \<Longrightarrow>
(\<not> (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
(\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
(\<forall>SY27.
(\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
(\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
(\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17))) =
True"
apply (tactic {*polarity_switch_tac @{context}*})
done
*)
(* beware lack of type annotations
(* lemma "!!x. (A x = B x) = False ==> (B x = A x) = False" *)
(* lemma "!!x. (A x = B x) = True ==> (B x = A x) = True" *)
(* lemma "((A x) = (B x)) = True ==> ((B x) = (A x)) = True" *)
lemma "(A = B) = True ==> (B = A) = True"
*)
lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False"
apply (tactic \<open>expander_animal @{context} 1\<close>)
oops
lemma "(A & B) ==> ~(~A | ~B)"
by (tactic \<open>expander_animal @{context} 1\<close>)
lemma "(A | B) ==> ~(~A & ~B)"
by (tactic \<open>expander_animal @{context} 1\<close>)
lemma "(A | B) | C ==> A | (B | C)"
by (tactic \<open>expander_animal @{context} 1\<close>)
lemma "(~~A) = B ==> A = B"
by (tactic \<open>expander_animal @{context} 1\<close>)
lemma "~ ~ (A = True) ==> A = True"
by (tactic \<open>expander_animal @{context} 1\<close>)
(*This might not be a goal which might realistically arise:
lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *)
lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))"
apply (tactic \<open>expander_animal @{context} 1\<close>)+
apply (rule conjI)
apply assumption
apply (rule sym, assumption)
done
lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))"
by (tactic \<open>expander_animal @{context} 1\<close>)+
(*some lemmas assume constants in the signature of PUZ114^5*)
consts
PUZ114_5_bnd_sK1 :: "TPTP_Interpret.ind"
PUZ114_5_bnd_sK2 :: "TPTP_Interpret.ind"
PUZ114_5_bnd_sK3 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
PUZ114_5_bnd_sK4 :: "(TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind"
PUZ114_5_bnd_sK5 :: "(TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind"
PUZ114_5_bnd_s :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
PUZ114_5_bnd_c1 :: TPTP_Interpret.ind
(*testing logical expansion*)
lemma "!! SY30. (SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1 \
(\<forall>Xj Xk.
SY30 Xj Xk \<longrightarrow>
SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)) \<longrightarrow>
SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2)
==> (
(~ SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1)
| (~ (\<forall>Xj Xk.
SY30 Xj Xk \<longrightarrow>
SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)))
| SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2
)"
by (tactic \<open>expander_animal @{context} 1\<close>)+
(*
extcnf_forall_pos:
(! X. L1) | ... | Ln
---------------------------- X' fresh
! X'. (L1[X'/X] | ... | Ln)
After elimination rule has been applied we'll have a subgoal which looks like this:
(! X. L1)
---------------------------- X' fresh
! X'. (L1[X'/X] | ... | Ln)
and we need to transform it so that, in Isabelle, we go from
(! X. L1) ==> ! X'. (L1[X'/X] | ... | Ln)
to
\<And> X'. L1[X'/X] ==> (L1[X'/X] | ... | Ln)
(where X' is fresh, or renamings are done suitably).*)
lemma "A | B \ A | B | C"
apply (tactic \<open>flip_conclusion_tac @{context} 1\<close>)+
apply (tactic \<open>break_hypotheses 1\<close>)+
oops
consts
CSR122_1_bnd_lBill_THFTYPE_i :: TPTP_Interpret.ind
CSR122_1_bnd_lMary_THFTYPE_i :: TPTP_Interpret.ind
CSR122_1_bnd_lSue_THFTYPE_i :: TPTP_Interpret.ind
CSR122_1_bnd_n2009_THFTYPE_i :: TPTP_Interpret.ind
CSR122_1_bnd_lYearFn_THFTYPE_IiiI :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
CSR122_1_bnd_holdsDuring_THFTYPE_IiooI ::
"TPTP_Interpret.ind \ bool \ bool"
CSR122_1_bnd_likes_THFTYPE_IiioI ::
"TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
lemma "\SV2. (CSR122_1_bnd_holdsDuring_THFTYPE_IiooI
(CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i)
(\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
CSR122_1_bnd_lMary_THFTYPE_i
CSR122_1_bnd_lBill_THFTYPE_i \<or>
\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
CSR122_1_bnd_lSue_THFTYPE_i
CSR122_1_bnd_lBill_THFTYPE_i)) =
CSR122_1_bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
False \<Longrightarrow>
\<forall>SV2. (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i =
SV2) =
False \<or>
((\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i \<or>
\<not> CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i
CSR122_1_bnd_lBill_THFTYPE_i)) =
True) =
False"
apply (rule allI, erule_tac x = "SV2" in allE)
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
done
(*SEU882^5*)
(*
lemma
"\<forall>(SV2::TPTP_Interpret.ind)
SV1::TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind.
(SV1 SV2 = bnd_sK1_Xy) =
False
\<Longrightarrow>
\<forall>SV2::TPTP_Interpret.ind.
(bnd_sK1_Xy = bnd_sK1_Xy) =
False"
ML_prf {*
open TPTP_Syntax;
open TPTP_Proof;
val binds =
[Bind ("SV1", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_Xy", [])))))]
val tec = bind_tac @{context} (hd prob_names) binds
*}
(*
apply (tactic {*strip_qtfrs
(* THEN tec *)
*)
apply (tactic {*tec*})
done
*)
lemma "A | B \ C1 | A | C2 | B | C3"
apply (erule disjE)
apply (tactic \<open>clause_breaker 1\<close>)
apply (tactic \<open>clause_breaker 1\<close>)
done
lemma "A \ A"
apply (tactic \<open>clause_breaker 1\<close>)
done
typedecl NUM667_1_bnd_nat
consts
NUM667_1_bnd_less :: "NUM667_1_bnd_nat \ NUM667_1_bnd_nat \ bool"
NUM667_1_bnd_x :: NUM667_1_bnd_nat
NUM667_1_bnd_y :: NUM667_1_bnd_nat
(*NUM667^1 node 302 -- dec*)
lemma "\SV12 SV13 SV14 SV9 SV10 SV11.
((((NUM667_1_bnd_less SV12 SV13 = NUM667_1_bnd_less SV11 SV10) = False \<or>
(SV14 = SV13) = False) \<or>
NUM667_1_bnd_less SV12 SV14 = False) \<or>
NUM667_1_bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) =
False \<Longrightarrow>
\<forall>SV9 SV14 SV10 SV13 SV11 SV12.
(((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
(SV14 = SV13) = False) \<or>
NUM667_1_bnd_less SV12 SV14 = False) \<or>
NUM667_1_bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) =
False"
apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
apply (tactic \<open>break_hypotheses 1\<close>)
apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
done
ML \<open>
extuni_dec_n @{context} 2;
\<close>
(*NUM667^1, node 202*)
lemma "\SV9 SV10 SV11.
((((SV9 = SV11) = (NUM667_1_bnd_x = NUM667_1_bnd_y)) = False \<or>
NUM667_1_bnd_less SV11 SV10 = False) \<or>
NUM667_1_bnd_less SV9 SV10 = True) \<or>
NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
True \<Longrightarrow>
\<forall>SV10 SV9 SV11.
((((SV11 = NUM667_1_bnd_x) = False \<or> (SV9 = NUM667_1_bnd_y) = False) \<or>
NUM667_1_bnd_less SV11 SV10 = False) \<or>
NUM667_1_bnd_less SV9 SV10 = True) \<or>
NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
True"
apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
apply (tactic \<open>break_hypotheses 1\<close>)
apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
done
(*NUM667^1 node 141*)
(*
lemma "((bnd_x = bnd_x) = False \<or> (bnd_y = bnd_z) = False) \<or>
bnd_less bnd_x bnd_y = True \<Longrightarrow>
(bnd_y = bnd_z) = False \<or> bnd_less bnd_x bnd_y = True"
apply (tactic {*strip_qtfrs*})
apply (tactic {*break_hypotheses 1*})
apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
apply (erule extuni_triv)
done
*)
ML \<open>
fun full_extcnf_combined_tac ctxt =
extcnf_combined_tac ctxt NONE
[ConstsDiff,
StripQuantifiers,
Flip_Conclusion,
Loop [
Close_Branch,
ConjI,
King_Cong,
Break_Hypotheses,
Existential_Free,
Existential_Var,
Universal,
RemoveRedundantQuantifications],
CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates],
AbsorbSkolemDefs]
[]
\<close>
ML \<open>
fun nonfull_extcnf_combined_tac ctxt feats =
extcnf_combined_tac ctxt NONE
[ConstsDiff,
StripQuantifiers,
InnerLoopOnce (Break_Hypotheses :: feats),
AbsorbSkolemDefs]
[]
\<close>
consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind
lemma
"\SV2. (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False \
(SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False"
(* apply (erule_tac x = "(@X. False)" in allE) *)
(* apply (tactic {*remove_redundant_quantification 1*}) *)
(* apply assumption *)
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]\<close>)
(*NUM667^1*)
(*
(* (Annotated_step ("153", "extuni_triv"), *)
lemma "((bnd_y = bnd_x) = False \ (bnd_z = bnd_z) = False) \
(bnd_y = bnd_z) = True \<Longrightarrow>
(bnd_y = bnd_x) = False \<or> (bnd_y = bnd_z) = True"
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
done
(* (Annotated_step ("162", "extuni_triv"), *)
lemma "((bnd_y = bnd_x) = False \ (bnd_z = bnd_z) = False) \
bnd_less bnd_y bnd_z = True \<Longrightarrow>
(bnd_y = bnd_x) = False \<or> bnd_less bnd_y bnd_z = True"
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
done
*)
(* SEU602^2 *)
consts
SEU602_2_bnd_sK7_E :: "(TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind"
SEU602_2_bnd_sK2_SY17 :: TPTP_Interpret.ind
SEU602_2_bnd_in :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
(* (Annotated_step ("113", "extuni_func"), *)
lemma "\SV49::TPTP_Interpret.ind \ bool.
(SV49 =
(\<lambda>SY23::TPTP_Interpret.ind.
\<not> SEU602_2_bnd_in SY23 SEU602_2_bnd_sK2_SY17)) =
False \<Longrightarrow>
\<forall>SV49::TPTP_Interpret.ind \<Rightarrow> bool.
(SV49 (SEU602_2_bnd_sK7_E SV49) =
(\<not> SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
False"
(*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]\<close>)
consts
SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind"
SEV405_5_bnd_cA :: bool
lemma "\SV1::TPTP_Interpret.ind \ bool.
(\<forall>SY2::TPTP_Interpret.ind.
\<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
\<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
False \<Longrightarrow>
\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
(\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
\<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
(*
strip quantifiers -- creating a space of permutations; from shallowest to deepest (iterative deepening)
flip the conclusion -- giving us branch
apply some collection of rules, in some order, until the space has been explored completely. advantage of not having extcnf_combined: search space is shallow -- particularly if the collection of rules is small.
*)
consts
SEU581_2_bnd_sK1 :: "TPTP_Interpret.ind"
SEU581_2_bnd_sK2 :: "TPTP_Interpret.ind \ bool"
SEU581_2_bnd_subset :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ HOL.bool"
SEU581_2_bnd_dsetconstr :: "TPTP_Interpret.ind \ (TPTP_Interpret.ind \ HOL.bool) \ TPTP_Interpret.ind"
(*testing parameters*)
lemma "! X :: TPTP_Interpret.ind . (\A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> ! X :: TPTP_Interpret.ind . (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "(A & B) = True ==> (A | B) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "(\ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \ (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing goals with parameters*)
lemma "(\ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \ ! X. (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "(A & B) = True ==> (B & A) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*appreciating differences between THEN, REPEAT, and APPEND*)
lemma "A & B ==> B & A"
apply (tactic \<open>
TRY (etac @{thm conjE} 1)
THEN TRY (rtac @{thm conjI} 1)\<close>)
by assumption+
lemma "A & B ==> B & A"
by (tactic \<open>
etac @{thm conjE} 1
THEN rtac @{thm conjI} 1
THEN REPEAT (atac 1)\<close>)
lemma "A & B ==> B & A"
apply (tactic \<open>
rtac @{thm conjI} 1
APPEND etac @{thm conjE} 1\<close>)+
back
by assumption+
consts
SEU581_2_bnd_sK3 :: "TPTP_Interpret.ind"
SEU581_2_bnd_sK4 :: "TPTP_Interpret.ind"
SEU581_2_bnd_sK5 :: "(TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind"
SEU581_2_bnd_powerset :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
SEU581_2_bnd_in :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
consts
bnd_c1 :: TPTP_Interpret.ind
bnd_s :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
lemma "(\SX0. (\ (\ SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \
\<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
(PUZ114_5_bnd_sK5 SX0) \<or>
\<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
(bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
\<not> SX0 bnd_c1 bnd_c1) \<or>
SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
True ==> \<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
\<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
(PUZ114_5_bnd_sK5 SV1) \<or>
\<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
(bnd_s (PUZ114_5_bnd_sK5 SV1)))) \<or>
\<not> SV1 bnd_c1 bnd_c1) \<or>
SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "(\ SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = True \ (SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = False"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing repeated application of simulator*)
lemma "(\ \ False) = True \
SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
False = True \<or> False = True \<or> False = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*Testing non-normal conclusion. Ideally we should be able to apply
the tactic to arbitrary chains of extcnf steps -- where it's not
generally the case that the conclusions are normal.*)
lemma "(\ \ False) = True \
SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
(\<not> False) = False"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing repeated application of simulator, involving different extcnf rules*)
lemma "(\ \ (False | False)) = True \
SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
False = True \<or> False = True \<or> False = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing logical expansion*)
lemma "(\A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing extcnf_forall_pos*)
lemma "(\A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True \ \SV1. (\SY14.
SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14)
(SEU581_2_bnd_powerset SV1)) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "((\A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True) | ((~ False) = False) \
\<forall>SV1. ((\<forall>SY14. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True) | ((~ False) = False)"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing parameters*)
lemma "(\A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> ! X. (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "((? A .P1 A) = False) | P2 = True \ !X. ((P1 X) = False | P2 = True)"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) \ !X. (P1a X = True | P1b X = True | P2 = True)"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \ ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \ ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \ ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
consts dud_bnd_s :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
(*this lemma kills blast*)
lemma "(\ (\SX0 SX1.
\<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or> PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SX0)) SX1) \<or>
\<not> (\<forall>SX0 SX1.
\<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
False \<Longrightarrow> (\<not> (\<forall>SX0 SX1.
\<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
False"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing logical expansion -- this should be done by blast*)
lemma "(\A B. bnd_in B (bnd_powerset A) \ SEU581_2_bnd_subset B A) = True
\<Longrightarrow> (\<forall>A B. \<not> bnd_in B (bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
(*testing related to PUZ114^5.p.out*)
lemma "\SV1. ((\ (\ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \
\<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
(PUZ114_5_bnd_sK5 SV1) \<or>
\<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
(bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
True \<or>
(\<not> SV1 bnd_c1 bnd_c1) = True) \<or>
SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True \<Longrightarrow>
\<forall>SV1. (SV1 bnd_c1 bnd_c1 = False \<or>
(\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
\<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
(PUZ114_5_bnd_sK5 SV1) \<or>
\<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
(bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
True) \<or>
SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "\SV2. (\SY41.
\<not> PUZ114_5_bnd_sK3 SV2 SY41 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SY41) =
True \<Longrightarrow>
\<forall>SV4 SV2.
(\<not> PUZ114_5_bnd_sK3 SV2 SV4 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) =
True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
lemma "\SV3. (\SY42.
\<not> PUZ114_5_bnd_sK3 SV3 SY42 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SY42)) =
True \<Longrightarrow>
\<forall>SV5 SV3.
(\<not> PUZ114_5_bnd_sK3 SV3 SV5 \<or>
PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) =
True"
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
subsection "unfold_def"
(* (Annotated_step ("9", "unfold_def"), *)
lemma "bnd_kpairiskpair =
(ALL Xx Xy.
bnd_iskpair
(bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset))) &
bnd_kpair =
(%Xx Xy.
bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset)) &
bnd_iskpair =
(%A. EX Xx. bnd_in Xx (bnd_setunion A) &
(EX Xy. bnd_in Xy (bnd_setunion A) &
A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin Xx
(bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset))) &
(~ (ALL SY0 SY1.
EX SY3.
bnd_in SY3
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
bnd_emptyset))) &
(EX SY4.
bnd_in SY4
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY0
(bnd_setadjoin SY1 bnd_emptyset))
bnd_emptyset))) &
bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
bnd_emptyset) =
bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
bnd_emptyset)))) =
True
==> (~ (ALL SX0 SX1.
~ (ALL SX2.
~ ~ (~ bnd_in SX2
(bnd_setunion
(bnd_setadjoin
(bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) |
~ ~ (ALL SX3.
~ ~ (~ bnd_in SX3
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
bnd_emptyset))) |
bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
bnd_emptyset) ~=
bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
bnd_emptyset))))))) =
True"
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(* (Annotated_step ("10", "unfold_def"), *)
lemma "bnd_kpairiskpair =
(ALL Xx Xy.
bnd_iskpair
(bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset))) &
bnd_kpair =
(%Xx Xy.
bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset)) &
bnd_iskpair =
(%A. EX Xx. bnd_in Xx (bnd_setunion A) &
(EX Xy. bnd_in Xy (bnd_setunion A) &
A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin Xx
(bnd_setadjoin Xy bnd_emptyset))
bnd_emptyset))) &
(ALL SY5 SY6.
EX SY7.
bnd_in SY7
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
bnd_emptyset))) &
(EX SY8.
bnd_in SY8
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
bnd_emptyset))) &
bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
bnd_emptyset) =
bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset))
bnd_emptyset))) =
True
==> (ALL SX0 SX1.
~ (ALL SX2.
~ ~ (~ bnd_in SX2
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin
(bnd_setadjoin SX0
(bnd_setadjoin SX1 bnd_emptyset))
bnd_emptyset))) |
~ ~ (ALL SX3.
~ ~ (~ bnd_in SX3
(bnd_setunion
(bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
bnd_emptyset))) |
bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
bnd_emptyset) ~=
bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
(bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
bnd_emptyset)))))) =
True"
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(* (Annotated_step ("12", "unfold_def"), *)
lemma "bnd_cCKB6_BLACK =
(\<lambda>Xu Xv.
\<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
(\<forall>Xj Xk.
Xw Xj Xk \<longrightarrow>
Xw (bnd_s (bnd_s Xj)) Xk \<and>
Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
Xw Xu Xv) \<and>
((((\<forall>SY36 SY37.
\<not> PUZ114_5_bnd_sK3 SY36 SY37 \<or>
PUZ114_5_bnd_sK3 (bnd_s (bnd_s SY36)) SY37) \<and>
(\<forall>SY38 SY39.
\<not> PUZ114_5_bnd_sK3 SY38 SY39 \<or>
PUZ114_5_bnd_sK3 (bnd_s SY38) (bnd_s SY39))) \<and>
PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<and>
\<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
(bnd_s PUZ114_5_bnd_sK2)) =
True \<Longrightarrow>
(\<not> (\<not> \<not> (\<not> \<not> (\<not> (\<forall>SX0 SX1.
\<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
PUZ114_5_bnd_sK3 (bnd_s (bnd_s SX0)) SX1) \<or>
\<not> (\<forall>SX0 SX1.
\<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
PUZ114_5_bnd_sK3 (bnd_s SX0) (bnd_s SX1))) \<or>
\<not> PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<or>
\<not> \<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
(bnd_s PUZ114_5_bnd_sK2))) =
True"
(*
apply (erule conjE)+
apply (erule subst)+
apply (tactic {*log_expander 1*})+
apply (rule refl)
*)
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(* (Annotated_step ("13", "unfold_def"), *)
lemma "bnd_cCKB6_BLACK =
(\<lambda>Xu Xv.
\<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
(\<forall>Xj Xk.
Xw Xj Xk \<longrightarrow>
Xw (bnd_s (bnd_s Xj)) Xk \<and>
Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
Xw Xu Xv) \<and>
(\<forall>SY30.
(SY30 (PUZ114_5_bnd_sK4 SY30) (PUZ114_5_bnd_sK5 SY30) \<and>
(\<not> SY30 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SY30)))
(PUZ114_5_bnd_sK5 SY30) \<or>
\<not> SY30 (bnd_s (PUZ114_5_bnd_sK4 SY30))
(bnd_s (PUZ114_5_bnd_sK5 SY30))) \<or>
\<not> SY30 bnd_c1 bnd_c1) \<or>
SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
True \<Longrightarrow>
(\<forall>SX0. (\<not> (\<not> SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \<or>
\<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
(PUZ114_5_bnd_sK5 SX0) \<or>
\<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
(bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
\<not> SX0 bnd_c1 bnd_c1) \<or>
SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
True"
(*
apply (erule conjE)+
apply (tactic {*expander_animal 1*})+
apply assumption
*)
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(*FIXME move this heuristic elsewhere*)
ML \<open>
(*Other than the list (which must not be empty) this function
expects a parameter indicating the smallest integer.
(Using Int.minInt isn't always viable).*)
fun max_int_floored min l =
if null l then raise List.Empty
else fold (curry Int.max) l min;
val _ = @{assert} (max_int_floored ~101002 [1] = 1)
val _ = @{assert} (max_int_floored 0 [1, 3, 5] = 5)
fun max_index_floored min l =
let
val max = max_int_floored min l
in find_index (pair max #> (=)) l end
\<close>
ML \<open>
max_index_floored 0 [1, 3, 5]
\<close>
ML \<open>
(*
Given argument ([h_1, ..., h_n], conc),
obtained from term of form
h_1 ==> ... ==> h_n ==> conclusion,
this function indicates which h_i is biggest,
or NONE if h_n = 0.
*)
fun biggest_hypothesis (hypos, _) =
if null hypos then NONE
else
map size_of_term hypos
|> max_index_floored 0
|> SOME
\<close>
ML \<open>
fun biggest_hyp_first_tac i = fn st =>
let
val results = TERMFUN biggest_hypothesis (SOME i) st
in
if null results then no_tac st
else
let
val result = the_single results
in
case result of
NONE => no_tac st
| SOME n =>
if n > 0 then rotate_tac n i st else no_tac st
end
end
\<close>
(* (Annotated_step ("6", "unfold_def"), *)
lemma "(\ (\U :: TPTP_Interpret.ind \ bool. \V. U V = SEV405_5_bnd_cA)) = True \
(\<not> \<not> (\<forall>SX0 :: TPTP_Interpret.ind \<Rightarrow> bool. \<not> (\<forall>SX1. \<not> (\<not> (\<not> SX0 SX1 \<or> SEV405_5_bnd_cA) \<or>
\<not> (\<not> SEV405_5_bnd_cA \<or> SX0 SX1))))) =
True"
(* by (tactic {*unfold_def_tac []*}) *)
oops
subsection "Using leo2_tac"
(*these require PUZ114^5's proof to be loaded
ML {*leo2_tac @{context} (hd prob_names) "50"*}
ML {*leo2_tac @{context} (hd prob_names) "4"*}
ML {*leo2_tac @{context} (hd prob_names) "9"*}
(* (Annotated_step ("9", "extcnf_combined"), *)
lemma "(\SY30.
SY30 bnd_c1 bnd_c1 \<and>
(\<forall>Xj Xk.
SY30 Xj Xk \<longrightarrow>
SY30 (bnd_s (bnd_s Xj)) Xk \<and>
SY30 (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
SY30 bnd_sK1 bnd_sK2) =
True \<Longrightarrow>
(\<forall>SY30.
(SY30 (bnd_sK4 SY30) (bnd_sK5 SY30) \<and>
(\<not> SY30 (bnd_s (bnd_s (bnd_sK4 SY30)))
(bnd_sK5 SY30) \<or>
\<not> SY30 (bnd_s (bnd_sK4 SY30))
(bnd_s (bnd_sK5 SY30))) \<or>
\<not> SY30 bnd_c1 bnd_c1) \<or>
SY30 bnd_sK1 bnd_sK2) =
True"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
*)
typedecl GEG007_1_bnd_reg
consts
GEG007_1_bnd_sK7_SX2 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ GEG007_1_bnd_reg"
GEG007_1_bnd_sK6_SX2 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ GEG007_1_bnd_reg"
GEG007_1_bnd_a :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
GEG007_1_bnd_catalunya :: "GEG007_1_bnd_reg"
GEG007_1_bnd_spain :: "GEG007_1_bnd_reg"
GEG007_1_bnd_c :: "GEG007_1_bnd_reg \ GEG007_1_bnd_reg \ bool"
(* (Annotated_step ("147", "extcnf_forall_neg"), *)
lemma "\SV13 SV6.
(\<forall>SX2. \<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya) =
False \<or>
GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
\<forall>SV6 SV13.
(\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_spain \<or>
GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) =
False \<or>
GEG007_1_bnd_a SV6 SV13 = False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
(* (Annotated_step ("116", "extcnf_forall_neg"), *)
lemma "\SV13 SV6.
(\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya \<or>
\<not> \<not> \<not> (\<forall>SX3.
\<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
\<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
\<not> \<not> \<not> (\<forall>SX3.
\<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
False \<or>
GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
\<forall>SV6 SV13.
(\<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
GEG007_1_bnd_catalunya \<or>
\<not> \<not> \<not> (\<forall>SY68.
\<not> \<not> (\<not> (\<forall>SY69.
\<not> GEG007_1_bnd_c SY69 SY68 \<or>
GEG007_1_bnd_c SY69 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY68 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
\<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
GEG007_1_bnd_spain \<or>
\<not> \<not> \<not> (\<forall>SY71.
\<not> \<not> (\<not> (\<forall>SY72.
\<not> GEG007_1_bnd_c SY72 SY71 \<or>
GEG007_1_bnd_c SY72 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY71 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
False \<or>
GEG007_1_bnd_a SV6 SV13 = False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
consts PUZ107_5_bnd_sK1_SX0 ::
"TPTP_Interpret.ind
\<Rightarrow> TPTP_Interpret.ind
\<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
lemma "\(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
(SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
(SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
(SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
(SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
((SV1 = SV3) = True \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Not_neg]\<close>)
lemma "
\<forall>(SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind)
(SV4::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
(SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
((SV1 \<noteq> SV3 \<or> SV2 \<noteq> SV4) = False \<or>
PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
(SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
(SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Or_neg]\<close>)
consts
NUM016_5_bnd_a :: TPTP_Interpret.ind
NUM016_5_bnd_prime :: "TPTP_Interpret.ind \ bool"
NUM016_5_bnd_factorial_plus_one :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
NUM016_5_bnd_prime_divisor :: "TPTP_Interpret.ind \ TPTP_Interpret.ind"
NUM016_5_bnd_divides :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
NUM016_5_bnd_less :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
(* (Annotated_step ("6", "unfold_def"), *)
lemma "((((((((((((\X::TPTP_Interpret.ind. \ NUM016_5_bnd_less X X) \
(\<forall>(X::TPTP_Interpret.ind)
Y::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_less X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
(\<forall>X::TPTP_Interpret.ind. NUM016_5_bnd_divides X X)) \<and>
(\<forall>(X::TPTP_Interpret.ind)
(Y::TPTP_Interpret.ind)
Z::TPTP_Interpret.ind.
(\<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_divides Y Z) \<or>
NUM016_5_bnd_divides X Z)) \<and>
(\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
(\<forall>X::TPTP_Interpret.ind.
NUM016_5_bnd_less X (NUM016_5_bnd_factorial_plus_one X))) \<and>
(\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_divides X (NUM016_5_bnd_factorial_plus_one Y) \<or>
NUM016_5_bnd_less Y X)) \<and>
(\<forall>X::TPTP_Interpret.ind.
NUM016_5_bnd_prime X \<or>
NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor X) X)) \<and>
(\<forall>X::TPTP_Interpret.ind.
NUM016_5_bnd_prime X \<or>
NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor X))) \<and>
(\<forall>X::TPTP_Interpret.ind.
NUM016_5_bnd_prime X \<or>
NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor X) X)) \<and>
NUM016_5_bnd_prime NUM016_5_bnd_a) \<and>
(\<forall>X::TPTP_Interpret.ind.
(\<not> NUM016_5_bnd_prime X \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a X) \<or>
NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) X)) =
True \<Longrightarrow>
(\<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> (\<forall>SX0::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_less SX0 SX0) \<or>
\<not> (\<forall>(SX0::TPTP_Interpret.ind)
SX1::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_less SX0 SX1 \<or> \<not> NUM016_5_bnd_less SX1 SX0)) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
NUM016_5_bnd_divides SX0 SX0)) \<or>
\<not> (\<forall>(SX0::TPTP_Interpret.ind)
(SX1::TPTP_Interpret.ind)
SX2::TPTP_Interpret.ind.
(\<not> NUM016_5_bnd_divides SX0 SX1 \<or>
\<not> NUM016_5_bnd_divides SX1 SX2) \<or>
NUM016_5_bnd_divides SX0 SX2)) \<or>
\<not> (\<forall>(SX0::TPTP_Interpret.ind)
SX1::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_divides SX0 SX1 \<or>
\<not> NUM016_5_bnd_less SX1 SX0)) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
NUM016_5_bnd_less SX0 (NUM016_5_bnd_factorial_plus_one SX0))) \<or>
\<not> (\<forall>(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind.
\<not> NUM016_5_bnd_divides SX0 (NUM016_5_bnd_factorial_plus_one SX1) \<or>
NUM016_5_bnd_less SX1 SX0)) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
NUM016_5_bnd_prime SX0 \<or>
NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor SX0) SX0)) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
NUM016_5_bnd_prime SX0 \<or> NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor SX0))) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
NUM016_5_bnd_prime SX0 \<or>
NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor SX0)
SX0)) \<or>
\<not> NUM016_5_bnd_prime NUM016_5_bnd_a) \<or>
\<not> (\<forall>SX0::TPTP_Interpret.ind.
(\<not> NUM016_5_bnd_prime SX0 \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a SX0) \<or>
NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a)
SX0))) =
True"
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(* (Annotated_step ("3", "unfold_def"), *)
lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) &
(ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
(ALL X. bnd_divides X X)) &
(ALL X Y Z.
(~ bnd_divides X Y | ~ bnd_divides Y Z) |
bnd_divides X Z)) &
(ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
(ALL X. bnd_less X (bnd_factorial_plus_one X))) &
(ALL X Y.
~ bnd_divides X (bnd_factorial_plus_one Y) |
bnd_less Y X)) &
(ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) &
(ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
(ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
bnd_prime bnd_a) &
(ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
bnd_less (bnd_factorial_plus_one bnd_a) X))) =
False
==> (~ ((((((((((((ALL X. ~ bnd_less X X) &
(ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
(ALL X. bnd_divides X X)) &
(ALL X Y Z.
(~ bnd_divides X Y | ~ bnd_divides Y Z) |
bnd_divides X Z)) &
(ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
(ALL X. bnd_less X (bnd_factorial_plus_one X))) &
(ALL X Y.
~ bnd_divides X (bnd_factorial_plus_one Y) |
bnd_less Y X)) &
(ALL X. bnd_prime X |
bnd_divides (bnd_prime_divisor X) X)) &
(ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
(ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
bnd_prime bnd_a) &
(ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
bnd_less (bnd_factorial_plus_one bnd_a) X))) =
False"
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(* SET062^6.p.out
[[(Annotated_step ("3", "unfold_def"), *)
lemma "(\Z3. False \ bnd_cA Z3) = False \
(\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False"
by (tactic \<open>unfold_def_tac @{context} []\<close>)
(*
(* SEU559^2.p.out *)
(* [[(Annotated_step ("3", "unfold_def"), *)
lemma "bnd_subset = (\A B. \Xx. bnd_in Xx A \ bnd_in Xx B) \
(\<forall>A B. (\<forall>Xx. bnd_in Xx A \<longrightarrow> bnd_in Xx B) \<longrightarrow>
bnd_subset A B) =
False \<Longrightarrow>
(\<forall>SY0 SY1.
(\<forall>Xx. bnd_in Xx SY0 \<longrightarrow> bnd_in Xx SY1) \<longrightarrow>
(\<forall>SY5. bnd_in SY5 SY0 \<longrightarrow> bnd_in SY5 SY1)) =
False"
by (tactic {*unfold_def_tac [@{thm bnd_subset_def}]*})
(* SEU559^2.p.out
[[(Annotated_step ("6", "unfold_def"), *)
lemma "(\ (\Xx. \Xy. Xx \ Xy)) = True \
(\<not> \<not> (\<forall>SX0. \<not> (\<forall>SX1. \<not> SX0 \<or> SX1))) = True"
by (tactic {*unfold_def_tac []*})
(* SEU502^2.p.out
[[(Annotated_step ("3", "unfold_def"), *)
lemma "bnd_emptysetE =
(\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<and>
(bnd_emptysetE \<longrightarrow>
(\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
False \<Longrightarrow>
((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
(\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
False"
by (tactic {*unfold_def_tac [@{thm bnd_emptysetE_def}]*})
*)
typedecl AGT037_2_bnd_mu
consts
AGT037_2_bnd_sK1_SX0 :: TPTP_Interpret.ind
AGT037_2_bnd_cola :: AGT037_2_bnd_mu
AGT037_2_bnd_jan :: AGT037_2_bnd_mu
AGT037_2_bnd_possibly_likes :: "AGT037_2_bnd_mu \ AGT037_2_bnd_mu \ TPTP_Interpret.ind \ bool"
AGT037_2_bnd_sK5_SY68 ::
"TPTP_Interpret.ind
\<Rightarrow> AGT037_2_bnd_mu
\<Rightarrow> AGT037_2_bnd_mu
\<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
AGT037_2_bnd_likes :: "AGT037_2_bnd_mu \ AGT037_2_bnd_mu \ TPTP_Interpret.ind \ bool"
AGT037_2_bnd_very_much_likes :: "AGT037_2_bnd_mu \ AGT037_2_bnd_mu \ TPTP_Interpret.ind \ bool"
AGT037_2_bnd_a1 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
AGT037_2_bnd_a2 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
AGT037_2_bnd_a3 :: "TPTP_Interpret.ind \ TPTP_Interpret.ind \ bool"
(*test that nullary skolem terms are OK*)
(* (Annotated_step ("79", "extcnf_forall_neg"), *)
lemma "(\SX0::TPTP_Interpret.ind.
AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola SX0) =
False \<Longrightarrow>
AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_SX0 =
False"
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
(* (Annotated_step ("202", "extcnf_forall_neg"), *)
lemma "\(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu)
SV45::TPTP_Interpret.ind.
((((\<forall>SY68::TPTP_Interpret.ind.
\<not> AGT037_2_bnd_a1 SV45 SY68 \<or>
AGT037_2_bnd_likes SV29 SV39 SY68) =
False \<or>
(\<not> (\<forall>SY69::TPTP_Interpret.ind.
\<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
AGT037_2_bnd_likes SV29 SV39 SY69)) =
True) \<or>
AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
AGT037_2_bnd_a3 SV13 SV45 = False \<Longrightarrow>
\<forall>(SV29::AGT037_2_bnd_mu) (SV39::AGT037_2_bnd_mu) (SV13::TPTP_Interpret.ind)
SV45::TPTP_Interpret.ind.
((((\<not> AGT037_2_bnd_a1 SV45
(AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45) \<or>
AGT037_2_bnd_likes SV29 SV39
(AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45)) =
False \<or>
(\<not> (\<forall>SY69::TPTP_Interpret.ind.
\<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
AGT037_2_bnd_likes SV29 SV39 SY69)) =
True) \<or>
AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
AGT037_2_bnd_a3 SV13 SV45 = False"
(*
apply (rule allI)+
apply (erule_tac x = "SV13" in allE)
apply (erule_tac x = "SV39" in allE)
apply (erule_tac x = "SV29" in allE)
apply (erule_tac x = "SV45" in allE)
apply (erule disjE)+
defer
apply (tactic {*clause_breaker 1*})+
apply (drule_tac sk = "bnd_sK5_SY68 SV13 SV39 SV29 SV45" in leo2_skolemise)
defer
apply (tactic {*clause_breaker 1*})
apply (tactic {*nonfull_extcnf_combined_tac []*})
*)
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
(*(*NUM667^1*)
lemma "\SV12 SV13 SV14 SV9 SV10 SV11.
((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
(SV14 = SV13) = False) \<or>
bnd_less SV12 SV14 = False) \<or>
bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) = False \<Longrightarrow>
\<forall>SV9 SV14 SV10 SV11 SV13 SV12.
((((bnd_less SV12 SV13 = False \<or>
bnd_less SV11 SV10 = False) \<or>
(SV14 = SV13) = False) \<or>
bnd_less SV12 SV14 = False) \<or>
bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) = False"
(*
apply (tactic {*
extcnf_combined_tac NONE
[ConstsDiff,
StripQuantifiers]
[]*})
*)
(*
apply (rule allI)+
apply (erule_tac x = "SV12" in allE)
apply (erule_tac x = "SV13" in allE)
apply (erule_tac x = "SV14" in allE)
apply (erule_tac x = "SV9" in allE)
apply (erule_tac x = "SV10" in allE)
apply (erule_tac x = "SV11" in allE)
*)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "300") 1*})
(*NUM667^1 node 302 -- dec*)
lemma "\SV12 SV13 SV14 SV9 SV10 SV11.
((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
(SV14 = SV13) = False) \<or>
bnd_less SV12 SV14 = False) \<or>
bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) =
False \<Longrightarrow>
\<forall>SV9 SV14 SV10 SV13 SV11 SV12.
(((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
(SV14 = SV13) = False) \<or>
bnd_less SV12 SV14 = False) \<or>
bnd_less SV9 SV10 = True) \<or>
(SV9 = SV11) =
False"
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "302") 1*})
*)
(*
(*CSR122^2*)
(* (Annotated_step ("23", "extuni_bool2"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i) =
False \<Longrightarrow>
bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
True \<or>
bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i =
True"
(* apply (erule extuni_bool2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "23") 1*})
(* (Annotated_step ("24", "extuni_bool1"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i) =
False \<Longrightarrow>
bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
False \<or>
bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i =
False"
(* apply (erule extuni_bool1) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "24") 1*})
(* (Annotated_step ("25", "extuni_bool2"), *)
lemma "(bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i) =
False \<Longrightarrow>
bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
True \<or>
bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i =
True"
(* apply (erule extuni_bool2) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "25") 1*})
(* (Annotated_step ("26", "extuni_bool1"), *)
lemma "\SV2. (bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI
bnd_lMary_THFTYPE_i
bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI
bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
False \<Longrightarrow>
\<forall>SV2. bnd_holdsDuring_THFTYPE_IiooI
(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
(\<not> (\<not> bnd_likes_THFTYPE_IiioI
bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
\<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
bnd_lBill_THFTYPE_i)) =
False \<or>
bnd_holdsDuring_THFTYPE_IiooI SV2 True = False"
(* apply (rule allI, erule allE) *)
(* apply (erule extuni_bool1) *)
(* done *)
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "26") 1*})
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.74 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
