src/FOL/FOL.thy
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (20 months ago)
changeset 67087 733017b19de9
parent 63120 629a4c5e953e
child 69590 e65314985426
permissions -rw-r--r--
generalized more lemmas
wenzelm@9487
     1
(*  Title:      FOL/FOL.thy
wenzelm@9487
     2
    Author:     Lawrence C Paulson and Markus Wenzel
wenzelm@11678
     3
*)
wenzelm@9487
     4
wenzelm@60770
     5
section \<open>Classical first-order logic\<close>
wenzelm@4093
     6
wenzelm@18456
     7
theory FOL
paulson@15481
     8
imports IFOL
wenzelm@46950
     9
keywords "print_claset" "print_induct_rules" :: diag
wenzelm@18456
    10
begin
wenzelm@9487
    11
wenzelm@48891
    12
ML_file "~~/src/Provers/classical.ML"
wenzelm@48891
    13
ML_file "~~/src/Provers/blast.ML"
wenzelm@48891
    14
ML_file "~~/src/Provers/clasimp.ML"
wenzelm@48891
    15
wenzelm@9487
    16
wenzelm@60770
    17
subsection \<open>The classical axiom\<close>
wenzelm@4093
    18
wenzelm@41779
    19
axiomatization where
wenzelm@61487
    20
  classical: "(\<not> P \<Longrightarrow> P) \<Longrightarrow> P"
wenzelm@4093
    21
wenzelm@9487
    22
wenzelm@60770
    23
subsection \<open>Lemmas and proof tools\<close>
wenzelm@9487
    24
wenzelm@21539
    25
lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
wenzelm@21539
    26
  by (erule FalseE [THEN classical])
wenzelm@21539
    27
wenzelm@21539
    28
wenzelm@62020
    29
subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
wenzelm@61487
    30
wenzelm@61487
    31
lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
wenzelm@21539
    32
  apply (rule classical)
wenzelm@21539
    33
  apply (assumption | erule meta_mp | rule disjI1 notI)+
wenzelm@21539
    34
  apply (erule notE disjI2)+
wenzelm@21539
    35
  done
wenzelm@21539
    36
wenzelm@62020
    37
text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
wenzelm@21539
    38
lemma ex_classical:
wenzelm@61487
    39
  assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
wenzelm@61487
    40
  shows "\<exists>x. P(x)"
wenzelm@21539
    41
  apply (rule classical)
wenzelm@21539
    42
  apply (rule exI, erule r)
wenzelm@21539
    43
  done
wenzelm@21539
    44
wenzelm@62020
    45
text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
wenzelm@21539
    46
lemma exCI:
wenzelm@61487
    47
  assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
wenzelm@61487
    48
  shows "\<exists>x. P(x)"
wenzelm@21539
    49
  apply (rule ex_classical)
wenzelm@21539
    50
  apply (rule notI [THEN allI, THEN r])
wenzelm@21539
    51
  apply (erule notE)
wenzelm@21539
    52
  apply (erule exI)
wenzelm@21539
    53
  done
wenzelm@21539
    54
wenzelm@61487
    55
lemma excluded_middle: "\<not> P \<or> P"
wenzelm@21539
    56
  apply (rule disjCI)
wenzelm@21539
    57
  apply assumption
wenzelm@21539
    58
  done
wenzelm@21539
    59
wenzelm@27115
    60
lemma case_split [case_names True False]:
wenzelm@61487
    61
  assumes r1: "P \<Longrightarrow> Q"
wenzelm@61487
    62
    and r2: "\<not> P \<Longrightarrow> Q"
wenzelm@21539
    63
  shows Q
wenzelm@21539
    64
  apply (rule excluded_middle [THEN disjE])
wenzelm@21539
    65
  apply (erule r2)
wenzelm@21539
    66
  apply (erule r1)
wenzelm@21539
    67
  done
wenzelm@21539
    68
wenzelm@60770
    69
ML \<open>
wenzelm@59780
    70
  fun case_tac ctxt a fixes =
