1 

     2 header {* 

     3 

     4   Nominal Isabelle Tutorial

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

     6 

     7   There will be hands-on exercises throughout the tutorial. Therefore

     8   it would be good if you have your own laptop.

     9 

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

    11   means it does not add any new axioms to higher-order logic. It merely

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

    13 

    14 

    15   The Interface

    16   -------------

    17 

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

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

    20   try to advance a 'checked' region in a proof script, this interface immediately 

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

    22   as you type. Malformed text or unfinished proofs are highlighted in red 

    23   with a little red 'stop' signal on the left-hand side. If you drag the 

    24   'red-box' cursor over a line, the Output window gives further feedback. 

    25 

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

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

    28   Cmd is Ctrl on the Mac)

    29 

    30   Nominal Isabelle and the interface can be started on the command line with

    31 

    32      isabelle jedit -l HOL-Nominal2

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

    34 

    35 

    36   Symbols

    37   ------- 

    38 

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

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

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

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

    43   

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

    45   For example 

    46 

    47       short-cut  symbol

    48 

    49           =>      \<Rightarrow>

    50           ==>     \<Longrightarrow>

    51           -->     \<longrightarrow>

    52           !       \<forall>        

    53           ?       \<exists>

    54           /\      \<and>

    55           \/      \<or>

    56           ~       \<not>

    57           ~=      \<noteq>

    58           :       \<in>

    59           ~:      \<notin>

    60 

    61   For nominal two important symbols are

    62 

    63           \<sharp>       sharp     (freshness)

    64           \<bullet>       bullet    (permutations)

    65 *}

    66 

    67 theory Tutorial1

    68 imports Lambda

    69 begin

    70 

    71 section {* Theories *}

    72 

    73 text {*

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

    75   needs to have a name and must import some pre-existing theory (as indicated 

    76   above). The imported theory will normally be the theory Nominal2 (which 

    77   contains many useful concepts like set-theory, lists, nominal theory etc).

    78 

    79   For the purpose of the tutorial we import the theory Lambda.thy which

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

    81 *}

    82 

    83 

    84 

    85 section {* Types *}

    86 

    87 text {*

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

    89   some overloading, which means that sometimes explicit type annotations need to 

    90   be given.

    91 

    92     - Base types include: nat, bool, string

    93 

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

    95 

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

    97 

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

    99 *}

   100 

   101 typ nat

   102 typ bool

   103 typ string           

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

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

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

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

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

   109 typ "nat \<Rightarrow> bool"   -- {* type of functions from natural numbers to booleans *}

   110 

   111 

   112 text {* Some malformed types: *}

   113 

   114 (*

   115 typ boolean     -- {* undeclared type *} 

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

   117 *)

   118 

   119 

   120 section {* Terms *}

   121 

   122 text {*

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

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

   125    the command "term". 

   126 *}

   127 

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

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

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

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

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

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

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

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

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

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

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

   139 

   140 text {* 

   141   Lam [x].Var is the syntax we made up for lambda abstractions. You can have

   142   your own syntax. We also came up with "name". If you prefer, you can call

   143   it identifiers or have more than one type for (object languag) variables.

   144 

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

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

   147 *}

   148 

   149 term "True"    -- {* a constant that is defined in HOL...written in black *}

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

   151                      as a free variable, written in blue *}

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

   153 

   154 

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

   156 

   157 term "True"

   158 term "True \<and> False"

   159 term "True \<or> B"

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

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

   162 term "A \<longrightarrow> B"

   163 term "atom a \<sharp> t"

   164 

   165 text {*

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

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

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

   169 *}

   170 

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

   172 term "A \<Longrightarrow> B"

   173 

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

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

   176 

   177 

   178 

   179 section {* Inductive Definitions: Transitive Closures of Beta-Reduction *}

   180 

   181 text {*

   182   The theory Lmabda alraedy contains a definition for beta-reduction, written

   183 

   184      t \<longrightarrow>b t'

   185 

   186   In this section we want to define inductively the transitive closure of

   187   beta-reduction.

   188 

   189   Inductive definitions in Isabelle start with the keyword "inductive" and a predicate 

   190   name.  One can optionally provide a type for the predicate. Clauses of the inductive

   191   predicate are introduced by "where" and more than two clauses need to be 

   192   separated by "|". One can also give a name to each clause and indicate that it 

   193   should be added to the hints database ("[intro]"). A typical clause has some 

   194   premises and a conclusion. This is written in Isabelle as:

   195 

   196    "premise \<Longrightarrow> conclusion"

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

   198 

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

   200 

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

   202 

   203   If no premise is present, then one just writes

   204 

   205    "conclusion"

   206 

   207   Below we give two definitions for the transitive closure

   208 *}

   209 

   210 inductive

   211   beta_star1 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b* _" [60, 60] 60)

   212 where

   213   bs1_refl: "t \<longrightarrow>b* t"

   214 | bs1_trans: "\<lbrakk>t1 \<longrightarrow>b t2; t2 \<longrightarrow>b* t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b* t3"

   215 

   216 

   217 inductive

   218   beta_star2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<longrightarrow>b** _" [60, 60] 60)

   219 where

   220   bs2_refl: "t \<longrightarrow>b** t"

   221 | bs2_step: "t1 \<longrightarrow>b t2 \<Longrightarrow> t1 \<longrightarrow>b** t2"

   222 | bs2_trans: "\<lbrakk>t1 \<longrightarrow>b** t2; t2 \<longrightarrow>b** t3\<rbrakk> \<Longrightarrow> t1 \<longrightarrow>b** t3"

   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 bs1_refl

   232 thm bs2_trans

   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 beta_star1.intros

   247 thm beta_star2.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: "x \<noteq> y"

   271   and     b: "atom y \<sharp> Lam [x].t"

   272   shows "atom y \<sharp> t"

   273   using a b by (simp add: lam.fresh Abs_fresh_iff) 

   274 

   275 lemma neutral_element:

   276   fixes x::"nat"

   277   shows "x + 0 = x"

   278   by simp

   279 

   280 text {*

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

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

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

   284 *}

   285 

   286 

   287 section {* Isar Proofs *}

   288 

   289 text {*

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

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

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

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

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

   295 

   296       have "statement"  \<dots>

   297       show "goal_to_be_proved" \<dots>

   298 

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

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

   301   corresponding stepping stone ("using").

   302 

   303       have label: "statement1"  \<dots>

   304       \<dots>

   305       have "later_statement" using label \<dots>

   306 

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

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

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

   310 

   311       have "outrageous_false_statement" sorry

   312 

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

   314 

   315       have "assumption" by fact

   316 

   317   Derived facts can be justified using 

   318 

   319       have "statement" by simp    -- simplification 

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

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

   322 

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

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

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

   326   example

   327 

   328       have "statement" using label1 label2 theorem_name by auto

   329 

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

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

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

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

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

   335   such as well-founded inductions. 

   336 

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

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

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

   340   the case. 

   341 

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

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

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

   345 

   346   This means a typical induction proof has the following pattern

   347 

   348      proof (induct)

   349        case \<dots>

   350        \<dots>

   351        show \<dots>

   352      next

   353        case \<dots>

   354        \<dots>

   355        show \<dots>

   356      \<dots>

   357      qed

   358 *}

   359 

   360 

   361 subsection {* Exercise I *}

   362 

   363 text {*

   364   Remove the sorries in the proof below and fill in the proper

   365   justifications. 

   366 *}

   367 

   368 

   369 lemma

   370   assumes a: "t1 \<longrightarrow>b* t2" 

   371   shows "t1 \<longrightarrow>b** t2"

   372   using a

   373 proof (induct)

   374   case (bs1_refl t)

   375   show "t \<longrightarrow>b** t" using bs2_refl by blast

   376 next

   377   case (bs1_trans t1 t2 t3)

   378   have beta: "t1 \<longrightarrow>b t2" by fact

   379   have ih: "t2 \<longrightarrow>b** t3" by fact

   380   have a: "t1 \<longrightarrow>b** t2" using beta bs2_step by blast

   381   show "t1 \<longrightarrow>b** t3" using a ih bs2_trans by blast

   382 qed

   383 

   384 

   385 subsection {* Exercise II *}

   386 

   387 text {*

   388   Again remove the sorries in the proof below and fill in the proper

   389   justifications. 

   390 *}

   391 

   392 lemma bs1_trans2:

   393   assumes a: "t1 \<longrightarrow>b* t2"

   394   and     b: "t2 \<longrightarrow>b* t3"

   395   shows "t1 \<longrightarrow>b* t3"

   396 using a b

   397 proof (induct)

   398   case (bs1_refl t1)

   399   have a: "t1 \<longrightarrow>b* t3" by fact

   400   show "t1 \<longrightarrow>b* t3" using a by blast

   401 next

   402   case (bs1_trans t1 t2 t3')

   403   have ih1: "t1 \<longrightarrow>b t2" by fact

   404   have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact

   405   have asm: "t3' \<longrightarrow>b* t3" by fact

   406   have a: "t2 \<longrightarrow>b* t3" using ih2 asm by blast

   407   show "t1 \<longrightarrow>b* t3" using ih1 a beta_star1.bs1_trans by blast

   408 qed

   409   

   410 lemma

   411   assumes a: "t1 \<longrightarrow>b** t2"

   412   shows "t1 \<longrightarrow>b* t2"

   413 using a

   414 proof (induct)

   415   case (bs2_refl t)

   416   show "t \<longrightarrow>b* t" using bs1_refl by blast

   417 next

   418   case (bs2_step t1 t2)

   419   have ih: "t1 \<longrightarrow>b t2" by fact

   420   have a: "t2 \<longrightarrow>b* t2" using bs1_refl by blast

   421   show "t1 \<longrightarrow>b* t2" using ih a bs1_trans by blast

   422 next

   423   case (bs2_trans t1 t2 t3)

   424   have ih1: "t1 \<longrightarrow>b* t2" by fact

   425   have ih2: "t2 \<longrightarrow>b* t3" by fact

   426   show "t1 \<longrightarrow>b* t3" using ih1 ih2 bs1_trans2 by blast  

   427 qed

   428   

   429 text {* 

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

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

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

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

   434 *}

   435 

   436 lemma 

   437   assumes a: "t1 \<longrightarrow>b* t2"

   438   and     b: "t2 \<longrightarrow>b* t3"

   439   shows "t1 \<longrightarrow>b* t3"

   440 using a b

   441 proof (induct)

   442   case (bs1_refl t1)

   443   show "t1 \<longrightarrow>b* t3" by fact

   444 next

   445   case (bs1_trans t1 t2 t3')

   446   have ih1: "t1 \<longrightarrow>b t2" by fact

   447   have ih2: "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact

   448   have "t3' \<longrightarrow>b* t3" by fact

   449   then have "t2 \<longrightarrow>b* t3" using ih2 by blast

   450   then show "t1 \<longrightarrow>b* t3" using ih1 beta_star1.bs1_trans by blast

   451 qed

   452 

   453 text {* 

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

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

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

   457   "moreover"-chaining mechanism:

   458 

   459    have "statement_1" \<dots>

   460    moreover

   461    have "statement_2" \<dots>

   462    \<dots>

   463    moreover

   464    have "statement_n" \<dots>

   465    ultimately have "statement" \<dots>

   466 

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

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

   469 *}

   470 

   471 lemma 

   472   assumes a: "t1 \<longrightarrow>b* t2"

   473   and     b: "t2 \<longrightarrow>b* t3"

   474   shows "t1 \<longrightarrow>b* t3"

   475 using a b

   476 proof (induct)

   477   case (bs1_refl t1)

   478   show "t1 \<longrightarrow>b* t3" by fact

   479 next

   480   case (bs1_trans t1 t2 t3')

   481   have "t3' \<longrightarrow>b* t3 \<Longrightarrow> t2 \<longrightarrow>b* t3" by fact

   482   moreover

   483   have "t3' \<longrightarrow>b* t3" by fact

   484   ultimately 

   485   have "t2 \<longrightarrow>b* t3" by blast

   486   moreover 

   487   have "t1 \<longrightarrow>b t2" by fact

   488   ultimately show "t1 \<longrightarrow>b* t3" using beta_star1.bs1_trans by blast

   489 qed

   490 

   491 

   492 text {* 

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

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

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

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

   497 *}

   498 

   499 lemma

   500   assumes a: "t1 \<longrightarrow>b* t2" 

   501   shows "t1 \<longrightarrow>b** t2"

   502   using a

   503 by (induct) (auto intro: beta_star2.intros)

   504 

   505 lemma 

   506   assumes a: "t1 \<longrightarrow>b* t2"

   507   and     b: "t2 \<longrightarrow>b* t3"

   508   shows "t1 \<longrightarrow>b* t3"

   509 using a b

   510 by (induct) (auto intro: beta_star1.intros)

   511 

   512 lemma

   513   assumes a: "t1 \<longrightarrow>b** t2"

   514   shows "t1 \<longrightarrow>b* t2"

   515 using a

   516 by (induct) (auto intro: bs1_trans2 beta_star1.intros)

   517 

   518 inductive

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

   520 where

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

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

   523 

   524 declare eval.intros[intro]

   525 

   526 text {* 

   527   Values are also defined using inductive. In our case values

   528   are just lambda-abstractions. *}

   529 

   530 inductive

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

   532 where

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

   534 

   535 

   536 section {* Datatypes: Evaluation Contexts *}

   537 

   538 text {*

   539 

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

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

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

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

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

   545 *}

   546 

   547 datatype ctx = 

   548     Hole ("\<box>")  

   549   | CAppL "ctx" "lam"

   550   | CAppR "lam" "ctx"

   551 

   552 text {* Now Isabelle knows about: *}

   553 

   554 typ ctx

   555 term "\<box>"

   556 term "CAppL"

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

   558 

   559 text {* 

   560 

   561   1.) MINI EXERCISE

   562   -----------------

   563 

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

   565 

   566 *}

   567 

   568 type_synonym ctxs = "ctx list"

   569 

   570 inductive

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

   572 where

   573   m1[intro]: "<App t1 t2,Es> \<mapsto> <t1,(CAppL \<box> t2) # Es>"

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

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

   576 

   577 

   578 text {*

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

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

   581 

   582 inductive 

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

   584 where

   585   ms1[intro]: "<t,Es> \<mapsto>* <t,Es>"

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

   587 

   588 lemma 

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

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

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

   592 using a b

   593 proof(induct)

   594   case (ms1 e1 Es1)

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

   596   show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry

   597 next

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

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

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

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

   602   

   603   show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry

   604 qed

   605 

   606 text {* 

   607   Just like gotos in the Basic programming language, labels can reduce 

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

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

   610   the next have-statement. In the proof below this has been used

   611   in order to get rid of the labels c and d1. 

   612 *}

   613 

   614 lemma 

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

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

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

   618 using a b

   619 proof(induct)

   620   case (ms1 e1 Es1)

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

   622 next

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

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

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

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

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

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

   629 qed

   630 

   631 lemma 

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

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

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

   635 using a b

   636 proof(induct)

   637   case (ms1 e1 Es1)

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

   639 next

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

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

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

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

   644   moreover

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

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

   647 qed

   648 

   649 

   650 lemma ms3[intro]:

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

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

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

   654 using a b by (induct) (auto)

   655 

   656 lemma eval_to_val:

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

   658   shows "val t'"

   659 using a by (induct) (auto)

   660 

   661 

   662 theorem 

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

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

   665 using a 

   666 proof (induct)

   667   case (e_Lam x t)

   668   (* no assumptions *)

   669   show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" sorry

   670 next

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

   672   (* all assumptions in this case *)

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

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

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

   676   have ih2: "<t2, []> \<mapsto>* <v', []>" by fact

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

   678   have ih3: "<t[x::=v'], []> \<mapsto>* <v, []>" by fact

   679   (* your details *)

   680   show "<App t1 t2, []> \<mapsto>* <v, []>" sorry

   681 qed

   682 

   683 text {* 

   684   Again the automatic tools in Isabelle can discharge automatically 

   685   of the routine work in these proofs. We can write: *}

   686 

   687 theorem eval_implies_machines_ctx:

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

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

   690 using a

   691 by (induct arbitrary: Es)

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

   693 

   694 corollary eval_implies_machines:

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

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

   697 using a eval_implies_machines_ctx by simp

   698 

   699 

   700 nominal_datatype ty =

   701   tVar "string"

   702 | tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100)

   703 

   704 

   705 text {* 

   706   Having defined them as nominal datatypes gives us additional

   707   definitions and theorems that come with types (see below).

   708   *}

   709 

   710 text {* 

   711   We next define the type of typing contexts, a predicate that

   712   defines valid contexts (i.e. lists that contain only unique

   713   variables) and the typing judgement.

   714 

   715 *}

   716 

   717 type_synonym ty_ctx = "(name \<times> ty) list"

   718 

   719 inductive

   720   valid :: "ty_ctx \<Rightarrow> bool"

   721 where

   722   v1[intro]: "valid []"

   723 | v2[intro]: "\<lbrakk>valid \<Gamma>; atom x \<sharp> \<Gamma>\<rbrakk>\<Longrightarrow> valid ((x, T) # \<Gamma>)"

   724 

   725 inductive

   726   typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) 

   727 where

   728   t_Var[intro]:  "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

   729 | t_App[intro]:  "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

   730 | t_Lam[intro]:  "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1 \<rightarrow> T2"

   731 

   732 

   733 text {*

   734   The predicate x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by Nominal Isabelle.

   735   Freshness is defined for lambda-terms, products, lists etc. For example

   736   we have:

   737   *}

   738 

   739 lemma

   740   fixes x::"name"

   741   shows "atom x \<sharp> Lam [x].t"

   742   and   "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2"

   743   and   "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y" 

   744   and   "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)"

   745   and   "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)"

   746   and   "atom x \<sharp> y \<Longrightarrow> x \<noteq> y"

   747   by (simp_all add: lam.fresh fresh_append fresh_at_base) 

   748 

   749 text {* We can also prove that every variable is fresh for a type *}

   750 

   751 lemma ty_fresh:

   752   fixes x::"name"

   753   and   T::"ty"

   754   shows "atom x \<sharp> T"

   755 by (induct T rule: ty.induct)

   756    (simp_all add: ty.fresh pure_fresh)

   757 

   758 text {* 

   759   In order to state the weakening lemma in a convenient form, we overload

   760   the subset-notation and define the abbreviation below. Abbreviations behave

   761   like definitions, except that they are always automatically folded and

   762   unfolded.

   763 *}

   764 

   765 abbreviation

   766   "sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60) 

   767 where

   768   "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"

   769 

   770 text {***************************************************************** 

   771 

   772   4.) Exercise

   773   ------------

   774 

   775   Fill in the details and give a proof of the weakening lemma. 

   776 

   777 *}

   778 

   779 lemma 

   780   assumes a: "\<Gamma>1 \<turnstile> t : T"

   781   and     b: "valid \<Gamma>2" 

   782   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

   783   shows "\<Gamma>2 \<turnstile> t : T"

   784 using a b c

   785 proof (induct arbitrary: \<Gamma>2)

   786   case (t_Var \<Gamma>1 x T)

   787   have a1: "valid \<Gamma>1" by fact

   788   have a2: "(x, T) \<in> set \<Gamma>1" by fact

   789   have a3: "valid \<Gamma>2" by fact

   790   have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   791 

   792   show "\<Gamma>2 \<turnstile> Var x : T" sorry

   793 next

   794   case (t_Lam x \<Gamma>1 T1 t T2) 

   795   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

   796   have a0: "atom x \<sharp> \<Gamma>1" by fact

   797   have a1: "valid \<Gamma>2" by fact

   798   have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   799 

   800   show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry

   801 qed (auto)

   802 

   803 

   804 text {* 

   805   Despite the frequent claim that the weakening lemma is trivial,

   806   routine or obvious, the proof in the lambda-case does not go 

   807   smoothly through. Painful variable renamings seem to be necessary. 

   808   But the proof using renamings is horribly complicated. It is really 

   809   interesting whether people who claim this proof is  trivial, routine 

   810   or obvious had this proof in mind. 

   811 

   812   BTW: The following two commands help already with showing that validity 

   813   and typing are invariant under variable (permutative) renamings. 

   814 *}

   815 

   816 equivariance valid

   817 equivariance typing

   818 

   819 lemma not_to_be_tried_at_home_weakening: 

   820   assumes a: "\<Gamma>1 \<turnstile> t : T"

   821   and     b: "valid \<Gamma>2" 

   822   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

   823   shows "\<Gamma>2 \<turnstile> t : T"

   824 using a b c

   825 proof (induct arbitrary: \<Gamma>2)

   826   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)

   827   have fc0: "atom x \<sharp> \<Gamma>1" by fact

   828   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

   829   obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh)

   830   have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)

   831     by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def)

   832   moreover

   833   have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)

   834   proof - 

   835     (* 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)) *)

   836     have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" 

   837     proof -

   838       have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   839       then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1

   840 	by (perm_simp) (simp add: flip_fresh_fresh)

   841       then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE)

   842     qed

   843     moreover 

   844     have "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" 

   845     proof -

   846       have "valid \<Gamma>2" by fact

   847       then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1

   848 	by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)	

   849     qed

   850     (* these two facts give us by induction hypothesis the following *)

   851     ultimately have "(x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2" using ih by simp 

   852     (* we now apply renamings to get to our goal *)

   853     then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)

   854     then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1

   855       by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)

   856     then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto

   857   qed

   858   ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp

   859 qed (auto) (* var and app cases *)

   860 

   861 

   862 text {* 

   863   The remedy to the complicated proof of the weakening proof

   864   shown above is to use a stronger induction principle that

   865   has the usual variable convention already build in. The

   866   following command derives this induction principle for us.

   867   (We shall explain what happens here later.)

   868 

   869 *}

   870 

   871 nominal_inductive typing

   872   avoids t_Lam: "x"

   873   unfolding fresh_star_def

   874   by (simp_all add: fresh_Pair lam.fresh ty_fresh)

   875 

   876 text {* Compare the two induction principles *}

   877 thm typing.induct

   878 thm typing.strong_induct

   879 

   880 text {* 

   881   We can use the stronger induction principle by replacing

   882   the line

   883 

   884   proof (induct arbitrary: \<Gamma>2)

   885 

   886   with 

   887   

   888   proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)

   889 

   890   Try now the proof.

   891 

   892 *}

   893   

   894 

   895 lemma weakening: 

   896   assumes a: "\<Gamma>1 \<turnstile> t : T"

   897   and     b: "valid \<Gamma>2" 

   898   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

   899   shows "\<Gamma>2 \<turnstile> t : T"

   900 using a b c

   901 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)

   902   case (t_Var \<Gamma>1 x T)  (* variable case *)

   903   have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact 

   904   moreover  

   905   have "valid \<Gamma>2" by fact 

   906   moreover 

   907   have "(x, T)\<in> set \<Gamma>1" by fact

   908   ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto

   909 next

   910   case (t_Lam x \<Gamma>1 T1 t T2) 

   911   have vc: "atom x \<sharp> \<Gamma>2" by fact   (* additional fact *)

   912   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

   913   have a0: "atom x \<sharp> \<Gamma>1" by fact

   914   have a1: "valid \<Gamma>2" by fact

   915   have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   916 

   917   show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry

   918 qed (auto) (* app case *)

   919 

   920 

   921 text {***************************************************************** 

   922 

   923   Function Definitions: Filling a Lambda-Term into a Context

   924   ----------------------------------------------------------

   925 

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

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

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

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

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

   931 

   932 *}

   933 

   934 fun

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

   936 where

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

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

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

   940 

   941 text {* 

   942   After this definition Isabelle will be able to simplify

   943   statements like: *}

   944 

   945 lemma 

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

   947   by simp

   948 

   949 

   950 fun 

   951  ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<cdot> _" [101,100] 100)

   952 where

   953   "\<box> \<cdot> E' = E'"

   954 | "(CAppL E t') \<cdot> E' = CAppL (E \<cdot> E') t'"

   955 | "(CAppR t' E) \<cdot> E' = CAppR t' (E \<cdot> E')"

   956 

   957 fun

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

   959 where

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

   961   | "(E # Es)\<down> = (Es\<down>) \<cdot> E"

   962 

   963 text {*  

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

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

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

   967   

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

   969   interpreted as Es1 \<cdot> (Es2 \<cdot> Es3).

   970 *}

   971 

   972 text {******************************************************************

   973   

   974   Structural Inductions over Contexts

   975   ------------------------------------

   976 

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

   978   Another important induction principle is structural inductions for 

   979   datatypes. To illustrate structural inductions we prove some facts

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

   981 

   982 *}

   983 

   984 text {******************************************************************

   985 

   986   5.) EXERCISE

   987   ------------

   988 

   989   Complete the proof and remove the sorries.

   990 

   991 *}

   992 

   993 lemma ctx_compose:

   994   shows "(E1 \<cdot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"

   995 proof (induct E1)

   996   case Hole

   997   show "\<box> \<cdot> E2\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry

   998 next

   999   case (CAppL E1 t')

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

  1001   show "((CAppL E1 t') \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry

  1002 next

  1003   case (CAppR t' E1)

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

  1005   show "((CAppR t' E1) \<cdot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry

  1006 qed

  1007 

  1008 lemma neut_hole:

  1009   shows "E \<cdot> \<box> = E"

  1010 by (induct E) (simp_all)

  1011 

  1012 lemma circ_assoc:

  1013   fixes E1 E2 E3::"ctx"

  1014   shows "(E1 \<cdot> E2) \<cdot> E3 = E1 \<cdot> (E2 \<cdot> E3)"

  1015 by (induct E1) (simp_all)

  1016 

  1017 lemma

  1018   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"

  1019 proof (induct Es1)

  1020   case Nil

  1021   show "([] @ Es2)\<down> = Es2\<down> \<cdot> []\<down>" sorry

  1022 next

  1023   case (Cons E Es1)

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

  1025 

  1026   show "((E # Es1) @ Es2)\<down> = Es2\<down> \<cdot> (E # Es1)\<down>" sorry

  1027 qed

  1028 

  1029 

  1030 text {* 

  1031   The last proof involves several steps of equational reasoning.

  1032   Isar provides some convenient means to express such equational 

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

  1034   construction. *}

  1035 

  1036 lemma 

  1037   shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<cdot> (Es1\<down>)"

  1038 proof (induct Es1)

  1039   case Nil

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

  1041 next

  1042   case (Cons E Es1)

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

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

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

  1046   also have "\<dots> = Es2\<down> \<cdot> (Es1\<down> \<cdot> E)" using circ_assoc by simp

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

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

  1049 qed

  1050 

  1051 text {******************************************************************

  1052   

  1053   Formalising Barendregt's Proof of the Substitution Lemma

  1054   --------------------------------------------------------

  1055 

  1056   Barendregt's proof needs in the variable case a case distinction.

  1057   One way to do this in Isar is to use blocks. A block is some sequent

  1058   or reasoning steps enclosed in curly braces

  1059 

  1060   { \<dots>

  1061 

  1062     have "statement"

  1063   }

  1064 

  1065   Such a block can contain local assumptions like

  1066 

  1067   { assume "A"

  1068     assume "B"

  1069     \<dots>

  1070     have "C" by \<dots>

  1071   }

  1072 

  1073   Where "C" is the last have-statement in this block. The behaviour 

  1074   of such a block to the 'outside' is the implication

  1075 

  1076    \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C" 

  1077 

  1078   Now if we want to prove a property "smth" using the case-distinctions

  1079   P\<^isub>1, P\<^isub>2 and P\<^isub>3 then we can use the following reasoning:

  1080 

  1081     { assume "P\<^isub>1"

  1082       \<dots>

  1083       have "smth"

  1084     }

  1085     moreover

  1086     { assume "P\<^isub>2"

  1087       \<dots>

  1088       have "smth"

  1089     }

  1090     moreover

  1091     { assume "P\<^isub>3"

  1092       \<dots>

  1093       have "smth"

  1094     }

  1095     ultimately have "smth" by blast

  1096 

  1097   The blocks establish the implications

  1098 

  1099     P\<^isub>1 \<Longrightarrow> smth

  1100     P\<^isub>2 \<Longrightarrow> smth

  1101     P\<^isub>3 \<Longrightarrow> smth

  1102 

  1103   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

  1104   true, then we have 'ultimately' established the property "smth" 

  1105   

  1106 *}

  1107 

  1108 text {******************************************************************

  1109   

  1110   7.) Exercise

  1111   ------------

  1112 

  1113   Fill in the cases 1.2 and 1.3 and the equational reasoning 

  1114   in the lambda-case.

  1115 *}

  1116 

  1117 lemma forget:

  1118   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

  1119 apply(nominal_induct t avoiding: x s rule: lam.strong_induct)

  1120 apply(auto simp add: lam.fresh fresh_at_base)

  1121 done

  1122 

  1123 lemma fresh_fact:

  1124   fixes z::"name"

  1125   assumes a: "atom z \<sharp> s"

  1126   and b: "z = y \<or> atom z \<sharp> t"

  1127   shows "atom z \<sharp> t[y ::= s]"

  1128 using a b

  1129 apply (nominal_induct t avoiding: z y s rule: lam.strong_induct)

  1130 apply (auto simp add: lam.fresh fresh_at_base)

  1131 done

  1132 

  1133 thm forget

  1134 thm fresh_fact

  1135