--- a/Tutorial/Tutorial3.thy Sat Dec 17 16:58:11 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,157 +0,0 @@
-theory Tutorial3
-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
-
- { \<dots>
- have "statement"
- have "last_statement_in_the_block"
- }
-
- Such a block may contain local assumptions like
-
- { assume "A"
- assume "B"
- \<dots>
- have "C" by \<dots>
- }
-
- Where "C" is the last have-statement in this block. The behaviour
- of such a block to the 'outside' is the implication
-
- A \<Longrightarrow> B \<Longrightarrow> 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"
- \<dots>
- have "smth"
- }
- moreover
- { assume "P2"
- \<dots>
- have "smth"
- }
- moreover
- { assume "P3"
- \<dots>
- have "smth"
- }
- ultimately have "smth" by blast
-
- The blocks establish the implications
-
- P1 \<Longrightarrow> smth
- P2 \<Longrightarrow> smth
- P3 \<Longrightarrow> smth
-
- If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3
- holds, then we have 'ultimately' established the property "smth"
-
-*}
-
-subsection {* Two preliminary facts *}
-
-lemma forget:
- shows "atom x \<sharp> t \<Longrightarrow> 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 \<sharp> s"
- and b: "z = y \<or> atom z \<sharp> t"
- shows "atom z \<sharp> 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 \<noteq> y"
- and b: "atom x \<sharp> 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 \<noteq> y" by fact
- have a2: "atom x \<sharp> 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 \<noteq> x"
-
- have "?LHS = ?RHS" sorry
- }
- moreover
- { -- {* Case 1.3 *}
- assume c3: "z \<noteq> x" "z \<noteq> y"
-
- have "?LHS = ?RHS" sorry
- }
- ultimately show "?LHS = ?RHS" by blast
- qed
-next
- case (Lam z M1) -- {* case 2: lambdas *}
- 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
- have a1: "x \<noteq> y" by fact
- have a2: "atom x \<sharp> L" by fact
- have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+ -- {* !! *}
- then have b: "atom z \<sharp> 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 = \<dots>" sorry
-
- also have "\<dots> = ?RHS" sorry
- 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 \<noteq> y" "atom x \<sharp> 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