src/HOL/Induct/Common_Patterns.thy
author wenzelm
Sun, 16 Sep 2007 21:18:43 +0200
changeset 24609 3f238d4987c0
parent 24608 aae1095dbe3b
child 29961 c7849326100e
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24608
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Common_Patterns.thy
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     4
*)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     5
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     6
header {* Common patterns of induction *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     7
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     8
theory Common_Patterns
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
     9
imports Main
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    10
begin
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    11
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    12
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    13
  The subsequent Isar proof schemes illustrate common proof patterns
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    14
  supported by the generic @{text "induct"} method.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    15
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    16
  To demonstrate variations on statement (goal) structure we refer to
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    17
  the induction rule of Peano natural numbers: @{thm nat.induct
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    18
  [no_vars]}, which is the simplest case of datatype induction.  We
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    19
  shall also see more complex (mutual) datatype inductions involving
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    20
  several rules.  Working with inductive predicates is similar, but
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    21
  involves explicit facts about membership, instead of implicit
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    22
  syntactic typing.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    23
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    24
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    25
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    26
subsection {* Variations on statement structure *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    27
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    28
subsubsection {* Local facts and parameters *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    29
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    30
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    31
  Augmenting a problem by additional facts and locally fixed variables
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    32
  is a bread-and-butter method in many applications.  This is where
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    33
  unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    34
  the past.  The @{text "induct"} method works with primary means of
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    35
  the proof language instead.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    36
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    37
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    38
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    39
  fixes n :: nat
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    40
    and x :: 'a
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    41
  assumes "A n x"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    42
  shows "P n x" using `A n x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    43
proof (induct n arbitrary: x)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    44
  case 0
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    45
  note prem = `A 0 x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    46
  show "P 0 x" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    47
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    48
  case (Suc n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    49
  note hyp = `\<And>x. A n x \<Longrightarrow> P n x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    50
    and prem = `A (Suc n) x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    51
  show "P (Suc n) x" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    52
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    53
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    54
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    55
subsubsection {* Local definitions *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    56
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    57
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    58
  Here the idea is to turn sub-expressions of the problem into a
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    59
  defined induction variable.  This is often accompanied with fixing
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    60
  of auxiliary parameters in the original expression, otherwise the
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    61
  induction step would refer invariably to particular entities.  This
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    62
  combination essentially expresses a partially abstracted
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    63
  representation of inductive expressions.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    64
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    65
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    66
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    67
  fixes a :: "'a \<Rightarrow> nat"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    68
  assumes "A (a x)"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    69
  shows "P (a x)" using `A (a x)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    70
proof (induct n \<equiv> "a x" arbitrary: x)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    71
  case 0
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    72
  note prem = `A (a x)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    73
    and defn = `0 = a x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    74
  show "P (a x)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    75
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    76
  case (Suc n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    77
  note hyp = `\<And>x. A (a x) \<Longrightarrow> n = a x \<Longrightarrow> P (a x)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    78
    and prem = `A (a x)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    79
    and defn = `Suc n = a x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    80
  show "P (a x)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    81
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    82
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    83
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    84
  Observe how the local definition @{text "n = a x"} recurs in the
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    85
  inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"},
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    86
  according to underlying induction rule.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    87
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    88
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    89
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    90
subsubsection {* Simple simultaneous goals *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    91
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    92
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    93
  The most basic simultaneous induction operates on several goals
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    94
  one-by-one, where each case refers to induction hypotheses that are
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    95
  duplicated according to the number of conclusions.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    96
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    97
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    98
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
    99
  fixes n :: nat
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   100
  shows "P n" and "Q n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   101
proof (induct n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   102
  case 0 case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   103
  show "P 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   104
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   105
  case 0 case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   106
  show "Q 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   107
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   108
  case (Suc n) case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   109
  note hyps = `P n` `Q n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   110
  show "P (Suc n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   111
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   112
  case (Suc n) case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   113
  note hyps = `P n` `Q n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   114
  show "Q (Suc n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   115
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   116
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   117
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   118
  The split into subcases may be deferred as follows -- this is
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   119
  particularly relevant for goal statements with local premises.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   120
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   121
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   122
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   123
  fixes n :: nat
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   124
  shows "A n \<Longrightarrow> P n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   125
    and "B n \<Longrightarrow> Q n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   126
proof (induct n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   127
  case 0
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   128
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   129
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   130
    note `A 0`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   131
    show "P 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   132
  next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   133
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   134
    note `B 0`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   135
    show "Q 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   136
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   137
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   138
  case (Suc n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   139
  note `A n \<Longrightarrow> P n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   140
    and `B n \<Longrightarrow> Q n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   141
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   142
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   143
    note `A (Suc n)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   144
    show "P (Suc n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   145
  next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   146
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   147
    note `B (Suc n)`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   148
    show "Q (Suc n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   149
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   150
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   151
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   152
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   153
subsubsection {* Compound simultaneous goals *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   154
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   155
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   156
  The following pattern illustrates the slightly more complex
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   157
  situation of simultaneous goals with individual local assumptions.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   158
  In compound simultaneous statements like this, local assumptions
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   159
  need to be included into each goal, using @{text "\<Longrightarrow>"} of the Pure
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   160
  framework.  In contrast, local parameters do not require separate
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   161
  @{text "\<And>"} prefixes here, but may be moved into the common context
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   162
  of the whole statement.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   163
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   164
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   165
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   166
  fixes n :: nat
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   167
    and x :: 'a
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   168
    and y :: 'b
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   169
  shows "A n x \<Longrightarrow> P n x"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   170
    and "B n y \<Longrightarrow> Q n y"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   171
proof (induct n arbitrary: x y)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   172
  case 0
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   173
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   174
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   175
    note prem = `A 0 x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   176
    show "P 0 x" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   177
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   178
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   179
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   180
    note prem = `B 0 y`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   181
    show "Q 0 y" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   182
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   183
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   184
  case (Suc n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   185
  note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   186
  then have some_intermediate_result sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   187
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   188
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   189
    note prem = `A (Suc n) x`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   190
    show "P (Suc n) x" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   191
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   192
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   193
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   194
    note prem = `B (Suc n) y`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   195
    show "Q (Suc n) y" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   196
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   197
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   198
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   199
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   200
  Here @{text "induct"} provides again nested cases with numbered
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   201
  sub-cases, which allows to share common parts of the body context.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   202
  In typical applications, there could be a long intermediate proof of
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   203
  general consequences of the induction hypotheses, before finishing
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   204
  each conclusion separately.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   205
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   206
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   207
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   208
subsection {* Multiple rules *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   209
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   210
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   211
  Multiple induction rules emerge from mutual definitions of
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   212
  datatypes, inductive predicates, functions etc.  The @{text
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   213
  "induct"} method accepts replicated arguments (with @{text "and"}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   214
  separator), corresponding to each projection of the induction
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   215
  principle.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   216
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   217
  The goal statement essentially follows the same arrangement,
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   218
  although it might be subdivided into simultaneous sub-problems as
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   219
  before!
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   220
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   221
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   222
datatype foo = Foo1 nat | Foo2 bar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   223
  and bar = Bar1 bool | Bar2 bazar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   224
  and bazar = Bazar foo
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   225
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   226
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   227
  The pack of induction rules for this datatype is: @{thm [display]
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   228
  foo_bar_bazar.inducts [no_vars]}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   229
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   230
  This corresponds to the following basic proof pattern:
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   231
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   232
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   233
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   234
  fixes foo :: foo
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   235
    and bar :: bar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   236
    and bazar :: bazar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   237
  shows "P foo"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   238
    and "Q bar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   239
    and "R bazar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   240
proof (induct foo and bar and bazar)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   241
  case (Foo1 n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   242
  show "P (Foo1 n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   243
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   244
  case (Foo2 bar)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   245
  note `Q bar`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   246
  show "P (Foo2 bar)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   247
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   248
  case (Bar1 b)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   249
  show "Q (Bar1 b)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   250
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   251
  case (Bar2 bazar)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   252
  note `R bazar`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   253
  show "Q (Bar2 bazar)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   254
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   255
  case (Bazar foo)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   256
  note `P foo`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   257
  show "R (Bazar foo)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   258
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   259
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   260
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   261
  This can be combined with the previous techniques for compound
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   262
  statements, e.g.\ like this.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   263
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   264
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   265
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   266
  fixes x :: 'a and y :: 'b and z :: 'c
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   267
    and foo :: foo
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   268
    and bar :: bar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   269
    and bazar :: bazar
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   270
  shows
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   271
    "A x foo \<Longrightarrow> P x foo"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   272
  and
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   273
    "B1 y bar \<Longrightarrow> Q1 y bar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   274
    "B2 y bar \<Longrightarrow> Q2 y bar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   275
  and
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   276
    "C1 z bazar \<Longrightarrow> R1 z bazar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   277
    "C2 z bazar \<Longrightarrow> R2 z bazar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   278
    "C3 z bazar \<Longrightarrow> R3 z bazar"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   279
proof (induct foo and bar and bazar arbitrary: x and y and z)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   280
  oops
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   281
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   282
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   283
subsection {* Inductive predicates *}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   284
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   285
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   286
  The most basic form of induction involving predicates (or sets)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   287
  essentially eliminates a given membership fact.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   288
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   289
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   290
inductive Even :: "nat \<Rightarrow> bool" where
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   291
  zero: "Even 0"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   292
| double: "Even n \<Longrightarrow> Even (2 * n)"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   293
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   294
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   295
  assumes "Even n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   296
  shows "P n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   297
  using assms
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   298
proof induct
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   299
  case zero
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   300
  show "P 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   301
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   302
  case (double n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   303
  note `Even n` and `P n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   304
  show "P (2 * n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   305
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   306
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   307
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   308
  Alternatively, an initial rule statement may be proven as follows,
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   309
  performing ``in-situ'' elimination with explicit rule specification.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   310
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   311
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   312
lemma "Even n \<Longrightarrow> P n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   313
proof (induct rule: Even.induct)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   314
  oops
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   315
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   316
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   317
  Simultaneous goals do not introduce anything new.
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   318
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   319
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   320
lemma
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   321
  assumes "Even n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   322
  shows "P1 n" and "P2 n"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   323
  using assms
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   324
proof induct
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   325
  case zero
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   326
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   327
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   328
    show "P1 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   329
  next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   330
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   331
    show "P2 0" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   332
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   333
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   334
  case (double n)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   335
  note `Even n` and `P1 n` and `P2 n`
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   336
  {
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   337
    case 1
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   338
    show "P1 (2 * n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   339
  next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   340
    case 2
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   341
    show "P2 (2 * n)" sorry
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   342
  }
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   343
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   344
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   345
text {*
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   346
  Working with mutual rules requires special care in composing the
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   347
  statement as a two-level conjunction, using lists of propositions
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   348
  separated by @{text "and"}.  For example:
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   349
*}
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   350
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   351
inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   352
where
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   353
  zero: "Evn 0"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   354
| succ_Evn: "Evn n \<Longrightarrow> Odd (Suc n)"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   355
| succ_Odd: "Odd n \<Longrightarrow> Evn (Suc n)"
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   356
24609
wenzelm
parents: 24608
diff changeset
   357
lemma
wenzelm
parents: 24608
diff changeset
   358
    "Evn n \<Longrightarrow> P1 n"
wenzelm
parents: 24608
diff changeset
   359
    "Evn n \<Longrightarrow> P2 n"
wenzelm
parents: 24608
diff changeset
   360
    "Evn n \<Longrightarrow> P3 n"
wenzelm
parents: 24608
diff changeset
   361
  and
wenzelm
parents: 24608
diff changeset
   362
    "Odd n \<Longrightarrow> Q1 n"
wenzelm
parents: 24608
diff changeset
   363
    "Odd n \<Longrightarrow> Q2 n"
24608
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   364
proof (induct rule: Evn_Odd.inducts)
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   365
  case zero
24609
wenzelm
parents: 24608
diff changeset
   366
  { case 1 show "P1 0" sorry }
wenzelm
parents: 24608
diff changeset
   367
  { case 2 show "P2 0" sorry }
wenzelm
parents: 24608
diff changeset
   368
  { case 3 show "P3 0" sorry }
24608
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   369
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   370
  case (succ_Evn n)
24609
wenzelm
parents: 24608
diff changeset
   371
  note `Evn n` and `P1 n` `P2 n` `P3 n`
wenzelm
parents: 24608
diff changeset
   372
  { case 1 show "Q1 (Suc n)" sorry }
wenzelm
parents: 24608
diff changeset
   373
  { case 2 show "Q2 (Suc n)" sorry }
24608
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   374
next
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   375
  case (succ_Odd n)
24609
wenzelm
parents: 24608
diff changeset
   376
  note `Odd n` and `Q1 n` `Q2 n`
wenzelm
parents: 24608
diff changeset
   377
  { case 1 show "P1 (Suc n)" sorry }
wenzelm
parents: 24608
diff changeset
   378
  { case 2 show "P2 (Suc n)" sorry }
wenzelm
parents: 24608
diff changeset
   379
  { case 3 show "P3 (Suc n)" sorry }
24608
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   380
qed
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   381
aae1095dbe3b HOL/Induct/Common_Patterns.thy
wenzelm
parents:
diff changeset
   382
end