wenzelm@61487
    71
    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
wenzelm@60770
    72
\<close>
wenzelm@21539
    73
wenzelm@60770
    74
method_setup case_tac = \<open>
wenzelm@63120
    75
  Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
wenzelm@59780
    76
    (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
wenzelm@60770
    77
\<close> "case_tac emulation (dynamic instantiation!)"
wenzelm@27211
    78
wenzelm@21539
    79
wenzelm@61487
    80
subsection \<open>Special elimination rules\<close>
wenzelm@21539
    81
wenzelm@62020
    82
text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
wenzelm@21539
    83
lemma impCE:
wenzelm@61487
    84
  assumes major: "P \<longrightarrow> Q"
wenzelm@61487
    85
    and r1: "\<not> P \<Longrightarrow> R"
wenzelm@61487
    86
    and r2: "Q \<Longrightarrow> R"
wenzelm@21539
    87
  shows R
wenzelm@21539
    88
  apply (rule excluded_middle [THEN disjE])
wenzelm@21539
    89
   apply (erule r1)
wenzelm@21539
    90
  apply (rule r2)
wenzelm@21539
    91
  apply (erule major [THEN mp])
wenzelm@21539
    92
  done
wenzelm@21539
    93
wenzelm@61487
    94
text \<open>
wenzelm@62020
    95
  This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''.
wenzelm@61487
    96
  Can't install as default: would break old proofs.
wenzelm@61487
    97
\<close>
wenzelm@21539
    98
lemma impCE':
wenzelm@61487
    99
  assumes major: "P \<longrightarrow> Q"
wenzelm@61487
   100
    and r1: "Q \<Longrightarrow> R"
wenzelm@61487
   101
    and r2: "\<not> P \<Longrightarrow> R"
wenzelm@21539
   102
  shows R
wenzelm@21539
   103
  apply (rule excluded_middle [THEN disjE])
wenzelm@21539
   104
   apply (erule r2)
wenzelm@21539
   105
  apply (rule r1)
wenzelm@21539
   106
  apply (erule major [THEN mp])
wenzelm@21539
   107
  done
wenzelm@21539
   108
wenzelm@61487
   109
text \<open>Double negation law.\<close>
wenzelm@61487
   110
lemma notnotD: "\<not> \<not> P \<Longrightarrow> P"
wenzelm@21539
   111
  apply (rule classical)
wenzelm@21539
   112
  apply (erule notE)
wenzelm@21539
   113
  apply assumption
wenzelm@21539
   114
  done
wenzelm@21539
   115
wenzelm@61487
   116
lemma contrapos2:  "\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P"
wenzelm@21539
   117
  apply (rule classical)
wenzelm@21539
   118
  apply (drule (1) meta_mp)
wenzelm@21539
   119
  apply (erule (1) notE)
wenzelm@21539
   120
  done
wenzelm@21539
   121
wenzelm@61487
   122
wenzelm@61487
   123
subsubsection \<open>Tactics for implication and contradiction\<close>
wenzelm@21539
   124
wenzelm@61487
   125
text \<open>
wenzelm@62020
   126
  Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in
wenzelm@62020
   127
  \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>.
wenzelm@61487
   128
\<close>
wenzelm@21539
   129
lemma iffCE:
wenzelm@61487
   130
  assumes major: "P \<longleftrightarrow> Q"
wenzelm@61487
   131
    and r1: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
wenzelm@61487
   132
    and r2: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
wenzelm@21539
   133
  shows R
wenzelm@21539
   134
  apply (rule major [unfolded iff_def, THEN conjE])
wenzelm@21539
   135
  apply (elim impCE)
wenzelm@21539
   136
     apply (erule (1) r2)
wenzelm@21539
   137
    apply (erule (1) notE)+
wenzelm@21539
   138
  apply (erule (1) r1)
wenzelm@21539
   139
  done
wenzelm@21539
   140
wenzelm@21539
   141
wenzelm@21539
   142
(*Better for fast_tac: needs no quantifier duplication!*)
wenzelm@21539
   143
lemma alt_ex1E:
wenzelm@61487
   144
  assumes major: "\<exists>! x. P(x)"
wenzelm@61487
   145
    and r: "\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
wenzelm@21539
   146
  shows R
wenzelm@21539
   147
  using major
wenzelm@21539
   148
proof (rule ex1E)
wenzelm@21539
   149
  fix x
wenzelm@21539
   150
  assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
wenzelm@21539
   151
  assume "P(x)"
wenzelm@21539
   152
  then show R
wenzelm@21539
   153
  proof (rule r)
wenzelm@61487
   154
    {
wenzelm@61487
   155
      fix y y'
wenzelm@21539
   156
      assume "P(y)" and "P(y')"
wenzelm@61487
   157
      with * have "x = y" and "x = y'"
wenzelm@61487
   158
        by - (tactic "IntPr.fast_tac @{context} 1")+
wenzelm@21539
   159
      then have "y = y'" by (rule subst)
wenzelm@21539
   160
    } note r' = this
wenzelm@61487
   161
    show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'"
wenzelm@61487
   162
      by (intro strip, elim conjE) (rule r')
wenzelm@21539
   163
  qed
wenzelm@21539
   164
qed
wenzelm@9525
   165
wenzelm@61487
   166
lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
wenzelm@26411
   167
  by (rule classical) iprover
wenzelm@26411
   168
wenzelm@61487
   169
lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
wenzelm@26411
   170
  by (rule classical) iprover
wenzelm@26411
   171
wenzelm@27849
   172
wenzelm@60770
   173
section \<open>Classical Reasoner\<close>
wenzelm@27849
   174
wenzelm@60770
   175
ML \<open>
wenzelm@42799
   176
structure Cla = Classical
wenzelm@42793
   177
(
wenzelm@42793
   178
  val imp_elim = @{thm imp_elim}
wenzelm@42793
   179
  val not_elim = @{thm notE}
wenzelm@42793
   180
  val swap = @{thm swap}
wenzelm@42793
   181
  val classical = @{thm classical}
wenzelm@42793
   182
  val sizef = size_of_thm
wenzelm@42793
   183
  val hyp_subst_tacs = [hyp_subst_tac]
wenzelm@42793
   184
);
wenzelm@42793
   185
wenzelm@42793
   186
structure Basic_Classical: BASIC_CLASSICAL = Cla;
wenzelm@42793
   187
open Basic_Classical;
wenzelm@60770
   188
\<close>
wenzelm@42793
   189
wenzelm@42793
   190
(*Propositional rules*)
wenzelm@42793
   191
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
wenzelm@42793
   192
  and [elim!] = conjE disjE impCE FalseE iffCE
wenzelm@60770
   193
ML \<open>val prop_cs = claset_of @{context}\<close>
wenzelm@42793
   194
wenzelm@42793
   195
(*Quantifier rules*)
wenzelm@42793
   196
lemmas [intro!] = allI ex_ex1I
wenzelm@42793
   197
  and [intro] = exI
wenzelm@42793
   198
  and [elim!] = exE alt_ex1E
wenzelm@42793
   199
  and [elim] = allE
wenzelm@60770
   200
ML \<open>val FOL_cs = claset_of @{context}\<close>
wenzelm@10383
   201
wenzelm@60770
   202
ML \<open>
wenzelm@32176
   203
  structure Blast = Blast
wenzelm@32176
   204
  (
wenzelm@42477
   205
    structure Classical = Cla
wenzelm@42802
   206
    val Trueprop_const = dest_Const @{const Trueprop}
wenzelm@41310
   207
    val equality_name = @{const_name eq}
wenzelm@32176
   208
    val not_name = @{const_name Not}
wenzelm@32960
   209
    val notE = @{thm notE}
wenzelm@32960
   210
    val ccontr = @{thm ccontr}
wenzelm@32176
   211
    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
wenzelm@32176
   212
  );
wenzelm@32176
   213
  val blast_tac = Blast.blast_tac;
wenzelm@60770
   214
\<close>
wenzelm@32176
   215
paulson@13550
   216
wenzelm@61487
   217
lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
wenzelm@21539
   218
  by blast
wenzelm@20223
   219
wenzelm@62020
   220
text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
wenzelm@61487
   221
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
wenzelm@20223
   222
proof
wenzelm@20223
   223
  assume "True \<Longrightarrow> PROP P"
wenzelm@20223
   224
  from this and TrueI show "PROP P" .
wenzelm@20223
   225
next
wenzelm@20223
   226
  assume "PROP P"
wenzelm@20223
   227
  then show "PROP P" .
wenzelm@20223
   228
qed
wenzelm@9487
   229
wenzelm@61487
   230
lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
wenzelm@21539
   231
  by blast
wenzelm@21539
   232
wenzelm@61487
   233
lemma iff_allI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
wenzelm@21539
   234
  by blast
wenzelm@21539
   235
wenzelm@61487
   236
lemma iff_exI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
wenzelm@21539
   237
  by blast
wenzelm@21539
   238
wenzelm@61487
   239
lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
wenzelm@61487
   240
  by blast
wenzelm@21539
   241
wenzelm@61487
   242
lemma ex_comm: "(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
wenzelm@61487
   243
  by blast
wenzelm@21539
   244
wenzelm@26286
   245
wenzelm@26286
   246
wenzelm@61487
   247
subsection \<open>Classical simplification rules\<close>
wenzelm@26286
   248
wenzelm@61487
   249
text \<open>
wenzelm@62020
   250
  Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and
wenzelm@61487
   251
  false cases boil down to the same thing.
wenzelm@61487
   252
\<close>
wenzelm@61487
   253
wenzelm@61487
   254
lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
wenzelm@61487
   255
  by blast
wenzelm@26286
   256
wenzelm@26286
   257
wenzelm@61487
   258
subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
wenzelm@61487
   259
wenzelm@61487
   260
text \<open>
wenzelm@62020
   261
  We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of
wenzelm@62020
   262
  \<open>\<exists>\<close> over \<open>\<or>\<close>.
wenzelm@26286
   263
wenzelm@61487
   264
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
wenzelm@61487
   265
  this step can increase proof length!
wenzelm@61487
   266
\<close>
wenzelm@61487
   267
wenzelm@61487
   268
text \<open>Existential miniscoping.\<close>
wenzelm@26286
   269
lemma int_ex_simps:
wenzelm@61487
   270
  "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
wenzelm@61487
   271
  "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
wenzelm@61487
   272
  "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
wenzelm@61487
   273
  "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
wenzelm@26286
   274
  by iprover+
wenzelm@26286
   275
wenzelm@61487
   276
text \<open>Classical rules.\<close>
wenzelm@26286
   277
lemma cla_ex_simps:
wenzelm@61487
   278
  "\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
wenzelm@61487
   279
  "\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@26286
   280
  by blast+
wenzelm@26286
   281
wenzelm@26286
   282
lemmas ex_simps = int_ex_simps cla_ex_simps
wenzelm@26286
   283
wenzelm@61487
   284
text \<open>Universal miniscoping.\<close>
wenzelm@26286
   285
lemma int_all_simps:
wenzelm@61487
   286
  "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
wenzelm@61487
   287
  "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
wenzelm@61487
   288
  "\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q"
wenzelm@61487
   289
  "\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
wenzelm@26286
   290
  by iprover+
wenzelm@26286
   291
wenzelm@61487
   292
text \<open>Classical rules.\<close>
wenzelm@26286
   293
lemma cla_all_simps:
wenzelm@61487
   294
  "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
wenzelm@61487
   295
  "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
wenzelm@26286
   296
  by blast+
wenzelm@26286
   297
wenzelm@26286
   298
lemmas all_simps = int_all_simps cla_all_simps
wenzelm@26286
   299
wenzelm@26286
   300
wenzelm@61487
   301
subsubsection \<open>Named rewrite rules proved for IFOL\<close>
wenzelm@26286
   302
wenzelm@61487
   303
lemma imp_disj1: "(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
wenzelm@61487
   304
lemma imp_disj2: "Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
wenzelm@26286
   305
wenzelm@61487
   306
lemma de_Morgan_conj: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)" by blast
wenzelm@26286
   307
wenzelm@61487
   308
lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)" by blast
wenzelm@61487
   309
