--- a/Tutorial/Tutorial3.thy Sun Jan 23 07:32:28 2011 +0900
+++ b/Tutorial/Tutorial3.thy Sat Jan 22 16:37:00 2011 -0600
@@ -5,16 +5,20 @@
section {* Formalising Barendregt's Proof of the Substitution Lemma *}
text {*
- Barendregt's proof 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
+ 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 can contain local assumptions like
+ Such a block may contain local assumptions like
{ assume "A"
assume "B"
@@ -74,7 +78,7 @@
-section {* EXERCISE 7 *}
+section {* EXERCISE 10 *}
text {*
Fill in the cases 1.2 and 1.3 and the equational reasoning
@@ -143,5 +147,11 @@
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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial3s.thy Sat Jan 22 16:37:00 2011 -0600
@@ -0,0 +1,162 @@
+
+theory Tutorial3s
+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 "(1)": "?LHS = L" using c2 by simp
+ have "(2)": "?RHS = L[x::=N[y::=L]]" using c2 by simp
+ have "(3)": "L[x::=N[y::=L]] = L" using a2 forget by simp
+ have "?LHS = ?RHS" using "(1)" "(2)" "(3)" by simp
+ }
+ moreover
+ { -- {* Case 1.3 *}
+ assume c3: "z \<noteq> x" "z \<noteq> y"
+ have "(1)": "?LHS = Var z" using c3 by simp
+ have "(2)": "?RHS = Var z" using c3 by simp
+ have "?LHS = ?RHS" using "(1)" "(2)" by simp
+ }
+ 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 = Lam [z].(M1[x ::= N][y ::= L])" using fs by simp
+ also have "\<dots> = Lam [z].(M1[y ::= L][x ::= N[y ::= L]])" using ih a1 a2 by simp
+ also have "\<dots> = (Lam [z].(M1[y ::= L]))[x ::= N[y ::= L]]" using b fs by simp
+ also have "\<dots> = ?RHS" using fs by simp
+ 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