equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory ABexpr imports Main begin; |
2 theory ABexpr imports Main begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{* |
5 text{* |
6 \index{datatypes!mutually recursive}% |
6 \index{datatypes!mutually recursive}% |
7 Sometimes it is necessary to define two datatypes that depend on each |
7 Sometimes it is necessary to define two datatypes that depend on each |
22 | Diff "'a aexp" "'a aexp" |
22 | Diff "'a aexp" "'a aexp" |
23 | Var 'a |
23 | Var 'a |
24 | Num nat |
24 | Num nat |
25 and 'a bexp = Less "'a aexp" "'a aexp" |
25 and 'a bexp = Less "'a aexp" "'a aexp" |
26 | And "'a bexp" "'a bexp" |
26 | And "'a bexp" "'a bexp" |
27 | Neg "'a bexp"; |
27 | Neg "'a bexp" |
28 |
28 |
29 text{*\noindent |
29 text{*\noindent |
30 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, |
30 Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler}, |
31 except that we have added an @{text IF} constructor, |
31 except that we have added an @{text IF} constructor, |
32 fixed the values to be of type @{typ"nat"} and declared the two binary |
32 fixed the values to be of type @{typ"nat"} and declared the two binary |
90 theorem in the induction step. Therefore you need to state and prove both |
90 theorem in the induction step. Therefore you need to state and prove both |
91 theorems simultaneously: |
91 theorems simultaneously: |
92 *} |
92 *} |
93 |
93 |
94 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and> |
94 lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and> |
95 evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"; |
95 evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)" |
96 apply(induct_tac a and b); |
96 apply(induct_tac a and b) |
97 |
97 |
98 txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
98 txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
99 *} |
99 *} |
100 |
100 |
101 apply simp_all; |
101 apply simp_all |
102 (*<*)done(*>*) |
102 (*<*)done(*>*) |
103 |
103 |
104 text{* |
104 text{* |
105 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
105 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
106 an inductive proof expects a goal of the form |
106 an inductive proof expects a goal of the form |