1 header {* 

     2 

     3   Nominal Isabelle Tutorial at POPL'11

     4   ====================================

     5 

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

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

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

     9 

    10 

    11   The jEdit Interface

    12   -------------------

    13 

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

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

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

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

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

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

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

    21 

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

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

    24   Cmd is Ctrl on the Mac)

    25 

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

    27 

    28      isabelle jedit -l HOL-Nominal2

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

    30 

    31 

    32   Symbols

    33   ------- 

    34 

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

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

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

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

    39   

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

    41   For example 

    42 

    43       short-cut  symbol

    44 

    45           =>      \<Rightarrow>

    46           ==>     \<Longrightarrow>

    47           -->     \<longrightarrow>

    48           !       \<forall>        

    49           ?       \<exists>

    50           /\      \<and>

    51           \/      \<or>

    52           ~       \<not>

    53           ~=      \<noteq>

    54           :       \<in>

    55           ~:      \<notin>

    56 

    57   For nominal the following two symbols have a special meaning

    58 

    59         \<sharp>    sharp     (freshness)

    60         \<bullet>    bullet    (permutation application)

    61 *}

    62 

    63 

    64 theory Tutorial1

    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" sorry

   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)" sorry

   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'" sorry

   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   

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

   466 next

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

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

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

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

   471 

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

   473 qed

   474 

   475 text {* 

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

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

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

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

   480 *}

   481  

   482 lemma 

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

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

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

   486 using a b

   487 proof(induct)

   488   case (ms1 e1 Es1)

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

   490 next

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

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

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

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

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

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

   497 qed

   498 

   499 text {* 

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

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

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

   503   "moreover"-chaining mechanism:

   504 

   505    have "statement_1" \<dots>

   506    moreover

   507    have "statement_2" \<dots>

   508    \<dots>

   509    moreover

   510    have "statement_n" \<dots>

   511    ultimately have "statement" \<dots>

   512 

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

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

   515 *}

   516 

   517 lemma 

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

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

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

   521 using a b

   522 proof(induct)

   523   case (ms1 e1 Es1)

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

   525 next

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

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

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

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

   530   moreover

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

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

   533 qed

   534 

   535 

   536 text {* 

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

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

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

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

   541 *}

   542 

   543 lemma 

   544   assumes a: "val t"

   545   shows "t \<Down> t"

   546 using a by (induct) (auto)

   547 

   548 lemma 

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

   550   shows "val t'"

   551 using a by (induct) (auto)

   552 

   553 lemma

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

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

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

   557 using a b by (induct) (auto)

   558 

   559 

   560 section {* EXERCISE 4 *}

   561 

   562 text {*

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

   564   relation. Therefore we like to prove the following:

   565 *}

   566 

   567 theorem 

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

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

   570 using a 

   571 proof (induct)

   572   case (e_Lam x t) 

   573   -- {* no assumptions *}

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

   575 next

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

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

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

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

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

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

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

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

   584 

   585   -- {* your reasoning *}

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

   587 qed

   588 

   589 

   590 text {* 

   591   Again the automatic tools in Isabelle can discharge automatically 

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

   593 *}

   594 

   595 theorem eval_implies_machines_ctx:

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

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

   598 using a

   599 by (induct arbitrary: Es)

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

   601 

   602 corollary eval_implies_machines:

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

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

   605 using a eval_implies_machines_ctx by simp

   606 

   607 

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

   609  

   610 text {*

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

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

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

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

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

   616 *}

   617 

   618 fun

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

   620 where

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

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

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

   624 

   625 

   626 text {* 

   627   After this definition Isabelle will be able to simplify

   628   statements like: 

   629 *}

   630 

   631 lemma 

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

   633   by simp

   634 

   635 fun 

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

   637 where

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

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

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

   641 

   642 fun

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

   644 where

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

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

   647 

   648 text {*  

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

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

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

   652   

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

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

   655 *}

   656 

   657 section {* Structural Inductions over Contexts *}

   658  

   659 text {*

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

   661   Another important induction principle is structural inductions for 

   662   datatypes. To illustrate structural inductions we prove some facts

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

   664 *}

   665 

   666 subsection {* EXERCISE 5 *}

   667 

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

   669 

   670 lemma ctx_compose:

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

   672 proof (induct E1)

   673   case Hole

   674   show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry

   675 next

   676   case (CAppL E1 t')

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

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

   679 next

   680   case (CAppR t' E1)

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

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

   683 qed

   684 

   685 

   686 subsection {* EXERCISE 6 *}

   687 

   688 text {*

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

   690   use of the following two properties.    

   691 *}

   692 

   693 lemma neut_hole:

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

   695 by (induct E) (simp_all)

   696 

   697 lemma compose_assoc:  

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

   699 by (induct E1) (simp_all)

   700 

   701 lemma

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

   703 proof (induct Es1)

   704   case Nil

   705   show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" sorry

   706 next

   707   case (Cons E Es1)

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

   709 

   710   show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry

   711 qed

   712 

   713 text {* 

   714   The last proof involves several steps of equational reasoning.

   715   Isar provides some convenient means to express such equational 

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

   717   construction. 

   718 *}

   719 

   720 lemma 

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

   722 proof (induct Es1)

   723   case Nil

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

   725 next

   726   case (Cons E Es1)

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

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

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

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

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

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

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

   734 qed

   735 

   736 

   737 end  

   738