nominal2: comparison Tutorial/Tutorial1.thy

equal deleted inserted replaced

-:abb6c3ac2df2
+:da9bed7baf23
 \<sharp>    sharp     (freshness)
 \<bullet>    bullet    (permutation application)
 *}
 theory Tutorial1
 imports Lambda
 begin
 section {* Theories *}
 term "\<forall>x. P x"  -- {* versus *}
 term "\<And>x. P x"
+section {* Inductive Definitions: Evaluation Relation *}
-section {* Inductive Definitions: Transitive Closures of Beta-Reduction *}
+text {*
-text {*
+In this section we want to define inductively the evaluation
-The theory Lmabda already contains a definition for beta-reduction, written
+relation for lambda terms.
-*}
+Inductive definitions in Isabelle start with the keyword "inductive"
-term "t \<longrightarrow>b t'"
+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
-text {*
+two clauses need to be separated by "|". One can also give a name to each
-In this section we want to define inductively the transitive closure of
+clause and indicate that it should be added to the hints database ("[intro]").
-beta-reduction.
+A typical clause has some premises and a conclusion. This is written in
+Isabelle as:
-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 clause and indicate that it
-should be added to the hints database ("[intro]"). A typical clause has some
-premises and a conclusion. This is written in Isabelle as:
 "premise \<Longrightarrow> conclusion"
 "premise1 \<Longrightarrow> premise2 \<Longrightarrow> \<dots> premisen \<Longrightarrow> conclusion"
 There is an alternative way of writing the latter clause as
 Below we give two definitions for the transitive closure
 *}
 inductive
-beta_star1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b* _" [60, 60] 60)
+eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
 where
-bs1_refl: "t \<longrightarrow>b* t"
+e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
-| bs1_trans: "\<lbrakk>t1 \<longrightarrow>b t2; t2 \<longrightarrow>b* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b* t3"
+| 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 {*
+Values are also defined using inductive. In our case values
+are just lambda-abstractions.
+*}
 inductive
-beta_star2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b** _" [60, 60] 60)
+val :: "lam \<Rightarrow> bool"
 where
-bs2_refl: "t \<longrightarrow>b** t"
+v_Lam[intro]:   "val (Lam [x].t)"
-| bs2_step: "t1 \<longrightarrow>b t2 \<Longrightarrow> t1 \<longrightarrow>b** t2"
-| bs2_trans: "\<lbrakk>t1 \<longrightarrow>b** t2; t2 \<longrightarrow>b** t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b** t3"
 section {* Theorems *}
 text {*
 A central concept in Isabelle is that of theorems. Isabelle's theorem
 database can be queried using
 *}
-thm bs1_refl
+thm e_App
-thm bs2_trans
+thm e_Lam
 thm conjI
 thm conjunct1
 text {*
 Notice that theorems usually contain schematic variables (e.g. ?P, ?Q, \<dots>).
 When defining the predicates beta_star, Isabelle provides us automatically
 with the following theorems that state how they can be introduced and what
 constitutes an induction over them.
 *}
-thm beta_star1.intros
+thm eval.intros
-thm beta_star2.induct
+thm eval.induct
 section {* Lemmas / Theorems / Corollaries *}
 text {*
 Lemmas also need to have a proof, but ignore this 'detail' for the moment.
 Examples are
 *}
 lemma alpha_equ:
 shows "Lam [x].Var x = Lam [y].Var y"
 by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)
 case \<dots>
 \<dots>
 show \<dots>
 \<dots>
 qed
-*}
+Two very simple example proofs are as follows.
+*}
-subsection {* Exercise I *}
-text {*
+lemma eval_val:
-Remove the sorries in the proof below and fill in the proper
+assumes a: "val t"
-justifications.
+shows "t \<Down> t"
-*}
-lemma
-assumes a: "t1 \<longrightarrow>b* t2"
-shows "t1 \<longrightarrow>b** t2"
-using a
-proof (induct)
-case (bs1_refl t)
-show "t \<longrightarrow>b** t" using bs2_refl by blast
-next
-case (bs1_trans t1 t2 t3)
-have beta: "t1 \<longrightarrow>b t2" by fact
-have ih: "t2 \<longrightarrow>b** t3" by fact
-have a: "t1 \<longrightarrow>b** t2" using beta bs2_step by blast
-show "t1 \<longrightarrow>b** t3" using a ih bs2_trans by blast
-qed
-subsection {* Exercise II *}
-text {*
-Again remove the sorries in the proof below and fill in the proper
-justifications.
-*}
-lemma bs1_trans2:
-assumes a: "t1 \<longrightarrow>b* t2"
-and     b: "t2 \<longrightarrow>b* t3"
-shows "t1 \<longrightarrow>b* t3"
-using a b
-proof (induct)
-case (bs1_refl t1)
-have a: "t1 \<longrightarrow>b* t3" by fact
-show "t1 \<longrightarrow>b* t3" using a by blast
-next
-case (bs1_trans t1 t2 t3')
-have ih1: "t1 \<longrightarrow>b t2" by fact
-have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-have asm: "t3' \<longrightarrow>b* t3" by fact
-have a: "t2 \<longrightarrow>b* t3" using ih2 asm by blast
-show "t1 \<longrightarrow>b* t3" using ih1 a beta_star1.bs1_trans by blast
-qed
-lemma
-assumes a: "t1 \<longrightarrow>b** t2"
-shows "t1 \<longrightarrow>b* t2"
 using a
 proof (induct)
-case (bs2_refl t)
+case (v_Lam x t)
-show "t \<longrightarrow>b* t" using bs1_refl by blast
+show "Lam [x]. t \<Down> Lam [x]. t" sorry
-next
+qed
-case (bs2_step t1 t2)
-have ih: "t1 \<longrightarrow>b t2" by fact
+lemma eavl_to_val:
-have a: "t2 \<longrightarrow>b* t2" using bs1_refl by blast
+assumes a: "t \<Down> t'"
-show "t1 \<longrightarrow>b* t2" using ih a bs1_trans by blast
+shows "val t'"
-next
+using a
-case (bs2_trans t1 t2 t3)
+proof (induct)
-have ih1: "t1 \<longrightarrow>b* t2" by fact
+case (e_Lam x t)
-have ih2: "t2 \<longrightarrow>b* t3" by fact
+show "val (Lam [x].t)" sorry
-show "t1 \<longrightarrow>b* t3" using ih1 ih2 bs1_trans2 by blast
+next
+case (e_App t1 x t t2 v v')
+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 {*
 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. This is used in teh second case below.
 *}
-lemma
-assumes a: "t1 \<longrightarrow>b* t2"
-and     b: "t2 \<longrightarrow>b* t3"
-shows "t1 \<longrightarrow>b* t3"
-using a b
-proof (induct)
-case (bs1_refl t1)
-show "t1 \<longrightarrow>b* t3" by fact
-next
-case (bs1_trans t1 t2 t3')
-have ih1: "t1 \<longrightarrow>b t2" by fact
-have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-have "t3' \<longrightarrow>b* t3" by fact
-then have "t2 \<longrightarrow>b* t3" using ih2 by blast
-then show "t1 \<longrightarrow>b* t3" using ih1 beta_star1.bs1_trans by blast
-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
 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: "t1 \<longrightarrow>b* t2"
-and     b: "t2 \<longrightarrow>b* t3"
-shows "t1 \<longrightarrow>b* t3"
-using a b
-proof (induct)
-case (bs1_refl t1)
-show "t1 \<longrightarrow>b* t3" by fact
-next
-case (bs1_trans t1 t2 t3')
-have "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact
-moreover
-have "t3' \<longrightarrow>b* t3" by fact
-ultimately
-have "t2 \<longrightarrow>b* t3" by blast
-moreover
-have "t1 \<longrightarrow>b t2" by fact
-ultimately show "t1 \<longrightarrow>b* t3" using beta_star1.bs1_trans by blast
-qed
 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: "t1 \<longrightarrow>b* t2"
-shows "t1 \<longrightarrow>b** t2"
-using a
-by (induct) (auto intro: beta_star2.intros)
-lemma
-assumes a: "t1 \<longrightarrow>b* t2"
-and     b: "t2 \<longrightarrow>b* t3"
-shows "t1 \<longrightarrow>b* t3"
-using a b
-by (induct) (auto intro: beta_star1.intros)
-lemma
-assumes a: "t1 \<longrightarrow>b** t2"
-shows "t1 \<longrightarrow>b* t2"
-using a
-by (induct) (auto intro: bs1_trans2 beta_star1.intros)
-inductive
-eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
-where
-e_Lam:  "Lam [x].t \<Down> Lam [x].t"
-| e_App:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
-declare eval.intros[intro]
-text {*
-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 {* Datatypes: Evaluation Contexts *}
 text {*
 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:
+lemma eval_to_val:  (* fixme: done above *)
 assumes a: "t \<Down> t'"
 shows "val t'"
 using a by (induct) (auto)
 theorem

changeset 2692	da9bed7baf23
parent 2690	f325eefe803e
child 2693	2abc8cb46a5c
child 2705	67451725fb41