(* 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