# Theory Common_Patterns

theory Common_Patterns
imports Main

section

theory Common_Patterns
imports Main
begin

text

subsection

subsubsection

text

lemma
fixes n :: nat
and x :: 'a
assumes
shows  using
proof (induct n arbitrary: x)
case 0
note prem =
show  \<proof>
next
case (Suc n)
note hyp =
and prem =
show  \<proof>
qed

subsubsection

text

lemma
fixes a ::
assumes
shows  using
proof (induct n   arbitrary: x)
case 0
note prem =
and defn =
show  \<proof>
next
case (Suc n)
note hyp =
and prem =
and defn =
show  \<proof>
qed

text

subsubsection

text

lemma
fixes n :: nat
shows  and
proof (induct n)
case 0 case 1
show  \<proof>
next
case 0 case 2
show  \<proof>
next
case (Suc n) case 1
note hyps =
show  \<proof>
next
case (Suc n) case 2
note hyps =
show  \<proof>
qed

text

lemma
fixes n :: nat
shows
and
proof (induct n)
case 0
{
case 1
note
show  \<proof>
next
case 2
note
show  \<proof>
}
next
case (Suc n)
note
and
{
case 1
note
show  \<proof>
next
case 2
note
show  \<proof>
}
qed

subsubsection

text

lemma
fixes n :: nat
and x :: 'a
and y :: 'b
shows
and
proof (induct n arbitrary: x y)
case 0
{
case 1
note prem =
show  \<proof>
}
{
case 2
note prem =
show  \<proof>
}
next
case (Suc n)
note hyps =
then have some_intermediate_result \<proof>
{
case 1
note prem =
show  \<proof>
}
{
case 2
note prem =
show  \<proof>
}
qed

text

subsection

text

datatype foo = Foo1 nat | Foo2 bar
and bar = Bar1 bool | Bar2 bazar
and bazar = Bazar foo

text

lemma
fixes foo :: foo
and bar :: bar
and bazar :: bazar
shows
and
and
proof (induct foo and bar and bazar)
case (Foo1 n)
show  \<proof>
next
case (Foo2 bar)
note
show  \<proof>
next
case (Bar1 b)
show  \<proof>
next
case (Bar2 bazar)
note
show  \<proof>
next
case (Bazar foo)
note
show  \<proof>
qed

text

lemma
fixes x :: 'a and y :: 'b and z :: 'c
and foo :: foo
and bar :: bar
and bazar :: bazar
shows

and

and

proof (induct foo and bar and bazar arbitrary: x and y and z)
oops

subsection

text

inductive Even ::  where
zero:
| double:  if  for n

lemma
assumes
shows
using assms
proof induct
case zero
show  \<proof>
next
case (double n)
note  and
show  \<proof>
qed

text

lemma
proof (induct rule: Even.induct)
oops

text

lemma
assumes
shows  and
using assms
proof induct
case zero
{
case 1
show  \<proof>
next
case 2
show  \<proof>
}
next
case (double n)
note  and  and
{
case 1
show  \<proof>
next
case 2
show  \<proof>
}
qed

text

inductive Evn ::  and Odd ::
where
zero:
| succ_Evn:  if  for n
| succ_Odd:  if  for n

lemma

and

proof (induct rule: Evn_Odd.inducts)
case zero
{ case 1 show  \<proof> }
{ case 2 show  \<proof> }
{ case 3 show  \<proof> }
next
case (succ_Evn n)
note  and
{ case 1 show  \<proof> }
{ case 2 show  \<proof> }
next
case (succ_Odd n)
note  and
{ case 1 show  \<proof> }
{ case 2 show  \<proof> }
{ case 3 show  \<proof> }
qed

text

inductive star ::  for r
where
refl:  for x
| step:  if  and  for x y z

text

lemmas star_induct = star.induct [case_names base step[r _ IH]]

lemma
proof (induct rule: star_induct) print_cases
case base
then show ?case .
next
case (step a b c) print_facts
from step.prems have  by (rule step.IH)
with step.r show ?case by (rule star.step)
qed

end