header {*
Nominal Isabelle Tutorial at POPL'11
====================================
Nominal Isabelle is a definitional extension of Isabelle/HOL, which
means it does not add any new axioms to higher-order logic. It merely
adds new definitions and an infrastructure for 'nominal resoning'.
The jEdit Interface
-------------------
The Isabelle theorem prover comes with an interface for the jEdit.
Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you
try to advance a 'checked' region in a proof script, this interface immediately
checks the whole buffer. The text you type is also immediately checked
as you type. Malformed text or unfinished proofs are highlighted in red
with a little red 'stop' signal on the left-hand side. If you drag the
'red-box' cursor over a line, the Output window gives further feedback.
Note: If a section is not parsed correctly, the work-around is to cut it
out and paste it back into the text (cut-out: Ctrl + X; paste in: Ctrl + V;
Cmd is Ctrl on the Mac)
Nominal Isabelle and the interface can be started on the command line with
isabelle jedit -l HOL-Nominal2
isabelle jedit -l HOL-Nominal2 A.thy B.thy ...
Symbols
-------
Symbols can considerably improve the readability of your statements and proofs.
They can be input by just typing 'name-of-symbol' where 'name-of-symbol' is the
usual latex name of that symbol. A little window will then appear in which
you can select the symbol. With `Escape' you can ignore any suggestion.
There are some handy short-cuts for frequently used symbols.
For example
short-cut symbol
=> \<Rightarrow>
==> \<Longrightarrow>
--> \<longrightarrow>
! \<forall>
? \<exists>
/\ \<and>
\/ \<or>
~ \<not>
~= \<noteq>
: \<in>
~: \<notin>
For nominal two important symbols are
\<sharp> sharp (freshness)
\<bullet> bullet (permutations)
*}
theory Tutorial1
imports Lambda
begin
section {* Theories *}
text {*
All formal developments in Isabelle are part of a theory. A theory
needs to have a name and must import some pre-existing theory. The
imported theory will normally be the theory Nominal2 (which contains
many useful concepts like set-theory, lists, nominal theory etc).
For the purpose of the tutorial we import the theory Lambda.thy which
contains already some useful definitions for (alpha-equated) lambda
terms.
*}
section {* Types *}
text {*
Isabelle is based on simple types including some polymorphism. It also
includes overloading, which means that sometimes explicit type annotations
need to be given.
- Base types include: nat, bool, string, lam (defined in the Lambda theory)
- Type formers include: 'a list, ('a \<times> 'b), 'c set
- Type variables are written like in ML with an apostrophe: 'a, 'b, \<dots>
Types known to Isabelle can be queried using the command "typ".
*}
typ nat
typ bool
typ string
typ lam -- {* alpha-equated lambda terms defined in Lambda.thy *}
typ name -- {* type of (object) variables defined in Lambda.thy *}
typ "('a \<times> 'b)" -- {* pair type *}
typ "'c set" -- {* set type *}
typ "'a list" -- {* list type *}
typ "lam \<Rightarrow> nat" -- {* type of functions from lambda terms to natural numbers *}
text {* Some malformed types - note the "stop" signal on the left margin *}
(*
typ boolean -- {* undeclared type *}
typ set -- {* type argument missing *}
*)
section {* Terms *}
text {*
Every term in Isabelle needs to be well-typed. However they can have
polymorphic type. Whether a term is accepted can be queried using
the command "term".
*}
term c -- {* a variable of polymorphic type *}
term "1::nat" -- {* the constant 1 in natural numbers *}
term 1 -- {* the constant 1 with polymorphic type *}
term "{1, 2, 3::nat}" -- {* the set containing natural numbers 1, 2 and 3 *}
term "[1, 2, 3]" -- {* the list containing the polymorphic numbers 1, 2 and 3 *}
term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *}
term "Suc 0" -- {* successor of 0, in other words 1::nat *}
term "Lam [x].Var x" -- {* a lambda-term *}
term "App t1 t2" -- {* another lambda-term *}
term "x::name" -- {* an (object) variable of type name *}
term "atom (x::name)" -- {* atom is an overloded function *}
text {*
Lam [x].Var is the syntax we made up for lambda abstractions. You can have
your own syntax, if you prefer (but \<lambda> is already taken up for Isabelle's
functions). We also came up with "name". If you prefer, you can call
it "ident" or have more than one type for (object language) variables.
Isabelle provides some useful colour feedback about its constants (black),
free variables (blue) and bound variables (green).
*}
term "True" -- {* a constant that is defined in HOL...written in black *}
term "true" -- {* not recognised as a constant, therefore it is interpreted
as a free variable, written in blue *}
term "\<forall>x. P x" -- {* x is bound (green), P is free (blue) *}
text {* Formulae in Isabelle/HOL are terms of type bool *}
term "True"
term "True \<and> False"
term "True \<or> B"
term "{1,2,3} = {3,2,1}"
term "\<forall>x. P x"
term "A \<longrightarrow> B"
term "atom a \<sharp> t" -- {* freshness in Nominal *}
text {*
When working with Isabelle, one deals with an object logic (that is HOL) and
Isabelle's rule framework (called Pure). Occasionally one has to pay attention
to this fact. But for the moment we ignore this completely.
*}
term "A \<longrightarrow> B" -- {* versus *}
term "A \<Longrightarrow> B"
term "\<forall>x. P x" -- {* versus *}
term "\<And>x. P x"
section {* Inductive Definitions: Transitive Closures of Beta-Reduction *}
text {*
The theory Lmabda already contains a definition for beta-reduction, written
*}
term "t \<longrightarrow>b t'"
text {*
In this section we want to define inductively the transitive closure of
beta-reduction.
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
"\<lbrakk>premise1; premise2; \<dots> premisen\<rbrakk> \<Longrightarrow> conclusion"
If no premise is present, then one just writes
"conclusion"
Below we give two definitions for the transitive closure
*}
inductive
beta_star1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b* _" [60, 60] 60)
where
bs1_refl: "t \<longrightarrow>b* t"
| bs1_trans: "\<lbrakk>t1 \<longrightarrow>b t2; t2 \<longrightarrow>b* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b* t3"
inductive
beta_star2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b** _" [60, 60] 60)
where
bs2_refl: "t \<longrightarrow>b** 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 bs2_trans
thm conjI
thm conjunct1
text {*
Notice that theorems usually contain schematic variables (e.g. ?P, ?Q, \<dots>).
These schematic variables can be substituted with any term (of the right type
of course).
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 beta_star2.induct
section {* Lemmas / Theorems / Corollaries *}
text {*
Whether to use lemma, theorem or corollary makes no semantic difference
in Isabelle.
A lemma starts with "lemma" and consists of a statement ("shows \<dots>") and
optionally a lemma name, some type-information for variables ("fixes \<dots>")
and some assumptions ("assumes \<dots>").
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)
lemma Lam_freshness:
assumes a: "x \<noteq> y"
and b: "atom y \<sharp> Lam [x].t"
shows "atom y \<sharp> t"
using a b by (simp add: lam.fresh Abs_fresh_iff)
lemma neutral_element:
fixes x::"nat"
shows "x + 0 = x"
by simp
text {*
Note that in the last statement, the explicit type annotation is important
in order for Isabelle to be able to figure out what 0 stands for (e.g. a
natural number, a vector, etc) and which lemmas to apply.
*}
section {* Isar Proofs *}
text {*
Isar is a language for writing formal proofs that can be understood by humans
and by Isabelle. An Isar proof can be thought of as a sequence of 'stepping stones'
that start with some assumptions and lead to the goal to be established. Every such
stepping stone is introduced by "have" followed by the statement of the stepping
stone. An exception is the goal to be proved, which need to be introduced with "show".
have "statement" \<dots>
show "goal_to_be_proved" \<dots>
Since proofs usually do not proceed in a linear fashion, labels can be given
to every stepping stone and they can be used later to explicitly refer to this
corresponding stepping stone ("using").
have label: "statement1" \<dots>
\<dots>
have "later_statement" using label \<dots>
Each stepping stone (or have-statement) needs to have a justification. The
simplest justification is "sorry" which admits any stepping stone, even false
ones (this is good during the development of proofs).
have "outrageous_false_statement" sorry
Assumptions can be 'justified' using "by fact".
have "assumption" by fact
Derived facts can be justified using
have "statement" by simp -- simplification
have "statement" by auto -- proof search and simplification
have "statement" by blast -- only proof search
If facts or lemmas are needed in order to justify a have-statement, then
one can feed these facts into the proof by using "using label \<dots>" or
"using theorem-name \<dots>". More than one label at a time is allowed. For
example
have "statement" using label1 label2 theorem_name by auto
Induction proofs in Isar are set up by indicating over which predicate(s)
the induction proceeds ("using a b") followed by the command "proof (induct)".
In this way, Isabelle uses defaults for which induction should be performed.
These defaults can be overridden by giving more information, like the variable
over which a structural induction should proceed, or a specific induction principle,
such as well-founded inductions.
After the induction is set up, the proof proceeds by cases. In Isar these
cases can be given in any order. Most commonly they are started with "case" and the
name of the case, and optionally some legible names for the variables used inside
the case.
In each "case", we need to establish a statement introduced by "show". Once
this has been done, the next case can be started using "next". When all cases
are completed, the proof can be finished using "qed".
This means a typical induction proof has the following pattern
proof (induct)
case \<dots>
\<dots>
show \<dots>
next
case \<dots>
\<dots>
show \<dots>
\<dots>
qed
*}
subsection {* Exercise I *}
text {*
Remove the sorries in the proof below and fill in the proper
justifications.
*}
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)
show "t \<longrightarrow>b* t" using bs1_refl by blast
next
case (bs2_step t1 t2)
have ih: "t1 \<longrightarrow>b t2" by fact
have a: "t2 \<longrightarrow>b* t2" using bs1_refl by blast
show "t1 \<longrightarrow>b* t2" using ih a bs1_trans by blast
next
case (bs2_trans t1 t2 t3)
have ih1: "t1 \<longrightarrow>b* t2" by fact
have ih2: "t2 \<longrightarrow>b* t3" by fact
show "t1 \<longrightarrow>b* t3" using ih1 ih2 bs1_trans2 by blast
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
"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: "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 {*
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
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 {* Now Isabelle knows about: *}
typ ctx
term "\<box>"
term "CAppL"
term "CAppL \<box> (Var x)"
text {*
1.) MINI EXERCISE
-----------------
Try and see what happens if you apply a Hole to a Hole?
*}
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>"
| m2[intro]: "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>"
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>"
| ms2[intro]: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
lemma
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
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>" sorry
qed
text {*
Just like gotos in the Basic programming language, labels can 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
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
proof(induct)
case (ms1 e1 Es1)
show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
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 "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
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
lemma
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)
show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
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 "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
then have "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
moreover
have "<e1, Es1> \<mapsto> <e2, Es2>" by fact
ultimately show "<e1, Es1> \<mapsto>* <e3, Es3>" by auto
qed
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 by (induct) (auto)
lemma eval_to_val:
assumes a: "t \<Down> t'"
shows "val t'"
using a by (induct) (auto)
theorem
assumes a: "t \<Down> t'"
shows "<t, []> \<mapsto>* <t', []>"
using a
proof (induct)
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 *)
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 *)
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: *}
theorem eval_implies_machines_ctx:
assumes a: "t \<Down> t'"
shows "<t, Es> \<mapsto>* <t', Es>"
using a
by (induct arbitrary: Es)
(metis eval_to_val machine.intros ms1 ms2 ms3 v_Lam)+
corollary eval_implies_machines:
assumes a: "t \<Down> t'"
shows "<t, []> \<mapsto>* <t', []>"
using a eval_implies_machines_ctx by simp
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.
Freshness is defined for lambda-terms, products, lists etc. For example
we have:
*}
lemma
fixes x::"name"
shows "atom x \<sharp> Lam [x].t"
and "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2"
and "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y"
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 *}
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
the subset-notation and define the abbreviation below. Abbreviations behave
like definitions, except that they are always automatically folded 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 {*****************************************************************
4.) Exercise
------------
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"
and c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"
shows "\<Gamma>2 \<turnstile> t : T"
using a b c
proof (induct arbitrary: \<Gamma>2)
case (t_Var \<Gamma>1 x T)
have a1: "valid \<Gamma>1" by fact
have a2: "(x, T) \<in> set \<Gamma>1" by fact
have a3: "valid \<Gamma>2" by fact
have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact
show "\<Gamma>2 \<turnstile> Var x : T" sorry
next
case (t_Lam x \<Gamma>1 T1 t T2)
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)
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.
*}
equivariance valid
equivariance typing
lemma not_to_be_tried_at_home_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 (induct arbitrary: \<Gamma>2)
case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
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
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 *)
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 *)
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)"
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)
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))"
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)
qed
(* 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 *)
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 *)
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
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
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 *)
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 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 *)
text {*****************************************************************
Function Definitions: Filling a Lambda-Term into a Context
----------------------------------------------------------
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
"\<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" ("_ \<cdot> _" [101,100] 100)
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')"
fun
ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)
where
"[]\<down> = \<box>"
| "(E # Es)\<down> = (Es\<down>) \<cdot> 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
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).
*}
text {******************************************************************
Structural Inductions over Contexts
------------------------------------
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 {******************************************************************
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>"
proof (induct E1)
case Hole
show "\<box> \<cdot> 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
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
qed
lemma neut_hole:
shows "E \<cdot> \<box> = E"
by (induct E) (simp_all)
lemma circ_assoc:
fixes E1 E2 E3::"ctx"
shows "(E1 \<cdot> E2) \<cdot> E3 = E1 \<cdot> (E2 \<cdot> E3)"
by (induct E1) (simp_all)
lemma
shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"
proof (induct Es1)
case Nil
show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" sorry
next
case (Cons E Es1)
have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<cdot> Es1\<down>" by fact
show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (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>) \<cdot> (Es1\<down>)"
proof (induct Es1)
case Nil
show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<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
qed
text {******************************************************************
Formalising Barendregt's Proof of the Substitution Lemma
--------------------------------------------------------
Barendregt's proof needs in the variable case a case distinction.
One way to do this in Isar is to use blocks. A block is some sequent
or reasoning steps enclosed in curly braces
{ \<dots>
have "statement"
}
Such a block can contain local assumptions like
{ assume "A"
assume "B"
\<dots>
have "C" by \<dots>
}
Where "C" is the last have-statement in this block. The behaviour
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:
{ assume "P\<^isub>1"
\<dots>
have "smth"
}
moreover
{ assume "P\<^isub>2"
\<dots>
have "smth"
}
moreover
{ assume "P\<^isub>3"
\<dots>
have "smth"
}
ultimately have "smth" by blast
The blocks establish the implications
P\<^isub>1 \<Longrightarrow> smth
P\<^isub>2 \<Longrightarrow> smth
P\<^isub>3 \<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
true, then we have 'ultimately' established the property "smth"
*}
text {******************************************************************
7.) Exercise
------------
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
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)
apply (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]]"
using a b
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
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*)
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*)
assume c2: "z = y" "z \<noteq> x"
have "?LHS = ?RHS" sorry
}
moreover
{ (*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 *)
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)
show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS")
proof -
have "?LHS = \<dots>" sorry
also have "\<dots> = ?RHS" sorry
finally show "?LHS = ?RHS" by simp
qed
next
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
the proof of the substitution lemma automatically.
*}
lemma substitution_lemma_version:
assumes asm: "x \<noteq> y" "atom x \<sharp> L"
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using asm
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
(auto simp add: fresh_fact forget)
end