src/FOL/FOL.thy
author wenzelm
Mon, 24 Oct 2016 11:42:39 +0200
changeset 64367 a424f2737646
parent 63120 629a4c5e953e
child 69590 e65314985426
permissions -rw-r--r--
updated for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     1
(*  Title:      FOL/FOL.thy
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     2
    Author:     Lawrence C Paulson and Markus Wenzel
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
     3
*)
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
     4
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
     5
section \<open>Classical first-order logic\<close>
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
     6
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
     7
theory FOL
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15019
diff changeset
     8
imports IFOL
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 45654
diff changeset
     9
keywords "print_claset" "print_induct_rules" :: diag
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
    10
begin
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    11
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48776
diff changeset
    12
ML_file "~~/src/Provers/classical.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48776
diff changeset
    13
ML_file "~~/src/Provers/blast.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48776
diff changeset
    14
ML_file "~~/src/Provers/clasimp.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48776
diff changeset
    15
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    16
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    17
subsection \<open>The classical axiom\<close>
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    18
41779
a68f503805ed modernized specifications;
wenzelm
parents: 41310
diff changeset
    19
axiomatization where
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    20
  classical: "(\<not> P \<Longrightarrow> P) \<Longrightarrow> P"
4093
5e8f3d57dee7 added claset thy_data;
wenzelm
parents: 0
diff changeset
    21
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    22
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    23
subsection \<open>Lemmas and proof tools\<close>
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
    24
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    25
lemma ccontr: "(\<not> P \<Longrightarrow> False) \<Longrightarrow> P"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    26
  by (erule FalseE [THEN classical])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    27
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    28
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
    29
subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    30
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    31
lemma disjCI: "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    32
  apply (rule classical)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    33
  apply (assumption | erule meta_mp | rule disjI1 notI)+
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    34
  apply (erule notE disjI2)+
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    35
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    36
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
    37
text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    38
lemma ex_classical:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    39
  assumes r: "\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    40
  shows "\<exists>x. P(x)"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    41
  apply (rule classical)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    42
  apply (rule exI, erule r)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    43
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    44
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
    45
text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    46
lemma exCI:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    47
  assumes r: "\<forall>x. \<not> P(x) \<Longrightarrow> P(a)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    48
  shows "\<exists>x. P(x)"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    49
  apply (rule ex_classical)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    50
  apply (rule notI [THEN allI, THEN r])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    51
  apply (erule notE)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    52
  apply (erule exI)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    53
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    54
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    55
lemma excluded_middle: "\<not> P \<or> P"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    56
  apply (rule disjCI)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    57
  apply assumption
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    58
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    59
27115
0dcafa5c9e3f eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents: 26496
diff changeset
    60
lemma case_split [case_names True False]:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    61
  assumes r1: "P \<Longrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    62
    and r2: "\<not> P \<Longrightarrow> Q"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    63
  shows Q
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    64
  apply (rule excluded_middle [THEN disjE])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    65
  apply (erule r2)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    66
  apply (erule r1)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    67
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    68
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    69
ML \<open>
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
    70
  fun case_tac ctxt a fixes =
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    71
    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    72
\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    73
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    74
method_setup case_tac = \<open>
63120
629a4c5e953e embedded content may be delimited via cartouches;
wenzelm
parents: 62020
diff changeset
    75
  Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >>
