--- a/Tutorial/Tutorial1.thy Thu Jan 20 23:19:30 2011 +0100
+++ b/Tutorial/Tutorial1.thy Fri Jan 21 00:55:28 2011 +0100
@@ -61,7 +61,6 @@
\<bullet> bullet (permutations)
*}
-
theory Tutorial1
imports Lambda
begin
@@ -665,25 +664,26 @@
shows "<t, []> \<mapsto>* <t', []>"
using a
proof (induct)
- case (e_Lam x t)
- (* no assumptions *)
+ case (e_Lam x t)
+ -- {* 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 *)
+ case (e_App t1 x t t2 v' v)
+ -- {* 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'"
@@ -697,6 +697,7 @@
shows "<t, []> \<mapsto>* <t', []>"
using a eval_implies_machines_ctx by simp
+section {* Types *}
nominal_datatype ty =
tVar "string"
@@ -706,9 +707,7 @@
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.
@@ -717,12 +716,14 @@
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
@@ -732,9 +733,9 @@
text {*
- The predicate x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by Nominal Isabelle.
- Freshness is defined for lambda-terms, products, lists etc. For example
- we have:
+ The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by
+ Nominal Isabelle. Freshness is defined for lambda-terms, products,
+ lists etc. For example we have:
*}
lemma
@@ -747,7 +748,9 @@
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"
@@ -757,10 +760,10 @@
(simp_all add: ty.fresh pure_fresh)
text {*
- In order to state the weakening lemma in a convenient form, we overload
- the subset-notation and define the abbreviation below. Abbreviations behave
- like definitions, except that they are always automatically folded and
- unfolded.
+ In order to state the weakening lemma in a convenient form, we
+ using the following abbreviation. Abbreviations behave like
+ definitions, except that they are always automatically folded
+ and unfolded.
*}
abbreviation
@@ -768,13 +771,11 @@
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
@@ -799,74 +800,73 @@
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.
- But the proof using renamings is horribly complicated. It is really
- 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.
+ through smoothly. Painful variable renamings seem to be necessary.
+ But the proof using renamings is horribly complicated (see below).
*}
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)) *)
- have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)"
+ -- {* we need to establish
+ * (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
- shown above is to use a stronger induction principle that
- has the usual variable convention already build in. The
+ The remedy is to use a stronger induction principle that
+ 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
@@ -875,21 +875,21 @@
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)
+ proof (induct arbitrary: \<Gamma>2)
with
- proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
+ proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)
Try now the proof.
-
*}
@@ -900,7 +900,7 @@
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
@@ -909,27 +909,28 @@
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
-
- show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry
-qed (auto) (* app case *)
+ have "valid ((x, T1) # \<Gamma>2)" using a1 vc by auto
+ moreover
+ 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
+ then show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" using vc by auto
+qed (auto) -- {* app case *}
-text {*****************************************************************
-
- 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
@@ -941,90 +942,82 @@
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'"
-| "(CAppL E t') \<cdot> E' = CAppL (E \<cdot> E') t'"
-| "(CAppR t' E) \<cdot> E' = CAppR t' (E \<cdot> E')"
+ "\<box> \<odot> E' = E'"
+| "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
+| "(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
- interpreted as Es1 \<cdot> (Es2 \<cdot> Es3).
+ This means we have to write (Es1 \<odot> Es2) \<odot> Es3 otherwise Es1 \<odot> Es2 \<odot> Es3 is
+ interpreted as Es1 \<odot> (Es2 \<odot> Es3).
*}
-text {******************************************************************
-
- Structural Inductions over Contexts
- ------------------------------------
-
+section {* 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.
-
*}
-text {******************************************************************
+subsection {* EXERCISE 5 *}
- 5.) EXERCISE
- ------------
-
- Complete the proof and remove the sorries.
-
-*}
+text {* 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
- show "((CAppL E1 t') \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+ have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
+ 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
- show "((CAppR t' E1) \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
+ 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
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
@@ -1032,21 +1025,23 @@
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 "((E # Es1) @ Es2)\<down> = (Es1 @ Es2)\<down> \<cdot> E" by simp
- also have "\<dots> = (Es2\<down> \<cdot> Es1\<down>) \<cdot> 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> \<cdot> (E # Es1)\<down>" by simp
- finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" by simp
+ have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
+ have "((E # Es1) @ Es2)\<down> = (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> (E # Es1)\<down>" by simp
+ finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
qed
text {******************************************************************
@@ -1077,19 +1072,19 @@
\<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"
}
@@ -1097,29 +1092,26 @@
The blocks establish the implications
- P\<^isub>1 \<Longrightarrow> smth
- P\<^isub>2 \<Longrightarrow> smth
- P\<^isub>3 \<Longrightarrow> smth
+ P1 \<Longrightarrow> smth
+ P2 \<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 {******************************************************************
-
- 7.) Exercise
- ------------
+section {* EXERCISE 7 *}
+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)
-apply(auto simp add: lam.fresh fresh_at_base)
-done
+by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
lemma fresh_fact:
fixes z::"name"
@@ -1127,12 +1119,9 @@
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)
-apply (auto simp add: lam.fresh fresh_at_base)
-done
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
+ (auto simp add: lam.fresh fresh_at_base)
-thm forget
-thm fresh_fact
lemma
assumes a: "x \<noteq> y"
@@ -1145,20 +1134,20 @@
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*)
- assume c1: "z=x"
+ { -- {* Case 1.1 *}
+ 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
@@ -1166,7 +1155,7 @@
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
@@ -1180,7 +1169,7 @@
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