doc-src/TutorialI/Sets/Recur.thy
author wenzelm
Mon, 02 May 2011 22:31:46 +0200
changeset 42637 381fdcab0f36
parent 36745 403585a89772
child 48611 b34ff75c23a7
permissions -rw-r--r--
eliminated old CVS Ids;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 10341
diff changeset
     1
theory Recur imports Main begin
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     2
36745
403585a89772 unified/simplified Pretty.margin_default;
wenzelm
parents: 16417
diff changeset
     3
ML "Pretty.margin_default := 64"
10294
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     4
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     5
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     6
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     7
@{thm[display] mono_def[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     8
\rulename{mono_def}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
     9
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    10
@{thm[display] monoI[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    11
\rulename{monoI}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    12
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    13
@{thm[display] monoD[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    14
\rulename{monoD}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    15
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    16
@{thm[display] lfp_unfold[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    17
\rulename{lfp_unfold}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    18
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    19
@{thm[display] lfp_induct[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    20
\rulename{lfp_induct}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    21
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    22
@{thm[display] gfp_unfold[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    23
\rulename{gfp_unfold}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    24
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    25
@{thm[display] coinduct[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    26
\rulename{coinduct}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    27
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    28
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    29
text{*\noindent
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    30
A relation $<$ is
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    31
\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    32
a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    33
of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    34
of an equation and $r$ the argument of some recursive call on the
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    35
corresponding right-hand side, induces a wellfounded relation. 
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    36
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    37
The HOL library formalizes
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    38
some of the theory of wellfounded relations. For example
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    39
@{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    40
wellfounded.
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    41
Finally we should mention that HOL already provides the mother of all
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    42
inductions, \textbf{wellfounded
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    43
induction}\indexbold{induction!wellfounded}\index{wellfounded
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    44
induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    45
@{thm[display]wf_induct[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    46
where @{term"wf r"} means that the relation @{term r} is wellfounded
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    47
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    48
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    49
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    50
text{*
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    51
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    52
@{thm[display] wf_induct[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    53
\rulename{wf_induct}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    54
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    55
@{thm[display] less_than_iff[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    56
\rulename{less_than_iff}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    57
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    58
@{thm[display] inv_image_def[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    59
\rulename{inv_image_def}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    60
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    61
@{thm[display] measure_def[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    62
\rulename{measure_def}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    63
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    64
@{thm[display] wf_less_than[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    65
\rulename{wf_less_than}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    66
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    67
@{thm[display] wf_inv_image[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    68
\rulename{wf_inv_image}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    69
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    70
@{thm[display] wf_measure[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    71
\rulename{wf_measure}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    72
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    73
@{thm[display] lex_prod_def[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    74
\rulename{lex_prod_def}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    75
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    76
@{thm[display] wf_lex_prod[no_vars]}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    77
\rulename{wf_lex_prod}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    78
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    79
*}
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    80
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    81
end
2ec9c808a8a7 the Sets chapter and theories
paulson
parents:
diff changeset
    82