src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
wenzelm@59720
     1
(*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
sultana@55596
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@55596
     3
sultana@55596
     4
Unit tests for proof reconstruction module.
sultana@55596
     5
*)
sultana@55596
     6
wenzelm@60649
     7
theory TPTP_Proof_Reconstruction_Test_Units
sultana@55596
     8
imports TPTP_Test TPTP_Proof_Reconstruction
sultana@55596
     9
begin
sultana@55596
    10
wenzelm@56281
    11
declare [[ML_exception_trace, ML_print_depth = 200]]
sultana@55596
    12
wenzelm@60926
    13
declare [[tptp_trace_reconstruction = true]]
sultana@55596
    14
sultana@55596
    15
lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
wenzelm@63167
    16
apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
sultana@55596
    17
oops
sultana@55596
    18
sultana@55596
    19
lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
wenzelm@63167
    20
apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
sultana@55596
    21
apply (rule allI)+
wenzelm@63167
    22
apply (tactic \<open>nominal_inst_parametermatch_tac @{context} @{thm allE} 1\<close>)+
sultana@55596
    23
oops
sultana@55596
    24
sultana@55596
    25
(*Could test bind_tac further with NUM667^1 inode43*)
sultana@55596
    26
sultana@55596
    27
(*
sultana@55596
    28
  (* SEU581^2.p_nux *)
sultana@55596
    29
     (* (Annotated_step ("inode1", "bind"), *)
wenzelm@61076
    30
lemma "\<forall>(SV5::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
    31
            SV6::TPTP_Interpret.ind.
sultana@55596
    32
            (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    33
              (bnd_powerset bnd_sK1_A) =
sultana@55596
    34
             bnd_in (bnd_dsetconstr SV6 SV5)
sultana@55596
    35
              (bnd_powerset SV6)) =
sultana@55596
    36
            False \<Longrightarrow>
sultana@55596
    37
         (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    38
           (bnd_powerset bnd_sK1_A) =
sultana@55596
    39
          bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    40
           (bnd_powerset bnd_sK1_A)) =
sultana@55596
    41
         False"
sultana@55596
    42
ML_prf {*
sultana@55596
    43
open TPTP_Syntax;
sultana@55596
    44
open TPTP_Proof;
sultana@55596
    45
sultana@55596
    46
sultana@55596
    47
val binds =
sultana@55596
    48
[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"))])))]
sultana@55596
    49
(* |> TPTP_Reconstruct.permute *)
sultana@55596
    50
sultana@55596
    51
(*
sultana@55596
    52
val binds =
sultana@55596
    53
[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"))]))),
sultana@55596
    54
Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))
sultana@55596
    55
]
sultana@55596
    56
*)
sultana@55596
    57
sultana@55596
    58
val tec =
sultana@55596
    59
(*
sultana@55596
    60
  map (bind_tac @{context} (hd prob_names)) binds
sultana@55596
    61
  |> FIRST
sultana@55596
    62
*)
sultana@55596
    63
  bind_tac @{context} (hd prob_names) binds
sultana@55596
    64
*}
sultana@55596
    65
apply (tactic {*tec*})
sultana@55596
    66
done
sultana@55596
    67
sultana@55596
    68
     (* (Annotated_step ("inode2", "bind"), *)
wenzelm@61076
    69
lemma "\<forall>(SV7::TPTP_Interpret.ind) SV8::TPTP_Interpret.ind.
sultana@55596
    70
            (bnd_subset SV8 SV7 =
sultana@55596
    71
             bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    72
              bnd_sK1_A) =
sultana@55596
    73
            False \<or>
sultana@55596
    74
            bnd_in SV8 (bnd_powerset SV7) = False \<Longrightarrow>
sultana@55596
    75
         (bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    76
           bnd_sK1_A =
sultana@55596
    77
          bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    78
           bnd_sK1_A) =
sultana@55596
    79
         False \<or>
sultana@55596
    80
         bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
sultana@55596
    81
          (bnd_powerset bnd_sK1_A) =
sultana@55596
    82
         False"
sultana@55596
    83
ML_prf {*
sultana@55596
    84
open TPTP_Syntax;
sultana@55596
    85
open TPTP_Proof;
sultana@55596
    86
sultana@55596
    87
sultana@55596
    88
val binds =
sultana@55596
    89
[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", []))))]
sultana@55596
    90
(* |> TPTP_Reconstruct.permute *)
sultana@55596
    91
sultana@55596
    92
val tec =
sultana@55596
    93
(*
sultana@55596
    94
  map (bind_tac @{context} (hd prob_names)) binds
sultana@55596
    95
  |> FIRST
sultana@55596
    96
*)
sultana@55596
    97
  bind_tac @{context} (hd prob_names) binds
sultana@55596
    98
*}
sultana@55596
    99
apply (tactic {*tec*})
sultana@55596
   100
done
sultana@55596
   101
*)
sultana@55596
   102
sultana@55596
   103
(*
sultana@55596
   104
from SEU897^5
sultana@55596
   105
lemma "
sultana@55596
   106
\<forall>SV9 SV10 SV11 SV12 SV13 SV14.
sultana@55596
   107
   (((((bnd_sK5_SY14 SV14 SV13 SV12 = SV11) = False \<or>
sultana@55596
   108
       (bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 SV11)) =
sultana@55596
   109
       False) \<or>
sultana@55596
   110
      bnd_cR SV14 = False) \<or>
sultana@55596
   111
     (SV12 = SV13 SV14) = False) \<or>
sultana@55596
   112
    bnd_cR SV9 = False) \<or>
sultana@55596
   113
   (SV11 = SV10 SV9) = False \<Longrightarrow>
sultana@55596
   114
\<forall>SV14 SV13 SV12 SV10 SV9.
sultana@55596
   115
   (((((bnd_sK5_SY14 SV14 SV13 SV12 =
sultana@55596
   116
        bnd_sK5_SY14 SV14 SV13 SV12) =
sultana@55596
   117
       False \<or>
sultana@55596
   118
       (bnd_sK4_SX0 =
sultana@55596
   119
        SV10
sultana@55596
   120
         (bnd_sK5_SY14 SV9 SV10
sultana@55596
   121
           (bnd_sK5_SY14 SV14 SV13 SV12))) =
sultana@55596
   122
       False) \<or>
sultana@55596
   123
      bnd_cR SV14 = False) \<or>
sultana@55596
   124
     (SV12 = SV13 SV14) = False) \<or>
sultana@55596
   125
    bnd_cR SV9 = False) \<or>
sultana@55596
   126
   (bnd_sK5_SY14 SV14 SV13 SV12 = SV10 SV9) = False"
sultana@55596
   127
ML_prf {*
sultana@55596
   128
open TPTP_Syntax;
sultana@55596
   129
open TPTP_Proof;
sultana@55596
   130
sultana@55596
   131
val binds =
sultana@55596
   132
[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"))]))]
sultana@55596
   133
sultana@55596
   134
val tec = bind_tac @{context} (hd prob_names) binds
sultana@55596
   135
*}
sultana@55596
   136
apply (tactic {*tec*})
sultana@55596
   137
done
sultana@55596
   138
*)
sultana@55596
   139
sultana@55596
   140
sultana@55596
   141
subsection "Interpreting the inferences"
sultana@55596
   142
sultana@55596
   143
(*from SET598^5
sultana@55596
   144
lemma "(bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
sultana@55596
   145
   ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
sultana@55596
   146
    (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
sultana@55596
   147
   (\<forall>SY27.
sultana@55596
   148
       (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
sultana@55596
   149
       (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
sultana@55596
   150
       (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30))) =
sultana@55596
   151
  False \<Longrightarrow>
sultana@55596
   152
  (\<not> (bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
sultana@55596
   153
      ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
sultana@55596
   154
       (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
sultana@55596
   155
      (\<forall>SY27.
sultana@55596
   156
          (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
sultana@55596
   157
          (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
sultana@55596
   158
          (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)))) =
sultana@55596
   159
  True"
sultana@55596
   160
apply (tactic {*polarity_switch_tac @{context}*})
sultana@55596
   161
done
sultana@55596
   162
lemma "
sultana@55596
   163
  (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
sultana@55596
   164
    (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
sultana@55596
   165
   (\<forall>SY27.
sultana@55596
   166
       (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
sultana@55596
   167
       (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
sultana@55596
   168
       (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
sultana@55596
   169
   bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17)) =
sultana@55596
   170
  False \<Longrightarrow>
sultana@55596
   171
  (\<not> (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
sultana@55596
   172
       (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
sultana@55596
   173
      (\<forall>SY27.
sultana@55596
   174
          (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
sultana@55596
   175
          (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
sultana@55596
   176
          (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
sultana@55596
   177
      bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17))) =
sultana@55596
   178
  True"
sultana@55596
   179
apply (tactic {*polarity_switch_tac @{context}*})
sultana@55596
   180
done
sultana@55596
   181
*)
sultana@55596
   182
sultana@55596
   183
(* beware lack of type annotations
sultana@55596
   184
(* lemma "!!x. (A x = B x) = False ==> (B x = A x) = False" *)
sultana@55596
   185
(* lemma "!!x. (A x = B x) = True ==> (B x = A x) = True" *)
sultana@55596
   186
(* lemma "((A x) = (B x)) = True ==> ((B x) = (A x)) = True" *)
sultana@55596
   187
lemma "(A = B) = True ==> (B = A) = True"
sultana@55596
   188
*)
sultana@55596
   189
lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False"
wenzelm@63167
   190
apply (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   191
oops
sultana@55596
   192
sultana@55596
   193
lemma "(A & B) ==> ~(~A | ~B)"
wenzelm@63167
   194
by (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   195
sultana@55596
   196
lemma "(A | B) ==> ~(~A & ~B)"
wenzelm@63167
   197
by (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   198
sultana@55596
   199
lemma "(A | B) | C ==> A | (B | C)"
wenzelm@63167
   200
by (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   201
sultana@55596
   202
lemma "(~~A) = B ==> A = B"
wenzelm@63167
   203
by (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   204
sultana@55596
   205
lemma "~ ~ (A = True) ==> A = True"
wenzelm@63167
   206
by (tactic \<open>expander_animal @{context} 1\<close>)
sultana@55596
   207
sultana@55596
   208
(*This might not be a goal which might realistically arise:
sultana@55596
   209
lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *)
sultana@55596
   210
lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))"
wenzelm@63167
   211
apply (tactic \<open>expander_animal @{context} 1\<close>)+
sultana@55596
   212
apply (rule conjI)
sultana@55596
   213
apply assumption
sultana@55596
   214
apply (rule sym, assumption)
sultana@55596
   215
done
sultana@55596
   216
sultana@55596
   217
lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))"
wenzelm@63167
   218
by (tactic \<open>expander_animal @{context} 1\<close>)+
sultana@55596
   219
sultana@55596
   220
(*some lemmas assume constants in the signature of PUZ114^5*)
sultana@55596
   221
consts
sultana@55596
   222
  PUZ114_5_bnd_sK1 :: "TPTP_Interpret.ind"
sultana@55596
   223
  PUZ114_5_bnd_sK2 :: "TPTP_Interpret.ind"
sultana@55596
   224
  PUZ114_5_bnd_sK3 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   225
  PUZ114_5_bnd_sK4 :: "(TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   226
  PUZ114_5_bnd_sK5 :: "(TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   227
  PUZ114_5_bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   228
  PUZ114_5_bnd_c1 :: TPTP_Interpret.ind
sultana@55596
   229
sultana@55596
   230
(*testing logical expansion*)
sultana@55596
   231
lemma "!! SY30. (SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1 \<and>
sultana@55596
   232
       (\<forall>Xj Xk.
sultana@55596
   233
           SY30 Xj Xk \<longrightarrow>
sultana@55596
   234
           SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
sultana@55596
   235
           SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)) \<longrightarrow>
sultana@55596
   236
       SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2)
sultana@55596
   237
==> (
sultana@55596
   238
       (~ SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1)
sultana@55596
   239
     | (~ (\<forall>Xj Xk.
sultana@55596
   240
           SY30 Xj Xk \<longrightarrow>
sultana@55596
   241
           SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
sultana@55596
   242
           SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)))
sultana@55596
   243
     | SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2
sultana@55596
   244
)"
wenzelm@63167
   245
by (tactic \<open>expander_animal @{context} 1\<close>)+
sultana@55596
   246
sultana@55596
   247
(*
sultana@55596
   248
extcnf_forall_pos:
sultana@55596
   249
sultana@55596
   250
     (! X. L1) | ... | Ln
sultana@55596
   251
 ----------------------------   X' fresh
sultana@55596
   252
  ! X'. (L1[X'/X] | ... | Ln)
sultana@55596
   253
sultana@55596
   254
After elimination rule has been applied we'll have a subgoal which looks like this:
sultana@55596
   255
            (! X. L1)
sultana@55596
   256
 ----------------------------   X' fresh
sultana@55596
   257
  ! X'. (L1[X'/X] | ... | Ln)
sultana@55596
   258
and we need to transform it so that, in Isabelle, we go from
sultana@55596
   259
 (! X. L1) ==> ! X'. (L1[X'/X] | ... | Ln)
sultana@55596
   260
to
sultana@55596
   261
 \<And> X'. L1[X'/X] ==> (L1[X'/X] | ... | Ln)
sultana@55596
   262
(where X' is fresh, or renamings are done suitably).*)
sultana@55596
   263
sultana@55596
   264
lemma "A | B \<Longrightarrow> A | B | C"
wenzelm@63167
   265
apply (tactic \<open>flip_conclusion_tac @{context} 1\<close>)+
wenzelm@63167
   266
apply (tactic \<open>break_hypotheses 1\<close>)+
sultana@55596
   267
oops
sultana@55596
   268
sultana@55596
   269
consts
sultana@55596
   270
  CSR122_1_bnd_lBill_THFTYPE_i :: TPTP_Interpret.ind
sultana@55596
   271
  CSR122_1_bnd_lMary_THFTYPE_i :: TPTP_Interpret.ind
sultana@55596
   272
  CSR122_1_bnd_lSue_THFTYPE_i :: TPTP_Interpret.ind
sultana@55596
   273
  CSR122_1_bnd_n2009_THFTYPE_i :: TPTP_Interpret.ind
sultana@55596
   274
  CSR122_1_bnd_lYearFn_THFTYPE_IiiI :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   275
  CSR122_1_bnd_holdsDuring_THFTYPE_IiooI ::
sultana@55596
   276
    "TPTP_Interpret.ind \<Rightarrow> bool \<Rightarrow> bool"
sultana@55596
   277
  CSR122_1_bnd_likes_THFTYPE_IiioI ::
sultana@55596
   278
    "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   279
sultana@55596
   280
lemma "\<forall>SV2. (CSR122_1_bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
   281
                 (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i)
sultana@55596
   282
                 (\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
sultana@55596
   283
                        CSR122_1_bnd_lMary_THFTYPE_i
sultana@55596
   284
                        CSR122_1_bnd_lBill_THFTYPE_i \<or>
sultana@55596
   285
                     \<not> CSR122_1_bnd_likes_THFTYPE_IiioI
sultana@55596
   286
                        CSR122_1_bnd_lSue_THFTYPE_i
sultana@55596
   287
                        CSR122_1_bnd_lBill_THFTYPE_i)) =
sultana@55596
   288
                CSR122_1_bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
sultana@55596
   289
               False \<Longrightarrow>
sultana@55596
   290
         \<forall>SV2. (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i =
sultana@55596
   291
                SV2) =
sultana@55596
   292
               False \<or>
sultana@55596
   293
               ((\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
sultana@55596
   294
                       CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i \<or>
sultana@55596
   295
                    \<not> CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i
sultana@55596
   296
                       CSR122_1_bnd_lBill_THFTYPE_i)) =
sultana@55596
   297
                True) =
sultana@55596
   298
               False"
sultana@55596
   299
apply (rule allI, erule_tac x = "SV2" in allE)
wenzelm@63167
   300
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
sultana@55596
   301
done
sultana@55596
   302
sultana@55596
   303
(*SEU882^5*)
sultana@55596
   304
(*
sultana@55596
   305
lemma
wenzelm@61076
   306
 "\<forall>(SV2::TPTP_Interpret.ind)
wenzelm@61076
   307
        SV1::TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind.
sultana@55596
   308
        (SV1 SV2 = bnd_sK1_Xy) =
sultana@55596
   309
        False
sultana@55596
   310
   \<Longrightarrow>
wenzelm@61076
   311
   \<forall>SV2::TPTP_Interpret.ind.
sultana@55596
   312
            (bnd_sK1_Xy = bnd_sK1_Xy) =
sultana@55596
   313
            False"
sultana@55596
   314
ML_prf {*
sultana@55596
   315
open TPTP_Syntax;
sultana@55596
   316
open TPTP_Proof;
sultana@55596
   317
sultana@55596
   318
val binds =
sultana@55596
   319
[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", [])))))]
sultana@55596
   320
sultana@55596
   321
val tec = bind_tac @{context} (hd prob_names) binds
sultana@55596
   322
*}
sultana@55596
   323
(*
sultana@55596
   324
apply (tactic {*strip_qtfrs
sultana@55596
   325
                (* THEN tec *)*})
sultana@55596
   326
*)
sultana@55596
   327
apply (tactic {*tec*})
sultana@55596
   328
done
sultana@55596
   329
*)
sultana@55596
   330
sultana@55596
   331
lemma "A | B \<Longrightarrow> C1 | A | C2 | B | C3"
sultana@55596
   332
apply (erule disjE)
wenzelm@63167
   333
apply (tactic \<open>clause_breaker 1\<close>)
wenzelm@63167
   334
apply (tactic \<open>clause_breaker 1\<close>)
sultana@55596
   335
done
sultana@55596
   336
sultana@55596
   337
lemma "A \<Longrightarrow> A"
wenzelm@63167
   338
apply (tactic \<open>clause_breaker 1\<close>)
sultana@55596
   339
done
sultana@55596
   340
sultana@55596
   341
typedecl NUM667_1_bnd_nat
sultana@55596
   342
consts
sultana@55596
   343
  NUM667_1_bnd_less :: "NUM667_1_bnd_nat \<Rightarrow> NUM667_1_bnd_nat \<Rightarrow> bool"
sultana@55596
   344
  NUM667_1_bnd_x :: NUM667_1_bnd_nat
sultana@55596
   345
  NUM667_1_bnd_y :: NUM667_1_bnd_nat
sultana@55596
   346
sultana@55596
   347
(*NUM667^1 node 302 -- dec*)
sultana@55596
   348
lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
sultana@55596
   349
       ((((NUM667_1_bnd_less SV12 SV13 = NUM667_1_bnd_less SV11 SV10) = False \<or>
sultana@55596
   350
          (SV14 = SV13) = False) \<or>
sultana@55596
   351
         NUM667_1_bnd_less SV12 SV14 = False) \<or>
sultana@55596
   352
        NUM667_1_bnd_less SV9 SV10 = True) \<or>
sultana@55596
   353
       (SV9 = SV11) =
sultana@55596
   354
       False \<Longrightarrow>
sultana@55596
   355
       \<forall>SV9 SV14 SV10 SV13 SV11 SV12.
sultana@55596
   356
       (((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
sultana@55596
   357
          (SV14 = SV13) = False) \<or>
sultana@55596
   358
         NUM667_1_bnd_less SV12 SV14 = False) \<or>
sultana@55596
   359
        NUM667_1_bnd_less SV9 SV10 = True) \<or>
sultana@55596
   360
       (SV9 = SV11) =
sultana@55596
   361
       False"
wenzelm@63167
   362
apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
wenzelm@63167
   363
apply (tactic \<open>break_hypotheses 1\<close>)
wenzelm@63167
   364
apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
wenzelm@63167
   365
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
sultana@55596
   366
done
sultana@55596
   367
wenzelm@63167
   368
ML \<open>
sultana@55596
   369
extuni_dec_n @{context} 2;
wenzelm@63167
   370
\<close>
sultana@55596
   371
sultana@55596
   372
(*NUM667^1, node 202*)
sultana@55596
   373
lemma "\<forall>SV9 SV10 SV11.
sultana@55596
   374
       ((((SV9 = SV11) = (NUM667_1_bnd_x = NUM667_1_bnd_y)) = False \<or>
sultana@55596
   375
         NUM667_1_bnd_less SV11 SV10 = False) \<or>
sultana@55596
   376
        NUM667_1_bnd_less SV9 SV10 = True) \<or>
sultana@55596
   377
       NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
sultana@55596
   378
       True \<Longrightarrow>
sultana@55596
   379
       \<forall>SV10 SV9 SV11.
sultana@55596
   380
       ((((SV11 = NUM667_1_bnd_x) = False \<or> (SV9 = NUM667_1_bnd_y) = False) \<or>
sultana@55596
   381
         NUM667_1_bnd_less SV11 SV10 = False) \<or>
sultana@55596
   382
        NUM667_1_bnd_less SV9 SV10 = True) \<or>
sultana@55596
   383
       NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
sultana@55596
   384
       True"
wenzelm@63167
   385
apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
wenzelm@63167
   386
apply (tactic \<open>break_hypotheses 1\<close>)
wenzelm@63167
   387
apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
wenzelm@63167
   388
apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
sultana@55596
   389
done
sultana@55596
   390
sultana@55596
   391
(*NUM667^1 node 141*)
sultana@55596
   392
(*
sultana@55596
   393
lemma "((bnd_x = bnd_x) = False \<or> (bnd_y = bnd_z) = False) \<or>
sultana@55596
   394
         bnd_less bnd_x bnd_y = True \<Longrightarrow>
sultana@55596
   395
         (bnd_y = bnd_z) = False \<or> bnd_less bnd_x bnd_y = True"
sultana@55596
   396
apply (tactic {*strip_qtfrs*})
sultana@55596
   397
apply (tactic {*break_hypotheses 1*})
sultana@55596
   398
apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
sultana@55596
   399
apply (erule extuni_triv)
sultana@55596
   400
done
sultana@55596
   401
*)
sultana@55596
   402
wenzelm@63167
   403
ML \<open>
sultana@55596
   404
fun full_extcnf_combined_tac ctxt =
sultana@55596
   405
  extcnf_combined_tac ctxt NONE
sultana@55596
   406
   [ConstsDiff,
sultana@55596
   407
    StripQuantifiers,
sultana@55596
   408
    Flip_Conclusion,
sultana@55596
   409
    Loop [
sultana@55596
   410
     Close_Branch,
sultana@55596
   411
     ConjI,
sultana@55596
   412
     King_Cong,
sultana@55596
   413
     Break_Hypotheses,
sultana@55596
   414
     Existential_Free,
sultana@55596
   415
     Existential_Var,
sultana@55596
   416
     Universal,
sultana@55596
   417
     RemoveRedundantQuantifications],
sultana@55596
   418
    CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates],
sultana@55596
   419
    AbsorbSkolemDefs]
sultana@55596
   420
   []
wenzelm@63167
   421
\<close>
sultana@55596
   422
wenzelm@63167
   423
ML \<open>
sultana@55596
   424
fun nonfull_extcnf_combined_tac ctxt feats =
sultana@55596
   425
  extcnf_combined_tac ctxt NONE
sultana@55596
   426
   [ConstsDiff,
sultana@55596
   427
    StripQuantifiers,
sultana@55596
   428
    InnerLoopOnce (Break_Hypotheses :: feats),
sultana@55596
   429
    AbsorbSkolemDefs]
sultana@55596
   430
   []
wenzelm@63167
   431
\<close>
sultana@55596
   432
sultana@55596
   433
consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind
sultana@55596
   434
lemma
sultana@55596
   435
  "\<forall>SV2. (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False \<Longrightarrow>
sultana@55596
   436
   (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False"
sultana@55596
   437
(* apply (erule_tac x = "(@X. False)" in allE) *)
sultana@55596
   438
(* apply (tactic {*remove_redundant_quantification 1*}) *)
sultana@55596
   439
(* apply assumption *)
wenzelm@63167
   440
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]\<close>)
sultana@55596
   441
sultana@55596
   442
(*NUM667^1*)
sultana@55596
   443
(*
sultana@55596
   444
     (* (Annotated_step ("153", "extuni_triv"), *)
sultana@55596
   445
lemma "((bnd_y = bnd_x) = False \<or> (bnd_z = bnd_z) = False) \<or>
sultana@55596
   446
         (bnd_y = bnd_z) = True \<Longrightarrow>
sultana@55596
   447
         (bnd_y = bnd_x) = False \<or> (bnd_y = bnd_z) = True"
sultana@55596
   448
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
sultana@55596
   449
done
sultana@55596
   450
     (* (Annotated_step ("162", "extuni_triv"), *)
sultana@55596
   451
lemma "((bnd_y = bnd_x) = False \<or> (bnd_z = bnd_z) = False) \<or>
sultana@55596
   452
         bnd_less bnd_y bnd_z = True \<Longrightarrow>
sultana@55596
   453
         (bnd_y = bnd_x) = False \<or> bnd_less bnd_y bnd_z = True"
sultana@55596
   454
apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
sultana@55596
   455
done
sultana@55596
   456
*)
sultana@55596
   457
sultana@55596
   458
(* SEU602^2 *)
sultana@55596
   459
consts
sultana@55596
   460
  SEU602_2_bnd_sK7_E :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   461
  SEU602_2_bnd_sK2_SY17 :: TPTP_Interpret.ind
sultana@55596
   462
  SEU602_2_bnd_in :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   463
sultana@55596
   464
     (* (Annotated_step ("113", "extuni_func"), *)
wenzelm@61076
   465
lemma "\<forall>SV49::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
   466
            (SV49 =
wenzelm@61076
   467
             (\<lambda>SY23::TPTP_Interpret.ind.
sultana@55596
   468
                 \<not> SEU602_2_bnd_in SY23 SEU602_2_bnd_sK2_SY17)) =
sultana@55596
   469
            False \<Longrightarrow>
wenzelm@61076
   470
         \<forall>SV49::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
   471
            (SV49 (SEU602_2_bnd_sK7_E SV49) =
sultana@55596
   472
             (\<not> SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
sultana@55596
   473
            False"
sultana@55596
   474
(*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
wenzelm@63167
   475
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]\<close>)
sultana@55596
   476
sultana@55596
   477
consts
sultana@55596
   478
  SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   479
  SEV405_5_bnd_cA :: bool
sultana@55596
   480
wenzelm@61076
   481
lemma "\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
   482
            (\<forall>SY2::TPTP_Interpret.ind.
sultana@55596
   483
                \<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
sultana@55596
   484
                   \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
sultana@55596
   485
            False \<Longrightarrow>
wenzelm@61076
   486
         \<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
   487
            (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
sultana@55596
   488
                \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
sultana@55596
   489
            False"
wenzelm@63167
   490
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
   491
(*
sultana@55596
   492
strip quantifiers -- creating a space of permutations; from shallowest to deepest (iterative deepening)
sultana@55596
   493
flip the conclusion -- giving us branch
sultana@55596
   494
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.
sultana@55596
   495
*)
sultana@55596
   496
sultana@55596
   497
consts
sultana@55596
   498
  SEU581_2_bnd_sK1 :: "TPTP_Interpret.ind"
sultana@55596
   499
  SEU581_2_bnd_sK2 :: "TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   500
  SEU581_2_bnd_subset :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> HOL.bool"
sultana@55596
   501
  SEU581_2_bnd_dsetconstr ::  "TPTP_Interpret.ind \<Rightarrow> (TPTP_Interpret.ind \<Rightarrow> HOL.bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   502
sultana@55596
   503
(*testing parameters*)
sultana@55596
   504
lemma "! X :: TPTP_Interpret.ind . (\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
sultana@55596
   505
\<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"
wenzelm@63167
   506
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   507
sultana@55596
   508
lemma "(A & B) = True ==> (A | B) = True"
wenzelm@63167
   509
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   510
sultana@55596
   511
lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
wenzelm@63167
   512
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   513
sultana@55596
   514
(*testing goals with parameters*)
sultana@55596
   515
lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> ! X. (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
wenzelm@63167
   516
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   517
sultana@55596
   518
lemma "(A & B) = True ==> (B & A) = True"
wenzelm@63167
   519
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   520
sultana@55596
   521
(*appreciating differences between THEN, REPEAT, and APPEND*)
sultana@55596
   522
lemma "A & B ==> B & A"
wenzelm@63167
   523
apply (tactic \<open>
sultana@55596
   524
  TRY (etac @{thm conjE} 1)
wenzelm@63167
   525
  THEN TRY (rtac @{thm conjI} 1)\<close>)
sultana@55596
   526
by assumption+
sultana@55596
   527
sultana@55596
   528
lemma "A & B ==> B & A"
wenzelm@63167
   529
by (tactic \<open>
sultana@55596
   530
  etac @{thm conjE} 1
sultana@55596
   531
  THEN rtac @{thm conjI} 1
wenzelm@63167
   532
  THEN REPEAT (atac 1)\<close>)
sultana@55596
   533
sultana@55596
   534
lemma "A & B ==> B & A"
wenzelm@63167
   535
apply (tactic \<open>
sultana@55596
   536
  rtac @{thm conjI} 1
wenzelm@63167
   537
  APPEND etac @{thm conjE} 1\<close>)+
sultana@55596
   538
back
sultana@55596
   539
by assumption+
sultana@55596
   540
sultana@55596
   541
consts
sultana@55596
   542
  SEU581_2_bnd_sK3 :: "TPTP_Interpret.ind"
sultana@55596
   543
  SEU581_2_bnd_sK4 :: "TPTP_Interpret.ind"
sultana@55596
   544
  SEU581_2_bnd_sK5 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   545
  SEU581_2_bnd_powerset :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   546
  SEU581_2_bnd_in :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   547
sultana@55596
   548
consts
sultana@55596
   549
  bnd_c1 :: TPTP_Interpret.ind
sultana@55596
   550
  bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   551
sultana@55596
   552
lemma "(\<forall>SX0. (\<not> (\<not> SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \<or>
sultana@55596
   553
              \<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
sultana@55596
   554
                    (PUZ114_5_bnd_sK5 SX0) \<or>
sultana@55596
   555
                 \<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
sultana@55596
   556
                    (bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
sultana@55596
   557
           \<not> SX0 bnd_c1 bnd_c1) \<or>
sultana@55596
   558
          SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
sultana@55596
   559
   True ==> \<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   560
              \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
sultana@55596
   561
                    (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   562
                 \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
sultana@55596
   563
                    (bnd_s (PUZ114_5_bnd_sK5 SV1)))) \<or>
sultana@55596
   564
           \<not> SV1 bnd_c1 bnd_c1) \<or>
sultana@55596
   565
          SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
sultana@55596
   566
         True"
wenzelm@63167
   567
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   568
sultana@55596
   569
lemma "(\<not> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = True \<Longrightarrow> (SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = False"
wenzelm@63167
   570
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   571
sultana@55596
   572
(*testing repeated application of simulator*)
sultana@55596
   573
lemma "(\<not> \<not> False) = True \<Longrightarrow>
sultana@55596
   574
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
sultana@55596
   575
    False = True \<or> False = True \<or> False = True"
wenzelm@63167
   576
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   577
sultana@55596
   578
(*Testing non-normal conclusion. Ideally we should be able to apply
sultana@55596
   579
  the tactic to arbitrary chains of extcnf steps -- where it's not
sultana@55596
   580
  generally the case that the conclusions are normal.*)
sultana@55596
   581
lemma "(\<not> \<not> False) = True \<Longrightarrow>
sultana@55596
   582
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
sultana@55596
   583
    (\<not> False) = False"
wenzelm@63167
   584
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   585
sultana@55596
   586
(*testing repeated application of simulator, involving different extcnf rules*)
sultana@55596
   587
lemma "(\<not> \<not> (False | False)) = True \<Longrightarrow>
sultana@55596
   588
    SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
sultana@55596
   589
    False = True \<or> False = True \<or> False = True"
wenzelm@63167
   590
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   591
sultana@55596
   592
(*testing logical expansion*)
sultana@55596
   593
lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
sultana@55596
   594
\<Longrightarrow> (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
wenzelm@63167
   595
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   596
sultana@55596
   597
(*testing extcnf_forall_pos*)
sultana@55596
   598
lemma "(\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True \<Longrightarrow> \<forall>SV1. (\<forall>SY14.
sultana@55596
   599
             SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14)
sultana@55596
   600
              (SEU581_2_bnd_powerset SV1)) = True"
wenzelm@63167
   601
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   602
sultana@55596
   603
lemma "((\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True) | ((~ False) = False) \<Longrightarrow>
sultana@55596
   604
\<forall>SV1. ((\<forall>SY14. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True) | ((~ False) = False)"
wenzelm@63167
   605
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   606
sultana@55596
   607
(*testing parameters*)
sultana@55596
   608
lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
sultana@55596
   609
\<Longrightarrow> ! X. (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
wenzelm@63167
   610
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   611
sultana@55596
   612
lemma "((? A .P1 A) = False) | P2 = True \<Longrightarrow> !X. ((P1 X) = False | P2 = True)"
wenzelm@63167
   613
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   614
sultana@55596
   615
lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) \<Longrightarrow> !X. (P1a X = True | P1b X = True | P2 = True)"
wenzelm@63167
   616
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   617
sultana@55596
   618
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
wenzelm@63167
   619
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   620
sultana@55596
   621
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
wenzelm@63167
   622
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   623
sultana@55596
   624
lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
wenzelm@63167
   625
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   626
sultana@55596
   627
consts dud_bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
   628
sultana@55596
   629
(*this lemma kills blast*)
sultana@55596
   630
lemma "(\<not> (\<forall>SX0 SX1.
sultana@55596
   631
          \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or> PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SX0)) SX1) \<or>
sultana@55596
   632
    \<not> (\<forall>SX0 SX1.
sultana@55596
   633
          \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
sultana@55596
   634
          PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
sultana@55596
   635
   False \<Longrightarrow> (\<not> (\<forall>SX0 SX1.
sultana@55596
   636
          \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
sultana@55596
   637
          PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
sultana@55596
   638
   False"
wenzelm@63167
   639
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   640
sultana@55596
   641
(*testing logical expansion -- this should be done by blast*)
sultana@55596
   642
lemma "(\<forall>A B. bnd_in B (bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
sultana@55596
   643
\<Longrightarrow> (\<forall>A B. \<not> bnd_in B (bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
wenzelm@63167
   644
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   645
sultana@55596
   646
(*testing related to PUZ114^5.p.out*)
sultana@55596
   647
lemma "\<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   648
                    \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
sultana@55596
   649
                          (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   650
                       \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
sultana@55596
   651
                          (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
sultana@55596
   652
                True \<or>
sultana@55596
   653
                (\<not> SV1 bnd_c1 bnd_c1) = True) \<or>
sultana@55596
   654
               SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True \<Longrightarrow>
sultana@55596
   655
         \<forall>SV1. (SV1 bnd_c1 bnd_c1 = False \<or>
sultana@55596
   656
                (\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   657
                    \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
sultana@55596
   658
                          (PUZ114_5_bnd_sK5 SV1) \<or>
sultana@55596
   659
                       \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
sultana@55596
   660
                          (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
sultana@55596
   661
                True) \<or>
sultana@55596
   662
               SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True"
wenzelm@63167
   663
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   664
sultana@55596
   665
lemma "\<forall>SV2. (\<forall>SY41.
sultana@55596
   666
                   \<not> PUZ114_5_bnd_sK3 SV2 SY41 \<or>
sultana@55596
   667
                   PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SY41) =
sultana@55596
   668
               True \<Longrightarrow>
sultana@55596
   669
         \<forall>SV4 SV2.
sultana@55596
   670
            (\<not> PUZ114_5_bnd_sK3 SV2 SV4 \<or>
sultana@55596
   671
             PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) =
sultana@55596
   672
            True"
wenzelm@63167
   673
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   674
sultana@55596
   675
lemma "\<forall>SV3. (\<forall>SY42.
sultana@55596
   676
                   \<not> PUZ114_5_bnd_sK3 SV3 SY42 \<or>
sultana@55596
   677
                   PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SY42)) =
sultana@55596
   678
               True \<Longrightarrow>
sultana@55596
   679
         \<forall>SV5 SV3.
sultana@55596
   680
            (\<not> PUZ114_5_bnd_sK3 SV3 SV5 \<or>
sultana@55596
   681
             PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) =
sultana@55596
   682
            True"
wenzelm@63167
   683
by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
sultana@55596
   684
sultana@55596
   685
sultana@55596
   686
subsection "unfold_def"
sultana@55596
   687
     (* (Annotated_step ("9", "unfold_def"), *)
sultana@55596
   688
lemma "bnd_kpairiskpair =
sultana@55596
   689
             (ALL Xx Xy.
sultana@55596
   690
                 bnd_iskpair
sultana@55596
   691
                  (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   692
                    (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   693
                      bnd_emptyset))) &
sultana@55596
   694
             bnd_kpair =
sultana@55596
   695
             (%Xx Xy.
sultana@55596
   696
                 bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   697
                  (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   698
                    bnd_emptyset)) &
sultana@55596
   699
             bnd_iskpair =
sultana@55596
   700
             (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
sultana@55596
   701
                         (EX Xy. bnd_in Xy (bnd_setunion A) &
sultana@55596
   702
                                 A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   703
                                      (bnd_setadjoin
sultana@55596
   704
                                        (bnd_setadjoin Xx
sultana@55596
   705
(bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   706
                                        bnd_emptyset))) &
sultana@55596
   707
             (~ (ALL SY0 SY1.
sultana@55596
   708
                    EX SY3.
sultana@55596
   709
                       bnd_in SY3
sultana@55596
   710
                        (bnd_setunion
sultana@55596
   711
                          (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
   712
                            (bnd_setadjoin
sultana@55596
   713
                              (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
   714
                              bnd_emptyset))) &
sultana@55596
   715
                       (EX SY4.
sultana@55596
   716
                           bnd_in SY4
sultana@55596
   717
                            (bnd_setunion
sultana@55596
   718
                              (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
   719
                                (bnd_setadjoin
sultana@55596
   720
                                  (bnd_setadjoin SY0
sultana@55596
   721
                                    (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
   722
                                  bnd_emptyset))) &
sultana@55596
   723
                           bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
   724
                            (bnd_setadjoin
sultana@55596
   725
                              (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
   726
                              bnd_emptyset) =
sultana@55596
   727
                           bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset)
sultana@55596
   728
                            (bnd_setadjoin
sultana@55596
   729
                              (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
sultana@55596
   730
                              bnd_emptyset)))) =
sultana@55596
   731
             True
sultana@55596
   732
             ==> (~ (ALL SX0 SX1.
sultana@55596
   733
                        ~ (ALL SX2.
sultana@55596
   734
                              ~ ~ (~ bnd_in SX2
sultana@55596
   735
                                      (bnd_setunion
sultana@55596
   736
                                        (bnd_setadjoin
sultana@55596
   737
(bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   738
(bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) |
sultana@55596
   739
                                   ~ ~ (ALL SX3.
sultana@55596
   740
 ~ ~ (~ bnd_in SX3
sultana@55596
   741
         (bnd_setunion
sultana@55596
   742
           (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   743
             (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
   744
               bnd_emptyset))) |
sultana@55596
   745
      bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   746
       (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
   747
         bnd_emptyset) ~=
sultana@55596
   748
      bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
sultana@55596
   749
       (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
sultana@55596
   750
         bnd_emptyset))))))) =
sultana@55596
   751
                 True"
wenzelm@63167
   752
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
   753
sultana@55596
   754
     (* (Annotated_step ("10", "unfold_def"), *)
sultana@55596
   755
lemma "bnd_kpairiskpair =
sultana@55596
   756
             (ALL Xx Xy.
sultana@55596
   757
                 bnd_iskpair
sultana@55596
   758
                  (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   759
                    (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   760
                      bnd_emptyset))) &
sultana@55596
   761
             bnd_kpair =
sultana@55596
   762
             (%Xx Xy.
sultana@55596
   763
                 bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   764
                  (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   765
                    bnd_emptyset)) &
sultana@55596
   766
             bnd_iskpair =
sultana@55596
   767
             (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
sultana@55596
   768
                         (EX Xy. bnd_in Xy (bnd_setunion A) &
sultana@55596
   769
                                 A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
   770
                                      (bnd_setadjoin
sultana@55596
   771
                                        (bnd_setadjoin Xx
sultana@55596
   772
(bnd_setadjoin Xy bnd_emptyset))
sultana@55596
   773
                                        bnd_emptyset))) &
sultana@55596
   774
             (ALL SY5 SY6.
sultana@55596
   775
                 EX SY7.
sultana@55596
   776
                    bnd_in SY7
sultana@55596
   777
                     (bnd_setunion
sultana@55596
   778
                       (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
   779
                         (bnd_setadjoin
sultana@55596
   780
                           (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
   781
                           bnd_emptyset))) &
sultana@55596
   782
                    (EX SY8.
sultana@55596
   783
                        bnd_in SY8
sultana@55596
   784
                         (bnd_setunion
sultana@55596
   785
                           (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
   786
                             (bnd_setadjoin
sultana@55596
   787
                               (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
   788
                               bnd_emptyset))) &
sultana@55596
   789
                        bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
   790
                         (bnd_setadjoin
sultana@55596
   791
                           (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
   792
                           bnd_emptyset) =
sultana@55596
   793
                        bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset)
sultana@55596
   794
                         (bnd_setadjoin
sultana@55596
   795
                           (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset))
sultana@55596
   796
                           bnd_emptyset))) =
sultana@55596
   797
             True
sultana@55596
   798
             ==> (ALL SX0 SX1.
sultana@55596
   799
                     ~ (ALL SX2.
sultana@55596
   800
                           ~ ~ (~ bnd_in SX2
sultana@55596
   801
                                   (bnd_setunion
sultana@55596
   802
                                     (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   803
                                       (bnd_setadjoin
sultana@55596
   804
                                         (bnd_setadjoin SX0
sultana@55596
   805
 (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
   806
                                         bnd_emptyset))) |
sultana@55596
   807
                                ~ ~ (ALL SX3.
sultana@55596
   808
                                        ~ ~ (~ bnd_in SX3
sultana@55596
   809
      (bnd_setunion
sultana@55596
   810
        (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   811
          (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
   812
            bnd_emptyset))) |
sultana@55596
   813
   bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
   814
    (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
   815
      bnd_emptyset) ~=
sultana@55596
   816
   bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
sultana@55596
   817
    (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
sultana@55596
   818
      bnd_emptyset)))))) =
sultana@55596
   819
                 True"
wenzelm@63167
   820
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
   821
sultana@55596
   822
     (* (Annotated_step ("12", "unfold_def"), *)
sultana@55596
   823
lemma "bnd_cCKB6_BLACK =
sultana@55596
   824
         (\<lambda>Xu Xv.
sultana@55596
   825
             \<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
sultana@55596
   826
                  (\<forall>Xj Xk.
sultana@55596
   827
                      Xw Xj Xk \<longrightarrow>
sultana@55596
   828
                      Xw (bnd_s (bnd_s Xj)) Xk \<and>
sultana@55596
   829
                      Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
sultana@55596
   830
                  Xw Xu Xv) \<and>
sultana@55596
   831
         ((((\<forall>SY36 SY37.
sultana@55596
   832
                \<not> PUZ114_5_bnd_sK3 SY36 SY37 \<or>
sultana@55596
   833
                PUZ114_5_bnd_sK3 (bnd_s (bnd_s SY36)) SY37) \<and>
sultana@55596
   834
            (\<forall>SY38 SY39.
sultana@55596
   835
                \<not> PUZ114_5_bnd_sK3 SY38 SY39 \<or>
sultana@55596
   836
                PUZ114_5_bnd_sK3 (bnd_s SY38) (bnd_s SY39))) \<and>
sultana@55596
   837
           PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<and>
sultana@55596
   838
          \<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
sultana@55596
   839
             (bnd_s PUZ114_5_bnd_sK2)) =
sultana@55596
   840
         True \<Longrightarrow>
sultana@55596
   841
         (\<not> (\<not> \<not> (\<not> \<not> (\<not> (\<forall>SX0 SX1.
sultana@55596
   842
                             \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
sultana@55596
   843
                             PUZ114_5_bnd_sK3 (bnd_s (bnd_s SX0)) SX1) \<or>
sultana@55596
   844
                       \<not> (\<forall>SX0 SX1.
sultana@55596
   845
                             \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
sultana@55596
   846
                             PUZ114_5_bnd_sK3 (bnd_s SX0) (bnd_s SX1))) \<or>
sultana@55596
   847
                  \<not> PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<or>
sultana@55596
   848
             \<not> \<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
sultana@55596
   849
                  (bnd_s PUZ114_5_bnd_sK2))) =
sultana@55596
   850
         True"
sultana@55596
   851
(*
sultana@55596
   852
apply (erule conjE)+
sultana@55596
   853
apply (erule subst)+
sultana@55596
   854
apply (tactic {*log_expander 1*})+
sultana@55596
   855
apply (rule refl)
sultana@55596
   856
*)
wenzelm@63167
   857
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
   858
sultana@55596
   859
     (* (Annotated_step ("13", "unfold_def"), *)
sultana@55596
   860
lemma "bnd_cCKB6_BLACK =
sultana@55596
   861
         (\<lambda>Xu Xv.
sultana@55596
   862
             \<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
sultana@55596
   863
                  (\<forall>Xj Xk.
sultana@55596
   864
                      Xw Xj Xk \<longrightarrow>
sultana@55596
   865
                      Xw (bnd_s (bnd_s Xj)) Xk \<and>
sultana@55596
   866
                      Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
sultana@55596
   867
                  Xw Xu Xv) \<and>
sultana@55596
   868
         (\<forall>SY30.
sultana@55596
   869
             (SY30 (PUZ114_5_bnd_sK4 SY30) (PUZ114_5_bnd_sK5 SY30) \<and>
sultana@55596
   870
              (\<not> SY30 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SY30)))
sultana@55596
   871
                  (PUZ114_5_bnd_sK5 SY30) \<or>
sultana@55596
   872
               \<not> SY30 (bnd_s (PUZ114_5_bnd_sK4 SY30))
sultana@55596
   873
                  (bnd_s (PUZ114_5_bnd_sK5 SY30))) \<or>
sultana@55596
   874
              \<not> SY30 bnd_c1 bnd_c1) \<or>
sultana@55596
   875
             SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
sultana@55596
   876
         True \<Longrightarrow>
sultana@55596
   877
         (\<forall>SX0. (\<not> (\<not> SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \<or>
sultana@55596
   878
                    \<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
sultana@55596
   879
                          (PUZ114_5_bnd_sK5 SX0) \<or>
sultana@55596
   880
                       \<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
sultana@55596
   881
                          (bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
sultana@55596
   882
                 \<not> SX0 bnd_c1 bnd_c1) \<or>
sultana@55596
   883
                SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
sultana@55596
   884
         True"
sultana@55596
   885
(*
sultana@55596
   886
apply (erule conjE)+
sultana@55596
   887
apply (tactic {*expander_animal 1*})+
sultana@55596
   888
apply assumption
sultana@55596
   889
*)
wenzelm@63167
   890
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
   891
sultana@55596
   892
(*FIXME move this heuristic elsewhere*)
wenzelm@63167
   893
ML \<open>
sultana@55596
   894
(*Other than the list (which must not be empty) this function
sultana@55596
   895
  expects a parameter indicating the smallest integer.
sultana@55596
   896
  (Using Int.minInt isn't always viable).*)
sultana@55596
   897
fun max_int_floored min l =
sultana@55596
   898
  if null l then raise List.Empty
sultana@55596
   899
  else fold (curry Int.max) l min;
sultana@55596
   900
sultana@55596
   901
val _ = @{assert} (max_int_floored ~101002 [1]  = 1)
sultana@55596
   902
val _ = @{assert} (max_int_floored 0 [1, 3, 5] = 5)
sultana@55596
   903
sultana@55596
   904
fun max_index_floored min l =
sultana@55596
   905
  let
sultana@55596
   906
    val max = max_int_floored min l
sultana@55596
   907
  in find_index (pair max #> op =) l end
wenzelm@63167
   908
\<close>
sultana@55596
   909
wenzelm@63167
   910
ML \<open>
sultana@55596
   911
max_index_floored 0 [1, 3, 5]
wenzelm@63167
   912
\<close>
sultana@55596
   913
wenzelm@63167
   914
ML \<open>
sultana@55596
   915
(*
sultana@55596
   916
Given argument ([h_1, ..., h_n], conc),
sultana@55596
   917
obtained from term of form
sultana@55596
   918
  h_1 ==> ... ==> h_n ==> conclusion,
sultana@55596
   919
this function indicates which h_i is biggest,
sultana@55596
   920
or NONE if h_n = 0.
sultana@55596
   921
*)
sultana@55596
   922
fun biggest_hypothesis (hypos, _) =
sultana@55596
   923
  if null hypos then NONE
sultana@55596
   924
  else
sultana@55596
   925
    map size_of_term hypos
sultana@55596
   926
    |> max_index_floored 0
sultana@55596
   927
    |> SOME
wenzelm@63167
   928
\<close>
sultana@55596
   929
wenzelm@63167
   930
ML \<open>
sultana@55596
   931
fun biggest_hyp_first_tac i = fn st =>
sultana@55596
   932
  let
sultana@55596
   933
    val results = TERMFUN biggest_hypothesis (SOME i) st
wenzelm@60925
   934
val _ = tracing ("result=" ^ @{make_string} results)
sultana@55596
   935
  in
sultana@55596
   936
    if null results then no_tac st
sultana@55596
   937
    else
sultana@55596
   938
      let
sultana@55596
   939
        val result = the_single results
sultana@55596
   940
      in
sultana@55596
   941
        case result of
sultana@55596
   942
            NONE => no_tac st
sultana@55596
   943
          | SOME n =>
sultana@55596
   944
              if n > 0 then rotate_tac n i st else no_tac st
sultana@55596
   945
      end
sultana@55596
   946
  end
wenzelm@63167
   947
\<close>
sultana@55596
   948
sultana@55596
   949
     (* (Annotated_step ("6", "unfold_def"), *)
sultana@55596
   950
lemma  "(\<not> (\<exists>U :: TPTP_Interpret.ind \<Rightarrow> bool. \<forall>V. U V = SEV405_5_bnd_cA)) = True \<Longrightarrow>
sultana@55596
   951
         (\<not> \<not> (\<forall>SX0 :: TPTP_Interpret.ind \<Rightarrow> bool. \<not> (\<forall>SX1. \<not> (\<not> (\<not> SX0 SX1 \<or> SEV405_5_bnd_cA) \<or>
sultana@55596
   952
 \<not> (\<not> SEV405_5_bnd_cA \<or> SX0 SX1))))) =
sultana@55596
   953
         True"
sultana@55596
   954
(* by (tactic {*unfold_def_tac []*}) *)
sultana@55596
   955
oops
sultana@55596
   956
sultana@55596
   957
subsection "Using leo2_tac"
sultana@55596
   958
(*these require PUZ114^5's proof to be loaded
sultana@55596
   959
sultana@55596
   960
ML {*leo2_tac @{context} (hd prob_names) "50"*}
sultana@55596
   961
sultana@55596
   962
ML {*leo2_tac @{context} (hd prob_names) "4"*}
sultana@55596
   963
sultana@55596
   964
ML {*leo2_tac @{context} (hd prob_names) "9"*}
sultana@55596
   965
sultana@55596
   966
     (* (Annotated_step ("9", "extcnf_combined"), *)
sultana@55596
   967
lemma "(\<forall>SY30.
sultana@55596
   968
             SY30 bnd_c1 bnd_c1 \<and>
sultana@55596
   969
             (\<forall>Xj Xk.
sultana@55596
   970
                 SY30 Xj Xk \<longrightarrow>
sultana@55596
   971
                 SY30 (bnd_s (bnd_s Xj)) Xk \<and>
sultana@55596
   972
                 SY30 (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
sultana@55596
   973
             SY30 bnd_sK1 bnd_sK2) =
sultana@55596
   974
         True \<Longrightarrow>
sultana@55596
   975
         (\<forall>SY30.
sultana@55596
   976
             (SY30 (bnd_sK4 SY30) (bnd_sK5 SY30) \<and>
sultana@55596
   977
              (\<not> SY30 (bnd_s (bnd_s (bnd_sK4 SY30)))
sultana@55596
   978
                  (bnd_sK5 SY30) \<or>
sultana@55596
   979
               \<not> SY30 (bnd_s (bnd_sK4 SY30))
sultana@55596
   980
                  (bnd_s (bnd_sK5 SY30))) \<or>
sultana@55596
   981
              \<not> SY30 bnd_c1 bnd_c1) \<or>
sultana@55596
   982
             SY30 bnd_sK1 bnd_sK2) =
sultana@55596
   983
         True"
sultana@55596
   984
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
sultana@55596
   985
*)
sultana@55596
   986
sultana@55596
   987
sultana@55596
   988
sultana@55596
   989
typedecl GEG007_1_bnd_reg
sultana@55596
   990
consts
sultana@55596
   991
  GEG007_1_bnd_sK7_SX2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> GEG007_1_bnd_reg"
sultana@55596
   992
  GEG007_1_bnd_sK6_SX2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> GEG007_1_bnd_reg"
sultana@55596
   993
  GEG007_1_bnd_a :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
   994
  GEG007_1_bnd_catalunya  :: "GEG007_1_bnd_reg"
sultana@55596
   995
  GEG007_1_bnd_spain :: "GEG007_1_bnd_reg"
sultana@55596
   996
  GEG007_1_bnd_c :: "GEG007_1_bnd_reg \<Rightarrow> GEG007_1_bnd_reg \<Rightarrow> bool"
sultana@55596
   997
sultana@55596
   998
     (* (Annotated_step ("147", "extcnf_forall_neg"), *)
sultana@55596
   999
lemma "\<forall>SV13 SV6.
sultana@55596
  1000
            (\<forall>SX2. \<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
sultana@55596
  1001
                   GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya) =
sultana@55596
  1002
            False \<or>
sultana@55596
  1003
            GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
sultana@55596
  1004
         \<forall>SV6 SV13.
sultana@55596
  1005
            (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_spain \<or>
sultana@55596
  1006
             GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) =
sultana@55596
  1007
            False \<or>
sultana@55596
  1008
            GEG007_1_bnd_a SV6 SV13 = False"
wenzelm@63167
  1009
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
  1010
sultana@55596
  1011
     (* (Annotated_step ("116", "extcnf_forall_neg"), *)
sultana@55596
  1012
lemma "\<forall>SV13 SV6.
sultana@55596
  1013
            (\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya \<or>
sultana@55596
  1014
                             \<not> \<not> \<not> (\<forall>SX3.
sultana@55596
  1015
       \<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
sultana@55596
  1016
            \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
sultana@55596
  1017
                     GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
sultana@55596
  1018
                        \<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
sultana@55596
  1019
                             \<not> \<not> \<not> (\<forall>SX3.
sultana@55596
  1020
       \<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
sultana@55596
  1021
            \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
sultana@55596
  1022
                     GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
sultana@55596
  1023
            False \<or>
sultana@55596
  1024
            GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
sultana@55596
  1025
         \<forall>SV6 SV13.
sultana@55596
  1026
            (\<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
sultana@55596
  1027
                          GEG007_1_bnd_catalunya \<or>
sultana@55596
  1028
                       \<not> \<not> \<not> (\<forall>SY68.
sultana@55596
  1029
 \<not> \<not> (\<not> (\<forall>SY69.
sultana@55596
  1030
            \<not> GEG007_1_bnd_c SY69 SY68 \<or>
sultana@55596
  1031
            GEG007_1_bnd_c SY69 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
sultana@55596
  1032
      \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY68 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
sultana@55596
  1033
                  \<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
sultana@55596
  1034
                          GEG007_1_bnd_spain \<or>
sultana@55596
  1035
                       \<not> \<not> \<not> (\<forall>SY71.
sultana@55596
  1036
 \<not> \<not> (\<not> (\<forall>SY72.
sultana@55596
  1037
            \<not> GEG007_1_bnd_c SY72 SY71 \<or>
sultana@55596
  1038
            GEG007_1_bnd_c SY72 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
sultana@55596
  1039
      \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY71 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
sultana@55596
  1040
            False \<or>
sultana@55596
  1041
            GEG007_1_bnd_a SV6 SV13 = False"
wenzelm@63167
  1042
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
  1043
sultana@55596
  1044
consts PUZ107_5_bnd_sK1_SX0 ::
sultana@55596
  1045
  "TPTP_Interpret.ind
sultana@55596
  1046
      \<Rightarrow> TPTP_Interpret.ind
sultana@55596
  1047
        \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1048
wenzelm@61076
  1049
lemma "\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
wenzelm@61076
  1050
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
wenzelm@61076
  1051
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
sultana@55596
  1052
   ((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
sultana@55596
  1053
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
wenzelm@61076
  1054
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
wenzelm@61076
  1055
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
wenzelm@61076
  1056
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
sultana@55596
  1057
   ((SV1 = SV3) = True \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
sultana@55596
  1058
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
wenzelm@63167
  1059
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Not_neg]\<close>)
sultana@55596
  1060
sultana@55596
  1061
lemma "
wenzelm@61076
  1062
\<forall>(SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind)
wenzelm@61076
  1063
   (SV4::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
wenzelm@61076
  1064
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
sultana@55596
  1065
   ((SV1 \<noteq> SV3 \<or> SV2 \<noteq> SV4) = False \<or>
sultana@55596
  1066
    PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
sultana@55596
  1067
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
wenzelm@61076
  1068
\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
wenzelm@61076
  1069
   (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
wenzelm@61076
  1070
   (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
sultana@55596
  1071
   ((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
sultana@55596
  1072
   PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
wenzelm@63167
  1073
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Or_neg]\<close>)
sultana@55596
  1074
sultana@55596
  1075
consts
sultana@55596
  1076
  NUM016_5_bnd_a :: TPTP_Interpret.ind
sultana@55596
  1077
  NUM016_5_bnd_prime :: "TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1078
  NUM016_5_bnd_factorial_plus_one :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
  1079
  NUM016_5_bnd_prime_divisor :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
  1080
  NUM016_5_bnd_divides :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1081
  NUM016_5_bnd_less :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1082
sultana@55596
  1083
     (* (Annotated_step ("6", "unfold_def"), *)
wenzelm@61076
  1084
lemma "((((((((((((\<forall>X::TPTP_Interpret.ind. \<not> NUM016_5_bnd_less X X) \<and>
wenzelm@61076
  1085
                    (\<forall>(X::TPTP_Interpret.ind)
wenzelm@61076
  1086
                        Y::TPTP_Interpret.ind.
sultana@55596
  1087
                        \<not> NUM016_5_bnd_less X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
wenzelm@61076
  1088
                   (\<forall>X::TPTP_Interpret.ind. NUM016_5_bnd_divides X X)) \<and>
wenzelm@61076
  1089
                  (\<forall>(X::TPTP_Interpret.ind)
wenzelm@61076
  1090
                      (Y::TPTP_Interpret.ind)
wenzelm@61076
  1091
                      Z::TPTP_Interpret.ind.
sultana@55596
  1092
                      (\<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_divides Y Z) \<or>
sultana@55596
  1093
                      NUM016_5_bnd_divides X Z)) \<and>
wenzelm@61076
  1094
                 (\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
sultana@55596
  1095
                     \<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
wenzelm@61076
  1096
                (\<forall>X::TPTP_Interpret.ind.
sultana@55596
  1097
                    NUM016_5_bnd_less X (NUM016_5_bnd_factorial_plus_one X))) \<and>
wenzelm@61076
  1098
               (\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
sultana@55596
  1099
                   \<not> NUM016_5_bnd_divides X (NUM016_5_bnd_factorial_plus_one Y) \<or>
sultana@55596
  1100
                   NUM016_5_bnd_less Y X)) \<and>
wenzelm@61076
  1101
              (\<forall>X::TPTP_Interpret.ind.
sultana@55596
  1102
                  NUM016_5_bnd_prime X \<or>
sultana@55596
  1103
                  NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor X) X)) \<and>
wenzelm@61076
  1104
             (\<forall>X::TPTP_Interpret.ind.
sultana@55596
  1105
                 NUM016_5_bnd_prime X \<or>
sultana@55596
  1106
                 NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor X))) \<and>
wenzelm@61076
  1107
            (\<forall>X::TPTP_Interpret.ind.
sultana@55596
  1108
                NUM016_5_bnd_prime X \<or>
sultana@55596
  1109
                NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor X) X)) \<and>
sultana@55596
  1110
           NUM016_5_bnd_prime NUM016_5_bnd_a) \<and>
wenzelm@61076
  1111
          (\<forall>X::TPTP_Interpret.ind.
sultana@55596
  1112
              (\<not> NUM016_5_bnd_prime X \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a X) \<or>
sultana@55596
  1113
              NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) X)) =
sultana@55596
  1114
         True \<Longrightarrow>
wenzelm@61076
  1115
         (\<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.
sultana@55596
  1116
     \<not> NUM016_5_bnd_less SX0 SX0) \<or>
wenzelm@61076
  1117
                               \<not> (\<forall>(SX0::TPTP_Interpret.ind)
wenzelm@61076
  1118
     SX1::TPTP_Interpret.ind.
sultana@55596
  1119
     \<not> NUM016_5_bnd_less SX0 SX1 \<or> \<not> NUM016_5_bnd_less SX1 SX0)) \<or>
wenzelm@61076
  1120
                          \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1121
NUM016_5_bnd_divides SX0 SX0)) \<or>
wenzelm@61076
  1122
                     \<not> (\<forall>(SX0::TPTP_Interpret.ind)
wenzelm@61076
  1123
                           (SX1::TPTP_Interpret.ind)
wenzelm@61076
  1124
                           SX2::TPTP_Interpret.ind.
sultana@55596
  1125
                           (\<not> NUM016_5_bnd_divides SX0 SX1 \<or>
sultana@55596
  1126
                            \<not> NUM016_5_bnd_divides SX1 SX2) \<or>
sultana@55596
  1127
                           NUM016_5_bnd_divides SX0 SX2)) \<or>
wenzelm@61076
  1128
                \<not> (\<forall>(SX0::TPTP_Interpret.ind)
wenzelm@61076
  1129
                      SX1::TPTP_Interpret.ind.
sultana@55596
  1130
                      \<not> NUM016_5_bnd_divides SX0 SX1 \<or>
sultana@55596
  1131
                      \<not> NUM016_5_bnd_less SX1 SX0)) \<or>
wenzelm@61076
  1132
           \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1133
                 NUM016_5_bnd_less SX0 (NUM016_5_bnd_factorial_plus_one SX0))) \<or>
wenzelm@61076
  1134
      \<not> (\<forall>(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind.
sultana@55596
  1135
            \<not> NUM016_5_bnd_divides SX0 (NUM016_5_bnd_factorial_plus_one SX1) \<or>
sultana@55596
  1136
            NUM016_5_bnd_less SX1 SX0)) \<or>
wenzelm@61076
  1137
 \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1138
       NUM016_5_bnd_prime SX0 \<or>
sultana@55596
  1139
       NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor SX0) SX0)) \<or>
wenzelm@61076
  1140
                            \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1141
  NUM016_5_bnd_prime SX0 \<or> NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor SX0))) \<or>
wenzelm@61076
  1142
                       \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1143
                             NUM016_5_bnd_prime SX0 \<or>
sultana@55596
  1144
                             NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor SX0)
sultana@55596
  1145
                              SX0)) \<or>
sultana@55596
  1146
                  \<not> NUM016_5_bnd_prime NUM016_5_bnd_a) \<or>
wenzelm@61076
  1147
             \<not> (\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1148
                   (\<not> NUM016_5_bnd_prime SX0 \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a SX0) \<or>
sultana@55596
  1149
                   NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a)
sultana@55596
  1150
                    SX0))) =
sultana@55596
  1151
         True"
wenzelm@63167
  1152
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
  1153
sultana@55596
  1154
     (* (Annotated_step ("3", "unfold_def"), *)
sultana@55596
  1155
lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) &
sultana@55596
  1156
                           (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
sultana@55596
  1157
                          (ALL X. bnd_divides X X)) &
sultana@55596
  1158
                         (ALL X Y Z.
sultana@55596
  1159
                             (~ bnd_divides X Y | ~ bnd_divides Y Z) |
sultana@55596
  1160
                             bnd_divides X Z)) &
sultana@55596
  1161
                        (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
sultana@55596
  1162
                       (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
sultana@55596
  1163
                      (ALL X Y.
sultana@55596
  1164
                          ~ bnd_divides X (bnd_factorial_plus_one Y) |
sultana@55596
  1165
                          bnd_less Y X)) &
sultana@55596
  1166
                     (ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) &
sultana@55596
  1167
                    (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
sultana@55596
  1168
                   (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
sultana@55596
  1169
                  bnd_prime bnd_a) &
sultana@55596
  1170
                 (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
sultana@55596
  1171
                         bnd_less (bnd_factorial_plus_one bnd_a) X))) =
sultana@55596
  1172
             False
sultana@55596
  1173
             ==> (~ ((((((((((((ALL X. ~ bnd_less X X) &
sultana@55596
  1174
                               (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
sultana@55596
  1175
                              (ALL X. bnd_divides X X)) &
sultana@55596
  1176
                             (ALL X Y Z.
sultana@55596
  1177
                                 (~ bnd_divides X Y | ~ bnd_divides Y Z) |
sultana@55596
  1178
                                 bnd_divides X Z)) &
sultana@55596
  1179
                            (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
sultana@55596
  1180
                           (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
sultana@55596
  1181
                          (ALL X Y.
sultana@55596
  1182
                              ~ bnd_divides X (bnd_factorial_plus_one Y) |
sultana@55596
  1183
                              bnd_less Y X)) &
sultana@55596
  1184
                         (ALL X. bnd_prime X |
sultana@55596
  1185
                                 bnd_divides (bnd_prime_divisor X) X)) &
sultana@55596
  1186
                        (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
sultana@55596
  1187
                       (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
sultana@55596
  1188
                      bnd_prime bnd_a) &
sultana@55596
  1189
                     (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
sultana@55596
  1190
                             bnd_less (bnd_factorial_plus_one bnd_a) X))) =
sultana@55596
  1191
                 False"
wenzelm@63167
  1192
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
  1193
sultana@55596
  1194
(* SET062^6.p.out
sultana@55596
  1195
      [[(Annotated_step ("3", "unfold_def"), *)
sultana@55596
  1196
lemma "(\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False \<Longrightarrow>
sultana@55596
  1197
         (\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False"
wenzelm@63167
  1198
by (tactic \<open>unfold_def_tac @{context} []\<close>)
sultana@55596
  1199
sultana@55596
  1200
(*
sultana@55596
  1201
(* SEU559^2.p.out *)
sultana@55596
  1202
   (* [[(Annotated_step ("3", "unfold_def"), *)
sultana@55596
  1203
lemma "bnd_subset = (\<lambda>A B. \<forall>Xx. bnd_in Xx A \<longrightarrow> bnd_in Xx B) \<and>
sultana@55596
  1204
         (\<forall>A B. (\<forall>Xx. bnd_in Xx A \<longrightarrow> bnd_in Xx B) \<longrightarrow>
sultana@55596
  1205
                bnd_subset A B) =
sultana@55596
  1206
         False \<Longrightarrow>
sultana@55596
  1207
         (\<forall>SY0 SY1.
sultana@55596
  1208
             (\<forall>Xx. bnd_in Xx SY0 \<longrightarrow> bnd_in Xx SY1) \<longrightarrow>
sultana@55596
  1209
             (\<forall>SY5. bnd_in SY5 SY0 \<longrightarrow> bnd_in SY5 SY1)) =
sultana@55596
  1210
         False"
sultana@55596
  1211
by (tactic {*unfold_def_tac [@{thm bnd_subset_def}]*})
sultana@55596
  1212
sultana@55596
  1213
(* SEU559^2.p.out
sultana@55596
  1214
    [[(Annotated_step ("6", "unfold_def"), *)
sultana@55596
  1215
lemma "(\<not> (\<exists>Xx. \<forall>Xy. Xx \<longrightarrow> Xy)) = True \<Longrightarrow>
sultana@55596
  1216
         (\<not> \<not> (\<forall>SX0. \<not> (\<forall>SX1. \<not> SX0 \<or> SX1))) = True"
sultana@55596
  1217
by (tactic {*unfold_def_tac []*})
sultana@55596
  1218
sultana@55596
  1219
(* SEU502^2.p.out
sultana@55596
  1220
    [[(Annotated_step ("3", "unfold_def"), *)
sultana@55596
  1221
lemma "bnd_emptysetE =
sultana@55596
  1222
         (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<and>
sultana@55596
  1223
         (bnd_emptysetE \<longrightarrow>
sultana@55596
  1224
          (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
sultana@55596
  1225
         False \<Longrightarrow>
sultana@55596
  1226
         ((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
sultana@55596
  1227
          (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
sultana@55596
  1228
         False"
sultana@55596
  1229
by (tactic {*unfold_def_tac [@{thm bnd_emptysetE_def}]*})
sultana@55596
  1230
*)
sultana@55596
  1231
sultana@55596
  1232
typedecl AGT037_2_bnd_mu
sultana@55596
  1233
consts
sultana@55596
  1234
  AGT037_2_bnd_sK1_SX0 :: TPTP_Interpret.ind
sultana@55596
  1235
  AGT037_2_bnd_cola :: AGT037_2_bnd_mu
sultana@55596
  1236
  AGT037_2_bnd_jan :: AGT037_2_bnd_mu
sultana@55596
  1237
  AGT037_2_bnd_possibly_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1238
  AGT037_2_bnd_sK5_SY68 ::
sultana@55596
  1239
    "TPTP_Interpret.ind
sultana@55596
  1240
     \<Rightarrow> AGT037_2_bnd_mu
sultana@55596
  1241
       \<Rightarrow> AGT037_2_bnd_mu
sultana@55596
  1242
         \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
sultana@55596
  1243
  AGT037_2_bnd_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1244
  AGT037_2_bnd_very_much_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1245
  AGT037_2_bnd_a1 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1246
  AGT037_2_bnd_a2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1247
  AGT037_2_bnd_a3 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
sultana@55596
  1248
sultana@55596
  1249
(*test that nullary skolem terms are OK*)
sultana@55596
  1250
     (* (Annotated_step ("79", "extcnf_forall_neg"), *)
wenzelm@61076
  1251
lemma "(\<forall>SX0::TPTP_Interpret.ind.
sultana@55596
  1252
             AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola SX0) =
sultana@55596
  1253
         False \<Longrightarrow>
sultana@55596
  1254
         AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_SX0 =
sultana@55596
  1255
         False"
wenzelm@63167
  1256
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
  1257
sultana@55596
  1258
     (* (Annotated_step ("202", "extcnf_forall_neg"), *)
wenzelm@61076
  1259
lemma "\<forall>(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu)
wenzelm@61076
  1260
            SV45::TPTP_Interpret.ind.
wenzelm@61076
  1261
            ((((\<forall>SY68::TPTP_Interpret.ind.
sultana@55596
  1262
                   \<not> AGT037_2_bnd_a1 SV45 SY68 \<or>
sultana@55596
  1263
                   AGT037_2_bnd_likes SV29 SV39 SY68) =
sultana@55596
  1264
               False \<or>
wenzelm@61076
  1265
               (\<not> (\<forall>SY69::TPTP_Interpret.ind.
sultana@55596
  1266
                      \<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
sultana@55596
  1267
                      AGT037_2_bnd_likes SV29 SV39 SY69)) =
sultana@55596
  1268
               True) \<or>
sultana@55596
  1269
              AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
sultana@55596
  1270
             AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
sultana@55596
  1271
            AGT037_2_bnd_a3 SV13 SV45 = False \<Longrightarrow>
wenzelm@61076
  1272
         \<forall>(SV29::AGT037_2_bnd_mu) (SV39::AGT037_2_bnd_mu) (SV13::TPTP_Interpret.ind)
wenzelm@61076
  1273
            SV45::TPTP_Interpret.ind.
sultana@55596
  1274
            ((((\<not> AGT037_2_bnd_a1 SV45
sultana@55596
  1275
                   (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45) \<or>
sultana@55596
  1276
                AGT037_2_bnd_likes SV29 SV39
sultana@55596
  1277
                 (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45)) =
sultana@55596
  1278
               False \<or>
wenzelm@61076
  1279
               (\<not> (\<forall>SY69::TPTP_Interpret.ind.
sultana@55596
  1280
                      \<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
sultana@55596
  1281
                      AGT037_2_bnd_likes SV29 SV39 SY69)) =
sultana@55596
  1282
               True) \<or>
sultana@55596
  1283
              AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
sultana@55596
  1284
             AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
sultana@55596
  1285
            AGT037_2_bnd_a3 SV13 SV45 = False"
sultana@55596
  1286
(*
sultana@55596
  1287
apply (rule allI)+
sultana@55596
  1288
apply (erule_tac x = "SV13" in allE)
sultana@55596
  1289
apply (erule_tac x = "SV39" in allE)
sultana@55596
  1290
apply (erule_tac x = "SV29" in allE)
sultana@55596
  1291
apply (erule_tac x = "SV45" in allE)
sultana@55596
  1292
apply (erule disjE)+
sultana@55596
  1293
defer
sultana@55596
  1294
apply (tactic {*clause_breaker 1*})+
sultana@55596
  1295
apply (drule_tac sk = "bnd_sK5_SY68 SV13 SV39 SV29 SV45" in leo2_skolemise)
sultana@55596
  1296
defer
sultana@55596
  1297
apply (tactic {*clause_breaker 1*})
sultana@55596
  1298
apply (tactic {*nonfull_extcnf_combined_tac []*})
sultana@55596
  1299
*)
wenzelm@63167
  1300
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
  1301
sultana@55596
  1302
(*(*NUM667^1*)
sultana@55596
  1303
lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
sultana@55596
  1304
   ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
sultana@55596
  1305
      (SV14 = SV13) = False) \<or>
sultana@55596
  1306
     bnd_less SV12 SV14 = False) \<or>
sultana@55596
  1307
    bnd_less SV9 SV10 = True) \<or>
sultana@55596
  1308
   (SV9 = SV11) = False \<Longrightarrow>
sultana@55596
  1309
\<forall>SV9 SV14 SV10 SV11 SV13 SV12.
sultana@55596
  1310
   ((((bnd_less SV12 SV13 = False \<or>
sultana@55596
  1311
       bnd_less SV11 SV10 = False) \<or>
sultana@55596
  1312
      (SV14 = SV13) = False) \<or>
sultana@55596
  1313
     bnd_less SV12 SV14 = False) \<or>
sultana@55596
  1314
    bnd_less SV9 SV10 = True) \<or>
sultana@55596
  1315
   (SV9 = SV11) = False"
sultana@55596
  1316
(*
sultana@55596
  1317
apply (tactic {*
sultana@55596
  1318
  extcnf_combined_tac NONE
sultana@55596
  1319
   [ConstsDiff,
sultana@55596
  1320
    StripQuantifiers]
sultana@55596
  1321
   []*})
sultana@55596
  1322
*)
sultana@55596
  1323
(*
sultana@55596
  1324
apply (rule allI)+
sultana@55596
  1325
apply (erule_tac x = "SV12" in allE)
sultana@55596
  1326
apply (erule_tac x = "SV13" in allE)
sultana@55596
  1327
apply (erule_tac x = "SV14" in allE)
sultana@55596
  1328
apply (erule_tac x = "SV9" in allE)
sultana@55596
  1329
apply (erule_tac x = "SV10" in allE)
sultana@55596
  1330
apply (erule_tac x = "SV11" in allE)
sultana@55596
  1331
*)
sultana@55596
  1332
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "300") 1*})
sultana@55596
  1333
sultana@55596
  1334
sultana@55596
  1335
(*NUM667^1 node 302 -- dec*)
sultana@55596
  1336
lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
sultana@55596
  1337
       ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
sultana@55596
  1338
          (SV14 = SV13) = False) \<or>
sultana@55596
  1339
         bnd_less SV12 SV14 = False) \<or>
sultana@55596
  1340
        bnd_less SV9 SV10 = True) \<or>
sultana@55596
  1341
       (SV9 = SV11) =
sultana@55596
  1342
       False \<Longrightarrow>
sultana@55596
  1343
       \<forall>SV9 SV14 SV10 SV13 SV11 SV12.
sultana@55596
  1344
       (((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
sultana@55596
  1345
          (SV14 = SV13) = False) \<or>
sultana@55596
  1346
         bnd_less SV12 SV14 = False) \<or>
sultana@55596
  1347
        bnd_less SV9 SV10 = True) \<or>
sultana@55596
  1348
       (SV9 = SV11) =
sultana@55596
  1349
       False"
sultana@55596
  1350
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "302") 1*})
sultana@55596
  1351
*)
sultana@55596
  1352
sultana@55596
  1353
sultana@55596
  1354
(*
sultana@55596
  1355
(*CSR122^2*)
sultana@55596
  1356
     (* (Annotated_step ("23", "extuni_bool2"), *)
sultana@55596
  1357
lemma "(bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1358
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1359
           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1360
                  bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1361
               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1362
                  bnd_lBill_THFTYPE_i)) =
sultana@55596
  1363
          bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1364
           bnd_lBill_THFTYPE_i) =
sultana@55596
  1365
         False \<Longrightarrow>
sultana@55596
  1366
         bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1367
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1368
          (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1369
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1370
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1371
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1372
         True \<or>
sultana@55596
  1373
         bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1374
          bnd_lBill_THFTYPE_i =
sultana@55596
  1375
         True"
sultana@55596
  1376
(* apply (erule extuni_bool2) *)
sultana@55596
  1377
(* done *)
sultana@55596
  1378
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "23") 1*})
sultana@55596
  1379
sultana@55596
  1380
     (* (Annotated_step ("24", "extuni_bool1"), *)
sultana@55596
  1381
lemma "(bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1382
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1383
           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1384
                  bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1385
               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1386
                  bnd_lBill_THFTYPE_i)) =
sultana@55596
  1387
          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1388
           bnd_lBill_THFTYPE_i) =
sultana@55596
  1389
         False \<Longrightarrow>
sultana@55596
  1390
         bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1391
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1392
          (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1393
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1394
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1395
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1396
         False \<or>
sultana@55596
  1397
         bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1398
          bnd_lBill_THFTYPE_i =
sultana@55596
  1399
         False"
sultana@55596
  1400
(* apply (erule extuni_bool1) *)
sultana@55596
  1401
(* done *)
sultana@55596
  1402
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "24") 1*})
sultana@55596
  1403
sultana@55596
  1404
     (* (Annotated_step ("25", "extuni_bool2"), *)
sultana@55596
  1405
lemma "(bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1406
           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1407
           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1408
                  bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1409
               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1410
                  bnd_lBill_THFTYPE_i)) =
sultana@55596
  1411
          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1412
           bnd_lBill_THFTYPE_i) =
sultana@55596
  1413
         False \<Longrightarrow>
sultana@55596
  1414
         bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1415
          (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1416
          (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1417
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1418
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1419
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1420
         True \<or>
sultana@55596
  1421
         bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1422
          bnd_lBill_THFTYPE_i =
sultana@55596
  1423
         True"
sultana@55596
  1424
(* apply (erule extuni_bool2) *)
sultana@55596
  1425
(* done *)
sultana@55596
  1426
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "25") 1*})
sultana@55596
  1427
sultana@55596
  1428
     (* (Annotated_step ("26", "extuni_bool1"), *)
sultana@55596
  1429
lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1430
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1431
                 (\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1432
                        bnd_lMary_THFTYPE_i
sultana@55596
  1433
                        bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1434
                     \<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1435
                        bnd_lSue_THFTYPE_i
sultana@55596
  1436
                        bnd_lBill_THFTYPE_i)) =
sultana@55596
  1437
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
sultana@55596
  1438
               False \<Longrightarrow>
sultana@55596
  1439
         \<forall>SV2. bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1440
                (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1441
                (\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1442
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1443
                    \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1444
                       bnd_lBill_THFTYPE_i)) =
sultana@55596
  1445
               False \<or>
sultana@55596
  1446
               bnd_holdsDuring_THFTYPE_IiooI SV2 True = False"
sultana@55596
  1447
(* apply (rule allI, erule allE) *)
sultana@55596
  1448
(* apply (erule extuni_bool1) *)
sultana@55596
  1449
(* done *)
sultana@55596
  1450
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "26") 1*})
sultana@55596
  1451
sultana@55596
  1452
     (* (Annotated_step ("27", "extuni_bool2"), *)
sultana@55596
  1453
lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1454
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1455
                 (\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1456
                        bnd_lMary_THFTYPE_i
sultana@55596
  1457
                        bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1458
                     \<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1459
                        bnd_lSue_THFTYPE_i
sultana@55596
  1460
                        bnd_lBill_THFTYPE_i)) =
sultana@55596
  1461
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
sultana@55596
  1462
               False \<Longrightarrow>
sultana@55596
  1463
         \<forall>SV2. bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1464
                (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1465
                (\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1466
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1467
                    \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1468
                       bnd_lBill_THFTYPE_i)) =
sultana@55596
  1469
               True \<or>
sultana@55596
  1470
               bnd_holdsDuring_THFTYPE_IiooI SV2 True = True"
sultana@55596
  1471
(* apply (rule allI, erule allE) *)
sultana@55596
  1472
(* apply (erule extuni_bool2) *)
sultana@55596
  1473
(* done *)
sultana@55596
  1474
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "27") 1*})
sultana@55596
  1475
sultana@55596
  1476
     (* (Annotated_step ("30", "extuni_bool1"), *)
sultana@55596
  1477
lemma "((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1478
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1479
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1480
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1481
          True) =
sultana@55596
  1482
         False \<Longrightarrow>
sultana@55596
  1483
         (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1484
                bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1485
             \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1486
                bnd_lBill_THFTYPE_i)) =
sultana@55596
  1487
         False \<or>
sultana@55596
  1488
         True = False"
sultana@55596
  1489
(* apply (erule extuni_bool1) *)
sultana@55596
  1490
(* done *)
sultana@55596
  1491
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "30") 1*})
sultana@55596
  1492
sultana@55596
  1493
     (* (Annotated_step ("29", "extuni_bind"), *)
sultana@55596
  1494
lemma "(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
sultana@55596
  1495
          bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) =
sultana@55596
  1496
         False \<or>
sultana@55596
  1497
         ((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1498
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1499
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1500
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1501
          True) =
sultana@55596
  1502
         False \<Longrightarrow>
sultana@55596
  1503
         ((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
sultana@55596
  1504
                 bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1505
              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1506
                 bnd_lBill_THFTYPE_i)) =
sultana@55596
  1507
          True) =
sultana@55596
  1508
         False"
sultana@55596
  1509
(* apply (tactic {*break_hypotheses 1*}) *)
sultana@55596
  1510
(* apply (erule extuni_bind) *)
sultana@55596
  1511
(* apply (tactic {*clause_breaker 1*}) *)
sultana@55596
  1512
(* done *)
sultana@55596
  1513
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "29") 1*})
sultana@55596
  1514
sultana@55596
  1515
     (* (Annotated_step ("28", "extuni_dec"), *)
sultana@55596
  1516
lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
sultana@55596
  1517
                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
sultana@55596
  1518
                 (\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1519
                        bnd_lMary_THFTYPE_i
sultana@55596
  1520
                        bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1521
                     \<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1522
                        bnd_lSue_THFTYPE_i
sultana@55596
  1523
                        bnd_lBill_THFTYPE_i)) =
sultana@55596
  1524
                bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
sultana@55596
  1525
               False \<Longrightarrow>
sultana@55596
  1526
         \<forall>SV2. (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
sultana@55596
  1527
                SV2) =
sultana@55596
  1528
               False \<or>
sultana@55596
  1529
               ((\<not> (\<not> bnd_likes_THFTYPE_IiioI
sultana@55596
  1530
                       bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
sultana@55596
  1531
                    \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
sultana@55596
  1532
                       bnd_lBill_THFTYPE_i)) =
sultana@55596
  1533
                True) =
sultana@55596
  1534
               False"
sultana@55596
  1535
(* apply (rule allI) *)
sultana@55596
  1536
(* apply (erule_tac x = "SV2" in allE) *)
sultana@55596
  1537
(* apply (erule extuni_dec_2) *)
sultana@55596
  1538
(* done *)
sultana@55596
  1539
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "28") 1*})
sultana@55596
  1540
*)
sultana@55596
  1541
sultana@55596
  1542
(* QUA002^1
sultana@55596
  1543
   (* [[(Annotated_step ("49", "extuni_dec"), *)
sultana@55596
  1544
lemma "((bnd_sK3_E = bnd_sK1_X1 \<or> bnd_sK3_E = bnd_sK2_X2) =
sultana@55596
  1545
          (bnd_sK3_E = bnd_sK2_X2 \<or> bnd_sK3_E = bnd_sK1_X1)) =
sultana@55596
  1546
         False \<Longrightarrow>
sultana@55596
  1547
         ((bnd_sK3_E = bnd_sK2_X2) = (bnd_sK3_E = bnd_sK2_X2)) =
sultana@55596
  1548
         False \<or>
sultana@55596
  1549
         ((bnd_sK3_E = bnd_sK1_X1) = (bnd_sK3_E = bnd_sK1_X1)) =
sultana@55596
  1550
         False"
sultana@55596
  1551
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "49") 1*})
sultana@55596
  1552
sultana@55596
  1553
     (* (Annotated_step ("20", "unfold_def"), *)
sultana@55596
  1554
lemma "(bnd_addition bnd_sK1_X1 bnd_sK2_X2 \<noteq>
sultana@55596
  1555
          bnd_addition bnd_sK2_X2 bnd_sK1_X1) =
sultana@55596
  1556
         True \<Longrightarrow>
sultana@55596
  1557
         (bnd_sup
wenzelm@61076
  1558
           (\<lambda>SX0::TPTP_Interpret.ind.
sultana@55596
  1559
               SX0 = bnd_sK1_X1 \<or> SX0 = bnd_sK2_X2) \<noteq>
sultana@55596
  1560
          bnd_sup
wenzelm@61076
  1561
           (\<lambda>SX0::TPTP_Interpret.ind.
sultana@55596
  1562
               SX0 = bnd_sK2_X2 \<or> SX0 = bnd_sK1_X1)) =
sultana@55596
  1563
         True"
sultana@55596
  1564
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "20") 1*})
sultana@55596
  1565
*)
sultana@55596
  1566
sultana@55596
  1567
(*
sultana@55596
  1568
(*SEU620^2*)
sultana@55596
  1569
     (* (Annotated_step ("11", "unfold_def"), *)
sultana@55596
  1570
lemma "bnd_kpairiskpair =
sultana@55596
  1571
         (\<forall>Xx Xy.
sultana@55596
  1572
             bnd_iskpair
sultana@55596
  1573
              (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1574
                (bnd_setadjoin
sultana@55596
  1575
                  (bnd_setadjoin Xx
sultana@55596
  1576
                    (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1577
                  bnd_emptyset))) \<and>
sultana@55596
  1578
         bnd_kpair =
sultana@55596
  1579
         (\<lambda>Xx Xy.
sultana@55596
  1580
             bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1581
              (bnd_setadjoin
sultana@55596
  1582
                (bnd_setadjoin Xx
sultana@55596
  1583
                  (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1584
                bnd_emptyset)) \<and>
sultana@55596
  1585
         bnd_iskpair =
sultana@55596
  1586
         (\<lambda>A. \<exists>Xx. bnd_in Xx (bnd_setunion A) \<and>
sultana@55596
  1587
                   (\<exists>Xy. bnd_in Xy (bnd_setunion A) \<and>
sultana@55596
  1588
                         A =
sultana@55596
  1589
                         bnd_setadjoin
sultana@55596
  1590
                          (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1591
                          (bnd_setadjoin
sultana@55596
  1592
                            (bnd_setadjoin Xx
sultana@55596
  1593
                              (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1594
                            bnd_emptyset))) \<and>
sultana@55596
  1595
         (\<forall>SY5 SY6.
sultana@55596
  1596
             (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1597
               (bnd_setadjoin
sultana@55596
  1598
                 (bnd_setadjoin SY5
sultana@55596
  1599
                   (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1600
                 bnd_emptyset) =
sultana@55596
  1601
              bnd_setadjoin
sultana@55596
  1602
               (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
sultana@55596
  1603
               (bnd_setadjoin
sultana@55596
  1604
                 (bnd_setadjoin (bnd_sK3 SY6 SY5)
sultana@55596
  1605
                   (bnd_setadjoin (bnd_sK4 SY6 SY5)
sultana@55596
  1606
                     bnd_emptyset))
sultana@55596
  1607
                 bnd_emptyset) \<and>
sultana@55596
  1608
              bnd_in (bnd_sK4 SY6 SY5)
sultana@55596
  1609
               (bnd_setunion
sultana@55596
  1610
                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1611
                   (bnd_setadjoin
sultana@55596
  1612
                     (bnd_setadjoin SY5
sultana@55596
  1613
                       (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1614
                     bnd_emptyset)))) \<and>
sultana@55596
  1615
             bnd_in (bnd_sK3 SY6 SY5)
sultana@55596
  1616
              (bnd_setunion
sultana@55596
  1617
                (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1618
                  (bnd_setadjoin
sultana@55596
  1619
                    (bnd_setadjoin SY5
sultana@55596
  1620
                      (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1621
                    bnd_emptyset)))) =
sultana@55596
  1622
         True \<Longrightarrow>
sultana@55596
  1623
         (\<forall>SX0 SX1.
sultana@55596
  1624
             \<not> (\<not> \<not> (bnd_setadjoin
sultana@55596
  1625
                      (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
  1626
                      (bnd_setadjoin
sultana@55596
  1627
                        (bnd_setadjoin SX0
sultana@55596
  1628
                          (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
  1629
                        bnd_emptyset) \<noteq>
sultana@55596
  1630
                     bnd_setadjoin
sultana@55596
  1631
                      (bnd_setadjoin (bnd_sK3 SX1 SX0)
sultana@55596
  1632
                        bnd_emptyset)
sultana@55596
  1633
                      (bnd_setadjoin
sultana@55596
  1634
                        (bnd_setadjoin (bnd_sK3 SX1 SX0)
sultana@55596
  1635
                          (bnd_setadjoin (bnd_sK4 SX1 SX0)
sultana@55596
  1636
                            bnd_emptyset))
sultana@55596
  1637
                        bnd_emptyset) \<or>
sultana@55596
  1638
                     \<not> bnd_in (bnd_sK4 SX1 SX0)
sultana@55596
  1639
                        (bnd_setunion
sultana@55596
  1640
                          (bnd_setadjoin
sultana@55596
  1641
                            (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
  1642
                            (bnd_setadjoin
sultana@55596
  1643
                              (bnd_setadjoin SX0
sultana@55596
  1644
(bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
  1645
                              bnd_emptyset)))) \<or>
sultana@55596
  1646
                \<not> bnd_in (bnd_sK3 SX1 SX0)
sultana@55596
  1647
                   (bnd_setunion
sultana@55596
  1648
                     (bnd_setadjoin
sultana@55596
  1649
                       (bnd_setadjoin SX0 bnd_emptyset)
sultana@55596
  1650
                       (bnd_setadjoin
sultana@55596
  1651
                         (bnd_setadjoin SX0
sultana@55596
  1652
                           (bnd_setadjoin SX1 bnd_emptyset))
sultana@55596
  1653
                         bnd_emptyset))))) =
sultana@55596
  1654
         True"
sultana@55596
  1655
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
sultana@55596
  1656
sultana@55596
  1657
     (* (Annotated_step ("3", "unfold_def"), *)
sultana@55596
  1658
lemma "bnd_kpairiskpair =
sultana@55596
  1659
         (\<forall>Xx Xy.
sultana@55596
  1660
             bnd_iskpair
sultana@55596
  1661
              (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1662
                (bnd_setadjoin
sultana@55596
  1663
                  (bnd_setadjoin Xx
sultana@55596
  1664
                    (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1665
                  bnd_emptyset))) \<and>
sultana@55596
  1666
         bnd_kpair =
sultana@55596
  1667
         (\<lambda>Xx Xy.
sultana@55596
  1668
             bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1669
              (bnd_setadjoin
sultana@55596
  1670
                (bnd_setadjoin Xx
sultana@55596
  1671
                  (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1672
                bnd_emptyset)) \<and>
sultana@55596
  1673
         bnd_iskpair =
sultana@55596
  1674
         (\<lambda>A. \<exists>Xx. bnd_in Xx (bnd_setunion A) \<and>
sultana@55596
  1675
                   (\<exists>Xy. bnd_in Xy (bnd_setunion A) \<and>
sultana@55596
  1676
                         A =
sultana@55596
  1677
                         bnd_setadjoin
sultana@55596
  1678
                          (bnd_setadjoin Xx bnd_emptyset)
sultana@55596
  1679
                          (bnd_setadjoin
sultana@55596
  1680
                            (bnd_setadjoin Xx
sultana@55596
  1681
                              (bnd_setadjoin Xy bnd_emptyset))
sultana@55596
  1682
                            bnd_emptyset))) \<and>
sultana@55596
  1683
         (bnd_kpairiskpair \<longrightarrow>
sultana@55596
  1684
          (\<forall>Xx Xy. bnd_iskpair (bnd_kpair Xx Xy))) =
sultana@55596
  1685
         False \<Longrightarrow>
sultana@55596
  1686
         ((\<forall>SY5 SY6.
sultana@55596
  1687
              \<exists>SY7. bnd_in SY7
sultana@55596
  1688
                     (bnd_setunion
sultana@55596
  1689
                       (bnd_setadjoin
sultana@55596
  1690
                         (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1691
                         (bnd_setadjoin
sultana@55596
  1692
                           (bnd_setadjoin SY5
sultana@55596
  1693
                             (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1694
                           bnd_emptyset))) \<and>
sultana@55596
  1695
                    (\<exists>SY8. bnd_in SY8
sultana@55596
  1696
                            (bnd_setunion
sultana@55596
  1697
                              (bnd_setadjoin
sultana@55596
  1698
(bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1699
(bnd_setadjoin
sultana@55596
  1700
  (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1701
  bnd_emptyset))) \<and>
sultana@55596
  1702
                           bnd_setadjoin
sultana@55596
  1703
                            (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1704
                            (bnd_setadjoin
sultana@55596
  1705
                              (bnd_setadjoin SY5
sultana@55596
  1706
(bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1707
                              bnd_emptyset) =
sultana@55596
  1708
                           bnd_setadjoin
sultana@55596
  1709
                            (bnd_setadjoin SY7 bnd_emptyset)
sultana@55596
  1710
                            (bnd_setadjoin
sultana@55596
  1711
                              (bnd_setadjoin SY7
sultana@55596
  1712
(bnd_setadjoin SY8 bnd_emptyset))
sultana@55596
  1713
                              bnd_emptyset))) \<longrightarrow>
sultana@55596
  1714
          (\<forall>SY0 SY1.
sultana@55596
  1715
              \<exists>SY3. bnd_in SY3
sultana@55596
  1716
                     (bnd_setunion
sultana@55596
  1717
                       (bnd_setadjoin
sultana@55596
  1718
                         (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1719
                         (bnd_setadjoin
sultana@55596
  1720
                           (bnd_setadjoin SY0
sultana@55596
  1721
                             (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1722
                           bnd_emptyset))) \<and>
sultana@55596
  1723
                    (\<exists>SY4. bnd_in SY4
sultana@55596
  1724
                            (bnd_setunion
sultana@55596
  1725
                              (bnd_setadjoin
sultana@55596
  1726
(bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1727
(bnd_setadjoin
sultana@55596
  1728
  (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1729
  bnd_emptyset))) \<and>
sultana@55596
  1730
                           bnd_setadjoin
sultana@55596
  1731
                            (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1732
                            (bnd_setadjoin
sultana@55596
  1733
                              (bnd_setadjoin SY0
sultana@55596
  1734
(bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1735
                              bnd_emptyset) =
sultana@55596
  1736
                           bnd_setadjoin
sultana@55596
  1737
                            (bnd_setadjoin SY3 bnd_emptyset)
sultana@55596
  1738
                            (bnd_setadjoin
sultana@55596
  1739
                              (bnd_setadjoin SY3
sultana@55596
  1740
(bnd_setadjoin SY4 bnd_emptyset))
sultana@55596
  1741
                              bnd_emptyset)))) =
sultana@55596
  1742
         False"
sultana@55596
  1743
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "3") 1*})
sultana@55596
  1744
sultana@55596
  1745
     (* (Annotated_step ("8", "extcnf_combined"), *)
sultana@55596
  1746
lemma "(\<forall>SY5 SY6.
sultana@55596
  1747
             \<exists>SY7. bnd_in SY7
sultana@55596
  1748
                    (bnd_setunion
sultana@55596
  1749
                      (bnd_setadjoin
sultana@55596
  1750
                        (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1751
                        (bnd_setadjoin
sultana@55596
  1752
                          (bnd_setadjoin SY5
sultana@55596
  1753
                            (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1754
                          bnd_emptyset))) \<and>
sultana@55596
  1755
                   (\<exists>SY8. bnd_in SY8
sultana@55596
  1756
                           (bnd_setunion
sultana@55596
  1757
                             (bnd_setadjoin
sultana@55596
  1758
                               (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1759
                               (bnd_setadjoin
sultana@55596
  1760
 (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1761
 bnd_emptyset))) \<and>
sultana@55596
  1762
                          bnd_setadjoin
sultana@55596
  1763
                           (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1764
                           (bnd_setadjoin
sultana@55596
  1765
                             (bnd_setadjoin SY5
sultana@55596
  1766
                               (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1767
                             bnd_emptyset) =
sultana@55596
  1768
                          bnd_setadjoin
sultana@55596
  1769
                           (bnd_setadjoin SY7 bnd_emptyset)
sultana@55596
  1770
                           (bnd_setadjoin
sultana@55596
  1771
                             (bnd_setadjoin SY7
sultana@55596
  1772
                               (bnd_setadjoin SY8 bnd_emptyset))
sultana@55596
  1773
                             bnd_emptyset))) =
sultana@55596
  1774
         True \<Longrightarrow>
sultana@55596
  1775
         (\<forall>SY5 SY6.
sultana@55596
  1776
             (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1777
               (bnd_setadjoin
sultana@55596
  1778
                 (bnd_setadjoin SY5
sultana@55596
  1779
                   (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1780
                 bnd_emptyset) =
sultana@55596
  1781
              bnd_setadjoin
sultana@55596
  1782
               (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
sultana@55596
  1783
               (bnd_setadjoin
sultana@55596
  1784
                 (bnd_setadjoin (bnd_sK3 SY6 SY5)
sultana@55596
  1785
                   (bnd_setadjoin (bnd_sK4 SY6 SY5)
sultana@55596
  1786
                     bnd_emptyset))
sultana@55596
  1787
                 bnd_emptyset) \<and>
sultana@55596
  1788
              bnd_in (bnd_sK4 SY6 SY5)
sultana@55596
  1789
               (bnd_setunion
sultana@55596
  1790
                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1791
                   (bnd_setadjoin
sultana@55596
  1792
                     (bnd_setadjoin SY5
sultana@55596
  1793
                       (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1794
                     bnd_emptyset)))) \<and>
sultana@55596
  1795
             bnd_in (bnd_sK3 SY6 SY5)
sultana@55596
  1796
              (bnd_setunion
sultana@55596
  1797
                (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
sultana@55596
  1798
                  (bnd_setadjoin
sultana@55596
  1799
                    (bnd_setadjoin SY5
sultana@55596
  1800
                      (bnd_setadjoin SY6 bnd_emptyset))
sultana@55596
  1801
                    bnd_emptyset)))) =
sultana@55596
  1802
         True"
sultana@55596
  1803
by (tactic {*
sultana@55596
  1804
HEADGOAL (extcnf_combined_tac Full false (hd prob_names))
sultana@55596
  1805
*})
sultana@55596
  1806
sultana@55596
  1807
     (* (Annotated_step ("7", "extcnf_combined"), *)
sultana@55596
  1808
lemma "(\<not> (\<forall>SY0 SY1.
sultana@55596
  1809
                \<exists>SY3. bnd_in SY3
sultana@55596
  1810
                       (bnd_setunion
sultana@55596
  1811
                         (bnd_setadjoin
sultana@55596
  1812
                           (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1813
                           (bnd_setadjoin
sultana@55596
  1814
                             (bnd_setadjoin SY0
sultana@55596
  1815
                               (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1816
                             bnd_emptyset))) \<and>
sultana@55596
  1817
                      (\<exists>SY4. bnd_in SY4
sultana@55596
  1818
                              (bnd_setunion
sultana@55596
  1819
(bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1820
  (bnd_setadjoin
sultana@55596
  1821
    (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1822
    bnd_emptyset))) \<and>
sultana@55596
  1823
                             bnd_setadjoin
sultana@55596
  1824
                              (bnd_setadjoin SY0 bnd_emptyset)
sultana@55596
  1825
                              (bnd_setadjoin
sultana@55596
  1826
(bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
sultana@55596
  1827
bnd_emptyset) =
sultana@55596
  1828
                             bnd_setadjoin
sultana@55596
  1829
                              (bnd_setadjoin SY3 bnd_emptyset)
sultana@55596
  1830
                              (bnd_setadjoin
sultana@55596
  1831
(bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
sultana@55596
  1832
bnd_emptyset)))) =
sultana@55596
  1833
         True \<Longrightarrow>
sultana@55596
  1834
         (\<forall>SY24.
sultana@55596
  1835
             (\<forall>SY25.
sultana@55596
  1836
                 bnd_setadjoin
sultana@55596
  1837
                  (bnd_setadjoin bnd_sK1 bnd_emptyset)
sultana@55596
  1838
                  (bnd_setadjoin
sultana@55596
  1839
                    (bnd_setadjoin bnd_sK1
sultana@55596
  1840
                      (bnd_setadjoin bnd_sK2 bnd_emptyset))
sultana@55596
  1841
                    bnd_emptyset) \<noteq>
sultana@55596
  1842
                 bnd_setadjoin (bnd_setadjoin SY24 bnd_emptyset)
sultana@55596
  1843
                  (bnd_setadjoin
sultana@55596
  1844
                    (bnd_setadjoin SY24
sultana@55596
  1845
                      (bnd_setadjoin SY25 bnd_emptyset))
sultana@55596
  1846
                    bnd_emptyset) \<or>
sultana@55596
  1847
                 \<not> bnd_in SY25
sultana@55596
  1848
                    (bnd_setunion
sultana@55596
  1849
                      (bnd_setadjoin
sultana@55596
  1850
                        (bnd_setadjoin bnd_sK1 bnd_emptyset)
sultana@55596
  1851
                        (bnd_setadjoin
sultana@55596
  1852
                          (bnd_setadjoin bnd_sK1
sultana@55596
  1853
                            (bnd_setadjoin bnd_sK2
sultana@55596
  1854
                              bnd_emptyset))
sultana@55596
  1855
                          bnd_emptyset)))) \<or>
sultana@55596
  1856
             \<not> bnd_in SY24
sultana@55596
  1857
                (bnd_setunion
sultana@55596
  1858
                  (bnd_setadjoin
sultana@55596
  1859
                    (bnd_setadjoin bnd_sK1 bnd_emptyset)
sultana@55596
  1860
                    (bnd_setadjoin
sultana@55596
  1861
                      (bnd_setadjoin bnd_sK1
sultana@55596
  1862
                        (bnd_setadjoin bnd_sK2 bnd_emptyset))
sultana@55596
  1863
                      bnd_emptyset)))) =
sultana@55596
  1864
         True"
sultana@55596
  1865
by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
sultana@55596
  1866
*)
sultana@55596
  1867
sultana@55596
  1868
(*PUZ081^2*)
sultana@55596
  1869
(*
sultana@55596
  1870
     (* (Annotated_step ("9", "unfold_def"), *)
sultana@55596
  1871
lemma "bnd_says bnd_mel
sultana@55596
  1872
          (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) \<Longrightarrow>
sultana@55596
  1873
         bnd_says bnd_mel
sultana@55596
  1874
          (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) =
sultana@55596
  1875
         True"
sultana@55596
  1876
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
sultana@55596
  1877
sultana@55596
  1878
     (* (Annotated_step ("10", "unfold_def"), *)
sultana@55596
  1879
lemma "bnd_says bnd_zoey (bnd_knave bnd_mel) \<Longrightarrow>
sultana@55596
  1880
         bnd_says bnd_zoey (bnd_knave bnd_mel) = True"
sultana@55596
  1881
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})
sultana@55596
  1882
sultana@55596
  1883
     (* (Annotated_step ("11", "unfold_def"), *)
sultana@55596
  1884
lemma "\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S \<Longrightarrow>
sultana@55596
  1885
         (\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S) = True"
sultana@55596
  1886
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
sultana@55596
  1887
sultana@55596
  1888
     (* (Annotated_step ("12", "unfold_def"), *)
sultana@55596
  1889
lemma "\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S \<Longrightarrow>
sultana@55596
  1890
         (\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S) = True"
sultana@55596
  1891
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})
sultana@55596
  1892
sultana@55596
  1893
     (* (Annotated_step ("13", "unfold_def"), *)
sultana@55596
  1894
lemma "\<forall>P. bnd_knight P \<noteq> bnd_knave P \<Longrightarrow>
sultana@55596
  1895
         (\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True"
sultana@55596
  1896
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "13") 1*})
sultana@55596
  1897
sultana@55596
  1898
     (* (Annotated_step ("15", "extcnf_combined"), *)
sultana@55596
  1899
lemma "(\<not> (\<exists>TZ TM. TZ bnd_zoey \<and> TM bnd_mel)) = True \<Longrightarrow>
sultana@55596
  1900
         ((\<forall>TM. \<not> TM bnd_mel) \<or> (\<forall>TZ. \<not> TZ bnd_zoey)) = True"
sultana@55596
  1901
by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})
sultana@55596
  1902
sultana@55596
  1903
     (* (Annotated_step ("18", "extcnf_combined"), *)
sultana@55596
  1904
lemma "(\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True \<Longrightarrow>
sultana@55596
  1905
         ((\<forall>P. \<not> bnd_knave P \<or> \<not> bnd_knight P) \<and>
sultana@55596
  1906
          (\<forall>P. bnd_knave P \<or> bnd_knight P)) =
sultana@55596
  1907
         True"
sultana@55596
  1908
by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})
sultana@55596
  1909
*)
sultana@55596
  1910
sultana@55596
  1911
(*
sultana@55596
  1912
(*from SEU667^2.p.out*)
sultana@55596
  1913
     (* (Annotated_step ("10", "unfold_def"), *)
sultana@55596
  1914
lemma "bnd_dpsetconstrSub =
sultana@55596
  1915
         (\<forall>A B Xphi.
sultana@55596
  1916
             bnd_subset (bnd_dpsetconstr A B Xphi)
sultana@55596
  1917
              (bnd_cartprod A B)) \<and>
sultana@55596
  1918
         bnd_dpsetconstr =
sultana@55596
  1919
         (\<lambda>A B Xphi.
sultana@55596
  1920
             bnd_dsetconstr (bnd_cartprod A B)
sultana@55596
  1921
              (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
sultana@55596
  1922
                         (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
sultana@55596
  1923
                               Xu = bnd_kpair Xx Xy))) \<and>
sultana@55596
  1924
         bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
sultana@55596
  1925
         (\<not> bnd_subset
sultana@55596
  1926
             (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
sultana@55596
  1927
               (\<lambda>SY66.
sultana@55596
  1928
                   \<exists>SY67.
sultana@55596
  1929
                      bnd_in SY67 bnd_sK1 \<and>
sultana@55596
  1930
                      (\<exists>SY68.
sultana@55596
  1931
                          (bnd_in SY68 bnd_sK2 \<and>
sultana@55596
  1932
                           bnd_sK3 SY67 SY68) \<and>
sultana@55596
  1933
                          SY66 = bnd_kpair SY67 SY68)))
sultana@55596
  1934
             (bnd_cartprod bnd_sK1 bnd_sK2)) =
sultana@55596
  1935
         True \<Longrightarrow>
sultana@55596
  1936
         (\<not> bnd_subset
sultana@55596
  1937
             (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
sultana@55596
  1938
               (\<lambda>SX0. \<not> (\<forall>SX1. \<not> \<not> (\<not> bnd_in SX1 bnd_sK1 \<or>
sultana@55596
  1939
    \<not> \<not> (\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX2 bnd_sK2 \<or>
sultana@55596
  1940
                         \<not> bnd_sK3 SX1 SX2) \<or>
sultana@55596
  1941
                    SX0 \<noteq> bnd_kpair SX1 SX2))))))
sultana@55596
  1942
             (bnd_cartprod bnd_sK1 bnd_sK2)) =
sultana@55596
  1943
         True"
sultana@55596
  1944
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})
sultana@55596
  1945
sultana@55596
  1946
sultana@55596
  1947
     (* (Annotated_step ("11", "unfold_def"), *)
sultana@55596
  1948
lemma "bnd_dpsetconstrSub =
sultana@55596
  1949
         (\<forall>A B Xphi.
sultana@55596
  1950
             bnd_subset (bnd_dpsetconstr A B Xphi)
sultana@55596
  1951
              (bnd_cartprod A B)) \<and>
sultana@55596
  1952
         bnd_dpsetconstr =
sultana@55596
  1953
         (\<lambda>A B Xphi.
sultana@55596
  1954
             bnd_dsetconstr (bnd_cartprod A B)
sultana@55596
  1955
              (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
sultana@55596
  1956
                         (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
sultana@55596
  1957
                               Xu = bnd_kpair Xx Xy))) \<and>
sultana@55596
  1958
         bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
sultana@55596
  1959
         (\<forall>SY21 SY22 SY23.
sultana@55596
  1960
             bnd_subset
sultana@55596
  1961
              (bnd_dsetconstr (bnd_cartprod SY21 SY22)
sultana@55596
  1962
                (\<lambda>SY35.
sultana@55596
  1963
                    \<exists>SY36.
sultana@55596
  1964
                       bnd_in SY36 SY21 \<and>
sultana@55596
  1965
                       (\<exists>SY37.
sultana@55596
  1966
                           (bnd_in SY37 SY22 \<and> SY23 SY36 SY37) \<and>
sultana@55596
  1967
                           SY35 = bnd_kpair SY36 SY37)))
sultana@55596
  1968
              (bnd_cartprod SY21 SY22)) =
sultana@55596
  1969
         True \<Longrightarrow>
sultana@55596
  1970
         (\<forall>SX0 SX1 SX2.
sultana@55596
  1971
             bnd_subset
sultana@55596
  1972
              (bnd_dsetconstr (bnd_cartprod SX0 SX1)
sultana@55596
  1973
                (\<lambda>SX3. \<not> (\<forall>SX4. \<not> \<not> (\<not> bnd_in SX4 SX0 \<or>
sultana@55596
  1974
     \<not> \<not> (\<forall>SX5. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX5 SX1 \<or> \<not> SX2 SX4 SX5) \<or>
sultana@55596
  1975
                     SX3 \<noteq> bnd_kpair SX4 SX5))))))
sultana@55596
  1976
              (bnd_cartprod SX0 SX1)) =
sultana@55596
  1977
         True"
sultana@55596
  1978
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
sultana@55596
  1979
*)
sultana@55596
  1980
sultana@55596
  1981
(*
sultana@55596
  1982
(*from ALG001^5*)
sultana@55596
  1983
      (* (Annotated_step ("4", "extcnf_forall_neg"), *)
sultana@55596
  1984
lemma "(\<forall>(Xh1 :: bnd_g \<Rightarrow> bnd_b) (Xh2 :: bnd_b \<Rightarrow> bnd_a) (Xf1 :: bnd_g \<Rightarrow> bnd_g \<Rightarrow> bnd_g) (Xf2 :: bnd_b \<Rightarrow> bnd_b \<Rightarrow> bnd_b) (Xf3 :: bnd_a \<Rightarrow> bnd_a \<Rightarrow> bnd_a).
sultana@55596
  1985
             (\<forall>Xx Xy. Xh1 (Xf1 Xx Xy) = Xf2 (Xh1 Xx) (Xh1 Xy)) \<and>
sultana@55596
  1986
             (\<forall>Xx Xy.
sultana@55596
  1987
                 Xh2 (Xf2 Xx Xy) = Xf3 (Xh2 Xx) (Xh2 Xy)) \<longrightarrow>
sultana@55596
  1988
             (\<forall>Xx Xy.
sultana@55596
  1989
                 Xh2 (Xh1 (Xf1 Xx Xy)) =
sultana@55596
  1990
                 Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy)))) =
sultana@55596
  1991
         False \<Longrightarrow>
sultana@55596
  1992
         ((\<forall>SY35 SY36.
sultana@55596
  1993
              bnd_sK1 (bnd_sK3 SY35 SY36) =
sultana@55596
  1994
              bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) \<and>
sultana@55596
  1995
          (\<forall>SY31 SY32.
sultana@55596
  1996
              bnd_sK2 (bnd_sK4 SY31 SY32) =
sultana@55596
  1997
              bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) \<longrightarrow>
sultana@55596
  1998
          (\<forall>SY39 SY40.
sultana@55596
  1999
              bnd_sK2 (bnd_sK1 (bnd_sK3 SY39 SY40)) =
sultana@55596
  2000
              bnd_sK5 (bnd_sK2 (bnd_sK1 SY39))
sultana@55596
  2001
               (bnd_sK2 (bnd_sK1 SY40)))) =
sultana@55596
  2002
         False"
sultana@55596
  2003
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "4") 1*})
sultana@55596
  2004
*)
sultana@55596
  2005
sultana@55596
  2006
(*SYN044^4*)
sultana@55596
  2007
(*
wenzelm@56281
  2008
declare [[ML_print_depth = 1400]]
sultana@55596
  2009
(* the_tactics *)
sultana@55596
  2010
*}
sultana@55596
  2011
sultana@55596
  2012
     (* (Annotated_step ("12", "unfold_def"), *)
sultana@55596
  2013
lemma "bnd_mor =
wenzelm@61076
  2014
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2015
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2016
             X U \<or> Y U) \<and>
sultana@55596
  2017
         bnd_mnot =
wenzelm@61076
  2018
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2019
             \<not> X U) \<and>
sultana@55596
  2020
         bnd_mimplies =
wenzelm@61076
  2021
         (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
sultana@55596
  2022
         bnd_mbox_s4 =
wenzelm@61076
  2023
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
wenzelm@61076
  2024
             \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
sultana@55596
  2025
         bnd_mand =
wenzelm@61076
  2026
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2027
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2028
             X U \<and> Y U) \<and>
sultana@55596
  2029
         bnd_ixor =
wenzelm@61076
  2030
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2031
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2032
             bnd_inot (bnd_iequiv P Q)) \<and>
sultana@55596
  2033
         bnd_ivalid = All \<and>
wenzelm@61076
  2034
         bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
sultana@55596
  2035
         bnd_isatisfiable = Ex \<and>
sultana@55596
  2036
         bnd_ior =
wenzelm@61076
  2037
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2038
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2039
             bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
sultana@55596
  2040
         bnd_inot =
wenzelm@61076
  2041
         (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2042
             bnd_mnot (bnd_mbox_s4 P)) \<and>
sultana@55596
  2043
         bnd_iinvalid =
wenzelm@61076
  2044
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
  2045
             \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
sultana@55596
  2046
         bnd_iimplies =
wenzelm@61076
  2047
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2048
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2049
             bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
sultana@55596
  2050
         bnd_iimplied =
wenzelm@61076
  2051
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2052
             Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
sultana@55596
  2053
         bnd_ifalse = bnd_inot bnd_itrue \<and>
sultana@55596
  2054
         bnd_iequiv =
wenzelm@61076
  2055
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2056
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2057
             bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
sultana@55596
  2058
         bnd_icountersatisfiable =
wenzelm@61076
  2059
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
  2060
             \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
wenzelm@61076
  2061
         bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
sultana@55596
  2062
         bnd_iand = bnd_mand \<and>
wenzelm@61076
  2063
         (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
wenzelm@61076
  2064
             Z::TPTP_Interpret.ind.
sultana@55596
  2065
             bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) \<Longrightarrow>
wenzelm@61076
  2066
         (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
wenzelm@61076
  2067
             Z::TPTP_Interpret.ind.
sultana@55596
  2068
             bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) =
sultana@55596
  2069
         True"
sultana@55596
  2070
(* by (tactic {*tectoc @{context}*}) *)
sultana@55596
  2071
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})
sultana@55596
  2072
sultana@55596
  2073
     (* (Annotated_step ("11", "unfold_def"), *)
sultana@55596
  2074
lemma "bnd_mor =
wenzelm@61076
  2075
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2076
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2077
             X U \<or> Y U) \<and>
sultana@55596
  2078
         bnd_mnot =
wenzelm@61076
  2079
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2080
             \<not> X U) \<and>
sultana@55596
  2081
         bnd_mimplies =
wenzelm@61076
  2082
         (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
sultana@55596
  2083
         bnd_mbox_s4 =
wenzelm@61076
  2084
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
wenzelm@61076
  2085
             \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
sultana@55596
  2086
         bnd_mand =
wenzelm@61076
  2087
         (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2088
             (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
sultana@55596
  2089
             X U \<and> Y U) \<and>
sultana@55596
  2090
         bnd_ixor =
wenzelm@61076
  2091
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2092
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2093
             bnd_inot (bnd_iequiv P Q)) \<and>
sultana@55596
  2094
         bnd_ivalid = All \<and>
wenzelm@61076
  2095
         bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
sultana@55596
  2096
         bnd_isatisfiable = Ex \<and>
sultana@55596
  2097
         bnd_ior =
wenzelm@61076
  2098
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2099
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2100
             bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
sultana@55596
  2101
         bnd_inot =
wenzelm@61076
  2102
         (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2103
             bnd_mnot (bnd_mbox_s4 P)) \<and>
sultana@55596
  2104
         bnd_iinvalid =
wenzelm@61076
  2105
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
  2106
             \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
sultana@55596
  2107
         bnd_iimplies =
wenzelm@61076
  2108
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2109
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2110
             bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
sultana@55596
  2111
         bnd_iimplied =
wenzelm@61076
  2112
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2113
             Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
sultana@55596
  2114
         bnd_ifalse = bnd_inot bnd_itrue \<and>
sultana@55596
  2115
         bnd_iequiv =
wenzelm@61076
  2116
         (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
wenzelm@61076
  2117
             Q::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2118
             bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
sultana@55596
  2119
         bnd_icountersatisfiable =
wenzelm@61076
  2120
         (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
  2121
             \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
wenzelm@61076
  2122
         bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
sultana@55596
  2123
         bnd_iand = bnd_mand \<and>
sultana@55596
  2124
         bnd_ivalid
sultana@55596
  2125
          (bnd_iimplies (bnd_iatom bnd_q) (bnd_iatom bnd_r)) \<Longrightarrow>
wenzelm@61076
  2126
         (\<forall>SY161::TPTP_Interpret.ind.
wenzelm@61076
  2127
             \<not> (\<forall>SY162::TPTP_Interpret.ind.
sultana@55596
  2128
                   bnd_irel SY161 SY162 \<longrightarrow> bnd_q SY162) \<or>
wenzelm@61076
  2129
             (\<forall>SY163::TPTP_Interpret.ind.
sultana@55596
  2130
                 bnd_irel SY161 SY163 \<longrightarrow> bnd_r SY163)) =
sultana@55596
  2131
         True"
sultana@55596
  2132
(* by (tactic {*tectoc @{context}*}) *)
sultana@55596
  2133
by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
sultana@55596
  2134
sultana@55596
  2135
lemma "
sultana@55596
  2136
(\<forall>SY136.
sultana@55596
  2137
    \<not> (\<forall>SY137. bnd_irel SY136 SY137 \<longrightarrow> bnd_r SY137) \<or>
sultana@55596
  2138
    (\<forall>SY138.
sultana@55596
  2139
        bnd_irel SY136 SY138 \<longrightarrow> bnd_p SY138 \<and> bnd_q SY138)) =
sultana@55596
  2140
True \<Longrightarrow>
sultana@55596
  2141
(\<forall>SY136.
sultana@55596
  2142
    bnd_irel SY136 (bnd_sK5 SY136) \<and> \<not> bnd_r (bnd_sK5 SY136) \<or>
sultana@55596
  2143
    (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_p SY138) \<and>
sultana@55596
  2144
    (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_q SY138)) =
sultana@55596
  2145
True"
sultana@55596
  2146
by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
sultana@55596
  2147
*)
sultana@55596
  2148
sultana@55596
  2149
     (* (Annotated_step ("11", "extcnf_forall_neg"), *)
wenzelm@61076
  2150
lemma "\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
wenzelm@61076
  2151
            (\<forall>SY2::TPTP_Interpret.ind.
sultana@55596
  2152
                \<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
sultana@55596
  2153
                   \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
sultana@55596
  2154
            False \<Longrightarrow>
wenzelm@61076
  2155
         \<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
sultana@55596
  2156
            (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
sultana@55596
  2157
                \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
sultana@55596
  2158
            False"
sultana@55596
  2159
(* apply (tactic {*full_extcnf_combined_tac*}) *)
wenzelm@63167
  2160
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
sultana@55596
  2161
sultana@55596
  2162
     (* (Annotated_step ("13", "extcnf_forall_pos"), *)
sultana@55596
  2163
lemma "(\<forall>SY31 SY32.
sultana@55596
  2164
             bnd_sK2 (bnd_sK4 SY31 SY32) =
sultana@55596
  2165
             bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) =
sultana@55596
  2166
         True \<Longrightarrow>
sultana@55596
  2167
         \<forall>SV1. (\<forall>SY42.
sultana@55596
  2168
                   bnd_sK2 (bnd_sK4 SV1 SY42) =
sultana@55596
  2169
                   bnd_sK5 (bnd_sK2 SV1) (bnd_sK2 SY42)) =
sultana@55596
  2170
               True"
wenzelm@63167
  2171
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
sultana@55596
  2172
sultana@55596
  2173
     (* (Annotated_step ("14", "extcnf_forall_pos"), *)
sultana@55596
  2174
lemma "(\<forall>SY35 SY36.
sultana@55596
  2175
             bnd_sK1 (bnd_sK3 SY35 SY36) =
sultana@55596
  2176
             bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) =
sultana@55596
  2177
         True \<Longrightarrow>
sultana@55596
  2178
         \<forall>SV2. (\<forall>SY43.
sultana@55596
  2179
                   bnd_sK1 (bnd_sK3 SV2 SY43) =
sultana@55596
  2180
                   bnd_sK4 (bnd_sK1 SV2) (bnd_sK1 SY43)) =
sultana@55596
  2181
               True"
wenzelm@63167
  2182
by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
sultana@55596
  2183
sultana@55596
  2184
sultana@55596
  2185
(*from SYO198^5.p.out*)
sultana@55596
  2186
   (* [[(Annotated_step ("11", "extcnf_forall_special_pos"), *)
wenzelm@61076
  2187
lemma "(\<forall>SX0::bool \<Rightarrow> bool.
sultana@55596
  2188
             \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
sultana@55596
  2189
         True \<Longrightarrow>
sultana@55596
  2190
         (\<not> \<not> (\<not> True \<or> \<not> True)) = True"
wenzelm@63167
  2191
apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
sultana@55596
  2192
done
sultana@55596
  2193
sultana@55596
  2194
     (* (Annotated_step ("13", "extcnf_forall_special_pos"), *)
wenzelm@61076
  2195
lemma "(\<forall>SX0::bool \<Rightarrow> bool.
sultana@55596
  2196
             \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
sultana@55596
  2197
         True \<Longrightarrow>
sultana@55596
  2198
         (\<not> \<not> (\<not> bnd_sK1_Xx \<or> \<not> bnd_sK2_Xy)) = True"
wenzelm@63167
  2199
apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
sultana@55596
  2200
done
sultana@55596
  2201
sultana@55596
  2202
   (* [[(Annotated_step ("8", "polarity_switch"), *)
wenzelm@61076
  2203
lemma "(\<forall>(Xx::bool) (Xy::bool) Xz::bool. True \<and> True \<longrightarrow> True) =
sultana@55596
  2204
         False \<Longrightarrow>
wenzelm@61076
  2205
         (\<not> (\<forall>(Xx::bool) (Xy::bool) Xz::bool.
sultana@55596
  2206
                True \<and> True \<longrightarrow> True)) =
sultana@55596
  2207
         True"
wenzelm@63167
  2208
apply (tactic \<open>nonfull_extcnf_combined_tac @{context} [Polarity_switch]\<close>)
sultana@55596
  2209
done
sultana@55596
  2210
sultana@55596
  2211
lemma "((\<forall>SY22 SY23 SY24.
sultana@55596
  2212
       bnd_sK1_RRR SY22 SY23 \<and> bnd_sK1_RRR SY23 SY24 \<longrightarrow>
sultana@55596
  2213
       bnd_sK1_RRR SY22 SY24) \<and>
sultana@55596
  2214
   (\<forall>SY25.
sultana@55596
  2215
       (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
sultana@55596
  2216
       (\<forall>SY27.
sultana@55596
  2217
           (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
sultana@55596
  2218
           bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) \<longrightarrow>
sultana@55596
  2219
   (\<forall>SY29. \<exists>SY30. \<forall>SY31. SY29 SY31 \<longrightarrow> bnd_sK1_RRR SY31 SY30)) =
sultana@55596
  2220
  False \<Longrightarrow>
sultana@55596
  2221
  (\<forall>SY25.
sultana@55596
  2222
      (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
sultana@55596
  2223
      (\<forall>SY27.
sultana@55596
  2224
          (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
sultana@55596
  2225
          bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) =
sultana@55596
  2226
  True"
wenzelm@63167
  2227
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2228
done
sultana@55596
  2229
sultana@55596
  2230
lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
sultana@55596
  2231
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
sultana@55596
  2232
   (\<forall>A B. A = B \<longrightarrow>
sultana@55596
  2233
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
sultana@55596
  2234
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
sultana@55596
  2235
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
sultana@55596
  2236
  False \<Longrightarrow>
sultana@55596
  2237
 (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) =
sultana@55596
  2238
  True"
wenzelm@63167
  2239
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2240
done
sultana@55596
  2241
sultana@55596
  2242
lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
sultana@55596
  2243
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
sultana@55596
  2244
   (\<forall>A B. A = B \<longrightarrow>
sultana@55596
  2245
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
sultana@55596
  2246
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
sultana@55596
  2247
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
sultana@55596
  2248
  False \<Longrightarrow>
sultana@55596
  2249
  (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) =
sultana@55596
  2250
  True"
wenzelm@63167
  2251
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2252
done
sultana@55596
  2253
sultana@55596
  2254
lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
sultana@55596
  2255
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
sultana@55596
  2256
   (\<forall>A B. A = B \<longrightarrow>
sultana@55596
  2257
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
sultana@55596
  2258
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
sultana@55596
  2259
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
sultana@55596
  2260
  False \<Longrightarrow>
sultana@55596
  2261
  (\<forall>A B. A = B \<longrightarrow>
sultana@55596
  2262
         (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) =
sultana@55596
  2263
  True"
wenzelm@63167
  2264
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2265
done
sultana@55596
  2266
sultana@55596
  2267
lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
sultana@55596
  2268
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
sultana@55596
  2269
   (\<forall>A B. A = B \<longrightarrow>
sultana@55596
  2270
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
sultana@55596
  2271
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
sultana@55596
  2272
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
sultana@55596
  2273
  False \<Longrightarrow>
sultana@55596
  2274
  (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
sultana@55596
  2275
         bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset) =
sultana@55596
  2276
  False"
wenzelm@63167
  2277
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2278
done
sultana@55596
  2279
sultana@55596
  2280
(*nested conjunctions*)
sultana@55596
  2281
lemma "((((\<forall>Xx. bnd_cP bnd_e Xx = Xx) \<and>
sultana@55596
  2282
     (\<forall>Xy. bnd_cP Xy bnd_e = Xy)) \<and>
sultana@55596
  2283
    (\<forall>Xz. bnd_cP Xz Xz = bnd_e)) \<and>
sultana@55596
  2284
   (\<forall>Xx Xy Xz.
sultana@55596
  2285
       bnd_cP (bnd_cP Xx Xy) Xz = bnd_cP Xx (bnd_cP Xy Xz)) \<longrightarrow>
sultana@55596
  2286
   (\<forall>Xa Xb. bnd_cP Xa Xb = bnd_cP Xb Xa)) =
sultana@55596
  2287
  False \<Longrightarrow>
sultana@55596
  2288
  (\<forall>Xx. bnd_cP bnd_e Xx = Xx) =
sultana@55596
  2289
  True"
wenzelm@63167
  2290
apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
sultana@55596
  2291
done
sultana@55596
  2292
nipkow@62390
  2293
end