author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
child 58305  57752a91eec4 
permissions  rwrr 
8745  1 
(*<*) 
16417  2 
theory Nested imports ABexpr begin 
8745  3 
(*>*) 
4 

5 
text{* 

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: 
13 
*} 

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(*>*) 
10971  15 
datatype ('v,'f)"term" = Var 'v  App 'f "('v,'f)term list"; 
8745  16 

17 
text{*\noindent 

10171  18 
Note that we need to quote @{text term} on the left to avoid confusion with 
19 
the Isabelle command \isacommand{term}. 

10971  20 
Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of 
8745  21 
function symbols. 
9541  22 
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g 
10171  23 
[Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are 
8745  24 
suitable values, e.g.\ numbers or strings. 
25 

10171  26 
What complicates the definition of @{text term} is the nested occurrence of 
27 
@{text term} inside @{text list} on the righthand side. In principle, 

8745  28 
nested recursion can be eliminated in favour of mutual recursion by unfolding 
10171  29 
the offending datatypes, here @{text list}. The result for @{text term} 
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. 

10171  39 
Now we return to the initial definition of @{text term} 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: 

44 
*} 

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 

57 
text{*\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: 

66 
*} 

67 

12334  68 
lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and> 
69 
substs Var ts = (ts::('v,'f)term list)"; 

27318  70 
apply(induct_tac t and ts, simp_all); 
10171  71 
done 
8745  72 

73 
text{*\noindent 

10171  74 
Note that @{term Var} is the identity substitution because by definition it 
9792  75 
leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. 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 

10971  78 
parameters @{text"('v,'f)"}. 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), 
10178  86 
strengthen it, and prove it. (Note: @{text"\<circ>"} 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} 
10971  90 
Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"} 
9792  91 
that recursively reverses the order of arguments of all function symbols in a 
92 
term. Prove that @{prop"trev(trev t) = t"}. 

9644  93 
\end{exercise} 
94 

10795  95 
The experienced functional programmer may feel that our definition of 
15904  96 
@{term subst} is too complicated in that @{const substs} is 
10795  97 
unnecessary. The @{term App}case can be defined directly as 
9644  98 
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} 
99 
where @{term"map"} is the standard list function such that 

9792  100 
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. 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: 
9644  103 
*} 
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)" 

27318  108 
apply (induct_tac t and ts) 
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)" 

27318  128 
apply (induct_tac t and ts, 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 

9689  136 
text{*\noindent 
9644  137 
What is more, we can now disable the old defining equation as a 
138 
simplification rule: 

139 
*} 

140 

9933  141 
declare subst_App [simp del] 
9644  142 

25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

143 
text{*\noindent The advantage is that now we have replaced @{const 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

144 
substs} by @{const map}, we can profit from the large number of 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

145 
preproved lemmas about @{const map}. Unfortunately, inductive proofs 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

146 
about type @{text term} are still awkward because they expect a 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

147 
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

148 
\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

149 
\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

150 
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

151 
\S\ref{sec:fun} below. Advanced applications, including functions 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

152 
over nested datatypes like @{text term}, are discussed in a 
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset

153 
separate tutorial~\cite{isabellefunction}. 
8745  154 

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

8745  158 
*} 
12334  159 
(*<*)end(*>*) 