lemma not_iff: "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
wenzelm@26286
   310
wenzelm@61487
   311
lemma not_all: "(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))" by blast
wenzelm@61487
   312
lemma imp_all: "((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)" by blast
wenzelm@26286
   313
wenzelm@26286
   314
wenzelm@26286
   315
lemmas meta_simps =
wenzelm@62020
   316
  triv_forall_equality  \<comment> \<open>prunes params\<close>
wenzelm@62020
   317
  True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
wenzelm@26286
   318
wenzelm@26286
   319
lemmas IFOL_simps =
wenzelm@26286
   320
  refl [THEN P_iff_T] conj_simps disj_simps not_simps
wenzelm@26286
   321
  imp_simps iff_simps quant_simps
wenzelm@26286
   322
wenzelm@61487
   323
lemma notFalseI: "\<not> False" by iprover
wenzelm@26286
   324
wenzelm@26286
   325
lemma cla_simps_misc:
wenzelm@61487
   326
  "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
wenzelm@61487
   327
  "P \<or> \<not> P"
wenzelm@61487
   328
  "\<not> P \<or> P"
wenzelm@61487
   329
  "\<not> \<not> P \<longleftrightarrow> P"
wenzelm@61487
   330
  "(\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
wenzelm@61487
   331
  "(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)" by blast+
