nominal2: comparison Tutorial/Tutorial1.thy

equal deleted inserted replaced

-:d0fb94035969
+:87b735f86060
 \<sharp>       sharp     (freshness)
 \<bullet>       bullet    (permutations)
 *}
 theory Tutorial1
 imports Lambda
 begin
 section {* Theories *}
 theorem
 assumes a: "t \<Down> t'"
 shows "<t, []> \<mapsto>* <t', []>"
 using a
 proof (induct)
 case (e_Lam x t)
-(* no assumptions *)
+-- {* no assumptions *}
 show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" sorry
 next
 case (e_App t1 x t t2 v' v)
-(* all assumptions in this case *)
+-- {* all assumptions in this case *}
 have a1: "t1 \<Down> Lam [x].t" by fact
 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 details *)
+-- {* 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: *}
+of the routine work in these proofs. We can write:
+*}
 theorem eval_implies_machines_ctx:
 assumes a: "t \<Down> t'"
 shows "<t, Es> \<mapsto>* <t', Es>"
 using a
 corollary eval_implies_machines:
 assumes a: "t \<Down> t'"
 shows "<t, []> \<mapsto>* <t', []>"
 using a eval_implies_machines_ctx by simp
+section {* Types *}
 nominal_datatype ty =
 tVar "string"
 | tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100)
 text {*
 Having defined them as nominal datatypes gives us additional
 definitions and theorems that come with types (see below).
-*}
-text {*
 We next define the type of typing contexts, a predicate that
 defines valid contexts (i.e. lists that contain only unique
 variables) and the typing judgement.
 *}
 type_synonym ty_ctx = "(name \<times> ty) list"
 inductive
 valid :: "ty_ctx \<Rightarrow> bool"
 where
 v1[intro]: "valid []"
 | v2[intro]: "\<lbrakk>valid \<Gamma>; atom x \<sharp> \<Gamma>\<rbrakk>\<Longrightarrow> valid ((x, T) # \<Gamma>)"
 inductive
 typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60)
 where
 t_Var[intro]:  "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | t_App[intro]:  "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
 | t_Lam[intro]:  "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1 \<rightarrow> T2"
 text {*
-The predicate x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by Nominal Isabelle.
+The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by
-Freshness is defined for lambda-terms, products, lists etc. For example
+Nominal Isabelle. Freshness is defined for lambda-terms, products,
-we have:
+lists etc. For example we have:
 *}
 lemma
 fixes x::"name"
 shows "atom x \<sharp> Lam [x].t"
 and   "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)"
 and   "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)"
 and   "atom x \<sharp> y \<Longrightarrow> x \<noteq> y"
 by (simp_all add: lam.fresh fresh_append fresh_at_base)
-text {* We can also prove that every variable is fresh for a type *}
+text {*
+We can also prove that every variable is fresh for a type.
+*}
 lemma ty_fresh:
 fixes x::"name"
 and   T::"ty"
 shows "atom x \<sharp> T"
 by (induct T rule: ty.induct)
 (simp_all add: ty.fresh pure_fresh)
 text {*
-In order to state the weakening lemma in a convenient form, we overload
+In order to state the weakening lemma in a convenient form, we
-the subset-notation and define the abbreviation below. Abbreviations behave
+using the following abbreviation. Abbreviations behave like
-like definitions, except that they are always automatically folded and
+definitions, except that they are always automatically folded
-unfolded.
+and unfolded.
 *}
 abbreviation
 "sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60)
 where
 "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"
-text {*****************************************************************
+subsection {* EXERCISE 4 *}
-4.) Exercise
-------------
+text {*
 Fill in the details and give a proof of the weakening lemma.
 *}
 lemma
 assumes a: "\<Gamma>1 \<turnstile> t : T"
 and     b: "valid \<Gamma>2"
 have a0: "atom x \<sharp> \<Gamma>1" by fact
 have a1: "valid \<Gamma>2" by fact
 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
 show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-qed (auto)
