author  desharna 
Fri, 27 May 2022 16:16:45 +0200  
changeset 75466  5f2a1efd0560 
parent 69597  ff784d5a5bfb 
permissions  rwrr 
8745  1 
(*<*) 
16417  2 
theory Fundata imports Main begin 
8745  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  5 

67406  6 
text\<open>\noindent 
69597  7 
Parameter \<^typ>\<open>'a\<close> is the type of values stored in 
8 
the \<^term>\<open>Br\<close>anches of the tree, whereas \<^typ>\<open>'i\<close> is the index 

9 
type over which the tree branches. If \<^typ>\<open>'i\<close> is instantiated to 

10 
\<^typ>\<open>bool\<close>, the result is a binary tree; if it is instantiated to 

11 
\<^typ>\<open>nat\<close>, we have an infinitely branching tree because each node 

8745  12 
has as many subtrees as there are natural numbers. How can we possibly 
9541  13 
write down such a tree? Using functional notation! For example, the term 
12631  14 
@{term[display]"Br (0::nat) (\<lambda>i. Br i (\<lambda>n. Tip))"} 
69597  15 
of type \<^typ>\<open>(nat,nat)bigtree\<close> is the tree whose 
8771  16 
root is labeled with 0 and whose $i$th subtree is labeled with $i$ and 
69597  17 
has merely \<^term>\<open>Tip\<close>s as further subtrees. 
8745  18 

69597  19 
Function \<^term>\<open>map_bt\<close> applies a function to all labels in a \<open>bigtree\<close>: 
67406  20 
\<close> 
8745  21 

27015  22 
primrec map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree" 
23 
where 

24 
"map_bt f Tip = Tip"  

10420  25 
"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))" 
8745  26 

67406  27 
text\<open>\noindent This is a valid \isacommand{primrec} definition because the 
69597  28 
recursive calls of \<^term>\<open>map_bt\<close> involve only subtrees of 
29 
\<^term>\<open>F\<close>, which is itself a subterm of the lefthand side. Thus termination 

14188  30 
is assured. The seasoned functional programmer might try expressing 
69597  31 
\<^term>\<open>%i. map_bt f (F i)\<close> as \<^term>\<open>map_bt f o F\<close>, which Isabelle 
32 
however will reject. Applying \<^term>\<open>map_bt\<close> to only one of its arguments 

11458  33 
makes the termination proof less obvious. 
8745  34 

67406  35 
The following lemma has a simple proof by induction:\<close> 
8745  36 

58860  37 
lemma "map_bt (g o f) T = map_bt g (map_bt f T)" 
10171  38 
apply(induct_tac T, simp_all) 
39 
done 

58860  40 
(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)" 
10420  41 
apply(induct_tac T, rename_tac[2] F)(*>*) 
67406  42 
txt\<open>\noindent 
13439  43 
Because of the function type, the proof state after induction looks unusual. 
10795  44 
Notice the quantified induction hypothesis: 
10420  45 
@{subgoals[display,indent=0]} 
67406  46 
\<close> 
8745  47 
(*<*) 
10420  48 
oops 
8745  49 
end 
50 
(*>*) 