nominal2: Tutorial/Tutorial1.thy@eebc24b9cf39

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

          =>      \<Rightarrow>
          ==>     \<Longrightarrow>
          -->     \<longrightarrow>
          !       \<forall>        
          ?       \<exists>
          /\      \<and>
          \/      \<or>
          ~       \<not>
          ~=      \<noteq>
          :       \<in>
          ~:      \<notin>

  For nominal the following two symbols have a special meaning

        \<sharp>    sharp     (freshness)
        \<bullet>    bullet    (permutation application)
*}


theory Tutorial1
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 \<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 lam           -- {* alpha-equated lambda terms defined in Lambda.thy *}
typ name          -- {* type of (object) variables defined in Lambda.thy *}
typ "('a \<times> 'b)"   -- {* pair type *}
typ "'c set"      -- {* set type *}
typ "'a list"     -- {* list type *}
typ "lam \<Rightarrow> 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 overloaded function *}

text {* 
  Lam [x].Var is the syntax we made up for lambda abstractions. If you
  prefer, you can have your own syntax (but \<lambda> 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 "\<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"
term "atom a \<sharp> 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 \<longrightarrow> B"  -- {* versus *}
term "A \<Longrightarrow> B"

term "\<forall>x. P x"  -- {* versus *}
term "\<And>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 \<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
  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60)
where
  e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
| e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"

text {* 
  Values and cbv are also defined using inductive.  
*}

inductive
  val :: "lam \<Rightarrow> 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, \<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 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 \<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: "atom y \<sharp> Lam [x].t"
  shows "(y = x) \<or> (y \<noteq> x \<and> atom y \<sharp> 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"  \<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

   Two very simple example proofs are as follows.
*}

subsection {* EXERCISE 1 *}

lemma eval_val:
  assumes a: "val t"
  shows "t \<Down> t"
using a
proof (induct)
  case (v_Lam x t)
  show "Lam [x]. t \<Down> Lam [x]. t" sorry
qed

subsection {* EXERCISE 2 *}

text {* Fill the gaps in the proof below. *}

lemma eval_to_val:
  assumes a: "t \<Down> t'"
  shows "val t'"
using a
proof (induct)
  case (e_Lam x t)
  show "val (Lam [x].t)" sorry
next
  case (e_App t1 x t t2 v v')
  -- {* all assumptions in this case *}
  have "t1 \<Down> Lam [x].t" by fact
  have ih1: "val (Lam [x]. t)" by fact
  have "t2 \<Down> v" by fact
  have ih2: "val v" by fact
  have "t [x ::= v] \<Down> 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 "\<box>" for holes.
*}
  
datatype ctx = 
    Hole ("\<box>")  
  | CAppL "ctx" "lam"
  | CAppR "lam" "ctx"

text {* Now Isabelle knows about: *}

typ ctx
term "\<box>"
term "CAppL"
term "CAppL \<box> (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 \<Rightarrow> ctxs \<Rightarrow>lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto> <_,_>" [60, 60, 60, 60] 60)
where
  m1: "<App t1 t2, Es> \<mapsto> <t1, (CAppL \<box> t2) # Es>"
| m2: "val v \<Longrightarrow> <v, (CAppL \<box> t2) # Es> \<mapsto> <t2, (CAppR v \<box>) # Es>"
| m3: "val v \<Longrightarrow> <v, (CAppR (Lam [x].t) \<box>) # Es> \<mapsto> <t[x ::= 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 \<Rightarrow> ctxs \<Rightarrow> lam \<Rightarrow> ctxs \<Rightarrow> bool" ("<_,_> \<mapsto>* <_,_>" [60, 60, 60, 60] 60)
where
  ms1: "<t,Es> \<mapsto>* <t,Es>"
| ms2: "\<lbrakk><t1,Es1> \<mapsto> <t2,Es2>; <t2,Es2> \<mapsto>* <t3,Es3>\<rbrakk> \<Longrightarrow> <t1,Es1> \<mapsto>* <t3,Es3>"

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: "<e1, Es1> \<mapsto>* <e2, Es2>" 
  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
using a b
proof(induct)
  case (ms1 e1 Es1)
  have c: "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
  
  show "<e1, Es1> \<mapsto>* <e3, Es3>" sorry
next
  case (ms2 e1 Es1 e2 Es2 e2' Es2') 
  have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
  have d1: "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
  have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact

  show "<e1, Es1> \<mapsto>* <e3, Es3>" 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
  "then have" in order to feed a have-statement to the proof of 
  the next have-statement. This is used in the second case below.
*}
 
lemma 
  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
using a b
proof(induct)
  case (ms1 e1 Es1)
  show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
next
  case (ms2 e1 Es1 e2 Es2 e2' Es2')
  have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
  have "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
  then have d3: "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
  have d2: "<e1, Es1> \<mapsto> <e2, Es2>" by fact
  show "<e1, Es1> \<mapsto>* <e3, Es3>" 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 rearrange 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: "<e1, Es1> \<mapsto>* <e2, Es2>" 
  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
using a b
proof(induct)
  case (ms1 e1 Es1)
  show "<e1, Es1> \<mapsto>* <e3, Es3>" by fact
