--- a/IsaMakefile Wed Feb 29 17:14:31 2012 +0000
+++ b/IsaMakefile Mon Mar 05 16:27:28 2012 +0000
@@ -29,6 +29,7 @@
$(LOG)/HOL-Nominal2-tests.gz: Nominal/ROOT.ML Nominal/*.thy
@$(USEDIR) HOL Nominal
+ @$(USEDIR) HOL Tutorial
## ESOP Paper
--- a/Tutorial/Lambda.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Lambda.thy Mon Mar 05 16:27:28 2012 +0000
@@ -15,7 +15,7 @@
nominal_datatype lam =
Var "name"
| App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
text {* some automatically derived theorems *}
@@ -38,43 +38,17 @@
"height (Var x) = 1"
| "height (App t1 t2) = max (height t1) (height t2) + 1"
| "height (Lam [x].t) = height t + 1"
-apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)")
-unfolding eqvt_def
-apply(rule allI)
-apply(simp add: permute_fun_def)
-apply(rule ext)
-apply(rule ext)
-apply(simp add: permute_bool_def)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp)
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply(simp)
-apply(erule height_graph.induct)
-apply(perm_simp)
-apply(rule height_graph.intros)
-apply(perm_simp)
-apply(rule height_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(perm_simp)
-apply(rule height_graph.intros)
-apply(assumption)
+apply(simp add: eqvt_def height_graph_def)
+apply (rule, perm_simp, rule)
+apply(rule TrueI)
apply(rule_tac y="x" in lam.exhaust)
-apply(auto simp add: lam.distinct lam.eq_iff)
-apply(simp add: Abs_eq_iff alphas)
-apply(clarify)
-apply(subst (4) supp_perm_eq[where p="p", symmetric])
-apply(simp add: pure_supp fresh_star_def)
-apply(simp add: eqvt_at_def)
+apply(auto)
+apply(erule_tac c="()" in Abs_lst1_fcb2)
+apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
done
-termination
- by (relation "measure size") (simp_all add: lam.size)
+termination (eqvt)
+ by lexicographic_order
subsection {* Capture-Avoiding Substitution *}
@@ -85,78 +59,22 @@
"(Var x)[y ::= s] = (if x = y then s else (Var x))"
| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
-apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
-unfolding eqvt_def
-apply(rule allI)
-apply(simp add: permute_fun_def)
-apply(rule ext)
-apply(rule ext)
-apply(simp add: permute_bool_def)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp)
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply(simp)
-apply(erule subst_graph.induct)
-apply(perm_simp)
-apply(rule subst_graph.intros)
-apply(perm_simp)
-apply(rule subst_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_graph.intros)
-apply(simp add: fresh_Pair)
-apply(assumption)
-apply(auto simp add: lam.distinct lam.eq_iff)
-apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
-apply(blast)+
-apply(simp add: fresh_star_def)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta")
-apply(subst (asm) Abs_eq_iff2)
-apply(simp add: alphas atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_perm_set_conv)
-apply(simp add: finite_supp)
-apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp (no_asm) add: fresh_star_def)
-apply(rule conjI)
-apply(simp (no_asm) add: Abs_fresh_iff)
-apply(clarify)
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff)
-apply(simp)
-apply(simp add: Abs_fresh_iff)
-apply(subgoal_tac "p \<bullet> ya = ya")
-apply(subgoal_tac "p \<bullet> sa = sa")
-apply(simp add: atom_eqvt eqvt_at_def)
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule conjI)
-apply(simp add: Abs_fresh_iff)
-apply(drule sym)
-apply(simp add: Abs_fresh_iff)
+ unfolding eqvt_def subst_graph_def
+ apply(rule, perm_simp, rule)
+ apply(rule TrueI)
+ apply(auto)
+ apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+ apply(blast)+
+ apply(simp_all add: fresh_star_def fresh_Pair_elim)
+ apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+ apply(simp_all add: Abs_fresh_iff)
+ apply(simp add: fresh_star_def fresh_Pair)
+ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+ apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
done
-termination
- by (relation "measure (\<lambda>(t, _, _). size t)")
- (simp_all add: lam.size)
-
-lemma subst_eqvt[eqvt]:
- shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]"
-by (induct t x s rule: subst.induct) (simp_all)
+termination (eqvt)
+ by lexicographic_order
lemma fresh_fact:
assumes a: "atom z \<sharp> s"
--- a/Tutorial/Minimal.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Minimal.thy Mon Mar 05 16:27:28 2012 +0000
@@ -7,7 +7,7 @@
nominal_datatype lam =
Var "name"
| App "lam" "lam"
-| Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100)
--- a/Tutorial/Tutorial1.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial1.thy Mon Mar 05 16:27:28 2012 +0000
@@ -131,7 +131,7 @@
term "Lam [x].Var x" -- {* a lambda-term *}
term "App t1 t2" -- {* another lambda-term *}
term "x::name" -- {* an (object) variable of type name *}
-term "atom (x::name)" -- {* atom is an overloaded function *}
+term "atom (x::name)" -- {* atom is an overloded function *}
text {*
Lam [x].Var is the syntax we made up for lambda abstractions. If you
@@ -207,7 +207,7 @@
*}
inductive
- eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60)
+ eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60)
where
e_Lam[intro]: "Lam [x].t \<Down> Lam [x].t"
| e_App[intro]: "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
@@ -476,7 +476,7 @@
Just like gotos in the Basic programming language, labels often reduce
the readability of proofs. Therefore one can use in Isar the notation
"then have" in order to feed a have-statement to the proof of
- the next have-statement. This is used in the second case below.
+ the next have-statement. This is used in teh second case below.
*}
lemma
@@ -498,7 +498,7 @@
text {*
The label ih2 cannot be got rid of in this way, because it is used
- two lines below and we cannot rearrange them. We can still avoid the
+ two lines below and we cannot rearange them. We can still avoid the
label by feeding a sequence of facts into a proof using the
"moreover"-chaining mechanism:
--- a/Tutorial/Tutorial1s.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial1s.thy Mon Mar 05 16:27:28 2012 +0000
@@ -678,7 +678,7 @@
text {* Complete the proof and remove the sorries. *}
-lemma
+lemma ctx_compose:
shows "(E1 \<odot> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
proof (induct E1)
case Hole
--- a/Tutorial/Tutorial2.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial2.thy Mon Mar 05 16:27:28 2012 +0000
@@ -242,7 +242,7 @@
by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)
then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto
qed
- ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
+ ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by (simp only:)
qed (auto) -- {* var and app cases, luckily, are automatic *}
--- a/Tutorial/Tutorial2s.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial2s.thy Mon Mar 05 16:27:28 2012 +0000
@@ -208,7 +208,7 @@
by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)
then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto
qed
- ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
+ ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by (simp only:)
qed (auto) -- {* var and app cases, luckily, are automatic *}
--- a/Tutorial/Tutorial4.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial4.thy Mon Mar 05 16:27:28 2012 +0000
@@ -49,7 +49,7 @@
text {*
In order to help establishing the property that the machine
- calculates a normal form that corresponds to the evaluation
+ calculates a nomrmalform that corresponds to the evaluation
relation, we introduce the call-by-value small-step semantics.
*}
@@ -124,7 +124,7 @@
text {*
The point of the cbv-reduction was that we can easily relatively
- establish the following property:
+ establish the follwoing property:
*}
lemma machine_implies_cbvs_ctx:
--- a/Tutorial/Tutorial4s.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial4s.thy Mon Mar 05 16:27:28 2012 +0000
@@ -1,5 +1,5 @@
-theory Tutorial4
-imports Tutorial1
+theory Tutorial4s
+imports Tutorial1s
begin
section {* The CBV Reduction Relation (Small-Step Semantics) *}
@@ -115,18 +115,22 @@
proof (induct)
case (m1 t1 t2 Es)
thm machine.intros thm cbv2
- have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
+ have "Es\<down>\<lbrakk>App t1 t2\<rbrakk> = (Es\<down> \<odot> CAppL \<box> t2)\<lbrakk>t1\<rbrakk>"
+ using ctx_compose ctx_composes.simps filling.simps by simp
then show "Es\<down>\<lbrakk>App t1 t2\<rbrakk> \<longrightarrow>cbv* ((CAppL \<box> t2) # Es)\<down>\<lbrakk>t1\<rbrakk>" using cbvs.intros by simp
next
case (m2 v t2 Es)
have "val v" by fact
- have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
+ have "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> = (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>"
+ using ctx_compose ctx_composes.simps filling.simps by simp
then show "((CAppL \<box> t2) # Es)\<down>\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (CAppR v \<box> # Es)\<down>\<lbrakk>t2\<rbrakk>" using cbvs.intros by simp
next
case (m3 v x t Es)
have aa: "val v" by fact
- have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>" using ctx_compose ctx_composes.simps filling.simps by simp
- then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using better_cbv1[OF aa] cbv_in_ctx by simp
+ have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> = Es\<down>\<lbrakk>App (Lam [x]. t) v\<rbrakk>"
+ using ctx_compose ctx_composes.simps filling.simps by simp
+ then have "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>"
+ using better_cbv1[OF aa] cbv_in_ctx by simp
then show "(((CAppR (Lam [x].t) \<box>) # Es)\<down>)\<lbrakk>v\<rbrakk> \<longrightarrow>cbv* (Es\<down>)\<lbrakk>(t[x ::= v])\<rbrakk>" using cbvs.intros by blast
qed
--- a/Tutorial/Tutorial5.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial5.thy Mon Mar 05 16:27:28 2012 +0000
@@ -1,4 +1,3 @@
-
theory Tutorial5
imports Tutorial4
--- a/Tutorial/Tutorial6.thy Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial6.thy Mon Mar 05 16:27:28 2012 +0000
@@ -17,7 +17,7 @@
Var "name"
| Fun "ty" "ty" (infixr "\<rightarrow>" 100)
and tys =
- All as::"name fset" ty::"ty" bind (set+) as in ty ("All _. _" [100, 100] 100)
+ All as::"name fset" ty::"ty" binds (set+) as in ty ("All _. _" [100, 100] 100)
text {* Some alpha-equivalences *}