+qed (auto) -- {* the application case *}
 text {*
 Despite the frequent claim that the weakening lemma is trivial,
 routine or obvious, the proof in the lambda-case does not go
-smoothly through. Painful variable renamings seem to be necessary.
+through smoothly. Painful variable renamings seem to be necessary.
-But the proof using renamings is horribly complicated. It is really
+But the proof using renamings is horribly complicated (see below).
-interesting whether people who claim this proof is  trivial, routine
-or obvious had this proof in mind.
-BTW: The following two commands help already with showing that validity
-and typing are invariant under variable (permutative) renamings.
 *}
 equivariance valid
 equivariance typing
-lemma not_to_be_tried_at_home_weakening:
+lemma weakening_NOT_TO_BE_TRIED_AT_HOME:
 assumes a: "\<Gamma>1 \<turnstile> t : T"
 and     b: "valid \<Gamma>2"
 and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
 shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (induct arbitrary: \<Gamma>2)
-case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
+-- {* lambda case *}
+case (t_Lam x \<Gamma>1 T1 t T2)
 have fc0: "atom x \<sharp> \<Gamma>1" by fact
 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
+-- {* we choose a fresh variable *}
 obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh)
-have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
+-- {* we alpha-rename the abstraction *}
+have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1
 by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def)
 moreover
-have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)
+-- {* we can then alpha rename the goal *}
+have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2"
 proof -
-(* we establish (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) and valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *)
+-- {* we need to establish
-have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)"
+*   (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) and
+**  valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}
+have *: "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)"
 proof -
 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
 then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1
-	by (perm_simp) (simp add: flip_fresh_fresh)
+by (perm_simp) (simp add: flip_fresh_fresh)
 then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE)
 qed
 moreover
-have "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))"
+have **: "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))"
 proof -
 have "valid \<Gamma>2" by fact
 then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1
-	by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)
+by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)
 qed
-(* these two facts give us by induction hypothesis the following *)
+-- {* these two facts give us by induction hypothesis the following *}
 ultimately have "(x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2" using ih by simp
-(* we now apply renamings to get to our goal *)
+-- {* we now apply renamings to get to our goal *}
 then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)
 then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1
 by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)
 then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto
 qed
 ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
-qed (auto) (* var and app cases *)
+qed (auto) -- {* var and app cases, luckily, are automatic *}
 text {*
-The remedy to the complicated proof of the weakening proof
+The remedy is to use a stronger induction principle that
-shown above is to use a stronger induction principle that
+has the usual "variable convention" already build in. The
-has the usual variable convention already build in. The
 following command derives this induction principle for us.
 (We shall explain what happens here later.)
 *}
 nominal_inductive typing
 avoids t_Lam: "x"
 unfolding fresh_star_def
 by (simp_all add: fresh_Pair lam.fresh ty_fresh)
 text {* Compare the two induction principles *}
 thm typing.induct
-thm typing.strong_induct
+thm typing.strong_induct -- {* has the additional assumption {atom x} \<sharp> c *}
 text {*
 We can use the stronger induction principle by replacing
 the line
 proof (induct arbitrary: \<Gamma>2)
 with
 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
 Try now the proof.
 *}
 lemma weakening:
 assumes a: "\<Gamma>1 \<turnstile> t : T"
 and     b: "valid \<Gamma>2"
 and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
 shows "\<Gamma>2 \<turnstile> t : T"
 using a b c
 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
-case (t_Var \<Gamma>1 x T)  (* variable case *)
+case (t_Var \<Gamma>1 x T)  -- {* variable case is as before *}
 have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
 moreover
 have "valid \<Gamma>2" by fact
 moreover
 have "(x, T)\<in> set \<Gamma>1" by fact
 ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto
 next
 case (t_Lam x \<Gamma>1 T1 t T2)
-have vc: "atom x \<sharp> \<Gamma>2" by fact   (* additional fact *)
+have vc: "atom x \<sharp> \<Gamma>2" by fact  -- {* additional fact afforded by the stron induction *}
 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
 have a0: "atom x \<sharp> \<Gamma>1" by fact
 have a1: "valid \<Gamma>2" by fact
 have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
