equal
deleted
inserted
replaced
3 begin |
3 begin |
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 The substitution lemma is another theorem where the variable |
9 One way to do this in Isar is to use blocks. A block consist of some |
9 convention plays a crucial role. |
10 assumptions and reasoning steps enclosed in curly braces, like |
10 |
|
11 Barendregt's proof of this lemma needs in the variable case a |
|
12 case distinction. One way to do this in Isar is to use blocks. |
|
13 A block consist of some assumptions and reasoning steps |
|
14 enclosed in curly braces, like |
11 |
15 |
12 { \<dots> |
16 { \<dots> |
13 have "statement" |
17 have "statement" |
14 have "last_statement_in_the_block" |
18 have "last_statement_in_the_block" |
15 } |
19 } |
16 |
20 |
17 Such a block can contain local assumptions like |
21 Such a block may contain local assumptions like |
18 |
22 |
19 { assume "A" |
23 { assume "A" |
20 assume "B" |
24 assume "B" |
21 \<dots> |
25 \<dots> |
22 have "C" by \<dots> |
26 have "C" by \<dots> |
72 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
76 by (nominal_induct t avoiding: z y s rule: lam.strong_induct) |
73 (auto simp add: lam.fresh fresh_at_base) |
77 (auto simp add: lam.fresh fresh_at_base) |
74 |
78 |
75 |
79 |
76 |
80 |
77 section {* EXERCISE 7 *} |
81 section {* EXERCISE 10 *} |
78 |
82 |
79 text {* |
83 text {* |
80 Fill in the cases 1.2 and 1.3 and the equational reasoning |
84 Fill in the cases 1.2 and 1.3 and the equational reasoning |
81 in the lambda-case. |
85 in the lambda-case. |
82 *} |
86 *} |
141 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
145 shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
142 using asm |
146 using asm |
143 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) |
147 by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) |
144 (auto simp add: fresh_fact forget) |
148 (auto simp add: fresh_fact forget) |
145 |
149 |
|
150 subsection {* MINI EXERCISE *} |
|
151 |
|
152 text {* |
|
153 Compare and contrast Barendregt's reasoning and the |
|
154 formalised proofs. |
|
155 *} |
146 |
156 |
147 end |
157 end |