# HG changeset patch # User Cezary Kaliszyk # Date 1295891504 -32400 # Node ID 8ae1c2e6369eeb08827eb78a4d14468c6fde0b7f # Parent 67451725fb410cbdd44c8126b5abff5e8b312df1# Parent b4bad45dbc0fef65c513df6404e67149fa3d28de merge diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Lambda.thy --- a/Tutorial/Lambda.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Lambda.thy Tue Jan 25 02:51:44 2011 +0900 @@ -105,18 +105,13 @@ shows "(p \ t[x ::= s]) = (p \ t)[(p \ x) ::= (p \ s)]" by (induct t x s rule: subst.induct) (simp_all) - -subsection {* Single-Step Beta-Reduction *} - -inductive - beta :: "lam \ lam \ bool" (" _ \b _" [80,80] 80) -where - b1[intro]: "t1 \b t2 \ App t1 s \b App t2 s" -| b2[intro]: "s1 \b s2 \ App t s1 \b App t s2" -| b3[intro]: "t1 \b t2 \ Lam [x]. t1 \b Lam [x]. t2" -| b4[intro]: "App (Lam [x]. t) s \b t[x ::= s]" - - +lemma fresh_fact: + assumes a: "atom z \ s" + and b: "z = y \ atom z \ t" + shows "atom z \ t[y ::= s]" +using a b +by (nominal_induct t avoiding: z y s rule: lam.strong_induct) + (auto simp add: lam.fresh fresh_at_base) end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial1.thy --- a/Tutorial/Tutorial1.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Tutorial1.thy Tue Jan 25 02:51:44 2011 +0900 @@ -1,4 +1,3 @@ - header {* Nominal Isabelle Tutorial at POPL'11 @@ -183,7 +182,7 @@ text {* In this section we want to define inductively the evaluation - relation for lambda terms. + relation and for cbv-reduction relation. Inductive definitions in Isabelle start with the keyword "inductive" and a predicate name. One can optionally provide a type for the predicate. @@ -208,15 +207,13 @@ *} inductive - eval :: "lam \ lam \ bool" ("_ \ _" [60, 60] 60) + eval :: "lam \ lam \ bool" (infixr "\" 60) where e_Lam[intro]: "Lam [x].t \ Lam [x].t" | e_App[intro]: "\t1 \ Lam [x].t; t2 \ v'; t[x::=v'] \ v\ \ App t1 t2 \ v" - text {* - Values are also defined using inductive. In our case values - are just lambda-abstractions. + Values and cbv are also defined using inductive. *} inductive @@ -224,7 +221,6 @@ where v_Lam[intro]: "val (Lam [x].t)" - section {* Theorems *} text {* @@ -362,6 +358,7 @@ Two very simple example proofs are as follows. *} +subsection {* EXERCISE 1 *} lemma eval_val: assumes a: "val t" @@ -372,7 +369,11 @@ show "Lam [x]. t \ Lam [x]. t" sorry qed -lemma eavl_to_val: +subsection {* EXERCISE 2 *} + +text {* Fill the gaps in the proof below. *} + +lemma eval_to_val: assumes a: "t \ t'" shows "val t'" using a @@ -381,16 +382,96 @@ show "val (Lam [x].t)" sorry next case (e_App t1 x t t2 v v') + -- {* all assumptions in this case *} have "t1 \ Lam [x].t" by fact have ih1: "val (Lam [x]. t)" by fact have "t2 \ v" by fact have ih2: "val v" by fact have "t [x ::= v] \ v'" by fact have ih3: "val v'" by fact + show "val v'" sorry qed + + +section {* Datatypes: Evaluation Contexts*} + +text {* + Datatypes can be defined in Isabelle as follows: we have to provide the name + of the datatype and a list its type-constructors. Each type-constructor needs + to have the information about the types of its arguments, and optionally + can also contain some information about pretty syntax. For example, we like + to write "\" for holes. +*} - +datatype ctx = + Hole ("\") + | CAppL "ctx" "lam" + | CAppR "lam" "ctx" + +text {* Now Isabelle knows about: *} + +typ ctx +term "\" +term "CAppL" +term "CAppL \ (Var x)" + +subsection {* MINI EXERCISE *} + +text {* + Try and see what happens if you apply a Hole to a Hole? +*} + + +section {* Machines for Evaluation *} + +type_synonym ctxs = "ctx list" + +inductive + machine :: "lam \ ctxs \lam \ ctxs \ bool" ("<_,_> \ <_,_>" [60, 60, 60, 60] 60) +where + m1: " \ t2) # Es>" +| m2: "val v \ t2) # Es> \ ) # Es>" +| m3: "val v \ ) # Es> \ " + +text {* + Since the machine defined above only performs a single reduction, + we need to define the transitive closure of this machine. *} + +inductive + machines :: "lam \ ctxs \ lam \ ctxs \ bool" ("<_,_> \* <_,_>" [60, 60, 60, 60] 60) +where + ms1: " \* " +| ms2: "\ \ ; \* \ \ \* " + +declare machine.intros[intro] machines.intros[intro] + +section {* EXERCISE 3 *} + +text {* + We need to show that the machines-relation is transitive. + Fill in the gaps below. +*} + +lemma ms3[intro]: + assumes a: " \* " + and b: " \* " + shows " \* " +using a b +proof(induct) + case (ms1 e1 Es1) + have c: " \* " by fact + + show " \* " sorry +next + case (ms2 e1 Es1 e2 Es2 e2' Es2') + have ih: " \* \ \* " by fact + have d1: " \* " by fact + have d2: " \ " by fact + + show " \* " sorry +qed + text {* Just like gotos in the Basic programming language, labels often reduce the readability of proofs. Therefore one can use in Isar the notation @@ -398,7 +479,22 @@ the next have-statement. This is used in the second case below. *} - +lemma + assumes a: " \* " + and b: " \* " + shows " \* " +using a b +proof(induct) + case (ms1 e1 Es1) + show " \* " by fact +next + case (ms2 e1 Es1 e2 Es2 e2' Es2') + have ih: " \* \ \* " by fact + have " \* " by fact + then have d3: " \* " using ih by simp + have d2: " \ " by fact + show " \* " using d2 d3 by auto +qed text {* The label ih2 cannot be got rid of in this way, because it is used @@ -418,108 +514,6 @@ "statement". With this we can simplify our proof further to: *} - -text {* - While automatic proof procedures in Isabelle are not able to prove statements - like "P = NP" assuming usual definitions for P and NP, they can automatically - discharge the lemmas we just proved. For this we only have to set up the induction - and auto will take care of the rest. This means we can write: -*} - - - - -section {* Datatypes: Evaluation Contexts *} - -text {* - - Datatypes can be defined in Isabelle as follows: we have to provide the name - of the datatype and list its type-constructors. Each type-constructor needs - to have the information about the types of its arguments, and optionally - can also contain some information about pretty syntax. For example, we like - to write "\" for holes. -*} - -datatype ctx = - Hole ("\") - | CAppL "ctx" "lam" - | CAppR "lam" "ctx" - -text {* Now Isabelle knows about: *} - -typ ctx -term "\" -term "CAppL" -term "CAppL \ (Var x)" - -subsection {* MINI EXERCISE *} - -text {* - Try and see what happens if you apply a Hole to a Hole? -*} - -type_synonym ctxs = "ctx list" - -inductive - machine :: "lam \ ctxs \lam \ ctxs \ bool" ("<_,_> \ <_,_>" [60, 60, 60, 60] 60) -where - m1[intro]: " \ t2) # Es>" -| m2[intro]: "val v \ t2) # Es> \ ) # Es>" -| m3[intro]: "val v \ ) # Es> \ " - - -text {* - Since the machine defined above only performs a single reduction, - we need to define the transitive closure of this machine. *} - -inductive - machines :: "lam \ ctxs \ lam \ ctxs \ bool" ("<_,_> \* <_,_>" [60, 60, 60, 60] 60) -where - ms1[intro]: " \* " -| ms2[intro]: "\ \ ; \* \ \ \* " - -lemma - assumes a: " \* " - and b: " \* " - shows " \* " -using a b -proof(induct) - case (ms1 e1 Es1) - have c: " \* " by fact - then show " \* " by simp -next - case (ms2 e1 Es1 e2 Es2 e2' Es2') - have ih: " \* \ \* " by fact - have d1: " \* " by fact - have d2: " \ " by fact - show " \* " using d1 d2 ih by blast -qed - -text {* - Just like gotos in the Basic programming language, labels can reduce - the readability of proofs. Therefore one can use in Isar the notation - "then have" in order to feed a have-statement to the proof of - the next have-statement. In the proof below this has been used - in order to get rid of the labels c and d1. -*} - -lemma - assumes a: " \* " - and b: " \* " - shows " \* " -using a b -proof(induct) - case (ms1 e1 Es1) - show " \* " by fact -next - case (ms2 e1 Es1 e2 Es2 e2' Es2') - have ih: " \* \ \* " by fact - have " \* " by fact - then have d3: " \* " using ih by simp - have d2: " \ " by fact - show " \* " using d2 d3 by auto -qed - lemma assumes a: " \* " and b: " \* " @@ -539,16 +533,36 @@ qed -lemma ms3[intro]: +text {* + While automatic proof procedures in Isabelle are not able to prove statements + like "P = NP" assuming usual definitions for P and NP, they can automatically + discharge the lemmas we just proved. For this we only have to set up the induction + and auto will take care of the rest. This means we can write: +*} + +lemma + assumes a: "val t" + shows "t \ t" +using a by (induct) (auto) + +lemma + assumes a: "t \ t'" + shows "val t'" +using a by (induct) (auto) + +lemma assumes a: " \* " and b: " \* " shows " \* " using a b by (induct) (auto) -lemma eval_to_val: (* fixme: done above *) - assumes a: "t \ t'" - shows "val t'" -using a by (induct) (auto) + +section {* EXERCISE 4 *} + +text {* + The point of the machine is that it simulates the evaluation + relation. Therefore we like to prove the following: +*} theorem assumes a: "t \ t'" @@ -567,10 +581,12 @@ have ih2: " \* " by fact have a3: "t[x::=v'] \ v" by fact have ih3: " \* " by fact + -- {* your reasoning *} show " \* " sorry qed + text {* Again the automatic tools in Isabelle can discharge automatically of the routine work in these proofs. We can write: @@ -589,7 +605,6 @@ using a eval_implies_machines_ctx by simp - section {* Function Definitions: Filling a Lambda-Term into a Context *} text {* @@ -607,6 +622,7 @@ | "(CAppL E t')\t\ = App (E\t\) t'" | "(CAppR t' E)\t\ = App t' (E\t\)" + text {* After this definition Isabelle will be able to simplify statements like: @@ -617,7 +633,7 @@ by simp fun - ctx_compose :: "ctx \ ctx \ ctx" ("_ \ _" [99,98] 99) + ctx_compose :: "ctx \ ctx \ ctx" (infixr "\" 99) where "\ \ E' = E'" | "(CAppL E t') \ E' = CAppL (E \ E') t'" @@ -666,11 +682,19 @@ show "((CAppR t' E1) \ E2)\t\ = (CAppR t' E1)\E2\t\\" sorry qed + +subsection {* EXERCISE 6 *} + +text {* + Remove the sorries in the ctx_append proof below. You can make + use of the following two properties. +*} + lemma neut_hole: shows "E \ \ = E" by (induct E) (simp_all) -lemma odot_assoc: (* fixme call compose *) +lemma compose_assoc: shows "(E1 \ E2) \ E3 = E1 \ (E2 \ E3)" by (induct E1) (simp_all) @@ -686,7 +710,6 @@ show "((E # Es1) @ Es2)\ = Es2\ \ (E # Es1)\" sorry qed - text {* The last proof involves several steps of equational reasoning. Isar provides some convenient means to express such equational @@ -694,7 +717,6 @@ construction. *} - lemma shows "(Es1 @ Es2)\ = (Es2\) \ (Es1\)" proof (induct Es1) @@ -703,14 +725,14 @@ next case (Cons E Es1) have ih: "(Es1 @ Es2)\ = Es2\ \ Es1\" by fact - have "((E # Es1) @ Es2)\ = (Es1 @ Es2)\ \ E" by simp + have "((E # Es1) @ Es2)\ = (E # (Es1 @ Es2))\" by simp + also have "\ = (Es1 @ Es2)\ \ E" by simp also have "\ = (Es2\ \ Es1\) \ E" using ih by simp - also have "\ = Es2\ \ (Es1\ \ E)" using odot_assoc by simp + also have "\ = Es2\ \ (Es1\ \ E)" using compose_assoc by simp also have "\ = Es2\ \ (E # Es1)\" by simp finally show "((E # Es1) @ Es2)\ = Es2\ \ (E # Es1)\" by simp qed - end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial1s.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tutorial/Tutorial1s.thy Tue Jan 25 02:51:44 2011 +0900 @@ -0,0 +1,752 @@ + +header {* + + Nominal Isabelle Tutorial at POPL'11 + ==================================== + + Nominal Isabelle is a definitional extension of Isabelle/HOL, which + means it does not add any new axioms to higher-order logic. It just + adds new definitions and an infrastructure for 'nominal resoning'. + + + The jEdit Interface + ------------------- + + The Isabelle theorem prover comes with an interface for jEdit. + Unlike many other theorem prover interfaces (e.g. ProofGeneral) where you + advance a 'checked' region in a proof script, this interface immediately + checks the whole buffer. The text you type is also immediately checked. + Malformed text or unfinished proofs are highlighted in red with a little + red 'stop' signal on the left-hand side. If you drag the 'red-box' cursor + over a line, the Output window gives further feedback. + + Note: If a section is not parsed correctly, the work-around is to cut it + out and paste it back into the text (cut-out: Ctrl + X; paste in: Ctrl + V; + Cmd is Ctrl on the Mac) + + Nominal Isabelle and jEdit can be started by typing on the command line + + isabelle jedit -l HOL-Nominal2 + isabelle jedit -l HOL-Nominal2 A.thy B.thy ... + + + Symbols + ------- + + Symbols can considerably improve the readability of your statements and proofs. + They can be input by just typing 'name-of-symbol' where 'name-of-symbol' is the + usual latex name of that symbol. A little window will then appear in which + you can select the symbol. With `Escape' you can ignore any suggestion. + + There are some handy short-cuts for frequently used symbols. + For example + + short-cut symbol + + => \ + ==> \ + --> \ + ! \ + ? \ + /\ \ + \/ \ + ~ \ + ~= \ + : \ + ~: \ + + For nominal the following two symbols have a special meaning + + \ sharp (freshness) + \ bullet (permutation application) +*} + +theory Tutorial1s +imports Lambda +begin + +section {* Theories *} + +text {* + All formal developments in Isabelle are part of a theory. A theory + needs to have a name and must import some pre-existing theory. The + imported theory will normally be Nominal2 (which provides many useful + concepts like set-theory, lists, nominal things etc). For the purpose + of this tutorial we import the theory Lambda.thy, which contains + already some useful definitions for (alpha-equated) lambda terms. +*} + + + +section {* Types *} + +text {* + Isabelle is based on simple types including some polymorphism. It also + includes overloading, which means that sometimes explicit type annotations + need to be given. + + - Base types include: nat, bool, string, lam (defined in the Lambda theory) + + - Type formers include: 'a list, ('a \ 'b), 'c set + + - Type variables are written like in ML with an apostrophe: 'a, 'b, \ + + Types known to Isabelle can be queried using the command "typ". +*} + +typ nat +typ bool +typ string +typ lam -- {* alpha-equated lambda terms defined in Lambda.thy *} +typ name -- {* type of (object) variables defined in Lambda.thy *} +typ "('a \ 'b)" -- {* pair type *} +typ "'c set" -- {* set type *} +typ "'a list" -- {* list type *} +typ "lam \ nat" -- {* type of functions from lambda terms to natural numbers *} + + +text {* Some malformed types - note the "stop" signal on the left margin *} + +(* +typ boolean -- {* undeclared type *} +typ set -- {* type argument missing *} +*) + + +section {* Terms *} + +text {* + Every term in Isabelle needs to be well-typed. However they can have + polymorphic type. Whether a term is accepted can be queried using + the command "term". +*} + +term c -- {* a variable of polymorphic type *} +term "1::nat" -- {* the constant 1 in natural numbers *} +term 1 -- {* the constant 1 with polymorphic type *} +term "{1, 2, 3::nat}" -- {* the set containing natural numbers 1, 2 and 3 *} +term "[1, 2, 3]" -- {* the list containing the polymorphic numbers 1, 2 and 3 *} +term "(True, ''c'')" -- {* a pair consisting of the boolean true and the string "c" *} +term "Suc 0" -- {* successor of 0, in other words 1::nat *} +term "Lam [x].Var x" -- {* a lambda-term *} +term "App t1 t2" -- {* another lambda-term *} +term "x::name" -- {* an (object) variable of type name *} +term "atom (x::name)" -- {* atom is an overloded function *} + +text {* + Lam [x].Var is the syntax we made up for lambda abstractions. If you + prefer, you can have your own syntax (but \ is already taken up for + Isabelle's functions). We also came up with the type "name" for variables. + You can introduce your own types of object variables using the + command atom_decl: +*} + +atom_decl ident +atom_decl ty_var + +text {* + Isabelle provides some useful colour feedback about its constants (black), + free variables (blue) and bound variables (green). +*} + +term "True" -- {* a constant defined somewhere...written in black *} +term "true" -- {* not recognised as a constant, therefore it is interpreted + as a free variable, written in blue *} +term "\x. P x" -- {* x is bound (green), P is free (blue) *} + + +text {* Formulae in Isabelle/HOL are terms of type bool *} + +term "True" +term "True \ False" +term "True \ B" +term "{1,2,3} = {3,2,1}" +term "\x. P x" +term "A \ B" +term "atom a \ t" -- {* freshness in Nominal *} + +text {* + When working with Isabelle, one deals with an object logic (that is HOL) and + Isabelle's rule framework (called Pure). Occasionally one has to pay attention + to this fact. But for the moment we ignore this completely. +*} + +term "A \ B" -- {* versus *} +term "A \ B" + +term "\x. P x" -- {* versus *} +term "\x. P x" + + +section {* Inductive Definitions: Evaluation Relation *} + +text {* + In this section we want to define inductively the evaluation + relation and for cbv-reduction relation. + + Inductive definitions in Isabelle start with the keyword "inductive" + and a predicate name. One can optionally provide a type for the predicate. + Clauses of the inductive predicate are introduced by "where" and more than + two clauses need to be separated by "|". One can also give a name to each + clause and indicate that it should be added to the hints database ("[intro]"). + A typical clause has some premises and a conclusion. This is written in + Isabelle as: + + "premise \ conclusion" + "premise1 \ premise2 \ \ premisen \ conclusion" + + There is an alternative way of writing the latter clause as + + "\premise1; premise2; \ premisen\ \ conclusion" + + If no premise is present, then one just writes + + "conclusion" + + Below we give two definitions for the transitive closure +*} + +inductive + eval :: "lam \ lam \ bool" ("_ \ _" [60, 60] 60) +where + e_Lam[intro]: "Lam [x].t \ Lam [x].t" +| e_App[intro]: "\t1 \ Lam [x].t; t2 \ v'; t[x::=v'] \ v\ \ App t1 t2 \ v" + +text {* + Values and cbv are also defined using inductive. +*} + +inductive + val :: "lam \ bool" +where + v_Lam[intro]: "val (Lam [x].t)" + +section {* Theorems *} + +text {* + A central concept in Isabelle is that of theorems. Isabelle's theorem + database can be queried using +*} + +thm e_App +thm e_Lam +thm conjI +thm conjunct1 + +text {* + Notice that theorems usually contain schematic variables (e.g. ?P, ?Q, \). + These schematic variables can be substituted with any term (of the right type + of course). + + When defining the predicates beta_star, Isabelle provides us automatically + with the following theorems that state how they can be introduced and what + constitutes an induction over them. +*} + +thm eval.intros +thm eval.induct + + +section {* Lemmas / Theorems / Corollaries *} + +text {* + Whether to use lemma, theorem or corollary makes no semantic difference + in Isabelle. + + A lemma starts with "lemma" and consists of a statement ("shows \") and + optionally a lemma name, some type-information for variables ("fixes \") + and some assumptions ("assumes \"). + + Lemmas also need to have a proof, but ignore this 'detail' for the moment. + + Examples are +*} + +lemma alpha_equ: + shows "Lam [x].Var x = Lam [y].Var y" + by (simp add: lam.eq_iff Abs1_eq_iff lam.fresh fresh_at_base) + +lemma Lam_freshness: + assumes a: "atom y \ Lam [x].t" + shows "(y = x) \ (y \ x \ atom y \ t)" + using a by (auto simp add: lam.fresh Abs_fresh_iff) + +lemma neutral_element: + fixes x::"nat" + shows "x + 0 = x" + by simp + +text {* + Note that in the last statement, the explicit type annotation is important + in order for Isabelle to be able to figure out what 0 stands for (e.g. a + natural number, a vector, etc) and which lemmas to apply. +*} + + +section {* Isar Proofs *} + +text {* + Isar is a language for writing formal proofs that can be understood by humans + and by Isabelle. An Isar proof can be thought of as a sequence of 'stepping stones' + that start with some assumptions and lead to the goal to be established. Every such + stepping stone is introduced by "have" followed by the statement of the stepping + stone. An exception is the goal to be proved, which need to be introduced with "show". + + have "statement" \ + show "goal_to_be_proved" \ + + Since proofs usually do not proceed in a linear fashion, labels can be given + to every stepping stone and they can be used later to explicitly refer to this + corresponding stepping stone ("using"). + + have label: "statement1" \ + \ + have "later_statement" using label \ + + Each stepping stone (or have-statement) needs to have a justification. The + simplest justification is "sorry" which admits any stepping stone, even false + ones (this is good during the development of proofs). + + have "outrageous_false_statement" sorry + + Assumptions can be 'justified' using "by fact". + + have "assumption" by fact + + Derived facts can be justified using + + have "statement" by simp -- simplification + have "statement" by auto -- proof search and simplification + have "statement" by blast -- only proof search + + If facts or lemmas are needed in order to justify a have-statement, then + one can feed these facts into the proof by using "using label \" or + "using theorem-name \". More than one label at a time is allowed. For + example + + have "statement" using label1 label2 theorem_name by auto + + Induction proofs in Isar are set up by indicating over which predicate(s) + the induction proceeds ("using a b") followed by the command "proof (induct)". + In this way, Isabelle uses defaults for which induction should be performed. + These defaults can be overridden by giving more information, like the variable + over which a structural induction should proceed, or a specific induction principle, + such as well-founded inductions. + + After the induction is set up, the proof proceeds by cases. In Isar these + cases can be given in any order. Most commonly they are started with "case" and the + name of the case, and optionally some legible names for the variables used inside + the case. + + In each "case", we need to establish a statement introduced by "show". Once + this has been done, the next case can be started using "next". When all cases + are completed, the proof can be finished using "qed". + + This means a typical induction proof has the following pattern + + proof (induct) + case \ + \ + show \ + next + case \ + \ + show \ + \ + qed + + Two very simple example proofs are as follows. +*} + +subsection {* EXERCISE 1 *} + +lemma eval_val: + assumes a: "val t" + shows "t \ t" +using a +proof (induct) + case (v_Lam x t) + show "Lam [x]. t \ Lam [x]. t" by auto +qed + +subsection {* EXERCISE 2 *} + +text {* Fill the gaps in the proof below. *} + +lemma eval_to_val: + assumes a: "t \ t'" + shows "val t'" +using a +proof (induct) + case (e_Lam x t) + show "val (Lam [x].t)" by auto +next + case (e_App t1 x t t2 v v') + -- {* all assumptions in this case *} + have "t1 \ Lam [x].t" by fact + have ih1: "val (Lam [x]. t)" by fact + have "t2 \ v" by fact + have ih2: "val v" by fact + have "t [x ::= v] \ v'" by fact + have ih3: "val v'" by fact + + show "val v'" using ih3 by auto +qed + + +section {* Datatypes: Evaluation Contexts*} + +text {* + Datatypes can be defined in Isabelle as follows: we have to provide the name + of the datatype and a list its type-constructors. Each type-constructor needs + to have the information about the types of its arguments, and optionally + can also contain some information about pretty syntax. For example, we like + to write "\" for holes. +*} + +datatype ctx = + Hole ("\") + | CAppL "ctx" "lam" + | CAppR "lam" "ctx" + +text {* Now Isabelle knows about: *} + +typ ctx +term "\" +term "CAppL" +term "CAppL \ (Var x)" + +subsection {* MINI EXERCISE *} + +text {* + Try and see what happens if you apply a Hole to a Hole? +*} + + +section {* Machines for Evaluation *} + +type_synonym ctxs = "ctx list" + +inductive + machine :: "lam \ ctxs \lam \ ctxs \ bool" ("<_,_> \ <_,_>" [60, 60, 60, 60] 60) +where + m1: " \ t2) # Es>" +| m2: "val v \ t2) # Es> \ ) # Es>" +| m3: "val v \ ) # Es> \ " + +text {* + Since the machine defined above only performs a single reduction, + we need to define the transitive closure of this machine. *} + +inductive + machines :: "lam \ ctxs \ lam \ ctxs \ bool" ("<_,_> \* <_,_>" [60, 60, 60, 60] 60) +where + ms1: " \* " +| ms2: "\ \ ; \* \ \ \* " + +declare machine.intros[intro] machines.intros[intro] + +section {* EXERCISE 3 *} + +text {* + We need to show that the machines-relation is transitive. + Fill in the gaps below. +*} + +lemma ms3[intro]: + assumes a: " \* " + and b: " \* " + shows " \* " +using a b +proof(induct) + case (ms1 e1 Es1) + have c: " \* " by fact + then show " \* " by simp +next + case (ms2 e1 Es1 e2 Es2 e2' Es2') + have ih: " \* \ \* " by fact + have d1: " \* " by fact + have d2: " \ " by fact + have d3: " \* " using ih d1 by auto + show " \* " using d2 d3 by auto +qed + +text {* + Just like gotos in the Basic programming language, labels often reduce + the readability of proofs. Therefore one can use in Isar the notation + "then have" in order to feed a have-statement to the proof of + the next have-statement. This is used in teh second case below. +*} + +lemma + assumes a: " \* " + and b: " \* " + shows " \* " +using a b +proof(induct) + case (ms1 e1 Es1) + show " \* " by fact +next + case (ms2 e1 Es1 e2 Es2 e2' Es2') + have ih: " \* \ \* " by fact + have " \* " by fact + then have d3: " \* " using ih by simp + have d2: " \ " by fact + show " \* " using d2 d3 by auto +qed + +text {* + The label ih2 cannot be got rid of in this way, because it is used + two lines below and we cannot rearange them. We can still avoid the + label by feeding a sequence of facts into a proof using the + "moreover"-chaining mechanism: + + have "statement_1" \ + moreover + have "statement_2" \ + \ + moreover + have "statement_n" \ + ultimately have "statement" \ + + In this chain, all "statement_i" can be used in the proof of the final + "statement". With this we can simplify our proof further to: +*} + +lemma + assumes a: " \* " + and b: " \* " + shows " \* " +using a b +proof(induct) + case (ms1 e1 Es1) + show " \* " by fact +next + case (ms2 e1 Es1 e2 Es2 e2' Es2') + have ih: " \* \ \* " by fact + have " \* " by fact + then have " \* " using ih by simp + moreover + have " \ " by fact + ultimately show " \* " by auto +qed + + +text {* + While automatic proof procedures in Isabelle are not able to prove statements + like "P = NP" assuming usual definitions for P and NP, they can automatically + discharge the lemmas we just proved. For this we only have to set up the induction + and auto will take care of the rest. This means we can write: +*} + +lemma + assumes a: "val t" + shows "t \ t" +using a by (induct) (auto) + +lemma + assumes a: "t \ t'" + shows "val t'" +using a by (induct) (auto) + +lemma + assumes a: " \* " + and b: " \* " + shows " \* " +using a b by (induct) (auto) + + +section {* EXERCISE 4 *} + +text {* + The point of the machine is that it simulates the evaluation + relation. Therefore we like to prove the following: +*} + +theorem + assumes a: "t \ t'" + shows " \* " +using a +proof (induct arbitrary: Es) + case (e_Lam x t Es) + -- {* no assumptions *} + show " \* " by auto +next + case (e_App t1 x t t2 v' v Es) + -- {* all assumptions in this case *} + have a1: "t1 \ Lam [x].t" by fact + have ih1: "\Es. \* " by fact + have a2: "t2 \ v'" by fact + have ih2: "\Es. \* " by fact + have a3: "t[x::=v'] \ v" by fact + have ih3: "\Es. \* " by fact + -- {* your reasoning *} + have " \* t2 # Es>" by auto + moreover + have " t2 # Es> \* t2 # Es>" using ih1 by auto + moreover + have " t2 # Es> \* # Es>" by auto + moreover + have " # Es> \* # Es>" + using ih2 by auto + moreover + have "val v'" using a2 eval_to_val by auto + then have " # Es> \* " by auto + moreover + have " \* " using ih3 by auto + ultimately show " \* " by blast +qed + + +text {* + Again the automatic tools in Isabelle can discharge automatically + of the routine work in these proofs. We can write: +*} + +theorem eval_implies_machines_ctx: + assumes a: "t \ t'" + shows " \* " +using a +by (induct arbitrary: Es) + (metis eval_to_val machine.intros ms1 ms2 ms3 v_Lam)+ + +corollary eval_implies_machines: + assumes a: "t \ t'" + shows " \* " +using a eval_implies_machines_ctx by simp + + +section {* Function Definitions: Filling a Lambda-Term into a Context *} + +text {* + Many functions over datatypes can be defined by recursion on the + structure. For this purpose, Isabelle provides "fun". To use it one needs + to give a name for the function, its type, optionally some pretty-syntax + and then some equations defining the function. Like in "inductive", + "fun" expects that more than one such equation is separated by "|". +*} + +fun + filling :: "ctx \ lam \ lam" ("_\_\" [100, 100] 100) +where + "\\t\ = t" +| "(CAppL E t')\t\ = App (E\t\) t'" +| "(CAppR t' E)\t\ = App t' (E\t\)" + + +text {* + After this definition Isabelle will be able to simplify + statements like: +*} + +lemma + shows "(CAppL \ (Var x))\Var y\ = App (Var y) (Var x)" + by simp + +fun + ctx_compose :: "ctx \ ctx \ ctx" (infixr "\" 99) +where + "\ \ E' = E'" +| "(CAppL E t') \ E' = CAppL (E \ E') t'" +| "(CAppR t' E) \ E' = CAppR t' (E \ E')" + +fun + ctx_composes :: "ctxs \ ctx" ("_\" [110] 110) +where + "[]\ = \" + | "(E # Es)\ = (Es\) \ E" + +text {* + Notice that we not just have given a pretty syntax for the functions, but + also some precedences. The numbers inside the [\] stand for the precedences + of the arguments; the one next to it the precedence of the whole term. + + This means we have to write (Es1 \ Es2) \ Es3 otherwise Es1 \ Es2 \ Es3 is + interpreted as Es1 \ (Es2 \ Es3). +*} + +section {* Structural Inductions over Contexts *} + +text {* + So far we have had a look at an induction over an inductive predicate. + Another important induction principle is structural inductions for + datatypes. To illustrate structural inductions we prove some facts + about context composition, some of which we will need later on. +*} + +subsection {* EXERCISE 5 *} + +text {* Complete the proof and remove the sorries. *} + +lemma + shows "(E1 \ E2)\t\ = E1\E2\t\\" +proof (induct E1) + case Hole + show "(\ \ E2)\t\ = \\E2\t\\" by simp +next + case (CAppL E1 t') + have ih: "(E1 \ E2)\t\ = E1\E2\t\\" by fact + show "((CAppL E1 t') \ E2)\t\ = (CAppL E1 t')\E2\t\\" using ih by simp +next + case (CAppR t' E1) + have ih: "(E1 \ E2)\t\ = E1\E2\t\\" by fact + show "((CAppR t' E1) \ E2)\t\ = (CAppR t' E1)\E2\t\\" using ih by simp +qed + +subsection {* EXERCISE 6 *} + +text {* + Remove the sorries in the ctx_append proof below. You can make + use of the following two properties. +*} + +lemma neut_hole: + shows "E \ \ = E" +by (induct E) (simp_all) + +lemma compose_assoc: + shows "(E1 \ E2) \ E3 = E1 \ (E2 \ E3)" +by (induct E1) (simp_all) + +lemma + shows "(Es1 @ Es2)\ = (Es2\) \ (Es1\)" +proof (induct Es1) + case Nil + show "([] @ Es2)\ = Es2\ \ []\" using neut_hole by simp +next + case (Cons E Es1) + have ih: "(Es1 @ Es2)\ = Es2\ \ Es1\" by fact + have eq1: "((E # Es1) @ Es2)\ = (E # (Es1 @ Es2))\" by simp + have eq2: "(E # (Es1 @ Es2))\ = (Es1 @ Es2)\ \ E" by simp + have eq3: "(Es1 @ Es2)\ \ E = (Es2\ \ Es1\) \ E" using ih by simp + have eq4: "(Es2\ \ Es1\) \ E = Es2\ \ (Es1\ \ E)" using compose_assoc by simp + have eq5: "Es2\ \ (Es1\ \ E) = Es2\ \ (E # Es1)\" by simp + show "((E # Es1) @ Es2)\ = Es2\ \ (E # Es1)\" using eq1 eq2 eq3 eq4 eq5 by (simp only:) +qed + +text {* + The last proof involves several steps of equational reasoning. + Isar provides some convenient means to express such equational + reasoning in a much cleaner fashion using the "also have" + construction. +*} + +lemma + shows "(Es1 @ Es2)\ = (Es2\) \ (Es1\)" +proof (induct Es1) + case Nil + show "([] @ Es2)\ = Es2\ \ []\" using neut_hole by simp +next + case (Cons E Es1) + have ih: "(Es1 @ Es2)\ = Es2\ \ Es1\" by fact + have "((E # Es1) @ Es2)\ = (E # (Es1 @ Es2))\" by simp + also have "\ = (Es1 @ Es2)\ \ E" by simp + also have "\ = (Es2\ \ Es1\) \ E" using ih by simp + also have "\ = Es2\ \ (Es1\ \ E)" using compose_assoc by simp + also have "\ = Es2\ \ (E # Es1)\" by simp + finally show "((E # Es1) @ Es2)\ = Es2\ \ (E # Es1)\" by simp +qed + + +end + diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial2.thy --- a/Tutorial/Tutorial2.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Tutorial2.thy Tue Jan 25 02:51:44 2011 +0900 @@ -1,15 +1,93 @@ + theory Tutorial2 -imports Tutorial1 +imports Lambda begin -(* fixme: put height example here *) +section {* Height of a Lambda-Term *} + +text {* + The theory Lambda defines the notions of capture-avoiding + substitution and the height of lambda terms. +*} + +thm height.simps +thm subst.simps + +subsection {* EXERCISE 7 *} + +text {* + Lets prove a property about the height of substitutions. + + Assume that the height of a lambda-term is always greater + or equal to 1. +*} + +lemma height_ge_one: + shows "1 \ height t" +by (induct t rule: lam.induct) (auto) + +text {* Remove the sorries *} + +theorem height_subst: + shows "height (t[x ::= t']) \ height t - 1 + height t'" +proof (induct t rule: lam.induct) + case (Var y) + show "height (Var y[x ::= t']) \ height (Var y) - 1 + height t'" sorry +next + case (App t1 t2) + have ih1: "height (t1[x::=t']) \ (height t1) - 1 + height t'" by fact + have ih2: "height (t2[x::=t']) \ (height t2) - 1 + height t'" by fact + + show "height ((App t1 t2)[x ::= t']) \ height (App t1 t2) - 1 + height t'" sorry +next + case (Lam y t1) + have ih: "height (t1[x::=t']) \ height t1 - 1 + height t'" by fact + -- {* the definition of capture-avoiding substitution *} + thm subst.simps + + show "height ((Lam [y].t1)[x ::= t']) \ height (Lam [y].t1) - 1 + height t'" sorry +qed -section {* Types *} +text {* + The point is that substitutions can only be moved under a binder + provided certain freshness conditions are satisfied. The structural + induction above does not say anything about such freshness conditions. + + Fortunately, Nominal derives automatically some stronger induction + principle for lambda terms which has the usual variable convention + build in. + + In the proof below, we use this stronger induction principle. The + variable and application case are as before. +*} + + +theorem + shows "height (t[x ::= t']) \ height t - 1 + height t'" +proof (nominal_induct t avoiding: x t' rule: lam.strong_induct) + case (Var y) + have "1 \ height t'" using height_ge_one by simp + then show "height (Var y[x ::= t']) \ height (Var y) - 1 + height t'" by simp +next + case (App t1 t2) + have ih1: "height (t1[x::=t']) \ (height t1) - 1 + height t'" + and ih2: "height (t2[x::=t']) \ (height t2) - 1 + height t'" by fact+ + then show "height ((App t1 t2)[x ::= t']) \ height (App t1 t2) - 1 + height t'" by simp +next + case (Lam y t1) + have ih: "height (t1[x::=t']) \ height t1 - 1 + height t'" by fact + have vc: "atom y \ x" "atom y \ t'" by fact+ -- {* usual variable convention *} + + show "height ((Lam [y].t1)[x ::= t']) \ height (Lam [y].t1) - 1 + height t'" sorry +qed + + +section {* Types and the Weakening Lemma *} nominal_datatype ty = tVar "string" -| tArr "ty" "ty" ("_ \ _" [100, 100] 100) +| tArr "ty" "ty" (infixr "\" 100) text {* @@ -19,7 +97,6 @@ We next define the type of typing contexts, a predicate that defines valid contexts (i.e. lists that contain only unique variables) and the typing judgement. - *} type_synonym ty_ctx = "(name \ ty) list" @@ -79,7 +156,7 @@ "\1 \ \2 \ \x. x \ set \1 \ x \ set \2" -subsection {* EXERCISE 4 *} +subsection {* EXERCISE 8 *} text {* Fill in the details and give a proof of the weakening lemma. @@ -107,7 +184,7 @@ have a2: "\1 \ \2" by fact show "\2 \ Lam [x].t : T1 \ T2" sorry -qed (auto) -- {* the application case *} +qed (auto) -- {* the application case is automatic*} text {* @@ -170,10 +247,10 @@ text {* - The remedy is to use a stronger induction principle that + The remedy is to use again a stronger induction principle that has the usual "variable convention" already build in. The - following command derives this induction principle for us. - (We shall explain what happens here later.) + following command derives this induction principle for the typing + relation. (We shall explain what happens here later.) *} nominal_inductive typing @@ -184,7 +261,7 @@ text {* Compare the two induction principles *} thm typing.induct -thm typing.strong_induct -- {* has the additional assumption {atom x} \ c *} +thm typing.strong_induct -- {* note the additional assumption {atom x} \ c *} text {* We can use the stronger induction principle by replacing @@ -198,7 +275,8 @@ Try now the proof. *} - + +subsection {* EXERCISE 9 *} lemma weakening: assumes a: "\1 \ t : T" @@ -207,7 +285,7 @@ shows "\2 \ t : T" using a b c proof (nominal_induct avoiding: \2 rule: typing.strong_induct) - case (t_Var \1 x T) -- {* variable case is as before *} + case (t_Var \1 x T) -- {* again the variable case is as before *} have "\1 \ \2" by fact moreover have "valid \2" by fact @@ -221,34 +299,56 @@ have a0: "atom x \ \1" by fact have a1: "valid \2" by fact have a2: "\1 \ \2" by fact - have "valid ((x, T1) # \2)" using a1 vc by auto - moreover - have "(x, T1) # \1 \ (x, T1) # \2" using a2 by auto - ultimately - have "(x, T1) # \2 \ t : T2" using ih by simp - then show "\2 \ Lam [x].t : T1 \ T2" using vc by auto + + show "\2 \ Lam [x].t : T1 \ T2" sorry qed (auto) -- {* app case *} -text {* unbind / inconsistency example *} + +section {* Unbind and an Inconsistency Example *} + +text {* + You might wonder why we had to discharge some proof + obligations in order to obtain the stronger induction + principle for the typing relation. (Remember for + lambda terms this stronger induction principle is + derived automatically.) + + This proof obligation is really needed, because if we + assume universally a stronger induction principle, then + in some cases we can derive false. This is "shown" below. +*} + inductive - unbind :: "lam \ lam \ bool" ("_ \ _" [60, 60] 60) + unbind :: "lam \ lam \ bool" (infixr "\" 60) where u_Var[intro]: "Var x \ Var x" | u_App[intro]: "App t1 t2 \ App t1 t2" | u_Lam[intro]: "t \ t' \ Lam [x].t \ t'" +text {* It is clear that the following judgement holds. *} + lemma unbind_simple: shows "Lam [x].Var x \ Var x" by auto +text {* + Now lets derive the strong induction principle for unbind. + The point is that we cannot establish the proof obligations, + therefore we force Isabelle to accept them by using "sorry". +*} + equivariance unbind - nominal_inductive unbind avoids u_Lam: "x" sorry +text {* + Using the stronger induction principle, we can establish + th follwoing bogus property. +*} + lemma unbind_fake: fixes y::"name" assumes a: "t \ t'" @@ -265,12 +365,20 @@ then show "atom y \ t'" using ih by simp qed +text {* + And from this follows the inconsitency: +*} + lemma shows "False" proof - have "atom x \ Lam [x]. Var x" by (simp add: lam.fresh) - then have "atom x \ Var x" using unbind_fake unbind_simple by auto - then show "False" by (simp add: lam.fresh fresh_at_base) + moreover + have "Lam [x]. Var x \ Var x" using unbind_simple by auto + ultimately + have "atom x \ Var x" using unbind_fake by auto + then have "x \ x" by (simp add: lam.fresh fresh_at_base) + then show "False" by simp qed end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial2s.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tutorial/Tutorial2s.thy Tue Jan 25 02:51:44 2011 +0900 @@ -0,0 +1,354 @@ + +theory Tutorial2s +imports Lambda +begin + +section {* Height of a Lambda-Term *} + +text {* + The theory Lambda defines the notions of capture-avoiding + substitution and the height of lambda terms. +*} + +thm height.simps +thm subst.simps + +subsection {* EXERCISE 7 *} + +text {* + Lets prove a property about the height of substitutions. + + Assume that the height of a lambda-term is always greater + or equal to 1. +*} + +lemma height_ge_one: + shows "1 \ height t" +by (induct t rule: lam.induct) (auto) + +text {* Remove the sorries *} + +theorem + shows "height (t[x ::= t']) \ height t - 1 + height t'" +proof (nominal_induct t avoiding: x t' rule: lam.strong_induct) + case (Var y) + have "1 \ height t'" using height_ge_one by simp + then show "height (Var y[x ::= t']) \ height (Var y) - 1 + height t'" by simp +next + case (App t1 t2) + have ih1: "height (t1[x::=t']) \ (height t1) - 1 + height t'" + and ih2: "height (t2[x::=t']) \ (height t2) - 1 + height t'" by fact+ + then show "height ((App t1 t2)[x ::= t']) \ height (App t1 t2) - 1 + height t'" by simp +next + case (Lam y t1) + have ih: "height (t1[x::=t']) \ height t1 - 1 + height t'" by fact + moreover + have vc: "atom y \ x" "atom y \ t'" by fact+ -- {* usual variable convention *} + ultimately + show "height ((Lam [y].t1)[x ::= t']) \ height (Lam [y].t1) - 1 + height t'" by simp +qed + + +section {* Types and the Weakening Lemma *} + +nominal_datatype ty = + tVar "string" +| tArr "ty" "ty" (infixr "\" 100) + + +text {* + Having defined them as nominal datatypes gives us additional + definitions and theorems that come with types (see below). + + We next define the type of typing contexts, a predicate that + defines valid contexts (i.e. lists that contain only unique + variables) and the typing judgement. +*} + +type_synonym ty_ctx = "(name \ ty) list" + +inductive + valid :: "ty_ctx \ bool" +where + v1[intro]: "valid []" +| v2[intro]: "\valid \; atom x \ \\\ valid ((x, T) # \)" + + +inductive + typing :: "ty_ctx \ lam \ ty \ bool" ("_ \ _ : _" [60, 60, 60] 60) +where + t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" +| t_App[intro]: "\\ \ t1 : T1 \ T2; \ \ t2 : T1\ \ \ \ App t1 t2 : T2" +| t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam [x].t : T1 \ T2" + + +text {* + The predicate atom x \ \, read as x fresh for \, is defined by + Nominal Isabelle. It is defined for lambda-terms, products, lists etc. + For example we have: +*} + +lemma + fixes x::"name" + shows "atom x \ Lam [x].t" + and "atom x \ (t1, t2) \ atom x \ App t1 t2" + and "atom x \ Var y \ atom x \ y" + and "\atom x \ t1; atom x \ t2\ \ atom x \ (t1, t2)" + and "\atom x \ l1; atom x \ l2\ \ atom x \ (l1 @ l2)" + and "atom x \ y \ x \ y" + by (simp_all add: lam.fresh fresh_append fresh_at_base) + +text {* + We can also prove that every variable is fresh for a type. +*} + +lemma ty_fresh: + fixes x::"name" + and T::"ty" + shows "atom x \ T" +by (induct T rule: ty.induct) + (simp_all add: ty.fresh pure_fresh) + +text {* + In order to state the weakening lemma in a convenient form, we + using the following abbreviation. Abbreviations behave like + definitions, except that they are always automatically folded + and unfolded. +*} + +abbreviation + "sub_ty_ctx" :: "ty_ctx \ ty_ctx \ bool" ("_ \ _" [60, 60] 60) +where + "\1 \ \2 \ \x. x \ set \1 \ x \ set \2" + + +subsection {* EXERCISE 8 *} + +text {* + Fill in the details and give a proof of the weakening lemma. +*} + +lemma + assumes a: "\1 \ t : T" + and b: "valid \2" + and c: "\1 \ \2" + shows "\2 \ t : T" +using a b c +proof (induct arbitrary: \2) + case (t_Var \1 x T) + have a1: "valid \1" by fact + have a2: "(x, T) \ set \1" by fact + have a3: "valid \2" by fact + have a4: "\1 \ \2" by fact + + show "\2 \ Var x : T" sorry +next + case (t_Lam x \1 T1 t T2) + have ih: "\\3. \valid \3; (x, T1) # \1 \ \3\ \ \3 \ t : T2" by fact + have a0: "atom x \ \1" by fact + have a1: "valid \2" by fact + have a2: "\1 \ \2" by fact + + show "\2 \ Lam [x].t : T1 \ T2" sorry +qed (auto) -- {* the application case is automatic*} + + +text {* + Despite the frequent claim that the weakening lemma is trivial, + routine or obvious, the proof in the lambda-case does not go + through smoothly. Painful variable renamings seem to be necessary. + But the proof using renamings is horribly complicated (see below). +*} + +equivariance valid +equivariance typing + +lemma weakening_NOT_TO_BE_TRIED_AT_HOME: + assumes a: "\1 \ t : T" + and b: "valid \2" + and c: "\1 \ \2" + shows "\2 \ t : T" +using a b c +proof (induct arbitrary: \2) + -- {* lambda case *} + case (t_Lam x \1 T1 t T2) + have fc0: "atom x \ \1" by fact + have ih: "\\3. \valid \3; (x, T1) # \1 \ \3\ \ \3 \ t : T2" by fact + -- {* we choose a fresh variable *} + obtain c::"name" where fc1: "atom c \ (x, t, \1, \2)" by (rule obtain_fresh) + -- {* we alpha-rename the abstraction *} + have "Lam [c].((c \ x) \ t) = Lam [x].t" using fc1 + by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def) + moreover + -- {* we can then alpha rename the goal *} + have "\2 \ Lam [c].((c \ x) \ t) : T1 \ T2" + proof - + -- {* we need to establish *} + -- {* (1) (x, T1) # \1 \ (x, T1) # ((c \ x) \ \2) *} + -- {* (2) valid ((x, T1) # ((c \ x) \ \2)) *} + have "(1)": "(x, T1) # \1 \ (x, T1) # ((c \ x) \ \2)" + proof - + have "\1 \ \2" by fact + then have "(c \ x) \ ((x, T1) # \1 \ (x, T1) # ((c \ x) \ \2))" using fc0 fc1 + by (perm_simp) (simp add: flip_fresh_fresh) + then show "(x, T1) # \1 \ (x, T1) # ((c \ x) \ \2)" by (rule permute_boolE) + qed + moreover + have "(2)": "valid ((x, T1) # ((c \ x) \ \2))" + proof - + have "valid \2" by fact + then show "valid ((x, T1) # ((c \ x) \ \2))" using fc1 + by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt) + qed + -- {* these two facts give us by induction hypothesis the following *} + ultimately have "(x, T1) # ((c \ x) \ \2) \ t : T2" using ih by simp + -- {* we now apply renamings to get to our goal *} + then have "(c \ x) \ ((x, T1) # ((c \ x) \ \2) \ t : T2)" by (rule permute_boolI) + then have "(c, T1) # \2 \ ((c \ x) \ t) : T2" using fc1 + by (perm_simp) (simp add: flip_fresh_fresh ty_fresh) + then show "\2 \ Lam [c].((c \ x) \ t) : T1 \ T2" using fc1 by auto + qed + ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp +qed (auto) -- {* var and app cases, luckily, are automatic *} + + +text {* + The remedy is to use again a stronger induction principle that + has the usual "variable convention" already build in. The + following command derives this induction principle for the typing + relation. (We shall explain what happens here later.) +*} + +nominal_inductive typing + avoids t_Lam: "x" + unfolding fresh_star_def + by (simp_all add: fresh_Pair lam.fresh ty_fresh) + +text {* Compare the two induction principles *} + +thm typing.induct +thm typing.strong_induct -- {* note the additional assumption {atom x} \ c *} + +text {* + We can use the stronger induction principle by replacing + the line + + proof (induct arbitrary: \2) + + with + + proof (nominal_induct avoiding: \2 rule: typing.strong_induct) + + Try now the proof. +*} + +subsection {* EXERCISE 9 *} + +lemma weakening: + assumes a: "\1 \ t : T" + and b: "valid \2" + and c: "\1 \ \2" + shows "\2 \ t : T" +using a b c +proof (nominal_induct avoiding: \2 rule: typing.strong_induct) + case (t_Var \1 x T) -- {* variable case is as before *} + have "\1 \ \2" by fact + moreover + have "valid \2" by fact + moreover + have "(x, T)\ set \1" by fact + ultimately show "\2 \ Var x : T" by auto +next + case (t_Lam x \1 T1 t T2) + have vc: "atom x \ \2" by fact -- {* additional fact afforded by the strong induction *} + have ih: "\\3. \valid \3; (x, T1) # \1 \ \3\ \ \3 \ t : T2" by fact + have a0: "atom x \ \1" by fact + have a1: "valid \2" by fact + have a2: "\1 \ \2" by fact + have "valid ((x, T1) # \2)" using a1 vc by auto + moreover + have "(x, T1) # \1 \ (x, T1) # \2" using a2 by auto + ultimately + have "(x, T1) # \2 \ t : T2" using ih by simp + then show "\2 \ Lam [x].t : T1 \ T2" using vc by auto +qed (auto) -- {* app case *} + + + +section {* Unbind and an Inconsistency Example *} + +text {* + You might wonder why we had to discharge some proof + obligations in order to obtain the stronger induction + principle for the typing relation. (Remember for + lambda terms this stronger induction principle is + derived automatically.) + + This proof obligation is really needed, because if we + assume universally a stronger induction principle, then + in some cases we can derive false. This is "shown" below. +*} + + +inductive + unbind :: "lam \ lam \ bool" (infixr "\" 60) +where + u_Var[intro]: "Var x \ Var x" +| u_App[intro]: "App t1 t2 \ App t1 t2" +| u_Lam[intro]: "t \ t' \ Lam [x].t \ t'" + +text {* It is clear that the following judgement holds. *} + +lemma unbind_simple: + shows "Lam [x].Var x \ Var x" + by auto + +text {* + Now lets derive the strong induction principle for unbind. + The point is that we cannot establish the proof obligations, + therefore we force Isabelle to accept them by using "sorry". +*} + +equivariance unbind +nominal_inductive unbind + avoids u_Lam: "x" + sorry + +text {* + Using the stronger induction principle, we can establish + th follwoing bogus property. +*} + +lemma unbind_fake: + fixes y::"name" + assumes a: "t \ t'" + and b: "atom y \ t" + shows "atom y \ t'" +using a b +proof (nominal_induct avoiding: y rule: unbind.strong_induct) + case (u_Lam t t' x y) + have ih: "atom y \ t \ atom y \ t'" by fact + have asm: "atom y \ Lam [x]. t" by fact + have fc: "atom x \ y" by fact + then have in_eq: "x \ y" by (simp add: fresh_at_base) + then have "atom y \ t" using asm by (simp add: lam.fresh) + then show "atom y \ t'" using ih by simp +qed + +text {* + And from this follows the inconsitency: +*} + +lemma + shows "False" +proof - + have "atom x \ Lam [x]. Var x" by (simp add: lam.fresh) + moreover + have "Lam [x]. Var x \ Var x" using unbind_simple by auto + ultimately + have "atom x \ Var x" using unbind_fake by auto + then have "x \ x" by (simp add: lam.fresh fresh_at_base) + then show "False" by simp +qed + +end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial3.thy --- a/Tutorial/Tutorial3.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Tutorial3.thy Tue Jan 25 02:51:44 2011 +0900 @@ -5,16 +5,20 @@ section {* Formalising Barendregt's Proof of the Substitution Lemma *} text {* - Barendregt's proof needs in the variable case a case distinction. - One way to do this in Isar is to use blocks. A block consist of some - assumptions and reasoning steps enclosed in curly braces, like + The substitution lemma is another theorem where the variable + convention plays a crucial role. + + Barendregt's proof of this lemma needs in the variable case a + case distinction. One way to do this in Isar is to use blocks. + A block consist of some assumptions and reasoning steps + enclosed in curly braces, like { \ have "statement" have "last_statement_in_the_block" } - Such a block can contain local assumptions like + Such a block may contain local assumptions like { assume "A" assume "B" @@ -74,7 +78,7 @@ -section {* EXERCISE 7 *} +section {* EXERCISE 10 *} text {* Fill in the cases 1.2 and 1.3 and the equational reasoning @@ -143,5 +147,11 @@ by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) (auto simp add: fresh_fact forget) +subsection {* MINI EXERCISE *} + +text {* + Compare and contrast Barendregt's reasoning and the + formalised proofs. +*} end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial3s.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tutorial/Tutorial3s.thy Tue Jan 25 02:51:44 2011 +0900 @@ -0,0 +1,162 @@ + +theory Tutorial3s +imports Lambda +begin + +section {* Formalising Barendregt's Proof of the Substitution Lemma *} + +text {* + The substitution lemma is another theorem where the variable + convention plays a crucial role. + + Barendregt's proof of this lemma needs in the variable case a + case distinction. One way to do this in Isar is to use blocks. + A block consist of some assumptions and reasoning steps + enclosed in curly braces, like + + { \ + have "statement" + have "last_statement_in_the_block" + } + + Such a block may contain local assumptions like + + { assume "A" + assume "B" + \ + have "C" by \ + } + + Where "C" is the last have-statement in this block. The behaviour + of such a block to the 'outside' is the implication + + A \ B \ C + + Now if we want to prove a property "smth" using the case-distinctions + P1, P2 and P3 then we can use the following reasoning: + + { assume "P1" + \ + have "smth" + } + moreover + { assume "P2" + \ + have "smth" + } + moreover + { assume "P3" + \ + have "smth" + } + ultimately have "smth" by blast + + The blocks establish the implications + + P1 \ smth + P2 \ smth + P3 \ smth + + If we know that P1, P2 and P3 cover all the cases, that is P1 \ P2 \ P3 + holds, then we have 'ultimately' established the property "smth" + +*} + +subsection {* Two preliminary facts *} + +lemma forget: + shows "atom x \ t \ t[x ::= s] = t" +by (nominal_induct t avoiding: x s rule: lam.strong_induct) + (auto simp add: lam.fresh fresh_at_base) + +lemma fresh_fact: + assumes a: "atom z \ s" + and b: "z = y \ atom z \ t" + shows "atom z \ t[y ::= s]" +using a b +by (nominal_induct t avoiding: z y s rule: lam.strong_induct) + (auto simp add: lam.fresh fresh_at_base) + + + +section {* EXERCISE 10 *} + +text {* + Fill in the cases 1.2 and 1.3 and the equational reasoning + in the lambda-case. +*} + +lemma + assumes a: "x \ y" + and b: "atom x \ L" + shows "M[x ::= N][y ::= L] = M[y ::= L][x ::= N[y ::= L]]" +using a b +proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct) + case (Var z) + have a1: "x \ y" by fact + have a2: "atom x \ L" by fact + show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS") + proof - + { -- {* Case 1.1 *} + assume c1: "z = x" + have "(1)": "?LHS = N[y::=L]" using c1 by simp + have "(2)": "?RHS = N[y::=L]" using c1 a1 by simp + have "?LHS = ?RHS" using "(1)" "(2)" by simp + } + moreover + { -- {* Case 1.2 *} + assume c2: "z = y" "z \ x" + have "(1)": "?LHS = L" using c2 by simp + have "(2)": "?RHS = L[x::=N[y::=L]]" using c2 by simp + have "(3)": "L[x::=N[y::=L]] = L" using a2 forget by simp + have "?LHS = ?RHS" using "(1)" "(2)" "(3)" by simp + } + moreover + { -- {* Case 1.3 *} + assume c3: "z \ x" "z \ y" + have "(1)": "?LHS = Var z" using c3 by simp + have "(2)": "?RHS = Var z" using c3 by simp + have "?LHS = ?RHS" using "(1)" "(2)" by simp + } + ultimately show "?LHS = ?RHS" by blast + qed +next + case (Lam z M1) -- {* case 2: lambdas *} + have ih: "\x \ y; atom x \ L\ \ M1[x ::= N][y ::= L] = M1[y ::= L][x ::= N[y ::= L]]" by fact + have a1: "x \ y" by fact + have a2: "atom x \ L" by fact + have fs: "atom z \ x" "atom z \ y" "atom z \ N" "atom z \ L" by fact+ -- {* !! *} + then have b: "atom z \ N[y::=L]" by (simp add: fresh_fact) + show "(Lam [z].M1)[x ::= N][y ::= L] = (Lam [z].M1)[y ::= L][x ::= N[y ::= L]]" (is "?LHS=?RHS") + proof - + have "?LHS = Lam [z].(M1[x ::= N][y ::= L])" using fs by simp + also have "\ = Lam [z].(M1[y ::= L][x ::= N[y ::= L]])" using ih a1 a2 by simp + also have "\ = (Lam [z].(M1[y ::= L]))[x ::= N[y ::= L]]" using b fs by simp + also have "\ = ?RHS" using fs by simp + finally show "?LHS = ?RHS" by simp + qed +next + case (App M1 M2) -- {* case 3: applications *} + then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp +qed + +text {* + Again the strong induction principle enables Isabelle to find + the proof of the substitution lemma completely automatically. +*} + +lemma substitution_lemma_version: + assumes asm: "x \ y" "atom x \ L" + shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" + using asm +by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) + (auto simp add: fresh_fact forget) + +subsection {* MINI EXERCISE *} + +text {* + Compare and contrast Barendregt's reasoning and the + formalised proofs. +*} + +end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial4.thy --- a/Tutorial/Tutorial4.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Tutorial4.thy Tue Jan 25 02:51:44 2011 +0900 @@ -1,22 +1,58 @@ theory Tutorial4 -imports Tutorial1 Tutorial2 Tutorial3 +imports Tutorial1 Tutorial2 begin section {* The CBV Reduction Relation (Small-Step Semantics) *} -text {* - In order to help establishing the property that the Machine - calculates a normal form that corresponds to the evaluation - relation, we introduce the call-by-value small-step semantics. -*} inductive cbv :: "lam \ lam \ bool" ("_ \cbv _" [60, 60] 60) where cbv1: "\val v; atom x \ v\ \ App (Lam [x].t) v \cbv t[x ::= v]" -| cbv2[intro]: "t \cbv t' \ App t t2 \cbv App t' t2" -| cbv3[intro]: "t \cbv t' \ App t2 t \cbv App t2 t'" +| cbv2: "t \cbv t' \ App t t2 \cbv App t' t2" +| cbv3: "t \cbv t' \ App t2 t \cbv App t2 t'" + +inductive + "cbv_star" :: "lam \ lam \ bool" (" _ \cbv* _" [60, 60] 60) +where + cbvs1: "e \cbv* e" +| cbvs2: "\e1\cbv e2; e2 \cbv* e3\ \ e1 \cbv* e3" + +declare cbv.intros[intro] cbv_star.intros[intro] + +subsection {* EXERCISE 11 *} + +text {* + Show that cbv* is transitive, by filling the gaps in the + proof below. +*} + +lemma cbvs3 [intro]: + assumes a: "e1 \cbv* e2" "e2 \cbv* e3" + shows "e1 \cbv* e3" +using a +proof (induct) + case (cbvs1 e1) + have asm: "e1 \cbv* e3" by fact + show "e1 \cbv* e3" sorry +next + case (cbvs2 e1 e2 e3') + have "e1 \cbv e2" by fact + have "e2 \cbv* e3'" by fact + have "e3' \cbv* e3 \ e2 \cbv* e3" by fact + have "e3' \cbv* e3" by fact + + show "e1 \cbv* e3" sorry +qed + + +text {* + In order to help establishing the property that the machine + calculates a normal form that corresponds to the evaluation + relation, we introduce the call-by-value small-step semantics. +*} + equivariance val equivariance cbv @@ -44,7 +80,7 @@ lemma better_cbv1 [intro]: assumes a: "val v" - shows "App (Lam [x].t) v \cbv t[x::=v]" + shows "App (Lam [x].t) v \cbv t[x ::= v]" proof - obtain y::"name" where fs: "atom y \ (x, t, v)" by (rule obtain_fresh) have "App (Lam [x].t) v = App (Lam [y].((y \ x) \ t)) v" using fs @@ -54,23 +90,9 @@ finally show "App (Lam [x].t) v \cbv t[x ::= v]" by simp qed -text {* - The transitive closure of the cbv-reduction relation: -*} - -inductive - "cbvs" :: "lam \ lam \ bool" (" _ \cbv* _" [60, 60] 60) -where - cbvs1[intro]: "e \cbv* e" -| cbvs2[intro]: "\e1\cbv e2; e2 \cbv* e3\ \ e1 \cbv* e3" - -lemma cbvs3 [intro]: - assumes a: "e1 \cbv* e2" "e2 \cbv* e3" - shows "e1 \cbv* e3" -using a by (induct) (auto) -subsection {* EXERCISE 8 *} +subsection {* EXERCISE 12 *} text {* If more simple exercises are needed, then complete the following proof. @@ -83,26 +105,22 @@ proof (induct E) case Hole have "t \cbv t'" by fact - then show "\\t\ \cbv \\t'\" by simp + show "\\t\ \cbv \\t'\" sorry next case (CAppL E s) have ih: "t \cbv t' \ E\t\ \cbv E\t'\" by fact - moreover have "t \cbv t'" by fact - ultimately - have "E\t\ \cbv E\t'\" by simp - then show "(CAppL E s)\t\ \cbv (CAppL E s)\t'\" by auto + + show "(CAppL E s)\t\ \cbv (CAppL E s)\t'\" sorry next case (CAppR s E) have ih: "t \cbv t' \ E\t\ \cbv E\t'\" by fact - moreover have a: "t \cbv t'" by fact - ultimately - have "E\t\ \cbv E\t'\" by simp - then show "(CAppR s E)\t\ \cbv (CAppR s E)\t'\" by auto + + show "(CAppR s E)\t\ \cbv (CAppR s E)\t'\" sorry qed -section {* EXERCISE 9 *} +section {* EXERCISE 13 *} text {* The point of the cbv-reduction was that we can easily relatively @@ -131,7 +149,8 @@ text {* It is not difficult to extend the lemma above to - arbitrary reductions sequences of the CK machine. *} + arbitrary reductions sequences of the machine. +*} lemma machines_implies_cbvs_ctx: assumes a: " \* " @@ -140,7 +159,7 @@ by (induct) (blast)+ text {* - So whenever we let the CL machine start in an initial + So whenever we let the machine start in an initial state and it arrives at a final state, then there exists a corresponding cbv-reduction sequence. *} @@ -156,14 +175,10 @@ text {* We now want to relate the cbv-reduction to the evaluation - relation. For this we need two auxiliary lemmas. + relation. For this we need one auxiliary lemma about + inverting the e_App rule. *} -lemma eval_val: - assumes a: "val t" - shows "t \ t" -using a by (induct) (auto) - lemma e_App_elim: assumes a: "App t1 t2 \ v" @@ -171,7 +186,7 @@ using a by (cases) (auto simp add: lam.eq_iff lam.distinct) -subsection {* EXERCISE *} +subsection {* EXERCISE 13 *} text {* Complete the first and second case in the @@ -186,9 +201,8 @@ case (cbv1 v x t t3) have a1: "val v" by fact have a2: "t[x ::= v] \ t3" by fact - have a3: "Lam [x].t \ Lam [x].t" by auto - have a4: "v \ v" using a1 eval_val by auto - show "App (Lam [x].t) v \ t3" using a3 a4 a2 by auto + + show "App (Lam [x].t) v \ t3" sorry next case (cbv2 t t' t2 t3) have ih: "\t3. t' \ t3 \ t \ t3" by fact @@ -197,14 +211,15 @@ where a1: "t' \ Lam [x].t''" and a2: "t2 \ v'" and a3: "t''[x ::= v'] \ t3" by (rule e_App_elim) - have "t \ Lam [x].t''" using ih a1 by auto - then show "App t t2 \ t3" using a2 a3 by auto + + show "App t t2 \ t3" sorry qed (auto elim!: e_App_elim) text {* Next we extend the lemma above to arbitray initial - sequences of cbv-reductions. *} + sequences of cbv-reductions. +*} lemma cbvs_eval: assumes a: "t1 \cbv* t2" "t2 \ t3" @@ -214,30 +229,42 @@ text {* Finally, we can show that if from a term t we reach a value by a cbv-reduction sequence, then t evaluates to this value. + + This proof is not by induction. So we have to set up the proof + with + + proof - + + in order to prevent Isabelle from applying a default introduction + rule. *} lemma cbvs_implies_eval: - assumes a: "t \cbv* v" "val v" + assumes a: "t \cbv* v" + and b: "val v" shows "t \ v" -using a -by (induct) (auto intro: eval_val cbvs_eval) +proof - + have "v \ v" using b eval_val by simp + then show "t \ v" using a cbvs_eval by auto +qed + +section {* EXERCISE 15 *} text {* - All facts tied together give us the desired property about - machines. + All facts tied together give us the desired property + about machines: we know that a machines transitions + correspond to cbvs transitions, and with the lemma + above they correspond to an eval judgement. *} theorem machines_implies_eval: assumes a: " \* " and b: "val t2" shows "t1 \ t2" -proof - - have "t1 \cbv* t2" using a machines_implies_cbvs by simp - then show "t1 \ t2" using b cbvs_implies_eval by simp +proof - + + show "t1 \ t2" sorry qed - - - end diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial5.thy --- a/Tutorial/Tutorial5.thy Tue Jan 25 02:46:05 2011 +0900 +++ b/Tutorial/Tutorial5.thy Tue Jan 25 02:51:44 2011 +0900 @@ -1,9 +1,22 @@ + + theory Tutorial5 imports Tutorial4 begin +section {* Type-Preservation and Progress Lemma*} -section {* Type Preservation (fixme separate file) *} +text {* + The point of this tutorial is to prove the + type-preservation and progress lemma. Since + we now know that \, \cbv* and the machine + correspond to each other, we only need to + prove this property for one of them. We chose + \cbv. + + First we need to establish two elimination + properties and two auxiliary lemmas about contexts. +*} lemma valid_elim: @@ -30,6 +43,16 @@ using a1 a2 a3 by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base) + +section {* EXERCISE 16 *} + +text {* + Next we want to show the type substitution lemma. Unfortunately, + we have to prove a slightly more general version of it, where + the variable being substituted occurs somewhere inside the + context. +*} + lemma type_substitution_aux: assumes a: "\ @ [(x, T')] @ \ \ e : T" and b: "\ \ e' : T'" @@ -40,10 +63,11 @@ have a1: "valid (\ @ [(x, T')] @ \)" by fact have a2: "(y,T) \ set (\ @ [(x, T')] @ \)" by fact have a3: "\ \ e' : T'" by fact + from a1 have a4: "valid (\ @ \)" by (rule valid_insert) { assume eq: "x = y" - from a1 a2 have "T = T'" using eq by (auto intro: context_unique) - with a3 have "\ @ \ \ Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening) + + have "\ @ \ \ Var y[x ::= e'] : T" sorry } moreover { assume ineq: "x \ y" @@ -51,15 +75,46 @@ then have "\ @ \ \ Var y[x ::= e'] : T" using ineq a4 by auto } ultimately show "\ @ \ \ Var y[x::=e'] : T" by blast -qed (force simp add: fresh_append fresh_Cons)+ +next + case (t_Lam y T1 t T2 x e' \) + have a1: "atom y \ e'" by fact + have a2: "atom y \ \ @ [(x, T')] @ \" by fact + have a3: "\ \ e' : T'" by fact + have ih: "\ \ e' : T' \ ((y, T1) # \) @ \ \ t [x ::= e'] : T2" + using t_Lam(6)[of "(y, T1) # \"] by auto + + + show "\ @ \ \ (Lam [y]. t)[x ::= e'] : T1 \ T2" sorry +next + case (t_App t1 T1 T2 t2 x e' \) + have ih1: "\ \ e' : T' \ \ @ \ \ t1 [x ::= e'] : T1 \ T2" using t_App(2) by auto + have ih2: "\ \ e' : T' \ \ @ \ \ t2 [x ::= e'] : T1" using t_App(4) by auto + have a: "\ \ e' : T'" by fact + + show "\ @ \ \ App t1 t2 [x ::= e'] : T2" sorry +qed + +text {* + From this we can derive the usual version of the substitution + lemma. +*} corollary type_substitution: assumes a: "(x, T') # \ \ e : T" and b: "\ \ e' : T'" shows "\ \ e[x ::= e'] : T" -using a b type_substitution_aux[where \="[]"] +using a b type_substitution_aux[of "[]"] by auto + +section {* Type Preservation *} + +text {* + Finally we are in a position to establish the type preservation + property. We just need the following two inversion rules for + particualr typing instances. +*} + lemma t_App_elim: assumes a: "\ \ App t1 t2 : T" obtains T' where "\ \ t1 : T' \ T" "\ \ t2 : T'" @@ -81,13 +136,34 @@ apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) done + +section {* EXERCISE 17 *} + +text {* + Fill in the gaps in the t_Lam case. You will need + the type substitution lemma proved above. +*} + theorem cbv_type_preservation: assumes a: "t \cbv t'" and b: "\ \ t : T" shows "\ \ t' : T" using a b -by (nominal_induct avoiding: \ T rule: cbv.strong_induct) - (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff) +proof (nominal_induct avoiding: \ T rule: cbv.strong_induct) + case (cbv1 v x t \ T) + have fc: "atom x \ \" by fact + have "\ \ App (Lam [x]. t) v : T" by fact + then obtain T' where + *: "\ \ Lam [x]. t : T' \ T" and + **: "\ \ v : T'" by (rule t_App_elim) + have "(x, T') # \ \ t : T" using * fc by (rule t_Lam_elim) (simp add: ty.eq_iff) + + show "\ \ t [x ::= v] : T " sorry +qed (auto elim!: t_App_elim) + +text {* + We can easily extend this to sequences of cbv* reductions. +*} corollary cbvs_type_preservation: assumes a: "t \cbv* t'" @@ -132,7 +208,7 @@ shows "(\t'. t \cbv t') \ (val t)" using a by (induct \\"[]::ty_ctx" t T) - (auto elim: canonical_tArr) + (auto elim: canonical_tArr simp add: val.simps) text {* Done! Congratulations! diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/Tutorial6.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tutorial/Tutorial6.thy Tue Jan 25 02:51:44 2011 +0900 @@ -0,0 +1,49 @@ +theory Tutorial6 +imports "../Nominal/Nominal2" +begin + + +section {* Type Schemes *} + +text {* + Nominal2 can deal also with more complicated binding + structures; for example the finite set of binders found + in type schemes. +*} + +atom_decl name + +nominal_datatype ty = + Var "name" +| Fun "ty" "ty" (infixr "\" 100) +and tys = + All as::"name fset" ty::"ty" bind (set+) as in ty ("All _. _" [100, 100] 100) + + +text {* Some alpha-equivalences *} + +lemma + shows "All {|a, b|}. (Var a) \ (Var b) = All {|b, a|}. (Var a) \ (Var b)" + unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def + by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero) + +lemma + shows "All {|a, b|}. (Var a) \ (Var b) = All {|a, b|}. (Var b) \ (Var a)" + unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def + by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def swap_atom) + (metis permute_flip_at) + +lemma + shows "All {|a, b, c|}. (Var a) \ (Var b) = All {|a, b|}. (Var a) \ (Var b)" + unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def + by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def intro: permute_zero) + +lemma + assumes a: "a \ b" + shows "All {|a, b|}. (Var a) \ (Var b) \ All {|c|}. (Var c) \ (Var c)" + using a + unfolding ty_tys.eq_iff Abs_eq_iff alphas fresh_star_def + by (auto simp add: ty_tys.eq_iff ty_tys.supp supp_at_base fresh_star_def) + + +end \ No newline at end of file diff -r 67451725fb41 -r 8ae1c2e6369e Tutorial/slides.pdf Binary file Tutorial/slides.pdf has changed