src/FOL/FOL.thy
author wenzelm
Tue, 31 Jan 2023 19:27:02 +0100
changeset 77157 c0633a0da53e
parent 74563 042041c0ebeb
child 80701 39cd50407f79
permissions -rw-r--r--
clarified GUI events: reset everything on session context switch;
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
73015
2d7060a3ea11 tuned whitespace;
wenzelm
parents: 71959
diff changeset
     8
  imports IFOL
2d7060a3ea11 tuned whitespace;
wenzelm
parents: 71959
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
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
    12
ML_file \<open>~~/src/Provers/classical.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
    13
ML_file \<open>~~/src/Provers/blast.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
    14
ML_file \<open>~~/src/Provers/clasimp.ML\<close>
48891
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    20
  classical: \<open>(\<not> P \<Longrightarrow> P) \<Longrightarrow> P\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    25
lemma ccontr: \<open>(\<not> P \<Longrightarrow> False) \<Longrightarrow> P\<close>
21539
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    31
lemma disjCI: \<open>(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    39
  assumes r: \<open>\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    40
  shows \<open>\<exists>x. P(x)\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    47
  assumes r: \<open>\<forall>x. \<not> P(x) \<Longrightarrow> P(a)\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    48
  shows \<open>\<exists>x. P(x)\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    55
lemma excluded_middle: \<open>\<not> P \<or> P\<close>
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]:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    61
  assumes r1: \<open>P \<Longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    62
    and r2: \<open>\<not> P \<Longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    63
  shows \<open>Q\<close>