+have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto
-show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
+moreover
-qed (auto) (* app case *)
+have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto
+ultimately
+have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp
-text {*****************************************************************
+then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto
+qed (auto) -- {* app case *}
-Function Definitions: Filling a Lambda-Term into a Context
-----------------------------------------------------------
+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
 to give a name for the function, its type, optionally some pretty-syntax
 and then some equations defining the function. Like in "inductive",
 "fun" expects that more than one such equation is separated by "|".
 *}
 fun
 filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100, 100] 100)
 where
 | "(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: *}
+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" ("_ \<cdot> _" [101,100] 100)
+ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<odot> _" [99,98] 99)
 where
-"\<box> \<cdot> E' = E'"
+"\<box> \<odot> E' = E'"
-| "(CAppL E t') \<cdot> E' = CAppL (E \<cdot> E') t'"
+| "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
-| "(CAppR t' E) \<cdot> E' = CAppR t' (E \<cdot> E')"
+| "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')"
 fun
 ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)
 where
 "[]\<down> = \<box>"
-| "(E # Es)\<down> = (Es\<down>) \<cdot> E"
+| "(E # Es)\<down> = (Es\<down>) \<odot> E"
 text {*
 Notice that we not just have given a pretty syntax for the functions, but
-also some precedences..The numbers inside the [\<dots>] stand for the precedences
+also some precedences. The numbers inside the [\<dots>] stand for the precedences
 of the arguments; the one next to it the precedence of the whole term.
-This means we have to write (Es1 \<cdot> Es2) \<cdot> Es3 otherwise Es1 \<cdot> Es2 \<cdot> Es3 is
+This means we have to write (Es1 \<odot> Es2) \<odot> Es3 otherwise Es1 \<odot> Es2 \<odot> Es3 is
-interpreted as Es1 \<cdot> (Es2 \<cdot> Es3).
+interpreted as Es1 \<odot> (Es2 \<odot> Es3).
 *}
-text {******************************************************************
+section {* Structural Inductions over Contexts *}
-Structural Inductions over Contexts
+text {*
-------------------------------------
 So far we have had a look at an induction over an inductive predicate.
 Another important induction principle is structural inductions for
 datatypes. To illustrate structural inductions we prove some facts
 about context composition, some of which we will need later on.
+*}
-*}
+subsection {* EXERCISE 5 *}
-text {******************************************************************
+text {* Complete the proof and remove the sorries. *}
-5.) EXERCISE
-------------
-Complete the proof and remove the sorries.
-*}
 lemma ctx_compose:
-shows "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
+shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 proof (induct E1)
 case Hole
