nominal2: comparison Tutorial/Tutorial1.thy

equal deleted inserted replaced

-:67451725fb41
+:8ae1c2e6369e
 header {*
 Nominal Isabelle Tutorial at POPL'11
 ====================================
 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
 Below we give two definitions for the transitive closure
 *}
 inductive
-eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
+eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 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 the 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 rearrange 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)
 case (ms1 e1 Es1)
 have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
-then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp
+show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
 next
 case (ms2 e1 Es1 e2 Es2 e2' Es2')
 have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
 have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
 have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
-show "<e1, Es1> \<mapsto>* <e3, Es3>" using d1 d2 ih by blast
-qed
+show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
+qed
-text {*
-Just like gotos in the Basic programming language, labels can reduce
+text {*
+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 the 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 rearrange 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
 text {*
 Again the automatic tools in Isabelle can discharge automatically
 of the routine work in these proofs. We can write:
 *}
 assumes a: "t \<Down> t'"
 shows "<t, []> \<mapsto>* <t', []>"
 using a eval_implies_machines_ctx by simp
 section {* Function Definitions: Filling a Lambda-Term into a Context *}
 text {*
 Many functions over datatypes can be defined by recursion on the
 structure. For this purpose, Isabelle provides "fun". To use it one needs
 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:
 *}
 lemma
 shows "(CAppL \<box> (Var x))\<lbrakk>Var y\<rbrakk> = App (Var y) (Var x)"
 by simp
 fun
-ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99)
+ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99)
 where
 "\<box> \<odot> E' = E'"
 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
 | "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')"
 case (CAppR t' E1)
 have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
 show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 qed
+subsection {* EXERCISE 6 *}
+text {*
+Remove the sorries in the ctx_append proof below. You can make
+use of the following two properties.
+*}
 lemma neut_hole:
 shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
-lemma odot_assoc: (* fixme call compose *)
+lemma compose_assoc:
 shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 lemma
 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
 show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry
 qed
 text {*
 The last proof involves several steps of equational reasoning.
 Isar provides some convenient means to express such equational
 reasoning in a much cleaner fashion using the "also have"
 construction.
 *}
 lemma
 shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
 case Nil
 show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
 next
 case (Cons E Es1)
 have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
+have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
+also have "\<dots> = (Es1 @ Es2)\<down> \<odot> E" by simp
 also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
-also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using odot_assoc by simp
+also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp
 also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
 finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
 qed
 end

changeset 2706	8ae1c2e6369e
parent 2705	67451725fb41
parent 2704	b4bad45dbc0f
child 3132	87eca760dcba