equal
deleted
inserted
replaced
4 |
4 |
5 section {* Formalising Barendregt's Proof of the Substitution Lemma *} |
5 section {* Formalising Barendregt's Proof of the Substitution Lemma *} |
6 |
6 |
7 text {* |
7 text {* |
8 Barendregt's proof needs in the variable case a case distinction. |
8 Barendregt's proof needs in the variable case a case distinction. |
9 One way to do this in Isar is to use blocks. A block is some sequent |
9 One way to do this in Isar is to use blocks. A block consist of some |
10 or reasoning steps enclosed in curly braces |
10 assumptions and reasoning steps enclosed in curly braces, like |
11 |
11 |
12 { \<dots> |
12 { \<dots> |
13 |
|
14 have "statement" |
13 have "statement" |
|
14 have "last_statement_in_the_block" |
15 } |
15 } |
16 |
16 |
17 Such a block can contain local assumptions like |
17 Such a block can contain local assumptions like |
18 |
18 |
19 { assume "A" |
19 { assume "A" |
23 } |
23 } |
24 |
24 |
25 Where "C" is the last have-statement in this block. The behaviour |
25 Where "C" is the last have-statement in this block. The behaviour |
26 of such a block to the 'outside' is the implication |
26 of such a block to the 'outside' is the implication |
27 |
27 |
28 \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C" |
28 A \<Longrightarrow> B \<Longrightarrow> C |
29 |
29 |
30 Now if we want to prove a property "smth" using the case-distinctions |
30 Now if we want to prove a property "smth" using the case-distinctions |
31 P1, P2 and P3 then we can use the following reasoning: |
31 P1, P2 and P3 then we can use the following reasoning: |
32 |
32 |
33 { assume "P1" |
33 { assume "P1" |
50 |
50 |
51 P1 \<Longrightarrow> smth |
51 P1 \<Longrightarrow> smth |
52 P2 \<Longrightarrow> smth |
52 P2 \<Longrightarrow> smth |
53 P3 \<Longrightarrow> smth |
53 P3 \<Longrightarrow> smth |
54 |
54 |
55 If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 is |
55 If we know that P1, P2 and P3 cover all the cases, that is P1 \<or> P2 \<or> P3 |
56 true, then we have 'ultimately' established the property "smth" |
56 holds, then we have 'ultimately' established the property "smth" |
57 |
57 |
58 *} |
58 *} |
59 |
59 |
60 section {* EXERCISE 7 *} |
60 subsection {* Two preliminary facts *} |
61 |
|
62 text {* |
|
63 Fill in the cases 1.2 and 1.3 and the equational reasoning |
|
64 in the lambda-case. |
|
65 *} |
|
66 |
61 |
67 lemma forget: |
62 lemma forget: |
68 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
63 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
69 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
64 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
70 (auto simp add: lam.fresh fresh_at_base) |
65 (auto simp add: lam.fresh fresh_at_base) |
75 shows "atom z \<sharp> t[y ::= s]" |
70 shows "atom z \<sharp> t[y ::= s]" |
76 using a b |
71 using a b |
77 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
72 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
78 (auto simp add: lam.fresh fresh_at_base) |
73 (auto simp add: lam.fresh fresh_at_base) |
79 |
74 |
|
75 |
|
76 |
|
77 section {* EXERCISE 7 *} |
|
78 |
|
79 text {* |
|
80 Fill in the cases 1.2 and 1.3 and the equational reasoning |
|
81 in the lambda-case. |
|
82 *} |
80 |
83 |
81 lemma |
84 lemma |
82 assumes a: "x \<noteq> y" |
85 assumes a: "x \<noteq> y" |
83 and b: "atom x \<sharp> L" |
86 and b: "atom x \<sharp> L" |
84 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
87 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
109 } |
112 } |
110 ultimately show "?LHS = ?RHS" by blast |
113 ultimately show "?LHS = ?RHS" by blast |
111 qed |
114 qed |
112 next |
115 next |
113 case (Lam z M1) -- {* case 2: lambdas *} |
116 case (Lam z M1) -- {* case 2: lambdas *} |
114 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 |
117 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 |
115 have a1: "x \<noteq> y" by fact |
118 have a1: "x \<noteq> y" by fact |
116 have a2: "atom x \<sharp> L" by fact |
119 have a2: "atom x \<sharp> L" by fact |
117 have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+ |
120 have fs: "atom z \<sharp> x" "atom z \<sharp> y" "atom z \<sharp> N" "atom z \<sharp> L" by fact+ -- {* !! *} |
118 then have b: "atom z \<sharp> N[y::=L]" by (simp add: fresh_fact) |
121 then have b: "atom z \<sharp> N[y::=L]" by (simp add: fresh_fact) |
119 show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") |
122 show "(Lam [z].M1)[x ::= N][y ::= L] = (Lam [z].M1)[y ::= L][x ::= N[y ::= L]]" (is "?LHS=?RHS") |
120 proof - |
123 proof - |
121 have "?LHS = \<dots>" sorry |
124 have "?LHS = \<dots>" sorry |
122 |
125 |
123 also have "\<dots> = ?RHS" sorry |
126 also have "\<dots> = ?RHS" sorry |
124 finally show "?LHS = ?RHS" by simp |
127 finally show "?LHS = ?RHS" by simp |
128 then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp |
131 then show "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp |
129 qed |
132 qed |
130 |
133 |
131 text {* |
134 text {* |
132 Again the strong induction principle enables Isabelle to find |
135 Again the strong induction principle enables Isabelle to find |
133 the proof of the substitution lemma automatically. |
136 the proof of the substitution lemma completely automatically. |
134 *} |
137 *} |
135 |
138 |
136 lemma substitution_lemma_version: |
139 lemma substitution_lemma_version: |
137 assumes asm: "x \<noteq> y" "atom x \<sharp> L" |
140 assumes asm: "x \<noteq> y" "atom x \<sharp> L" |
138 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
141 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |