summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | urbanc |

Tue, 10 Oct 2006 16:26:59 +0200 | |

changeset 20955 | 65a9a30b8ece |

parent 20954 | 3bbe7cab8037 |

child 20956 | 00fe22000c6a |

made some proof look more like the ones in Barendregt

--- a/src/HOL/Nominal/Examples/CR.thy Tue Oct 10 15:33:25 2006 +0200 +++ b/src/HOL/Nominal/Examples/CR.thy Tue Oct 10 16:26:59 2006 +0200 @@ -7,69 +7,74 @@ text {* The Church-Rosser proof from Barendregt's book *} lemma forget: - assumes a: "a\<sharp>t1" - shows "t1[a::=t2] = t1" -using a -proof (nominal_induct t1 avoiding: a t2 rule: lam.induct) - case (Var b) - thus ?case by (simp add: fresh_atm) + assumes asm: "x\<sharp>L" + shows "L[x::=P] = L" +using asm +proof (nominal_induct L avoiding: x P rule: lam.induct) + case (Var z) + have "x\<sharp>Var z" by fact + thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm) next - case App - thus ?case by simp + case (App M1 M2) + have "x\<sharp>App M1 M2" by fact + moreover + have ih1: "x\<sharp>M1 \<Longrightarrow> M1[x::=P] = M1" by fact + moreover + have ih1: "x\<sharp>M2 \<Longrightarrow> M2[x::=P] = M2" by fact + ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp next - case (Lam c t) - have ih: "\<And>c t2. c\<sharp>t \<Longrightarrow> t[c::=t2] = t" by fact - have a: "c\<sharp>t2" by fact - have "c\<sharp>a" by fact - hence b: "a\<noteq>c" by (simp add: fresh_atm) - have "a\<sharp>Lam [c].t" by fact - hence "a\<sharp>t" using b by (simp add: abs_fresh) - hence "t[a::=t2] = t" using ih by simp - thus "(Lam [c].t)[a::=t2] = Lam [c].t" using a b by simp + case (Lam z M) + have vc: "z\<sharp>x" "z\<sharp>P" by fact + have ih: "x\<sharp>M \<Longrightarrow> M[x::=P] = M" by fact + have asm: "x\<sharp>Lam [z].M" by fact + with vc have "x\<sharp>M" by (simp add: fresh_atm abs_fresh) + hence "M[x::=P] = M" using ih by simp + thus "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp qed lemma forget_automatic: - assumes asm: "a\<sharp>t\<^isub>1" - shows "t\<^isub>1[a::=t\<^isub>2] = t\<^isub>1" - using asm by (nominal_induct t\<^isub>1 avoiding: a t\<^isub>2 rule: lam.induct) + assumes asm: "x\<sharp>L" + shows "L[x::=P] = L" + using asm by (nominal_induct L avoiding: x P rule: lam.induct) (auto simp add: abs_fresh fresh_atm) lemma fresh_fact: - fixes a :: "name" - assumes a: "a\<sharp>t1" - and b: "a\<sharp>t2" - shows "a\<sharp>(t1[b::=t2])" -using a b -proof (nominal_induct t1 avoiding: a b t2 rule: lam.induct) - case (Var c) - thus ?case by simp + fixes z::"name" + assumes asms: "z\<sharp>N" "z\<sharp>L" + shows "z\<sharp>(N[y::=L])" +using asms +proof (nominal_induct N avoiding: z y L rule: lam.induct) + case (Var u) + have "z\<sharp>(Var u)" "z\<sharp>L" by fact + thus "z\<sharp>((Var u)[y::=L])" by simp next - case App thus ?case by simp + case (App N1 N2) + have ih1: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N1[y::=L]" by fact + moreover + have ih2: "\<lbrakk>z\<sharp>N2; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N2[y::=L]" by fact + moreover + have "z\<sharp>App N1 N2" "z\<sharp>L" by fact + ultimately show "z\<sharp>((App N1 N2)[y::=L])" by simp next - case (Lam c t) - have ih: "\<And>(a::name) b t2. a\<sharp>t \<Longrightarrow> a\<sharp>t2 \<Longrightarrow> a\<sharp>(t[b::=t2])" by fact - have fr: "c\<sharp>a" "c\<sharp>b" "c\<sharp>t2" by fact+ - hence fr': "c\<noteq>a" by (simp add: fresh_atm) - have a1: "a\<sharp>t2" by fact - have a2: "a\<sharp>Lam [c].t" by fact - hence "a\<sharp>t" using fr' by (simp add: abs_fresh) - hence "a\<sharp>t[b::=t2]" using a1 ih by simp - thus "a\<sharp>(Lam [c].t)[b::=t2]" using fr by (simp add: abs_fresh) + case (Lam u N1) + have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact + have "z\<sharp>Lam [u].N1" by fact + hence "z\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm) + moreover + have ih: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>(N1[y::=L])" by fact + moreover + have "z\<sharp>L" by fact + ultimately show "z\<sharp>(Lam [u].N1)[y::=L]" using vc by (simp add: abs_fresh) qed lemma fresh_fact_automatic: - fixes a::"name" - assumes asm: "a\<sharp>t\<^isub>1" "a\<sharp>t\<^isub>2" - shows "a\<sharp>(t\<^isub>1[b::=t\<^isub>2])" -using asm by (nominal_induct t\<^isub>1 avoiding: a b t\<^isub>2 rule: lam.induct) - (auto simp add: abs_fresh fresh_atm) + fixes z::"name" + assumes asms: "z\<sharp>N" "z\<sharp>L" + shows "z\<sharp>(N[y::=L])" +using asms by (nominal_induct N avoiding: z y L rule: lam.induct) + (auto simp add: abs_fresh fresh_atm) -lemma subs_lemma: - fixes x::"name" - and y::"name" - and L::"lam" - and M::"lam" - and N::"lam" +lemma substitution_lemma: assumes a: "x\<noteq>y" and b: "x\<sharp>L" shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" @@ -88,7 +93,7 @@ } moreover { (*Case 1.2*) - assume "z\<noteq>x" and "z=y" + assume "z=y" and "z\<noteq>x" have "(1)": "?LHS = L" using `z\<noteq>x` `z=y` by force have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by force have "(3)": "L[x::=N[y::=L]] = L" using `x\<sharp>L` by (simp add: forget) @@ -105,13 +110,13 @@ qed next case (Lam z M1) (* case 2: lambdas *) - have ih: "\<And>x y N L. \<lbrakk>x\<noteq>y; 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; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact have "x\<noteq>y" by fact have "x\<sharp>L" by fact have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact hence "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") - proof - + proof - have "?LHS = Lam [z].(M1[x::=N][y::=L])" using `z\<sharp>x` `z\<sharp>y` `z\<sharp>N` `z\<sharp>L` by simp also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using `x\<noteq>y` `x\<sharp>L` by simp also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using `z\<sharp>x` `z\<sharp>N[y::=L]` by simp @@ -123,7 +128,7 @@ thus ?case by simp qed -lemma subs_lemma_automatic: +lemma substitution_lemma_automatic: assumes asm: "x\<noteq>y" "x\<sharp>L" shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" using asm by (nominal_induct M avoiding: x y N L rule: lam.induct) @@ -509,7 +514,7 @@ also have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" using o4 b by force also have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" - using e3 by (simp add: subs_lemma fresh_atm) + using e3 by (simp add: substitution_lemma fresh_atm) ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp qed qed @@ -520,7 +525,7 @@ shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" using a b apply(nominal_induct M M' avoiding: N N' x rule: one_induct) -apply(auto simp add: one_subst_aux subs_lemma fresh_atm) +apply(auto simp add: one_subst_aux substitution_lemma fresh_atm) done lemma diamond[rule_format]:

--- a/src/HOL/Nominal/Examples/Compile.thy Tue Oct 10 15:33:25 2006 +0200 +++ b/src/HOL/Nominal/Examples/Compile.thy Tue Oct 10 16:26:59 2006 +0200 @@ -54,7 +54,7 @@ inductive ctxts intros v1[intro]: "valid []" -v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" +v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *) text {* typing judgements for trms *}

--- a/src/HOL/Nominal/Examples/Weakening.thy Tue Oct 10 15:33:25 2006 +0200 +++ b/src/HOL/Nominal/Examples/Weakening.thy Tue Oct 10 16:26:59 2006 +0200 @@ -212,6 +212,9 @@ and b: "valid \<Gamma>2" and c: "\<Gamma>1 \<lless> \<Gamma>2" shows "\<Gamma>2 \<turnstile> t:\<sigma>" + +thm typing.induct[no_vars] + using a b c proof (induct arbitrary: \<Gamma>2) case (t1 \<Gamma>1 \<tau> a) (* variable case *)