header {* 

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

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

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

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

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

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

  as you type. 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 the interface can be started on the command line with

     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

          =>      \<Rightarrow>

          ==>     \<Longrightarrow>

          -->     \<longrightarrow>

          !       \<forall>        

          ?       \<exists>

          /\      \<and>

          \/      \<or>

          ~       \<not>

          ~=      \<noteq>

          :       \<in>

          ~:      \<notin>

  For nominal two important symbols are

          \<sharp>       sharp     (freshness)

          \<bullet>       bullet    (permutations)

*}

theory Tutorial1

imports Lambda

begin

section {* Theories *}

text {*

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

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

*}

section {* Types *}

text {*

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

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

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

*}

typ nat

typ bool

typ string           

(*

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. You can have

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

*}

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

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

                     as a free variable, written in blue *}

term "\<forall>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 \<and> False"

term "True \<or> B"

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

term "\<forall>x. P x"

term "A \<longrightarrow> B"

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 \<longrightarrow> B"  -- {* versus *}

term "A \<Longrightarrow> B"

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

term "\<And>x. P x"

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

text {*

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

  beta-reduction.

  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 \<Longrightarrow> conclusion"

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

  There is an alternative way of writing the latter clause as

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

  If no premise is present, then one just writes

   "conclusion"

  Below we give two definitions for the transitive closure

*}

inductive

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

where

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

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

inductive

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

where

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

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

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

section {* Theorems *}

text {*

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

  database can be queried using 

*}

thm bs1_refl

thm bs2_trans

thm conjI

thm conjunct1

text {* 

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

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

thm beta_star2.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 \<dots>") and 

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

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

  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: "x \<noteq> y"

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

  shows "atom y \<sharp> t"

  using a b by (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"  \<dots>

      show "goal_to_be_proved" \<dots>

  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"  \<dots>

      \<dots>

      have "later_statement" using label \<dots>

  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 \<dots>" or 

  "using theorem-name \<dots>". 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 \<dots>

       \<dots>

       show \<dots>

     next

       case \<dots>

       \<dots>

       show \<dots>

     \<dots>

     qed

*}

subsection {* Exercise I *}

text {*

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

  justifications. 

*}

lemma

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

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

  using a

proof (induct)

  case (bs1_refl t)

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

next

  case (bs1_trans t1 t2 t3)

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

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

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

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

qed

subsection {* Exercise II *}

text {*

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

  justifications. 

*}

lemma bs1_trans2:

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

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

  shows "t1 \<longrightarrow>b* t3"

using a b

proof (induct)

  case (bs1_refl t1)

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

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

next

  case (bs1_trans t1 t2 t3')

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

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

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

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

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

qed

lemma

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

  shows "t1 \<longrightarrow>b* t2"

using a

proof (induct)

  case (bs2_refl t)

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

next

  case (bs2_step t1 t2)

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

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

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

next

  case (bs2_trans t1 t2 t3)

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

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

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

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: "t1 \<longrightarrow>b* t2"

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

  shows "t1 \<longrightarrow>b* t3"

using a b

proof (induct)

  case (bs1_refl t1)

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

next

  case (bs1_trans t1 t2 t3')

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

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

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

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

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

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" \<dots>

   moreover

   have "statement_2" \<dots>

   \<dots>

   moreover

   have "statement_n" \<dots>

   ultimately have "statement" \<dots>

  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: "t1 \<longrightarrow>b* t2"

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

  shows "t1 \<longrightarrow>b* t3"

using a b

proof (induct)

  case (bs1_refl t1)

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

next

  case (bs1_trans t1 t2 t3')

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

  moreover

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

  ultimately 

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

  moreover 

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

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

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: "t1 \<longrightarrow>b* t2" 

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

  using a

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

lemma 

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

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

  shows "t1 \<longrightarrow>b* t3"

using a b

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

lemma

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

  shows "t1 \<longrightarrow>b* t2"

using a

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

inductive

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

where

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

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