# HG changeset patch # User Cezary Kaliszyk # Date 1295734655 -32400 # Node ID b9e2a66a317cf43fc13d8924599d368cf4d577e7 # Parent af4fb03ecf329120c8159e51bb9172ed373a2fd3# Parent e8736c1cdd7f4fe918ed1f95317165b7fc584496 merge diff -r af4fb03ecf32 -r b9e2a66a317c Tutorial/Tutorial1.thy --- a/Tutorial/Tutorial1.thy Sun Jan 23 07:15:59 2011 +0900 +++ b/Tutorial/Tutorial1.thy Sun Jan 23 07:17:35 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. @@ -213,10 +212,8 @@ 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 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 @@ -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 af4fb03ecf32 -r b9e2a66a317c Tutorial/Tutorial1s.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Tutorial/Tutorial1s.thy Sun Jan 23 07:17:35 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 ("\