nominal2: comparison Tutorial/Tutorial1.thy

equal deleted inserted replaced

-:da9bed7baf23
+:2abc8cb46a5c
 header {*
 Nominal Isabelle Tutorial at POPL'11
 ====================================
 \<sharp>    sharp     (freshness)
 \<bullet>    bullet    (permutation application)
 *}
 theory Tutorial1
 imports Lambda
 begin
 section {* Theories *}
 section {* Inductive Definitions: Evaluation Relation *}
 text {*
 In this section we want to define inductively the evaluation
-relation for lambda terms.
+relation and for cbv-reduction relation.
 Inductive definitions in Isabelle start with the keyword "inductive"
 and a predicate name.  One can optionally provide a type for the predicate.
 Clauses of the inductive predicate are introduced by "where" and more than
 two clauses need to be separated by "|". One can also give a name to each
 eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
 where
 e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
 | e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
+text {*
-text {*
+Values and cbv are also defined using inductive.
-Values are also defined using inductive. In our case values
-are just lambda-abstractions.
 *}
 inductive
 val :: "lam \<Rightarrow> bool"
 where
 v_Lam[intro]:   "val (Lam [x].t)"
 section {* Theorems *}
 text {*
 A central concept in Isabelle is that of theorems. Isabelle's theorem
 qed
 Two very simple example proofs are as follows.
 *}
+subsection {* EXERCISE 1 *}
 lemma eval_val:
 assumes a: "val t"
 shows "t \<Down> t"
 using a
 proof (induct)
 case (v_Lam x t)
 show "Lam [x]. t \<Down> Lam [x]. t" sorry
 qed
-lemma eavl_to_val:
+subsection {* EXERCISE 2 *}
+text {* Fill the gaps in the proof below. *}
+lemma eval_to_val:
 assumes a: "t \<Down> t'"
 shows "val t'"
 using a
 proof (induct)
 case (e_Lam x t)
 show "val (Lam [x].t)" sorry
 next
 case (e_App t1 x t t2 v v')
+-- {* all assumptions in this case *}
 have "t1 \<Down> Lam [x].t" by fact
 have ih1: "val (Lam [x]. t)" by fact
 have "t2 \<Down> v" by fact
 have ih2: "val v" by fact
 have "t [x ::= v] \<Down> v'" by fact
 have ih3: "val v'" by fact
 show "val v'" sorry
 qed
-text {*
+section {* Datatypes: Evaluation Contexts*}
-Just like gotos in the Basic programming language, labels often reduce
-the readability of proofs. Therefore one can use in Isar the notation
+text {*
-"then have" in order to feed a have-statement to the proof of
-the next have-statement. This is used in teh second case below.
-*}
-text {*
-The label ih2 cannot be got rid of in this way, because it is used
-two lines below and we cannot rearange them. We can still avoid the
-label by feeding a sequence of facts into a proof using the
-"moreover"-chaining mechanism:
-have "statement_1" \<dots>
-moreover
-have "statement_2" \<dots>
-\<dots>
-moreover
-have "statement_n" \<dots>
-ultimately have "statement" \<dots>
-In this chain, all "statement_i" can be used in the proof of the final
-"statement". With this we can simplify our proof further to:
-*}
-text {*
-While automatic proof procedures in Isabelle are not able to prove statements
-like "P = NP" assuming usual definitions for P and NP, they can automatically
-discharge the lemmas we just proved. For this we only have to set up the induction
-and auto will take care of the rest. This means we can write:
-*}
-section {* Datatypes: Evaluation Contexts *}
-text {*
 Datatypes can be defined in Isabelle as follows: we have to provide the name
-of the datatype and list its type-constructors. Each type-constructor needs
+of the datatype and a list its type-constructors. Each type-constructor needs
 to have the information about the types of its arguments, and optionally
 can also contain some information about pretty syntax. For example, we like
 to write "\<box>" for holes.
 *}
 datatype ctx =
 Hole ("\<box>")
 | CAppL "ctx" "lam"
 | CAppR "lam" "ctx"
 text {*
 Try and see what happens if you apply a Hole to a Hole?
 *}
+section {* Machines for Evaluation *}
 type_synonym ctxs = "ctx list"
 inductive
 machine :: "lam \<Rightarrow> ctxs \<Rightarrow>lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto> <_,_>" [60, 60, 60, 60] 60)
 where
-m1[intro]: "<App t1 t2,Es> \<mapsto> <t1,(CAppL \<box> t2) # Es>"
+m1: "<App t1 t2, Es> \<mapsto> <t1, (CAppL \<box> t2) # Es>"
-| m2[intro]: "val v \<Longrightarrow> <v,(CAppL \<box> t2) # Es> \<mapsto> <t2,(CAppR v \<box>) # Es>"
+| m2: "val v \<Longrightarrow> <v, (CAppL \<box> t2) # Es> \<mapsto> <t2, (CAppR v \<box>) # Es>"
-| m3[intro]: "val v \<Longrightarrow> <v,(CAppR (Lam [x].t) \<box>) # Es> \<mapsto> <t[x ::= v],Es>"
+| m3: "val v \<Longrightarrow> <v, (CAppR (Lam [x].t) \<box>) # Es> \<mapsto> <t[x ::= v], Es>"
 text {*
 Since the machine defined above only performs a single reduction,
 we need to define the transitive closure of this machine. *}
 inductive
 machines :: "lam \<Rightarrow> ctxs \<Rightarrow> lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto>* <_,_>" [60, 60, 60, 60] 60)
 where
-ms1[intro]: "<t,Es> \<mapsto>* <t,Es>"
+ms1: "<t,Es> \<mapsto>* <t,Es>"
-| ms2[intro]: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
+| ms2: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
-lemma
+declare machine.intros[intro] machines.intros[intro]
+section {* EXERCISE 3 *}
+text {*
+We need to show that the machines-relation is transitive.
+Fill in the gaps below.
+*}
+lemma ms3[intro]:
 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>"
 and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
 shows "<e1, Es1> \<mapsto>* <e3, Es3>"
 using a b
 proof(induct)
 have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
 show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
 qed
 text {*
-Just like gotos in the Basic programming language, labels can reduce
+Just like gotos in the Basic programming language, labels often reduce
 the readability of proofs. Therefore one can use in Isar the notation
 "then have" in order to feed a have-statement to the proof of
-the next have-statement. In the proof below this has been used
+the next have-statement. This is used in teh second case below.
-in order to get rid of the labels c and d1.
+*}
-*}
 lemma
 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>"
 and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
 shows "<e1, Es1> \<mapsto>* <e3, Es3>"
 using a b
 then have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
 have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
 show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto
 qed
+text {*
+The label ih2 cannot be got rid of in this way, because it is used
+two lines below and we cannot rearange them. We can still avoid the
+label by feeding a sequence of facts into a proof using the
+"moreover"-chaining mechanism:
+have "statement_1" \<dots>
+moreover
+have "statement_2" \<dots>
+\<dots>
+moreover
+have "statement_n" \<dots>
+ultimately have "statement" \<dots>
+In this chain, all "statement_i" can be used in the proof of the final
+"statement". With this we can simplify our proof further to:
+*}
 lemma
 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>"
 and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
 shows "<e1, Es1> \<mapsto>* <e3, Es3>"
 using a b
 have "<e1, Es1> \<mapsto> <e2, Es2>" by fact
 ultimately show "<e1, Es1> \<mapsto>* <e3, Es3>" by auto
 qed
-lemma ms3[intro]:
+text {*
+While automatic proof procedures in Isabelle are not able to prove statements
+like "P = NP" assuming usual definitions for P and NP, they can automatically
+discharge the lemmas we just proved. For this we only have to set up the induction
+and auto will take care of the rest. This means we can write:
+*}
+lemma
+assumes a: "val t"
+shows "t \<Down> t"
+using a by (induct) (auto)
+lemma
+assumes a: "t \<Down> t'"
+shows "val t'"
+using a by (induct) (auto)
+lemma
 assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>"
 and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
 shows "<e1, Es1> \<mapsto>* <e3, Es3>"
 using a b by (induct) (auto)
-lemma eval_to_val:  (* fixme: done above *)
-assumes a: "t \<Down> t'"
+section {* EXERCISE 4 *}
-shows "val t'"
-using a by (induct) (auto)
+text {*
+The point of the machine is that it simulates the evaluation
+relation. Therefore we like to prove the following:
+*}
 theorem
 assumes a: "t \<Down> t'"
 shows "<t, []> \<mapsto>* <t', []>"
 using a
 have ih1: "<t1, []> \<mapsto>* <Lam [x].t, []>" by fact
 have a2: "t2 \<Down> v'" by fact
 have ih2: "<t2, []> \<mapsto>* <v', []>" by fact
 have a3: "t[x::=v'] \<Down> v" by fact
 have ih3: "<t[x::=v'], []> \<mapsto>* <v, []>" by fact
 -- {* your reasoning *}
 show "<App t1 t2, []> \<mapsto>* <v, []>" sorry
 qed
+theorem
+assumes a: "t \<Down> t'"
+shows "<t, Es> \<mapsto>* <t', Es>"
+using a
+proof (induct arbitrary: Es)
+case (e_Lam x t Es)
+-- {* no assumptions *}
+show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto
+next
+case (e_App t1 x t t2 v' v Es)
+-- {* all assumptions in this case *}
+have a1: "t1 \<Down> Lam [x].t" by fact
+have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact
+have a2: "t2 \<Down> v'" by fact
+have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact
+have a3: "t[x::=v'] \<Down> v" by fact
+have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact
+-- {* your reasoning *}
+have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto
+moreover
+have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto
+moreover
+have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto
+moreover
+have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>"
+using ih2 by auto
+moreover
+have "val v'" using a2 eval_to_val by auto
+then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto
+moreover
+have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto
+ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast
+qed
 text {*
 Again the automatic tools in Isabelle can discharge automatically
 of the routine work in these proofs. We can write:
 *}
 filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100, 100] 100)
 where
 "\<box>\<lbrakk>t\<rbrakk> = t"
 | "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
 | "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
 text {*
 After this definition Isabelle will be able to simplify
 statements like:
 *}

changeset 2693	2abc8cb46a5c
parent 2692	da9bed7baf23
child 2694	3485111c7d62