diff --git a/thys/LambdaAuth/Semantics.thy b/thys/LambdaAuth/Semantics.thy --- a/thys/LambdaAuth/Semantics.thy +++ b/thys/LambdaAuth/Semantics.thy @@ -1,1140 +1,1149 @@ (* Author: Matthias Brun, ETH Zürich, 2019 *) (* Author: Dmitriy Traytel, ETH Zürich, 2019 *) section \Semantics of $\lambda\bullet$\ (*<*) theory Semantics imports FMap_Lemmas Syntax begin (*>*) text \Avoid clash with substitution notation.\ no_notation inverse_divide (infixl "'/" 70) text \Help automated provers with smallsteps.\ declare One_nat_def[simp del] subsection \Equivariant Hash Function\ consts hash_real :: "term \ hash" nominal_function map_fixed :: "var \ var list \ term \ term" where "map_fixed fp l Unit = Unit" | "map_fixed fp l (Var y) = (if y \ set l then (Var y) else (Var fp))" | "atom y \ (fp, l) \ map_fixed fp l (Lam y t) = (Lam y ((map_fixed fp (y # l) t)))" | "atom y \ (fp, l) \ map_fixed fp l (Rec y t) = (Rec y ((map_fixed fp (y # l) t)))" | "map_fixed fp l (Inj1 t) = (Inj1 ((map_fixed fp l t)))" | "map_fixed fp l (Inj2 t) = (Inj2 ((map_fixed fp l t)))" | "map_fixed fp l (Pair t1 t2) = (Pair ((map_fixed fp l t1)) ((map_fixed fp l t2)))" | "map_fixed fp l (Roll t) = (Roll ((map_fixed fp l t)))" | "atom y \ (fp, l) \ map_fixed fp l (Let t1 y t2) = (Let ((map_fixed fp l t1)) y ((map_fixed fp (y # l) t2)))" | "map_fixed fp l (App t1 t2) = (App ((map_fixed fp l t1)) ((map_fixed fp l t2)))" | "map_fixed fp l (Case t1 t2 t3) = (Case ((map_fixed fp l t1)) ((map_fixed fp l t2)) ((map_fixed fp l t3)))" | "map_fixed fp l (Prj1 t) = (Prj1 ((map_fixed fp l t)))" | "map_fixed fp l (Prj2 t) = (Prj2 ((map_fixed fp l t)))" | "map_fixed fp l (Unroll t) = (Unroll ((map_fixed fp l t)))" | "map_fixed fp l (Auth t) = (Auth ((map_fixed fp l t)))" | "map_fixed fp l (Unauth t) = (Unauth ((map_fixed fp l t)))" | "map_fixed fp l (Hash h) = (Hash h)" | "map_fixed fp l (Hashed h t) = (Hashed h ((map_fixed fp l t)))" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def map_fixed_graph_aux_def) subgoal by (erule map_fixed_graph.induct) (auto simp: fresh_star_def fresh_at_base) apply clarify subgoal for P fp l t by (rule term.strong_exhaust[of t P "(fp, l)"]) (auto simp: fresh_star_def fresh_Pair) apply (simp_all add: fresh_star_def fresh_at_base) subgoal for y fp l t ya fpa la ta apply (erule conjE)+ apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"]) apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done subgoal for y fp l t ya fpa la ta apply (erule conjE)+ apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"]) apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done subgoal for y fp l t ya fpa la ta apply (erule conjE)+ apply (erule Abs_lst1_fcb2'[where c = "(fp, l)"]) apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done done nominal_termination (eqvt) by lexicographic_order definition hash where "hash t = hash_real (map_fixed undefined [] t)" lemma permute_map_list: "p \ l = map (\x. p \ x) l" by (induct l) auto lemma map_fixed_eqvt: "p \ l = l \ map_fixed v l (p \ t) = map_fixed v l t" proof (nominal_induct t avoiding: v l p rule: term.strong_induct) case (Var x) then show ?case by (auto simp: term.supp supp_at_base permute_map_list list_eq_iff_nth_eq in_set_conv_nth) next case (Lam y e) from Lam(1,2,3,5) Lam(4)[of p "y # l" v] show ?case by (auto simp: fresh_perm) next case (Rec y e) from Rec(1,2,3,5) Rec(4)[of p "y # l" v] show ?case by (auto simp: fresh_perm) next case (Let e' y e) from Let(1,2,3,6) Let(4)[of p l v] Let(5)[of p "y # l" v] show ?case by (auto simp: fresh_perm) qed (auto simp: permute_pure) lemma hash_eqvt[eqvt]: "p \ hash t = hash (p \ t)" unfolding permute_pure hash_def by (auto simp: map_fixed_eqvt) lemma map_fixed_idle: "{x. \ atom x \ t} \ set l \ map_fixed v l t = t" proof (nominal_induct t avoiding: v l rule: term.strong_induct) case (Var x) then show ?case by (auto simp: subset_iff fresh_at_base) next case (Lam y e) from Lam(1,2,4) Lam(3)[of "y # l" v] show ?case by (auto simp: fresh_Pair Abs1_eq) next case (Rec y e) from Rec(1,2,4) Rec(3)[of "y # l" v] show ?case by (auto simp: fresh_Pair Abs1_eq) next case (Let e' y e) from Let(1,2,5) Let(3)[of l v] Let(4)[of "y # l" v] show ?case by (auto simp: fresh_Pair Abs1_eq) qed (auto simp: subset_iff) +lemma map_fixed_idle_closed: + "closed t \ map_fixed undefined [] t = t" + by (rule map_fixed_idle) auto + lemma map_fixed_inj_closed: "closed t \ closed u \ map_fixed undefined [] t = map_fixed undefined [] u \ t = u" - by (erule box_equals[OF _ map_fixed_idle map_fixed_idle]) auto + by (rule box_equals[OF _ map_fixed_idle_closed map_fixed_idle_closed]) + +lemma hash_eq_hash_real_closed: + assumes "closed t" + shows "hash t = hash_real t" + unfolding hash_def map_fixed_idle_closed[OF assms] .. subsection \Substitution\ nominal_function subst_term :: "term \ term \ var \ term" ("_[_ '/ _]" [250, 200, 200] 250) where "Unit[t' / x] = Unit" | "(Var y)[t' / x] = (if x = y then t' else Var y)" | "atom y \ (x, t') \ (Lam y t)[t' / x] = Lam y (t[t' / x])" | "atom y \ (x, t') \ (Rec y t)[t' / x] = Rec y (t[t' / x])" | "(Inj1 t)[t' / x] = Inj1 (t[t' / x])" | "(Inj2 t)[t' / x] = Inj2 (t[t' / x])" | "(Pair t1 t2)[t' / x] = Pair (t1[t' / x]) (t2[t' / x]) " | "(Roll t)[t' / x] = Roll (t[t' / x])" | "atom y \ (x, t') \ (Let t1 y t2)[t' / x] = Let (t1[t' / x]) y (t2[t' / x])" | "(App t1 t2)[t' / x] = App (t1[t' / x]) (t2[t' / x])" | "(Case t1 t2 t3)[t' / x] = Case (t1[t' / x]) (t2[t' / x]) (t3[t' / x])" | "(Prj1 t)[t' / x] = Prj1 (t[t' / x])" | "(Prj2 t)[t' / x] = Prj2 (t[t' / x])" | "(Unroll t)[t' / x] = Unroll (t[t' / x])" | "(Auth t)[t' / x] = Auth (t[t' / x])" | "(Unauth t)[t' / x] = Unauth (t[t' / x])" | "(Hash h)[t' / x] = Hash h" | "(Hashed h t)[t' / x] = Hashed h (t[t' / x])" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def subst_term_graph_aux_def) subgoal by (erule subst_term_graph.induct) (auto simp: fresh_star_def fresh_at_base) apply clarify subgoal for P a b t by (rule term.strong_exhaust[of a P "(b, t)"]) (auto simp: fresh_star_def fresh_Pair) apply (simp_all add: fresh_star_def fresh_at_base) subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done done nominal_termination (eqvt) by lexicographic_order type_synonym tenv = "(var, term) fmap" nominal_function psubst_term :: "term \ tenv \ term" where "psubst_term Unit f = Unit" | "psubst_term (Var y) f = (case f $$ y of Some t \ t | None \ Var y)" | "atom y \ f \ psubst_term (Lam y t) f = Lam y (psubst_term t f)" | "atom y \ f \ psubst_term (Rec y t) f = Rec y (psubst_term t f)" | "psubst_term (Inj1 t) f = Inj1 (psubst_term t f)" | "psubst_term (Inj2 t) f = Inj2 (psubst_term t f)" | "psubst_term (Pair t1 t2) f = Pair (psubst_term t1 f) (psubst_term t2 f) " | "psubst_term (Roll t) f = Roll (psubst_term t f)" | "atom y \ f \ psubst_term (Let t1 y t2) f = Let (psubst_term t1 f) y (psubst_term t2 f)" | "psubst_term (App t1 t2) f = App (psubst_term t1 f) (psubst_term t2 f)" | "psubst_term (Case t1 t2 t3) f = Case (psubst_term t1 f) (psubst_term t2 f) (psubst_term t3 f)" | "psubst_term (Prj1 t) f = Prj1 (psubst_term t f)" | "psubst_term (Prj2 t) f = Prj2 (psubst_term t f)" | "psubst_term (Unroll t) f = Unroll (psubst_term t f)" | "psubst_term (Auth t) f = Auth (psubst_term t f)" | "psubst_term (Unauth t) f = Unauth (psubst_term t f)" | "psubst_term (Hash h) f = Hash h" | "psubst_term (Hashed h t) f = Hashed h (psubst_term t f)" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def psubst_term_graph_aux_def) subgoal by (erule psubst_term_graph.induct) (auto simp: fresh_star_def fresh_at_base) apply clarify subgoal for P a b by (rule term.strong_exhaust[of a P b]) (auto simp: fresh_star_def fresh_Pair) apply (simp_all add: fresh_star_def fresh_at_base) subgoal by clarify subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done done nominal_termination (eqvt) by lexicographic_order nominal_function subst_type :: "ty \ ty \ tvar \ ty" where "subst_type One t' x = One" | "subst_type (Fun t1 t2) t' x = Fun (subst_type t1 t' x) (subst_type t2 t' x)" | "subst_type (Sum t1 t2) t' x = Sum (subst_type t1 t' x) (subst_type t2 t' x)" | "subst_type (Prod t1 t2) t' x = Prod (subst_type t1 t' x) (subst_type t2 t' x)" | "atom y \ (t', x) \ subst_type (Mu y t) t' x = Mu y (subst_type t t' x)" | "subst_type (Alpha y) t' x = (if y = x then t' else Alpha y)" | "subst_type (AuthT t) t' x = AuthT (subst_type t t' x)" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def subst_type_graph_aux_def) subgoal by (erule subst_type_graph.induct) (auto simp: fresh_star_def fresh_at_base) apply clarify subgoal for P a by (rule ty.strong_exhaust[of a P]) (auto simp: fresh_star_def) apply (simp_all add: fresh_star_def fresh_at_base) subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff fresh_Pair) done done nominal_termination (eqvt) by lexicographic_order lemma fresh_subst_term: "atom x \ t[t' / x'] \ (x = x' \ atom x \ t) \ (atom x' \ t \ atom x \ t')" by (nominal_induct t avoiding: t' x x' rule: term.strong_induct) (auto simp add: fresh_at_base) lemma term_fresh_subst[simp]: "atom x \ t \ atom x \ s \ (atom (x::var)) \ t[s / y]" by (nominal_induct t avoiding: s y rule: term.strong_induct) (auto) lemma term_subst_idle[simp]: "atom y \ t \ t[s / y] = t" by (nominal_induct t avoiding: s y rule: term.strong_induct) (auto simp: fresh_Pair fresh_at_base) lemma term_subst_subst: "atom y1 \ atom y2 \ atom y1 \ s2 \ t[s1 / y1][s2 / y2] = t[s2 / y2][s1[s2 / y2] / y1]" by (nominal_induct t avoiding: y1 y2 s1 s2 rule: term.strong_induct) auto lemma fresh_psubst: fixes x :: var assumes "atom x \ e" "atom x \ vs" shows "atom x \ psubst_term e vs" using assms by (induct e vs rule: psubst_term.induct) (auto simp: fresh_at_base elim: fresh_fmap_fresh_Some split: option.splits) lemma fresh_subst_type: "atom \ \ subst_type \ \' \' \ ((\ = \' \ atom \ \ \) \ (atom \' \ \ \ atom \ \ \'))" by (nominal_induct \ avoiding: \ \' \' rule: ty.strong_induct) (auto simp add: fresh_at_base) lemma type_fresh_subst[simp]: "atom x \ t \ atom x \ s \ (atom (x::tvar)) \ subst_type t s y" by (nominal_induct t avoiding: s y rule: ty.strong_induct) (auto) lemma type_subst_idle[simp]: "atom y \ t \ subst_type t s y = t" by (nominal_induct t avoiding: s y rule: ty.strong_induct) (auto simp: fresh_Pair fresh_at_base) lemma type_subst_subst: "atom y1 \ atom y2 \ atom y1 \ s2 \ subst_type (subst_type t s1 y1) s2 y2 = subst_type (subst_type t s2 y2) (subst_type s1 s2 y2) y1" by (nominal_induct t avoiding: y1 y2 s1 s2 rule: ty.strong_induct) auto subsection \Weak Typing Judgement\ type_synonym tyenv = "(var, ty) fmap" inductive judge_weak :: "tyenv \ term \ ty \ bool" ("_ \\<^sub>W _ : _" [150,0,150] 149) where jw_Unit: "\ \\<^sub>W Unit : One" | jw_Var: "\ \ $$ x = Some \ \ \ \ \\<^sub>W Var x : \" | jw_Lam: "\ atom x \ \; \(x $$:= \\<^sub>1) \\<^sub>W e : \\<^sub>2 \ \ \ \\<^sub>W Lam x e : Fun \\<^sub>1 \\<^sub>2" | jw_App: "\ \ \\<^sub>W e : Fun \\<^sub>1 \\<^sub>2; \ \\<^sub>W e' : \\<^sub>1 \ \ \ \\<^sub>W App e e' : \\<^sub>2" | jw_Let: "\ atom x \ (\, e\<^sub>1); \ \\<^sub>W e\<^sub>1 : \\<^sub>1; \(x $$:= \\<^sub>1) \\<^sub>W e\<^sub>2 : \\<^sub>2 \ \ \ \\<^sub>W Let e\<^sub>1 x e\<^sub>2 : \\<^sub>2" | jw_Rec: "\ atom x \ \; atom y \ (\,x); \(x $$:= Fun \\<^sub>1 \\<^sub>2) \\<^sub>W Lam y e : Fun \\<^sub>1 \\<^sub>2 \ \ \ \\<^sub>W Rec x (Lam y e) : Fun \\<^sub>1 \\<^sub>2" | jw_Inj1: "\ \ \\<^sub>W e : \\<^sub>1 \ \ \ \\<^sub>W Inj1 e : Sum \\<^sub>1 \\<^sub>2" | jw_Inj2: "\ \ \\<^sub>W e : \\<^sub>2 \ \ \ \\<^sub>W Inj2 e : Sum \\<^sub>1 \\<^sub>2" | jw_Case: "\ \ \\<^sub>W e : Sum \\<^sub>1 \\<^sub>2; \ \\<^sub>W e\<^sub>1 : Fun \\<^sub>1 \; \ \\<^sub>W e\<^sub>2 : Fun \\<^sub>2 \ \ \ \ \\<^sub>W Case e e\<^sub>1 e\<^sub>2 : \" | jw_Pair: "\ \ \\<^sub>W e\<^sub>1 : \\<^sub>1; \ \\<^sub>W e\<^sub>2 : \\<^sub>2 \ \ \ \\<^sub>W Pair e\<^sub>1 e\<^sub>2 : Prod \\<^sub>1 \\<^sub>2" | jw_Prj1: "\ \ \\<^sub>W e : Prod \\<^sub>1 \\<^sub>2 \ \ \ \\<^sub>W Prj1 e : \\<^sub>1" | jw_Prj2: "\ \ \\<^sub>W e : Prod \\<^sub>1 \\<^sub>2 \ \ \ \\<^sub>W Prj2 e : \\<^sub>2" | jw_Roll: "\ atom \ \ \; \ \\<^sub>W e : subst_type \ (Mu \ \) \ \ \ \ \\<^sub>W Roll e : Mu \ \" | jw_Unroll: "\ atom \ \ \; \ \\<^sub>W e : Mu \ \ \ \ \ \\<^sub>W Unroll e : subst_type \ (Mu \ \) \" | jw_Auth: "\ \ \\<^sub>W e : \ \ \ \ \\<^sub>W Auth e : \" | jw_Unauth: "\ \ \\<^sub>W e : \ \ \ \ \\<^sub>W Unauth e : \" declare judge_weak.intros[simp] declare judge_weak.intros[intro] equivariance judge_weak nominal_inductive judge_weak avoids jw_Lam: x | jw_Rec: x and y | jw_Let: x | jw_Roll: \ | jw_Unroll: \ by (auto simp: fresh_subst_type fresh_Pair) text \Inversion rules for typing judgment.\ inductive_cases jw_Unit_inv[elim]: "\ \\<^sub>W Unit : \" inductive_cases jw_Var_inv[elim]: "\ \\<^sub>W Var x : \" lemma jw_Lam_inv[elim]: assumes "\ \\<^sub>W Lam x e : \" and "atom x \ \" obtains \\<^sub>1 \\<^sub>2 where "\ = Fun \\<^sub>1 \\<^sub>2" "(\(x $$:= \\<^sub>1)) \\<^sub>W e : \\<^sub>2" using assms proof (atomize_elim, nominal_induct \ "Lam x e" \ avoiding: x e rule: judge_weak.strong_induct) case (jw_Lam x \ \\<^sub>1 t \\<^sub>2 y u) then show ?case by (auto simp: perm_supp_eq elim!: iffD1[OF Abs_lst1_fcb2'[where f = "\x t (\, \\<^sub>1, \\<^sub>2). (\(x $$:= \\<^sub>1)) \\<^sub>W t : \\<^sub>2" and c = "(\, \\<^sub>1, \\<^sub>2)" and a = x and b = y and x = t and y = u, unfolded prod.case], rotated -1]) qed lemma swap_permute_swap: "atom x \ \ \ atom y \ \ \ (x \ y) \ \ \ (x \ y) \ t = \ \ t" by (subst permute_eqvt) (auto simp: flip_fresh_fresh) lemma jw_Rec_inv[elim]: assumes "\ \\<^sub>W Rec x t : \" and "atom x \ \" obtains y e \\<^sub>1 \\<^sub>2 where "atom y \ (\,x)" "t = Lam y e" "\ = Fun \\<^sub>1 \\<^sub>2" "\(x $$:= Fun \\<^sub>1 \\<^sub>2) \\<^sub>W Lam y e : Fun \\<^sub>1 \\<^sub>2" using [[simproc del: alpha_lst]] assms proof (atomize_elim, nominal_induct \ "Rec x t" \ avoiding: x t rule: judge_weak.strong_induct) case (jw_Rec x \ y \\<^sub>1 \\<^sub>2 e z t) then show ?case proof (nominal_induct t avoiding: y x z rule: term.strong_induct) case (Lam y' e') show ?case proof (intro exI conjI) from Lam.prems show "atom y \ (\, z)" by simp from Lam.hyps(1-3) Lam.prems show "Lam y' e' = Lam y ((y' \ y) \ e')" by (subst term.eq_iff(3), intro Abs_lst_eq_flipI) (simp add: fresh_at_base) from Lam.hyps(1-3) Lam.prems show "\(z $$:= Fun \\<^sub>1 \\<^sub>2) \\<^sub>W Lam y ((y' \ y) \ e') : Fun \\<^sub>1 \\<^sub>2" by (elim judge_weak.eqvt[of "\(x $$:= Fun \\<^sub>1 \\<^sub>2)" "Lam y e" "Fun \\<^sub>1 \\<^sub>2" "(x \ z)", elim_format]) (simp add: perm_supp_eq Abs1_eq_iff fresh_at_base swap_permute_swap fresh_perm flip_commute) qed simp qed (simp_all add: Abs1_eq_iff) qed inductive_cases jw_Inj1_inv[elim]: "\ \\<^sub>W Inj1 e : \" inductive_cases jw_Inj2_inv[elim]: "\ \\<^sub>W Inj2 e : \" inductive_cases jw_Pair_inv[elim]: "\ \\<^sub>W Pair e\<^sub>1 e\<^sub>2 : \" lemma jw_Let_inv[elim]: assumes "\ \\<^sub>W Let e\<^sub>1 x e\<^sub>2 : \\<^sub>2" and "atom x \ (e\<^sub>1, \)" obtains \\<^sub>1 where "\ \\<^sub>W e\<^sub>1 : \\<^sub>1" "\(x $$:= \\<^sub>1) \\<^sub>W e\<^sub>2 : \\<^sub>2" using assms proof (atomize_elim, nominal_induct \ "Let e\<^sub>1 x e\<^sub>2" \\<^sub>2 avoiding: e\<^sub>1 x e\<^sub>2 rule: judge_weak.strong_induct) case (jw_Let x \ e\<^sub>1 \\<^sub>1 e\<^sub>2 \\<^sub>2 x' e\<^sub>2') then show ?case by (auto simp: fresh_Pair perm_supp_eq elim!: iffD1[OF Abs_lst1_fcb2'[where f = "\x t (\, \\<^sub>1, \\<^sub>2). \(x $$:= \\<^sub>1) \\<^sub>W t : \\<^sub>2" and c = "(\, \\<^sub>1, \\<^sub>2)" and a = x and b = x' and x = e\<^sub>2 and y = e\<^sub>2', unfolded prod.case], rotated -1]) qed inductive_cases jw_Prj1_inv[elim]: "\ \\<^sub>W Prj1 e : \\<^sub>1" inductive_cases jw_Prj2_inv[elim]: "\ \\<^sub>W Prj2 e : \\<^sub>2" inductive_cases jw_App_inv[elim]: "\ \\<^sub>W App e e' : \\<^sub>2" inductive_cases jw_Case_inv[elim]: "\ \\<^sub>W Case e e\<^sub>1 e\<^sub>2 : \" inductive_cases jw_Auth_inv[elim]: "\ \\<^sub>W Auth e : \" inductive_cases jw_Unauth_inv[elim]: "\ \\<^sub>W Unauth e : \" lemma subst_type_perm_eq: assumes "atom b \ t" shows "subst_type t (Mu a t) a = subst_type ((a \ b) \ t) (Mu b ((a \ b) \ t)) b" using assms proof - have f: "atom a \ subst_type t (Mu a t) a" by (rule iffD2[OF fresh_subst_type]) simp have "atom b \ subst_type t (Mu a t) a" by (auto simp: assms) with f have "subst_type t (Mu a t) a = (a \ b) \ subst_type t (Mu a t) a" by (simp add: flip_fresh_fresh) then show "subst_type t (Mu a t) a = subst_type ((a \ b) \ t) (Mu b ((a \ b) \ t)) b" by simp qed lemma jw_Roll_inv[elim]: assumes "\ \\<^sub>W Roll e : \" and "atom \ \ (\, \)" obtains \' where "\ = Mu \ \'" "\ \\<^sub>W e : subst_type \' (Mu \ \') \" using assms [[simproc del: alpha_lst]] proof (atomize_elim, nominal_induct \ "Roll e" \ avoiding: e \ rule: judge_weak.strong_induct) case (jw_Roll \ \ e \ \') then show ?case by (auto simp: perm_supp_eq fresh_Pair fresh_at_base subst_type.eqvt intro!: exI[of _ "(\ \ \') \ \"] Abs_lst_eq_flipI dest: judge_weak.eqvt[of _ _ _ "(\ \ \')"]) qed lemma jw_Unroll_inv[elim]: assumes "\ \\<^sub>W Unroll e : \" and "atom \ \ (\, \)" obtains \' where "\ = subst_type \' (Mu \ \') \" "\ \\<^sub>W e : Mu \ \'" using assms proof (atomize_elim, nominal_induct \ "Unroll e" \ avoiding: e \ rule: judge_weak.strong_induct) case (jw_Unroll \ \ e \ \') then show ?case by (auto simp: perm_supp_eq fresh_Pair subst_type_perm_eq fresh_subst_type intro!: exI[of _ "(\ \ \') \ \"] dest: judge_weak.eqvt[of _ _ _ "(\ \ \')"]) qed text \Additional inversion rules based on type rather than term.\ inductive_cases jw_Prod_inv[elim]: "{$$} \\<^sub>W e : Prod \\<^sub>1 \\<^sub>2" inductive_cases jw_Sum_inv[elim]: "{$$} \\<^sub>W e : Sum \\<^sub>1 \\<^sub>2" lemma jw_Fun_inv[elim]: assumes "{$$} \\<^sub>W v : Fun \\<^sub>1 \\<^sub>2" "value v" obtains e x where "v = Lam x e \ v = Rec x e" "atom x \ (c::term)" using assms [[simproc del: alpha_lst]] proof (atomize_elim, nominal_induct "{$$} :: tyenv" v "Fun \\<^sub>1 \\<^sub>2" avoiding: \\<^sub>1 \\<^sub>2 rule: judge_weak.strong_induct) case (jw_Lam x \\<^sub>1 e \\<^sub>2) then obtain x' where "atom (x'::var) \ (c, e)" using finite_supp obtain_fresh' by blast then have "[[atom x]]lst. e = [[atom x']]lst. (x \ x') \ e \ atom x' \ c" by (simp add: Abs_lst_eq_flipI fresh_Pair) then show ?case by auto next case (jw_Rec x y \\<^sub>1 \\<^sub>2 e') obtain x' where "atom (x'::var) \ (c, Lam y e')" using finite_supp obtain_fresh by blast then have "[[atom x]]lst. Lam y e' = [[atom x']]lst. (x \ x') \ (Lam y e') \ atom x' \ c" using Abs_lst_eq_flipI fresh_Pair by blast then show ?case by auto qed simp_all lemma jw_Mu_inv[elim]: assumes "{$$} \\<^sub>W v : Mu \ \" "value v" obtains v' where "v = Roll v'" using assms by (atomize_elim, nominal_induct "{$$} :: tyenv" v "Mu \ \" rule: judge_weak.strong_induct) simp_all subsection \Erasure of Authenticated Types\ nominal_function erase :: "ty \ ty" where "erase One = One" | "erase (Fun \\<^sub>1 \\<^sub>2) = Fun (erase \\<^sub>1) (erase \\<^sub>2)" | "erase (Sum \\<^sub>1 \\<^sub>2) = Sum (erase \\<^sub>1) (erase \\<^sub>2)" | "erase (Prod \\<^sub>1 \\<^sub>2) = Prod (erase \\<^sub>1) (erase \\<^sub>2)" | "erase (Mu \ \) = Mu \ (erase \)" | "erase (Alpha \) = Alpha \" | "erase (AuthT \) = erase \" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def erase_graph_aux_def) subgoal by (erule erase_graph.induct) (auto simp: fresh_star_def fresh_at_base) subgoal for P x by (rule ty.strong_exhaust[of x P x]) (auto simp: fresh_star_def) apply (simp_all add: fresh_star_def fresh_at_base) subgoal apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done done nominal_termination (eqvt) by lexicographic_order lemma fresh_erase_fresh: assumes "atom x \ \" shows "atom x \ erase \" using assms by (induct \ rule: ty.induct) auto lemma fresh_fmmap_erase_fresh: assumes "atom x \ \" shows "atom x \ fmmap erase \" using assms by transfer simp lemma erase_subst_type_shift[simp]: "erase (subst_type \ \' \) = subst_type (erase \) (erase \') \" by (induct \ \' \ rule: subst_type.induct) (auto simp: fresh_Pair fresh_erase_fresh) definition erase_env :: "tyenv \ tyenv" where "erase_env = fmmap erase" subsection \Strong Typing Judgement\ inductive judge :: "tyenv \ term \ ty \ bool" ("_ \ _ : _" [150,0,150] 149) where j_Unit: "\ \ Unit : One" | j_Var: "\ \ $$ x = Some \ \ \ \ \ Var x : \" | j_Lam: "\ atom x \ \; \(x $$:= \\<^sub>1) \ e : \\<^sub>2 \ \ \ \ Lam x e : Fun \\<^sub>1 \\<^sub>2" | j_App: "\ \ \ e : Fun \\<^sub>1 \\<^sub>2; \ \ e' : \\<^sub>1 \ \ \ \ App e e' : \\<^sub>2" | j_Let: "\ atom x \ (\, e\<^sub>1); \ \ e\<^sub>1 : \\<^sub>1; \(x $$:= \\<^sub>1) \ e\<^sub>2 : \\<^sub>2 \ \ \ \ Let e\<^sub>1 x e\<^sub>2 : \\<^sub>2" | j_Rec: "\ atom x \ \; atom y \ (\,x); \(x $$:= Fun \\<^sub>1 \\<^sub>2) \ Lam y e' : Fun \\<^sub>1 \\<^sub>2 \ \ \ \ Rec x (Lam y e') : Fun \\<^sub>1 \\<^sub>2" | j_Inj1: "\ \ \ e : \\<^sub>1 \ \ \ \ Inj1 e : Sum \\<^sub>1 \\<^sub>2" | j_Inj2: "\ \ \ e : \\<^sub>2 \ \ \ \ Inj2 e : Sum \\<^sub>1 \\<^sub>2" | j_Case: "\ \ \ e : Sum \\<^sub>1 \\<^sub>2; \ \ e\<^sub>1 : Fun \\<^sub>1 \; \ \ e\<^sub>2 : Fun \\<^sub>2 \ \ \ \ \ Case e e\<^sub>1 e\<^sub>2 : \" | j_Pair: "\ \ \ e\<^sub>1 : \\<^sub>1; \ \ e\<^sub>2 : \\<^sub>2 \ \ \ \ Pair e\<^sub>1 e\<^sub>2 : Prod \\<^sub>1 \\<^sub>2" | j_Prj1: "\ \ \ e : Prod \\<^sub>1 \\<^sub>2 \ \ \ \ Prj1 e : \\<^sub>1" | j_Prj2: "\ \ \ e : Prod \\<^sub>1 \\<^sub>2 \ \ \ \ Prj2 e : \\<^sub>2" | j_Roll: "\ atom \ \ \; \ \ e : subst_type \ (Mu \ \) \ \ \ \ \ Roll e : Mu \ \" | j_Unroll: "\ atom \ \ \; \ \ e : Mu \ \ \ \ \ \ Unroll e : subst_type \ (Mu \ \) \" | j_Auth: "\ \ \ e : \ \ \ \ \ Auth e : AuthT \" | j_Unauth: "\ \ \ e : AuthT \ \ \ \ \ Unauth e : \" declare judge.intros[intro] equivariance judge nominal_inductive judge avoids j_Lam: x | j_Rec: x and y | j_Let: x | j_Roll: \ | j_Unroll: \ by (auto simp: fresh_subst_type fresh_Pair) lemma judge_imp_judge_weak: assumes "\ \ e : \" shows "erase_env \ \\<^sub>W e : erase \" using assms unfolding erase_env_def by (induct \ e \ rule: judge.induct) (simp_all add: fresh_Pair fresh_fmmap_erase_fresh fmmap_fmupd) subsection \Shallow Projection\ nominal_function shallow :: "term \ term" ("\_\") where "\Unit\ = Unit" | "\Var v\ = Var v" | "\Lam x e\ = Lam x \e\" | "\Rec x e\ = Rec x \e\" | "\Inj1 e\ = Inj1 \e\" | "\Inj2 e\ = Inj2 \e\" | "\Pair e\<^sub>1 e\<^sub>2\ = Pair \e\<^sub>1\ \e\<^sub>2\" | "\Roll e\ = Roll \e\" | "\Let e\<^sub>1 x e\<^sub>2\ = Let \e\<^sub>1\ x \e\<^sub>2\" | "\App e\<^sub>1 e\<^sub>2\ = App \e\<^sub>1\ \e\<^sub>2\" | "\Case e e\<^sub>1 e\<^sub>2\ = Case \e\ \e\<^sub>1\ \e\<^sub>2\" | "\Prj1 e\ = Prj1 \e\" | "\Prj2 e\ = Prj2 \e\" | "\Unroll e\ = Unroll \e\" | "\Auth e\ = Auth \e\" | "\Unauth e\ = Unauth \e\" | \ \No rule is defined for Hash, but: "[..] preserving that structure in every case but that of [..]"\ "\Hash h\ = Hash h" | "\Hashed h e\ = Hash h" using [[simproc del: alpha_lst]] subgoal by (simp add: eqvt_def shallow_graph_aux_def) subgoal by (erule shallow_graph.induct) (auto simp: fresh_star_def fresh_at_base) subgoal for P a by (rule term.strong_exhaust[of a P a]) (auto simp: fresh_star_def) apply (simp_all add: fresh_star_def fresh_at_base) subgoal apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done subgoal apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done subgoal apply (erule conjE) apply (erule Abs_lst1_fcb2') apply (simp_all add: eqvt_at_def) apply (simp_all add: perm_supp_eq Abs_fresh_iff) done done nominal_termination (eqvt) by lexicographic_order lemma fresh_shallow: "atom x \ e \ atom x \ \e\" by (induct e rule: term.induct) auto subsection \Small-step Semantics\ datatype mode = I | P | V \ \Ideal, Prover and Verifier modes\ instantiation mode :: pure begin definition permute_mode :: "perm \ mode \ mode" where "permute_mode \ h = h" instance proof qed (auto simp: permute_mode_def) end type_synonym proofstream = "term list" inductive smallstep :: "proofstream \ term \ mode \ proofstream \ term \ bool" ("\_, _\ _\ \_, _\") where s_App1: "\ \ \, e\<^sub>1 \ m\ \ \', e\<^sub>1' \ \ \ \ \, App e\<^sub>1 e\<^sub>2 \ m\ \ \', App e\<^sub>1' e\<^sub>2 \" | s_App2: "\ value v\<^sub>1; \ \, e\<^sub>2 \ m\ \ \', e\<^sub>2' \ \ \ \ \, App v\<^sub>1 e\<^sub>2 \ m\ \ \', App v\<^sub>1 e\<^sub>2' \" | s_AppLam: "\ value v; atom x \ (v,\) \ \ \ \, App (Lam x e) v \ _\ \ \, e[v / x] \" | s_AppRec: "\ value v; atom x \ (v,\) \ \ \ \, App (Rec x e) v \ _\ \ \, App (e[(Rec x e) / x]) v \" | s_Let1: "\ atom x \ (e\<^sub>1,e\<^sub>1',\,\'); \ \, e\<^sub>1 \ m\ \ \', e\<^sub>1' \ \ \ \ \, Let e\<^sub>1 x e\<^sub>2 \ m\ \ \', Let e\<^sub>1' x e\<^sub>2 \" | s_Let2: "\ value v; atom x \ (v,\) \ \ \ \, Let v x e \ _\ \ \, e[v / x] \" | s_Inj1: "\ \ \, e \ m\ \ \', e' \ \ \ \ \, Inj1 e \ m\ \ \', Inj1 e' \" | s_Inj2: "\ \ \, e \ m\ \ \', e' \ \ \ \ \, Inj2 e \ m\ \ \', Inj2 e' \" | s_Case: "\ \ \, e \ m\ \ \', e' \ \ \ \ \, Case e e\<^sub>1 e\<^sub>2 \ m\ \ \', Case e' e\<^sub>1 e\<^sub>2 \" | \ \Case rules are different from paper to account for recursive functions.\ s_CaseInj1: "\ value v \ \ \ \, Case (Inj1 v) e\<^sub>1 e\<^sub>2 \ _\ \ \, App e\<^sub>1 v \" | s_CaseInj2: "\ value v \ \ \ \, Case (Inj2 v) e\<^sub>1 e\<^sub>2 \ _\ \ \, App e\<^sub>2 v \" | s_Pair1: "\ \ \, e\<^sub>1 \ m\ \ \', e\<^sub>1' \ \ \ \ \, Pair e\<^sub>1 e\<^sub>2 \ m\ \ \', Pair e\<^sub>1' e\<^sub>2 \" | s_Pair2: "\ value v\<^sub>1; \ \, e\<^sub>2 \ m\ \ \', e\<^sub>2' \ \ \ \ \, Pair v\<^sub>1 e\<^sub>2 \ m\ \ \', Pair v\<^sub>1 e\<^sub>2' \" | s_Prj1: "\ \ \, e \ m\ \ \', e' \ \ \ \ \, Prj1 e \ m\ \ \', Prj1 e' \" | s_Prj2: "\ \ \, e \ m\ \ \', e' \ \ \ \ \, Prj2 e \ m\ \ \', Prj2 e' \" | s_PrjPair1: "\ value v\<^sub>1; value v\<^sub>2 \ \ \ \, Prj1 (Pair v\<^sub>1 v\<^sub>2) \ _\ \ \, v\<^sub>1 \" | s_PrjPair2: "\ value v\<^sub>1; value v\<^sub>2 \ \ \ \, Prj2 (Pair v\<^sub>1 v\<^sub>2) \ _\ \ \, v\<^sub>2 \" | s_Unroll: "\ \, e \ m\ \ \', e' \ \ \ \, Unroll e \ m\ \ \', Unroll e' \" | s_Roll: "\ \, e \ m\ \ \', e' \ \ \ \, Roll e \ m\ \ \', Roll e' \" | s_UnrollRoll:"\ value v \ \ \ \, Unroll (Roll v) \ _\ \ \, v \" | \ \Mode-specific rules\ s_Auth: "\ \, e \ m\ \ \', e' \ \ \ \, Auth e \ m\ \ \', Auth e' \" | s_Unauth: "\ \, e \ m\ \ \', e' \ \ \ \, Unauth e \ m\ \ \', Unauth e' \" | s_AuthI: "\ value v \ \ \ \, Auth v \ I\ \ \, v \" | s_UnauthI: "\ value v \ \ \ \, Unauth v \ I\ \ \, v \" | s_AuthP: "\ closed \v\; value v \ \ \ \, Auth v \ P\ \ \, Hashed (hash \v\) v \" | s_UnauthP: "\ value v \ \ \ \, Unauth (Hashed h v) \ P\ \ \ @ [\v\], v \" | s_AuthV: "\ closed v; value v \ \ \ \, Auth v \ V\ \ \, Hash (hash v) \" | s_UnauthV: "\ closed s\<^sub>0; hash s\<^sub>0 = h \ \ \ s\<^sub>0#\, Unauth (Hash h) \ V\ \ \, s\<^sub>0 \" declare smallstep.intros[simp] declare smallstep.intros[intro] equivariance smallstep nominal_inductive smallstep avoids s_AppLam: x | s_AppRec: x | s_Let1: x | s_Let2: x by (auto simp add: fresh_Pair fresh_subst_term) inductive smallsteps :: "proofstream \ term \ mode \ nat \ proofstream \ term \ bool" ("\_, _\ _\_ \_, _\") where s_Id: "\ \, e \ _\0 \ \, e \" | s_Tr: "\ \ \\<^sub>1, e\<^sub>1 \ m\i \ \\<^sub>2, e\<^sub>2 \; \ \\<^sub>2, e\<^sub>2 \ m\ \ \\<^sub>3, e\<^sub>3 \ \ \ \ \\<^sub>1, e\<^sub>1 \ m\(i+1) \ \\<^sub>3, e\<^sub>3 \" declare smallsteps.intros[simp] declare smallsteps.intros[intro] equivariance smallsteps nominal_inductive smallsteps . lemma steps_1_step[simp]: "\ \, e \ m\1 \ \', e' \ = \ \, e \ m\ \ \', e' \" (is "?L \ ?R") proof assume ?L then show ?R proof (induct \ e m "1::nat" \' e' rule: smallsteps.induct) case (s_Tr \\<^sub>1 e\<^sub>1 m i \\<^sub>2 e\<^sub>2 \\<^sub>3 e\<^sub>3) then show ?case by (induct \\<^sub>1 e\<^sub>1 m i \\<^sub>2 e\<^sub>2 rule: smallsteps.induct) auto qed simp qed (auto intro: s_Tr[where i=0, simplified]) text \Inversion rules for smallstep(s) predicates.\ lemma value_no_step[intro]: assumes "\ \\<^sub>1, v \ m\ \ \\<^sub>2, t \" "value v" shows "False" using assms by (induct \\<^sub>1 v m \\<^sub>2 t rule: smallstep.induct) auto lemma subst_term_perm: assumes "atom x' \ (x, e)" shows "e[v / x] = ((x \ x') \ e)[v / x']" using assms [[simproc del: alpha_lst]] by (nominal_induct e avoiding: x x' v rule: term.strong_induct) (auto simp: fresh_Pair fresh_at_base(2) permute_hash_def) inductive_cases s_Unit_inv[elim]: "\ \\<^sub>1, Unit \ m\ \ \\<^sub>2, v \" inductive_cases s_App_inv[consumes 1, case_names App1 App2 AppLam AppRec, elim]: "\ \, App v\<^sub>1 v\<^sub>2 \ m\ \ \', e \" lemma s_Let_inv': assumes "\ \, Let e\<^sub>1 x e\<^sub>2 \ m\ \ \', e' \" and "atom x \ (e\<^sub>1,\)" obtains e\<^sub>1' where "(e' = e\<^sub>2[e\<^sub>1 / x] \ value e\<^sub>1 \ \ = \') \ (\ \, e\<^sub>1 \ m\ \ \', e\<^sub>1' \ \ e' = Let e\<^sub>1' x e\<^sub>2 \ \ value e\<^sub>1)" using assms [[simproc del: alpha_lst]] by (atomize_elim, induct \ "Let e\<^sub>1 x e\<^sub>2" m \' e' rule: smallstep.induct) (auto simp: fresh_Pair fresh_subst_term perm_supp_eq elim: Abs_lst1_fcb2') lemma s_Let_inv[consumes 2, case_names Let1 Let2, elim]: assumes "\ \, Let e\<^sub>1 x e\<^sub>2 \ m\ \ \', e' \" and "atom x \ (e\<^sub>1,\)" and "e' = e\<^sub>2[e\<^sub>1 / x] \ value e\<^sub>1 \ \ = \' \ Q" and "\e\<^sub>1'. \ \, e\<^sub>1 \ m\ \ \', e\<^sub>1' \ \ e' = Let e\<^sub>1' x e\<^sub>2 \ \ value e\<^sub>1 \ Q" shows "Q" using assms by (auto elim: s_Let_inv') inductive_cases s_Case_inv[consumes 1, case_names Case Inj1 Inj2, elim]: "\ \, Case e e\<^sub>1 e\<^sub>2 \ m\ \ \', e' \" inductive_cases s_Prj1_inv[consumes 1, case_names Prj1 PrjPair1, elim]: "\ \, Prj1 e \ m\ \ \', v \" inductive_cases s_Prj2_inv[consumes 1, case_names Prj2 PrjPair2, elim]: "\ \, Prj2 e \ m\ \ \', v \" inductive_cases s_Pair_inv[consumes 1, case_names Pair1 Pair2, elim]: "\ \, Pair e\<^sub>1 e\<^sub>2 \ m\ \ \', e' \" inductive_cases s_Inj1_inv[consumes 1, case_names Inj1, elim]: "\ \, Inj1 e \ m\ \ \', e' \" inductive_cases s_Inj2_inv[consumes 1, case_names Inj2, elim]: "\ \, Inj2 e \ m\ \ \', e' \" inductive_cases s_Roll_inv[consumes 1, case_names Roll, elim]: "\ \, Roll e \ m\ \ \', e' \" inductive_cases s_Unroll_inv[consumes 1, case_names Unroll UnrollRoll, elim]: "\ \, Unroll e \ m\ \ \', e' \" inductive_cases s_AuthI_inv[consumes 1, case_names Auth AuthI, elim]: "\ \, Auth e \ I\ \ \', e' \" inductive_cases s_UnauthI_inv[consumes 1, case_names Unauth UnauthI, elim]: "\ \, Unauth e \ I\ \ \', e' \" inductive_cases s_AuthP_inv[consumes 1, case_names Auth AuthP, elim]: "\ \, Auth e \ P\ \ \', e' \" inductive_cases s_UnauthP_inv[consumes 1, case_names Unauth UnauthP, elim]: "\ \, Unauth e \ P\ \ \', e' \" inductive_cases s_AuthV_inv[consumes 1, case_names Auth AuthV, elim]: "\ \, Auth e \ V\ \ \', e' \" inductive_cases s_UnauthV_inv[consumes 1, case_names Unauth UnauthV, elim]: "\ \, Unauth e \ V\ \ \', e' \" inductive_cases s_Id_inv[elim]: "\ \\<^sub>1, e\<^sub>1 \ m\0 \ \\<^sub>2, e\<^sub>2 \" inductive_cases s_Tr_inv[elim]: "\ \\<^sub>1, e\<^sub>1 \ m\i \ \\<^sub>3, e\<^sub>3 \" text \Freshness with smallstep.\ lemma fresh_smallstep_I: fixes x :: var assumes "\ \, e \ I\ \ \', e' \" "atom x \ e" shows "atom x \ e'" using assms by (induct \ e I \' e' rule: smallstep.induct) (auto simp: fresh_subst_term) lemma fresh_smallstep_P: fixes x :: var assumes "\ \, e \ P\ \ \', e' \" "atom x \ e" shows "atom x \ e'" using assms by (induct \ e P \' e' rule: smallstep.induct) (auto simp: fresh_subst_term) lemma fresh_smallsteps_I: fixes x :: var assumes "\ \, e \ I\i \ \', e' \" "atom x \ e" shows "atom x \ e'" using assms by (induct \ e I i \' e' rule: smallsteps.induct) (simp_all add: fresh_smallstep_I) lemma fresh_ps_smallstep_P: fixes x :: var assumes "\ \, e \ P\ \ \', e' \" "atom x \ e" "atom x \ \" shows "atom x \ \'" using assms proof (induct \ e P \' e' rule: smallstep.induct) case (s_UnauthP v \ h) then show ?case by (simp add: fresh_Cons fresh_append fresh_shallow) qed auto text \Proofstream lemmas.\ lemma smallstepI_ps_eq: assumes "\ \, e \ I\ \ \', e' \" shows "\ = \'" using assms by (induct \ e I \' e' rule: smallstep.induct) auto lemma smallstepI_ps_emptyD: "\\, e\ I\ \[], e'\ \ \[], e\ I\ \[], e'\" "\[], e\ I\ \\, e'\ \ \[], e\ I\ \[], e'\" using smallstepI_ps_eq by force+ lemma smallstepsI_ps_eq: assumes "\\, e\ I\i \\', e'\" shows "\ = \'" using assms by (induct \ e I i \' e' rule: smallsteps.induct) (auto dest: smallstepI_ps_eq) lemma smallstepsI_ps_emptyD: "\\, e\ I\i \[], e'\ \ \[], e\ I\i \[], e'\" "\[], e\ I\i \\, e'\ \ \[], e\ I\i \[], e'\" using smallstepsI_ps_eq by force+ lemma smallstepV_consumes_proofstream: assumes "\ \\<^sub>1, eV \ V\ \ \\<^sub>2, eV' \" obtains \ where "\\<^sub>1 = \ @ \\<^sub>2" using assms by (induct \\<^sub>1 eV V \\<^sub>2 eV' rule: smallstep.induct) auto lemma smallstepsV_consumes_proofstream: assumes "\ \\<^sub>1, eV \ V\i \ \\<^sub>2, eV' \" obtains \ where "\\<^sub>1 = \ @ \\<^sub>2" using assms by (induct \\<^sub>1 eV V i \\<^sub>2 eV' rule: smallsteps.induct) (auto elim: smallstepV_consumes_proofstream) lemma smallstepP_generates_proofstream: assumes "\ \\<^sub>1, eP \ P\ \ \\<^sub>2, eP' \" obtains \ where "\\<^sub>2 = \\<^sub>1 @ \" using assms by (induct \\<^sub>1 eP P \\<^sub>2 eP' rule: smallstep.induct) auto lemma smallstepsP_generates_proofstream: assumes "\ \\<^sub>1, eP \ P\i \ \\<^sub>2, eP' \" obtains \ where "\\<^sub>2 = \\<^sub>1 @ \" using assms by (induct \\<^sub>1 eP P i \\<^sub>2 eP' rule: smallsteps.induct) (auto elim: smallstepP_generates_proofstream) lemma smallstepV_ps_append: "\ \, eV \ V\ \ \', eV' \ \ \ \ @ X, eV \ V\ \ \' @ X, eV' \" (is "?L \ ?R") proof (rule iffI) assume ?L then show ?R by (nominal_induct \ eV V \' eV' avoiding: X rule: smallstep.strong_induct) (auto simp: fresh_append fresh_Pair) next assume ?R then show ?L by (nominal_induct "\ @ X" eV V "\' @ X" eV' avoiding: X rule: smallstep.strong_induct) (auto simp: fresh_append fresh_Pair) qed lemma smallstepV_ps_to_suffix: assumes "\\, e\ V\ \\' @ X, e'\" obtains \'' where "\ = \'' @ X" using assms by (induct \ e V "\' @ X" e' rule: smallstep.induct) auto lemma smallstepsV_ps_append: "\ \, eV \ V\i \ \', eV' \ \ \ \ @ X, eV \ V\i \ \' @ X, eV' \" (is "?L \ ?R") proof (rule iffI) assume ?L then show ?R proof (induct \ eV V i \' eV' rule: smallsteps.induct) case (s_Tr \\<^sub>1 e\<^sub>1 i \\<^sub>2 e\<^sub>2 \\<^sub>3 e\<^sub>3) then show ?case by (auto simp: iffD1[OF smallstepV_ps_append]) qed simp next assume ?R then show ?L proof (induct "\ @ X" eV V i "\' @ X" eV' arbitrary: \' rule: smallsteps.induct) case (s_Tr e\<^sub>1 i \\<^sub>2 e\<^sub>2 e\<^sub>3) from s_Tr(3) obtain \''' where "\\<^sub>2 = \''' @ X" by (auto elim: smallstepV_ps_to_suffix) with s_Tr show ?case by (auto dest: iffD2[OF smallstepV_ps_append]) qed simp qed lemma smallstepP_ps_prepend: "\ \, eP \ P\ \ \', eP' \ \ \ X @ \, eP \ P\ \ X @ \', eP' \" (is "?L \ ?R") proof (rule iffI) assume ?L then show ?R proof (nominal_induct \ eP P \' eP' avoiding: X rule: smallstep.strong_induct) case (s_UnauthP v \ h) then show ?case by (subst append_assoc[symmetric, of X \ "[\v\]"]) (erule smallstep.s_UnauthP) qed (auto simp: fresh_append fresh_Pair) next assume ?R then show ?L by (nominal_induct "X @ \" eP P "X @ \'" eP' avoiding: X rule: smallstep.strong_induct) (auto simp: fresh_append fresh_Pair) qed lemma smallstepsP_ps_prepend: "\ \, eP \ P\i \ \', eP' \ \ \ X @ \, eP \ P\i \ X @ \', eP' \" (is "?L \ ?R") proof (rule iffI) assume ?L then show ?R proof (induct \ eP P i \' eP' rule: smallsteps.induct) case (s_Tr \\<^sub>1 e\<^sub>1 i \\<^sub>2 e\<^sub>2 \\<^sub>3 e\<^sub>3) then show ?case by (auto simp: iffD1[OF smallstepP_ps_prepend]) qed simp next assume ?R then show ?L proof (induct "X @ \" eP P i "X @ \'" eP' arbitrary: \' rule: smallsteps.induct) case (s_Tr e\<^sub>1 i \\<^sub>2 e\<^sub>2 e\<^sub>3) then obtain \'' where \'': "\\<^sub>2 = X @ \ @ \''" by (auto elim: smallstepsP_generates_proofstream) then have "\\, e\<^sub>1\ P\i \\ @ \'', e\<^sub>2\" by (auto dest: s_Tr(2)) with \'' s_Tr(1,3) show ?case by (auto dest: iffD2[OF smallstepP_ps_prepend]) qed simp qed subsection \Type Progress\ lemma type_progress: assumes "{$$} \\<^sub>W e : \" shows "value e \ (\e'. \ [], e \ I\ \ [], e' \)" using assms proof (nominal_induct "{$$} :: tyenv" e \ rule: judge_weak.strong_induct) case (jw_Let x e\<^sub>1 \\<^sub>1 e\<^sub>2 \\<^sub>2) then show ?case by (auto 0 3 simp: fresh_smallstep_I elim!: s_Let2[of e\<^sub>2] intro: exI[where P="\e. \_, _\ _\ \_, e\", OF s_Let1, rotated]) next case (jw_Prj1 v \\<^sub>1 \\<^sub>2) then show ?case by (auto elim!: jw_Prod_inv[of v \\<^sub>1 \\<^sub>2]) next case (jw_Prj2 v \\<^sub>1 \\<^sub>2) then show ?case by (auto elim!: jw_Prod_inv[of v \\<^sub>1 \\<^sub>2]) next case (jw_App e \\<^sub>1 \\<^sub>2 e') then show ?case by (auto 0 4 elim: jw_Fun_inv[of _ _ _ e']) next case (jw_Case v v\<^sub>1 v\<^sub>2 \\<^sub>1 \\<^sub>2 \) then show ?case by (auto 0 4 elim: jw_Sum_inv[of _ v\<^sub>1 v\<^sub>2]) qed fast+ subsection \Weak Type Preservation\ lemma fresh_tyenv_None: fixes \ :: tyenv shows "atom x \ \ \ \ $$ x = None" (is "?L \ ?R") proof assume assm: ?L show ?R proof (rule ccontr) assume "\ $$ x \ None" then obtain \ where "\ $$ x = Some \" by blast with assm have "\a :: var. atom a \ \ \ \ $$ a = Some \" using fmap_freshness_lemma_unique[OF exI, of x \] by (simp add: fresh_Pair fresh_Some) metis then have "{a :: var. atom a \ \} \ fmdom' \" by (auto simp: image_iff Ball_def fmlookup_dom'_iff) moreover { assume "infinite {a :: var. \ atom a \ \}" then have "infinite {a :: var. atom a \ supp \}" unfolding fresh_def by auto then have "infinite (supp \)" by (rule contrapos_nn) (auto simp: image_iff inv_f_f[of atom] inj_on_def elim!: finite_surj[of _ _ "inv atom"] bexI[rotated]) then have False using finite_supp[of \] by blast } then have "infinite {a :: var. atom a \ \}" by auto ultimately show False using finite_subset[of "{a. atom a \ \}" "fmdom' \"] unfolding fmdom'_alt_def by auto qed next assume ?R then show ?L proof (induct \ arbitrary: x) case (fmupd y z \) then show ?case by (cases "y = x") (auto intro: fresh_fmap_update) qed simp qed lemma judge_weak_fresh_env_fresh_term[dest]: fixes a :: var assumes "\ \\<^sub>W e : \" "atom a \ \" shows "atom a \ e" using assms proof (nominal_induct \ e \ avoiding: a rule: judge_weak.strong_induct) case (jw_Var \ x \) then show ?case by (cases "a = x") (auto simp: fresh_tyenv_None) qed (simp_all add: fresh_Cons fresh_fmap_update) lemma judge_weak_weakening_1: assumes "\ \\<^sub>W e : \" "atom y \ e" shows "\(y $$:= \') \\<^sub>W e : \" using assms proof (nominal_induct \ e \ avoiding: y \' rule: judge_weak.strong_induct) case (jw_Lam x \ \\<^sub>1 e \\<^sub>2) from jw_Lam(5)[of y \'] jw_Lam(1-4,6) show ?case by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update) next case (jw_App v v' \ \\<^sub>1 \\<^sub>2) then show ?case by (force simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update) next case (jw_Let x \ e\<^sub>1 \\<^sub>1 e\<^sub>2 \\<^sub>2) from jw_Let(6)[of y \'] jw_Let(8)[of y \'] jw_Let(1-5,7,9) show ?case by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update) next case (jw_Rec x \ z \\<^sub>1 \\<^sub>2 e') from jw_Rec(9)[of y \'] jw_Rec(1-8,10) show ?case by (auto simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update fresh_Pair) next case (jw_Case v v\<^sub>1 v\<^sub>2 \ \\<^sub>1 \\<^sub>2 \) then show ?case by (fastforce simp add: fresh_at_base fmupd_reorder_neq fresh_fmap_update) next case (jw_Roll \ \ v \) then show ?case by (simp add: fresh_fmap_update) next case (jw_Unroll \ \ v \) then show ?case by (simp add: fresh_fmap_update) qed auto lemma judge_weak_weakening_2: assumes "\ \\<^sub>W e : \" "atom y \ \" shows "\(y $$:= \') \\<^sub>W e : \" proof - from assms have "atom y \ e" by (rule judge_weak_fresh_env_fresh_term) with assms show "\(y $$:= \') \\<^sub>W e : \" by (simp add: judge_weak_weakening_1) qed lemma judge_weak_weakening_env: assumes "{$$} \\<^sub>W e : \" shows "\ \\<^sub>W e : \" using assms proof (induct \) case fmempty then show ?case by assumption next case (fmupd x y \) then show ?case by (simp add: fresh_tyenv_None judge_weak_weakening_2) qed lemma value_subst_value: assumes "value e" "value e'" shows "value (e[e' / x])" using assms by (induct e e' x rule: subst_term.induct) auto lemma judge_weak_subst[intro]: assumes "\(a $$:= \') \\<^sub>W e : \" "{$$} \\<^sub>W e' : \'" shows "\ \\<^sub>W e[e' / a] : \" using assms proof (nominal_induct "\(a $$:= \')" e \ avoiding: a e' \ rule: judge_weak.strong_induct) case (jw_Var x \) then show ?case by (auto simp: judge_weak_weakening_env) next case (jw_Lam x \\<^sub>1 e \\<^sub>2) then show ?case by (fastforce simp: fmupd_reorder_neq) next case (jw_Rec x y \\<^sub>1 \\<^sub>2 e) then show ?case by (fastforce simp: fmupd_reorder_neq) next case (jw_Let x e\<^sub>1 \\<^sub>1 e\<^sub>2 \\<^sub>2) then show ?case by (fastforce simp: fmupd_reorder_neq) qed fastforce+ lemma type_preservation: assumes "\ [], e \ I\ \ [], e' \" "{$$} \\<^sub>W e : \" shows "{$$} \\<^sub>W e' : \" using assms [[simproc del: alpha_lst]] proof (nominal_induct "[]::proofstream" e I "[]::proofstream" e' arbitrary: \ rule: smallstep.strong_induct) case (s_AppLam v x e) then show ?case by force next case (s_AppRec v x e) then show ?case by (elim jw_App_inv jw_Rec_inv) (auto 0 3 simp del: subst_term.simps) next case (s_Let1 x e\<^sub>1 e\<^sub>1' e\<^sub>2) from s_Let1(1,2,7) show ?case by (auto intro: s_Let1(6) del: jw_Let_inv elim!: jw_Let_inv) next case (s_Unroll e e') then obtain \::tvar where "atom \ \ \" using obtain_fresh by blast with s_Unroll show ?case by (auto elim: jw_Unroll_inv[where \ = \]) next case (s_Roll e e') then obtain \::tvar where "atom \ \ \" using obtain_fresh by blast with s_Roll show ?case by (auto elim: jw_Roll_inv[where \ = \]) next case (s_UnrollRoll v) then obtain \::tvar where "atom \ \ \" using obtain_fresh by blast with s_UnrollRoll show ?case by (fastforce simp: Abs1_eq(3) elim: jw_Roll_inv[where \ = \] jw_Unroll_inv[where \ = \]) qed fastforce+ subsection \Corrected Lemma 1 from Miller et al.~\cite{adsg}: Weak Type Soundness\ lemma type_soundness: assumes "{$$} \\<^sub>W e : \" shows "value e \ (\e'. \ [], e \ I\ \ [], e' \ \ {$$} \\<^sub>W e' : \)" proof (cases "value e") case True then show ?thesis by simp next case False with assms obtain e' where "\[], e\ I\ \[], e'\" by (auto dest: type_progress) with assms show ?thesis by (auto simp: type_preservation) qed (*<*) end (*>*)