-show "\<box> \<cdot> E2\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 next
 case (CAppL E1 t')
-have ih: "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
+have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
-show "((CAppL E1 t') \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+show "((CAppL E1 t') \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 next
 case (CAppR t' E1)
-have ih: "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
+have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
-show "((CAppR t' E1) \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
 qed
 lemma neut_hole:
-shows "E \<cdot> \<box> = E"
+shows "E \<odot> \<box> = E"
 by (induct E) (simp_all)
-lemma circ_assoc:
+lemma odot_assoc:
 fixes E1 E2 E3::"ctx"
-shows "(E1 \<cdot> E2) \<cdot> E3 = E1 \<cdot> (E2 \<cdot> E3)"
+shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
 by (induct E1) (simp_all)
 lemma
-shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"
+shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
 case Nil
-show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" sorry
+show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" sorry
 next
 case (Cons E Es1)
-have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<cdot> Es1\<down>" by fact
+have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" sorry
+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. *}
+construction.
+*}
 lemma
-shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"
+shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
 proof (induct Es1)
 case Nil
-show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" using neut_hole by simp
+show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
 next
 case (Cons E Es1)
-have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<cdot> Es1\<down>" by fact
+have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
-have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<cdot> E" by simp
+have "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
-also have "\<dots> = (Es2\<down> \<cdot> Es1\<down>) \<cdot> E" using ih by simp
+also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
-also have "\<dots> = Es2\<down> \<cdot> (Es1\<down> \<cdot> E)" using circ_assoc by simp
+also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using odot_assoc by simp
-also have "\<dots> = Es2\<down> \<cdot> (E # Es1)\<down>" by simp
+also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
-finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" by simp
+finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
 qed
 text {******************************************************************
 Formalising Barendregt's Proof of the Substitution Lemma
 of such a block to the 'outside' is the implication
 \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C"
 Now if we want to prove a property "smth" using the case-distinctions
-P\<^isub>1, P\<^isub>2 and P\<^isub>3 then we can use the following reasoning:
+P1, P2 and P3 then we can use the following reasoning:
-{ assume "P\<^isub>1"
+{ assume "P1"
 \<dots>
 have "smth"
 }
 moreover
-{ assume "P\<^isub>2"
+{ assume "P2"
 \<dots>
 have "smth"
 }
 moreover
-{ assume "P\<^isub>3"
+{ assume "P3"
 \<dots>
 have "smth"
 }
 ultimately have "smth" by blast
 The blocks establish the implications
-P\<^isub>1 \<Longrightarrow> smth
+P1 \<Longrightarrow> smth
-P\<^isub>2 \<Longrightarrow> smth
+P2 \<Longrightarrow> smth
-P\<^isub>3 \<Longrightarrow> smth
+P3 \<Longrightarrow> smth
-If we know that P\<^isub>1, P\<^isub>2 and P\<^isub>3 cover all the cases, that is P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3 is
+If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 is
 true, then we have 'ultimately' established the property "smth"
 *}
-text {******************************************************************
+section {* EXERCISE 7 *}
-7.) Exercise
+text {*
-------------
 Fill in the cases 1.2 and 1.3 and the equational reasoning
 in the lambda-case.
 *}
 lemma forget:
 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-apply(nominal_induct t avoiding: x s rule: lam.strong_induct)
+by (nominal_induct t avoiding: x s rule: lam.strong_induct)
-apply(auto simp add: lam.fresh fresh_at_base)
+(auto simp add: lam.fresh fresh_at_base)
-done
 lemma fresh_fact:
 fixes z::"name"
 assumes a: "atom z \<sharp> s"
 and b: "z = y \<or> atom z \<sharp> t"
 shows "atom z \<sharp> t[y ::= s]"
 using a b
-apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
-apply (auto simp add: lam.fresh fresh_at_base)
+(auto simp add: lam.fresh fresh_at_base)
-done
-thm forget
-thm fresh_fact
 lemma
 assumes a: "x \<noteq> y"
 and     b: "atom x \<sharp> L"
 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 case (Var z)
 have a1: "x \<noteq> y" by fact
 have a2: "atom x \<sharp> L" by fact
 show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")
 proof -
-{ (*Case 1.1*)
+{ -- {* Case 1.1 *}
-assume c1: "z=x"
+assume c1: "z = x"
 have "(1)": "?LHS = N[y::=L]" using c1 by simp
 have "(2)": "?RHS = N[y::=L]" using c1 a1 by simp
 have "?LHS = ?RHS" using "(1)" "(2)" by simp
 }
 moreover
-{ (*Case 1.2*)
+{ -- {* Case 1.2 *}
 assume c2: "z = y" "z \<noteq> x"
 have "?LHS = ?RHS" sorry
 }
 moreover
-{ (*Case 1.3*)
+{ -- {* Case 1.3 *}
 assume c3: "z \<noteq> x" "z \<noteq> y"
 have "?LHS = ?RHS" sorry
 }
 ultimately show "?LHS = ?RHS" by blast
 qed
 next
-case (Lam z M1) (* case 2: lambdas *)
+case (Lam z M1) -- {* case 2: lambdas *}
 have ih: "\<lbrakk>x \<noteq> y; atom x \<sharp> L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact
 have a1: "x \<noteq> y" by fact
 have a2: "atom x \<sharp> L" by fact
 have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+
 then have b: "atom z \<sharp> N[y::=L]" by (simp add: fresh_fact)
 also have "\<dots> = ?RHS" sorry
 finally show "?LHS = ?RHS" by simp
 qed
 next
-case (App M1 M2) (* case 3: applications *)
+case (App M1 M2) -- {* case 3: applications *}
 then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp
 qed
 text {*
 Again the strong induction principle enables Isabelle to find

changeset 2688	87b735f86060
parent 2687	d0fb94035969
child 2689	ddc05a611005