Showing content from http://homepages.inf.ed.ac.uk/jcheney/projects/SNTT/SNTT.thy below:
(* Simple nominal type theory *) (* James Cheney*) (* 1/23/08: Started development *) (* 4/16/08: Renewed work *) (* 4/20/08: Proved weakening *) (* 4/22/08: Proved subject reduction *) theory SNTT imports Nominal begin atom_decl var name id data_ty name_ty section {* Types *} nominal_datatype ty = UnitTy | PairTy "ty" "ty" | FunTy "ty" "ty" | AbsTy "name_ty" "ty" | NameTy "name_ty" | DataTy "data_ty" abbreviation PairTy_syn::"ty \ ty \ ty" ("_ \ _" [100,100] 100) where "A \ B == PairTy A B" abbreviation FunTy_syn::"ty \ ty \ ty" ("_ \ _" [100,100] 100) where "A \ B == FunTy A B" abbreviation AbsTy_syn::"name_ty \ ty \ ty" ("<_>_" [100,100] 100) where " B == AbsTy a B" lemma ty_fresh_var: fixes A::"ty" and x::"var" shows "x\ A" apply(nominal_induct A rule: ty.inducts) by(simp_all add: fresh_atm) lemma ty_fresh_name: fixes A::"ty" and a::"name" shows "a \ A" apply(nominal_induct A rule: ty.inducts) by(simp_all add: fresh_atm) lemmas ty_fresh = ty_fresh_var ty_fresh_name section {* Terms *} nominal_datatype trm = Unit | Const "id" | Var "var" | Pair' "trm" "trm" | Fst "trm" | Snd "trm" | Lam' "ty" "\ var\ trm" | App "trm" "trm" | Name "name" | Abs' "name_ty" "\ name\ trm" | Conc "trm" "name" abbreviation Lam_syn::"var \ ty \ trm \ trm" ("[_:_]._" [100,100] 100) where "[x:A].M == Lam' A x M" abbreviation App_syn::"trm \ trm \ trm" ("_^_" [100,100] 100) where "M^N == App M N" abbreviation Abs_syn::"name \ name_ty \ trm \ trm" ("<_:_>._" [100,100] 100) where " .M == Abs' A a M" abbreviation Conc_syn::"trm \ name \ trm" ("_@_" [100,100] 100) where "M@a == Conc M a" section {* Signatures *} types Sig = "(id*ty) list" inductive in_sig :: "id \ ty \ Sig \ bool" ("_:_ insig _" [100,100,99] 100) where ic1: "x:A insig ((x,A)#\ )" | ic2: "\ x:A insig \ ;x \ y\ \ x:A insig ((y,B)#\ )" equivariance in_sig nominal_inductive in_sig done lemma sig_fresh_var: fixes x::"var" and \ ::"Sig" shows "x \ \ " apply(induct \ ) apply(simp_all add: fresh_list_nil fresh_list_cons) apply(clarify) apply(simp_all add: fresh_prod fresh_atm ty_fresh) done lemma sig_fresh_name: fixes a::"name" and \ ::"Sig" shows "a \ \ " apply(induct \ ) apply(simp_all add: fresh_list_nil fresh_list_cons) apply(clarify) apply(simp_all add: fresh_prod fresh_atm ty_fresh) done lemmas sig_fresh = sig_fresh_name sig_fresh_var lemma sig_unique: "\ c:A insig \ ; c:A' insig \ \ \ A = A'" apply(induct c A \ rule:in_sig.inducts) by(auto elim: in_sig.cases) section {* Contexts *} nominal_datatype ctx = EmptyCtx ("[]" 100) | VarCtx "ctx" "var" "ty" ("_,_:_" [100,100,100] 100) | NameCtx "ctx" "name" "name_ty" ("_\ _:_" [100,100,100] 100) inductive in_ctx :: "var \ ty \ ctx \ bool" ("_:_ in _" [100,100,99] 100) where ic1: "x:A in \ ,x:A" | ic2: "\ x:A in \ ;x \ y\ \ x:A in \ ,y:B" | ic3: "x:A in \ \ x:A in (\ \ a:\ )" equivariance in_ctx nominal_inductive in_ctx done lemma in_unique: "\ x:A in \ ; x:A' in \ \ \ A = A'" apply(induct x A \ rule:in_ctx.inducts) by(auto elim: in_ctx.cases simp add:ctx.inject) lemma in_fresh_neq: "\ y:A in \ ; x \ \ \ \ y \ x" apply(induct y A \ rule: in_ctx.inducts) by(simp_all add:fresh_atm,clarify) inductive in_ctx_name :: "name \ name_ty \ ctx \ bool" ("_:_ inn _" [100,100,99] 100) where icn1: "a:\ inn (\ \ a:\ )" | icn2: "a:\ inn \ \ a:\ inn (\ ,x:A)" | icn3: "\ a:\ inn \ ; a \ b\ \ a:\ inn (\ \ b:\ )" equivariance in_ctx_name nominal_inductive in_ctx_name done lemma inn_unique: "\ a:\ inn \ ; a:\ ' inn \ \ \ \ =\ '" apply(induct a \ \ rule:in_ctx_name.inducts) by(auto elim: in_ctx_name.cases simp add:ctx.inject) lemma inn_fresh_neq: "\ a:\ inn \ ; b \ \ \ \ a \ b" apply(induct a \ \ rule: in_ctx_name.inducts) by(simp_all add:fresh_atm,clarify) section {* Substitutions *} nominal_datatype subst = EmptySubst ("[]") | VarSubst "subst" "var" "trm" ("_,_\ _" [100,100,100] 100) | NameSubst "subst" "name" "name" ("_\ _\ _" [100,100,100] 100) consts lookup :: "subst \ var \ trm" nominal_primrec "lookup [] x = Var x" "lookup (\ ,y \ M) x = (if x=y then M else lookup \ x)" "lookup (\ \ a \ b) x = (lookup \ x)" by(simp_all) lemma lookup_eqvt[eqvt]: fixes pi::"var prm" shows "pi\ (lookup \ x) = lookup (pi\ \ ) (pi\ x)" by (nominal_induct \ rule: subst.inducts) (auto simp add: perm_bij) lemma lookup_eqvt_name[eqvt]: fixes pi::"name prm" shows "pi\ (lookup \ x) = lookup (pi\ \ ) (pi\ x)" by (nominal_induct \ rule: subst.inducts) (auto simp add: perm_bij) consts lookup_nm :: "subst \ name \ name" nominal_primrec "lookup_nm [] a = a" "lookup_nm (\ ,y \ M) a = (lookup_nm \ a)" "lookup_nm (\ \ b \ c) a = (if a = b then c else lookup_nm \ a)" by(simp_all) lemma lookup_nm_eqvt[eqvt]: fixes pi::"var prm" shows "pi\ (lookup_nm \ x) = lookup_nm (pi\ \ ) (pi\ x)" by (nominal_induct \ rule: subst.inducts) (auto simp add: perm_bij) lemma lookup_nm_eqvt_name[eqvt]: fixes pi::"name prm" shows "pi\ (lookup_nm \ x) = lookup_nm (pi\ \ ) (pi\ x)" by (nominal_induct \ rule: subst.inducts) (auto simp add: perm_bij) consts subst :: "trm \ subst \ trm" ("_[_]" [200,100] 100) nominal_primrec "(Pair' M N)[\ ] = Pair' (M[\ ]) (N[\ ])" "Unit[\ ] = Unit" "(Var x)[\ ] = (lookup \ x)" "(Const c)[\ ] = Const c" "(M^N)[\ ] = (M[\ ])^(N[\ ])" "x \ \ \ (Lam' A x M)[\ ] = Lam' A x (M[\ ])" "(Fst M)[\ ] = Fst (M[\ ])" "(Snd M)[\ ] = Snd (M[\ ])" "(Name a)[\ ] = (Name (lookup_nm \ a))" "a \ \ \ ( .M)[\ ] = .(M[\ ])" "(M@a)[\ ] = (M[\ ])@(lookup_nm \ a)" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh)+ apply(fresh_guess,simp add: ty_fresh ty_fresh_name fresh_atm)+ done lemma subst_eqvt_var[eqvt]: fixes pi::"var prm" and M ::"trm" and \ ::"subst" shows "pi\ (subst M \ ) = subst (pi\ M) (pi\ \ )" by (nominal_induct M avoiding: \ pi rule: trm.inducts) (simp_all add: lookup_eqvt lookup_nm_eqvt fresh_bij) lemma subst_eqvt_name[eqvt]: fixes pi::"name prm" and M::"trm" and \ ::"subst" shows "pi\ (subst M \ ) = subst (pi\ M) (pi\ \ )" by (nominal_induct M avoiding: \ pi rule: trm.inducts) (simp_all add: lookup_eqvt_name lookup_nm_eqvt_name fresh_bij) lemmas subst_eqvt = subst_eqvt_var subst_eqvt_name consts subst_minus :: "subst \ name \ subst" ("_ - _" [100,100] 100) nominal_primrec "[] - a = []" "(\ ,x\ M) - a = (\ - a)" "(\ \ b\ c) - a = (if a = b then \ else (\ -a)\ b\ c)" by auto lemma fresh_lookup: "x \ \ \ Var x = lookup \ x" apply(nominal_induct \ rule:subst.inducts) apply(simp_all add:fresh_atm) done lemma fresh_nmlookup: "a \ \ \ a = lookup_nm \ a" apply(nominal_induct \ rule:subst.inducts) apply(simp_all add:fresh_atm) done lemma subst_id1: "x\ \ \ (M[\ ,x\ Var x]) = (subst M \ )" apply(nominal_induct M avoiding: \ x rule: trm.inducts) apply(simp_all) apply(clarsimp, simp add:fresh_lookup) done lemma subst_id2: "a\ \ \ (M[\ \ a\ a]) = (subst M \ )" apply(nominal_induct M avoiding: \ a rule: trm.inducts) apply(simp_all) apply(auto simp add: trm.inject fresh_nmlookup) done lemmas subst_id = subst_id1 subst_id2 subsection {* Identity substitution *} consts id_sub :: "ctx \ subst" nominal_primrec "id_sub EmptyCtx = EmptySubst" "id_sub (\ ,x:A) = (id_sub \ ,x\ Var x)" "id_sub (\ \ a:\ ) = (id_sub \ \ a\ a)" by auto lemma id_sub_is_identity_var: "lookup (id_sub \ ) x = Var x" apply(nominal_induct \ rule:ctx.induct) by (simp_all) lemma id_sub_is_identity_name: "lookup_nm (id_sub \ ) a = a" apply(nominal_induct \ rule:ctx.induct) by (simp_all) lemmas id_sub_is_identity = id_sub_is_identity_var id_sub_is_identity_name section {* Validity *} inductive valid_ctx :: "ctx \ bool" where vc1[intro!] : "valid_ctx EmptyCtx" | vc2[intro!] : "\ valid_ctx \ ; x\ \ \ \ valid_ctx (\ ,x:A)" | vc3[intro!] : "\ valid_ctx \ ; a\ \ \ \ valid_ctx (\ \ a:\ )" inductive_cases valid_ctx_inv[elim!]: "valid_ctx EmptyCtx" "valid_ctx (\ ,x:A)" "valid_ctx (\ \ a:\ )" inductive res :: "ctx \ name \ name_ty \ ctx \ bool" ("_ \ _ : _ \\ _" [100,100,100,100] 100) where ctxr1 : "a \ \ \ \ \ a:\ \ a:\ \\ \ " | ctxr2 : "\ \ \ a : \ \\ \ ' ; a \ b; b \ \ \ \ \ \ b:\ \ a:\ \\ \ '\ b:\ " | ctxr3 : "\ \ \ a : \ \\ \ '; x \ \ \ \ \ ,x:B \ a:\ \\ \ '" equivariance res nominal_inductive res done lemma res_fresh_name: fixes a b::"name" shows"\ \ \ a:\ \\ \ ';b \ \ \ \ b \ \ '" by (induct \ a \ \ ' arbitrary: b rule:res.inducts) (simp_all) lemma res_fresh_var: fixes a::"name" and b::"var" shows"\ \ \ a:\ \\ \ ';b \ \ \ \ b \ \ '" by (induct \ a \ \ ' arbitrary: b rule:res.inducts) (simp_all) lemmas res_fresh = res_fresh_var res_fresh_name lemma res_preserves_backwards: "\ \ \ a : \ \\ \ '; x:A in \ '\ \ x:A in \ " apply(induct \ a \ \ ' rule:res.induct) apply(blast intro: in_ctx.intros) apply(erule in_ctx.cases,simp_all add:ctx.inject,clarsimp) apply(blast intro: in_ctx.intros) apply(erule in_ctx.intros) apply(erule in_fresh_neq) apply(erule res_fresh,simp) done lemma res_valid: "\ \ a:\ \\ \ ' \ valid_ctx \ \ valid_ctx \ '" apply(induct \ a \ \ ' rule:res.inducts) by(auto simp add: ctx.inject res_fresh) lemma res_neq_remains: fixes a b::"name" shows "\ \ \ a:\ \\ \ '; a \ b; b:\ inn \ \ \ b:\ inn \ '" apply(induct \ a \ \ ' rule:res.inducts) apply(erule in_ctx_name.cases,simp_all add:ctx.inject) apply(erule in_ctx_name.cases,simp_all add:ctx.inject,clarsimp) apply(blast intro:in_ctx_name.intros) apply(erule in_ctx_name.intros,simp) apply(erule in_ctx_name.cases,simp_all add:ctx.inject) done (* TODO: Get rid of redundant hypothesis a \ b *) lemma res_commutation: "\ \ \ b : \ \\ \ 0; \ 0 \ a : \ \\ \ 0';a\ b\ \ \ \ '. \ \ a : \ \\ \ ' \ \ ' \ b : \ \\ \ 0'" apply(nominal_induct \ arbitrary: \ 0 \ 0' rule: ctx.induct) apply(erule res.cases,simp_all) apply(erule res.cases,simp_all add:ctx.inject,clarify) apply(blast intro:res.intros) apply(erule res.cases,simp_all add:ctx.inject,clarify) apply(rule_tac x="\ 0'\ b:\ " in exI) apply(auto intro!: res.intros simp add: res_fresh) apply(erule res.cases,simp_all add:ctx.inject,clarify) apply(rule_tac x="\ " in exI) apply(auto intro!: res.intros simp add: res_fresh) apply(subgoal_tac "\ \ '. \ \ a : \ \\ \ ' \ \ ' \ b : \ \\ \ 'a") prefer 2 apply(blast) apply(clarify) apply(rule_tac x="\ '\ ba:\ '" in exI) apply(auto intro!: res.intros simp add: res_fresh) done lemma res_implies_inn: fixes a :: "name" shows "\ \ a:\ \\ \ ' \ a:\ inn \ " by(induct \ a \ \ ' rule: res.induct) (auto intro: in_ctx_name.intros) lemma res_name_is_fresh: fixes a::"name" shows "\ \ a:\ \\ \ ' \ a \ \ '" apply(induct \ a \ \ ' rule: res.inducts) apply(simp_all add: fresh_atm) done lemma res_ctx_unique: "\ \ \ a:\ \\ \ '; \ \ a:\ \\ \ ''\ \ \ '' = \ '" apply(induct \ a \ \ ' arbitrary:\ '' rule: res.induct) apply(erule res.cases,simp_all (no_asm_use) add:ctx.inject) apply(simp,simp) apply(erule res.cases, simp_all(no_asm_use) add:ctx.inject, clarify) apply(clarify) apply(simp add:ctx.inject) apply(erule res.cases, simp_all(no_asm_use) add:ctx.inject, clarify) apply(blast) done inductive valid :: "Sig \ ctx \ trm \ ty \ bool" ("_,_ \ _ : _ " [100,100,100] 100) where v_const: "c:A insig \ \ \ ,\ \ Const c : A" | v_var: "x:A in \ \ \ ,\ \ Var x : A" | v_lam: "\ \ ,\ ,x:A \ M : B;x\ \ \ \ \ ,\ \ [x:A].M : A \ B" | v_app: "\ \ ,\ \ M : A \ B; \ ,\ \ N : A\ \ \ ,\ \ M^N : B" | v_name: "a:\ inn \ \ \ ,\ \ Name a : NameTy \ " | v_abs: "\ \ ,\ \ a:\ \ M : A;a\ \ \ \ \ ,\ \ >.M : <\ >A" | v_conc: "\ \ \ a:\ \\ \ ' ; \ ,\ ' \ M : <\ >A\ \ \ ,\ \ M@a : A" | v_unit: "\ ,\ \ Unit : UnitTy" | v_pair: "\ \ ,\ \ M : A ; \ ,\ \ N : B\ \ \ ,\ \ Pair' M N : A \ B" | v_fst: "\ ,\ \ M : A \ B \ \ ,\ \ Fst M : A" | v_snd: "\ ,\ \ M : A \ B \ \ ,\ \ Snd M : B" inductive_cases valid_inv: "\ ,\ \ Const c : A" "\ ,\ \ Var x : A" "\ ,\ \ [x:A].M : B" "\ ,\ \ M^N : B" "\ ,\ \ Name a : A" "\ ,\ \ >.M : A" "\ ,\ \ M@a : A" "\ ,\ \ Unit : A" "\ ,\ \ Pair' M N : A" "\ ,\ \ Fst M : A" "\ ,\ \ Snd M : B" equivariance valid nominal_inductive valid apply(simp_all add: ty_fresh ty_fresh_name abs_fresh sig_fresh sig_fresh_name fresh_atm) done lemma valid_fresh1: fixes x::"var" shows "\ \ ,\ \ M : A; x \ \ \ \ x \ M" apply(induct rule:valid.inducts) apply(auto dest: in_fresh_neq simp add:fresh_atm ty_fresh abs_fresh in_fresh_neq res_fresh) done lemma valid_fresh2: fixes a::"name" shows "\ \ ,\ \ M : A; a \ \ \ \ a \ M" apply(induct rule:valid.inducts) apply(auto dest: res_implies_inn inn_fresh_neq simp add:fresh_atm ty_fresh abs_fresh res_fresh) done lemmas valid_fresh = valid_fresh1 valid_fresh2 lemma valid_type_unique: "\ \ ,\ \ M : A; \ ,\ \ M : B; valid_ctx \ \ \ A = B" apply (induct arbitrary: B rule:valid.inducts) (* Constant *) apply(erule valid_inv, simp (no_asm_use) add:trm.inject) apply(blast intro: sig_unique) (* Var *) apply(erule valid_inv, simp (no_asm_use) add:trm.inject) apply(blast intro: in_unique) (* Lambda *) apply(erule valid_inv,simp (no_asm_use) add: trm.inject,clarify) apply(simp (no_asm_use) add: alpha ty.inject) apply(case_tac "x=xa", blast) apply(drule_tac x="Bb" in meta_spec) apply(subgoal_tac "valid_ctx (\ ,x:Aa)") prefer 2 apply(blast intro: valid_ctx.intros) apply(subgoal_tac "\ ,\ ,x:Aa \ M : Bb",blast) apply(frule_tac pi="[(x,xa)]" in valid.eqvt(2)) back apply(perm_simp add:ty_fresh sig_fresh) (* App *) apply(erule valid_inv)+ apply(simp (no_asm_use) add:trm.inject) apply(clarify) apply(subgoal_tac "A \ B = Aa \ Ba") prefer 2 apply(blast) apply(simp (no_asm_use) add:ty.inject,clarify) (* Name *) apply(erule valid_inv) apply(simp (no_asm_use) add:trm.inject,clarify) apply(simp (no_asm_use) add:ty.inject) apply(blast intro: inn_unique) (* Abstraction *) apply(erule valid_inv,simp (no_asm_use) add: trm.inject,clarify) apply(simp (no_asm_use) add: alpha ty.inject) apply(case_tac "a=aa", blast) apply(drule_tac x="Aa" in meta_spec) apply(subgoal_tac "valid_ctx (\ \ a:\ ')") prefer 2 apply(blast intro: valid_ctx.intros) apply(subgoal_tac "\ ,\ \ a:\ ' \ M : Aa",blast) apply(frule_tac pi="[(a,aa)]" in valid.eqvt(3)) back apply(perm_simp add:ty_fresh sig_fresh fresh_atm) (* Concretion *) apply(erule valid_inv) apply(simp (no_asm_use) add:trm.inject) apply(clarify) apply(subgoal_tac "\ = \ '") prefer 2 apply(drule res_implies_inn)+ apply(blast intro: inn_unique) apply(subgoal_tac "\ ' = \ 'a") prefer 2 apply(blast intro: res_ctx_unique) apply(clarify) apply(subgoal_tac "<\ '>A = <\ '>B") prefer 2 apply(blast intro: res_valid) apply(simp (no_asm_use) add:ty.inject) (* Unit *) apply(erule valid_inv,simp) (* Pair *) apply(erule valid_inv) apply(simp (no_asm_use) add:trm.inject,clarify) apply(simp (no_asm_use) add:ty.inject) apply(blast) (* Fst *) apply(erule valid_inv) apply(simp (no_asm_use) add:trm.inject,clarify) apply(subgoal_tac "A \ B = Ba \ Bb") prefer 2 apply(blast ) apply(simp (no_asm_use) add:ty.inject,clarify) (* Snd *) apply(erule valid_inv) apply(simp (no_asm_use) add:trm.inject,clarify) apply(subgoal_tac "A \ B = Aa \ Ba") prefer 2 apply(blast ) apply(simp (no_asm_use) add:ty.inject,clarify) done inductive valid_subst :: "Sig \ ctx \ subst \ ctx \ bool" ("_,_ \ _ : _ sub" [100,100,100] 100) where vs_empty: "\ ,\ \ [] : [] sub" | vs_var: "\ \ ,\ \ \ : \ ' sub; \ ,\ \ M : A;x\ \ '\ \ \ ,\ \ \ ,x\ M : \ ',x:A sub" | vs_name: "\ \ \ b : \ \\ \ 0 ; \ ,\ 0 \ \ : \ ' sub;a\ \ '\ \ \ ,\ \ \ \ a\ b : \ '\ a:\ sub" inductive_cases valid_subst_inv[elim!]: "\ ,\ \ [] : [] sub" "\ ,\ \ \ ,x\ M : \ ' sub" "\ ,\ \ \ : \ ',x:A sub" "\ ,\ \ \ \ a\ b : \ ' sub" "\ ,\ \ \ : \ '\ a:\ sub" equivariance valid_subst nominal_inductive valid_subst done section{* Subcontexts *} text {* Currently have two definitions of subcontext, which are equivalent. Probably best to get rid of one. *} constdefs sem_sub :: "Sig \ ctx \ ctx \ bool" "sem_sub \ \ \ ' == (\ ,\ ' \ id_sub \ : \ sub)" inductive sub_ctx :: "ctx \ ctx \ bool" where sc1 : "sub_ctx EmptyCtx \ " | sc2 : "\ x:A in \ '; sub_ctx \ \ '; x\ \ \ \ sub_ctx (\ ,x:A) \ '" | sc3 : "\ \ ' \ a:\ \\ \ ''; sub_ctx \ \ ''; a \ \ \ \ sub_ctx (\ \ a:\ ) \ '" inductive_cases sub_ctx_inv[elim!]: "sub_ctx EmptyCtx \ " "sub_ctx (\ ,x:A) \ '" "sub_ctx (\ \ a:\ ) \ '" lemma sub_valid: "\ sub_ctx \ \ '; valid_ctx \ '\ \ valid_ctx \ " apply(induct \ \ ' rule: sub_ctx.inducts) apply(clarsimp) apply(clarsimp) apply(clarsimp) apply(drule res_valid,simp_all) done lemma sc1' : "sem_sub \ EmptyCtx \ " unfolding sem_sub_def by (auto simp add:vs_empty) lemma sc2' : "\ x:A in \ '; sem_sub \ \ \ ';x\ \ \ \ sem_sub \ (\ ,x:A) \ '" unfolding sem_sub_def by (auto simp add:vs_var v_var) lemma sc3': "\ \ ' \ a:\ \\ \ ''; sem_sub \ \ \ '';a\ \ \ \ sem_sub \ (\ \ a:\ ) \ '" unfolding sem_sub_def by (auto simp add:vs_name v_name) lemma sc2_inv': "sem_sub \ (\ ,x:A) \ ' \ x:A in \ ' \ sem_sub \ \ \ ' \ x\ \ " unfolding sem_sub_def apply(auto) apply(erule valid_subst.cases,simp_all add:ctx.inject subst.inject) apply(clarsimp) apply(erule valid.cases,simp_all add:trm.inject,clarsimp) apply(erule valid.cases,simp_all add:trm.inject,clarsimp) apply(erule valid.cases,simp_all add:ctx.inject trm.inject subst.inject) done lemma sc3_inv': "sem_sub \ (\ \ a:\ ) \ ' \ \ \ ''. \ ' \ a:\ \\ \ '' \ sem_sub \ \ \ '' \ a\ \ " unfolding sem_sub_def apply(auto) apply(erule valid_subst.cases,simp_all add:ctx.inject subst.inject) apply(clarsimp) apply(rule_tac x="\ " in exI) apply(simp add:valid_subst.intros) apply(clarsimp) apply(rule_tac x="\ " in exI) apply(simp add:valid_subst.intros) apply(clarsimp) apply(rule_tac x="\ " in exI) apply(simp) apply(simp add: valid_subst.intros) done lemma sub_ctx_implies_sem_sub: "sub_ctx \ \ ' \ sem_sub \ \ \ '" apply(induct \ \ ' rule:sub_ctx.inducts) apply(simp_all add:sc1' sc2' sc3') done lemma sem_sub_implies_sub_ctx: "sem_sub \ \ \ ' \ sub_ctx \ \ '" apply(nominal_induct \ arbitrary: \ ' rule:ctx.induct) apply(rule sc1) apply(drule sc2_inv') apply(rule sc2,simp_all) apply(drule sc3_inv') apply(blast intro:sc3) done lemma sem_sub_weak_in: "sem_sub \ \ \ ' \ x:A in \ \ x:A in \ '" unfolding sem_sub_def apply(induct \ \ ' \ \ "id_sub \ " \ rule:valid_subst.inducts) apply(erule in_ctx.cases,simp_all) apply(simp add:subst.inject,clarify) apply(erule in_ctx.cases,simp_all add:ctx.inject,clarify) apply(erule valid.cases,simp_all add:trm.inject) apply(simp add:subst.inject,clarify) apply(erule in_ctx.cases,simp_all add:ctx.inject,clarify) apply(erule res_preserves_backwards,simp) done lemma sem_sub_weak_res: "\ ,\ ' \ id_sub \ : \ sub \ \ \ a:\ \\ \ 0 \ \ \ 0'. \ ,\ 0' \ id_sub \ 0 : \ 0 sub \ \ ' \ a:\ \\ \ 0'" apply(induct \ \ ' \ \ "id_sub \ " \ arbitrary: \ 0 rule:valid_subst.inducts) apply(erule res.cases,simp_all) apply(simp add:subst.inject,clarify) apply(erule res.cases, simp_all add:ctx.inject) apply(simp add:subst.inject,clarify) apply(erule res.cases,simp_all) back apply(simp_all add:ctx.inject,clarify) apply(blast) apply(clarsimp) apply(drule_tac x="\ 'a" in meta_spec) apply(clarsimp) apply(subgoal_tac "\ \ '. \ \ a:\ \\ \ ' \ \ ' \ ba:\ \\ \ 0'") apply(clarify) apply(rule_tac x="\ '" in exI) apply(safe) apply(rule valid_subst.intros) apply(simp) apply(simp) apply(simp add: res_fresh) apply(blast intro: res_commutation) done lemma res_sem_sub_weak: "sem_sub \ \ \ ' \ \ \ a:\ \\ \ 0 \ \ \ 0'. sem_sub \ \ 0 \ 0' \ \ ' \ a:\ \\ \ 0'" unfolding sem_sub_def apply( blast intro:sem_sub_weak_res) done lemma sem_sub_trans: "sem_sub \ \ 1 \ 2 \ sem_sub \ \ 2 \ 3 \ sem_sub \ \ 1 \ 3" unfolding sem_sub_def apply(induct \ \ 2 \ \ "id_sub \ 1" \ 1 arbitrary: \ 3 rule:valid_subst.inducts) apply(simp add:valid_subst.intros) apply(clarsimp,simp add:subst.inject,clarsimp) apply(rule valid_subst.intros) apply(blast) apply(rule valid.intros) apply(rule sem_sub_weak_in) unfolding sem_sub_def apply(simp) apply(erule_tac valid.cases,simp_all) apply(simp add:trm.inject) apply(drule sem_sub_weak_res,simp) apply(simp add:subst.inject,clarsimp) apply(rule valid_subst.intros) apply(assumption) apply(blast) apply(simp) done lemma sub_ctx_lweak1: "\ sub_ctx \ \ '; x\ \ '\ \ sub_ctx \ (\ ',x:A)" apply(induct \ \ ' rule: sub_ctx.inducts) apply(simp add:sub_ctx.intros) apply(rule sub_ctx.intros, rule in_ctx.intros) apply(simp_all add:in_fresh_neq) apply(rule sub_ctx.intros) apply(rule res.intros, assumption+) done lemma sub_ctx_lweak2: "\ sub_ctx \ \ ';a\ \ '\ \ sub_ctx \ (\ '\ a:\ )" apply(induct \ \ ' rule: sub_ctx.inducts) apply(simp add:sub_ctx.intros) apply(rule sub_ctx.intros, rule in_ctx.intros) apply(simp_all) apply(simp add:res_fresh) apply(rule sub_ctx.intros) apply(rule res.intros, simp_all) apply(rule inn_fresh_neq) apply(erule res_implies_inn) apply(simp) done lemma sub_ctx_refl: "valid_ctx \ \ sub_ctx \ \ " apply(induct \ rule:valid_ctx.inducts) apply(auto intro: sub_ctx.intros in_ctx.intros sub_ctx_lweak1 res.intros) done lemma sem_sub_refl: "valid_ctx \ \ sem_sub \ \ \ " apply(auto intro:sub_ctx_refl sub_ctx_implies_sem_sub) done (* needed elsewhere *) lemma valid_id: "valid_ctx \ \ \ ,\ \ id_sub \ : \ sub" apply(drule sem_sub_refl) apply(simp add:sem_sub_def) done lemma sub_ctx_fresh_var: fixes a::"var" shows "sub_ctx \ \ ' \ a \ \ ' \ a \ \ " apply(induct \ \ ' arbitrary: a rule: sub_ctx.inducts) apply(simp_all add:fresh_atm ty_fresh) apply(auto dest: in_fresh_neq) apply(subgoal_tac "aa \ \ ''") apply(simp) apply(rule res_fresh) apply(simp_all) done lemma sub_ctx_fresh_name: fixes a::"name" shows "sub_ctx \ \ ' \ a \ \ ' \ a \ \ " apply(induct \ \ ' arbitrary: a rule: sub_ctx.inducts) apply(simp_all add:fresh_atm ty_fresh) apply(frule res_implies_inn) apply(auto dest: inn_fresh_neq) apply(subgoal_tac "aa \ \ ''") apply(simp) apply(rule res_fresh) apply(simp_all) done lemma sub_ctx_trans: "\ sub_ctx \ 1 \ 2; sub_ctx \ 2 \ 3\ \ sub_ctx \ 1 \ 3" apply(rule sem_sub_implies_sub_ctx) apply(rule sem_sub_trans) apply(erule sub_ctx_implies_sem_sub)+ done lemma res_implies_sub: fixes a b::"name" shows "\ \ \ a:\ \\ \ ';valid_ctx \ \ \ sub_ctx \ ' \ " apply (induct \ a \ \ ' rule:res.inducts) apply(clarify) apply(rule sub_ctx_lweak2) apply(rule sub_ctx_refl) apply(simp_all add:ctx.inject) apply(clarify) apply(simp add:ctx.inject) apply(clarsimp) apply(rule sc3) apply(rule res.intros) apply(simp_all add:sub_ctx_fresh_name) apply(clarify) apply(simp add:ctx.inject) apply(rule sub_ctx_lweak1,simp_all) done lemma res_plus_name_is_sub_ctx: "\ \ \ a : \ \\ \ '; valid_ctx \ ; a\ \ '\ \ sub_ctx (\ '\ a:\ ) \ " apply(frule res_implies_sub,simp) apply(rule sub_ctx.intros) apply(simp) apply(rule sub_ctx_refl, simp add: res_valid) apply(simp) done section{* Weakening *} lemma in_weakening: shows "\ x:A in \ ; sub_ctx \ \ '; valid_ctx \ '\ \ x:A in \ '" apply(induct x A \ arbitrary: \ ' rule:in_ctx.inducts) apply(clarify, simp add:ctx.inject)+ apply(drule res_implies_sub,simp_all) apply(drule sub_ctx_trans, simp,blast) done lemma inn_weakening: shows "\ a:\ inn \ ; sub_ctx \ \ '; valid_ctx \ '\ \ a:\ inn \ '" apply(induct a \ \ arbitrary: \ ' rule:in_ctx_name.inducts) apply(clarify, simp_all add:ctx.inject,clarify) apply(frule res_implies_inn) apply(drule res_implies_sub) apply(simp) apply(simp add:sub_ctx_trans) apply(clarify,simp add:ctx.inject) apply(clarify,simp add:ctx.inject,clarify) apply(drule res_implies_sub,simp_all) apply(drule sub_ctx_trans, simp,blast) done lemma res_weakening: fixes a::"name" and \ ::"name_ty" and \ 1 \ 2 \ 1' :: "ctx" shows "\ \ 1 \ a:\ \\ \ 1'; sub_ctx \ 1 \ 2; valid_ctx \ 2\ \ \ \ 2'. \ 2 \ a:\ \\ \ 2' \ sub_ctx \ 1' \ 2'" apply(drule sub_ctx_implies_sem_sub) apply(drule res_sem_sub_weak,simp) apply(blast intro:sem_sub_implies_sub_ctx) done lemma weakening: fixes x::"var" and A::"ty" and \ ::"ctx" shows"\ \ ,\ \ M : A; sub_ctx \ \ '; valid_ctx \ '\ \ \ ,\ ' \ M : A " apply(nominal_induct \ \ M A avoiding: \ ' rule: valid.strong_inducts) apply(auto intro:valid.intros in_weakening inn_weakening) (* Lambda *) apply(rule valid.intros) apply(subgoal_tac "sub_ctx (\ ,x:A) (\ ',x:A) \ valid_ctx (\ ',x:A)") apply(clarsimp) apply(auto) apply(intro sc2 ic1) apply(intro sub_ctx_lweak1,simp_all) (* Abstraction *) apply(rule valid.intros) apply(subgoal_tac "sub_ctx (\ \ a:\ ) (\ '\ a:\ ) \ valid_ctx (\ '\ a:\ )") apply(clarsimp) apply(auto) apply(intro sc3) apply(rule ctxr1,simp_all) (* Concretion *) apply(drule res_weakening) apply(simp_all) apply(clarsimp) apply(subgoal_tac "valid_ctx \ 2'") prefer 2 apply(blast intro: res_valid) apply(subgoal_tac "\ ,\ 2' \ M : <\ >A") prefer 2 apply(blast) apply(blast intro: valid.intros) done lemma valid_subst_weakening: shows"\ \ ,\ \ \ : \ 0 sub; sub_ctx \ \ '; valid_ctx \ '\ \ \ ,\ ' \ \ : \ 0 sub" apply(induct \ \ \ \ 0 arbitrary: \ ' rule: valid_subst.induct) apply(rule valid_subst.intros) apply(rule valid_subst.intros) apply(blast) apply(erule weakening) apply(simp_all) apply(drule res_weakening) apply(simp+) apply(clarify) apply(rule valid_subst.intros) apply(assumption) apply(frule res_valid,simp_all) done section{* Agreement *} inductive agree :: "ctx \ subst \ subst \ bool" where ag1 : "agree EmptyCtx \ \ '" | ag2 : "\ agree \ \ \ '; lookup \ x = lookup \ ' x\ \ agree (\ ,x:A) \ \ '" | ag3 : "\ agree \ \ \ '; lookup_nm \ a = lookup_nm \ ' a\ \ agree (\ \ a:\ ) \ \ '" lemma agree_id: "agree \ ' (id_sub \ ) []" apply(nominal_induct \ ' rule:ctx.inducts) apply(rule agree.intros) apply(erule agree.intros) apply(simp add:id_sub_is_identity) apply(erule agree.intros) apply(simp_all add:id_sub_is_identity) done lemma agree_in: "agree \ \ \ ' \ x:A in \ \ lookup \ x = lookup \ ' x" apply(induct rule:agree.inducts) apply(auto elim:in_ctx.cases simp add:ctx.inject) done lemma agree_inn: "agree \ \ \ ' \ a:\ inn \ \ lookup_nm \ a = lookup_nm \ ' a" apply(induct rule:agree.inducts) apply(auto elim:in_ctx_name.cases simp add:ctx.inject) done lemma res_agree: "\ \ a:\ \\ \ ' \ agree \ \ \ ' \ agree \ ' \ \ ' " apply(induct rule:res.induct) apply(erule agree.cases,simp_all add:ctx.inject) apply(auto elim:agree.cases intro:agree.intros simp add:ctx.inject)+ apply(erule agree.cases,simp_all add:ctx.inject,clarify) apply(blast intro: agree.intros) done lemma fresh_agree_var: "agree \ \ \ ' \ x\ (\ ,\ ,\ ') \ agree (\ ,x:A) \ \ '" apply(erule agree.intros) apply(auto simp add:fresh_prod fresh_lookup[THEN sym]) done lemma fresh_agree_name: "agree \ \ \ ' \ a\ (\ ,\ ,\ ') \ agree (\ \ a:\ ) \ \ '" apply(erule agree.intros) apply(auto simp add:fresh_prod fresh_nmlookup[THEN sym]) done lemma subst_agree_equal: "\ \ ,\ \ M : A; agree \ \ \ '\ \ M[\ ] = M[\ ']" apply(nominal_induct avoiding: \ \ ' rule:valid.strong_induct) apply(auto simp add:agree_in agree_inn trm.inject alpha fresh_agree_var fresh_agree_name intro: res_agree dest: res_implies_inn) done lemma agree_fresh: "a \ \ \ agree \ (\ \ a\ b) \ " apply(nominal_induct \ rule:ctx.induct) apply(auto intro:agree.intros simp add: fresh_atm) done lemma agree_name: "\ agree \ \ \ ';a \ \ \ \ agree (\ \ a:\ ) (\ \ a\ b) (\ '\ a\ b)" apply(induct rule:agree.inducts) apply(auto intro: agree.intros elim: agree.cases simp add: ctx.inject subst.inject) apply(erule agree.cases,simp_all add:ctx.inject subst.inject,clarify) back apply(intro agree.intros,simp_all) apply(erule agree.cases,simp_all add:ctx.inject subst.inject,clarify) back apply(intro agree.intros,simp_all) done lemma agree_var: "\ agree \ \ \ ';x \ \ \ \ agree (\ ) (\ ,x\ M) (\ ')" apply(induct rule:agree.inducts) apply(auto intro: agree.intros elim: agree.cases simp add: ctx.inject subst.inject fresh_atm) done lemma agree_var2: "agree \ \ \ ' \ x\ \ \ agree (\ ,x:A) (\ ,x\ M) (\ ',x\ M)" apply(induct rule:agree.inducts) apply(auto intro: agree.intros elim: agree.cases simp add: ctx.inject subst.inject) apply(erule agree.cases,simp_all add:ctx.inject subst.inject,clarify) back apply(intro agree.intros,simp_all) apply(erule agree.cases,simp_all add:ctx.inject subst.inject,clarify) back apply(intro agree.intros,simp_all) done lemma res_subst_agree: "\ \ \ a : \ \\ \ '; \ ,\ 0 \ \ : \ sub\ \ agree \ ' \ (\ -a)" apply(induct arbitrary:\ \ 0 rule:res.inducts) apply(auto elim:res.intros intro: agree_fresh simp add: ctx.inject) apply(rule agree_name) apply(simp_all add:res_fresh) apply(rule agree_var) apply(simp_all add:res_fresh) done section {* Substitution Lemma *} lemma subst_lookup: fixes x::"var" and a::"ty" and \ ::"ctx" shows"\ x:A in \ '; \ ,\ \ \ : \ ' sub; valid_ctx \ \ \ \ ,\ \ lookup \ x : A " apply(induct x A \ ' arbitrary: \ \ rule: in_ctx.induct) apply(erule valid_subst.cases, simp_all add:ctx.inject) apply(erule valid_subst.cases, simp_all add:ctx.inject) apply(erule valid_subst.cases, simp_all add:ctx.inject) apply(clarify) apply(subgoal_tac "sub_ctx \ 0 \ ''") prefer 2 apply(erule res_implies_sub,simp) apply(subgoal_tac "\ ,\ 0 \ lookup \ ' x : A") prefer 2 apply(simp add: sub_valid) apply(erule weakening,simp_all) done lemma subst_nmlookup: "\ a:\ inn \ '; \ ,\ \ \ : \ ' sub; valid_ctx \ \ \ \ ,\ \ Name (lookup_nm \ a) : NameTy \ " apply(induct a \ \ ' arbitrary: \ \ rule: in_ctx_name.induct) apply(erule valid_subst.cases, simp_all add:ctx.inject,clarify) apply(intro valid.intros) apply(blast intro:res_implies_inn) apply(erule valid_subst.cases, simp_all add:ctx.inject,clarify) apply(simp add:ctx.inject,clarify) apply(subgoal_tac "sub_ctx \ 0 \ '") prefer 2 apply(erule res_implies_sub,simp) apply(subgoal_tac "\ ,\ 0 \ Name(lookup_nm \ ' a) : NameTy \ ") prefer 2 apply(simp add: sub_valid) apply(erule weakening,simp_all) done lemma subst_valid_subst:"\ \ \ a : \ \\ \ ';\ ,\ 0 \ \ :\ sub\ \ \ \ 0'. \ 0 \ lookup_nm \ a : \ \\ \ 0' \ \ ,\ 0' \ \ -a : \ ' sub" apply(induct \ a \ \ ' arbitrary: \ 0 \ rule:res.inducts) apply(auto simp add: ctx.inject) apply(subgoal_tac "\ \ 0'. \ 0a \ lookup_nm \ ' a : \ \\ \ 0' \ \ ,\ 0' \ \ ' - a : \ ' sub") prefer 2 apply(blast) apply(clarify) apply(frule res_commutation) back apply(assumption) apply(rule inn_fresh_neq) apply(erule res_implies_inn) apply(erule res_name_is_fresh) apply(clarify) apply(rule_tac x="\ 'b" in exI) apply(simp) apply(erule valid_subst.intros) apply(auto intro: res_fresh) done lemma subst: "\ \ ,\ \ M : A; \ ,\ ' \ \ : \ sub; valid_ctx \ '\ \ \ ,\ ' \ M[\ ] : A" apply(nominal_induct \ \ M A avoiding: \ \ ' rule:valid.strong_inducts ) apply(auto intro: valid.intros) (* Var *) apply(erule subst_lookup,simp_all) (* Lam *) apply(subgoal_tac "\ ,\ ',x:A \ M[\ ,x\ Var x] : B") prefer 2 apply(drule_tac x="\ ,x\ Var x" in meta_spec) apply(drule_tac x="\ ',x:A" in meta_spec) apply(subgoal_tac "valid_ctx (\ ',x:A)") prefer 2 apply(blast intro: valid_ctx.intros) apply(subgoal_tac "\ ,\ ',x:A \ \ ,x\ Var x : \ ,x:A sub") prefer 2 apply(rule valid_subst.intros) apply(erule valid_subst_weakening) apply(simp add:sub_ctx_lweak1 sub_ctx_refl) apply(simp) apply(blast intro:in_ctx.intros valid.intros) apply(simp) apply(blast) apply(rule valid.intros) apply(simp add:subst_id1) apply(simp) (* App *) apply(blast intro: valid.intros) (* Name *) apply(erule subst_nmlookup,simp_all) (* Abs *) apply(subgoal_tac "\ ,\ '\ a:\ \ M[\ \ a\ a] : A") prefer 2 apply(drule_tac x="\ \ a\ a" in meta_spec) apply(drule_tac x="\ '\ a:\ " in meta_spec) apply(subgoal_tac "valid_ctx (\ '\ a:\ )") prefer 2 apply(blast intro: valid_ctx.intros) apply(subgoal_tac "\ ,\ '\ a:\ \ \ \ a\ a : \ \ a:\ sub") prefer 2 apply(rule valid_subst.intros) apply(rule res.intros,simp) apply(erule valid_subst_weakening) apply(simp add:sub_ctx_refl) apply(simp) apply(simp) apply(blast) apply(rule valid.intros) apply(simp add:subst_id2) apply(simp) (* Conc *) apply(frule subst_valid_subst,simp,clarify) apply(rule valid.intros) apply(assumption) apply(subgoal_tac "valid_ctx \ 0'") prefer 2 apply(blast intro: res_valid) apply(subgoal_tac "\ ,\ 0' \ M[\ -a] : <\ >A") prefer 2 apply(blast) apply(subgoal_tac "M[\ ] = M[\ -a]") prefer 2 apply(erule subst_agree_equal) apply(erule res_subst_agree,simp) apply(simp) done section {* One-at-a-time substitution and renaming *} constdefs subst1 :: "trm \ var \ trm \ trm" ("_[_:=_]" [100,100,100] 100) "M[x:=N] \ M[[],x\ N]" constdefs rename1 :: "trm \ name \ name \ trm" ("_[_:=_]" [100,100,100] 100) "M[a:=b] \ M[[]\ a\ b]" lemma subst1_eqvt_var[eqvt]: fixes x::"var" and pi :: "var prm" shows "pi \ (M[x:=N]) = (pi \ M)[(pi\ x):=(pi\ N)]" unfolding subst1_def by(simp add:subst_eqvt_var) lemma subst1_eqvt_name[eqvt]: fixes x::"var" and pi ::"name prm" shows "pi \ (M[x:=N]) = (pi \ M)[(pi\ x):=(pi\ N)]" unfolding subst1_def by (simp add:subst_eqvt_name) lemma rename1_eqvt_var[eqvt]: fixes a b ::"name" and pi :: "var prm" shows "pi \ (M[a:=b]) = (pi \ M)[(pi\ a):=(pi\ b)]" unfolding rename1_def by(simp add:subst_eqvt_var) lemma rename1_eqvt_name[eqvt]: fixes a b::"name" and pi ::"name prm" shows "pi \ (M[a:=b]) = (pi \ M)[(pi\ a):=(pi\ b)]" unfolding rename1_def by (simp add:subst_eqvt_name) lemma subst1_fresh: fixes x::"var" shows "x\ N \ x\ M[x:=N]" apply(nominal_induct M avoiding: x N rule:trm.inducts) apply(simp_all add:subst1_def fresh_atm abs_fresh ty_fresh) done lemma rename1_fresh: fixes a::"name" shows "a\ b \ a\ M[a:=b]" apply(nominal_induct M avoiding: a b rule:trm.inducts) apply(simp_all add:rename1_def fresh_atm abs_fresh ty_fresh) done lemma subst1_agree: "x \ \ \ agree (\ ,x:A) (id_sub \ ,x\ M) ([],x\ M)" apply(blast intro:agree_var2 agree_id) done lemma rename1_agree: "a \ \ \ agree (\ \ a:\ ) (id_sub \ \ a\ b) ([]\ a\ b)" apply(blast intro:agree_name agree_id) done section {* Beta reduction and subject reduction theorem *} inductive beta :: "trm \ trm \ bool" where beta_fun: "x\ N \ beta (([x:A].M)^N) (M[x:=N])" | beta_abs: "a\ b \ beta (( >.M)@b) (M[a:=b])" | beta_pair1: "beta (Fst (Pair' M N)) M" | beta_pair2: "beta (Snd (Pair' M N)) N" equivariance beta[var,name] nominal_inductive beta apply(simp_all add: ty_fresh ty_fresh_name abs_fresh sig_fresh sig_fresh_name fresh_atm subst1_fresh rename1_fresh) done inductive red :: "trm \ trm \ bool" ("_ \ \<^isub>\ _" [100,100] 100) where red_v: "Var x \ \<^isub>\ Var x" | red_c: "Const c \ \<^isub>\ Const c" | red_a: "\ M \ \<^isub>\ M'; N \ \<^isub>\ N'\ \ App M N \ \<^isub>\ App M' N'" | red_l: "red M M' \ red ([x:A].M) ([x:A].M')" | red_n: "red (Name a) (Name a)" | red_a: "red M M' \ red (M@a) (M'@a)" | red_l: "red M M' \ red ( >.M) ( >.M')" | red_beta: "beta M M' \ red M M'" equivariance red[var,name] nominal_inductive red apply(simp_all add: ty_fresh ty_fresh_name abs_fresh sig_fresh sig_fresh_name fresh_atm subst1_fresh rename1_fresh) done lemma subst1: "\ \ ,(\ ,x:A) \ M : B; \ ,\ \ N : A;valid_ctx \ ;x\ \ \ \ \ ,\ \ M[x:=N] : B" apply(subgoal_tac "\ ,\ \ M[id_sub \ ,x\ N] : B") prefer 2 apply(erule subst) apply(intro valid_subst.intros,simp_all) apply(blast intro:valid_id) apply(subgoal_tac "M[id_sub \ ,x\ N] = M[x:=N]",simp) unfolding subst1_def apply(erule subst_agree_equal) apply(erule subst1_agree) done lemma rename1: "\ \ ,(\ \ a:\ ) \ M : B; valid_ctx \ ;a\ \ ; b\ \ \ \ \ ,(\ \ b:\ ) \ M[a:=b] : B" apply(subgoal_tac "\ ,(\ \ b:\ ) \ M[id_sub \ \ a\ b] : B") prefer 2 apply(erule subst) apply(intro valid_subst.intros,simp_all) apply(erule res.intros) apply(blast intro:valid_id) apply(simp add: valid_ctx.intros) apply(subgoal_tac "M[id_sub \ \ a\ b] = M[a:=b]",simp) unfolding rename1_def apply(erule subst_agree_equal) apply(erule rename1_agree) done lemma local_soundness: "\ beta M M'; \ ,\ \ M : A; valid_ctx \ \ \ \ ,\ \ M' : A" apply(nominal_induct M M' avoiding: \ rule:beta.strong_inducts) (* App/Lam *) apply(erule valid.cases,simp_all add:trm.inject,clarsimp) apply(subgoal_tac "\ a::name. a\ (\ ', M)") prefer 2 apply(rule exists_fresh',finite_guess) apply(erule exE) apply(erule_tac x="x" in valid.strong_cases,simp_all add:sig_fresh ty_fresh ty.inject trm.inject alpha abs_fresh) apply(rule subst1,simp_all) apply(simp add:fresh_prod,blast) (* Abs/Conc *) apply(erule valid.cases,simp_all add:trm.inject,clarsimp) apply(subgoal_tac "\ x::var. x\ (\ ,\ ',\ 'a,M)") prefer 2 apply(rule exists_fresh',finite_guess) apply(erule exE) apply(erule_tac a="a" and x="x" in valid.strong_cases,simp_all add:sig_fresh ty_fresh ty.inject trm.inject alpha abs_fresh fresh_atm res_fresh) apply(clarsimp) apply(subgoal_tac "\ ,\ \ aa:\ '' \ Ma[a:=aa] : A") prefer 2 apply(erule rename1, simp_all add:res_valid res_fresh res_name_is_fresh) apply(rule weakening,simp_all) apply(rule res_plus_name_is_sub_ctx,simp_all add:res_name_is_fresh) (* Pairs *) apply(erule valid.cases,simp_all add:trm.inject ty.inject)+ done lemma subject_reduction: "\ M \ \<^isub>\ N;\ ,\ \ M : A; valid_ctx \ \ \ \ ,\ \ N : A" apply(nominal_induct avoiding: \ arbitrary: A rule:red.strong_inducts) apply(auto) (* App *) apply(erule valid.cases,simp_all add: trm.inject,clarsimp) apply(blast intro: valid.intros) (* Lam *) apply(erule valid.cases,simp_all add:trm.inject alpha, clarsimp) apply(case_tac "x=xa") apply(simp_all add: valid.intros valid_ctx.intros) apply(subgoal_tac "valid_ctx (\ ',x:Ab)") prefer 2 apply(simp add:valid_ctx.intros) apply(subgoal_tac "\ ,(\ ',x:Ab) \ ([(x,xa)] \ Ma) : B") prefer 2 apply(frule_tac pi="[(x,xa)]" in valid.eqvt(2),perm_simp add:ty_fresh sig_fresh) apply(blast intro:valid.intros) (* Conc *) apply(erule valid.cases,simp_all add: trm.inject,clarsimp) apply(blast intro:valid.intros res_valid) (* Abs *) apply(erule valid.cases,simp_all add:trm.inject alpha, clarsimp) apply(case_tac "a=aa") apply(simp_all add: valid.intros valid_ctx.intros) apply(subgoal_tac "valid_ctx (\ '\ a:\ ')") prefer 2 apply(simp add:valid_ctx.intros) apply(subgoal_tac "\ ,(\ '\ a:\ ') \ ([(a,aa)] \ Ma) : Aa") prefer 2 apply(frule_tac pi="[(a,aa)]" in valid.eqvt(3),perm_simp add:ty_fresh sig_fresh fresh_atm) apply(blast intro:valid.intros) (* beta step *) apply(blast intro:local_soundness) done section {* Eta expansion and subject expansion theorem *} inductive eta :: "Sig \ ctx \ trm \ trm \ bool" where eta_fun: "\ \ ,\ \ M : A \ B;x\ \ \ \ eta \ \ M ([x:A].(M^Var x))" | eta_abs: "\ \ ,\ \ M : <\ >A;a\ \ \ \ eta \ \ M ( >.(M@a))" | eta_unit: "\ ,\ \ M : UnitTy \ eta \ \ M Unit" | eta_pair: "\ \ ,\ \ M : A \ B\ \ eta \ \ M (Pair' (Fst M) (Snd M))" equivariance eta[var,name] nominal_inductive eta apply(simp_all add: ty_fresh ty_fresh_name abs_fresh sig_fresh sig_fresh_name fresh_atm subst1_fresh rename1_fresh valid_fresh) done lemma local_completeness: "\ eta \ \ M M'; \ ,\ \ M : A; valid_ctx \ \ \ \ ,\ \ M' : A" apply(nominal_induct M M' arbitrary: A rule: eta.strong_inducts) apply(subgoal_tac "Aa = A \ B") prefer 2 apply(blast intro: valid_type_unique) apply(clarsimp, rule valid.intros,simp_all) apply(rule valid.intros) apply(erule weakening) apply(rule sub_ctx_lweak1, rule sub_ctx_refl,simp_all add:valid_ctx.intros) apply(rule valid.intros, rule in_ctx.intros) (* abstraction *) apply(subgoal_tac "Aa = <\ >A") prefer 2 apply(blast intro: valid_type_unique) apply(clarsimp, rule valid.intros,simp_all) apply(rule valid.intros) apply(rule res.intros) apply(simp_all) (* Unit *) apply(subgoal_tac "A = UnitTy") prefer 2 apply(blast intro: valid_type_unique) apply(simp,rule valid.intros) (* Pair *) apply(subgoal_tac "Aa = A \ B") prefer 2 apply(blast intro: valid_type_unique) apply(simp, blast intro:valid.intros) done inductive exp :: "Sig \ ctx \ trm \ trm \ bool" where exp_v: "exp \ \ (Var x) (Var x)" | exp_c: "exp \ \ (Const c) (Const c)" | exp_a: "\ exp \ \ M M'; exp \ \ N N'\ \ exp \ \ (App M N) (App M' N')" | exp_l: "\ exp \ (\ ,x:A) M M';x\ \ \ \ exp \ \ ([x:A].M) ([x:A].M')" | exp_n: "exp \ \ (Name a) (Name a)" | exp_a: "\ \ \ a:\ \\ \ '; exp \ \ ' M M'\ \ exp \ \ (M@a) (M'@a)" | exp_l: "\ exp \ (\ \ a:\ ) M M'; a\ \ \ \ exp \ \ ( >.M) ( >.M')" | exp_eta: "eta \ \ M M' \ exp \ \ M M'" equivariance exp[var,name] nominal_inductive exp apply(simp_all add: ty_fresh ty_fresh_name abs_fresh sig_fresh sig_fresh_name fresh_atm subst1_fresh rename1_fresh) done lemma subject_expansion: "\ exp \ \ M N;\ ,\ \ M : A; valid_ctx \ \ \ \ ,\ \ N : A" apply(nominal_induct \ \ M N arbitrary: A rule:exp.strong_inducts) apply(auto) (* application *) apply(erule valid.cases,simp_all add: trm.inject,clarsimp) apply(blast intro: valid.intros) (* lambda *) apply(erule valid.cases,simp_all add:trm.inject alpha, clarsimp) apply(case_tac "x=xa") apply(simp_all add: valid.intros valid_ctx.intros) apply(subgoal_tac "valid_ctx (\ ',x:Ab)") prefer 2 apply(simp add:valid_ctx.intros) apply(subgoal_tac "\ ',(\ ',x:Ab) \ ([(x,xa)] \ Ma) : B") prefer 2 apply(frule_tac pi="[(x,xa)]" in valid.eqvt(2),perm_simp add:ty_fresh sig_fresh) apply(blast intro:valid.intros) (* concretion *) apply(erule valid.cases,simp_all add: trm.inject,clarsimp) apply(subgoal_tac "\ = \ '") prefer 2 apply(drule res_implies_inn)+ apply(blast intro: inn_unique) apply(subgoal_tac "\ ' = \ 'a") prefer 2 apply(blast intro: res_ctx_unique) apply(subgoal_tac "valid_ctx \ 'a") prefer 2 apply(simp add:res_valid) apply(blast intro:valid.intros) (* abstraction *) apply(erule valid.cases,simp_all add:trm.inject alpha, clarsimp) apply(case_tac "a=aa") apply(simp_all add: valid.intros valid_ctx.intros) apply(subgoal_tac "valid_ctx (\ '\ a:\ ')") prefer 2 apply(simp add:valid_ctx.intros) apply(subgoal_tac "\ ',(\ '\ a:\ ') \ ([(a,aa)] \ Ma) : Aa") prefer 2 apply(frule_tac pi="[(a,aa)]" in valid.eqvt(3),perm_simp add:ty_fresh sig_fresh fresh_atm) apply(blast intro:valid.intros) (* eta *) apply(blast intro: local_completeness) done end
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.3