equal
deleted
inserted
replaced
59 |
59 |
60 text{* |
60 text{* |
61 \subsubsection{Transformation into and of If-expressions} |
61 \subsubsection{Transformation into and of If-expressions} |
62 |
62 |
63 The type \isa{boolex} is close to the customary representation of logical |
63 The type \isa{boolex} is close to the customary representation of logical |
64 formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to |
64 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
65 translate from \isa{boolex} into \isa{ifex}: |
65 translate from \isa{boolex} into \isa{ifex}: |
66 *} |
66 *} |
67 |
67 |
68 consts bool2if :: "boolex \\<Rightarrow> ifex"; |
68 consts bool2if :: "boolex \\<Rightarrow> ifex"; |
69 primrec |
69 primrec |
151 text{*\noindent |
151 text{*\noindent |
152 and prove \isa{normal(norm b)}. Of course, this requires a lemma about |
152 and prove \isa{normal(norm b)}. Of course, this requires a lemma about |
153 normality of \isa{normif}: |
153 normality of \isa{normif}: |
154 *} |
154 *} |
155 |
155 |
156 lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*) |
156 lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)"; |
|
157 (*<*) |
157 apply(induct_tac b); |
158 apply(induct_tac b); |
158 apply(auto).; |
159 apply(auto).; |
159 |
160 |
160 theorem "normal(norm b)"; |
161 theorem "normal(norm b)"; |
161 apply(induct_tac b); |
162 apply(induct_tac b); |
162 apply(auto).; |
163 apply(auto).; |
163 |
164 |
164 end(*>*) |
165 end |
|
166 (*>*) |