next
  case (ms2 e1 Es1 e2 Es2 e2' Es2')
  have ih: "<e2', Es2'> \<mapsto>* <e3, Es3> \<Longrightarrow> <e2, Es2> \<mapsto>* <e3, Es3>" by fact
  have "<e2', Es2'> \<mapsto>* <e3, Es3>" by fact
  then have "<e2, Es2> \<mapsto>* <e3, Es3>" using ih by simp
  moreover
  have "<e1, Es1> \<mapsto> <e2, Es2>" by fact
  ultimately show "<e1, Es1> \<mapsto>* <e3, Es3>" 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 \<Down> t"
using a by (induct) (auto)

lemma 
  assumes a: "t \<Down> t'"
  shows "val t'"
using a by (induct) (auto)

lemma
  assumes a: "<e1, Es1> \<mapsto>* <e2, Es2>" 
  and     b: "<e2, Es2> \<mapsto>* <e3, Es3>"
  shows "<e1, Es1> \<mapsto>* <e3, Es3>"
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 \<Down> t'"
  shows "<t, []> \<mapsto>* <t', []>"
using a 
proof (induct)
  case (e_Lam x t) 
  -- {* no assumptions *}
  show "<Lam [x].t, []> \<mapsto>* <Lam [x].t, []>" by auto
next
  case (e_App t1 x t t2 v' v) 
  -- {* all assumptions in this case *}
  have a1: "t1 \<Down> Lam [x].t" by fact
  have ih1: "<t1, []> \<mapsto>* <Lam [x].t, []>" by fact
  have a2: "t2 \<Down> v'" by fact
  have ih2: "<t2, []> \<mapsto>* <v', []>" by fact
  have a3: "t[x::=v'] \<Down> v" by fact
  have ih3: "<t[x::=v'], []> \<mapsto>* <v, []>" by fact

  -- {* your reasoning *}
  show "<App t1 t2, []> \<mapsto>* <v, []>" sorry
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 \<Down> t'"
  shows "<t, Es> \<mapsto>* <t', Es>"
using a
by (induct arbitrary: Es)
   (metis eval_to_val machine.intros ms1 ms2 ms3 v_Lam)+

corollary eval_implies_machines:
  assumes a: "t \<Down> t'"
  shows "<t, []> \<mapsto>* <t', []>"
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 \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100, 100] 100)
where
  "\<box>\<lbrakk>t\<rbrakk> = t"
| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"


text {* 
  After this definition Isabelle will be able to simplify
  statements like: 
*}

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

fun 
 ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" (infixr "\<odot>" 99)
where
  "\<box> \<odot> E' = E'"
| "(CAppL E t') \<odot> E' = CAppL (E \<odot> E') t'"
| "(CAppR t' E) \<odot> E' = CAppR t' (E \<odot> E')"

fun
  ctx_composes :: "ctxs \<Rightarrow> ctx" ("_\<down>" [110] 110)
where
    "[]\<down> = \<box>"
  | "(E # Es)\<down> = (Es\<down>) \<odot> E"

text {*  
  Notice that we not just have given a pretty syntax for the functions, but
  also some precedences. The numbers inside the [\<dots>] 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 \<odot> Es2) \<odot> Es3 otherwise Es1 \<odot> Es2 \<odot> Es3 is
  interpreted as Es1 \<odot> (Es2 \<odot> 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 ctx_compose:
  shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
proof (induct E1)
  case Hole
  show "(\<box> \<odot> E2)\<lbrakk>t\<rbrakk> = \<box>\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
next
  case (CAppL E1 t')
  have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
  show "((CAppL E1 t') \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppL E1 t')\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" sorry
next
  case (CAppR t' E1)
  have ih: "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" by fact
  show "((CAppR t' E1) \<odot> E2)\<lbrakk>t\<rbrakk> = (CAppR t' E1)\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>" 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 \<odot> \<box> = E"
by (induct E) (simp_all)

lemma compose_assoc:  
  shows "(E1 \<odot> E2) \<odot> E3 = E1 \<odot> (E2 \<odot> E3)"
by (induct E1) (simp_all)

lemma
  shows "(Es1 @ Es2)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
proof (induct Es1)
  case Nil
  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" sorry
next
  case (Cons E Es1)
  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact

  show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" sorry
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)\<down> = (Es2\<down>) \<odot> (Es1\<down>)"
proof (induct Es1)
  case Nil
  show "([] @ Es2)\<down> = Es2\<down> \<odot> []\<down>" using neut_hole by simp
next
  case (Cons E Es1)
  have ih: "(Es1 @ Es2)\<down> = Es2\<down> \<odot> Es1\<down>" by fact
  have "((E # Es1) @ Es2)\<down> = (E # (Es1 @ Es2))\<down>" by simp
  also have "\<dots> = (Es1 @ Es2)\<down> \<odot> E" by simp
  also have "\<dots> = (Es2\<down> \<odot> Es1\<down>) \<odot> E" using ih by simp
  also have "\<dots> = Es2\<down> \<odot> (Es1\<down> \<odot> E)" using compose_assoc by simp
  also have "\<dots> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
  finally show "((E # Es1) @ Es2)\<down> = Es2\<down> \<odot> (E # Es1)\<down>" by simp
qed


end
author	Christian Urban <urbanc@in.tum.de>
	Thu, 24 Feb 2011 16:26:11 +0000 (2011-02-24)
changeset 2730	eebc24b9cf39
parent 2706	8ae1c2e6369e
child 3132	87eca760dcba
permissions	-rw-r--r--