1 

     2 theory Tutorial3s

     3 imports Lambda

     4 begin

     5 

     6 section {* Formalising Barendregt's Proof of the Substitution Lemma *}

     7 

     8 text {*

     9   The substitution lemma is another theorem where the variable

    10   convention plays a crucial role.

    11 

    12   Barendregt's proof of this lemma needs in the variable case a 

    13   case distinction. One way to do this in Isar is to use blocks. 

    14   A block consist of some assumptions and reasoning steps 

    15   enclosed in curly braces, like

    16 

    17   { \<dots>

    18     have "statement"

    19     have "last_statement_in_the_block"

    20   }

    21 

    22   Such a block may contain local assumptions like

    23 

    24   { assume "A"

    25     assume "B"

    26     \<dots>

    27     have "C" by \<dots>

    28   }

    29 

    30   Where "C" is the last have-statement in this block. The behaviour 

    31   of such a block to the 'outside' is the implication

    32 

    33    A \<Longrightarrow> B \<Longrightarrow> C 

    34 

    35   Now if we want to prove a property "smth" using the case-distinctions

    36   P1, P2 and P3 then we can use the following reasoning:

    37 

    38     { assume "P1"

    39       \<dots>

    40       have "smth"

    41     }

    42     moreover

    43     { assume "P2"

    44       \<dots>

    45       have "smth"

    46     }

    47     moreover

    48     { assume "P3"

    49       \<dots>

    50       have "smth"

    51     }

    52     ultimately have "smth" by blast

    53 

    54   The blocks establish the implications

    55 

    56     P1 \<Longrightarrow> smth

    57     P2 \<Longrightarrow> smth

    58     P3 \<Longrightarrow> smth

    59 

    60   If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 

    61   holds, then we have 'ultimately' established the property "smth" 

    62   

    63 *}

    64 

    65 subsection {* Two preliminary facts *}

    66 

    67 lemma forget:

    68   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"

    69 by (nominal_induct t avoiding: x s rule: lam.strong_induct)

    70    (auto simp add: lam.fresh fresh_at_base)

    71 

    72 lemma fresh_fact:

    73   assumes a: "atom z \<sharp> s"

    74   and b: "z = y \<or> atom z \<sharp> t"

    75   shows "atom z \<sharp> t[y ::= s]"

    76 using a b

    77 by (nominal_induct t avoiding: z y s rule: lam.strong_induct)

    78    (auto simp add: lam.fresh fresh_at_base)

    79 

    80 

    81 

    82 section {* EXERCISE 10 *}

    83 

    84 text {*

    85   Fill in the cases 1.2 and 1.3 and the equational reasoning 

    86   in the lambda-case.

    87 *}

    88 

    89 lemma 

    90   assumes a: "x \<noteq> y"

    91   and     b: "atom x \<sharp> L"

    92   shows "M[x ::= N][y ::= L] = M[y ::= L][x ::= N[y ::= L]]"

    93 using a b

    94 proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

    95   case (Var z)

    96   have a1: "x \<noteq> y" by fact

    97   have a2: "atom x \<sharp> L" by fact

    98   show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS")

    99   proof -

   100     { -- {* Case 1.1 *}

   101       assume c1: "z = x"

   102       have "(1)": "?LHS = N[y::=L]" using c1 by simp

   103       have "(2)": "?RHS = N[y::=L]" using c1 a1 by simp

   104       have "?LHS = ?RHS" using "(1)" "(2)" by simp

   105     }

   106     moreover 

   107     { -- {* Case 1.2 *}

   108       assume c2: "z = y" "z \<noteq> x" 

   109       have "(1)": "?LHS = L" using c2 by simp

   110       have "(2)": "?RHS = L[x::=N[y::=L]]" using c2 by simp

   111       have "(3)": "L[x::=N[y::=L]] = L" using a2 forget by simp

   112       have "?LHS = ?RHS" using "(1)" "(2)" "(3)" by simp

   113     }

   114     moreover 

   115     { -- {* Case 1.3 *}

   116       assume c3: "z \<noteq> x" "z \<noteq> y"

   117       have "(1)": "?LHS = Var z" using c3 by simp

   118       have "(2)": "?RHS = Var z" using c3 by simp

   119       have "?LHS = ?RHS" using "(1)" "(2)" by simp

   120     }

   121     ultimately show "?LHS = ?RHS" by blast

   122   qed

   123 next

   124   case (Lam z M1) -- {* case 2: lambdas *}

   125   have ih: "\<lbrakk>x \<noteq> y; atom x \<sharp> L\<rbrakk> \<Longrightarrow> M1[x ::= N][y ::= L] = M1[y ::= L][x ::= N[y ::= L]]" by fact

   126   have a1: "x \<noteq> y" by fact

   127   have a2: "atom x \<sharp> L" by fact

   128   have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+   -- {* !! *}

   129   then have b: "atom z \<sharp> N[y::=L]" by (simp add: fresh_fact)

   130   show "(Lam [z].M1)[x ::= N][y ::= L] = (Lam [z].M1)[y ::= L][x ::= N[y ::= L]]" (is "?LHS=?RHS") 

   131   proof - 

   132     have "?LHS = Lam [z].(M1[x ::= N][y ::= L])" using fs by simp

   133     also have "\<dots> = Lam [z].(M1[y ::= L][x ::= N[y ::= L]])" using ih a1 a2 by simp

   134     also have "\<dots> = (Lam [z].(M1[y ::= L]))[x ::= N[y ::= L]]" using b fs by simp

   135     also have "\<dots> = ?RHS" using fs by simp

   136     finally show "?LHS = ?RHS" by simp

   137   qed

   138 next

   139   case (App M1 M2) -- {* case 3: applications *}

   140   then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp

   141 qed

   142 

   143 text {* 

   144   Again the strong induction principle enables Isabelle to find

   145   the proof of the substitution lemma completely automatically. 

   146 *}

   147 

   148 lemma substitution_lemma_version:  

   149   assumes asm: "x \<noteq> y" "atom x \<sharp> L"

   150   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"

   151   using asm 

   152 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)

   153    (auto simp add: fresh_fact forget)

   154 

   155 subsection {* MINI EXERCISE *}

   156 

   157 text {*

   158   Compare and contrast Barendregt's reasoning and the 

   159   formalised proofs.

   160 *}

   161 

   162 end