21539
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>
74563
042041c0ebeb clarified modules;
wenzelm
parents: 74300
diff changeset
    75
  Args.goal_spec -- Scan.lift (Parse.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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    84
  assumes major: \<open>P \<longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    85
    and r1: \<open>\<not> P \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    86
    and r2: \<open>Q \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    87
  shows \<open>R\<close>
21539
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':
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
    99
  assumes major: \<open>P \<longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   100
    and r1: \<open>Q \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   101
    and r2: \<open>\<not> P \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   102
  shows \<open>R\<close>
21539
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>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   110
lemma notnotD: \<open>\<not> \<not> P \<Longrightarrow> P\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   116
lemma contrapos2:  \<open>\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   130
  assumes major: \<open>P \<longleftrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   131
    and r1: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   132
    and r2: \<open>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   133
  shows \<open>R\<close>
21539
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   144
  assumes major: \<open>\<exists>! x. P(x)\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   145
    and r: \<open>\<And>x. \<lbrakk>P(x);  \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   146
  shows \<open>R\<close>
21539
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   150
  assume * : \<open>\<forall>y. P(y) \<longrightarrow> y = x\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   151
  assume \<open>P(x)\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   152
  then show \<open>R\<close>
21539
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'
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   156
      assume \<open>P(y)\<close> and \<open>P(y')\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   157
      with * have \<open>x = y\<close> and \<open>x = y'\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   158
        by - (tactic "IntPr.fast_tac \<^context> 1")+
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   159
      then have \<open>y = y'\<close> by (rule subst)
21539
c5cf9243ad62 converted legacy ML scripts;
wenzelm
parents: 20223
diff changeset
   160
    } note r' = this
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   161
    show \<open>\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<close>
61487
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   166
lemma imp_elim: \<open>P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   169
lemma swap: \<open>\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R\<close>
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
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
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
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
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
74300
33f13d2d211c clarified antiquotations;
wenzelm
parents: 73015
diff changeset
   206
    val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close>
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   207
    val equality_name = \<^const_name>\<open>eq\<close>
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   208
    val not_name = \<^const_name>\<open>Not\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   217
lemma ex1_functional: \<open>\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c\<close>
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>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   221
lemma True_implies_equals: \<open>(True \<Longrightarrow> PROP P) \<equiv> PROP P\<close>
20223
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   222
proof
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   223
  assume \<open>True \<Longrightarrow> PROP P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   224
  from this and TrueI show \<open>PROP P\<close> .
20223
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   225
next
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   226
  assume \<open>PROP P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   227
  then show \<open>PROP P\<close> .
20223
89d2758ecddf tuned proofs;
wenzelm
parents: 18816
diff changeset
   228
qed
9487
7e377f912629 improved comments;
wenzelm
parents: 8643
diff changeset
   229
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   230
lemma uncurry: \<open>P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   233
lemma iff_allI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   236
lemma iff_exI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   239
lemma all_comm: \<open>(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))\<close>
61487
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   242
lemma ex_comm: \<open>(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))\<close>
61487
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   254
lemma cases_simp: \<open>(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q\<close>
61487
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   270
  \<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   271
  \<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   272
  \<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   273
  \<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   278
  \<open>\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   279
  \<open>\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   286
  \<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   287
  \<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   288
  \<open>\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   289
  \<open>\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))\<close>
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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   294
  \<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   295
  \<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close>
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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   303
lemma imp_disj1: \<open>(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   304
lemma imp_disj2: \<open>Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   305
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   306
lemma de_Morgan_conj: \<open>(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)\<close> by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   307
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   308
lemma not_imp: \<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> by blast
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   309
lemma not_iff: \<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)\<close> by blast
26286
3ff5d257f175 added lemmas from simpdata.ML;
wenzelm
parents: 24830
diff changeset
   310
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   311
lemma not_all: \<open>(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> by blast
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   312
lemma imp_all: \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close> 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
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   323
lemma notFalseI: \<open>\<not> False\<close> 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:
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   326
  \<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   327
  \<open>P \<or> \<not> P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   328
  \<open>\<not> P \<or> P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   329
  \<open>\<not> \<not> P \<longleftrightarrow> P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   330
  \<open>(\<not> P \<longrightarrow> P) \<longleftrightarrow> P\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   331
  \<open>(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)\<close> 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
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
   338
ML_file \<open>simpdata.ML\<close>
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 42453
diff changeset
   339
71920
b0da0537f307 activate simproc for FOL
haftmann
parents: 71919
diff changeset
   340
simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_Ex\<close>
b0da0537f307 activate simproc for FOL
haftmann
parents: 71919
diff changeset
   341
simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_All\<close>
b0da0537f307 activate simproc for FOL
haftmann
parents: 71919
diff changeset
   342
simproc_setup defined_all("\<And>x. PROP P(x)") = \<open>K Quantifier1.rearrange_all\<close>
42455
6702c984bf5a modernized Quantifier1 simproc setup;
wenzelm
parents: 42453
diff changeset
   343
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   344
ML \<open>
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   345
(*intuitionistic simprules only*)
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   346
val IFOL_ss =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   347
  put_simpset FOL_basic_ss \<^context>
71959
ee2c7f0dd1be prefer single name
haftmann
parents: 71920
diff changeset
   348
  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all}
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   349
  addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   350
  |> Simplifier.add_cong @{thm imp_cong}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   351
  |> simpset_of;
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   352
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   353
(*classical simprules too*)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   354
val FOL_ss =
69593
3dda49e08b9d isabelle update -u control_cartouches;
wenzelm
parents: 69590
diff changeset
   355
  put_simpset IFOL_ss \<^context>
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51687
diff changeset
   356
  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
   357
  |> simpset_of;
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   358
\<close>
42453
cd5005020f4e clarified simpset setup;
wenzelm
parents: 41827
diff changeset
   359
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   360
setup \<open>
58826
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   361
  map_theory_simpset (put_simpset FOL_ss) #>
2ed2eaabe3df modernized setup;
wenzelm
parents: 55111
diff changeset
   362
  Simplifier.method_setup Splitter.split_modifiers
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   363
\<close>
52241
5f6e885382e9 tuned import;
wenzelm
parents: 51798
diff changeset
   364
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
   365
