diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 0000000..392c1b2 --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,35 @@ +name: Build +on: + push: + paths-ignore: + - '**.md' + +jobs: + build: + name: build + runs-on: ubuntu-18.04 + steps: + - name: Checkout repo + uses: actions/checkout@v2 + + - name: Setup buildx + uses: crazy-max/ghaction-docker-buildx@v3 + + - name: Cache docker layers + uses: actions/cache@v1 + with: + path: /tmp/docker-cache + key: docker-cache-${{ hashFiles('Dockerfile') }}-1 + restore-keys: | + docker-cache- + + - name: Build Nominal Isabelle + run: | + docker buildx build \ + --cache-from "type=local,src=/tmp/docker-cache" \ + --cache-to "type=local,dest=/tmp/docker-cache,mode=max" \ + --output "type=docker" \ + --tag isabelle_nominal:latest . + + - name: Run theories + run: docker run isabelle_nominal build -d . Lambda diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..ecd5bb9 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,15 @@ +FROM makarius/isabelle:Isabelle2020 + +RUN for t in Nominal2 FinFun; do \ + curl https://www.isa-afp.org/release/afp-$t-current.tar.gz -o $t.tar.gz ; \ + cd Isabelle/src/ ; \ + tar -xzf ../../$t.tar.gz ; \ + cd .. ; \ + echo "src/$t" >> ROOTS ; \ + cd .. ; \ + rm $t.tar.gz ; \ + done + +RUN ./Isabelle/bin/isabelle build -o system_heaps -b Nominal2 + +COPY ROOT Defs.thy Soundness.thy ./ diff --git a/ROOT b/ROOT new file mode 100644 index 0000000..5c6dd91 --- /dev/null +++ b/ROOT @@ -0,0 +1,4 @@ +session Lambda = HOL + sessions "HOL-Eisbach" Nominal2 +theories + Defs + Soundness diff --git a/Soundness.thy b/Soundness.thy index e218a98..ec9b60a 100644 --- a/Soundness.thy +++ b/Soundness.thy @@ -2,65 +2,65 @@ theory Soundness imports Defs begin -lemma context_invariance: "⟦ Γ ⊢ e : τ ; ∀x τ'. atom x ∈ fv_term e ∧ (x, τ') ∈ Γ ⟶ (x, τ') ∈ Γ' ⟧ ⟹ Γ' ⊢ e : τ" -proof(nominal_induct Γ e τ avoiding: Γ' rule: T.strong_induct) - case (T_UnitI Γ) +lemma context_invariance: "\ \ \ e : \ ; \x \'. atom x \ fv_term e \ (x, \') \ \ \ (x, \') \ \' \ \ \' \ e : \" +proof(nominal_induct \ e \ avoiding: \' rule: T.strong_induct) + case (T_UnitI \) then show ?case using T.T_UnitI by simp next - case (T_VarI x τ Γ) + case (T_VarI x \ \) then show ?case using T.T_VarI supp_at_base by fastforce next - case (T_AbsI x Γ τ1 e τ2) + case (T_AbsI x \ \1 e \2) then show ?case using T.T_AbsI by fastforce next - case (T_AppI Γ e1 τ1 τ2 e2) + case (T_AppI \ e1 \1 \2 e2) then show ?case by (metis T.T_AppI Un_iff term.fv_defs(3)) next - case (T_LetI x Γ e1 τ1 e2 τ2) - then have 1: "atom x ♯ (Γ', e1)" by simp - from T_LetI have 2: "(x, τ1) # Γ' ⊢ e2 : τ2" by simp + case (T_LetI x \ e1 \1 e2 \2) + then have 1: "atom x \ (\', e1)" by simp + from T_LetI have 2: "(x, \1) # \' \ e2 : \2" by simp show ?case using T.T_LetI[OF 1 2] using T_LetI by simp qed -lemma free_in_context: "⟦ Γ ⊢ e : τ ; atom x ∈ fv_term e ⟧ ⟹ ∃τ'. (x, τ') ∈ Γ" -proof(nominal_induct Γ e τ avoiding: x rule: T.strong_induct) - case (T_UnitI Γ) +lemma free_in_context: "\ \ \ e : \ ; atom x \ fv_term e \ \ \\'. (x, \') \ \" +proof(nominal_induct \ e \ avoiding: x rule: T.strong_induct) + case (T_UnitI \) then show ?case by simp next - case (T_VarI x' τ Γ) + case (T_VarI x' \ \) then show ?case by (metis atom_eq_iff singletonD supp_at_base term.fv_defs(1)) next - case (T_AbsI x' Γ τ1 e τ2) + case (T_AbsI x' \ \1 e \2) then show ?case by (metis Diff_iff Un_iff fresh_def insert_iff isin.simps(2) list.set(2) no_vars_in_ty term.fv_defs(2)) next - case (T_AppI Γ e1 τ1 τ2 e2) + case (T_AppI \ e1 \1 \2 e2) then show ?case by auto next - case (T_LetI x' Γ e1 τ1 e2 τ2) + case (T_LetI x' \ e1 \1 e2 \2) then show ?case by (metis Diff_iff UnE fresh_at_base(2) isin.simps(2) term.fv_defs(5)) qed -lemma fresh_term[simp]: "⟦ Γ ⊢ e : τ ; atom x ♯ Γ ⟧ ⟹ atom x ♯ e" - apply (nominal_induct Γ e τ avoiding: x rule: T.strong_induct) +lemma fresh_term[simp]: "\ \ \ e : \ ; atom x \ \ \ \ atom x \ e" + apply (nominal_induct \ e \ avoiding: x rule: T.strong_induct) apply (auto simp: fresh_Cons) using fresh_ineq_at_base fresh_not_isin apply force done -lemma fun_ty_lam: "⟦ Γ ⊢ e : τ1 → τ2 ; is_v_of_e e ⟧ ⟹ ∃x e'. e = (λx:τ1. e')" - by (nominal_induct Γ e "τ1 → τ2" rule: T.strong_induct) auto +lemma fun_ty_lam: "\ \ \ e : \1 \ \2 ; is_v_of_e e \ \ \x e'. e = (\x:\1. e')" + by (nominal_induct \ e "\1 \ \2" rule: T.strong_induct) auto -theorem progress: "[] ⊢ e : τ ⟹ is_v_of_e e ∨ (∃e'. Step e e')" -proof (induction "[] :: Γ" e τ rule: T.induct) +theorem progress: "[] \ e : \ \ is_v_of_e e \ (\e'. Step e e')" +proof (induction "[] :: \" e \ rule: T.induct) case T_UnitI then show ?case by simp next - case (T_VarI x τ) + case (T_VarI x \) then show ?case by simp next - case (T_AbsI x τ1 e τ2) + case (T_AbsI x \1 e \2) then show ?case by simp next - case (T_AppI e1 τ1 τ2 e2) + case (T_AppI e1 \1 \2 e2) note IH1 = T_AppI(2) note IH2 = T_AppI(4) @@ -70,103 +70,103 @@ next from IH2 show ?thesis proof (elim disjE) assume "is_v_of_e e2" - from ‹is_v_of_e e1› T_AppI(1) have "∃x e. e1 = (λx:τ1. e)" by (simp add: fun_ty_lam) - then have "∃e'. Step (App e1 e2) e'" using ‹is_v_of_e e2› ST_BetaI by blast + from \is_v_of_e e1\ T_AppI(1) have "\x e. e1 = (\x:\1. e)" by (simp add: fun_ty_lam) + then have "\e'. Step (App e1 e2) e'" using \is_v_of_e e2\ ST_BetaI by blast then show ?thesis by simp next - assume "∃e2'. Step e2 e2'" - then show ?thesis using ST_App2I ‹is_v_of_e e1› by blast + assume "\e2'. Step e2 e2'" + then show ?thesis using ST_App2I \is_v_of_e e1\ by blast qed next - assume "∃e1'. Step e1 e1'" + assume "\e1'. Step e1 e1'" then obtain e1' where "Step e1 e1'" by blast then have "Step (App e1 e2) (App e1' e2)" by (rule ST_AppI) then show ?thesis by blast qed next - case (T_LetI e1 τ1 x e2 τ2) + case (T_LetI e1 \1 x e2 \2) then show ?case using ST_SubstI ST_LetI by blast qed -lemma swap_term: "⟦ Γ ⊢ e : τ ; atom y ♯ Γ ⟧ ⟹ ((x ↔ y) ∙ Γ) ⊢ (x ↔ y) ∙ e : τ" -proof (nominal_induct Γ e τ avoiding: x y rule: T.strong_induct) - case (T_UnitI Γ) +lemma swap_term: "\ \ \ e : \ ; atom y \ \ \ \ ((x \ y) \ \) \ (x \ y) \ e : \" +proof (nominal_induct \ e \ avoiding: x y rule: T.strong_induct) + case (T_UnitI \) then show ?case by (simp add: T.T_UnitI) next - case (T_VarI z τ Γ) + case (T_VarI z \ \) then show ?case by (metis T.T_VarI T.eqvt flip_fresh_fresh no_vars_in_ty) next - case (T_AbsI x Γ τ1 e τ2) + case (T_AbsI x \ \1 e \2) then show ?case by (metis T.T_AbsI T.eqvt flip_fresh_fresh no_vars_in_ty) next - case (T_AppI Γ e1 τ1 τ2 e2) + case (T_AppI \ e1 \1 \2 e2) then show ?case using T.T_AppI by fastforce next - case (T_LetI z Γ e1 τ1 e2 τ2) - then have 1: "atom y ♯ (z, τ1) # Γ" by (simp add: fresh_Cons fresh_at_base(2)) + case (T_LetI z \ e1 \1 e2 \2) + then have 1: "atom y \ (z, \1) # \" by (simp add: fresh_Cons fresh_at_base(2)) - from T_LetI have e1: "atom z ♯ (x ↔ y) ∙ e1" by (smt eq_eqvt flip_def fresh_at_base(2) fresh_eqvt swap_atom_simps(3)) - from T_LetI have "atom z ♯ (x ↔ y) ∙ Γ" by (metis flip_def fresh_at_base(2) fresh_permute_iff swap_atom_simps(3)) - then have 2: "atom z ♯ ((x ↔ y) ∙ Γ, (x ↔ y) ∙ e1)" using T_LetI e1 by simp + from T_LetI have e1: "atom z \ (x \ y) \ e1" by (smt eq_eqvt flip_def fresh_at_base(2) fresh_eqvt swap_atom_simps(3)) + from T_LetI have "atom z \ (x \ y) \ \" by (metis flip_def fresh_at_base(2) fresh_permute_iff swap_atom_simps(3)) + then have 2: "atom z \ ((x \ y) \ \, (x \ y) \ e1)" using T_LetI e1 by simp - from T_LetI have "(x ↔ y) ∙ ((z, τ1) # Γ) = (z, τ1)#((x ↔ y) ∙ Γ)" by (simp add: flip_fresh_fresh fresh_at_base(2)) - then have 3: "(z, τ1) # (x ↔ y) ∙ Γ ⊢ (x ↔ y) ∙ e2 : τ2" using T_LetI(6)[OF 1, of x] by simp + from T_LetI have "(x \ y) \ ((z, \1) # \) = (z, \1)#((x \ y) \ \)" by (simp add: flip_fresh_fresh fresh_at_base(2)) + then have 3: "(z, \1) # (x \ y) \ \ \ (x \ y) \ e2 : \2" using T_LetI(6)[OF 1, of x] by simp - show ?case using T.T_LetI[OF 2 3 T_LetI(8)[OF ‹atom y ♯ Γ›, of x]] + show ?case using T.T_LetI[OF 2 3 T_LetI(8)[OF \atom y \ \\, of x]] by (smt "1" T_LetI.hyps(1) flip_fresh_fresh fresh_Cons fresh_PairD(1) fresh_at_base(2) term.perm_simps(5)) qed lemma T_Abs_Inv: - assumes a: "Γ ⊢ (λx : τ1 . e) : τ" and b: "atom x ♯ Γ" - shows "∃τ2. (x, τ1)#Γ ⊢ e : τ2 ∧ τ = (τ1 → τ2)" + assumes a: "\ \ (\x : \1 . e) : \" and b: "atom x \ \" + shows "\\2. (x, \1)#\ \ e : \2 \ \ = (\1 \ \2)" proof (cases rule: T.cases[OF a]) - case (3 x' Γ' τ1' e' τ2) + case (3 x' \' \1' e' \2) then show ?thesis proof (cases "atom x' = atom x") case True then show ?thesis by (metis "3"(1) "3"(2) "3"(3) "3"(5) Abs1_eq_iff(3) atom_eq_iff term.eq_iff(2)) next case False - then have 1: "atom x ♯ (x', τ1') # Γ'" using b by (simp add: 3 fresh_Cons) - have 2: "((x' ↔ x) ∙ ((x', τ1) # Γ)) ⊢ (x' ↔ x) ∙ e' : τ2" using swap_term[OF "3"(5) 1, of x'] 3 by auto + then have 1: "atom x \ (x', \1') # \'" using b by (simp add: 3 fresh_Cons) + have 2: "((x' \ x) \ ((x', \1) # \)) \ (x' \ x) \ e' : \2" using swap_term[OF "3"(5) 1, of x'] 3 by auto - have 4: "(x' ↔ x) ∙ e' = e" by (metis "3"(2) Abs1_eq_iff(3) False flip_commute term.eq_iff(2)) - have 5: "((x' ↔ x) ∙ ((x', τ1) # Γ)) = (x, τ1)#Γ" by (smt "3"(1) "3"(4) Cons_eqvt Pair_eqvt b flip_at_simps(1) flip_fresh_fresh no_vars_in_ty) + have 4: "(x' \ x) \ e' = e" by (metis "3"(2) Abs1_eq_iff(3) False flip_commute term.eq_iff(2)) + have 5: "((x' \ x) \ ((x', \1) # \)) = (x, \1)#\" by (smt "3"(1) "3"(4) Cons_eqvt Pair_eqvt b flip_at_simps(1) flip_fresh_fresh no_vars_in_ty) from 2 3 4 5 show ?thesis by auto qed qed simp_all lemma T_Let_Inv: - assumes a: "Γ ⊢ Let x e1 e2 : τ" and b: "atom x ♯ Γ" - shows "∃τ1. Γ ⊢ e1 : τ1 ∧ (x, τ1)#Γ ⊢ e2 : τ" + assumes a: "\ \ Let x e1 e2 : \" and b: "atom x \ \" + shows "\\1. \ \ e1 : \1 \ (x, \1)#\ \ e2 : \" proof (cases rule: T.cases[OF a]) - case (5 x' Γ' _ τ1 e2' τ2) + case (5 x' \' _ \1 e2' \2) show ?thesis proof (cases "atom x' = atom x") case True then show ?thesis by (metis "5"(1) "5"(2) "5"(3) "5"(5) "5"(6) Abs1_eq_iff(3) atom_eq_iff term.eq_iff(5)) next case False - then have 1: "atom x ♯ (x', τ1) # Γ'" using b by (simp add: 5 fresh_Cons) - have 2: "((x' ↔ x) ∙ ((x', τ1)#Γ)) ⊢ (x' ↔ x) ∙ e2' : τ" using swap_term[OF "5"(5) 1, of x'] 5 by blast + then have 1: "atom x \ (x', \1) # \'" using b by (simp add: 5 fresh_Cons) + have 2: "((x' \ x) \ ((x', \1)#\)) \ (x' \ x) \ e2' : \" using swap_term[OF "5"(5) 1, of x'] 5 by blast - have 3: "(x' ↔ x) ∙ e2' = e2" by (metis "5"(2) Abs1_eq_iff(3) False flip_commute term.eq_iff(5)) - have 4: "((x' ↔ x) ∙ ((x', τ1) # Γ)) = (x, τ1)#Γ" by (smt "5"(1) "5"(4) Cons_eqvt Pair_eqvt b flip_at_simps(1) flip_fresh_fresh fresh_PairD(1) no_vars_in_ty) + have 3: "(x' \ x) \ e2' = e2" by (metis "5"(2) Abs1_eq_iff(3) False flip_commute term.eq_iff(5)) + have 4: "((x' \ x) \ ((x', \1) # \)) = (x, \1)#\" by (smt "5"(1) "5"(4) Cons_eqvt Pair_eqvt b flip_at_simps(1) flip_fresh_fresh fresh_PairD(1) no_vars_in_ty) from 2 3 4 5 show ?thesis by auto qed qed simp_all -lemma substitution: "⟦ (x, τ')#Γ ⊢ e : τ ; [] ⊢ v : τ' ⟧ ⟹ Γ ⊢ subst_term v x e : τ" -proof (nominal_induct e avoiding: Γ τ v x τ' rule: term.strong_induct) +lemma substitution: "\ (x, \')#\ \ e : \ ; [] \ v : \' \ \ \ \ subst_term v x e : \" +proof (nominal_induct e avoiding: \ \ v x \' rule: term.strong_induct) case (Var y) then show ?case proof (cases "x = y") case True - then have "τ = τ'" using Var T.cases by fastforce + then have "\ = \'" using Var T.cases by fastforce then show ?thesis using True Var context_invariance by fastforce next case False @@ -174,53 +174,53 @@ proof (nominal_induct e avoiding: Γ τ v x τ' rule: term.strong_induct) by (metis (no_types, lifting) Rep_name_inverse atom_name_def subst_term.simps(1) isin.simps(2) singletonD supp_at_base term.fv_defs(1)) qed next - case (Lam y σ e) - then obtain τ2 where P: "(y, σ)#(x, τ')#Γ ⊢ e : τ2 ∧ τ = (σ → τ2)" using T_Abs_Inv[OF Lam(7)] fresh_Cons fresh_Pair by blast - then have "(x, τ')#(y, σ)#Γ ⊢ e : τ2" using context_invariance ‹atom y ♯ x› by auto + case (Lam y \ e) + then obtain \2 where P: "(y, \)#(x, \')#\ \ e : \2 \ \ = (\ \ \2)" using T_Abs_Inv[OF Lam(7)] fresh_Cons fresh_Pair by blast + then have "(x, \')#(y, \)#\ \ e : \2" using context_invariance \atom y \ x\ by auto then show ?case using Lam T_AbsI P by simp next case (App e1 e2) - obtain τ1 where P: "((x, τ') # Γ ⊢ e1 : τ1 → τ) ∧ ((x, τ') # Γ ⊢ e2 : τ1)" using T.cases[OF App(3)] by fastforce + obtain \1 where P: "((x, \') # \ \ e1 : \1 \ \) \ ((x, \') # \ \ e2 : \1)" using T.cases[OF App(3)] by fastforce then show ?case using T_AppI App by fastforce next case Unit then show ?case using T.cases[OF Unit(1)] T_UnitI by auto next case (Let y e1 e2) - have "atom y ♯ e1" using Let.hyps(1) Let.hyps(4) Let.prems(1) T_Let_Inv fresh_Cons fresh_Pair fresh_term no_vars_in_ty by blast - then have "atom y ♯ subst_term v x e1" by (simp add: Let.hyps(3) fresh_subst_term) - then have 0: "atom y ♯ (Γ, subst_term v x e1)" using Let fresh_Pair by simp + have "atom y \ e1" using Let.hyps(1) Let.hyps(4) Let.prems(1) T_Let_Inv fresh_Cons fresh_Pair fresh_term no_vars_in_ty by blast + then have "atom y \ subst_term v x e1" by (simp add: Let.hyps(3) fresh_subst_term) + then have 0: "atom y \ (\, subst_term v x e1)" using Let fresh_Pair by simp - obtain τ1 where P: "(x, τ')#Γ ⊢ e1 : τ1 ∧ (y, τ1)#(x, τ')#Γ ⊢ e2 : τ" using T_Let_Inv[OF Let(8)] Let fresh_Cons fresh_Pair by blast - then have 1: "(x, τ')#(y, τ1)#Γ ⊢ e2 : τ" using context_invariance Let(4) by force - from P have 2: "(x, τ')#Γ ⊢ e1 : τ1" by simp + obtain \1 where P: "(x, \')#\ \ e1 : \1 \ (y, \1)#(x, \')#\ \ e2 : \" using T_Let_Inv[OF Let(8)] Let fresh_Cons fresh_Pair by blast + then have 1: "(x, \')#(y, \1)#\ \ e2 : \" using context_invariance Let(4) by force + from P have 2: "(x, \')#\ \ e1 : \1" by simp - have 3: "Γ ⊢ subst_term v x e1 : τ1" using Let(6)[OF 2 Let(9)] . - have 4: "(y, τ1)#Γ ⊢ subst_term v x e2 : τ" using Let(7)[OF 1 Let(9)] . + have 3: "\ \ subst_term v x e1 : \1" using Let(6)[OF 2 Let(9)] . + have 4: "(y, \1)#\ \ subst_term v x e2 : \" using Let(7)[OF 1 Let(9)] . show ?case using T_LetI[OF 0 4 3] using Let by simp qed -theorem preservation: "⟦ [] ⊢ e : τ ; Step e e' ⟧ ⟹ [] ⊢ e' : τ" -proof (nominal_induct "[] :: Γ" e τ arbitrary: e' rule: T.strong_induct) +theorem preservation: "\ [] \ e : \ ; Step e e' \ \ [] \ e' : \" +proof (nominal_induct "[] :: \" e \ arbitrary: e' rule: T.strong_induct) case T_UnitI then show ?case using Step.cases by fastforce next - case (T_VarI x τ) + case (T_VarI x \) then show ?case by simp next - case (T_AbsI x τ1 e τ2) + case (T_AbsI x \1 e \2) then show ?case using Step.cases by fastforce next - case (T_AppI e1 τ1 τ2 e2) - from ‹App e1 e2 ⟶ e'› show ?case + case (T_AppI e1 \1 \2 e2) + from \App e1 e2 \ e'\ show ?case proof cases - case (ST_BetaI x τ e) - then have "τ = τ1" using T_AppI.hyps(1) fun_ty_lam is_v_of_e.simps(2) term.eq_iff(2) by blast - then have 1: "[] ⊢ e2 : τ" using T_AppI(3) by simp + case (ST_BetaI x \ e) + then have "\ = \1" using T_AppI.hyps(1) fun_ty_lam is_v_of_e.simps(2) term.eq_iff(2) by blast + then have 1: "[] \ e2 : \" using T_AppI(3) by simp - have "[] ⊢ λ x : τ . e : τ1 → τ2" using T_AppI ST_BetaI by blast - then have 2: "[(x, τ)] ⊢ e : τ2" using T_Abs_Inv fresh_Nil by fastforce + have "[] \ \ x : \ . e : \1 \ \2" using T_AppI ST_BetaI by blast + then have 2: "[(x, \)] \ e : \2" using T_Abs_Inv fresh_Nil by fastforce show ?thesis using substitution[OF 2 1] ST_BetaI by simp next @@ -231,8 +231,8 @@ next then show ?thesis using T_AppI T.T_AppI by blast qed next - case (T_LetI x e1 τ1 e2 τ2) - from ‹Let x e1 e2 ⟶ e'› show ?case + case (T_LetI x e1 \1 e2 \2) + from \Let x e1 e2 \ e'\ show ?case proof cases case (ST_SubstI y e) @@ -242,9 +242,9 @@ next then show ?thesis by (metis Abs1_eq(3) T_LetI.hyps(3) T_LetI.hyps(4) atom_eq_iff local.ST_SubstI(1) local.ST_SubstI(2) substitution) next case False - then have 1: "atom y ♯ [(x, τ1)]" by (simp add: fresh_Cons fresh_Nil) - have "(x ↔ y) ∙ e2 = e" by (metis Abs1_eq_iff'(3) False flip_commute local.ST_SubstI(1)) - then have "[(y, τ1)] ⊢ e : τ2" using swap_term[OF T_LetI(3) 1, of x] by (simp add: flip_fresh_fresh) + then have 1: "atom y \ [(x, \1)]" by (simp add: fresh_Cons fresh_Nil) + have "(x \ y) \ e2 = e" by (metis Abs1_eq_iff'(3) False flip_commute local.ST_SubstI(1)) + then have "[(y, \1)] \ e : \2" using swap_term[OF T_LetI(3) 1, of x] by (simp add: flip_fresh_fresh) then show ?thesis using T_LetI ST_SubstI substitution by auto qed next @@ -253,18 +253,18 @@ next qed qed -definition stuck :: "term ⇒ bool" where - "stuck e ≡ ¬(is_v_of_e e ∨ (∃e'. Step e e'))" +definition stuck :: "term \ bool" where + "stuck e \ \(is_v_of_e e \ (\e'. Step e e'))" -inductive Steps :: "term ⇒ term ⇒ bool" (infix "⟶*" 70) where +inductive Steps :: "term \ term \ bool" (infix "\*" 70) where refl: "Steps e e" -| trans: "⟦ Steps e1 e2 ; Step e2 e3 ⟧ ⟹ Steps e1 e3" +| trans: "\ Steps e1 e2 ; Step e2 e3 \ \ Steps e1 e3" -lemma multi_preservation: "⟦ e ⟶* e' ; [] ⊢ e : τ ⟧ ⟹ [] ⊢ e' : τ" +lemma multi_preservation: "\ e \* e' ; [] \ e : \ \ \ [] \ e' : \" apply (induction e e' rule: Steps.induct) using preservation by blast+ -corollary soundness: "⟦ [] ⊢ e : τ ; e ⟶* e' ⟧ ⟹ ¬(stuck e')" +corollary soundness: "\ [] \ e : \ ; e \* e' \ \ \(stuck e')" unfolding stuck_def using progress multi_preservation by blast