--- a/Tutorial/Tutorial3.thy Fri Jan 21 22:02:34 2011 +0100
+++ b/Tutorial/Tutorial3.thy Fri Jan 21 22:23:44 2011 +0100
@@ -6,12 +6,12 @@
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 is some sequent
- or reasoning steps enclosed in curly braces
+ 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
@@ -25,7 +25,7 @@
Where "C" is the last have-statement in this block. The behaviour
of such a block to the 'outside' is the implication
- \<lbrakk>A; B\<rbrakk> \<Longrightarrow> "C"
+ 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:
@@ -52,17 +52,12 @@
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 is
- true, then we have 'ultimately' established the property "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"
*}
-section {* EXERCISE 7 *}
-
-text {*
- Fill in the cases 1.2 and 1.3 and the equational reasoning
- in the lambda-case.
-*}
+subsection {* Two preliminary facts *}
lemma forget:
shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
@@ -78,6 +73,14 @@
(auto simp add: lam.fresh fresh_at_base)
+
+section {* EXERCISE 7 *}
+
+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"
@@ -111,12 +114,12 @@
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 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+
+ 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")
+ 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
@@ -130,7 +133,7 @@
text {*
Again the strong induction principle enables Isabelle to find
- the proof of the substitution lemma automatically.
+ the proof of the substitution lemma completely automatically.
*}
lemma substitution_lemma_version:
--- a/Tutorial/Tutorial4.thy Fri Jan 21 22:02:34 2011 +0100
+++ b/Tutorial/Tutorial4.thy Fri Jan 21 22:23:44 2011 +0100
@@ -1,5 +1,6 @@
+
theory Tutorial4
-imports Tutorial1 Tutorial2
+imports Tutorial1 Tutorial2 Tutorial3
begin
section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -163,6 +164,7 @@
shows "t \<Down> t"
using a by (induct) (auto)
+
lemma e_App_elim:
assumes a: "App t1 t2 \<Down> v"
obtains x t v' where "t1 \<Down> Lam [x].t" "t2 \<Down> v'" "t[x::=v'] \<Down> v"
@@ -234,137 +236,8 @@
then show "t1 \<Down> t2" using b cbvs_implies_eval by simp
qed
-lemma valid_elim:
- assumes a: "valid ((x, T) # \<Gamma>)"
- shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"
-using a by (cases) (auto)
-
-lemma valid_insert:
- assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
- shows "valid (\<Delta> @ \<Gamma>)"
-using a
-by (induct \<Delta>)
- (auto simp add: fresh_append fresh_Cons dest!: valid_elim)
-
-lemma fresh_list:
- shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"
-by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
-
-lemma context_unique:
- assumes a1: "valid \<Gamma>"
- and a2: "(x, T) \<in> set \<Gamma>"
- and a3: "(x, U) \<in> set \<Gamma>"
- shows "T = U"
-using a1 a2 a3
-by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
-
-lemma type_substitution_aux:
- assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
- and b: "\<Gamma> \<turnstile> e' : T'"
- shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T"
-using a b
-proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
- case (t_Var y T x e' \<Delta>)
- have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
- have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
- have a3: "\<Gamma> \<turnstile> e' : T'" by fact
- from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
- { assume eq: "x = y"
- from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
- with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)
- }
- moreover
- { assume ineq: "x \<noteq> y"
- from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
- then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto
- }
- ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
-qed (force simp add: fresh_append fresh_Cons)+
-
-corollary type_substitution:
- assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
- and b: "\<Gamma> \<turnstile> e' : T'"
- shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
-using a b type_substitution_aux[where \<Delta>="[]"]
-by auto
-
-lemma t_App_elim:
- assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
- obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
-using a
-by (cases) (auto simp add: lam.eq_iff lam.distinct)
-text {* we have not yet generated strong elimination rules *}
-lemma t_Lam_elim:
- assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T"
- and fc: "atom x \<sharp> \<Gamma>"
- obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
-using ty fc
-apply(cases)
-apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
-apply(auto simp add: Abs1_eq_iff)
-apply(rotate_tac 3)
-apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
-apply(perm_simp)
-apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
-done
-theorem cbv_type_preservation:
- assumes a: "t \<longrightarrow>cbv t'"
- and b: "\<Gamma> \<turnstile> t : T"
- shows "\<Gamma> \<turnstile> t' : T"
-using a b
-by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
- (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
-
-corollary cbvs_type_preservation:
- assumes a: "t \<longrightarrow>cbv* t'"
- and b: "\<Gamma> \<turnstile> t : T"
- shows "\<Gamma> \<turnstile> t' : T"
-using a b
-by (induct) (auto intro: cbv_type_preservation)
-
-text {*
- The type-preservation property for the machine and
- evaluation relation.
-*}
-
-theorem machine_type_preservation:
- assumes a: "<t, []> \<mapsto>* <t', []>"
- and b: "\<Gamma> \<turnstile> t : T"
- shows "\<Gamma> \<turnstile> t' : T"
-proof -
- have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
- then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp
-qed
-
-theorem eval_type_preservation:
- assumes a: "t \<Down> t'"
- and b: "\<Gamma> \<turnstile> t : T"
- shows "\<Gamma> \<turnstile> t' : T"
-proof -
- have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
- then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp
-qed
-
-text {* The Progress Property *}
-
-lemma canonical_tArr:
- assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
- and b: "val t"
- obtains x t' where "t = Lam [x].t'"
-using b a by (induct) (auto)
-
-theorem progress:
- assumes a: "[] \<turnstile> t : T"
- shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
-using a
-by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
- (auto elim: canonical_tArr)
-
-text {*
- Done!
-*}
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Tutorial/Tutorial5.thy Fri Jan 21 22:23:44 2011 +0100
@@ -0,0 +1,142 @@
+theory Tutorial5
+imports Tutorial4
+begin
+
+
+section {* Type Preservation (fixme separate file) *}
+
+
+lemma valid_elim:
+ assumes a: "valid ((x, T) # \<Gamma>)"
+ shows "atom x \<sharp> \<Gamma> \<and> valid \<Gamma>"
+using a by (cases) (auto)
+
+lemma valid_insert:
+ assumes a: "valid (\<Delta> @ [(x, T)] @ \<Gamma>)"
+ shows "valid (\<Delta> @ \<Gamma>)"
+using a
+by (induct \<Delta>)
+ (auto simp add: fresh_append fresh_Cons dest!: valid_elim)
+
+lemma fresh_list:
+ shows "atom y \<sharp> xs = (\<forall>x \<in> set xs. atom y \<sharp> x)"
+by (induct xs) (simp_all add: fresh_Nil fresh_Cons)
+
+lemma context_unique:
+ assumes a1: "valid \<Gamma>"
+ and a2: "(x, T) \<in> set \<Gamma>"
+ and a3: "(x, U) \<in> set \<Gamma>"
+ shows "T = U"
+using a1 a2 a3
+by (induct) (auto simp add: fresh_list fresh_Pair fresh_at_base)
+
+lemma type_substitution_aux:
+ assumes a: "\<Delta> @ [(x, T')] @ \<Gamma> \<turnstile> e : T"
+ and b: "\<Gamma> \<turnstile> e' : T'"
+ shows "\<Delta> @ \<Gamma> \<turnstile> e[x ::= e'] : T"
+using a b
+proof (nominal_induct \<Gamma>'\<equiv>"\<Delta> @ [(x, T')] @ \<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
+ case (t_Var y T x e' \<Delta>)
+ have a1: "valid (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
+ have a2: "(y,T) \<in> set (\<Delta> @ [(x, T')] @ \<Gamma>)" by fact
+ have a3: "\<Gamma> \<turnstile> e' : T'" by fact
+ from a1 have a4: "valid (\<Delta> @ \<Gamma>)" by (rule valid_insert)
+ { assume eq: "x = y"
+ from a1 a2 have "T = T'" using eq by (auto intro: context_unique)
+ with a3 have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using eq a4 by (auto intro: weakening)
+ }
+ moreover
+ { assume ineq: "x \<noteq> y"
+ from a2 have "(y, T) \<in> set (\<Delta> @ \<Gamma>)" using ineq by simp
+ then have "\<Delta> @ \<Gamma> \<turnstile> Var y[x ::= e'] : T" using ineq a4 by auto
+ }
+ ultimately show "\<Delta> @ \<Gamma> \<turnstile> Var y[x::=e'] : T" by blast
+qed (force simp add: fresh_append fresh_Cons)+
+
+corollary type_substitution:
+ assumes a: "(x, T') # \<Gamma> \<turnstile> e : T"
+ and b: "\<Gamma> \<turnstile> e' : T'"
+ shows "\<Gamma> \<turnstile> e[x ::= e'] : T"
+using a b type_substitution_aux[where \<Delta>="[]"]
+by auto
+
+lemma t_App_elim:
+ assumes a: "\<Gamma> \<turnstile> App t1 t2 : T"
+ obtains T' where "\<Gamma> \<turnstile> t1 : T' \<rightarrow> T" "\<Gamma> \<turnstile> t2 : T'"
+using a
+by (cases) (auto simp add: lam.eq_iff lam.distinct)
+
+text {* we have not yet generated strong elimination rules *}
+lemma t_Lam_elim:
+ assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T"
+ and fc: "atom x \<sharp> \<Gamma>"
+ obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
+using ty fc
+apply(cases)
+apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
+apply(auto simp add: Abs1_eq_iff)
+apply(rotate_tac 3)
+apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
+apply(perm_simp)
+apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
+done
+
+theorem cbv_type_preservation:
+ assumes a: "t \<longrightarrow>cbv t'"
+ and b: "\<Gamma> \<turnstile> t : T"
+ shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (nominal_induct avoiding: \<Gamma> T rule: cbv.strong_induct)
+ (auto elim!: t_Lam_elim t_App_elim simp add: type_substitution ty.eq_iff)
+
+corollary cbvs_type_preservation:
+ assumes a: "t \<longrightarrow>cbv* t'"
+ and b: "\<Gamma> \<turnstile> t : T"
+ shows "\<Gamma> \<turnstile> t' : T"
+using a b
+by (induct) (auto intro: cbv_type_preservation)
+
+text {*
+ The type-preservation property for the machine and
+ evaluation relation.
+*}
+
+theorem machine_type_preservation:
+ assumes a: "<t, []> \<mapsto>* <t', []>"
+ and b: "\<Gamma> \<turnstile> t : T"
+ shows "\<Gamma> \<turnstile> t' : T"
+proof -
+ have "t \<longrightarrow>cbv* t'" using a machines_implies_cbvs by simp
+ then show "\<Gamma> \<turnstile> t' : T" using b cbvs_type_preservation by simp
+qed
+
+theorem eval_type_preservation:
+ assumes a: "t \<Down> t'"
+ and b: "\<Gamma> \<turnstile> t : T"
+ shows "\<Gamma> \<turnstile> t' : T"
+proof -
+ have "<t, []> \<mapsto>* <t', []>" using a eval_implies_machines by simp
+ then show "\<Gamma> \<turnstile> t' : T" using b machine_type_preservation by simp
+qed
+
+text {* The Progress Property *}
+
+lemma canonical_tArr:
+ assumes a: "[] \<turnstile> t : T1 \<rightarrow> T2"
+ and b: "val t"
+ obtains x t' where "t = Lam [x].t'"
+using b a by (induct) (auto)
+
+theorem progress:
+ assumes a: "[] \<turnstile> t : T"
+ shows "(\<exists>t'. t \<longrightarrow>cbv t') \<or> (val t)"
+using a
+by (induct \<Gamma>\<equiv>"[]::ty_ctx" t T)
+ (auto elim: canonical_tArr)
+
+text {*
+ Done! Congratulations!
+*}
+
+end
+