1 

     2 header {* 

     3 

     4   Nominal Isabelle Tutorial at POPL'11

     5   ====================================

     6 

     7   Nominal Isabelle is a definitional extension of Isabelle/HOL, which

     8   means it does not add any new axioms to higher-order logic. It just

     9   adds new definitions and an infrastructure for 'nominal resoning'.

    10 

    11 

    12   The jEdit Interface

    13   -------------------

    14 

    15   The Isabelle theorem prover comes with an interface for jEdit. 

    16   Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you 

    17   advance a 'checked' region in a proof script, this interface immediately 

    18   checks the whole buffer. The text you type is also immediately checked. 

    19   Malformed text or unfinished proofs are highlighted in red with a little 

    20   red 'stop' signal on the left-hand side. If you drag the 'red-box' cursor 

    21   over a line, the Output window gives further feedback. 

    22 

    23   Note: If a section is not parsed correctly, the work-around is to cut it 

    24   out and paste it back into the text (cut-out: Ctrl + X; paste in: Ctrl + V;

    25   Cmd is Ctrl on the Mac)

    26 

    27   Nominal Isabelle and jEdit can be started by typing on the command line

    28 

    29      isabelle jedit -l HOL-Nominal2

    30      isabelle jedit -l HOL-Nominal2 A.thy B.thy ...

    31 

    32 

    33   Symbols

    34   ------- 

    35 

    36   Symbols can considerably improve the readability of your statements and proofs. 

    37   They can be input by just typing 'name-of-symbol' where 'name-of-symbol' is the 

    38   usual latex name of that symbol. A little window will then appear in which 

    39   you can select the symbol. With `Escape' you can ignore any suggestion.

    40   

    41   There are some handy short-cuts for frequently used symbols. 

    42   For example 

    43 

    44       short-cut  symbol

    45 

    46           =>      \<Rightarrow>

    47           ==>     \<Longrightarrow>

    48           -->     \<longrightarrow>

    49           !       \<forall>        

    50           ?       \<exists>

    51           /\      \<and>

    52           \/      \<or>

    53           ~       \<not>

    54           ~=      \<noteq>

    55           :       \<in>

    56           ~:      \<notin>

    57 

    58   For nominal the following two symbols have a special meaning

    59 

    60         \<sharp>    sharp     (freshness)

    61         \<bullet>    bullet    (permutation application)

    62 *}

    63 

    64 theory Tutorial1s

    65 imports Lambda

    66 begin

    67 

    68 section {* Theories *}

    69 

    70 text {*

    71   All formal developments in Isabelle are part of a theory. A theory 

    72   needs to have a name and must import some pre-existing theory. The 

    73   imported theory will normally be Nominal2 (which provides many useful 

    74   concepts like set-theory, lists, nominal things etc). For the purpose 

    75   of this tutorial we import the theory Lambda.thy, which contains 

    76   already some useful definitions for (alpha-equated) lambda terms.

    77 *}

    78 

    79 

    80 

    81 section {* Types *}

    82 

    83 text {*

    84   Isabelle is based on simple types including some polymorphism. It also 

    85   includes overloading, which means that sometimes explicit type annotations 

    86   need to be given.

    87 

    88     - Base types include: nat, bool, string, lam (defined in the Lambda theory)

    89 

    90     - Type formers include: 'a list, ('a \<times> 'b), 'c set   

    91 

    92     - Type variables are written like in ML with an apostrophe: 'a, 'b, \<dots>

    93 

    94   Types known to Isabelle can be queried using the command "typ".

    95 *}

    96 

    97 typ nat

    98 typ bool

    99 typ string           

   100 typ lam           -- {* alpha-equated lambda terms defined in Lambda.thy *}

   101 typ name          -- {* type of (object) variables defined in Lambda.thy *}

   102 typ "('a \<times> 'b)"   -- {* pair type *}

   103 typ "'c set"      -- {* set type *}

   104 typ "'a list"     -- {* list type *}

   105 typ "lam \<Rightarrow> nat"   -- {* type of functions from lambda terms to natural numbers *}

   106 

   107 

   108 text {* Some malformed types - note the "stop" signal on the left margin *}

   109 

   110 (*

   111 typ boolean     -- {* undeclared type *} 

   112 typ set         -- {* type argument missing *}

   113 *)

   114 

   115 

   116 section {* Terms *}

   117 

   118 text {*

   119    Every term in Isabelle needs to be well-typed. However they can have 

   120    polymorphic type. Whether a term is accepted can be queried using

   121    the command "term". 

   122 *}

   123 

   124 term c                 -- {* a variable of polymorphic type *}

   125 term "1::nat"          -- {* the constant 1 in natural numbers *}

   126 term 1                 -- {* the constant 1 with polymorphic type *}

   127 term "{1, 2, 3::nat}"  -- {* the set containing natural numbers 1, 2 and 3 *}

   128 term "[1, 2, 3]"       -- {* the list containing the polymorphic numbers 1, 2 and 3 *}

   129 term "(True, ''c'')"   -- {* a pair consisting of the boolean true and the string "c" *}

   130 term "Suc 0"           -- {* successor of 0, in other words 1::nat *}

   131 term "Lam [x].Var x"   -- {* a lambda-term *}

   132 term "App t1 t2"       -- {* another lambda-term *}

   133 term "x::name"         -- {* an (object) variable of type name *}

   134 term "atom (x::name)"  -- {* atom is an overloded function *}

   135 

   136 text {* 

   137   Lam [x].Var is the syntax we made up for lambda abstractions. If you

   138   prefer, you can have your own syntax (but \<lambda> is already taken up for 

   139   Isabelle's functions). We also came up with the type "name" for variables. 

   140   You can introduce your own types of object variables using the 

   141   command atom_decl: 

   142 *}

   143 

   144 atom_decl ident

   145 atom_decl ty_var

   146 

   147 text {*

   148   Isabelle provides some useful colour feedback about its constants (black), 

   149   free variables (blue) and bound variables (green).

   150 *}

   151 

   152 term "True"    -- {* a constant defined somewhere...written in black *}

   153 term "true"    -- {* not recognised as a constant, therefore it is interpreted

   154                      as a free variable, written in blue *}

   155 term "\<forall>x. P x" -- {* x is bound (green), P is free (blue) *}

   156 

   157 

   158 text {* Formulae in Isabelle/HOL are terms of type bool *}

   159 

   160 term "True"

   161 term "True \<and> False"

   162 term "True \<or> B"

   163 term "{1,2,3} = {3,2,1}"

   164 term "\<forall>x. P x"

   165 term "A \<longrightarrow> B"

   166 term "atom a \<sharp> t"   -- {* freshness in Nominal *}

   167 

   168 text {*

   169   When working with Isabelle, one deals with an object logic (that is HOL) and 

   170   Isabelle's rule framework (called Pure). Occasionally one has to pay attention 

   171   to this fact. But for the moment we ignore this completely.

   172 *}

   173 

   174 term "A \<longrightarrow> B"  -- {* versus *}

   175 term "A \<Longrightarrow> B"

   176 

   177 term "\<forall>x. P x"  -- {* versus *}

   178 term "\<And>x. P x"

   179 

   180 

   181 section {* Inductive Definitions: Evaluation Relation *}

   182 

   183 text {*

   184   In this section we want to define inductively the evaluation

   185   relation and for cbv-reduction relation.

   186 

   187   Inductive definitions in Isabelle start with the keyword "inductive" 

   188   and a predicate name.  One can optionally provide a type for the predicate. 

   189   Clauses of the inductive predicate are introduced by "where" and more than 

   190   two clauses need to be separated by "|". One can also give a name to each 

   191   clause and indicate that it should be added to the hints database ("[intro]"). 

   192   A typical clause has some premises and a conclusion. This is written in 

   193   Isabelle as:

   194 

   195    "premise \<Longrightarrow> conclusion"

   196    "premise1 \<Longrightarrow> premise2 \<Longrightarrow> \<dots> premisen \<Longrightarrow> conclusion"

   197 

   198   There is an alternative way of writing the latter clause as

   199 

   200    "\<lbrakk>premise1; premise2; \<dots> premisen\<rbrakk> \<Longrightarrow> conclusion"

   201 

   202   If no premise is present, then one just writes

   203 

   204    "conclusion"

   205 

   206   Below we give two definitions for the transitive closure

   207 *}

   208 

   209 inductive

   210   eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 

   211 where

   212   e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"

   213 | e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"

   214 

   215 text {* 

   216   Values and cbv are also defined using inductive.  

   217 *}

   218 

   219 inductive

   220   val :: "lam \<Rightarrow> bool" 

   221 where

   222   v_Lam[intro]:   "val (Lam [x].t)"

   223 

   224 section {* Theorems *}

   225 

   226 text {*

   227   A central concept in Isabelle is that of theorems. Isabelle's theorem

   228   database can be queried using 

   229 *}

   230 

   231 thm e_App

   232 thm e_Lam

   233 thm conjI

   234 thm conjunct1

   235 

   236 text {* 

   237   Notice that theorems usually contain schematic variables (e.g. ?P, ?Q, \<dots>). 

   238   These schematic variables can be substituted with any term (of the right type 

   239   of course). 

   240 

   241   When defining the predicates beta_star, Isabelle provides us automatically 

   242   with the following theorems that state how they can be introduced and what 

   243   constitutes an induction over them. 

   244 *}

   245 

   246 thm eval.intros

   247 thm eval.induct

   248 

   249 

   250 section {* Lemmas / Theorems / Corollaries *}

   251 

   252 text {*

   253   Whether to use lemma, theorem or corollary makes no semantic difference 

   254   in Isabelle. 

   255 

   256   A lemma starts with "lemma" and consists of a statement ("shows \<dots>") and 

   257   optionally a lemma name, some type-information for variables ("fixes \<dots>") 

   258   and some assumptions ("assumes \<dots>"). 

   259 

   260   Lemmas also need to have a proof, but ignore this 'detail' for the moment.

   261 

   262   Examples are

   263 *}

   264 

   265 lemma alpha_equ:

   266   shows "Lam [x].Var x = Lam [y].Var y"

   267   by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base)

   268 

   269 lemma Lam_freshness:

   270   assumes a: "atom y \<sharp> Lam [x].t"

   271   shows "(y = x) \<or> (y \<noteq> x \<and> atom y \<sharp> t)"

   272   using a by (auto simp add: lam.fresh Abs_fresh_iff) 

   273 

   274 lemma neutral_element:

   275   fixes x::"nat"

   276   shows "x + 0 = x"

   277   by simp

   278 

   279 text {*

   280   Note that in the last statement, the explicit type annotation is important 

   281   in order for Isabelle to be able to figure out what 0 stands for (e.g. a 

   282   natural number, a vector, etc) and which lemmas to apply.

   283 *}

   284 

   285 

   286 section {* Isar Proofs *}

   287 

   288 text {*

   289   Isar is a language for writing formal proofs that can be understood by humans 

   290   and by Isabelle. An Isar proof can be thought of as a sequence of 'stepping stones' 

   291   that start with some assumptions and lead to the goal to be established. Every such 

   292   stepping stone is introduced by "have" followed by the statement of the stepping 

   293   stone. An exception is the goal to be proved, which need to be introduced with "show".

   294 

   295       have "statement"  \<dots>

   296       show "goal_to_be_proved" \<dots>

   297 

   298   Since proofs usually do not proceed in a linear fashion, labels can be given 

   299   to every stepping stone and they can be used later to explicitly refer to this 

   300   corresponding stepping stone ("using").

   301 

   302       have label: "statement1"  \<dots>

   303       \<dots>

   304       have "later_statement" using label \<dots>

   305 

   306   Each stepping stone (or have-statement) needs to have a justification. The 

   307   simplest justification is "sorry" which admits any stepping stone, even false 

   308   ones (this is good during the development of proofs). 

   309 

   310       have "outrageous_false_statement" sorry

   311 

   312   Assumptions can be 'justified' using "by fact". 

   313 

   314       have "assumption" by fact

   315 

   316   Derived facts can be justified using 

   317 

   318       have "statement" by simp    -- simplification 

   319       have "statement" by auto    -- proof search and simplification 

   320       have "statement" by blast   -- only proof search 

   321 

   322   If facts or lemmas are needed in order to justify a have-statement, then

   323   one can feed these facts into the proof by using "using label \<dots>" or 

   324   "using theorem-name \<dots>". More than one label at a time is allowed. For

   325   example

   326 

   327       have "statement" using label1 label2 theorem_name by auto

   328 

   329   Induction proofs in Isar are set up by indicating over which predicate(s) 

   330   the induction proceeds ("using a b") followed by the command "proof (induct)". 

   331   In this way, Isabelle uses defaults for which induction should be performed. 

   332   These defaults can be overridden by giving more information, like the variable 

   333   over which a structural induction should proceed, or a specific induction principle, 

   334   such as well-founded inductions. 

   335 

   336   After the induction is set up, the proof proceeds by cases. In Isar these 

   337   cases can be given in any order. Most commonly they are started with "case" and the 

   338   name of the case, and optionally some legible names for the variables used inside 

   339   the case. 

   340 

   341   In each "case", we need to establish a statement introduced by "show". Once 

   342   this has been done, the next case can be started using "next". When all cases 

   343   are completed, the proof can be finished using "qed".

   344 

   345   This means a typical induction proof has the following pattern

   346 

   347      proof (induct)

   348        case \<dots>

   349        \<dots>

   350        show \<dots>

   351      next

   352        case \<dots>

   353        \<dots>

   354        show \<dots>

   355      \<dots>

   356      qed

   357 

   358    Two very simple example proofs are as follows.

   359 *}

   360 

   361 subsection {* EXERCISE 1 *}

   362 

   363 lemma eval_val:

   364   assumes a: "val t"

   365   shows "t \<Down> t"

   366 using a

   367 proof (induct)

   368   case (v_Lam x t)

   369   show "Lam [x]. t \<Down> Lam [x]. t" by auto

   370 qed

   371 

   372 subsection {* EXERCISE 2 *}

   373 

   374 text {* Fill the gaps in the proof below. *}

   375 

   376 lemma eval_to_val:

   377   assumes a: "t \<Down> t'"

   378   shows "val t'"

   379 using a

   380 proof (induct)

   381   case (e_Lam x t)

   382   show "val (Lam [x].t)" by auto

   383 next

   384   case (e_App t1 x t t2 v v')

   385   -- {* all assumptions in this case *}

   386   have "t1 \<Down> Lam [x].t" by fact

   387   have ih1: "val (Lam [x]. t)" by fact

   388   have "t2 \<Down> v" by fact

   389   have ih2: "val v" by fact

   390   have "t [x ::= v] \<Down> v'" by fact

   391   have ih3: "val v'" by fact

   392 

   393   show "val v'" using ih3 by auto

   394 qed

   395 

   396 

   397 section {* Datatypes: Evaluation Contexts*}

   398 

   399 text {*

   400   Datatypes can be defined in Isabelle as follows: we have to provide the name 

   401   of the datatype and a list its type-constructors. Each type-constructor needs 

   402   to have the information about the types of its arguments, and optionally 

   403   can also contain some information about pretty syntax. For example, we like

   404   to write "\<box>" for holes.

   405 *}

   406   

   407 datatype ctx = 

   408     Hole ("\<box>")  

   409   | CAppL "ctx" "lam"

   410   | CAppR "lam" "ctx"

   411 

   412 text {* Now Isabelle knows about: *}

   413 

   414 typ ctx

   415 term "\<box>"

   416 term "CAppL"

   417 term "CAppL \<box> (Var x)"

   418 

   419 subsection {* MINI EXERCISE *}

   420 

   421 text {*

   422   Try and see what happens if you apply a Hole to a Hole? 

   423 *}

   424 

   425 

   426 section {* Machines for Evaluation *}

   427 

   428 type_synonym ctxs = "ctx list"

   429 

   430 inductive

   431   machine :: "lam \<Rightarrow> ctxs \<Rightarrow>lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto> <_,_>" [60, 60, 60, 60] 60)

   432 where

   433   m1: "<App t1 t2, Es> \<mapsto> <t1, (CAppL \<box> t2) # Es>"

   434 | m2: "val v \<Longrightarrow> <v, (CAppL \<box> t2) # Es> \<mapsto> <t2, (CAppR v \<box>) # Es>"

   435 | m3: "val v \<Longrightarrow> <v, (CAppR (Lam [x].t) \<box>) # Es> \<mapsto> <t[x ::= v], Es>"

   436 

   437 text {*

   438   Since the machine defined above only performs a single reduction,

   439   we need to define the transitive closure of this machine. *}

   440 

   441 inductive 

   442   machines :: "lam \<Rightarrow> ctxs \<Rightarrow> lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto>* <_,_>" [60, 60, 60, 60] 60)

   443 where

   444   ms1: "<t,Es> \<mapsto>* <t,Es>"

   445 | ms2: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"

   446 

   447 declare machine.intros[intro] machines.intros[intro]

   448 

   449 section {* EXERCISE 3 *}

   450 

   451 text {*

   452   We need to show that the machines-relation is transitive.

   453   Fill in the gaps below.   

   454 *}

   455 

   456 lemma ms3[intro]:

   457   assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 

   458   and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"

   459   shows "<e1, Es1> \<mapsto>* <e3, Es3>"

   460 using a b

   461 proof(induct)

   462   case (ms1 e1 Es1)

   463   have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact

   464   then show "<e1, Es1> \<mapsto>* <e3, Es3>" by simp

   465 next

   466   case (ms2 e1 Es1 e2 Es2 e2' Es2') 

   467   have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact

   468   have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact

   469   have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact

   470   have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih d1 by auto

   471   show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto

   472 qed

   473 

   474 text {* 

   475   Just like gotos in the Basic programming language, labels often reduce 

   476   the readability of proofs. Therefore one can use in Isar the notation

   477   "then have" in order to feed a have-statement to the proof of 

   478   the next have-statement. This is used in teh second case below.

   479 *}

   480  

   481 lemma 

   482   assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 

   483   and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"

   484   shows "<e1, Es1> \<mapsto>* <e3, Es3>"

   485 using a b

   486 proof(induct)

   487   case (ms1 e1 Es1)

   488   show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact

   489 next

   490   case (ms2 e1 Es1 e2 Es2 e2' Es2')

   491   have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact

   492   have "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact

   493   then have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp

   494   have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact

   495   show "<e1, Es1> \<mapsto>* <e3, Es3>" using d2 d3 by auto

   496 qed

   497 

   498 text {* 

   499   The label ih2 cannot be got rid of in this way, because it is used 

   500   two lines below and we cannot rearange them. We can still avoid the

   501   label by feeding a sequence of facts into a proof using the 

   502   "moreover"-chaining mechanism:

   503 

   504    have "statement_1" \<dots>

   505    moreover

   506    have "statement_2" \<dots>

   507    \<dots>

   508    moreover

   509    have "statement_n" \<dots>

   510    ultimately have "statement" \<dots>

   511 

   512   In this chain, all "statement_i" can be used in the proof of the final 

   513   "statement". With this we can simplify our proof further to:

   514 *}

   515 

   516 lemma 

   517   assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 

   518   and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"

   519   shows "<e1, Es1> \<mapsto>* <e3, Es3>"

   520 using a b

   521 proof(induct)

   522   case (ms1 e1 Es1)

   523   show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact

   524 next

   525   case (ms2 e1 Es1 e2 Es2 e2' Es2')

   526   have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact

   527   have "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact

   528   then have "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp

   529   moreover

   530   have "<e1, Es1> \<mapsto> <e2, Es2>" by fact

   531   ultimately show "<e1, Es1> \<mapsto>* <e3, Es3>" by auto

   532 qed

   533 

   534 

   535 text {* 

   536   While automatic proof procedures in Isabelle are not able to prove statements

   537   like "P = NP" assuming usual definitions for P and NP, they can automatically

   538   discharge the lemmas we just proved. For this we only have to set up the induction

   539   and auto will take care of the rest. This means we can write:

   540 *}

   541 

   542 lemma 

   543   assumes a: "val t"

   544   shows "t \<Down> t"

   545 using a by (induct) (auto)

   546 

   547 lemma 

   548   assumes a: "t \<Down> t'"

   549   shows "val t'"

   550 using a by (induct) (auto)

   551 

   552 lemma

   553   assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 

   554   and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"

   555   shows "<e1, Es1> \<mapsto>* <e3, Es3>"

   556 using a b by (induct) (auto)

   557 

   558 

   559 section {* EXERCISE 4 *}

   560 

   561 text {*

   562   The point of the machine is that it simulates the evaluation

   563   relation. Therefore we like to prove the following:

   564 *}

   565 

   566 theorem 

   567   assumes a: "t \<Down> t'"

   568   shows "<t, Es> \<mapsto>* <t', Es>"

   569 using a 

   570 proof (induct arbitrary: Es)

   571   case (e_Lam x t Es) 

   572   -- {* no assumptions *}

   573   show "<Lam [x].t, Es> \<mapsto>* <Lam [x].t, Es>" by auto

   574 next

   575   case (e_App t1 x t t2 v' v Es) 

   576   -- {* all assumptions in this case *}

   577   have a1: "t1 \<Down> Lam [x].t" by fact

   578   have ih1: "\<And>Es. <t1, Es> \<mapsto>* <Lam [x].t, Es>" by fact

   579   have a2: "t2 \<Down> v'" by fact

   580   have ih2: "\<And>Es. <t2, Es> \<mapsto>* <v', Es>" by fact

   581   have a3: "t[x::=v'] \<Down> v" by fact

   582   have ih3: "\<And>Es. <t[x::=v'], Es> \<mapsto>* <v, Es>" by fact

   583   -- {* your reasoning *}

   584   have "<App t1 t2, Es> \<mapsto>* <t1, CAppL \<box> t2 # Es>" by auto

   585   moreover

   586   have "<t1, CAppL \<box> t2 # Es> \<mapsto>* <Lam [x].t, CAppL \<box> t2 # Es>" using ih1 by auto 

   587   moreover

   588   have "<Lam [x].t, CAppL \<box> t2 # Es> \<mapsto>* <t2, CAppR (Lam [x].t) \<box> # Es>" by auto

   589   moreover

   590   have "<t2, CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <v', CAppR (Lam [x].t) \<box> # Es>" 

   591   using ih2 by auto

   592   moreover

   593   have "val v'" using a2 eval_to_val by auto

   594   then have "<v', CAppR (Lam [x].t) \<box> # Es> \<mapsto>* <t[x::=v'], Es>" by auto

   595   moreover

   596   have "<t[x::=v'], Es> \<mapsto>* <v, Es>" using ih3 by auto

   597   ultimately show "<App t1 t2, Es> \<mapsto>* <v, Es>" by blast

   598 qed

   599 

   600 

   601 text {* 

   602   Again the automatic tools in Isabelle can discharge automatically 

   603   of the routine work in these proofs. We can write: 

   604 *}

   605 

   606 theorem eval_implies_machines_ctx:

   607   assumes a: "t \<Down> t'"

   608   shows "<t, Es> \<mapsto>* <t', Es>"

   609 using a

   610 by (induct arbitrary: Es)

   611    (metis eval_to_val machine.intros ms1 ms2 ms3 v_Lam)+

   612 

   613 corollary eval_implies_machines:

   614   assumes a: "t \<Down> t'"

   615   shows "<t, []> \<mapsto>* <t', []>"

   616 using a eval_implies_machines_ctx by simp

   617 

   618 

   619 section {* Function Definitions: Filling a Lambda-Term into a Context *}

   620  

   621 text {*

   622   Many functions over datatypes can be defined by recursion on the

   623   structure. For this purpose, Isabelle provides "fun". To use it one needs 

   624   to give a name for the function, its type, optionally some pretty-syntax 

   625   and then some equations defining the function. Like in "inductive",

   626   "fun" expects that more than one such equation is separated by "|".

   627 *}

   628 

   629 fun

   630   filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100, 100] 100)

   631 where

   632   "\<box>\<lbrakk>t\<rbrakk> = t"

   633 | "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"

   634 | "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"

   635 

   636 

   637 text {* 

   638   After this definition Isabelle will be able to simplify

   639   statements like: 

   640 *}

   641 

   642 lemma 

   643   shows "(CAppL \<box> (Var x))\<lbrakk>Var y\<rbrakk> = App (Var y) (Var x)"

   644   by simp

   645 

   646 fun 

   647  ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99)

   648 where

   649   "\<box> \<odot> E' = E'"

   650 | "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"

   651 | "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')"

   652 

   653 fun

   654   ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)

   655 where

   656     "[]\<down> = \<box>"

   657   | "(E # Es)\<down> = (Es\<down>) \<odot> E"

   658 

   659 text {*  

   660   Notice that we not just have given a pretty syntax for the functions, but

   661   also some precedences. The numbers inside the [\<dots>] stand for the precedences

   662   of the arguments; the one next to it the precedence of the whole term.

   663   

   664   This means we have to write (Es1 \<odot> Es2) \<odot> Es3 otherwise Es1 \<odot> Es2 \<odot> Es3 is

   665   interpreted as Es1 \<odot> (Es2 \<odot> Es3).

   666 *}

   667 

   668 section {* Structural Inductions over Contexts *}

   669  

   670 text {*

   671   So far we have had a look at an induction over an inductive predicate. 

   672   Another important induction principle is structural inductions for 

   673   datatypes. To illustrate structural inductions we prove some facts

   674   about context composition, some of which we will need later on.

   675 *}

   676 

   677 subsection {* EXERCISE 5 *}

   678 

   679 text {* Complete the proof and remove the sorries. *}

   680 

   681 lemma

   682   shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"

   683 proof (induct E1)

   684   case Hole

   685   show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by simp

   686 next

   687   case (CAppL E1 t')

   688   have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact

   689   show "((CAppL E1 t') \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" using ih by simp

   690 next

   691   case (CAppR t' E1)

   692   have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact

   693   show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" using ih by simp

   694 qed

   695 

   696 subsection {* EXERCISE 6 *}

   697 

   698 text {*

   699   Remove the sorries in the ctx_append proof below. You can make 

   700   use of the following two properties.    

   701 *}

   702 

   703 lemma neut_hole:

   704   shows "E \<odot> \<box> = E"

   705 by (induct E) (simp_all)

   706 

   707 lemma compose_assoc:  

   708   shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"

   709 by (induct E1) (simp_all)

   710 

   711 lemma

   712   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"

   713 proof (induct Es1)

   714   case Nil

   715   show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp

   716 next

   717   case (Cons E Es1)

   718   have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact

   719   have eq1: "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp

   720   have eq2: "(E # (Es1 @ Es2))\<down> = (Es1 @ Es2)\<down> \<odot> E" by simp

   721   have eq3: "(Es1 @ Es2)\<down> \<odot> E = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp

   722   have eq4: "(Es2\<down> \<odot> Es1\<down>) \<odot> E = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp

   723   have eq5: "Es2\<down> \<odot> (Es1\<down> \<odot> E) = Es2\<down> \<odot> (E # Es1)\<down>" by simp

   724   show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" using eq1 eq2 eq3 eq4 eq5 by (simp only:)

   725 qed

   726 

   727 text {* 

   728   The last proof involves several steps of equational reasoning.

   729   Isar provides some convenient means to express such equational 

   730   reasoning in a much cleaner fashion using the "also have" 

   731   construction. 

   732 *}

   733 

   734 lemma 

   735   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"

   736 proof (induct Es1)

   737   case Nil

   738   show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp

   739 next

   740   case (Cons E Es1)

   741   have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact

   742   have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp

   743   also have "\<dots> = (Es1 @ Es2)\<down> \<odot> E" by simp

   744   also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp

   745   also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp

   746   also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp

   747   finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp

   748 qed

   749 

   750 

   751 end  

   752