equal
deleted
inserted
replaced
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 rule: aexp_bexp.induct); |
96 apply(induct_tac a and b); |
97 |
97 |
98 txt{*\noindent Unfortunately, induction needs to be told explicitly which induction rule to use (via @{text"rule:"}). |
98 txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
99 The resulting 8 goals (one for each constructor) are proved in one fell swoop: |
|
100 *} |
99 *} |
101 |
100 |
102 apply simp_all; |
101 apply simp_all; |
103 (*<*)done(*>*) |
102 (*<*)done(*>*) |
104 |
103 |
106 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$, |
107 an inductive proof expects a goal of the form |
106 an inductive proof expects a goal of the form |
108 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
107 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
109 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
108 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
110 \begin{isabelle} |
109 \begin{isabelle} |
111 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$ @{text"rule:"} $\tau@1$@{text"_"}\dots@{text"_"}$\tau@n$@{text".induct)"} |
110 \isacommand{apply}@{text"(induct_tac"} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$@{text ")"} |
112 \end{isabelle} |
111 \end{isabelle} |
113 |
112 |
114 \begin{exercise} |
113 \begin{exercise} |
115 Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that |
114 Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that |
116 replaces @{term"IF"}s with complex boolean conditions by nested |
115 replaces @{term"IF"}s with complex boolean conditions by nested |
136 "normb (And b1 b2) t e = normb b1 (normb b2 t e) e" | |
135 "normb (And b1 b2) t e = normb b1 (normb b2 t e) e" | |
137 "normb (Neg b) t e = normb b e t" |
136 "normb (Neg b) t e = normb b e t" |
138 |
137 |
139 lemma " evala (norma a) env = evala a env |
138 lemma " evala (norma a) env = evala a env |
140 \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)" |
139 \<and> (\<forall> t e. evala (normb b t e) env = evala (IF b t e) env)" |
141 apply (induct_tac a and b rule: aexp_bexp.induct) |
140 apply (induct_tac a and b) |
142 apply (simp_all) |
141 apply (simp_all) |
143 done |
142 done |
144 |
143 |
145 primrec normala :: "'a aexp \<Rightarrow> bool" and |
144 primrec normala :: "'a aexp \<Rightarrow> bool" and |
146 normalb :: "'a bexp \<Rightarrow> bool" where |
145 normalb :: "'a bexp \<Rightarrow> bool" where |
154 "normalb (And b1 b2) = False" | |
153 "normalb (And b1 b2) = False" | |
155 "normalb (Neg b) = False" |
154 "normalb (Neg b) = False" |
156 |
155 |
157 lemma "normala (norma (a::'a aexp)) \<and> |
156 lemma "normala (norma (a::'a aexp)) \<and> |
158 (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))" |
157 (\<forall> (t::'a aexp) e. (normala t \<and> normala e) \<longrightarrow> normala (normb b t e))" |
159 apply (induct_tac a and b rule: aexp_bexp.induct) |
158 apply (induct_tac a and b) |
160 apply (auto) |
159 apply (auto) |
161 done |
160 done |
162 |
161 |
163 end |
162 end |
164 (*>*) |
163 (*>*) |