wenzelm@26286
   332
wenzelm@26286
   333
lemmas cla_simps =
wenzelm@26286
   334
  de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
wenzelm@26286
   335
  not_imp not_all not_ex cases_simp cla_simps_misc
wenzelm@26286
   336
wenzelm@26286
   337
wenzelm@48891
   338
ML_file "simpdata.ML"
wenzelm@42455
   339
wenzelm@61487
   340
simproc_setup defined_Ex ("\<exists>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
wenzelm@61487
   341
simproc_setup defined_All ("\<forall>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
wenzelm@42455
   342
wenzelm@60770
   343
ML \<open>
wenzelm@42453
   344
(*intuitionistic simprules only*)
wenzelm@42453
   345
val IFOL_ss =
wenzelm@51717
   346
  put_simpset FOL_basic_ss @{context}
wenzelm@45654
   347
  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
wenzelm@42455
   348
  addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
wenzelm@51717
   349
  |> Simplifier.add_cong @{thm imp_cong}
wenzelm@51717
   350
  |> simpset_of;
wenzelm@42453
   351
wenzelm@42453
   352
(*classical simprules too*)
wenzelm@51717
   353
val FOL_ss =
wenzelm@51717
   354
  put_simpset IFOL_ss @{context}
wenzelm@51717
   355
  addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
wenzelm@51717
   356
  |> simpset_of;
wenzelm@60770
   357
\<close>
wenzelm@42453
   358
wenzelm@60770
   359
setup \<open>
wenzelm@58826
   360
  map_theory_simpset (put_simpset FOL_ss) #>
wenzelm@58826
   361
  Simplifier.method_setup Splitter.split_modifiers
wenzelm@60770
   362
\<close>
wenzelm@52241
   363
wenzelm@52241
   364
ML_file "~~/src/Tools/eqsubst.ML"
paulson@15481
   365
paulson@15481
   366
wenzelm@60770
   367
subsection \<open>Other simple lemmas\<close>
paulson@14085
   368
wenzelm@61487
   369
lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)"
wenzelm@61487
   370
  by blast
paulson@14085
   371
wenzelm@61487
   372
lemma [simp]: "((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))"
wenzelm@61487
   373
  by blast
paulson@14085
   374
wenzelm@61487
   375
lemma not_disj_iff_imp: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
wenzelm@61487
   376
  by blast
wenzelm@61487
   377
paulson@14085
   378
wenzelm@61487
   379
subsubsection \<open>Monotonicity of implications\<close>
paulson@14085
   380
wenzelm@61487
   381
lemma conj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
wenzelm@61487
   382
  by fast (*or (IntPr.fast_tac 1)*)
paulson@14085
   383
wenzelm@61487
   384
lemma disj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
wenzelm@61487
   385
  by fast (*or (IntPr.fast_tac 1)*)
paulson@14085
   386
wenzelm@61487
   387
lemma imp_mono: "\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
wenzelm@61487
   388
  by fast (*or (IntPr.fast_tac 1)*)
paulson@14085
   389
wenzelm@61487
   390
lemma imp_refl: "P \<longrightarrow> P"
wenzelm@61487
   391
  by (rule impI)
paulson@14085
   392
wenzelm@61487
   393
text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
wenzelm@61487
   394
lemma ex_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
wenzelm@61487
   395
  by blast
paulson@14085
   396
wenzelm@61487
   397
lemma all_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))"
wenzelm@61487
   398
  by blast
