author  desharna 
Fri, 27 May 2022 16:16:45 +0200  
changeset 75466  5f2a1efd0560 
parent 69597  ff784d5a5bfb 
permissions  rwrr 
8745  1 
(*<*) 
16417  2 
theory Nested imports ABexpr begin 
8745  3 
(*>*) 
4 

67406  5 
text\<open> 
11458  6 
\index{datatypes!and nested recursion}% 
8745  7 
So far, all datatypes had the property that on the righthand side of their 
11458  8 
definition they occurred only at the toplevel: directly below a 
11256  9 
constructor. Now we consider \emph{nested recursion}, where the recursive 
11310  10 
datatype occurs nested in some other datatype (but not inside itself!). 
11256  11 
Consider the following model of terms 
8745  12 
where function symbols can be applied to a list of arguments: 
67406  13 
\<close> 
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
27318
diff
changeset

14 
(*<*)hide_const Var(*>*) 
58860  15 
datatype ('v,'f)"term" = Var 'v  App 'f "('v,'f)term list" 
8745  16 

67406  17 
text\<open>\noindent 
69505  18 
Note that we need to quote \<open>term\<close> on the left to avoid confusion with 
10171  19 
the Isabelle command \isacommand{term}. 
69597  20 
Parameter \<^typ>\<open>'v\<close> is the type of variables and \<^typ>\<open>'f\<close> the type of 
8745  21 
function symbols. 
69597  22 
A mathematical term like $f(x,g(y))$ becomes \<^term>\<open>App f [Var x, App g 
23 
[Var y]]\<close>, where \<^term>\<open>f\<close>, \<^term>\<open>g\<close>, \<^term>\<open>x\<close>, \<^term>\<open>y\<close> are 

8745  24 
suitable values, e.g.\ numbers or strings. 
25 

69505  26 
What complicates the definition of \<open>term\<close> is the nested occurrence of 
27 
\<open>term\<close> inside \<open>list\<close> on the righthand side. In principle, 

8745  28 
nested recursion can be eliminated in favour of mutual recursion by unfolding 
69505  29 
the offending datatypes, here \<open>list\<close>. The result for \<open>term\<close> 
8745  30 
would be something like 
8751  31 
\medskip 
32 

48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48523
diff
changeset

33 
\input{unfoldnested.tex} 
8751  34 
\medskip 
35 

36 
\noindent 

8745  37 
Although we do not recommend this unfolding to the user, it shows how to 
38 
simulate nested recursion by mutual recursion. 

69505  39 
Now we return to the initial definition of \<open>term\<close> using 
8745  40 
nested recursion. 
41 

42 
Let us define a substitution function on terms. Because terms involve term 

43 
lists, we need to define two substitution functions simultaneously: 

67406  44 
\<close> 
8745  45 

27015  46 
primrec 
47 
subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term" and 

48 
substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list" 

49 
where 

50 
"subst s (Var x) = s x"  

51 
subst_App: 

52 
"subst s (App f ts) = App f (substs s ts)"  

8745  53 

27015  54 
"substs s [] = []"  
55 
"substs s (t # ts) = subst s t # substs s ts" 

8745  56 

67406  57 
text\<open>\noindent 
11458  58 
Individual equations in a \commdx{primrec} definition may be 
59 
named as shown for @{thm[source]subst_App}. 

10171  60 
The significance of this device will become apparent below. 
9644  61 

8745  62 
Similarly, when proving a statement about terms inductively, we need 
63 
to prove a related statement about term lists simultaneously. For example, 

64 
the fact that the identity substitution does not change a term needs to be 

65 
strengthened and proved as follows: 

67406  66 
\<close> 
8745  67 

12334  68 
lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and> 
58860  69 
substs Var ts = (ts::('v,'f)term list)" 
70 
apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all) 

10171  71 
done 
8745  72 

67406  73 
text\<open>\noindent 
69597  74 
Note that \<^term>\<open>Var\<close> is the identity substitution because by definition it 
75 
leaves variables unchanged: \<^prop>\<open>subst Var (Var x) = Var x\<close>. Note also 

8745  76 
that the type annotations are necessary because otherwise there is nothing in 
77 
the goal to enforce that both halves of the goal talk about the same type 

69505  78 
parameters \<open>('v,'f)\<close>. As a result, induction would fail 
8745  79 
because the two halves of the goal would be unrelated. 
80 

