src/Doc/Tutorial/Datatype/Fundata.thy
author desharna
Fri, 27 May 2022 16:16:45 +0200
changeset 75466 5f2a1efd0560
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
added predicate totalp_on and abbreviation totalp
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14188
diff changeset
     2
theory Fundata imports Main begin
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     3
(*>*)
58305
57752a91eec4 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents: 48985
diff changeset
     4
datatype (dead 'a,'i) bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
     6
text\<open>\noindent
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
     7
Parameter \<^typ>\<open>'a\<close> is the type of values stored in
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
     8
the \<^term>\<open>Br\<close>anches of the tree, whereas \<^typ>\<open>'i\<close> is the index
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
     9
type over which the tree branches. If \<^typ>\<open>'i\<close> is instantiated to
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    10
\<^typ>\<open>bool\<close>, the result is a binary tree; if it is instantiated to
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    11
\<^typ>\<open>nat\<close>, we have an infinitely branching tree because each node
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    12
has as many subtrees as there are natural numbers. How can we possibly
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 8771
diff changeset
    13
write down such a tree? Using functional notation! For example, the term
12631
wenzelm
parents: 11458
diff changeset
    14
@{term[display]"Br (0::nat) (\<lambda>i. Br i (\<lambda>n. Tip))"}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    15
of type \<^typ>\<open>(nat,nat)bigtree\<close> is the tree whose
8771
026f37a86ea7 *** empty log message ***
nipkow
parents: 8745
diff changeset
    16
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    17
has merely \<^term>\<open>Tip\<close>s as further subtrees.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    19
Function \<^term>\<open>map_bt\<close> applies a function to all labels in a \<open>bigtree\<close>:
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    20
\<close>
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
27015
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    22
primrec map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    23
where
f8537d69f514 *** empty log message ***
nipkow
parents: 16417
diff changeset
    24
"map_bt f Tip      = Tip" |
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    25
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    27
text\<open>\noindent This is a valid \isacommand{primrec} definition because the
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    28
recursive calls of \<^term>\<open>map_bt\<close> involve only subtrees of
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    29
\<^term>\<open>F\<close>, which is itself a subterm of the left-hand side. Thus termination
14188
f471cd4c7282 *** empty log message ***
nipkow
parents: 13439
diff changeset
    30
is assured.  The seasoned functional programmer might try expressing
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    31
\<^term>\<open>%i. map_bt f (F i)\<close> as \<^term>\<open>map_bt f o F\<close>, which Isabelle 
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    32
however will reject.  Applying \<^term>\<open>map_bt\<close> to only one of its arguments
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 11309
diff changeset
    33
makes the termination proof less obvious.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    35
The following lemma has a simple proof by induction:\<close>
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 58305
diff changeset
    37
lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
10171
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    38
apply(induct_tac T, simp_all)
59d6633835fa *** empty log message ***
nipkow
parents: 9933
diff changeset
    39
done
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 58305
diff changeset
    40
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    41
apply(induct_tac T, rename_tac[2] F)(*>*)
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    42
txt\<open>\noindent
13439
2f98365f57a8 *** empty log message ***
nipkow
parents: 12631
diff changeset
    43
Because of the function type, the proof state after induction looks unusual.
10795
9e888d60d3e5 minor edits to Chapters 1-3
paulson
parents: 10420
diff changeset
    44
Notice the quantified induction hypothesis:
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    45
@{subgoals[display,indent=0]}
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    46
\<close>
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
(*<*)
10420
ef006735bee8 *** empty log message ***
nipkow
parents: 10171
diff changeset
    48
oops
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
(*>*)