59780
23b67731f4f0 support 'for' fixes in rule_tac etc.;
wenzelm
parents: 59763
diff changeset
    76
    (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
    77
\<close> "case_tac emulation (dynamic instantiation!)"
27211
6724f31a1c8e removed unused excluded_middle_tac;
wenzelm
parents: 27115
diff changeset
    78
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    79
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    80
subsection \<open>Special elimination rules\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    81
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
    82
text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    83
lemma impCE:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    84
  assumes major: "P \<longrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    85
    and r1: "\<not> P \<Longrightarrow> R"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    86
    and r2: "Q \<Longrightarrow> R"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    87
  shows R
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    88
  apply (rule excluded_middle [THEN disjE])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    89
   apply (erule r1)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    90
  apply (rule r2)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    91
  apply (erule major [THEN mp])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    92
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    93
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    94
text \<open>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
    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''.
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    96
  Can't install as default: would break old proofs.
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    97
\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
    98
lemma impCE':
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
    99
  assumes major: "P \<longrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   100
    and r1: "Q \<Longrightarrow> R"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   101
    and r2: "\<not> P \<Longrightarrow> R"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   102
  shows R
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   103
  apply (rule excluded_middle [THEN disjE])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   104
   apply (erule r2)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   105
  apply (rule r1)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   106
  apply (erule major [THEN mp])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   107
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   108
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   109
text \<open>Double negation law.\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   110
lemma notnotD: "\<not> \<not> P \<Longrightarrow> P"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   111
  apply (rule classical)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   112
  apply (erule notE)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   113
  apply assumption
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   114
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   115
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   116
lemma contrapos2:  "\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   117
  apply (rule classical)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   118
  apply (drule (1) meta_mp)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   119
  apply (erule (1) notE)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   120
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   121
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   122
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   123
subsubsection \<open>Tactics for implication and contradiction\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   124
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   125
text \<open>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   126
  Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   127
  \<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>.
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   128
\<close>
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   129
lemma iffCE:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   130
  assumes major: "P \<longleftrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   131
    and r1: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   132
    and r2: "\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   133
  shows R
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   134
  apply (rule major [unfolded iff_def, THEN conjE])
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   135
  apply (elim impCE)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   136
     apply (erule (1) r2)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   137
    apply (erule (1) notE)+
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   138
  apply (erule (1) r1)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   139
  done
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   140
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   141
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   142
(*Better for fast_tac: needs no quantifier duplication!*)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   143
lemma alt_ex1E:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   144
  assumes major: "\<exists>! x. P(x)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   145
    and r: "\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   146
  shows R
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   147
  using major
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   148
proof (rule ex1E)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   149
  fix x
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   150
  assume * : "\<forall>y. P(y) \<longrightarrow> y = x"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   151
  assume "P(x)"
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   152
  then show R
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   153
  proof (rule r)
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   154
    {
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   155
      fix y y'
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   156
      assume "P(y)" and "P(y')"
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   157
      with * have "x = y" and "x = y'"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   158
        by - (tactic "IntPr.fast_tac @{context} 1")+
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   159
      then have "y = y'" by (rule subst)
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   160
    } note r' = this
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   161
    show "\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   162
      by (intro strip, elim conjE) (rule r')
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   163
  qed
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   164
qed
9525
46fb9ccae463 lemmas atomize = all_eq imp_eq;
wenzelm
parents: 9487
diff changeset
   165
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   166
lemma imp_elim: "P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
26411
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26286
diff changeset
   167
  by (rule classical) iprover
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26286
diff changeset
   168
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   169
lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
26411
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26286
diff changeset
   170
  by (rule classical) iprover
cd74690f3bfb pass imp_elim, swap to classical prover;
wenzelm
parents: 26286
diff changeset
   171
27849
c74905423895 tuned document;
wenzelm
parents: 27239
diff changeset
   172
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   173
section \<open>Classical Reasoner\<close>
27849
c74905423895 tuned document;
wenzelm
parents: 27239
diff changeset
   174
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   175
ML \<open>
42799
4e33894aec6d modernized functor names;
wenzelm
parents: 42795
diff changeset
   176
structure Cla = Classical
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   177
(
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   178
  val imp_elim = @{thm imp_elim}
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   179
  val not_elim = @{thm notE}
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   180
  val swap = @{thm swap}
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   181
  val classical = @{thm classical}
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   182
  val sizef = size_of_thm
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   183
  val hyp_subst_tacs = [hyp_subst_tac]
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   184
);
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   185
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   186
structure Basic_Classical: BASIC_CLASSICAL = Cla;
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   187
open Basic_Classical;
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   188
\<close>
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   189
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   190
(*Propositional rules*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   191
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   192
  and [elim!] = conjE disjE impCE FalseE iffCE
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   193
ML \<open>val prop_cs = claset_of @{context}\<close>
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   194
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   195
(*Quantifier rules*)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   196
lemmas [intro!] = allI ex_ex1I
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   197
  and [intro] = exI
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   198
  and [elim!] = exE alt_ex1E
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42477
diff changeset
   199
  and [elim] = allE
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   200
ML \<open>val FOL_cs = claset_of @{context}\<close>
10383
a092ae7bb2a6 "atomize" for classical tactics;
wenzelm
parents: 10130
diff changeset
   201
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   202
ML \<open>
32176
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   203
  structure Blast = Blast
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   204
  (
42477
52fa26b6c524 simplified Blast setup;
wenzelm
parents: 42459
diff changeset
   205
    structure Classical = Cla
42802
51d7e74f6899 simplified BLAST_DATA;
wenzelm
parents: 42799
diff changeset
   206
    val Trueprop_const = dest_Const @{const Trueprop}
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   207
    val equality_name = @{const_name eq}
32176
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   208
    val not_name = @{const_name Not}
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32261
diff changeset
   209
    val notE = @{thm notE}
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32261
diff changeset
   210
    val ccontr = @{thm ccontr}
32176
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   211
    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   212
  );
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   213
  val blast_tac = Blast.blast_tac;
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   214
\<close>
32176
893614e2c35c renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents: 32171
diff changeset
   215
13550
5a176b8dda84 removal of blast.overloaded
paulson
parents: 12367
diff changeset
   216
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   217
lemma ex1_functional: "\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   218
  by blast
20223
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   219
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   220
text \<open>Elimination of \<open>True\<close> from assumptions:\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   221
lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
20223
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   222
proof
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   223
  assume "True \<Longrightarrow> PROP P"
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   224
  from this and TrueI show "PROP P" .
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   225
next
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   226
  assume "PROP P"
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   227
  then show "PROP P" .
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   228
qed
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
   229
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   230
lemma uncurry: "P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   231
  by blast
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   232
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   233
lemma iff_allI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   234
  by blast
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   235
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   236
lemma iff_exI: "(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))"
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   237
  by blast
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   238
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   239
lemma all_comm: "(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   240
  by blast
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   241
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   242
lemma ex_comm: "(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   243
  by blast
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   244
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   245
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   246
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   247
subsection \<open>Classical simplification rules\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   248
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   249
text \<open>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   250
  Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   251
  false cases boil down to the same thing.
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   252
\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   253
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   254
lemma cases_simp: "(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   255
  by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   256
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   257
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   258
subsubsection \<open>Miniscoping: pushing quantifiers in\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   259
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   260
text \<open>
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   261
  We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   262
  \<open>\<exists>\<close> over \<open>\<or>\<close>.
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   263
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   264
  Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   265
  this step can increase proof length!
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   266
\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   267
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   268
text \<open>Existential miniscoping.\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   269
lemma int_ex_simps:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   270
  "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   271
  "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   272
  "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   273
  "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   274
  by iprover+
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   275
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   276
text \<open>Classical rules.\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   277
lemma cla_ex_simps:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   278
  "\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   279
  "\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   280
  by blast+
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   281
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   282
lemmas ex_simps = int_ex_simps cla_ex_simps
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   283
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   284
text \<open>Universal miniscoping.\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   285
lemma int_all_simps:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   286
  "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   287
  "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   288
  "\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   289
  "\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   290
  by iprover+
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   291
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   292
text \<open>Classical rules.\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   293
lemma cla_all_simps:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   294
  "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   295
  "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   296
  by blast+
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   297
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   298
lemmas all_simps = int_all_simps cla_all_simps
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   299
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   300
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   301
subsubsection \<open>Named rewrite rules proved for IFOL\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   302
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   303
lemma imp_disj1: "(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   304
lemma imp_disj2: "Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)" by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   305
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   306
lemma de_Morgan_conj: "(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)" by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   307
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   308
lemma not_imp: "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)" by blast
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   309
lemma not_iff: "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)" by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   310
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   311
lemma not_all: "(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))" by blast
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   312
lemma imp_all: "((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)" by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   313
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   314
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   315
lemmas meta_simps =
62020
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   316
  triv_forall_equality  \<comment> \<open>prunes params\<close>
5d208fd2507d isabelle update_cartouches -c -t;
wenzelm
parents: 61487
diff changeset
   317
  True_implies_equals  \<comment> \<open>prune asms \<open>True\<close>\<close>
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   318
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   319
lemmas IFOL_simps =
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   320
  refl [THEN P_iff_T] conj_simps disj_simps not_simps
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   321
  imp_simps iff_simps quant_simps
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   322
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   323
lemma notFalseI: "\<not> False" by iprover
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   324
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   325
lemma cla_simps_misc:
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   326
  "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   327
  "P \<or> \<not> P"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   328
  "\<not> P \<or> P"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   329
  "\<not> \<not> P \<longleftrightarrow> P"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   330
  "(\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   331
  "(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)" by blast+
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   332
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   333
lemmas cla_simps =
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   334
  de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   335
  not_imp not_all not_ex cases_simp cla_simps_misc
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   336
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   337
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48776
diff changeset
   338
ML_file "simpdata.ML"
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 42453
diff changeset
   339
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   340
simproc_setup defined_Ex ("\<exists>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_ex\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   341
simproc_setup defined_All ("\<forall>x. P(x)") = \<open>fn _ => Quantifier1.rearrange_all\<close>
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 42453
diff changeset
   342
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   343
ML \<open>
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   344
(*intuitionistic simprules only*)
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   345
val IFOL_ss =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   346
  put_simpset FOL_basic_ss @{context}
45654
cf10bde35973 more antiquotations;
wenzelm
parents: 45620
diff changeset
   347
  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps}
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 42453
diff changeset
   348
  addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}]
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   349
  |> Simplifier.add_cong @{thm imp_cong}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   350
  |> simpset_of;
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   351
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   352
(*classical simprules too*)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   353
val FOL_ss =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   354
  put_simpset IFOL_ss @{context}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   355
  addsimps @{thms cla_simps cla_ex_simps cla_all_simps}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   356
  |> simpset_of;
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   357
\<close>
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   358
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   359
setup \<open>
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   360
  map_theory_simpset (put_simpset FOL_ss) #>
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   361
  Simplifier.method_setup Splitter.split_modifiers
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   362
\<close>
52241
5f6e885382e9 tuned import;
wenzelm
parents: 51798
diff changeset
   363
5f6e885382e9 tuned import;
wenzelm
parents: 51798
diff changeset
   364
ML_file "~~/src/Tools/eqsubst.ML"
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15019
diff changeset
   365
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15019
diff changeset
   366
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   367
subsection \<open>Other simple lemmas\<close>
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   368
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   369
lemma [simp]: "((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   370
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   371
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   372
lemma [simp]: "((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   373
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   374
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   375
lemma not_disj_iff_imp: "\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   376
  by blast
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   377
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   378
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   379
subsubsection \<open>Monotonicity of implications\<close>
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   380
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   381
lemma conj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   382
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   383
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   384
lemma disj_mono: "\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   385
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   386
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   387
lemma imp_mono: "\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   388
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   389
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   390
lemma imp_refl: "P \<longrightarrow> P"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   391
  by (rule impI)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   392
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   393
text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   394
lemma ex_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   395
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   396
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   397
lemma all_mono: "(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))"
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   398
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   399
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   400
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   401
subsection \<open>Proof by cases and induction\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   402
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   403
text \<open>Proper handling of non-atomic rule statements.\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   404
59940
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   405
context
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   406
begin
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   407
59990
a81dc82ecba3 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents: 59942
diff changeset
   408
qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
a81dc82ecba3 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents: 59942
diff changeset
   409
qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
a81dc82ecba3 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents: 59942
diff changeset
   410
qualified definition "induct_equal(x, y) \<equiv> x = y"
a81dc82ecba3 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents: 59942
diff changeset
   411
qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   412
59942
wenzelm
parents: 59940
diff changeset
   413
lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   414
  unfolding atomize_all induct_forall_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   415
59942
wenzelm
parents: 59940
diff changeset
   416
lemma induct_implies_eq: "(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))"
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   417
  unfolding atomize_imp induct_implies_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   418
59942
wenzelm
parents: 59940
diff changeset
   419
lemma induct_equal_eq: "(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))"
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   420
  unfolding atomize_eq induct_equal_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   421
59942
wenzelm
parents: 59940
diff changeset
   422
lemma induct_conj_eq: "(A &&& B) \<equiv> Trueprop(induct_conj(A, B))"
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   423
  unfolding atomize_conj induct_conj_def .
11988
8340fb172607 induct_impliesI;
wenzelm
parents: 11848
diff changeset
   424
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   425
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
45594
wenzelm
parents: 43560
diff changeset
   426
lemmas induct_rulify [symmetric] = induct_atomize
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   427
lemmas induct_rulify_fallback =
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   428
  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   429
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   430
text \<open>Method setup.\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   431
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   432
ML_file "~~/src/Tools/induct.ML"
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   433
ML \<open>
32171
220abde9962b renamed functor InductFun to Induct;
wenzelm
parents: 31974
diff changeset
   434
  structure Induct = Induct
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24097
diff changeset
   435
  (
22139
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   436
    val cases_default = @{thm case_split}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   437
    val atomize = @{thms induct_atomize}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   438
    val rulify = @{thms induct_rulify}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   439
    val rulify_fallback = @{thms induct_rulify_fallback}
34989
b5c6e59e2cd7 Adapted to changes in setup of cases method.
berghofe
parents: 34914
diff changeset
   440
    val equal_def = @{thm induct_equal_def}
34914
e391c3de0f6b Adapted to changes in setup of induct method.
berghofe
parents: 32960
diff changeset
   441
    fun dest_def _ = NONE
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58889
diff changeset
   442
    fun trivial_tac _ _ = no_tac
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24097
diff changeset
   443
  );
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   444
\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   445
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24097
diff changeset
   446
declare case_split [cases type: o]
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   447
59940
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   448
end
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   449
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   450
ML_file "~~/src/Tools/case_product.ML"
41827
98eda7ffde79 setup case_product attribute in HOL and FOL
noschinl
parents: 41779
diff changeset
   451
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   452
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   453
hide_const (open) eq
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   454
4854
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
   455
end