81 
\begin{exercise} 

82 
The fact that substitution distributes over composition can be expressed 

83 
roughly as follows: 

10178  84 
@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"} 
8745  85 
Correct this statement (you will find that it does not typecheck), 
69505  86 
strengthen it, and prove it. (Note: \<open>\<circ>\<close> is function composition; 
9792  87 
its definition is found in theorem @{thm[source]o_def}). 
8745  88 
\end{exercise} 
9644  89 
\begin{exercise}\label{ex:trevtrev} 
69597  90 
Define a function \<^term>\<open>trev\<close> of type \<^typ>\<open>('v,'f)term => ('v,'f)term\<close> 
9792  91 
that recursively reverses the order of arguments of all function symbols in a 
69597  92 
term. Prove that \<^prop>\<open>trev(trev t) = t\<close>. 
9644  93 
\end{exercise} 
94 

10795  95 
The experienced functional programmer may feel that our definition of 
69597  96 
\<^term>\<open>subst\<close> is too complicated in that \<^const>\<open>substs\<close> is 
97 
unnecessary. The \<^term>\<open>App\<close>case can be defined directly as 

9644  98 
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} 
69597  99 
where \<^term>\<open>map\<close> is the standard list function such that 
69505  100 
\<open>map f [x1,...,xn] = [f x1,...,f xn]\<close>. This is true, but Isabelle 
10795  101 
insists on the conjunctive format. Fortunately, we can easily \emph{prove} 
9792  102 
that the suggested equation holds: 
67406  103 
\<close> 
12334  104 
(*<*) 
105 
(* Exercise 1: *) 

106 
lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and> 

107 
substs ((subst f) \<circ> g) ts = substs f (substs g ts)" 

58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
48985
diff
changeset

108 
apply (induct_tac t and ts rule: subst.induct substs.induct) 
12334  109 
apply (simp_all) 
110 
done 

111 

112 
(* Exercise 2: *) 

113 

39795  114 
primrec trev :: "('v,'f) term \<Rightarrow> ('v,'f) term" 
115 
and trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list" 

116 
where 

117 
"trev (Var v) = Var v" 

118 
 "trev (App f ts) = App f (trevs ts)" 

119 
 "trevs [] = []" 

120 
 "trevs (t#ts) = (trevs ts) @ [(trev t)]" 

12334  121 

122 
lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" 

123 
apply (induct_tac xs, auto) 

124 
done 

125 

126 
lemma "trev (trev t) = (t::('v,'f)term) \<and> 

127 
trevs (trevs ts) = (ts::('v,'f)term list)" 

58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
48985
diff
changeset

128 
apply (induct_tac t and ts rule: trev.induct trevs.induct, simp_all) 
12334  129 
done 
130 
(*>*) 

9644  131 

132 
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" 

10171  133 
apply(induct_tac ts, simp_all) 
134 
done 

9644  135 

67406  136 
text\<open>\noindent 
9644  137 
What is more, we can now disable the old defining equation as a 
138 
simplification rule: 

67406  139 
\<close> 
9644  140 

9933  141 
declare subst_App [simp del] 
9644  142 

69597  143 
text\<open>\noindent The advantage is that now we have replaced \<^const>\<open>substs\<close> by \<^const>\<open>map\<close>, we can profit from the large number of 
144 
preproved lemmas about \<^const>\<open>map\<close>. Unfortunately, inductive proofs 

69505  145 
about type \<open>term\<close> are still awkward because they expect a 
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

146 
conjunction. One could derive a new induction principle as well (see 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

147 
\S\ref{sec:deriveind}), but simpler is to stop using 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

148 
\isacommand{primrec} and to define functions with \isacommand{fun} 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

149 
instead. Simple uses of \isacommand{fun} are described in 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

150 
\S\ref{sec:fun} below. Advanced applications, including functions 
69505  151 
over nested datatypes like \<open>term\<close>, are discussed in a 
58620  152 
separate tutorial~@{cite "isabellefunction"}. 
8745  153 

10971  154 
Of course, you may also combine mutual and nested recursion of datatypes. For example, 
69505  155 
constructor \<open>Sum\<close> in \S\ref{sec:datatypemutrec} could take a list of 
156 
expressions as its argument: \<open>Sum\<close>~@{typ[quotes]"'a aexp list"}. 

67406  157 
\<close> 
12334  158 
(*<*)end(*>*) 