# HG changeset patch # User Christian Urban # Date 1330964848 0 # Node ID 87eca760dcba0b2d35548d51504def4ff0536f9d # Parent 3e37322465e28807c8c3bc62804a771b12582c31 updated tutorial to latest version and added it to the tests diff -r 3e37322465e2 -r 87eca760dcba IsaMakefile --- 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 diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Lambda.thy --- 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 "\p x r. height_graph x r \ height_graph (p \ x) (p \ 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 \ x" in meta_spec) -apply(drule_tac x="- p \ 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 \ (y, s) \ (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" -apply(subgoal_tac "\p x r. subst_graph x r \ subst_graph (p \ x) (p \ 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 \ x" in meta_spec) -apply(drule_tac x="- p \ 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 \ [[atom x]]lst. t \ atom x \ [[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 \ x), atom x} \* ([[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 \ 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 \ ya = ya") -apply(subgoal_tac "p \ 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 (\(t, _, _). size t)") - (simp_all add: lam.size) - -lemma subst_eqvt[eqvt]: - shows "(p \ t[x ::= s]) = (p \ t)[(p \ x) ::= (p \ s)]" -by (induct t x s rule: subst.induct) (simp_all) +termination (eqvt) + by lexicographic_order lemma fresh_fact: assumes a: "atom z \ s" diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Minimal.thy --- 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) diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial1.thy --- 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 \ lam \ bool" (infixr "\" 60) + eval :: "lam \ lam \ bool" ("_ \ _" [60, 60] 60) where e_Lam[intro]: "Lam [x].t \ Lam [x].t" | e_App[intro]: "\t1 \ Lam [x].t; t2 \ v'; t[x::=v'] \ v\ \ App t1 t2 \ 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: diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial1s.thy --- 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 \ E2)\t\ = E1\E2\t\\" proof (induct E1) case Hole diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial2.thy --- 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 "\2 \ Lam [c].((c \ x) \ t) : T1 \ T2" using fc1 by auto qed - ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp + ultimately show "\2 \ Lam [x].t : T1 \ T2" by (simp only:) qed (auto) -- {* var and app cases, luckily, are automatic *} diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial2s.thy --- 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 "\2 \ Lam [c].((c \ x) \ t) : T1 \ T2" using fc1 by auto qed - ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp + ultimately show "\2 \ Lam [x].t : T1 \ T2" by (simp only:) qed (auto) -- {* var and app cases, luckily, are automatic *} diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial4.thy --- 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: diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial4s.thy --- 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\\App t1 t2\ = (Es\ \ CAppL \ t2)\t1\" using ctx_compose ctx_composes.simps filling.simps by simp + have "Es\\App t1 t2\ = (Es\ \ CAppL \ t2)\t1\" + using ctx_compose ctx_composes.simps filling.simps by simp then show "Es\\App t1 t2\ \cbv* ((CAppL \ t2) # Es)\\t1\" using cbvs.intros by simp next case (m2 v t2 Es) have "val v" by fact - have "((CAppL \ t2) # Es)\\v\ = (CAppR v \ # Es)\\t2\" using ctx_compose ctx_composes.simps filling.simps by simp + have "((CAppL \ t2) # Es)\\v\ = (CAppR v \ # Es)\\t2\" + using ctx_compose ctx_composes.simps filling.simps by simp then show "((CAppL \ t2) # Es)\\v\ \cbv* (CAppR v \ # Es)\\t2\" using cbvs.intros by simp next case (m3 v x t Es) have aa: "val v" by fact - have "(((CAppR (Lam [x].t) \) # Es)\)\v\ = Es\\App (Lam [x]. t) v\" using ctx_compose ctx_composes.simps filling.simps by simp - then have "(((CAppR (Lam [x].t) \) # Es)\)\v\ \cbv (Es\)\(t[x ::= v])\" using better_cbv1[OF aa] cbv_in_ctx by simp + have "(((CAppR (Lam [x].t) \) # Es)\)\v\ = Es\\App (Lam [x]. t) v\" + using ctx_compose ctx_composes.simps filling.simps by simp + then have "(((CAppR (Lam [x].t) \) # Es)\)\v\ \cbv (Es\)\(t[x ::= v])\" + using better_cbv1[OF aa] cbv_in_ctx by simp then show "(((CAppR (Lam [x].t) \) # Es)\)\v\ \cbv* (Es\)\(t[x ::= v])\" using cbvs.intros by blast qed diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial5.thy --- 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 diff -r 3e37322465e2 -r 87eca760dcba Tutorial/Tutorial6.thy --- 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 "\" 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 *}