--- a/Tutorial/Tutorial1s.thy Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,752 +0,0 @@
-
-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 just
- adds new definitions and an infrastructure for 'nominal resoning'.
-
-
- The jEdit Interface
- -------------------
-
- The Isabelle theorem prover comes with an interface for jEdit.
- Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you
- advance a 'checked' region in a proof script, this interface immediately
- checks the whole buffer. The text you type is also immediately checked.
- 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 jEdit can be started by typing on the command line
-
- 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 the following two symbols have a special meaning
-
- \<sharp> sharp (freshness)
- \<bullet> bullet (permutation application)
-*}
-
-theory Tutorial1s
-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 Nominal2 (which provides many useful
- concepts like set-theory, lists, nominal things etc). For the purpose
- of this 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. If you
- prefer, you can have your own syntax (but \<lambda> is already taken up for
- Isabelle's functions). We also came up with the type "name" for variables.
- You can introduce your own types of object variables using the
- command atom_decl:
-*}
-
-atom_decl ident
-atom_decl ty_var
-
-text {*
- Isabelle provides some useful colour feedback about its constants (black),
- free variables (blue) and bound variables (green).
-*}
-
-term "True" -- {* a constant defined somewhere...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: Evaluation Relation *}
-
-text {*
- In this section we want to define inductively the evaluation
- 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
- 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
- eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 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 {*
- Values and cbv are also defined using inductive.
-*}
-
-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
- database can be queried using
-*}
-
-thm e_App
-thm e_Lam
-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 eval.intros
-thm eval.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: "atom y \<sharp> Lam [x].t"
- shows "(y = x) \<or> (y \<noteq> x \<and> atom y \<sharp> t)"
- using a by (auto 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
-
- 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" by auto
-qed
-
-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)" by auto
-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'" using ih3 by auto
-qed
-
-
-section {* Datatypes: Evaluation Contexts*}
-
-text {*
- Datatypes can be defined in Isabelle as follows: we have to provide the name
- 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 {* Now Isabelle knows about: *}
-
-typ ctx
-term "\<box>"
-term "CAppL"
-term "CAppL \<box> (Var x)"
-
-subsection {* MINI EXERCISE *}
-
-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: "<App t1 t2, Es> \<mapsto> <t1, (CAppL \<box> t2) # Es>"
-| m2: "val v \<Longrightarrow> <v, (CAppL \<box> t2) # Es> \<mapsto> <t2, (CAppR v \<box>) # 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: "<t,Es> \<mapsto>* <t,Es>"
-| ms2: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"
-
-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
-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
- have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih d1 by auto
- show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto
-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: "<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
-
-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: "<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
-
-
-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)
-
-
-section {* EXERCISE 4 *}
-
-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, Es> \<mapsto>* <t', Es>"
-using a
-proof (induct arbitrary: Es)
- case (e_Lam x t Es)
- -- {* no assumptions *}
- show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto
-next
- case (e_App t1 x t t2 v' v Es)
- -- {* all assumptions in this case *}
- have a1: "t1 \<Down> Lam [x].t" by fact
- have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact
- have a2: "t2 \<Down> v'" by fact
- have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact
- have a3: "t[x::=v'] \<Down> v" by fact
- have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact
- -- {* your reasoning *}
- have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto
- moreover
- have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto
- moreover
- have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto
- moreover
- have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>"
- using ih2 by auto
- moreover
- have "val v'" using a2 eval_to_val by auto
- then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto
- moreover
- have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto
- ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast
-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
-
-
-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
- "\<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" (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')"
-
-fun
- ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)
-where
- "[]\<down> = \<box>"
- | "(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
- of the arguments; the one next to it the precedence of the whole term.
-
- 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).
-*}
-
-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.
-*}
-
-subsection {* EXERCISE 5 *}
-
-text {* Complete the proof and remove the sorries. *}
-
-lemma ctx_compose:
- shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
-proof (induct E1)
- case Hole
- show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by simp
-next
- case (CAppL E1 t')
- 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>" using ih by simp
-next
- 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>" using ih by simp
-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 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>)"
-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 eq1: "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
- have eq2: "(E # (Es1 @ Es2))\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp
- have eq3: "(Es1 @ Es2)\<down> \<odot> E = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
- have eq4: "(Es2\<down> \<odot> Es1\<down>) \<odot> E = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp
- have eq5: "Es2\<down> \<odot> (Es1\<down> \<odot> E) = Es2\<down> \<odot> (E # Es1)\<down>" by simp
- show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" using eq1 eq2 eq3 eq4 eq5 by (simp only:)
-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> = (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 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
-