equal
deleted
inserted
replaced
129 term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *} |
129 term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *} |
130 term "Suc 0" -- {* successor of 0, in other words 1::nat *} |
130 term "Suc 0" -- {* successor of 0, in other words 1::nat *} |
131 term "Lam [x].Var x" -- {* a lambda-term *} |
131 term "Lam [x].Var x" -- {* a lambda-term *} |
132 term "App t1 t2" -- {* another lambda-term *} |
132 term "App t1 t2" -- {* another lambda-term *} |
133 term "x::name" -- {* an (object) variable of type name *} |
133 term "x::name" -- {* an (object) variable of type name *} |
134 term "atom (x::name)" -- {* atom is an overloaded function *} |
134 term "atom (x::name)" -- {* atom is an overloded function *} |
135 |
135 |
136 text {* |
136 text {* |
137 Lam [x].Var is the syntax we made up for lambda abstractions. If you |
137 Lam [x].Var is the syntax we made up for lambda abstractions. If you |
138 prefer, you can have your own syntax (but \<lambda> is already taken up for |
138 prefer, you can have your own syntax (but \<lambda> is already taken up for |
139 Isabelle's functions). We also came up with the type "name" for variables. |
139 Isabelle's functions). We also came up with the type "name" for variables. |
205 |
205 |
206 Below we give two definitions for the transitive closure |
206 Below we give two definitions for the transitive closure |
207 *} |
207 *} |
208 |
208 |
209 inductive |
209 inductive |
210 eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60) |
210 eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) |
211 where |
211 where |
212 e_Lam[intro]: "Lam [x].t \<Down> Lam [x].t" |
212 e_Lam[intro]: "Lam [x].t \<Down> Lam [x].t" |
213 | e_App[intro]: "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v" |
213 | e_App[intro]: "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v" |
214 |
214 |
215 text {* |
215 text {* |
474 |
474 |
475 text {* |
475 text {* |
476 Just like gotos in the Basic programming language, labels often reduce |
476 Just like gotos in the Basic programming language, labels often reduce |
477 the readability of proofs. Therefore one can use in Isar the notation |
477 the readability of proofs. Therefore one can use in Isar the notation |
478 "then have" in order to feed a have-statement to the proof of |
478 "then have" in order to feed a have-statement to the proof of |
479 the next have-statement. This is used in the second case below. |
479 the next have-statement. This is used in teh second case below. |
480 *} |
480 *} |
481 |
481 |
482 lemma |
482 lemma |
483 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" |
483 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" |
484 and b: "<e2, Es2> \<mapsto>* <e3, Es3>" |
484 and b: "<e2, Es2> \<mapsto>* <e3, Es3>" |
496 show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto |
496 show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto |
497 qed |
497 qed |
498 |
498 |
499 text {* |
499 text {* |
500 The label ih2 cannot be got rid of in this way, because it is used |
500 The label ih2 cannot be got rid of in this way, because it is used |
501 two lines below and we cannot rearrange them. We can still avoid the |
501 two lines below and we cannot rearange them. We can still avoid the |
502 label by feeding a sequence of facts into a proof using the |
502 label by feeding a sequence of facts into a proof using the |
503 "moreover"-chaining mechanism: |
503 "moreover"-chaining mechanism: |
504 |
504 |
505 have "statement_1" \<dots> |
505 have "statement_1" \<dots> |
506 moreover |
506 moreover |