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