ML_file \<open>~~/src/Tools/eqsubst.ML\<close>
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15019
diff changeset
   366
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents: 15019
diff changeset
   367
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   368
subsection \<open>Other simple lemmas\<close>
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   369
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   370
lemma [simp]: \<open>((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   371
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   372
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   373
lemma [simp]: \<open>((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   374
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   375
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   376
lemma not_disj_iff_imp: \<open>\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   377
  by blast
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   378
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   379
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   380
subsubsection \<open>Monotonicity of implications\<close>
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   381
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   382
lemma conj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   383
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   384
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   385
lemma disj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   386
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   387
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   388
lemma imp_mono: \<open>\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   389
  by fast (*or (IntPr.fast_tac 1)*)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   390
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   391
lemma imp_refl: \<open>P \<longrightarrow> P\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   392
  by (rule impI)
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   393
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   394
text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close>
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   395
lemma ex_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   396
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   397
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   398
lemma all_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))\<close>
61487
f8cb97e0fd0b more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents: 60770
diff changeset
   399
  by blast
14085
8dc3e532959a moved some lemmas here from ZF
paulson
parents: 13550
diff changeset
   400
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   401
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   402
subsection \<open>Proof by cases and induction\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   403
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   404
text \<open>Proper handling of non-atomic rule statements.\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   405
59940
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   406
context
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   407
begin
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   408
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   409
qualified definition \<open>induct_forall(P) \<equiv> \<forall>x. P(x)\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   410
qualified definition \<open>induct_implies(A, B) \<equiv> A \<longrightarrow> B\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   411
qualified definition \<open>induct_equal(x, y) \<equiv> x = y\<close>
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   412
qualified definition \<open>induct_conj(A, B) \<equiv> A \<and> B\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   413
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   414
lemma induct_forall_eq: \<open>(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))\<close>
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   415
  unfolding atomize_all induct_forall_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   416
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   417
lemma induct_implies_eq: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))\<close>
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   418
  unfolding atomize_imp induct_implies_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   419
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   420
lemma induct_equal_eq: \<open>(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))\<close>
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   421
  unfolding atomize_eq induct_equal_def .
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   422
69590
e65314985426 isabelle update_inner_syntax_cartouches;
wenzelm
parents: 63120
diff changeset
   423
lemma induct_conj_eq: \<open>(A &&& B) \<equiv> Trueprop(induct_conj(A, B))\<close>
18816
aebd7f315b92 tuned proofs;
wenzelm
parents: 18595
diff changeset
   424
  unfolding atomize_conj induct_conj_def .
11988
8340fb172607 induct_impliesI;
wenzelm
parents: 11848
diff changeset
   425
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   426
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
45594
wenzelm
parents: 43560
diff changeset
   427
lemmas induct_rulify [symmetric] = induct_atomize
18456
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   428
lemmas induct_rulify_fallback =
8cc35e95450a updated auxiliary facts for induct method;
wenzelm
parents: 16417
diff changeset
   429
  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
   430
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   431
text \<open>Method setup.\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   432
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
   433
ML_file \<open>~~/src/Tools/induct.ML\<close>
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   434
ML \<open>
32171
220abde9962b renamed functor InductFun to Induct;
wenzelm
parents: 31974
diff changeset
   435
  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
   436
  (
22139
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   437
    val cases_default = @{thm case_split}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   438
    val atomize = @{thms induct_atomize}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   439
    val rulify = @{thms induct_rulify}
539a63b98f76 tuned ML setup;
wenzelm
parents: 21539
diff changeset
   440
    val rulify_fallback = @{thms induct_rulify_fallback}
34989
b5c6e59e2cd7 Adapted to changes in setup of cases method.
berghofe
parents: 34914
diff changeset
   441
    val equal_def = @{thm induct_equal_def}
34914
e391c3de0f6b Adapted to changes in setup of induct method.
berghofe
parents: 32960
diff changeset
   442
    fun dest_def _ = NONE
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58889
diff changeset
   443
    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
   444
  );
60770
240563fbf41d isabelle update_cartouches;
wenzelm
parents: 59990
diff changeset
   445
\<close>
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   446
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24097
diff changeset
   447
declare case_split [cases type: o]
11678
6aa3e2d26683 moved atomize stuff to theory IFOL;
wenzelm
parents: 11096
diff changeset
   448
59940
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   449
end
087d81f5213e local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents: 59780
diff changeset
   450
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 69597
diff changeset
   451
ML_file \<open>~~/src/Tools/case_product.ML\<close>
41827
98eda7ffde79 setup case_product attribute in HOL and FOL
noschinl
parents: 41779
diff changeset
   452
41310
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   453
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   454
hide_const (open) eq
65631ca437c9 proper identifiers for consts and types;
wenzelm
parents: 36866
diff changeset
   455
4854
d1850e0964f2 tuned setup;
wenzelm
parents: 4793
diff changeset
   456
end