Tutorial/Tutorial1.thy
changeset 3132 87eca760dcba
parent 2706 8ae1c2e6369e
child 3245 017e33849f4d
equal deleted inserted replaced
3131:3e37322465e2 3132:87eca760dcba
   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