paulson@14085
   399
wenzelm@11678
   400
wenzelm@60770
   401
subsection \<open>Proof by cases and induction\<close>
wenzelm@11678
   402
wenzelm@60770
   403
text \<open>Proper handling of non-atomic rule statements.\<close>
wenzelm@11678
   404
wenzelm@59940
   405
context
wenzelm@59940
   406
begin
wenzelm@59940
   407
wenzelm@59990
   408
qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
wenzelm@59990
   409
qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
wenzelm@59990
   410
qualified definition "induct_equal(x, y) \<equiv> x = y"
wenzelm@59990
   411
qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
wenzelm@11678
   412
wenzelm@59942
   413
lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
wenzelm@18816
   414
  unfolding atomize_all induct_forall_def .
wenzelm@11678
   415
wenzelm@59942
   416
lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))"
wenzelm@18816
   417
  unfolding atomize_imp induct_implies_def .
wenzelm@11678
   418
wenzelm@59942
   419
lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))"
wenzelm@18816
   420
  unfolding atomize_eq induct_equal_def .
wenzelm@11678
   421
wenzelm@59942
   422
lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop(induct_conj(A, B))"
wenzelm@18816
   423
  unfolding atomize_conj induct_conj_def .
wenzelm@11988
   424
wenzelm@18456
   425
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
wenzelm@45594
   426
lemmas induct_rulify [symmetric] = induct_atomize
wenzelm@18456
   427
lemmas induct_rulify_fallback =
wenzelm@18456
   428
  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
wenzelm@11678
   429
wenzelm@60770
   430
text \<open>Method setup.\<close>
wenzelm@11678
   431
wenzelm@58826
   432
ML_file "~~/src/Tools/induct.ML"
wenzelm@60770
   433
ML \<open>
wenzelm@32171
   434
  structure Induct = Induct
wenzelm@24830
   435
  (
wenzelm@22139
   436
    val cases_default = @{thm case_split}
wenzelm@22139
   437
    val atomize = @{thms induct_atomize}
wenzelm@22139
   438
    val rulify = @{thms induct_rulify}
wenzelm@22139
   439
    val rulify_fallback = @{thms induct_rulify_fallback}
berghofe@34989
   440
    val equal_def = @{thm induct_equal_def}
berghofe@34914
   441
    fun dest_def _ = NONE
wenzelm@58957
   442
    fun trivial_tac _ _ = no_tac
wenzelm@24830
   443
  );
wenzelm@60770
   444
\<close>
wenzelm@11678
   445
wenzelm@24830
   446
declare case_split [cases type: o]
wenzelm@11678
   447
wenzelm@59940
   448
end
wenzelm@59940
   449
wenzelm@58826
   450
ML_file "~~/src/Tools/case_product.ML"
noschinl@41827
   451
wenzelm@41310
   452
wenzelm@41310
   453
hide_const (open) eq
wenzelm@41310
   454
wenzelm@4854
   455
end